From 3f15823a4331ddc0bd188aaf9dad185a14573647 Mon Sep 17 00:00:00 2001 From: Viktor Yudov Date: Thu, 19 Dec 2024 18:28:22 +0300 Subject: [PATCH] [ cleanup ] Cleaning up the use of applicative syntax --- src/Compiler/Common.idr | 4 +-- src/Compiler/CompileExpr.idr | 6 ++-- src/Compiler/Scheme/Common.idr | 14 ++++------ src/Core/Binary.idr | 6 ++-- src/Core/Case/CaseBuilder.idr | 4 +-- src/Core/Core.idr | 2 +- src/Core/LinearCheck.idr | 2 +- src/Core/Normalise.idr | 2 +- src/Idris/Desugar.idr | 4 +-- src/Idris/ModTree.idr | 2 +- src/Idris/Package.idr | 2 +- src/Idris/Parser.idr | 13 ++++----- src/Idris/REPL.idr | 4 +-- src/Idris/Resugar.idr | 43 ++++++++++++++--------------- src/TTImp/Elab/App.idr | 14 ++++------ src/TTImp/Elab/Lazy.idr | 7 ++--- src/TTImp/Elab/Record.idr | 5 ++-- src/TTImp/Interactive/CaseSplit.idr | 4 +-- src/TTImp/Parser.idr | 9 ++---- 19 files changed, 64 insertions(+), 83 deletions(-) diff --git a/src/Compiler/Common.idr b/src/Compiler/Common.idr index a2668fad6b..ccf897dece 100644 --- a/src/Compiler/Common.idr +++ b/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) diff --git a/src/Compiler/CompileExpr.idr b/src/Compiler/CompileExpr.idr index 249773ace0..5ad7e7ba48 100644 --- a/src/Compiler/CompileExpr.idr +++ b/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} -> diff --git a/src/Compiler/Scheme/Common.idr b/src/Compiler/Scheme/Common.idr index b872f0e9ca..2a7956e31c 100644 --- a/src/Compiler/Scheme/Common.idr +++ b/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 diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index acc126ead8..24ed3bfd3c 100644 --- a/src/Core/Binary.idr +++ b/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 diff --git a/src/Core/Case/CaseBuilder.idr b/src/Core/Case/CaseBuilder.idr index 23aefedaa6..dd74b0a6ff 100644 --- a/src/Core/Case/CaseBuilder.idr +++ b/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 diff --git a/src/Core/Core.idr b/src/Core/Core.idr index 48c8a61b4b..03bfe4555b 100644 --- a/src/Core/Core.idr +++ b/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 diff --git a/src/Core/LinearCheck.idr b/src/Core/LinearCheck.idr index b250f22387..3ede0d6631 100644 --- a/src/Core/LinearCheck.idr +++ b/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) -> diff --git a/src/Core/Normalise.idr b/src/Core/Normalise.idr index 787d22dff8..a0c6fbfb3a 100644 --- a/src/Core/Normalise.idr +++ b/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 diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index b1f70903b1..3bd19043bb 100644 --- a/src/Idris/Desugar.idr +++ b/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 diff --git a/src/Idris/ModTree.idr b/src/Idris/ModTree.idr index 6e50284eb8..911441b9f6 100644 --- a/src/Idris/ModTree.idr +++ b/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 diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index dc2e3b83c4..e195d9b185 100644 --- a/src/Idris/Package.idr +++ b/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 diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index fa962e368d..f1a4ab4520 100644 --- a/src/Idris/Parser.idr +++ b/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 diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index 86f5c32f97..5eca1d8ef0 100644 --- a/src/Idris/REPL.idr +++ b/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) diff --git a/src/Idris/Resugar.idr b/src/Idris/Resugar.idr index 22ca606a39..7aa3ecae83 100644 --- a/src/Idris/Resugar.idr +++ b/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 diff --git a/src/TTImp/Elab/App.idr b/src/TTImp/Elab/App.idr index ede3102048..d44823ea62 100644 --- a/src/TTImp/Elab/App.idr +++ b/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 " ++ diff --git a/src/TTImp/Elab/Lazy.idr b/src/TTImp/Elab/Lazy.idr index c30f6497a1..676b90d15b 100644 --- a/src/TTImp/Elab/Lazy.idr +++ b/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 diff --git a/src/TTImp/Elab/Record.idr b/src/TTImp/Elab/Record.idr index 7cae467d75..b651b8100e 100644 --- a/src/TTImp/Elab/Record.idr +++ b/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) -> diff --git a/src/TTImp/Interactive/CaseSplit.idr b/src/TTImp/Interactive/CaseSplit.idr index e741314556..695ca960e2 100644 --- a/src/TTImp/Interactive/CaseSplit.idr +++ b/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 diff --git a/src/TTImp/Parser.idr b/src/TTImp/Parser.idr index deb367ae55..a9ef5b1961 100644 --- a/src/TTImp/Parser.idr +++ b/src/TTImp/Parser.idr @@ -611,12 +611,9 @@ recordParam fname indents <|> do symbol "{" commit start <- location - info <- (pure AutoImplicit <* keyword "auto" - <|>(do - keyword "default" - t <- simpleExpr fname indents - pure $ DefImplicit t) - <|> pure Implicit) + info <- AutoImplicit <$ keyword "auto" + <|> keyword "default" *> DefImplicit <$> simpleExpr fname indents + <|> pure Implicit params <- pibindListName fname start indents symbol "}" pure $ map (\(c, n, tm) => (n, c, info, tm)) params