[ cleanup ] Cleaning up the use of applicative syntax

src/Compiler/Common.idr

@@ -354,7 +354,7 @@ getCompileDataWith exports doLazyAnnots phase_in tm_in
                       ldefs ++ concat lifted_in
 
          anf <- if phase >= ANF
-                   then logTime 2 "Get ANF" $ traverse (\ (n, d) => pure (n, !(toANF d))) lifted
+                   then logTime 2 "Get ANF" $ traverse (traversePair toANF) lifted
                    else pure []
          vmcode <- if phase >= VMCode
                       then logTime 2 "Get VM Code" $ pure (allDefs anf)
@@ -440,7 +440,7 @@ getIncCompileData doLazyAnnots phase
                          else pure []
          let lifted = concat lifted_in
          anf <- if phase >= ANF
-                   then logTime 2 "Get ANF" $ traverse (\ (n, d) => pure (n, !(toANF d))) lifted
+                   then logTime 2 "Get ANF" $ traverse (traversePair toANF) lifted
                    else pure []
          vmcode <- if phase >= VMCode
                       then logTime 2 "Get VM Code" $ pure (allDefs anf)

src/Compiler/CompileExpr.idr

@@ -354,9 +354,9 @@ toCExpTm n (As _ _ _ p) = toCExpTm n p
 -- TODO: Either make sure 'Delayed' is always Rig0, or add to typecase
 toCExpTm n (TDelayed fc _ _) = pure $ CErased fc
 toCExpTm n (TDelay fc lr _ arg)
-    = pure (CDelay fc lr !(toCExp n arg))
+    = CDelay fc lr <$> toCExp n arg
 toCExpTm n (TForce fc lr arg)
-    = pure (CForce fc lr !(toCExp n arg))
+    = CForce fc lr <$> toCExp n arg
 toCExpTm n (PrimVal fc $ PrT c) = pure $ CCon fc (UN $ Basic $ show c) TYCON Nothing [] -- Primitive type constant
 toCExpTm n (PrimVal fc c) = pure $ CPrimVal fc c -- Non-type constant
 toCExpTm n (Erased fc _) = pure $ CErased fc
@@ -604,7 +604,7 @@ getNArgs defs (NS _ (UN $ Basic "Unit")) [] = pure NUnit
 getNArgs defs (NS _ (UN $ Basic "Struct")) [n, args]
     = do NPrimVal _ (Str n') <- evalClosure defs n
              | nf => throw (GenericMsg (getLoc nf) "Unknown name for struct")
-         pure (Struct n' !(getFieldArgs defs args))
+         Struct n' <$> getFieldArgs defs args
 getNArgs defs n args = pure $ User n args
 
 nfToCFType : {auto c : Ref Ctxt Defs} ->

src/Compiler/Scheme/Common.idr

@@ -414,7 +414,7 @@ parameters (constants : SortedSet Name,
                     !(showAlts n alts)
     schCaseTree i sc alts def
         = do tcode <- schExp (i + 1) sc
-             defc <- maybe (pure Nothing) (\v => pure (Just !(schExp i v))) def
+             defc <- traverseOpt (schExp i) def
              let n = getScrutineeTemp i
              if var sc
                 then pure $ "(case (vector-ref " ++ tcode ++ " 0) "
@@ -446,8 +446,7 @@ parameters (constants : SortedSet Name,
     schListCase i sc alts def
         = do tcode <- schExp (i + 1) sc
              let n = getScrutineeTemp i
-             defc <- maybe (pure Nothing)
-                           (\v => pure (Just !(schExp (i + 1) v))) def
+             defc <- traverseOpt (schExp (i + 1)) def
              nil <- getNilCode alts
              if var sc
                 then do cons <- getConsCode tcode alts
@@ -473,7 +472,7 @@ parameters (constants : SortedSet Name,
         getNilCode : List NamedConAlt -> Core (Maybe Builder)
         getNilCode [] = pure Nothing
         getNilCode (MkNConAlt _ NIL _ _ sc :: _)
-            = pure (Just !(schExp (i + 1) sc))
+            = Just <$> schExp (i + 1) sc
         getNilCode (_ :: xs) = getNilCode xs
 
         getConsCode : Builder -> List NamedConAlt -> Core (Maybe Builder)
@@ -496,8 +495,7 @@ parameters (constants : SortedSet Name,
     schMaybeCase i sc alts def
         = do tcode <- schExp (i + 1) sc
              let n = getScrutineeTemp i
-             defc <- maybe (pure Nothing)
-                           (\v => pure (Just !(schExp (i + 1) v))) def
+             defc <- traverseOpt (schExp (i + 1)) def
              nothing <- getNothingCode alts
              if var sc
                 then do just <- getJustCode tcode alts
@@ -523,7 +521,7 @@ parameters (constants : SortedSet Name,
         getNothingCode : List NamedConAlt -> Core (Maybe Builder)
         getNothingCode [] = pure Nothing
         getNothingCode (MkNConAlt _ NOTHING _ _ sc :: _)
-            = pure (Just !(schExp (i + 1) sc))
+            = Just <$> schExp (i + 1) sc
         getNothingCode (_ :: xs) = getNothingCode xs
 
         getJustCode : Builder -> List NamedConAlt -> Core (Maybe Builder)
@@ -623,7 +621,7 @@ parameters (constants : SortedSet Name,
            = pure $ !(schConstAlt (i + 1) n alt) ++ " " ++
                     !(showConstAlts n alts)
     schExp i (NmConstCase fc sc alts def)
-        = do defc <- maybe (pure Nothing) (\v => pure (Just !(schExp i v))) def
+        = do defc <- traverseOpt (schExp i) def
              tcode <- schExp (i + 1) sc
              let n = getScrutineeTemp i
              if var sc

src/Core/Binary.idr

@@ -345,10 +345,8 @@ addGlobalDef modns filens asm (n, def)
          codedentry <- lookupContextEntry n (gamma defs)
          -- Don't update the coded entry because some names might not be
          -- resolved yet
-         entry <- maybe (pure Nothing)
-                        (\ p => do x <- decode (gamma defs) (fst p) False (snd p)
-                                   pure (Just x))
-                        codedentry
+         entry <- traverseOpt (\p => decode (gamma defs) (fst p) False (snd p))
+                              codedentry
          unless (completeDef entry) $
            ignore $ addContextEntry filens n def
 

src/Core/Case/CaseBuilder.idr

@@ -1080,10 +1080,10 @@ mutual
             Core (Maybe (CaseTree vars))
   mixture fc fn phase (ConClauses cs rest) err
       = do fallthrough <- mixture fc fn phase rest err
-           pure (Just !(conRule fc fn phase cs fallthrough))
+           Just <$> conRule fc fn phase cs fallthrough
   mixture fc fn phase (VarClauses vs rest) err
       = do fallthrough <- mixture fc fn phase rest err
-           pure (Just !(varRule fc fn phase vs fallthrough))
+           Just <$> varRule fc fn phase vs fallthrough
   mixture fc fn {a} {todo} phase NoClauses err
       = pure err
 

src/Core/Core.idr

@@ -894,7 +894,7 @@ namespace PiInfo
   traverse f Explicit = pure Explicit
   traverse f Implicit = pure Implicit
   traverse f AutoImplicit = pure AutoImplicit
-  traverse f (DefImplicit t) = pure (DefImplicit !(f t))
+  traverse f (DefImplicit t) = DefImplicit <$> f t
 
 namespace Binder
   export

src/Core/LinearCheck.idr

@@ -472,7 +472,7 @@ mutual
                 Core (List ArgUsage)
   getArgUsage topfc rig ty pats
       = do us <- traverse (getPUsage ty) pats
-           pure (map snd !(combine us))
+           map snd <$> combine us
     where
       getCaseUsage : {vs : _} ->
                      Term ns -> Env Term vs -> List (Term vs) ->

src/Core/Normalise.idr

@@ -154,7 +154,7 @@ etaContract tm = do
 export
 getValArity : Defs -> Env Term vars -> NF vars -> Core Nat
 getValArity defs env (NBind fc x (Pi _ _ _ _) sc)
-    = pure (S !(getValArity defs env !(sc defs (toClosure defaultOpts env (Erased fc Placeholder)))))
+    = S <$> getValArity defs env !(sc defs (toClosure defaultOpts env (Erased fc Placeholder)))
 getValArity defs env val = pure 0
 
 export

src/Idris/Desugar.idr

@@ -1155,9 +1155,7 @@ mutual
            let isb = map (\ (info, r, n, p, tm) => (info, r, n, p, doBind bnames tm)) is'
            let consb = map (\(n, tm) => (n, doBind bnames tm)) cons'
 
-           body' <- maybe (pure Nothing)
-                          (\b => do b' <- traverse (desugarDecl ps) b
-                                    pure (Just (concat b'))) body
+           body' <- traverseOpt (map concat . traverse (desugarDecl ps)) body
            -- calculate the name of the implementation, if it's not explicitly
            -- given.
            let impname = maybe (mkImplName fc tn paramsb) id impln

src/Idris/ModTree.idr

@@ -137,7 +137,7 @@ getBuildMods loc done fname
                  dm <- newRef DoneMod empty
                  o <- newRef BuildOrder []
                  mkBuildMods {d=dm} {o} t
-                 pure (reverse !(get BuildOrder))
+                 reverse <$> get BuildOrder
 
 checkTotalReq : {auto c : Ref Ctxt Defs} ->
                 String -> String -> TotalReq -> Core Bool

src/Idris/Package.idr

@@ -196,7 +196,7 @@ field fname
     depends
         = do name <- packageName
              bs <- sepBy andop bound
-             pure (MkDepends name !(mkBound (concat bs) anyBounds))
+             MkDepends name <$> mkBound (concat bs) anyBounds
 
     strField : (FC -> String -> DescField) -> String -> Rule DescField
     strField fieldConstructor fieldName

src/Idris/Parser.idr

@@ -71,9 +71,9 @@ decoratedNamespacedSymbol fname smb =
 
 parens : {b : _} -> OriginDesc -> BRule b a -> Rule a
 parens fname p
-  = pure id <* decoratedSymbol fname "("
-            <*> p
-            <* decoratedSymbol fname ")"
+  = id <$ decoratedSymbol fname "("
+       <*> p
+       <* decoratedSymbol fname ")"
 
 decoratedDataTypeName : OriginDesc -> Rule Name
 decoratedDataTypeName fname = decorate fname Typ dataTypeName
@@ -1822,10 +1822,9 @@ typedArg fname indents
          pure $ map (\(c, n, tm) => (n.val, c, Explicit, tm)) params
   <|> do decoratedSymbol fname "{"
          commit
-         info <-
-                 (pure  AutoImplicit <* decoratedKeyword fname "auto"
-              <|> (decoratedKeyword fname "default" *> DefImplicit <$> simpleExpr fname indents)
-              <|> pure      Implicit)
+         info <- AutoImplicit <$ decoratedKeyword fname "auto"
+             <|> decoratedKeyword fname "default" *> DefImplicit <$> simpleExpr fname indents
+             <|> pure Implicit
          params <- pibindListName fname indents
          decoratedSymbol fname "}"
          pure $ map (\(c, n, tm) => (n.val, c, info, tm)) params

src/Idris/REPL.idr

@@ -1130,10 +1130,10 @@ processCatch cmd
                            )
 
 parseEmptyCmd : EmptyRule (Maybe REPLCmd)
-parseEmptyCmd = eoi *> (pure Nothing)
+parseEmptyCmd = eoi $> Nothing
 
 parseCmd : EmptyRule (Maybe REPLCmd)
-parseCmd = do c <- command; eoi; pure $ Just c
+parseCmd = Just <$> command <* eoi
 
 export
 parseRepl : String -> Either Error (Maybe REPLCmd)

src/Idris/Resugar.idr

@@ -369,7 +369,7 @@ mutual
   toPTerm p (IAlternative fc _ _) = pure (PImplicit fc)
   toPTerm p (IRewrite fc rule tm)
       = pure (PRewrite fc !(toPTerm startPrec rule)
-                               !(toPTerm startPrec tm))
+                          !(toPTerm startPrec tm))
   toPTerm p (ICoerced fc tm) = toPTerm p tm
   toPTerm p (IPrimVal fc c) = pure (PPrimVal fc c)
   toPTerm p (IHole fc str) = pure (PHole fc False str)
@@ -378,19 +378,18 @@ mutual
     = let nm = UN (Basic v) in
       pure (PRef fc (MkKindedName (Just Bound) nm nm))
   toPTerm p (IBindHere fc _ tm) = toPTerm p tm
-  toPTerm p (IAs fc nameFC _ n pat) = pure (PAs fc nameFC n !(toPTerm argPrec pat))
-  toPTerm p (IMustUnify fc r pat) = pure (PDotted fc !(toPTerm argPrec pat))
+  toPTerm p (IAs fc nameFC _ n pat) = PAs fc nameFC n <$> toPTerm argPrec pat
+  toPTerm p (IMustUnify fc r pat) = PDotted fc <$> toPTerm argPrec pat
 
-  toPTerm p (IDelayed fc r ty) = pure (PDelayed fc r !(toPTerm argPrec ty))
-  toPTerm p (IDelay fc tm) = pure (PDelay fc !(toPTerm argPrec tm))
-  toPTerm p (IForce fc tm) = pure (PForce fc !(toPTerm argPrec tm))
-  toPTerm p (IQuote fc tm) = pure (PQuote fc !(toPTerm argPrec tm))
+  toPTerm p (IDelayed fc r ty) = PDelayed fc r <$> toPTerm argPrec ty
+  toPTerm p (IDelay fc tm) = PDelay fc <$> toPTerm argPrec tm
+  toPTerm p (IForce fc tm) = PForce fc <$> toPTerm argPrec tm
+  toPTerm p (IQuote fc tm) = PQuote fc <$> toPTerm argPrec tm
   toPTerm p (IQuoteName fc n) = pure (PQuoteName fc n)
   toPTerm p (IQuoteDecl fc ds)
-      = do ds' <- traverse toPDecl ds
-           pure $ PQuoteDecl fc (catMaybes ds')
-  toPTerm p (IUnquote fc tm) = pure (PUnquote fc !(toPTerm argPrec tm))
-  toPTerm p (IRunElab fc _ tm) = pure (PRunElab fc !(toPTerm argPrec tm))
+      = PQuoteDecl fc . catMaybes <$> traverse toPDecl ds
+  toPTerm p (IUnquote fc tm) = PUnquote fc <$> toPTerm argPrec tm
+  toPTerm p (IRunElab fc _ tm) = PRunElab fc <$> toPTerm argPrec tm
 
   toPTerm p (IUnifyLog fc _ tm) = toPTerm p tm
   toPTerm p (Implicit fc True) = pure (PImplicit fc)
@@ -468,22 +467,22 @@ mutual
                  flags
                  !(traverse toPClause cs)
   toPClause (ImpossibleClause fc lhs)
-      = pure (MkImpossible fc !(toPTerm startPrec lhs))
+      = MkImpossible fc <$> toPTerm startPrec lhs
 
   toPTypeDecl : {auto c : Ref Ctxt Defs} ->
                 {auto s : Ref Syn SyntaxInfo} ->
                 ImpTy' KindedName -> Core (PTypeDecl' KindedName)
   toPTypeDecl (MkImpTy fc n ty)
-      = pure (MkFCVal fc $ MkPTy (pure ("", n)) "" !(toPTerm startPrec ty))
+      = MkFCVal fc . MkPTy (pure ("", n)) "" <$> toPTerm startPrec ty
 
   toPData : {auto c : Ref Ctxt Defs} ->
             {auto s : Ref Syn SyntaxInfo} ->
             ImpData' KindedName -> Core (PDataDecl' KindedName)
   toPData (MkImpData fc n ty opts cs)
       = pure (MkPData fc n !(traverseOpt (toPTerm startPrec) ty) opts
-                   !(traverse toPTypeDecl cs))
+                           !(traverse toPTypeDecl cs))
   toPData (MkImpLater fc n ty)
-      = pure (MkPLater fc n !(toPTerm startPrec ty))
+      = MkPLater fc n <$> toPTerm startPrec ty
 
   toPField : {auto c : Ref Ctxt Defs} ->
              {auto s : Ref Syn SyntaxInfo} ->
@@ -528,11 +527,11 @@ mutual
             ImpDecl' KindedName -> Core (Maybe (PDecl' KindedName))
   toPDecl (IClaim (MkFCVal fc $ MkIClaimData rig vis opts ty))
       = do opts' <- traverse toPFnOpt opts
-           pure (Just (PClaim (MkFCVal fc $ MkPClaim rig vis opts' !(toPTypeDecl ty))))
+           Just . PClaim . MkFCVal fc . MkPClaim rig vis opts' <$> toPTypeDecl ty
   toPDecl (IData fc vis mbtot d)
-      = pure (Just (PData fc "" vis mbtot !(toPData d)))
+      = Just . PData fc "" vis mbtot <$> toPData d
   toPDecl (IDef fc n cs)
-      = pure (Just (PDef $ MkFCVal fc !(traverse toPClause cs)))
+      = Just . PDef . MkFCVal fc <$> traverse toPClause cs
   toPDecl (IParameters fc ps ds)
       = do ds' <- traverse toPDecl ds
            pure (Just (PParameters fc
@@ -545,17 +544,15 @@ mutual
       = do (n, ps, opts, con, fs) <- toPRecord r
            pure (Just (PRecord fc "" vis mbtot (MkPRecord n ps opts con fs)))
   toPDecl (IFail fc msg ds)
-      = do ds' <- traverse toPDecl ds
-           pure (Just (PFail fc msg (catMaybes ds')))
+      = Just . PFail fc msg . catMaybes <$> traverse toPDecl ds
   toPDecl (INamespace fc ns ds)
-      = do ds' <- traverse toPDecl ds
-           pure (Just (PNamespace fc ns (catMaybes ds')))
+      = Just . PNamespace fc ns . catMaybes <$> traverse toPDecl ds
   toPDecl (ITransform fc n lhs rhs)
       = pure (Just (PTransform fc (show n)
                                   !(toPTerm startPrec lhs)
                                   !(toPTerm startPrec rhs)))
   toPDecl (IRunElabDecl fc tm)
-      = pure (Just (PRunElabDecl fc !(toPTerm startPrec tm)))
+      = Just . PRunElabDecl fc <$> toPTerm startPrec tm
   toPDecl (IPragma _ _ _) = pure Nothing
   toPDecl (ILog _) = pure Nothing
   toPDecl (IBuiltin fc type name) = pure $ Just $ PBuiltin fc type name

src/TTImp/Elab/App.idr

@@ -543,9 +543,8 @@ mutual
              logNF "elab" 10 ("Full function type") env
                       (NBind fc x (Pi fc argRig Explicit aty) sc)
              logC "elab" 10
-                     (do ety <- maybe (pure Nothing)
-                                     (\t => pure (Just !(toFullNames!(getTerm t))))
-                                     expty
+                     (do ety <- traverseOpt (\t => toFullNames !(getTerm t))
+                                            expty
                          pure ("Overall expected type: " ++ show ety))
              res <- check argRig ({ topLevel := False } elabinfo)
                                    nest env arg (Just (glueClosure defs env aty))
@@ -829,11 +828,10 @@ checkApp rig elabinfo nest env fc (IVar fc' n) expargs autoargs namedargs exp
         logC "elab" 10
                 (do defs <- get Ctxt
                     fnty <- quote defs env nty
-                    exptyt <- maybe (pure Nothing)
-                                       (\t => do ety <- getTerm t
-                                                 etynf <- normaliseHoles defs env ety
-                                                 pure (Just !(toFullNames etynf)))
-                                       exp
+                    exptyt <- traverseOpt (\t => do ety <- getTerm t
+                                                    etynf <- normaliseHoles defs env ety
+                                                    toFullNames etynf)
+                                          exp
                     pure ("Checking application of " ++ show !(getFullName n) ++
                           " (" ++ show n ++ ")" ++
                           " to " ++ show expargs ++ "\n\tFunction type " ++

src/TTImp/Elab/Lazy.idr

@@ -91,11 +91,8 @@ checkForce : {vars : _} ->
              Core (Term vars, Glued vars)
 checkForce rig elabinfo nest env fc tm exp
     = do defs <- get Ctxt
-         expf <- maybe (pure Nothing)
-                       (\gty => do tynf <- getNF gty
-                                   pure (Just (glueBack defs env
-                                         (NDelayed fc LUnknown tynf))))
-                       exp
+         expf <- traverseOpt (map (glueBack defs env . NDelayed fc LUnknown) . getNF)
+                             exp
          (tm', gty) <- check rig elabinfo nest env tm expf
          tynf <- getNF gty
          case tynf of

src/TTImp/Elab/Record.idr

@@ -86,9 +86,8 @@ findFieldsAndTypeArgs : {auto c : Ref Ctxt Defs} ->
                         Defs -> Name ->
                         Core $ Maybe (List (String, Maybe Name, Maybe Name), SortedSet Name)
 findFieldsAndTypeArgs defs con
-    = case !(lookupTyExact con (gamma defs)) of
-           Just t => pure (Just !(getExpNames empty [] !(nf defs [] t)))
-           _ => pure Nothing
+    = traverseOpt (\t => getExpNames empty [] !(nf defs [] t))
+                  !(lookupTyExact con (gamma defs))
   where
     getExpNames : SortedSet Name ->
                   List (String, Maybe Name, Maybe Name) ->

src/TTImp/Interactive/CaseSplit.idr

@@ -250,7 +250,7 @@ getUpdates : Defs -> RawImp -> RawImp -> Core (List (Name, RawImp))
 getUpdates defs orig updated
     = do u <- newRef UPD (MkUpdates [] [])
          findUpdates defs orig updated
-         pure (updates !(get UPD))
+         updates <$> get UPD
 
 mkCase : {auto c : Ref Ctxt Defs} ->
          {auto u : Ref UST UState} ->
@@ -285,7 +285,7 @@ mkCase {c} {u} fn orig lhs_raw
                log "interaction.casesplit" 3 $ "Original LHS: " ++ show orig
                log "interaction.casesplit" 3 $ "New LHS: " ++ show lhs'
 
-               pure (Valid lhs' !(getUpdates defs orig lhs')))
+               Valid lhs' <$> getUpdates defs orig lhs')
            (\err =>
                do put Ctxt defs
                   put UST ust