From 339b82ae1ad51a18972f9470ea3fe2dd3b9fbefa Mon Sep 17 00:00:00 2001 From: Guillaume ALLAIS Date: Sat, 20 Feb 2021 01:16:01 +0000 Subject: [PATCH 01/12] [ cleanup ] insist that (>>) takes an `m ()` first --- libs/base/Data/Buffer.idr | 2 +- libs/base/System/File.idr | 3 +- libs/contrib/Control/Linear/LIO.idr | 14 +++++ .../contrib/Data/String/Parser/Expression.idr | 8 +-- libs/contrib/Language/JSON/Parser.idr | 16 +++--- libs/contrib/System/Path.idr | 4 +- libs/contrib/Test/Golden.idr | 2 +- libs/contrib/Text/Parser.idr | 2 +- libs/contrib/Text/Parser/Core.idr | 12 +++++ libs/prelude/Prelude/Interfaces.idr | 2 +- src/Compiler/Common.idr | 5 +- src/Compiler/ES/ES.idr | 16 +++--- src/Compiler/ES/Imperative.idr | 15 ++++-- src/Compiler/ES/Node.idr | 2 +- src/Compiler/ES/TailRec.idr | 2 +- src/Compiler/RefC/RefC.idr | 37 +++++++------- src/Compiler/Scheme/Chez.idr | 14 ++--- src/Compiler/Scheme/Gambit.idr | 4 +- src/Compiler/Scheme/Racket.idr | 11 ++-- src/Core/AutoSearch.idr | 20 +++----- src/Core/Binary.idr | 14 +++-- src/Core/Context.idr | 50 +++++++----------- src/Core/Core.idr | 18 +++++-- src/Core/LinearCheck.idr | 4 +- src/Core/Normalise.idr | 2 +- src/Core/Termination.idr | 2 +- src/Core/Unify.idr | 15 +++--- src/Core/UnifyState.idr | 9 ++-- src/Idris/Elab/Implementation.idr | 10 ++-- src/Idris/Elab/Interface.idr | 7 ++- src/Idris/ModTree.idr | 2 +- src/Idris/Package.idr | 33 ++++++------ src/Idris/Parser.idr | 2 + src/Idris/ProcessIdr.idr | 4 +- src/Idris/REPL.idr | 51 ++++++++++--------- src/Idris/SetOptions.idr | 12 ++--- src/Libraries/Text/Parser.idr | 2 +- src/Libraries/Text/Parser/Core.idr | 12 +++++ src/Libraries/Utils/Path.idr | 4 +- src/Libraries/Utils/Shunting.idr | 2 +- src/Parser/Rule/Source.idr | 7 +-- src/TTImp/Elab.idr | 16 +++--- src/TTImp/Elab/App.idr | 5 +- src/TTImp/Elab/Binders.idr | 2 +- src/TTImp/Elab/Delayed.idr | 8 ++- src/TTImp/Elab/ImplicitBind.idr | 3 +- src/TTImp/Elab/Local.idr | 2 +- src/TTImp/Elab/Utils.idr | 7 +-- src/TTImp/Interactive/ExprSearch.idr | 8 +-- src/TTImp/Parser.idr | 1 + src/TTImp/ProcessData.idr | 4 +- src/TTImp/ProcessDecls.idr | 7 +-- src/TTImp/ProcessDef.idr | 12 ++--- src/TTImp/ProcessParams.idr | 3 +- src/TTImp/ProcessRunElab.idr | 3 +- src/TTImp/ProcessType.idr | 9 ++-- src/TTImp/WithClause.idr | 2 +- src/Yaffle/Main.idr | 12 ++--- src/Yaffle/REPL.idr | 51 +++++++++---------- tests/Lib.idr | 2 +- 60 files changed, 313 insertions(+), 297 deletions(-) diff --git a/libs/base/Data/Buffer.idr b/libs/base/Data/Buffer.idr index c53f023f66..9ce042bfef 100644 --- a/libs/base/Data/Buffer.idr +++ b/libs/base/Data/Buffer.idr @@ -311,7 +311,7 @@ concatBuffers xs let cumulative = reverse revCumulative Just buf <- newBuffer totalSize | Nothing => pure Nothing - traverse (\(b, size, watermark) => copyData b 0 size buf watermark) (zip3 xs sizes cumulative) + traverse_ (\(b, size, watermark) => copyData b 0 size buf watermark) (zip3 xs sizes cumulative) pure (Just buf) where scanSize : (Int, List Int) -> Int -> (Int, List Int) diff --git a/libs/base/System/File.idr b/libs/base/System/File.idr index b254335ab7..bf5e12217e 100644 --- a/libs/base/System/File.idr +++ b/libs/base/System/File.idr @@ -246,8 +246,7 @@ fEOF (FHandle f) export fflush : HasIO io => (h : File) -> io () fflush (FHandle f) - = do primIO (prim__flush f) - pure () + = ignore $ primIO (prim__flush f) export popen : HasIO io => String -> Mode -> io (Either FileError File) diff --git a/libs/contrib/Control/Linear/LIO.idr b/libs/contrib/Control/Linear/LIO.idr index edd3825e2e..98196e8f4d 100644 --- a/libs/contrib/Control/Linear/LIO.idr +++ b/libs/contrib/Control/Linear/LIO.idr @@ -106,6 +106,20 @@ export %inline (1 _ : ContType io u_act u_k a b) -> L io {use=u_k} b (>>=) = Bind +export +delay : {u_act : _} -> (1 _ : L io {use=u_k} b) -> ContType io u_act u_k () b +delay mb = case u_act of + None => \ _ => mb + Linear => \ () => mb + Unrestricted => \ _ => mb + +export %inline +(>>) : {u_act : _} -> + LinearBind io => + (1 _ : L io {use=u_act} ()) -> + (1 _ : L io {use=u_k} b) -> L io {use=u_k} b +ma >> mb = ma >>= delay mb + export %inline pure0 : (0 x : a) -> L io {use=0} a pure0 = Pure0 diff --git a/libs/contrib/Data/String/Parser/Expression.idr b/libs/contrib/Data/String/Parser/Expression.idr index 51f742409d..ff98cb6208 100644 --- a/libs/contrib/Data/String/Parser/Expression.idr +++ b/libs/contrib/Data/String/Parser/Expression.idr @@ -44,7 +44,7 @@ toParserUn [] = fail "couldn't create unary parser" toParserUn (x :: xs) = x <|> toParserUn xs ambiguous : (assoc : String) -> (op : Parser (a -> a -> a)) -> Parser a -ambiguous assoc op = do op +ambiguous assoc op = do ignore op fail ("ambiguous use of a " ++ assoc ++ " associative operator") mutual @@ -71,11 +71,13 @@ mutual mkLassocP1 : (amRight : Parser a) -> (amNon : Parser a) -> (lassocOp : Parser (a -> a -> a)) -> (termP : Parser a) -> (x : a) -> Parser a mkLassocP1 amRight amNon lassocOp termP x = mkLassocP amRight amNon lassocOp termP x <|> pure x -mkNassocP : (amRight : Parser a) -> (amLeft : Parser a) -> (amNon : Parser a) -> (nassocOp : Parser (a -> a -> a)) -> (termP : Parser a) -> (x : a) -> Parser a +mkNassocP : (amRight, amLeft, amNon : Parser a) -> + (nassocOp : Parser (a -> a -> a)) -> + (termP : Parser a) -> (x : a) -> Parser a mkNassocP amRight amLeft amNon nassocOp termP x = do f <- nassocOp y <- termP - amRight <|> amLeft <|> amNon + ignore (amRight <|> amLeft <|> amNon) pure (f x y) public export diff --git a/libs/contrib/Language/JSON/Parser.idr b/libs/contrib/Language/JSON/Parser.idr index d84f36337a..a34c1ad993 100644 --- a/libs/contrib/Language/JSON/Parser.idr +++ b/libs/contrib/Language/JSON/Parser.idr @@ -34,10 +34,10 @@ mutual private object : Grammar JSONToken True JSON object = do punct $ Curly Open - commit - props <- properties - punct $ Curly Close - pure $ JObject props + mustWork $ do + props <- properties + punct $ Curly Close + pure $ JObject props where properties : Grammar JSONToken False (List (String, JSON)) properties = sepBy (punct Comma) $ @@ -49,10 +49,10 @@ mutual private array : Grammar JSONToken True JSON array = do punct (Square Open) - commit - vals <- values - punct (Square Close) - pure (JArray vals) + mustWork $ do + vals <- values + punct (Square Close) + pure (JArray vals) where values : Grammar JSONToken False (List JSON) values = sepBy (punct Comma) json diff --git a/libs/contrib/System/Path.idr b/libs/contrib/System/Path.idr index 4699e78147..61ca30e30b 100644 --- a/libs/contrib/System/Path.idr +++ b/libs/contrib/System/Path.idr @@ -171,7 +171,7 @@ bodySeparator = (match $ PTPunct '\\') <|> (match $ PTPunct '/') verbatim : Grammar PathToken True () verbatim = do - count (exactly 2) $ match $ PTPunct '\\' + ignore $ count (exactly 2) $ match $ PTPunct '\\' match $ PTPunct '?' match $ PTPunct '\\' pure () @@ -180,7 +180,7 @@ verbatim = unc : Grammar PathToken True Volume unc = do - count (exactly 2) $ match $ PTPunct '\\' + ignore $ count (exactly 2) $ match $ PTPunct '\\' server <- match PTText bodySeparator share <- match PTText diff --git a/libs/contrib/Test/Golden.idr b/libs/contrib/Test/Golden.idr index 0d5d50917f..9ea947c4ad 100644 --- a/libs/contrib/Test/Golden.idr +++ b/libs/contrib/Test/Golden.idr @@ -144,7 +144,7 @@ runTest opts testPath = forkIO $ do let cg = case codegen opts of Nothing => "" Just cg => "env IDRIS2_TESTS_CG=" ++ cg ++ " " - system $ "cd " ++ testPath ++ " && " ++ + ignore $ system $ "cd " ++ testPath ++ " && " ++ cg ++ "sh ./run " ++ exeUnderTest opts ++ " | tr -d '\\r' > output" end <- clockTime Thread diff --git a/libs/contrib/Text/Parser.idr b/libs/contrib/Text/Parser.idr index 0cfd7d0e6f..29026ddbf1 100644 --- a/libs/contrib/Text/Parser.idr +++ b/libs/contrib/Text/Parser.idr @@ -160,7 +160,7 @@ mutual (skip : Grammar tok True s) -> (p : Grammar tok c a) -> Grammar tok True a - afterSome skip p = do skip + afterSome skip p = do ignore skip afterMany skip p ||| Parse zero or more instance of `skip` until `p` is encountered, diff --git a/libs/contrib/Text/Parser/Core.idr b/libs/contrib/Text/Parser/Core.idr index e822a02824..71a71b2f43 100644 --- a/libs/contrib/Text/Parser/Core.idr +++ b/libs/contrib/Text/Parser/Core.idr @@ -37,6 +37,18 @@ public export %inline %tcinline (>>=) {c1 = False} = SeqEmpty (>>=) {c1 = True} = SeqEat +||| Sequence two grammars. If either consumes some input, the sequence is +||| guaranteed to consume some input. If the first one consumes input, the +||| second is allowed to be recursive (because it means some input has been +||| consumed and therefore the input is smaller) +public export %inline %tcinline +(>>) : {c1, c2 : Bool} -> + Grammar tok c1 () -> + inf c1 (Grammar tok c2 a) -> + Grammar tok (c1 || c2) a +(>>) {c1 = False} ma mb = SeqEmpty ma (const mb) +(>>) {c1 = True} ma mb = SeqEat ma (Delay \ a => mb) + ||| Sequence two grammars. If either consumes some input, the sequence is ||| guaranteed to consume input. This is an explicitly non-infinite version ||| of `>>=`. diff --git a/libs/prelude/Prelude/Interfaces.idr b/libs/prelude/Prelude/Interfaces.idr index 43ee24d60a..f518f58b7a 100644 --- a/libs/prelude/Prelude/Interfaces.idr +++ b/libs/prelude/Prelude/Interfaces.idr @@ -198,7 +198,7 @@ public export ||| Sequencing of effectful composition public export -(>>) : (Monad m) => m a -> m b -> m b +(>>) : (Monad m) => m () -> m b -> m b a >> b = a >>= \_ => b ||| Left-to-right Kleisli composition of monads. diff --git a/src/Compiler/Common.idr b/src/Compiler/Common.idr index e429d6f068..882f5e2809 100644 --- a/src/Compiler/Common.idr +++ b/src/Compiler/Common.idr @@ -141,7 +141,7 @@ getAllDesc (n@(Resolved i) :: rest) arr defs Nothing => getAllDesc rest arr defs Just (_, entry) => do (def, bin) <- getMinimalDef entry - addDef n def + ignore $ addDef n def let refs = refersToRuntime def if multiplicity def /= erased then do coreLift $ writeArray arr i (i, bin) @@ -172,8 +172,7 @@ replaceEntry : {auto c : Ref Ctxt Defs} -> (Int, Maybe Binary) -> Core () replaceEntry (i, Nothing) = pure () replaceEntry (i, Just b) - = do addContextEntry (Resolved i) b - pure () + = ignore $ addContextEntry (Resolved i) b natHackNames : List Name natHackNames diff --git a/src/Compiler/ES/ES.idr b/src/Compiler/ES/ES.idr index 1d6c80e7f4..cf100c072e 100644 --- a/src/Compiler/ES/ES.idr +++ b/src/Compiler/ES/ES.idr @@ -21,7 +21,8 @@ jsString : String -> String jsString s = "'" ++ (concatMap okchar (unpack s)) ++ "'" where okchar : Char -> String - okchar c = if (c >= ' ') && (c /= '\\') && (c /= '"') && (c /= '\'') && (c <= '~') + okchar c = if (c >= ' ') && (c /= '\\') + && (c /= '"') && (c /= '\'') && (c <= '~') then cast c else case c of '\0' => "\\0" @@ -35,7 +36,8 @@ esName : String -> String esName x = "__esPrim_" ++ x -addToPreamble : {auto c : Ref ESs ESSt} -> String -> String -> String -> Core String +addToPreamble : {auto c : Ref ESs ESSt} -> + String -> String -> String -> Core String addToPreamble name newName def = do s <- get ESs @@ -45,8 +47,10 @@ addToPreamble name newName def = put ESs (record { preamble = insert name def (preamble s) } s) pure newName Just x => - if x /= def then throw $ InternalError $ "two incompatible definitions for " ++ name ++ "<|" ++ x ++"|> <|"++ def ++ "|>" - else pure newName + if x /= def + then throw $ InternalError $ "two incompatible definitions for " + ++ name ++ "<|" ++ x ++"|> <|"++ def ++ "|>" + else pure newName addConstToPreamble : {auto c : Ref ESs ESSt} -> String -> String -> Core String addConstToPreamble name def = @@ -323,11 +327,11 @@ makeForeign n x = let (name, lib_) = break (== ',') def let lib = drop 1 lib_ lib_code <- readDataFile ("js/" ++ lib ++ ".js") - addSupportToPreamble lib lib_code + ignore $ addSupportToPreamble lib lib_code pure $ "const " ++ jsName n ++ " = " ++ lib ++ "_" ++ name ++ "\n" "stringIterator" => do - addStringIteratorToPreamble + ignore addStringIteratorToPreamble case def of "new" => pure $ "const " ++ jsName n ++ " = __prim_stringIteratorNew;\n" "next" => pure $ "const " ++ jsName n ++ " = __prim_stringIteratorNext;\n" diff --git a/src/Compiler/ES/Imperative.idr b/src/Compiler/ES/Imperative.idr index aae7f3fb50..1fe29f7881 100644 --- a/src/Compiler/ES/Imperative.idr +++ b/src/Compiler/ES/Imperative.idr @@ -18,11 +18,18 @@ mutual isNameUsed name (NmLocal fc n) = n == name isNameUsed name (NmRef fc n) = n == name isNameUsed name (NmLam fc n e) = isNameUsed name e - isNameUsed name (NmApp fc x args) = isNameUsed name x || any (isNameUsed name) args + isNameUsed name (NmApp fc x args) + = isNameUsed name x || any (isNameUsed name) args isNameUsed name (NmPrimVal fc c) = False isNameUsed name (NmOp fc op args) = any (isNameUsed name) args - isNameUsed name (NmConCase fc sc alts def) = isNameUsed name sc || any (isNameUsedConAlt name) alts || maybe False (isNameUsed name) def - isNameUsed name (NmConstCase fc sc alts def) = isNameUsed name sc || any (isNameUsedConstAlt name) alts || maybe False (isNameUsed name) def + isNameUsed name (NmConCase fc sc alts def) + = isNameUsed name sc + || any (isNameUsedConAlt name) alts + || maybe False (isNameUsed name) def + isNameUsed name (NmConstCase fc sc alts def) + = isNameUsed name sc + || any (isNameUsedConstAlt name) alts + || maybe False (isNameUsed name) def isNameUsed name (NmExtPrim fc p args) = any (isNameUsed name) args isNameUsed name (NmCon fc x t args) = any (isNameUsed name) args isNameUsed name (NmDelay fc t) = isNameUsed name t @@ -217,7 +224,7 @@ compileToImperative c tm = cdata <- getCompileData Cases tm let ndefs = namedDefs cdata let ctm = forget (mainExpr cdata) - newRef Imps (MkImpSt 0) + ref <- newRef Imps (MkImpSt 0) lst_defs <- traverse getImp (defsUsedByNamedCExp ctm ndefs) let defs = concat lst_defs defs_optim <- tailRecOptim defs diff --git a/src/Compiler/ES/Node.idr b/src/Compiler/ES/Node.idr index fa0a21d609..47095b155c 100644 --- a/src/Compiler/ES/Node.idr +++ b/src/Compiler/ES/Node.idr @@ -45,7 +45,7 @@ executeExpr c tmpDir tm Right () <- coreLift $ writeFile outn js | Left err => throw (FileErr outn err) node <- coreLift findNode - coreLift $ system (node ++ " " ++ outn) + coreLift_ $ system (node ++ " " ++ outn) pure () ||| Codegen wrapper for Node implementation. diff --git a/src/Compiler/ES/TailRec.idr b/src/Compiler/ES/TailRec.idr index 150a04ca76..533520976b 100644 --- a/src/Compiler/ES/TailRec.idr +++ b/src/Compiler/ES/TailRec.idr @@ -243,7 +243,7 @@ export tailRecOptim : ImperativeStatement -> Core ImperativeStatement tailRecOptim x = do - newRef TailRecS (MkTailSt 0) + ref <- newRef TailRecS (MkTailSt 0) let graph = tailCallGraph x let groups = recursiveTailCallGroups graph let functionsToOptimize = foldl SortedSet.union empty $ map SortedSet.fromList groups diff --git a/src/Compiler/RefC/RefC.idr b/src/Compiler/RefC/RefC.idr index f9c985e09c..6c9775b0f4 100644 --- a/src/Compiler/RefC/RefC.idr +++ b/src/Compiler/RefC/RefC.idr @@ -392,7 +392,7 @@ freeTmpVars = do lists <- get TemporaryVariableTracker case lists of (vars :: varss) => do - traverse (\v => emit EmptyFC $ "removeReference(" ++ v ++ ");" ) vars + traverse_ (\v => emit EmptyFC $ "removeReference(" ++ v ++ ");" ) vars put TemporaryVariableTracker varss [] => pure () @@ -734,7 +734,7 @@ mutual increaseIndentation newTemporaryVariableLevel defaultAssignment <- cStatementsFromANF d - -- traverse (\l => emit EmptyFC (l) ) defaultBody + -- traverse_ (\l => emit EmptyFC (l) ) defaultBody emit EmptyFC $ switchReturnVar ++ " = " ++ nonTailCall defaultAssignment ++ ";" freeTmpVars decreaseIndentation @@ -855,7 +855,7 @@ emitFDef funcName ((varType, varName, varCFType) :: xs) = do emit EmptyFC "(" increaseIndentation emit EmptyFC $ " Value *" ++ varName - traverse (\(varType, varName, varCFType) => emit EmptyFC $ ", Value *" ++ varName) xs + traverse_ (\(varType, varName, varCFType) => emit EmptyFC $ ", Value *" ++ varName) xs decreaseIndentation emit EmptyFC ")" @@ -936,7 +936,7 @@ createCFunctions n (MkAFun args anf) = do emit EmptyFC $ "(" increaseIndentation let commaSepArglist = addCommaToList (map (\a => "arglist->args["++ show a ++"]") argsNrs) - traverse (emit EmptyFC) commaSepArglist + traverse_ (emit EmptyFC) commaSepArglist decreaseIndentation emit EmptyFC ");" decreaseIndentation @@ -971,7 +971,7 @@ createCFunctions n (MkAForeign ccs fargs (CFIORes ret)) = do emit EmptyFC $ "(" increaseIndentation let commaSepArglist = addCommaToList (map (\a => "arglist->args["++ show a ++"]") (getArgsNrList fargs Z)) - traverse (emit EmptyFC) commaSepArglist + traverse_ (emit EmptyFC) commaSepArglist decreaseIndentation emit EmptyFC ");" decreaseIndentation @@ -1034,7 +1034,7 @@ header = do , "#include // for libidris2_support"] extLibs <- get ExternalLibs let extLibLines = map (\lib => "// add header(s) for library: " ++ lib ++ "\n") extLibs - traverse (\l => coreLift (putStrLn $ " header for " ++ l ++ " needed")) extLibs + traverse_ (\l => coreLift (putStrLn $ " header for " ++ l ++ " needed")) extLibs fns <- get FunctionDefinitions update OutfileText (appendL (initLines ++ extLibLines ++ ["\n// function definitions"] ++ fns)) @@ -1052,9 +1052,8 @@ footer = do export executeExpr : Ref Ctxt Defs -> (execDir : String) -> ClosedTerm -> Core () executeExpr c _ tm - = do coreLift $ putStrLn "Execute expression not yet implemented for refc" - coreLift $ system "false" - pure () + = do coreLift_ $ putStrLn "Execute expression not yet implemented for refc" + coreLift_ $ system "false" export compileExpr : UsePhase @@ -1069,23 +1068,23 @@ compileExpr ANF c _ outputDir tm outfile = let outobj = outputDir outfile ++ ".o" let outexec = outputDir outfile - coreLift $ mkdirAll outputDir + coreLift_ $ mkdirAll outputDir cdata <- getCompileData ANF tm let defs = anf cdata - newRef ArgCounter 0 - newRef FunctionDefinitions [] - newRef TemporaryVariableTracker [] - newRef OutfileText DList.Nil - newRef ExternalLibs [] - newRef IndentLevel 0 - traverse (\(n, d) => createCFunctions n d) defs + _ <- newRef ArgCounter 0 + _ <- newRef FunctionDefinitions [] + _ <- newRef TemporaryVariableTracker [] + _ <- newRef OutfileText DList.Nil + _ <- newRef ExternalLibs [] + _ <- newRef IndentLevel 0 + traverse_ (\(n, d) => createCFunctions n d) defs header -- added after the definition traversal in order to add all encountered function defintions footer fileContent <- get OutfileText let code = fastAppend (map (++ "\n") (reify fileContent)) - coreLift (writeFile outn code) - coreLift $ putStrLn $ "Generated C file " ++ outn + coreLift_ $ writeFile outn code + coreLift_ $ putStrLn $ "Generated C file " ++ outn cc <- coreLift findCC dirs <- getDirs diff --git a/src/Compiler/Scheme/Chez.idr b/src/Compiler/Scheme/Chez.idr index 920c4a8edf..03732d8c63 100644 --- a/src/Compiler/Scheme/Chez.idr +++ b/src/Compiler/Scheme/Chez.idr @@ -310,7 +310,7 @@ mkStruct (CFStruct n flds) showFld : (String, CFType) -> Core String showFld (n, ty) = pure $ "[" ++ n ++ " " ++ !(cftySpec emptyFC ty) ++ "]" mkStruct (CFIORes t) = mkStruct t -mkStruct (CFFun a b) = do mkStruct a; mkStruct b +mkStruct (CFFun a b) = do ignore (mkStruct a); mkStruct b mkStruct _ = pure "" schFgnDef : {auto c : Ref Ctxt Defs} -> @@ -401,7 +401,7 @@ compileToSS c appdir tm outfile main ++ schFooter Right () <- coreLift $ writeFile outfile scm | Left err => throw (FileErr outfile err) - coreLift $ chmodRaw outfile 0o755 + coreLift_ $ chmodRaw outfile 0o755 pure () ||| Compile a Chez Scheme source file to an executable, daringly with runtime checks off. @@ -413,8 +413,8 @@ compileToSO chez appDirRel outSsAbs show outSsAbs ++ "))" Right () <- coreLift $ writeFile tmpFileAbs build | Left err => throw (FileErr tmpFileAbs err) - coreLift $ chmodRaw tmpFileAbs 0o755 - coreLift $ system (chez ++ " --script \"" ++ tmpFileAbs ++ "\"") + coreLift_ $ chmodRaw tmpFileAbs 0o755 + coreLift_ $ system (chez ++ " --script \"" ++ tmpFileAbs ++ "\"") pure () makeSh : String -> String -> String -> Core () @@ -439,7 +439,7 @@ compileExpr : Bool -> Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) compileExpr makeitso c tmpDir outputDir tm outfile = do let appDirRel = outfile ++ "_app" -- relative to build dir let appDirGen = outputDir appDirRel -- relative to here - coreLift $ mkdirAll appDirGen + coreLift_ $ mkdirAll appDirGen Just cwd <- coreLift currentDir | Nothing => throw (InternalError "Can't get current directory") let outSsFile = appDirRel outfile <.> "ss" @@ -453,7 +453,7 @@ compileExpr makeitso c tmpDir outputDir tm outfile if isWindows then makeShWindows chez outShRel appDirRel (if makeitso then outSoFile else outSsFile) else makeSh outShRel appDirRel (if makeitso then outSoFile else outSsFile) - coreLift $ chmodRaw outShRel 0o755 + coreLift_ $ chmodRaw outShRel 0o755 pure (Just outShRel) ||| Chez Scheme implementation of the `executeExpr` interface. @@ -462,7 +462,7 @@ executeExpr : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core () executeExpr c tmpDir tm = do Just sh <- compileExpr False c tmpDir tmpDir tm "_tmpchez" | Nothing => throw (InternalError "compileExpr returned Nothing") - coreLift $ system sh + coreLift_ $ system sh pure () ||| Codegen wrapper for Chez scheme implementation. diff --git a/src/Compiler/Scheme/Gambit.idr b/src/Compiler/Scheme/Gambit.idr index 034a340f0f..a5ea8e0609 100644 --- a/src/Compiler/Scheme/Gambit.idr +++ b/src/Compiler/Scheme/Gambit.idr @@ -335,7 +335,7 @@ mkStruct (CFStruct n flds) showFld : (String, CFType) -> Core String showFld (n, ty) = pure $ "(" ++ n ++ " " ++ !(cftySpec emptyFC ty) ++ ")" mkStruct (CFIORes t) = mkStruct t -mkStruct (CFFun a b) = do mkStruct a; mkStruct b +mkStruct (CFFun a b) = do ignore (mkStruct a); mkStruct b mkStruct _ = pure "" schFgnDef : {auto c : Ref Ctxt Defs} -> @@ -414,7 +414,7 @@ executeExpr : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core () executeExpr c tmpDir tm = do Just sh <- compileExpr c tmpDir tmpDir tm "_tmpgambit" | Nothing => throw (InternalError "compileExpr returned Nothing") - coreLift $ system sh -- TODO: on windows, should add exe extension + coreLift_ $ system sh -- TODO: on windows, should add exe extension pure () export diff --git a/src/Compiler/Scheme/Racket.idr b/src/Compiler/Scheme/Racket.idr index 78fcd4cc83..911f871851 100644 --- a/src/Compiler/Scheme/Racket.idr +++ b/src/Compiler/Scheme/Racket.idr @@ -293,7 +293,7 @@ mkStruct (CFStruct n flds) showFld : (String, CFType) -> Core String showFld (n, ty) = pure $ "[" ++ n ++ " " ++ !(cftySpec emptyFC ty) ++ "]" mkStruct (CFIORes t) = mkStruct t -mkStruct (CFFun a b) = do mkStruct a; mkStruct b +mkStruct (CFFun a b) = do ignore (mkStruct a); mkStruct b mkStruct _ = pure "" schFgnDef : {auto f : Ref Done (List String) } -> @@ -390,7 +390,7 @@ compileToRKT c appdir tm outfile schFooter Right () <- coreLift $ writeFile outfile scm | Left err => throw (FileErr outfile err) - coreLift $ chmodRaw outfile 0o755 + coreLift_ $ chmodRaw outfile 0o755 pure () makeSh : String -> String -> String -> String -> Core () @@ -414,7 +414,7 @@ compileExpr : Bool -> Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) compileExpr mkexec c tmpDir outputDir tm outfile = do let appDirRel = outfile ++ "_app" -- relative to build dir let appDirGen = outputDir appDirRel -- relative to here - coreLift $ mkdirAll appDirGen + coreLift_ $ mkdirAll appDirGen Just cwd <- coreLift currentDir | Nothing => throw (InternalError "Can't get current directory") @@ -443,7 +443,7 @@ compileExpr mkexec c tmpDir outputDir tm outfile else if mkexec then makeSh "" outShRel appDirRel outBinFile else makeSh (racket ++ " ") outShRel appDirRel outRktFile - coreLift $ chmodRaw outShRel 0o755 + coreLift_ $ chmodRaw outShRel 0o755 pure (Just outShRel) else pure Nothing @@ -451,8 +451,7 @@ executeExpr : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core () executeExpr c tmpDir tm = do Just sh <- compileExpr False c tmpDir tmpDir tm "_tmpracket" | Nothing => throw (InternalError "compileExpr returned Nothing") - coreLift $ system sh - pure () + coreLift_ $ system sh export codegenRacket : Codegen diff --git a/src/Core/AutoSearch.idr b/src/Core/AutoSearch.idr index ed1525be55..09f9a75f3c 100644 --- a/src/Core/AutoSearch.idr +++ b/src/Core/AutoSearch.idr @@ -316,7 +316,7 @@ searchLocalWith {vars} fc rigc defaults trying depth def top env (prf, ty) targe let env' = clearEnv prf env -- Work right to left, because later arguments may solve -- earlier ones by unification - traverse (searchIfHole fc defaults trying False depth def top env') + traverse_ (searchIfHole fc defaults trying False depth def top env') (impLast args) pure candidate else do logNF "auto" 10 "Can't use " env ty @@ -452,7 +452,7 @@ searchName fc rigc defaults trying depth def top env target (n, ndef) logTermNF "auto" 10 "Candidate " env candidate -- Work right to left, because later arguments may solve earlier -- dependencies by unification - traverse (searchIfHole fc defaults trying ispair depth def top env) + traverse_ (searchIfHole fc defaults trying ispair depth def top env) (impLast args) pure candidate @@ -516,25 +516,21 @@ concreteDets {vars} fc defaults env top pos dets (arg :: args) concrete defs (NTCon nfc n t a args) atTop = do sd <- getSearchData nfc False n let args' = drop 0 (detArgs sd) args - traverse (\ parg => do argnf <- evalClosure defs parg - concrete defs argnf False) (map snd args') - pure () + traverse_ (\ parg => do argnf <- evalClosure defs parg + concrete defs argnf False) (map snd args') concrete defs (NDCon nfc n t a args) atTop - = do traverse (\ parg => do argnf <- evalClosure defs parg - concrete defs argnf False) (map snd args) - pure () + = do traverse_ (\ parg => do argnf <- evalClosure defs parg + concrete defs argnf False) (map snd args) concrete defs (NApp _ (NMeta n i _) _) True = do Just (Hole _ b) <- lookupDefExact n (gamma defs) | _ => throw (DeterminingArg fc n i [] top) - when (not (implbind b)) $ + unless (implbind b) $ throw (DeterminingArg fc n i [] top) - pure () concrete defs (NApp _ (NMeta n i _) _) False = do Just (Hole _ b) <- lookupDefExact n (gamma defs) | def => throw (CantSolveGoal fc [] top) - when (not (implbind b)) $ + unless (implbind b) $ throw (CantSolveGoal fc [] top) - pure () concrete defs tm atTop = pure () checkConcreteDets : {vars : _} -> diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index 322e1da1b6..2d70ad94d9 100644 --- a/src/Core/Binary.idr +++ b/src/Core/Binary.idr @@ -286,13 +286,11 @@ addGlobalDef modns asm (n, def) (\ p => do x <- decode (gamma defs) (fst p) False (snd p) pure (Just x)) codedentry - if completeDef entry - then pure () - else do addContextEntry n def - pure () - maybe (pure ()) - (\ as => addContextAlias (asName modns as n) n) - asm + unless (completeDef entry) $ + ignore $ addContextEntry n def + + whenJust asm $ \ as => addContextAlias (asName modns as n) n + where -- If the definition already exists, don't overwrite it with an empty -- definition or hole. This might happen if a function is declared in one @@ -428,7 +426,7 @@ readFromTTC nestedns loc reexp fname modNS importAs if alreadyDone modNS importAs (allImported defs) then pure (Just (ex, ifaceHash ttc, imported ttc)) else do - traverse (addGlobalDef modNS as) (context ttc) + traverse_ (addGlobalDef modNS as) (context ttc) traverse_ addUserHole (userHoles ttc) setNS (currentNS ttc) when nestedns $ setNestedNS (nestedNS ttc) diff --git a/src/Core/Context.idr b/src/Core/Context.idr index a5da1f15b2..755e0284eb 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -1184,8 +1184,9 @@ addBuiltin : {arity : _} -> {auto x : Ref Ctxt Defs} -> Name -> ClosedTerm -> Totality -> PrimFn arity -> Core () -addBuiltin n ty tot op = - do addDef n $ MkGlobalDef +addBuiltin n ty tot op + = do ignore $ + addDef n $ MkGlobalDef { location = emptyFC , fullname = n , type = ty @@ -1209,8 +1210,6 @@ addBuiltin n ty tot op = , sizeChange = [] } - pure () - export updateDef : {auto c : Ref Ctxt Defs} -> Name -> (Def -> Maybe Def) -> Core () @@ -1220,8 +1219,7 @@ updateDef n fdef | Nothing => pure () case fdef (definition gdef) of Nothing => pure () - Just def' => do addDef n (record { definition = def' } gdef) - pure () + Just def' => ignore $ addDef n (record { definition = def' } gdef) export updateTy : {auto c : Ref Ctxt Defs} -> @@ -1230,8 +1228,7 @@ updateTy i ty = do defs <- get Ctxt Just gdef <- lookupCtxtExact (Resolved i) (gamma defs) | Nothing => pure () - addDef (Resolved i) (record { type = ty } gdef) - pure () + ignore $ addDef (Resolved i) (record { type = ty } gdef) export setCompiled : {auto c : Ref Ctxt Defs} -> @@ -1240,8 +1237,7 @@ setCompiled n cexp = do defs <- get Ctxt Just gdef <- lookupCtxtExact n (gamma defs) | Nothing => pure () - addDef n (record { compexpr = Just cexp } gdef) - pure () + ignore $ addDef n (record { compexpr = Just cexp } gdef) export setNamedCompiled : {auto c : Ref Ctxt Defs} -> @@ -1250,8 +1246,7 @@ setNamedCompiled n cexp = do defs <- get Ctxt Just gdef <- lookupCtxtExact n (gamma defs) | Nothing => pure () - addDef n (record { namedcompexpr = Just cexp } gdef) - pure () + ignore $ addDef n (record { namedcompexpr = Just cexp } gdef) -- Record that the name has been linearity checked so we don't need to do -- it again @@ -1262,8 +1257,7 @@ setLinearCheck i chk = do defs <- get Ctxt Just gdef <- lookupCtxtExact (Resolved i) (gamma defs) | Nothing => pure () - addDef (Resolved i) (record { linearChecked = chk } gdef) - pure () + ignore $ addDef (Resolved i) (record { linearChecked = chk } gdef) export setCtxt : {auto c : Ref Ctxt Defs} -> Context -> Core () @@ -1445,20 +1439,18 @@ setFlag fc n fl Just def <- lookupCtxtExact n (gamma defs) | Nothing => throw (UndefinedName fc n) let flags' = fl :: filter (/= fl) (flags def) - addDef n (record { flags = flags' } def) - pure () + ignore $ addDef n (record { flags = flags' } def) export setNameFlag : {auto c : Ref Ctxt Defs} -> - FC -> Name -> DefFlag -> Core () + FC -> Name -> DefFlag -> Core () setNameFlag fc n fl = do defs <- get Ctxt [(n', i, def)] <- lookupCtxtName n (gamma defs) | [] => throw (UndefinedName fc n) | res => throw (AmbiguousName fc (map fst res)) let flags' = fl :: filter (/= fl) (flags def) - addDef (Resolved i) (record { flags = flags' } def) - pure () + ignore $ addDef (Resolved i) (record { flags = flags' } def) export unsetFlag : {auto c : Ref Ctxt Defs} -> @@ -1468,8 +1460,7 @@ unsetFlag fc n fl Just def <- lookupCtxtExact n (gamma defs) | Nothing => throw (UndefinedName fc n) let flags' = filter (/= fl) (flags def) - addDef n (record { flags = flags' } def) - pure () + ignore $ addDef n (record { flags = flags' } def) export hasFlag : {auto c : Ref Ctxt Defs} -> @@ -1487,8 +1478,7 @@ setSizeChange loc n sc = do defs <- get Ctxt Just def <- lookupCtxtExact n (gamma defs) | Nothing => throw (UndefinedName loc n) - addDef n (record { sizeChange = sc } def) - pure () + ignore $ addDef n (record { sizeChange = sc } def) export setTotality : {auto c : Ref Ctxt Defs} -> @@ -1497,8 +1487,7 @@ setTotality loc n tot = do defs <- get Ctxt Just def <- lookupCtxtExact n (gamma defs) | Nothing => throw (UndefinedName loc n) - addDef n (record { totality = tot } def) - pure () + ignore $ addDef n (record { totality = tot } def) export setCovering : {auto c : Ref Ctxt Defs} -> @@ -1507,8 +1496,7 @@ setCovering loc n tot = do defs <- get Ctxt Just def <- lookupCtxtExact n (gamma defs) | Nothing => throw (UndefinedName loc n) - addDef n (record { totality->isCovering = tot } def) - pure () + ignore $ addDef n (record { totality->isCovering = tot } def) export setTerminating : {auto c : Ref Ctxt Defs} -> @@ -1517,8 +1505,7 @@ setTerminating loc n tot = do defs <- get Ctxt Just def <- lookupCtxtExact n (gamma defs) | Nothing => throw (UndefinedName loc n) - addDef n (record { totality->isTerminating = tot } def) - pure () + ignore $ addDef n (record { totality->isTerminating = tot } def) export getTotality : {auto c : Ref Ctxt Defs} -> @@ -1545,8 +1532,7 @@ setVisibility fc n vis = do defs <- get Ctxt Just def <- lookupCtxtExact n (gamma defs) | Nothing => throw (UndefinedName fc n) - addDef n (record { visibility = vis } def) - pure () + ignore $ addDef n (record { visibility = vis } def) -- Set a name as Private that was previously visible (and, if 'everywhere' is -- set, hide in any modules imported by this one) @@ -2065,7 +2051,7 @@ export setWorkingDir : {auto c : Ref Ctxt Defs} -> String -> Core () setWorkingDir dir = do defs <- get Ctxt - coreLift $ changeDir dir + coreLift_ $ changeDir dir Just cdir <- coreLift $ currentDir | Nothing => throw (InternalError "Can't get current directory") put Ctxt (record { options->dirs->working_dir = cdir } defs) diff --git a/src/Core/Core.idr b/src/Core/Core.idr index ab6c9ead56..a88efc7ae8 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -447,6 +447,12 @@ export %inline ignore : Core a -> Core () ignore = map (\ _ => ()) +-- This would be better if we restrict it to a limited set of IO operations +export +%inline +coreLift_ : IO a -> Core () +coreLift_ op = ignore (coreLift op) + -- Monad (specialised) export %inline (>>=) : Core a -> (a -> Core b) -> Core b @@ -456,6 +462,10 @@ export %inline Left err => pure (Left err) Right val => runCore (f val))) +export %inline +(>>) : Core () -> Core a -> Core a +ma >> mb = ma >>= const mb + -- Flipped bind infixr 1 =<< export %inline @@ -551,8 +561,8 @@ export traverse_ : (a -> Core b) -> List a -> Core () traverse_ f [] = pure () traverse_ f (x :: xs) - = do f x - traverse_ f xs + = Core.do ignore (f x) + traverse_ f xs %inline export @@ -569,7 +579,7 @@ traverseList1_ : (a -> Core b) -> List1 a -> Core () traverseList1_ f xxs = do let x = head xxs let xs = tail xxs - f x + ignore (f x) traverse_ f xs namespace PiInfo @@ -638,7 +648,7 @@ filterM p (x :: xs) export data Ref : (l : label) -> Type -> Type where [search l] - MkRef : IORef a -> Ref x a + MkRef : IORef a -> Ref x a export newRef : (x : label) -> t -> Core (Ref x t) diff --git a/src/Core/LinearCheck.idr b/src/Core/LinearCheck.idr index 8d029ce58a..0c213c08c5 100644 --- a/src/Core/LinearCheck.idr +++ b/src/Core/LinearCheck.idr @@ -87,11 +87,11 @@ mutual else do scty <- updateHoleType useInHole var zs sc as pure (Bind bfc nm (Pi fc' c e ty) scty) updateHoleType useInHole var zs (Bind bfc nm (Pi fc' c e ty) sc) (a :: as) - = do updateHoleUsage False var zs a + = do ignore $ updateHoleUsage False var zs a scty <- updateHoleType useInHole var zs sc as pure (Bind bfc nm (Pi fc' c e ty) scty) updateHoleType useInHole var zs ty as - = do updateHoleUsageArgs False var zs as + = do ignore $ updateHoleUsageArgs False var zs as pure ty updateHoleUsagePats : {auto c : Ref Ctxt Defs} -> diff --git a/src/Core/Normalise.idr b/src/Core/Normalise.idr index 8db20361b6..971091d8dd 100644 --- a/src/Core/Normalise.idr +++ b/src/Core/Normalise.idr @@ -1012,7 +1012,7 @@ mutual | Nothing => pure False let Just sc' = getScrutinee scpos' nargs' | Nothing => pure False - convGen q defs env sc sc' + ignore $ convGen q defs env sc sc' pure (location def == location def') where -- Need to find the position of the scrutinee to see if they are the diff --git a/src/Core/Termination.idr b/src/Core/Termination.idr index 5a500e8a52..a56a8b0551 100644 --- a/src/Core/Termination.idr +++ b/src/Core/Termination.idr @@ -677,7 +677,7 @@ checkPositive loc n_in Unchecked => do (tot', cons) <- calcPositive loc n setTerminating loc n tot' - traverse (\c => setTerminating loc c tot') cons + traverse_ (\c => setTerminating loc c tot') cons pure tot' t => pure t diff --git a/src/Core/Unify.idr b/src/Core/Unify.idr index 19f96f287f..c932ac039f 100644 --- a/src/Core/Unify.idr +++ b/src/Core/Unify.idr @@ -493,7 +493,7 @@ instantiate {newvars} loc mode env mname mref num mdef locs otm tm let newdef = record { definition = PMDef simpleDef [] (STerm 0 rhs) (STerm 0 rhs) [] } mdef - addDef (Resolved mref) newdef + ignore $ addDef (Resolved mref) newdef removeHole mref where precise : Bool @@ -1324,8 +1324,7 @@ setInvertible fc n = do defs <- get Ctxt Just gdef <- lookupCtxtExact n (gamma defs) | Nothing => throw (UndefinedName fc n) - addDef n (record { invertible = True } gdef) - pure () + ignore $ addDef n (record { invertible = True } gdef) public export data SolveMode = Normal -- during elaboration: unifies and searches @@ -1421,7 +1420,7 @@ retryGuess mode smode (hid, (loc, hname)) (type def) [] let gdef = record { definition = PMDef defaultPI [] (STerm 0 tm) (STerm 0 tm) [] } def logTermNF "unify.retry" 5 ("Solved " ++ show hname) [] tm - addDef (Resolved hid) gdef + ignore $ addDef (Resolved hid) gdef removeGuess hid pure True) (\err => case err of @@ -1452,7 +1451,7 @@ retryGuess mode smode (hid, (loc, hname)) let gdef = record { definition = PMDef (MkPMDefInfo NotHole True) [] (STerm 0 tm') (STerm 0 tm') [] } def logTerm "unify.retry" 5 ("Resolved " ++ show hname) tm' - addDef (Resolved hid) gdef + ignore $ addDef (Resolved hid) gdef removeGuess hid pure (holesSolved cs) newcs => do tm' <- case addLazy cs of @@ -1463,7 +1462,7 @@ retryGuess mode smode (hid, (loc, hname)) logTerm "unify.retry" 5 "Retry Delay (constrained)" tm pure $ delayMeta r envb !(getTerm ty) tm let gdef = record { definition = Guess tm' envb newcs } def - addDef (Resolved hid) gdef + ignore $ addDef (Resolved hid) gdef pure False Guess tm envb constrs => do let umode = case smode of @@ -1478,11 +1477,11 @@ retryGuess mode smode (hid, (loc, hname)) [] => do let gdef = record { definition = PMDef (MkPMDefInfo NotHole True) [] (STerm 0 tm) (STerm 0 tm) [] } def logTerm "unify.retry" 5 ("Resolved " ++ show hname) tm - addDef (Resolved hid) gdef + ignore $ addDef (Resolved hid) gdef removeGuess hid pure (holesSolved csAll) newcs => do let gdef = record { definition = Guess tm envb newcs } def - addDef (Resolved hid) gdef + ignore $ addDef (Resolved hid) gdef pure False _ => pure False diff --git a/src/Core/UnifyState.idr b/src/Core/UnifyState.idr index 6d02d48254..427fb96aba 100644 --- a/src/Core/UnifyState.idr +++ b/src/Core/UnifyState.idr @@ -668,8 +668,7 @@ dumpHole' lvl hole show !(toFullNames !(normaliseHoles defs [] ty)) log' lvl $ "\t = " ++ show !(normaliseHoles defs [] tm) ++ "\n\twhen" - traverse dumpConstraint constraints - pure () + traverse_ dumpConstraint constraints (Hole _ p, ty) => log' lvl $ "?" ++ show (fullname gdef) ++ " : " ++ show !(normaliseHoles defs [] ty) @@ -720,12 +719,10 @@ dumpConstraints str n all = do ust <- get UST defs <- get Ctxt let lvl = mkLogLevel str n - if keepLog lvl (logLevel $ session $ options defs) then + when (keepLog lvl (logLevel $ session $ options defs)) $ do let hs = toList (guesses ust) ++ toList (if all then holes ust else currentHoles ust) case hs of [] => pure () _ => do log' lvl "--- CONSTRAINTS AND HOLES ---" - traverse (dumpHole' lvl) (map fst hs) - pure () - else pure () + traverse_ (dumpHole' lvl) (map fst hs) diff --git a/src/Idris/Elab/Implementation.idr b/src/Idris/Elab/Implementation.idr index 83b6eeef24..f0bec93c9e 100644 --- a/src/Idris/Elab/Implementation.idr +++ b/src/Idris/Elab/Implementation.idr @@ -237,9 +237,7 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps named im -- If it's a named implementation, add it as a global hint while -- elaborating the record and bodies - if named - then addOpenHint impName - else pure () + when named $ addOpenHint impName -- Make sure we don't use this name to solve parent constraints -- when elaborating the record, or we'll end up in a cycle! @@ -250,7 +248,7 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps named im names' <- traverse applyEnv (impName :: mtops) let nest' = record { names $= (names' ++) } nest - traverse (processDecl [] nest' env) [impFn] + traverse_ (processDecl [] nest' env) [impFn] unsetFlag fc impName BlockedHint setFlag fc impName TCInline @@ -265,10 +263,10 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps named im body' <- traverse (updateBody upds) body log "elab.implementation" 10 $ "Implementation body: " ++ show body' - traverse (processDecl [] nest' env) body' + traverse_ (processDecl [] nest' env) body' -- 6. Add transformation rules for top level methods - traverse (addTransform impName upds) (methods cdata) + traverse_ (addTransform impName upds) (methods cdata) -- inline flag has done its job, and outside the interface -- it can hurt, so unset it now diff --git a/src/Idris/Elab/Interface.idr b/src/Idris/Elab/Interface.idr index a2a7792623..4d01e32f6e 100644 --- a/src/Idris/Elab/Interface.idr +++ b/src/Idris/Elab/Interface.idr @@ -391,8 +391,7 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body dets meths log "elab.interface" 10 $ "Methods: " ++ show meths log "elab.interface" 5 $ "Making interface data type " ++ show dt - processDecls nest env [dt] - pure () + ignore $ processDecls nest env [dt] elabMethods : (conName : Name) -> List Name -> List Signature -> @@ -405,7 +404,7 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body params) meth_sigs let fns = concat fnsm log "elab.interface" 5 $ "Top level methods: " ++ show fns - traverse (processDecl [] nest env) fns + traverse_ (processDecl [] nest env) fns traverse_ (\n => do mn <- inCurrentNS n setFlag fc mn Inline setFlag fc mn TCInline @@ -499,6 +498,6 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body meth_names paramNames) nconstraints log "elab.interface" 5 $ "Constraint hints from " ++ show constraints ++ ": " ++ show chints - traverse (processDecl [] nest env) (concatMap snd chints) + traverse_ (processDecl [] nest env) (concatMap snd chints) traverse_ (\n => do mn <- inCurrentNS n setFlag fc mn TCInline) (map fst chints) diff --git a/src/Idris/ModTree.idr b/src/Idris/ModTree.idr index 8223ec5057..85e0dca598 100644 --- a/src/Idris/ModTree.idr +++ b/src/Idris/ModTree.idr @@ -184,7 +184,7 @@ buildMod loc num len mod <++> pretty "Building" <++> pretty mod.buildNS <++> parens (pretty src) [] <- process {u} {m} msg src | errs => do emitWarnings - traverse emitError errs + traverse_ emitError errs pure (ferrs ++ errs) emitWarnings traverse_ emitError ferrs diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index f9385a4246..672c4f8c31 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -150,24 +150,24 @@ field fname <|> strField PPostinstall "postinstall" <|> strField PPreclean "preclean" <|> strField PPostclean "postclean" - <|> do exactProperty "depends" + <|> do ignore $ exactProperty "depends" equals ds <- sep packageName pure (PDepends ds) - <|> do exactProperty "modules" + <|> do ignore $ exactProperty "modules" equals ms <- sep (do start <- location m <- moduleIdent end <- location pure (MkFC fname start end, m)) pure (PModules ms) - <|> do exactProperty "main" + <|> do ignore $ exactProperty "main" equals start <- location m <- moduleIdent end <- location pure (PMainMod (MkFC fname start end) m) - <|> do exactProperty "executable" + <|> do ignore $ exactProperty "executable" equals e <- (stringLit <|> packageName) pure (PExec e) @@ -175,7 +175,7 @@ field fname strField : (FC -> String -> DescField) -> String -> Rule DescField strField fieldConstructor fieldName = do start <- location - exactProperty fieldName + ignore $ exactProperty fieldName equals str <- stringLit end <- location @@ -183,7 +183,7 @@ field fname parsePkgDesc : String -> Rule (String, List DescField) parsePkgDesc fname - = do exactProperty "package" + = do ignore $ exactProperty "package" name <- packageName fields <- many (field fname) pure (name, fields) @@ -264,8 +264,7 @@ processOptions Nothing = pure () processOptions (Just (fc, opts)) = do let Right clopts = getOpts (words opts) | Left err => throw (GenericMsg fc err) - preOptions clopts - pure () + ignore $ preOptions clopts compileMain : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> @@ -274,10 +273,8 @@ compileMain : {auto c : Ref Ctxt Defs} -> compileMain mainn mmod exec = do m <- newRef MD initMetadata u <- newRef UST initUState - - loadMainFile mmod - compileExp (PRef replFC mainn) exec - pure () + ignore $ loadMainFile mmod + ignore $ compileExp (PRef replFC mainn) exec prepareCompilation : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> @@ -291,7 +288,7 @@ prepareCompilation pkg opts = addDeps pkg processOptions (options pkg) - preOptions opts + ignore $ preOptions opts runScript (prebuild pkg) @@ -374,10 +371,10 @@ install pkg opts -- not used but might be in the future -- We're in that directory now, so copy the files from -- srcdir/build into it - traverse (installFrom (name pkg) - (srcdir build) - (installPrefix name pkg)) toInstall - coreLift $ changeDir srcdir + traverse_ (installFrom (name pkg) + (srcdir build) + (installPrefix name pkg)) toInstall + coreLift_ $ changeDir srcdir runScript (postinstall pkg) -- Check package without compiling anything. @@ -614,7 +611,7 @@ findIpkg : {auto c : Ref Ctxt Defs} -> findIpkg fname = do Just (dir, ipkgn, up) <- coreLift findIpkgFile | Nothing => pure fname - coreLift $ changeDir dir + coreLift_ $ changeDir dir setWorkingDir dir Right (pname, fs) <- coreLift $ parseFile ipkgn (do desc <- parsePkgDesc ipkgn diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 8d7a1404e4..49de36a70b 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -47,7 +47,9 @@ export plhs : ParseOpts plhs = MkParseOpts False False +%hide Prelude.(>>) %hide Prelude.(>>=) +%hide Core.Core.(>>) %hide Core.Core.(>>=) %hide Prelude.pure %hide Core.Core.pure diff --git a/src/Idris/ProcessIdr.idr b/src/Idris/ProcessIdr.idr index a3b5b1ca55..f93fa9900a 100644 --- a/src/Idris/ProcessIdr.idr +++ b/src/Idris/ProcessIdr.idr @@ -40,7 +40,7 @@ processDecl : {auto c : Ref Ctxt Defs} -> PDecl -> Core (Maybe Error) processDecl decl = catch (do impdecls <- desugarDecl [] decl - traverse (Check.processDecl [] (MkNested []) []) impdecls + traverse_ (Check.processDecl [] (MkNested []) []) impdecls pure Nothing) (\err => do giveUpConstraints -- or we'll keep trying... pure (Just err)) @@ -261,7 +261,7 @@ processMod srcf ttcf msg sourcecode pure (runParser srcf (isLitFile srcf) sourcecode (do p <- prog srcf; eoi; pure p)) | Left err => pure (Just [err]) initHash - traverse addPublicHash (sort hs) + traverse_ addPublicHash (sort hs) resetNextVar when (ns /= nsAsModuleIdent mainNS) $ do let MkFC fname _ _ = headerloc mod diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index 38fc49ffa3..a708ad75b9 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -71,25 +71,24 @@ import System.File showInfo : {auto c : Ref Ctxt Defs} -> (Name, Int, GlobalDef) -> Core () showInfo (n, idx, d) - = do coreLift $ putStrLn (show (fullname d) ++ " ==> " ++ + = do coreLift_ $ putStrLn (show (fullname d) ++ " ==> " ++ show !(toFullNames (definition d))) - coreLift $ putStrLn (show (multiplicity d)) - coreLift $ putStrLn ("Erasable args: " ++ show (eraseArgs d)) - coreLift $ putStrLn ("Detaggable arg types: " ++ show (safeErase d)) - coreLift $ putStrLn ("Specialise args: " ++ show (specArgs d)) - coreLift $ putStrLn ("Inferrable args: " ++ show (inferrable d)) - case compexpr d of - Nothing => pure () - Just expr => coreLift $ putStrLn ("Compiled: " ++ show expr) - coreLift $ putStrLn ("Refers to: " ++ + coreLift_ $ putStrLn (show (multiplicity d)) + coreLift_ $ putStrLn ("Erasable args: " ++ show (eraseArgs d)) + coreLift_ $ putStrLn ("Detaggable arg types: " ++ show (safeErase d)) + coreLift_ $ putStrLn ("Specialise args: " ++ show (specArgs d)) + coreLift_ $ putStrLn ("Inferrable args: " ++ show (inferrable d)) + whenJust (compexpr d) $ \ expr => + coreLift_ $ putStrLn ("Compiled: " ++ show expr) + coreLift_ $ putStrLn ("Refers to: " ++ show !(traverse getFullName (keys (refersTo d)))) - coreLift $ putStrLn ("Refers to (runtime): " ++ + coreLift_ $ putStrLn ("Refers to (runtime): " ++ show !(traverse getFullName (keys (refersToRuntime d)))) - coreLift $ putStrLn ("Flags: " ++ show (flags d)) + coreLift_ $ putStrLn ("Flags: " ++ show (flags d)) when (not (isNil (sizeChange d))) $ let scinfo = map (\s => show (fnCall s) ++ ": " ++ show (fnArgs s)) !(traverse toFullNames (sizeChange d)) in - coreLift $ putStrLn $ + coreLift_ $ putStrLn $ "Size change: " ++ showSep ", " scinfo displayType : {auto c : Ref Ctxt Defs} -> @@ -197,7 +196,7 @@ findCG RefC => pure codegenRefC Other s => case !(getCodegen s) of Just cg => pure cg - Nothing => do coreLift $ putStrLn ("No such code generator: " ++ s) + Nothing => do coreLift_ $ putStrLn ("No such code generator: " ++ s) coreLift $ exitWith (ExitFailure 1) anyAt : (a -> Bool) -> a -> b -> Bool @@ -242,8 +241,8 @@ updateFile update | Nothing => pure (DisplayEdit emptyDoc) -- no file, nothing to do Right content <- coreLift $ readFile f | Left err => throw (FileErr f err) - coreLift $ writeFile (f ++ "~") content - coreLift $ writeFile f (unlines (update (lines content))) + coreLift_ $ writeFile (f ++ "~") content + coreLift_ $ writeFile f (unlines (update (lines content))) pure (DisplayEdit emptyDoc) rtrim : String -> String @@ -617,7 +616,7 @@ execDecls decls = do execDecl decl = do i <- desugarDecl [] decl inidx <- resolveName (UN "[defs]") - newRef EST (initEStateSub inidx [] SubRefl) + _ <- newRef EST (initEStateSub inidx [] SubRefl) processLocal [] (MkNested []) [] !getItDecls i export @@ -682,7 +681,7 @@ equivTypes : {auto c : Ref Ctxt Defs} -> equivTypes ty1 ty2 = do defs <- get Ctxt True <- pure (!(getArity defs [] ty1) == !(getArity defs [] ty2)) | False => pure False - newRef UST initUState + _ <- newRef UST initUState catch (do res <- unify inTerm replFC [] ty1 ty2 case res of (MkUnifyResult _ _ _ NoLazy) => pure True @@ -704,7 +703,7 @@ process (NewDefn decls) = execDecls decls process (Eval itm) = do opts <- get ROpts case evalMode opts of - Execute => do execExp itm; pure (Executed itm) + Execute => do ignore (execExp itm); pure (Executed itm) _ => do ttimp <- desugar AnyExpr [] itm let ttimpWithIt = ILocal replFC !getItDecls ttimp @@ -727,7 +726,9 @@ process (Eval itm) itm <- resugar [] ntm ty <- getTerm gty evalResultName <- DN "it" <$> genName "evalResult" - addDef evalResultName (newDef replFC evalResultName top [] ty Private (PMDef defaultPI [] (STerm 0 ntm) (STerm 0 ntm) [])) + ignore $ addDef evalResultName + $ newDef replFC evalResultName top [] ty Private + $ PMDef defaultPI [] (STerm 0 ntm) (STerm 0 ntm) [] addToSave evalResultName put ROpts (record { evalResultName = Just evalResultName } opts) if showTypes opts @@ -798,7 +799,7 @@ process Edit Nothing => pure NoFileLoaded Just f => do let line = maybe "" (\i => " +" ++ show (i + 1)) (errorLine opts) - coreLift $ system (editor opts ++ " \"" ++ f ++ "\"" ++ line) + coreLift_ $ system (editor opts ++ " \"" ++ f ++ "\"" ++ line) loadMainFile f process (Compile ctm outfile) = compileExp ctm outfile @@ -844,7 +845,7 @@ process (Total n) [] => throw (UndefinedName replFC n) ts => map CheckedTotal $ traverse (\fn => - do checkTotal replFC fn + do ignore $ checkTotal replFC fn tot <- getTotality replFC fn >>= toFullNames pure $ (fn, tot)) (map fst ts) @@ -902,7 +903,7 @@ process (CGDirective str) = do setSession (record { directives $= (str::) } !getSession) pure Done process (RunShellCommand cmd) - = do coreLift (system cmd) + = do coreLift_ (system cmd) pure Done process Quit = pure Exited @@ -981,13 +982,13 @@ mutual repl = do ns <- getNS opts <- get ROpts - coreLift (putStr (prompt (evalMode opts) ++ show ns ++ "> ")) + coreLift_ (putStr (prompt (evalMode opts) ++ show ns ++ "> ")) inp <- coreLift getLine end <- coreLift $ fEOF stdin if end then do -- start a new line in REPL mode (not relevant in IDE mode) - coreLift $ putStrLn "" + coreLift_ $ putStrLn "" iputStrLn $ pretty "Bye for now!" else do res <- interpret inp handleResult res diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr index 518a5c94cb..b9854c7e14 100644 --- a/src/Idris/SetOptions.idr +++ b/src/Idris/SetOptions.idr @@ -140,18 +140,18 @@ postOptions : {auto c : Ref Ctxt Defs} -> REPLResult -> List CLOpt -> Core Bool postOptions _ [] = pure True postOptions res@(ErrorLoadingFile _ _) (OutputFile _ :: rest) - = do postOptions res rest + = do ignore $ postOptions res rest pure False postOptions res (OutputFile outfile :: rest) - = do compileExp (PRef (MkFC "(script)" (0, 0) (0, 0)) (UN "main")) outfile - postOptions res rest + = do ignore $ compileExp (PRef (MkFC "(script)" (0, 0) (0, 0)) (UN "main")) outfile + ignore $ postOptions res rest pure False postOptions res (ExecFn str :: rest) - = do execExp (PRef (MkFC "(script)" (0, 0) (0, 0)) (UN str)) - postOptions res rest + = do ignore $ execExp (PRef (MkFC "(script)" (0, 0) (0, 0)) (UN str)) + ignore $ postOptions res rest pure False postOptions res (CheckOnly :: rest) - = do postOptions res rest + = do ignore $ postOptions res rest pure False postOptions res (RunREPL str :: rest) = do replCmd str diff --git a/src/Libraries/Text/Parser.idr b/src/Libraries/Text/Parser.idr index dd1a03a47b..7ad8f63c4f 100644 --- a/src/Libraries/Text/Parser.idr +++ b/src/Libraries/Text/Parser.idr @@ -154,7 +154,7 @@ mutual (skip : Grammar tok True s) -> (p : Grammar tok c a) -> Grammar tok True a - afterSome skip p = do skip + afterSome skip p = do ignore $ skip afterMany skip p ||| Parse zero or more instance of `skip` until `p` is encountered, diff --git a/src/Libraries/Text/Parser/Core.idr b/src/Libraries/Text/Parser/Core.idr index 11bdfa1d8b..cf0fdf7123 100644 --- a/src/Libraries/Text/Parser/Core.idr +++ b/src/Libraries/Text/Parser/Core.idr @@ -51,6 +51,18 @@ export %inline (>>=) {c1 = False} = SeqEmpty (>>=) {c1 = True} = SeqEat +||| Sequence two grammars. If either consumes some input, the sequence is +||| guaranteed to consume some input. If the first one consumes input, the +||| second is allowed to be recursive (because it means some input has been +||| consumed and therefore the input is smaller) +public export %inline %tcinline +(>>) : {c1, c2 : Bool} -> + Grammar tok c1 () -> + inf c1 (Grammar tok c2 a) -> + Grammar tok (c1 || c2) a +(>>) {c1 = False} ma mb = SeqEmpty ma (const mb) +(>>) {c1 = True} ma mb = SeqEat ma (Delay \ a => mb) + ||| Sequence two grammars. If either consumes some input, the sequence is ||| guaranteed to consume input. This is an explicitly non-infinite version ||| of `>>=`. diff --git a/src/Libraries/Utils/Path.idr b/src/Libraries/Utils/Path.idr index f6a28ed9c9..a44cb8d9dd 100644 --- a/src/Libraries/Utils/Path.idr +++ b/src/Libraries/Utils/Path.idr @@ -167,7 +167,7 @@ bodySeparator = (match $ PTPunct '\\') <|> (match $ PTPunct '/') verbatim : Grammar PathToken True () verbatim = do - count (exactly 2) $ match $ PTPunct '\\' + ignore $ count (exactly 2) $ match $ PTPunct '\\' match $ PTPunct '?' match $ PTPunct '\\' pure () @@ -176,7 +176,7 @@ verbatim = unc : Grammar PathToken True Volume unc = do - count (exactly 2) $ match $ PTPunct '\\' + ignore $ count (exactly 2) $ match $ PTPunct '\\' server <- match PTText bodySeparator share <- match PTText diff --git a/src/Libraries/Utils/Shunting.idr b/src/Libraries/Utils/Shunting.idr index 0645345ee2..c098668449 100644 --- a/src/Libraries/Utils/Shunting.idr +++ b/src/Libraries/Utils/Shunting.idr @@ -120,7 +120,7 @@ shunt stk (Op loc op prec :: rest) = do stk' <- processStack stk op prec shunt ((loc, op, prec) :: stk') rest shunt stk [] - = do traverse (\s => emit (Op (sloc s) (sop s) (sprec s))) stk + = do traverse_ (\s => emit (Op (sloc s) (sop s) (sprec s))) stk [out] <- get Out | out => throw (InternalError "Invalid input to shunting") pure out diff --git a/src/Parser/Rule/Source.idr b/src/Parser/Rule/Source.idr index 0cd906590d..b1f947e93c 100644 --- a/src/Parser/Rule/Source.idr +++ b/src/Parser/Rule/Source.idr @@ -20,9 +20,7 @@ SourceEmptyRule = EmptyRule Token export eoi : SourceEmptyRule () -eoi - = do nextIs "Expected end of input" (isEOI . val) - pure () +eoi = do ignore $ nextIs "Expected end of input" (isEOI . val) where isEOI : Token -> Bool isEOI EndInput = True @@ -332,8 +330,7 @@ export atEnd : (indent : IndentInfo) -> SourceEmptyRule () atEnd indent = eoi - <|> do nextIs "Expected end of block" (isTerminator . val) - pure () + <|> do ignore $ nextIs "Expected end of block" (isTerminator . val) <|> do col <- Common.column if (col <= indent) then pure () diff --git a/src/TTImp/Elab.idr b/src/TTImp/Elab.idr index 56e2aeeaab..bb5f7cca10 100644 --- a/src/TTImp/Elab.idr +++ b/src/TTImp/Elab.idr @@ -62,23 +62,19 @@ normaliseHoleTypes = do ust <- get UST let hs = keys (holes ust) defs <- get Ctxt - traverse (normaliseH defs) hs - pure () + traverse_ (normaliseH defs) hs where updateType : Defs -> Int -> GlobalDef -> Core () updateType defs i def = do ty' <- normaliseHoles defs [] (type def) - addDef (Resolved i) (record { type = ty' } def) - pure () + ignore $ addDef (Resolved i) (record { type = ty' } def) normaliseH : Defs -> Int -> Core () normaliseH defs i - = case !(lookupCtxtExact (Resolved i) (gamma defs)) of - Just gdef => - case definition gdef of - Hole _ _ => updateType defs i gdef - _ => pure () - Nothing => pure () + = whenJust !(lookupCtxtExact (Resolved i) (gamma defs)) $ \ gdef => + case definition gdef of + Hole _ _ => updateType defs i gdef + _ => pure () export addHoleToSave : {auto c : Ref Ctxt Defs} -> diff --git a/src/TTImp/Elab/App.idr b/src/TTImp/Elab/App.idr index 6743b538e2..d8d7d77c59 100644 --- a/src/TTImp/Elab/App.idr +++ b/src/TTImp/Elab/App.idr @@ -442,8 +442,7 @@ mutual case elabMode elabinfo of InLHS _ => -- reset hole and redo it with the unexpanded definition do updateDef (Resolved idx) (const (Just (Hole 0 (holeInit False)))) - solveIfUndefined env metaval argv - pure () + ignore $ solveIfUndefined env metaval argv _ => pure () removeHole idx pure (tm, gty) @@ -634,7 +633,7 @@ mutual fnty <- nf defs env retTy -- (Bind fc argn (Let RigW argv argTy) retTy) let expfnty = gnf env (Bind fc argn (Pi fc top Explicit argTy) (weaken retTy)) logGlue "elab.with" 10 "Expected function type" env expfnty - maybe (pure ()) (logGlue "elab.with" 10 "Expected result type" env) expty + whenJust expty (logGlue "elab.with" 10 "Expected result type" env) res <- checkAppWith rig elabinfo nest env fc fntm fnty (n, 1 + argpos) expargs autoargs namedargs kr expty cres <- Check.convert fc elabinfo env (glueBack defs env ty) expfnty let [] = constraints cres diff --git a/src/TTImp/Elab/Binders.idr b/src/TTImp/Elab/Binders.idr index 4a0d68bfe5..5fbc1eb569 100644 --- a/src/TTImp/Elab/Binders.idr +++ b/src/TTImp/Elab/Binders.idr @@ -156,7 +156,7 @@ checkLambda rig_in elabinfo nest env fc rigl info n argTy scope (Just expty_in) info' <- checkPiInfo rigl elabinfo nest env info (Just (gnf env tyv)) let rigb = rigl `glb` c let env' : Env Term (n :: _) = Lam fc rigb info' tyv :: env - convert fc elabinfo env (gnf env tyv) (gnf env pty) + ignore $ convert fc elabinfo env (gnf env tyv) (gnf env pty) let nest' = weaken (dropName n nest) (scopev, scopet) <- inScope fc env' (\e' => diff --git a/src/TTImp/Elab/Delayed.idr b/src/TTImp/Elab/Delayed.idr index 00395607e4..2bf8f65db6 100644 --- a/src/TTImp/Elab/Delayed.idr +++ b/src/TTImp/Elab/Delayed.idr @@ -252,8 +252,7 @@ retryDelayed : {vars : _} -> retryDelayed ds = do est <- get EST ds <- retryDelayed' RecoverableErrors [] ds -- try everything again - retryDelayed' AllErrors [] ds -- fail on all errors - pure () + ignore $ retryDelayed' AllErrors [] ds -- fail on all errors -- Run an elaborator, then all the delayed elaborators arising from it export @@ -270,9 +269,8 @@ runDelays pri elab tm <- elab ust <- get UST log "elab.delay" 2 $ "Rerunning delayed in elaborator" - handle (do retryDelayed' AllErrors [] - (reverse (filter hasPri (delayedElab ust))) - pure ()) + handle (do ignore $ retryDelayed' AllErrors [] + (reverse (filter hasPri (delayedElab ust)))) (\err => do put UST (record { delayedElab = olddelayed } ust) throw err) ust <- get UST diff --git a/src/TTImp/Elab/ImplicitBind.idr b/src/TTImp/Elab/ImplicitBind.idr index 554d90ebea..0890a3801e 100644 --- a/src/TTImp/Elab/ImplicitBind.idr +++ b/src/TTImp/Elab/ImplicitBind.idr @@ -147,11 +147,10 @@ bindUnsolved {vars} fc elabmode _ sub subEnv !(normaliseHoles defs env exp) logTerm "elab" 5 ("Added unbound implicit") bindtm - unify (case elabmode of + ignore $ unify (case elabmode of InLHS _ => inLHS _ => inTerm) fc env tm bindtm - pure () swapIsVarH : {idx : Nat} -> (0 p : IsVar name idx (x :: y :: xs)) -> Var (y :: x :: xs) diff --git a/src/TTImp/Elab/Local.idr b/src/TTImp/Elab/Local.idr index 099ccda865..d0e02731b5 100644 --- a/src/TTImp/Elab/Local.idr +++ b/src/TTImp/Elab/Local.idr @@ -58,7 +58,7 @@ localHelper {vars} nest env nestdecls_in func -- store the local hints, so we can reset them after we've elaborated -- everything let oldhints = localHints defs - traverse (processDecl [] nest' env') (map (updateName nest') nestdecls) + traverse_ (processDecl [] nest' env') (map (updateName nest') nestdecls) ust <- get UST put UST (record { delayedElab = olddelayed } ust) defs <- get Ctxt diff --git a/src/TTImp/Elab/Utils.idr b/src/TTImp/Elab/Utils.idr index 729db2fe04..5f1cb4bbfa 100644 --- a/src/TTImp/Elab/Utils.idr +++ b/src/TTImp/Elab/Utils.idr @@ -64,9 +64,10 @@ updateErasable n Just gdef <- lookupCtxtExact n (gamma defs) | Nothing => pure () (es, dtes) <- findErased (type gdef) - addDef n (record { eraseArgs = es, - safeErase = dtes } gdef) - pure () + ignore $ addDef n $ record + { eraseArgs = es, + safeErase = dtes } gdef + export wrapErrorC : List ElabOpt -> (Error -> Error) -> Core a -> Core a wrapErrorC opts err diff --git a/src/TTImp/Interactive/ExprSearch.idr b/src/TTImp/Interactive/ExprSearch.idr index 5073de7ffe..c8637ebc2a 100644 --- a/src/TTImp/Interactive/ExprSearch.idr +++ b/src/TTImp/Interactive/ExprSearch.idr @@ -322,8 +322,8 @@ searchName fc rigc opts env target topty (n, ndef) let [] = constraints ures | _ => noResult -- Search the explicit arguments first, they may resolve other holes - traverse (searchIfHole fc opts topty env) - (filter explicit args) + traverse_ (searchIfHole fc opts topty env) + (filter explicit args) args' <- traverse (searchIfHole fc opts topty env) args mkCandidates fc (Ref fc namety n) [] args' @@ -844,9 +844,9 @@ firstLinearOK : {auto c : Ref Ctxt Defs} -> firstLinearOK fc NoMore = noResult firstLinearOK fc (Result (t, ds) next) = handleUnify - (do when (not (isNil ds)) $ + (do unless (isNil ds) $ traverse_ (processDecl [InCase] (MkNested []) []) ds - linearCheck fc linear False [] t + ignore $ linearCheck fc linear False [] t defs <- get Ctxt nft <- normaliseHoles defs [] t raw <- unelab [] !(toFullNames nft) diff --git a/src/TTImp/Parser.idr b/src/TTImp/Parser.idr index 9eaaa3e9e7..8b3ad7159e 100644 --- a/src/TTImp/Parser.idr +++ b/src/TTImp/Parser.idr @@ -23,6 +23,7 @@ collectDefs : List ImpDecl -> List ImpDecl %default covering %hide Prelude.(>>=) +%hide Prelude.(>>) %hide Core.Core.(>>=) %hide Prelude.pure %hide Core.Core.pure diff --git a/src/TTImp/ProcessData.idr b/src/TTImp/ProcessData.idr index a6ff2de2ae..2ec56ca59c 100644 --- a/src/TTImp/ProcessData.idr +++ b/src/TTImp/ProcessData.idr @@ -335,7 +335,7 @@ processData {vars} eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_ra cons <- traverse (checkCon eopts nest env cvis n_in (Resolved tidx)) cons_raw let ddef = MkData (MkCon dfc n arity fullty) cons - addData vars vis tidx ddef + ignore $ addData vars vis tidx ddef -- Flag data type as a newtype, if possible (See `findNewtype` for criteria). -- Skip optimisation if the data type has specified `noNewtype` in its @@ -361,7 +361,7 @@ processData {vars} eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_ra log "declare.data" 10 $ "Saving from " ++ show n ++ ": " ++ show (keys (getMetas ty)) let connames = map conName cons - when (not (NoHints `elem` opts)) $ + unless (NoHints `elem` opts) $ traverse_ (\x => addHintFor fc (Resolved tidx) x True False) connames traverse_ updateErasable (Resolved tidx :: connames) diff --git a/src/TTImp/ProcessDecls.idr b/src/TTImp/ProcessDecls.idr index 93ac0f5c27..3153a08ead 100644 --- a/src/TTImp/ProcessDecls.idr +++ b/src/TTImp/ProcessDecls.idr @@ -96,7 +96,8 @@ checkTotalityOK n checkTotality : FC -> Core (Maybe Error) checkTotality fc - = do checkTotal fc n -- checked lazily, so better calculate here + = do ignore $ checkTotal fc n + -- ^ checked lazily, so better calculate here t <- getTotality fc n err <- checkCovering fc (isCovering t) maybe (case isTerminating t of @@ -174,9 +175,9 @@ processTTImpFile fname | Left err => do coreLift (putStrLn (show err)) pure False logTime "Elaboration" $ - catch (do processTTImpDecls (MkNested []) [] tti + catch (do ignore $ processTTImpDecls (MkNested []) [] tti Nothing <- checkDelayedHoles | Just err => throw err pure True) - (\err => do coreLift (printLn err) + (\err => do coreLift_ (printLn err) pure False) diff --git a/src/TTImp/ProcessDef.idr b/src/TTImp/ProcessDef.idr index f981ef3d5e..d1b6b3f3e2 100644 --- a/src/TTImp/ProcessDef.idr +++ b/src/TTImp/ProcessDef.idr @@ -597,7 +597,7 @@ calcRefs rt at fn refs <- ifThenElse rt (dropErased (keys refs_all) refs_all) (pure refs_all) - ifThenElse rt + ignore $ ifThenElse rt (addDef fn (record { refersToRuntimeM = Just refs } gdef)) (addDef fn (record { refersToM = Just refs } gdef)) traverse_ (calcRefs rt at) (keys refs) @@ -648,9 +648,9 @@ mkRunTime fc n let Just Refl = nameListEq cargs rargs | Nothing => throw (InternalError "WAT") - addDef n (record { definition = PMDef r rargs tree_ct tree_rt pats - } gdef) - pure () + ignore $ addDef n $ + record { definition = PMDef r rargs tree_ct tree_rt pats + } gdef where mkCrash : {vars : _} -> String -> Term vars mkCrash msg @@ -699,7 +699,7 @@ compileRunTime : {auto c : Ref Ctxt Defs} -> compileRunTime fc atotal = do defs <- get Ctxt traverse_ (mkRunTime fc) (toCompileCase defs) - traverse (calcRefs True atotal) (toCompileCase defs) + traverse_ (calcRefs True atotal) (toCompileCase defs) defs <- get Ctxt put Ctxt (record { toCompileCase = [] } defs) @@ -755,7 +755,7 @@ processDef opts nest env fc n_in cs_in -- Add compile time tree as a placeholder for the runtime tree, -- but we'll rebuild that in a later pass once all the case -- blocks etc are resolved - addDef (Resolved nidx) + ignore $ addDef (Resolved nidx) (record { definition = PMDef defaultPI cargs tree_ct tree_ct pats } gdef) diff --git a/src/TTImp/ProcessParams.idr b/src/TTImp/ProcessParams.idr index 81765df069..01900cea43 100644 --- a/src/TTImp/ProcessParams.idr +++ b/src/TTImp/ProcessParams.idr @@ -53,8 +53,7 @@ processParams {vars} {c} {m} {u} nest env fc ps ds let defNames = definedInBlock (currentNS defs) ds names' <- traverse (applyEnv env') defNames let nestBlock = record { names $= (names' ++) } nest' - traverse (processDecl [] nestBlock env') ds - pure () + traverse_ (processDecl [] nestBlock env') ds where mkParamTy : List (Name, RawImp) -> RawImp mkParamTy [] = IType fc diff --git a/src/TTImp/ProcessRunElab.idr b/src/TTImp/ProcessRunElab.idr index c5314a1d82..bdf8cb0961 100644 --- a/src/TTImp/ProcessRunElab.idr +++ b/src/TTImp/ProcessRunElab.idr @@ -34,5 +34,4 @@ processRunElab eopts nest env fc tm exp <- appCon fc defs n [unit] stm <- checkTerm tidx InExpr eopts nest env tm (gnf env exp) - elabScript fc nest env !(nfOpts withAll defs env stm) Nothing - pure () + ignore $ elabScript fc nest env !(nfOpts withAll defs env stm) Nothing diff --git a/src/TTImp/ProcessType.idr b/src/TTImp/ProcessType.idr index 784d4ebea2..d82c6cc35d 100644 --- a/src/TTImp/ProcessType.idr +++ b/src/TTImp/ProcessType.idr @@ -69,8 +69,7 @@ processFnOpt fc _ ndef (SpecArgs ns) ps <- getNamePos 0 nty ddeps <- collectDDeps nty specs <- collectSpec [] ddeps ps nty - addDef ndef (record { specArgs = specs } gdef) - pure () + ignore $ addDef ndef (record { specArgs = specs } gdef) where insertDeps : List Nat -> List (Name, Nat) -> List Name -> List Nat insertDeps acc ps [] = acc @@ -289,7 +288,7 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc nameFC n_in ty_ra empty <- clearDefs defs infargs <- findInferrable empty !(nf defs [] fullty) - addDef (Resolved idx) + ignore $ addDef (Resolved idx) (record { eraseArgs = erased, safeErase = dterased, inferrable = infargs } @@ -298,7 +297,7 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc nameFC n_in ty_ra -- from the top level. -- But, if it's a case block, it'll be checked as part of the top -- level check so don't set the flag. - when (not (InCase `elem` eopts)) $ setLinearCheck idx True + unless (InCase `elem` eopts) $ setLinearCheck idx True log "declare.type" 2 $ "Setting options for " ++ show n ++ ": " ++ show opts let name = Resolved idx @@ -307,7 +306,7 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc nameFC n_in ty_ra isNested (NS _ n) = isNested n isNested _ = False let nested = not (isNested n) - traverse (processFnOpt fc (not (isNested n)) name) opts + traverse_ (processFnOpt fc (not (isNested n)) name) opts -- If no function-specific totality pragma has been used, attach the default totality unless (any isTotalityReq opts) $ setFlag fc name (SetTotal !getDefaultTotalityOption) diff --git a/src/TTImp/WithClause.idr b/src/TTImp/WithClause.idr index 17585bbee1..667d583058 100644 --- a/src/TTImp/WithClause.idr +++ b/src/TTImp/WithClause.idr @@ -110,7 +110,7 @@ mutual case lookup n rest' of Nothing => pure ((n, tm) :: rest') Just tm' => - do getMatch lhs tm tm' -- just need to know it succeeds + do ignore $ getMatch lhs tm tm' -- just need to know it succeeds mergeMatches lhs rest -- Get the arguments for the rewritten pattern clause of a with by looking diff --git a/src/Yaffle/Main.idr b/src/Yaffle/Main.idr index 9149f3639b..6e2d611b4b 100644 --- a/src/Yaffle/Main.idr +++ b/src/Yaffle/Main.idr @@ -35,7 +35,7 @@ processArgs : List String -> Core Bool processArgs [] = pure False processArgs ["--timing"] = pure True processArgs _ - = coreLift $ do putStrLn usage + = coreLift $ do ignore $ putStrLn usage exitWith (ExitFailure 1) HasNames () where @@ -54,16 +54,16 @@ yaffleMain fname args setLogTimings t addPrimitives case extension fname of - Just "ttc" => do coreLift $ putStrLn "Processing as TTC" - readFromTTC {extra = ()} True emptyFC True fname (nsAsModuleIdent emptyNS) emptyNS - coreLift $ putStrLn "Read TTC" - _ => do coreLift $ putStrLn "Processing as TTImp" + Just "ttc" => do coreLift_ $ putStrLn "Processing as TTC" + ignore $ readFromTTC {extra = ()} True emptyFC True fname (nsAsModuleIdent emptyNS) emptyNS + coreLift_ $ putStrLn "Read TTC" + _ => do coreLift_ $ putStrLn "Processing as TTImp" ok <- processTTImpFile fname when ok $ do ns <- pathToNS (working_dir d) (source_dir d) fname makeBuildDirectory ns writeToTTC () !(getTTCFileName fname "ttc") - coreLift $ putStrLn "Written TTC" + coreLift_ $ putStrLn "Written TTC" ust <- get UST repl {c} {u} diff --git a/src/Yaffle/REPL.idr b/src/Yaffle/REPL.idr index ed841fbfaa..41c4de5996 100644 --- a/src/Yaffle/REPL.idr +++ b/src/Yaffle/REPL.idr @@ -28,7 +28,7 @@ import Parser.Source showInfo : (Name, Int, GlobalDef) -> Core () showInfo (n, _, d) - = coreLift $ putStrLn (show n ++ " ==>\n" ++ + = coreLift_ $ putStrLn (show n ++ " ==>\n" ++ "\t" ++ show (definition d) ++ "\n" ++ "\t" ++ show (sizeChange d) ++ "\n") @@ -41,26 +41,26 @@ process (Eval ttimp) = do (tm, _) <- elabTerm 0 InExpr [] (MkNested []) [] ttimp Nothing defs <- get Ctxt tmnf <- normalise defs [] tm - coreLift (printLn !(unelab [] tmnf)) + coreLift_ (printLn !(unelab [] tmnf)) pure True process (Check (IVar _ n)) = do defs <- get Ctxt ns <- lookupTyName n (gamma defs) - traverse printName ns + traverse_ printName ns pure True where printName : (Name, Int, ClosedTerm) -> Core () printName (n, _, tyh) = do defs <- get Ctxt ty <- normaliseHoles defs [] tyh - coreLift $ putStrLn $ show n ++ " : " ++ - show !(unelab [] ty) + coreLift_ $ putStrLn $ show n ++ " : " ++ + show !(unelab [] ty) process (Check ttimp) = do (tm, gty) <- elabTerm 0 InExpr [] (MkNested []) [] ttimp Nothing defs <- get Ctxt tyh <- getTerm gty ty <- normaliseHoles defs [] tyh - coreLift (printLn !(unelab [] ty)) + coreLift_ (printLn !(unelab [] ty)) pure True process (ProofSearch n_in) = do defs <- get Ctxt @@ -70,7 +70,7 @@ process (ProofSearch n_in) def <- search toplevelFC top False 1000 n ty [] defs <- get Ctxt defnf <- normaliseHoles defs [] def - coreLift (printLn !(toFullNames defnf)) + coreLift_ (printLn !(toFullNames defnf)) pure True process (ExprSearch n_in) = do defs <- get Ctxt @@ -83,18 +83,18 @@ process (ExprSearch n_in) process (GenerateDef line name) = do defs <- get Ctxt Just (_, n', _, _) <- findTyDeclAt (\p, n => onLine line p) - | Nothing => do coreLift (putStrLn ("Can't find declaration for " ++ show name)) + | Nothing => do coreLift_ (putStrLn ("Can't find declaration for " ++ show name)) pure True case !(lookupDefExact n' (gamma defs)) of Just None => catch (do ((fc, cs) :: _) <- logTime "Generation" $ makeDefN (\p, n => onLine line p) 1 n' - | _ => coreLift (putStrLn "Failed") - coreLift $ putStrLn (show cs)) - (\err => coreLift $ putStrLn $ "Can't find a definition for " ++ show n') - Just _ => coreLift $ putStrLn "Already defined" - Nothing => coreLift $ putStrLn $ "Can't find declaration for " ++ show name + | _ => coreLift_ (putStrLn "Failed") + coreLift_ $ putStrLn (show cs)) + (\err => coreLift_ $ putStrLn $ "Can't find a definition for " ++ show n') + Just _ => coreLift_ $ putStrLn "Already defined" + Nothing => coreLift_ $ putStrLn $ "Can't find declaration for " ++ show name pure True process (Missing n_in) = do defs <- get Ctxt @@ -104,15 +104,15 @@ process (Missing n_in) do tot <- getTotality emptyFC fn the (Core ()) $ case isCovering tot of MissingCases cs => - coreLift (putStrLn (show fn ++ ":\n" ++ + coreLift_ (putStrLn (show fn ++ ":\n" ++ showSep "\n" (map show cs))) NonCoveringCall ns => - coreLift (putStrLn + coreLift_ (putStrLn (show fn ++ ": Calls non covering function" ++ case ns of [fn] => " " ++ show fn _ => "s: " ++ showSep ", " (map show ns))) - _ => coreLift $ putStrLn (show fn ++ ": All cases covered")) + _ => coreLift_ $ putStrLn (show fn ++ ": All cases covered")) (map fst ts) pure True process (CheckTotal n) @@ -120,17 +120,17 @@ process (CheckTotal n) case !(lookupCtxtName n (gamma defs)) of [] => throw (UndefinedName emptyFC n) ts => do traverse_ (\fn => - do checkTotal emptyFC fn + do ignore $ checkTotal emptyFC fn tot <- getTotality emptyFC fn - coreLift (putStrLn (show fn ++ " is " ++ show tot))) + coreLift_ (putStrLn (show fn ++ " is " ++ show tot))) (map fst ts) pure True process (DebugInfo n) = do defs <- get Ctxt - traverse showInfo !(lookupCtxtName n (gamma defs)) + traverse_ showInfo !(lookupCtxtName n (gamma defs)) pure True process Quit - = do coreLift $ putStrLn "Bye for now!" + = do coreLift_ $ putStrLn "Bye for now!" pure False processCatch : {auto c : Ref Ctxt Defs} -> @@ -139,7 +139,7 @@ processCatch : {auto c : Ref Ctxt Defs} -> ImpREPL -> Core Bool processCatch cmd = catch (process cmd) - (\err => do coreLift (putStrLn (show err)) + (\err => do coreLift_ (putStrLn (show err)) pure True) export @@ -148,12 +148,9 @@ repl : {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> Core () repl - = do coreLift (putStr "Yaffle> ") + = do coreLift_ (putStr "Yaffle> ") inp <- coreLift getLine case runParser "(interactive)" Nothing inp command of - Left err => do coreLift (printLn err) + Left err => do coreLift_ (printLn err) repl - Right cmd => - do if !(processCatch cmd) - then repl - else pure () + Right cmd => when !(processCatch cmd) repl diff --git a/tests/Lib.idr b/tests/Lib.idr index 7a155fad33..479bca2892 100644 --- a/tests/Lib.idr +++ b/tests/Lib.idr @@ -144,7 +144,7 @@ runTest opts testPath = forkIO $ do let cg = case codegen opts of Nothing => "" Just cg => "env IDRIS2_TESTS_CG=" ++ cg ++ " " - system $ "cd " ++ testPath ++ " && " ++ + ignore $ system $ "cd " ++ testPath ++ " && " ++ cg ++ "sh ./run " ++ exeUnderTest opts ++ " | tr -d '\\r' > output" end <- clockTime Thread From 2353ca0c4e650449e3c6d0ddfe592a867c2b512d Mon Sep 17 00:00:00 2001 From: Guillaume ALLAIS Date: Sat, 20 Feb 2021 01:18:05 +0000 Subject: [PATCH 02/12] [ fix #758 ] desugar to (>>) --- src/Idris/Desugar.idr | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index fcc95cd926..98e40bcc3c 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -432,14 +432,8 @@ mutual expandDo side ps topfc ns (DoExp fc tm :: rest) = do tm' <- desugar side ps tm rest' <- expandDo side ps topfc ns rest - -- A free standing 'case' block must return () - let ty = case tm' of - ICase _ _ _ _ => IVar fc (UN "Unit") - _ => Implicit fc False gam <- get Ctxt - pure $ IApp fc (IApp fc (IVar fc (addNS ns (UN ">>="))) tm') - (ILam fc top Explicit Nothing - ty rest') + pure $ IApp fc (IApp fc (IVar fc (addNS ns (UN ">>"))) tm') rest' expandDo side ps topfc ns (DoBind fc nameFC n tm :: rest) = do tm' <- desugar side ps tm rest' <- expandDo side ps topfc ns rest From d8af56983f84a6eb0a29590175e2a6d5588f72ff Mon Sep 17 00:00:00 2001 From: Guillaume ALLAIS Date: Sat, 20 Feb 2021 01:22:31 +0000 Subject: [PATCH 03/12] [ test ] case for the fix --- tests/Main.idr | 3 ++- tests/idris2/linear013/Issue758.idr | 15 +++++++++++++++ tests/idris2/linear013/expected | 9 +++++++++ tests/idris2/linear013/input | 2 ++ tests/idris2/linear013/run | 3 +++ 5 files changed, 31 insertions(+), 1 deletion(-) create mode 100644 tests/idris2/linear013/Issue758.idr create mode 100644 tests/idris2/linear013/expected create mode 100644 tests/idris2/linear013/input create mode 100644 tests/idris2/linear013/run diff --git a/tests/Main.idr b/tests/Main.idr index 2606d5c750..30e07448ef 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -91,7 +91,8 @@ idrisTestsLinear = MkTestPool [] -- QTT and linearity related ["linear001", "linear002", "linear003", -- "linear004" -- disabled due to requiring linearity subtyping "linear005", "linear006", "linear007", "linear008", - "linear009", "linear010", "linear011", "linear012"] + "linear009", "linear010", "linear011", "linear012", + "linear013"] idrisTestsLiterate : TestPool idrisTestsLiterate = MkTestPool [] diff --git a/tests/idris2/linear013/Issue758.idr b/tests/idris2/linear013/Issue758.idr new file mode 100644 index 0000000000..7003abac5d --- /dev/null +++ b/tests/idris2/linear013/Issue758.idr @@ -0,0 +1,15 @@ +module Issue758 + +-- introduce linear bind and linear pure +interface LMonad m where + pure : (1 _ : a) -> m a + (>>=) : (1 _ : m a) -> (1 _ : (1 _ : a) -> m b) -> m b + +(>>) : LMonad m => (1 _ : m ()) -> (1 _ : m a) -> m a +ma >> mb = ma >>= \ () => mb + +fail : LMonad m => (1 _ : m ((1 _ : a) -> b)) -> (1 _ : a) -> m b +fail ma a = do f <- ma + ?what_is_f + pure (f a) + diff --git a/tests/idris2/linear013/expected b/tests/idris2/linear013/expected new file mode 100644 index 0000000000..94deab70b4 --- /dev/null +++ b/tests/idris2/linear013/expected @@ -0,0 +1,9 @@ +1/1: Building Issue758 (Issue758.idr) +Issue758> 0 b : Type + 0 m : Type -> Type + 0 a : a + 0 ma : m ((1 _ : a) -> b) + 0 f : (1 _ : a) -> b +------------------------------ +what_is_f : m () +Issue758> Bye for now! diff --git a/tests/idris2/linear013/input b/tests/idris2/linear013/input new file mode 100644 index 0000000000..053de6c316 --- /dev/null +++ b/tests/idris2/linear013/input @@ -0,0 +1,2 @@ +:t what_is_f +:q diff --git a/tests/idris2/linear013/run b/tests/idris2/linear013/run new file mode 100644 index 0000000000..287d9b43f5 --- /dev/null +++ b/tests/idris2/linear013/run @@ -0,0 +1,3 @@ +$1 --no-color --console-width 0 --no-banner Issue758.idr < input + +rm -rf build From 968038b6fa19c9fa337ca94bf1a97dc83ae8af97 Mon Sep 17 00:00:00 2001 From: Guillaume ALLAIS Date: Sat, 20 Feb 2021 01:35:47 +0000 Subject: [PATCH 04/12] [ fix ] test suite --- tests/chez/chez017/dir.idr | 2 +- tests/chez/chez018/File.idr | 2 +- tests/chez/chez027/StringParser.idr | 4 ++-- tests/chez/semaphores002/Main.idr | 2 +- tests/idris2/basic041/QDo.idr | 12 ++++++++++-- tests/idris2/basic041/expected | 14 +++++++------- tests/idris2/real001/Channel.idr | 6 +++++- tests/idris2/real001/Linear.idr | 9 +++++++++ tests/idris2/real002/Control/App.idr | 15 +++++++++++++++ tests/idris2/real002/StoreL.idr | 5 +++-- tests/idris2/reflection003/expected | 2 +- tests/idris2/reflection003/refprims.idr | 2 +- tests/idris2/reflection009/perf.idr | 25 ++++++++++++------------- tests/idris2/reg006/Cmd.idr | 3 +++ tests/idris2/reg008/Vending.idr | 17 +++++++++++++---- tests/node/node017/dir.idr | 2 +- tests/node/node018/File.idr | 2 +- tests/racket/semaphores002/Main.idr | 2 +- 18 files changed, 87 insertions(+), 39 deletions(-) diff --git a/tests/chez/chez017/dir.idr b/tests/chez/chez017/dir.idr index 0e687c920c..9fb71c7d17 100644 --- a/tests/chez/chez017/dir.idr +++ b/tests/chez/chez017/dir.idr @@ -10,5 +10,5 @@ main = do Right () <- createDir "testdir" printLn ok ok <- changeDir "testdir" printLn ok - writeFile "test.txt" "hello\n" + ignore $ writeFile "test.txt" "hello\n" printLn !currentDir diff --git a/tests/chez/chez018/File.idr b/tests/chez/chez018/File.idr index ee17155065..f6b03c7888 100644 --- a/tests/chez/chez018/File.idr +++ b/tests/chez/chez018/File.idr @@ -5,7 +5,7 @@ main = do Right ok <- readFile "test.txt" | Left err => printLn err putStr ok - writeFile "testout.txt" "abc\ndef\n" + ignore $ writeFile "testout.txt" "abc\ndef\n" Right ok <- readFile "testout.txt" | Left err => printLn err putStr ok diff --git a/tests/chez/chez027/StringParser.idr b/tests/chez/chez027/StringParser.idr index c0a6963a6c..a22e99d558 100644 --- a/tests/chez/chez027/StringParser.idr +++ b/tests/chez/chez027/StringParser.idr @@ -30,13 +30,13 @@ pureParsing str = parse (many (satisfy isDigit)) str -- test option optParser : ParseT IO String optParser = do res <- option "" (takeWhile isDigit) - string "def" + ignore $ string "def" pure $ res -- test optional maybeParser : ParseT IO Bool maybeParser = do res <- optional (string "abc") - string "def" + ignore $ string "def" pure $ isJust res main : IO () diff --git a/tests/chez/semaphores002/Main.idr b/tests/chez/semaphores002/Main.idr index 0028f420c7..94cd3aec95 100644 --- a/tests/chez/semaphores002/Main.idr +++ b/tests/chez/semaphores002/Main.idr @@ -5,7 +5,7 @@ import System.Concurrency main : IO () main = do sema <- makeSemaphore 0 - fork $ do + ignore $ fork $ do putStrLn "Hello" semaphorePost sema semaphorePost sema diff --git a/tests/idris2/basic041/QDo.idr b/tests/idris2/basic041/QDo.idr index b80f90e159..4818615247 100644 --- a/tests/idris2/basic041/QDo.idr +++ b/tests/idris2/basic041/QDo.idr @@ -3,6 +3,10 @@ namespace MyDo (>>=) : a -> (a -> IO b) -> IO b (>>=) val k = k val + export + (>>) : a -> IO b -> IO b + a >> f = a >>= const f + foo : IO () foo = MyDo.do x <- "Silly" @@ -14,14 +18,18 @@ namespace A (>>=) : Nat -> (() -> Nat) -> Nat (>>=) x fy = x + (fy ()) + export + (>>) : Nat -> Nat -> Nat + a >> f = a >>= const f + test : Nat test = B.A.do 5 - 6 + _ <- 6 7 test2 : Nat test2 = A.B.do 5 - 6 + _ <- 6 7 diff --git a/tests/idris2/basic041/expected b/tests/idris2/basic041/expected index b93caafb70..a0739eddc7 100644 --- a/tests/idris2/basic041/expected +++ b/tests/idris2/basic041/expected @@ -1,11 +1,11 @@ 1/1: Building QDo (QDo.idr) -Error: While processing right hand side of test. Undefined name B.A.>>=. +Error: While processing right hand side of test. Undefined name B.A.>>. -QDo.idr:19:10--19:11 - 15 | (>>=) x fy = x + (fy ()) - 16 | - 17 | test : Nat - 18 | test = B.A.do - 19 | 5 +QDo.idr:27:10--27:11 + 23 | a >> f = a >>= const f + 24 | + 25 | test : Nat + 26 | test = B.A.do + 27 | 5 ^ diff --git a/tests/idris2/real001/Channel.idr b/tests/idris2/real001/Channel.idr index d0030a63d7..e7a587a1d6 100644 --- a/tests/idris2/real001/Channel.idr +++ b/tests/idris2/real001/Channel.idr @@ -30,6 +30,10 @@ public export (>>=) : Protocol a -> (a -> Protocol b) -> Protocol b (>>=) = Bind +public export +(>>) : Protocol a -> Protocol b -> Protocol b +ma >> mb = ma >>= \ _ => mb + public export ClientK : Protocol a -> (a -> Actions b) -> Actions b ClientK (Request a) k = Send a k @@ -213,5 +217,5 @@ fork proc -- deconstruct and reconstruct is a hack to work around the fact that -- 'run' doesn't express the function is only used once in its type, because -- 'Monad' and 'Applicative' don't express linearity... ugh! - lift $ fork (run (proc (MkChannel a b c d e))) + lift $ ignore $ fork (run (proc (MkChannel a b c d e))) pure cchan diff --git a/tests/idris2/real001/Linear.idr b/tests/idris2/real001/Linear.idr index 2ee4cde8ec..60b5430237 100644 --- a/tests/idris2/real001/Linear.idr +++ b/tests/idris2/real001/Linear.idr @@ -35,6 +35,15 @@ public export (>>=) {p=Once} = BindOnce (>>=) {p=Many} = BindMany +public export +delay : {p : _} -> (1 k : Lin m q b) -> contType m p q () b +delay {p=Once} mb = \ () => mb +delay {p=Many} mb = \ _ => mb + +public export +(>>) : {p : _} -> (1 f : Lin m p ()) -> (1 k : Lin m q b) -> Lin m q b +ma >> mb = ma >>= delay mb + export run : Monad m => Lin m usage t -> m t run (Pure x) = pure x diff --git a/tests/idris2/real002/Control/App.idr b/tests/idris2/real002/Control/App.idr index 72f4b6b3ff..57e9a2fd82 100644 --- a/tests/idris2/real002/Control/App.idr +++ b/tests/idris2/real002/Control/App.idr @@ -157,6 +157,10 @@ bindL (MkApp prog) next r world' Left err => absurdWith2 next world' err +export +seqL : App {l=NoThrow} e () -> (1 k : App {l} e b) -> App {l} e b +seqL ma mb = bindL ma (\ () => mb) + export app : (1 p : App {l=NoThrow} e a) -> App1 {u=Any} e a app (MkApp prog) @@ -201,6 +205,17 @@ namespace App1 (1 k : Cont1Type u a u' e b) -> App1 {u=u'} e b (>>=) = bindApp1 + export + delay : {u : _} -> (1 k : App1 {u=u'} e b) -> + Cont1Type u a u' e b + delay {u = One} mb = \ () => mb + delay {u = Any} mb = \ _ => mb + + export + (>>) : {u : _} -> (1 act : App1 {u} e ()) -> + (1 k : App1 {u=u'} e b) -> App1 {u=u'} e b + ma >> mb = ma >>= delay mb + export pure : (x : a) -> App1 {u=Any} e a pure x = MkApp1 $ \w => MkApp1ResW x w diff --git a/tests/idris2/real002/StoreL.idr b/tests/idris2/real002/StoreL.idr index 903490de57..31eeb91686 100644 --- a/tests/idris2/real002/StoreL.idr +++ b/tests/idris2/real002/StoreL.idr @@ -15,11 +15,11 @@ interface StoreI e where Has [Console] e => StoreI e where connect f = let (>>=) = bindL in + let (>>) = seqL in do putStrLn "Connected" f (MkStore "xyzzy") disconnect (MkStore _) - = do putStrLn "Disconnected" - pure () + = do ignore $ putStrLn "Disconnected" login : (1 s : Store LoggedOut) -> (password : String) -> Res Bool (\ok => Store (if ok then LoggedIn else LoggedOut)) @@ -32,6 +32,7 @@ logout (MkStore secret) = MkStore secret storeProg : Has [Console, StoreI] e => App e () storeProg = let (>>=) = bindL in + let (>>) = seqL in do putStr "Password: " password <- Console.getStr connect $ \s => diff --git a/tests/idris2/reflection003/expected b/tests/idris2/reflection003/expected index 5dc50fa175..48d39f09be 100644 --- a/tests/idris2/reflection003/expected +++ b/tests/idris2/reflection003/expected @@ -35,7 +35,7 @@ refprims.idr:49:10--49:25 49 | dummy3 = %runElab logBad ^^^^^^^^^^^^^^^ -Error: While processing right hand side of dummy4. Error during reflection: failed after generating Main.{plus:XXXX} +Error: While processing right hand side of dummy4. Error during reflection: failed after generating Main.{plus:XXX} refprims.idr:52:10--52:28 48 | dummy3 : a diff --git a/tests/idris2/reflection003/refprims.idr b/tests/idris2/reflection003/refprims.idr index e61d057726..48662ee2ee 100644 --- a/tests/idris2/reflection003/refprims.idr +++ b/tests/idris2/reflection003/refprims.idr @@ -5,7 +5,7 @@ import Language.Reflection logPrims : Elab a logPrims = do ns <- getType `{{ (++) }} - traverse (\ (n, ty) => + traverse_ (\ (n, ty) => do logMsg "" 0 ("Name: " ++ show n) logTerm "" 0 "Type" ty) ns fail "Not really trying" diff --git a/tests/idris2/reflection009/perf.idr b/tests/idris2/reflection009/perf.idr index 237d29f207..dba73a8549 100644 --- a/tests/idris2/reflection009/perf.idr +++ b/tests/idris2/reflection009/perf.idr @@ -11,29 +11,28 @@ import Language.Reflection perftest : Elab () perftest = do logMsg "" 0 "Progress" - traverse (traverse (logMsg "" 1 . show)) [[the Int 1..10]] -- minor difference + traverse_ (traverse (logMsg "" 1 . show)) [[the Int 1..10]] -- minor difference logMsg "" 0 "Progress" - traverse (traverse (logMsg "" 2 . show)) [[the Int 1..10]] -- minor difference + traverse_ (traverse (logMsg "" 2 . show)) [[the Int 1..10]] -- minor difference logMsg "" 0 "Progress" - traverse (traverse (logMsg "" 3 . show)) [[the Int 1..10]] -- minor difference + traverse_ (traverse (logMsg "" 3 . show)) [[the Int 1..10]] -- minor difference logMsg "" 0 "Progress" - traverse (traverse (logMsg "" 4 . show)) [[the Int 1..10]] -- minor difference + traverse_ (traverse (logMsg "" 4 . show)) [[the Int 1..10]] -- minor difference logMsg "" 0 "Progress" - traverse (traverse (logMsg "" 5 . show)) [[the Int 1..10]] -- minor difference + traverse_ (traverse (logMsg "" 5 . show)) [[the Int 1..10]] -- minor difference logMsg "" 0 "Progress" - traverse (traverse (logMsg "" 6 . show)) [[the Int 1..10]] -- minor difference + traverse_ (traverse (logMsg "" 6 . show)) [[the Int 1..10]] -- minor difference logMsg "" 0 "Progress" - traverse (traverse (logMsg "" 7 . show)) [[the Int 1..10]] -- 0.3s + traverse_ (traverse (logMsg "" 7 . show)) [[the Int 1..10]] -- 0.3s logMsg "" 0 "Progress" - traverse (traverse (logMsg "" 8 . show)) [[the Int 1..10]] -- 0.4s + traverse_ (traverse (logMsg "" 8 . show)) [[the Int 1..10]] -- 0.4s logMsg "" 0 "Progress" - traverse (traverse (logMsg "" 9 . show)) [[the Int 1..10]] -- 0.5s + traverse_ (traverse (logMsg "" 9 . show)) [[the Int 1..10]] -- 0.5s logMsg "" 0 "Progress" - traverse (traverse (logMsg "" 10 . show)) [[the Int 1..10]] -- 1.5s + traverse_ (traverse (logMsg "" 10 . show)) [[the Int 1..10]] -- 1.5s logMsg "" 0 "Progress" - traverse (traverse (logMsg "" 11 . show)) [[the Int 1..10]] -- 4s + traverse_ (traverse (logMsg "" 11 . show)) [[the Int 1..10]] -- 4s logMsg "" 0 "Progress" - traverse (traverse (logMsg "" 12 . show)) [[the Int 1..10]] -- 13s - pure () + traverse_ (traverse (logMsg "" 12 . show)) [[the Int 1..10]] -- 13s %runElab perftest diff --git a/tests/idris2/reg006/Cmd.idr b/tests/idris2/reg006/Cmd.idr index ab5928faf0..0d6f76ef8f 100644 --- a/tests/idris2/reg006/Cmd.idr +++ b/tests/idris2/reg006/Cmd.idr @@ -5,6 +5,9 @@ data MyCmd : Type -> Type where Pure : ty -> MyCmd ty (>>=) : MyCmd a -> (a -> MyCmd b) -> MyCmd b +(>>) : MyCmd () -> MyCmd a -> MyCmd a +ma >> mb = ma >>= const mb + runMyCmd : MyCmd a -> IO a runMyCmd (Display str) = putStrLn str runMyCmd Input = do str <- getLine diff --git a/tests/idris2/reg008/Vending.idr b/tests/idris2/reg008/Vending.idr index ca73dd7e9f..146f600480 100644 --- a/tests/idris2/reg008/Vending.idr +++ b/tests/idris2/reg008/Vending.idr @@ -67,6 +67,15 @@ namespace MachineDo (a -> Inf (MachineIO state2)) -> MachineIO state1 (>>=) = Do + export + (>>) : {state1 : _} -> + MachineCmd a state1 state2 -> + Inf (MachineIO state2) -> + MachineIO state1 + ma >> mb = ma >>= const mb + + + data Fuel = Dry | More (Lazy Fuel) partial @@ -74,7 +83,7 @@ forever : Fuel forever = More forever ignore : IO a -> IO () -ignore x = do x; pure () +ignore mx = do x <- mx; pure () run : Fuel -> MachineIO mstate -> IO () run (More fuel) (Do c f) @@ -83,7 +92,7 @@ run (More fuel) (Do c f) run Dry p = pure () mutual - vend : {pounds : _} -> {chocs : _} -> MachineIO (pounds, chocs) + vend : {pounds, chocs : _} -> MachineIO (pounds, chocs) vend {pounds = (S p)} {chocs = (S c)} = do Vend Display "Enjoy!" machineLoop @@ -92,13 +101,13 @@ mutual vend {chocs = Z} = do Display "Out of stock" machineLoop - refill: {pounds : _} -> {chocs : _} -> (num : Nat) -> MachineIO (pounds, chocs) + refill: {pounds, chocs : _} -> (num : Nat) -> MachineIO (pounds, chocs) refill {pounds = Z} num = do Refill num machineLoop refill _ = do Display "Can't refill: Coins in machine" machineLoop - machineLoop : {pounds : _} -> {chocs : _} -> MachineIO (pounds, chocs) + machineLoop : {pounds, chocs : _} -> MachineIO (pounds, chocs) machineLoop = -- Do (Display "Foo") (\x => machineLoop) do Just x <- GetInput | Nothing => do Display "Invalid input" diff --git a/tests/node/node017/dir.idr b/tests/node/node017/dir.idr index 0e687c920c..9fb71c7d17 100644 --- a/tests/node/node017/dir.idr +++ b/tests/node/node017/dir.idr @@ -10,5 +10,5 @@ main = do Right () <- createDir "testdir" printLn ok ok <- changeDir "testdir" printLn ok - writeFile "test.txt" "hello\n" + ignore $ writeFile "test.txt" "hello\n" printLn !currentDir diff --git a/tests/node/node018/File.idr b/tests/node/node018/File.idr index ee17155065..f6b03c7888 100644 --- a/tests/node/node018/File.idr +++ b/tests/node/node018/File.idr @@ -5,7 +5,7 @@ main = do Right ok <- readFile "test.txt" | Left err => printLn err putStr ok - writeFile "testout.txt" "abc\ndef\n" + ignore $ writeFile "testout.txt" "abc\ndef\n" Right ok <- readFile "testout.txt" | Left err => printLn err putStr ok diff --git a/tests/racket/semaphores002/Main.idr b/tests/racket/semaphores002/Main.idr index 0028f420c7..94cd3aec95 100644 --- a/tests/racket/semaphores002/Main.idr +++ b/tests/racket/semaphores002/Main.idr @@ -5,7 +5,7 @@ import System.Concurrency main : IO () main = do sema <- makeSemaphore 0 - fork $ do + ignore $ fork $ do putStrLn "Hello" semaphorePost sema semaphorePost sema From 542749c8a4323282d37604af666f9ee14ed262c6 Mon Sep 17 00:00:00 2001 From: Guillaume ALLAIS Date: Sat, 20 Feb 2021 11:12:46 +0000 Subject: [PATCH 05/12] [ fix ] make (>>)'s second argument lazy --- libs/prelude/Prelude/Interfaces.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/libs/prelude/Prelude/Interfaces.idr b/libs/prelude/Prelude/Interfaces.idr index f518f58b7a..3a2c05b8f3 100644 --- a/libs/prelude/Prelude/Interfaces.idr +++ b/libs/prelude/Prelude/Interfaces.idr @@ -198,7 +198,7 @@ public export ||| Sequencing of effectful composition public export -(>>) : (Monad m) => m () -> m b -> m b +(>>) : Monad m => m () -> Lazy (m b) -> m b a >> b = a >>= \_ => b ||| Left-to-right Kleisli composition of monads. From 29b4cf3ba74b2e1bef1e77c8ea1527dd8861aec7 Mon Sep 17 00:00:00 2001 From: Guillaume ALLAIS Date: Sat, 20 Feb 2021 11:32:29 +0000 Subject: [PATCH 06/12] [ fix ] chapter11 --- tests/typedd-book/chapter11/ArithCmd.idr | 4 ++++ tests/typedd-book/chapter11/ArithCmdDo.idr | 10 ++++++++++ tests/typedd-book/chapter11/ArithTotal.idr | 5 +++++ tests/typedd-book/chapter11/Greet.idr | 4 ++++ tests/typedd-book/chapter11/InfIO.idr | 5 +++++ tests/typedd-book/chapter11/RunIO.idr | 8 ++++++-- 6 files changed, 34 insertions(+), 2 deletions(-) diff --git a/tests/typedd-book/chapter11/ArithCmd.idr b/tests/typedd-book/chapter11/ArithCmd.idr index 6de57a200b..f7f3ee7c2f 100644 --- a/tests/typedd-book/chapter11/ArithCmd.idr +++ b/tests/typedd-book/chapter11/ArithCmd.idr @@ -15,6 +15,10 @@ data ConsoleIO : Type -> Type where (>>=) : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b (>>=) = Do +%tcinline +(>>) : Command () -> Inf (ConsoleIO b) -> ConsoleIO b +ma >> mb = Do ma (\ _ => mb) + data Fuel = Dry | More (Lazy Fuel) runCommand : Command a -> IO a diff --git a/tests/typedd-book/chapter11/ArithCmdDo.idr b/tests/typedd-book/chapter11/ArithCmdDo.idr index 7ce3725a3b..99bde7c552 100644 --- a/tests/typedd-book/chapter11/ArithCmdDo.idr +++ b/tests/typedd-book/chapter11/ArithCmdDo.idr @@ -16,17 +16,26 @@ export data ConsoleIO : Type -> Type where Quit : a -> ConsoleIO a Do : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b + Seq : Command () -> Inf (ConsoleIO a) -> ConsoleIO a namespace CommandDo export (>>=) : Command a -> (a -> Command b) -> Command b (>>=) = Bind + export + (>>) : Command () -> Command b -> Command b + ma >> mb = Bind ma (\ _ => mb) + namespace ConsoleDo export (>>=) : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b (>>=) = Do + export + (>>) : Command () -> Inf (ConsoleIO b) -> ConsoleIO b + (>>) = Seq + data Fuel = Dry | More (Lazy Fuel) runCommand : Command a -> IO a @@ -40,6 +49,7 @@ run : Fuel -> ConsoleIO a -> IO (Maybe a) run fuel (Quit val) = do pure (Just val) run (More fuel) (Do c f) = do res <- runCommand c run fuel (f res) +run (More fuel) (Seq c d) = do runCommand c; run fuel d run Dry p = pure Nothing randoms : Int -> Stream Int diff --git a/tests/typedd-book/chapter11/ArithTotal.idr b/tests/typedd-book/chapter11/ArithTotal.idr index 3c26ebfacf..9c9febd53d 100644 --- a/tests/typedd-book/chapter11/ArithTotal.idr +++ b/tests/typedd-book/chapter11/ArithTotal.idr @@ -5,15 +5,20 @@ import System data InfIO : Type where Do : IO a -> (a -> Inf InfIO) -> InfIO + Seq : IO () -> Inf InfIO -> InfIO (>>=) : IO a -> (a -> Inf InfIO) -> InfIO (>>=) = Do +(>>) : IO () -> Inf InfIO -> InfIO +(>>) = Seq + data Fuel = Dry | More (Lazy Fuel) run : Fuel -> InfIO -> IO () run (More fuel) (Do c f) = do res <- c run fuel (f res) +run (More fuel) (Seq c d) = do c; run fuel d run Dry p = putStrLn "Out of fuel" randoms : Int -> Stream Int diff --git a/tests/typedd-book/chapter11/Greet.idr b/tests/typedd-book/chapter11/Greet.idr index 2dc31ab648..b09bc1038e 100644 --- a/tests/typedd-book/chapter11/Greet.idr +++ b/tests/typedd-book/chapter11/Greet.idr @@ -2,10 +2,14 @@ data InfIO : Type where Do : IO a -> (a -> Inf InfIO) -> InfIO + Seq : IO () -> Inf InfIO -> InfIO (>>=) : IO a -> (a -> Inf InfIO) -> InfIO (>>=) = Do +(>>) : IO () -> Inf InfIO -> InfIO +(>>) = Seq + greet : InfIO greet = do putStr "Enter your name: " name <- getLine diff --git a/tests/typedd-book/chapter11/InfIO.idr b/tests/typedd-book/chapter11/InfIO.idr index 8a02a5c296..e9df134d15 100644 --- a/tests/typedd-book/chapter11/InfIO.idr +++ b/tests/typedd-book/chapter11/InfIO.idr @@ -2,10 +2,14 @@ data InfIO : Type where Do : IO a -> (a -> Inf InfIO) -> InfIO + Seq : IO () -> Inf InfIO -> InfIO (>>=) : IO a -> (a -> Inf InfIO) -> InfIO (>>=) = Do +(>>) : IO () -> Inf InfIO -> InfIO +(>>) = Seq + loopPrint : String -> InfIO loopPrint msg = do putStrLn msg loopPrint msg @@ -24,6 +28,7 @@ runPartial (Do action f) = do res <- action run : Fuel -> InfIO -> IO () run (More fuel) (Do c f) = do res <- c run fuel (f res) +run (More fuel) (Seq io k) = do io; run fuel k run Dry p = putStrLn "Out of fuel" partial diff --git a/tests/typedd-book/chapter11/RunIO.idr b/tests/typedd-book/chapter11/RunIO.idr index 70c45db32e..775c776001 100644 --- a/tests/typedd-book/chapter11/RunIO.idr +++ b/tests/typedd-book/chapter11/RunIO.idr @@ -3,10 +3,14 @@ data RunIO : Type -> Type where Quit : a -> RunIO a Do : IO a -> (a -> Inf (RunIO b)) -> RunIO b + Seq : IO () -> Inf (RunIO b) -> RunIO b (>>=) : IO a -> (a -> Inf (RunIO b)) -> RunIO b (>>=) = Do +(>>) : IO () -> Inf (RunIO b) -> RunIO b +(>>) = Seq + greet : RunIO () greet = do putStr "Enter your name: " name <- getLine @@ -22,6 +26,7 @@ run : Fuel -> RunIO a -> IO (Maybe a) run fuel (Quit val) = do pure (Just val) run (More fuel) (Do c f) = do res <- c run fuel (f res) +run (More fuel) (Seq io k) = do io; run fuel k run Dry p = pure Nothing partial @@ -30,5 +35,4 @@ forever = More forever partial main : IO () -main = do run forever greet - pure () +main = ignore $ run forever greet From 258cc92dccfdd9a04eb7396f02c4c853a96347ad Mon Sep 17 00:00:00 2001 From: Guillaume ALLAIS Date: Sat, 20 Feb 2021 11:43:12 +0000 Subject: [PATCH 07/12] [ fix ] bring `commit` back The silent expansion of ```idris do p q ``` to ``` p >>= \ _ => q ``` acted like a pattern-synonym when building these grammars and thus did not get in the way of termination / productivity checking. When we introduce (>>), it breaks this convenient feature and to recover it we need to introduce new constructors. It's unfortunate but not too much trouble. --- libs/contrib/Language/JSON/Parser.idr | 16 ++++---- libs/contrib/Text/Parser/Core.idr | 55 ++++++++++++++++++++++++--- src/Libraries/Text/Parser/Core.idr | 46 +++++++++++++++++++--- 3 files changed, 98 insertions(+), 19 deletions(-) diff --git a/libs/contrib/Language/JSON/Parser.idr b/libs/contrib/Language/JSON/Parser.idr index a34c1ad993..d84f36337a 100644 --- a/libs/contrib/Language/JSON/Parser.idr +++ b/libs/contrib/Language/JSON/Parser.idr @@ -34,10 +34,10 @@ mutual private object : Grammar JSONToken True JSON object = do punct $ Curly Open - mustWork $ do - props <- properties - punct $ Curly Close - pure $ JObject props + commit + props <- properties + punct $ Curly Close + pure $ JObject props where properties : Grammar JSONToken False (List (String, JSON)) properties = sepBy (punct Comma) $ @@ -49,10 +49,10 @@ mutual private array : Grammar JSONToken True JSON array = do punct (Square Open) - mustWork $ do - vals <- values - punct (Square Close) - pure (JArray vals) + commit + vals <- values + punct (Square Close) + pure (JArray vals) where values : Grammar JSONToken False (List JSON) values = sepBy (punct Comma) json diff --git a/libs/contrib/Text/Parser/Core.idr b/libs/contrib/Text/Parser/Core.idr index 71a71b2f43..a7b3190785 100644 --- a/libs/contrib/Text/Parser/Core.idr +++ b/libs/contrib/Text/Parser/Core.idr @@ -22,6 +22,12 @@ data Grammar : (tok : Type) -> (consumes : Bool) -> Type -> Type where Grammar tok True b SeqEmpty : {c1, c2 : _} -> Grammar tok c1 a -> (a -> Grammar tok c2 b) -> Grammar tok (c1 || c2) b + + ThenEat : {c2 : _} -> Grammar tok True () -> Inf (Grammar tok c2 b) -> + Grammar tok True b + ThenEmpty : {c1, c2 : _} -> Grammar tok c1 () -> Grammar tok c2 b -> + Grammar tok (c1 || c2) b + Alt : {c1, c2 : _} -> Grammar tok c1 ty -> Grammar tok c2 ty -> Grammar tok (c1 && c2) ty @@ -46,8 +52,8 @@ public export %inline %tcinline Grammar tok c1 () -> inf c1 (Grammar tok c2 a) -> Grammar tok (c1 || c2) a -(>>) {c1 = False} ma mb = SeqEmpty ma (const mb) -(>>) {c1 = True} ma mb = SeqEat ma (Delay \ a => mb) +(>>) {c1 = False} = ThenEmpty +(>>) {c1 = True} = ThenEat ||| Sequence two grammars. If either consumes some input, the sequence is ||| guaranteed to consume input. This is an explicitly non-infinite version @@ -87,6 +93,10 @@ export = SeqEat act (\val => map f (next val)) map f (SeqEmpty act next) = SeqEmpty act (\val => map f (next val)) + map f (ThenEat act next) + = ThenEat act (map f next) + map f (ThenEmpty act next) + = ThenEmpty act (map f next) -- The remaining constructors (NextIs, EOF, Commit) have a fixed type, -- so a sequence must be used. map {c = False} f p = SeqEmpty p (Empty . f) @@ -132,8 +142,14 @@ mapToken f EOF = EOF mapToken f (Fail fatal msg) = Fail fatal msg mapToken f (MustWork g) = MustWork (mapToken f g) mapToken f Commit = Commit -mapToken f (SeqEat act next) = SeqEat (mapToken f act) (\x => mapToken f (next x)) -mapToken f (SeqEmpty act next) = SeqEmpty (mapToken f act) (\x => mapToken f (next x)) +mapToken f (SeqEat act next) + = SeqEat (mapToken f act) (\x => mapToken f (next x)) +mapToken f (SeqEmpty act next) + = SeqEmpty (mapToken f act) (\x => mapToken f (next x)) +mapToken f (ThenEat act next) + = ThenEat (mapToken f act) (mapToken f next) +mapToken f (ThenEmpty act next) + = ThenEmpty (mapToken f act) (mapToken f next) mapToken f (Alt x y) = Alt (mapToken f x) (mapToken f y) ||| Always succeed with the given value. @@ -198,7 +214,7 @@ data ParseResult : List tok -> (consumes : Bool) -> Type -> Type where -- flag to take both alternatives into account weakenRes : {whatever, c : Bool} -> {xs : List tok} -> (com' : Bool) -> - ParseResult xs c ty -> ParseResult xs (whatever && c) ty + ParseResult xs c ty -> ParseResult xs (whatever && c) ty weakenRes com' (Failure com fatal msg ts) = Failure com' fatal msg ts weakenRes {whatever=True} com' (EmptyRes com val xs) = EmptyRes com' val xs weakenRes {whatever=False} com' (EmptyRes com val xs) = EmptyRes com' val xs @@ -272,6 +288,35 @@ doParse com (SeqEat act next) xs with (doParse com act xs) NonEmptyRes {x=x1} {xs=xs1} com' val more' => rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in NonEmptyRes {xs = ys ++ (x1 :: xs1)} com' val more' +doParse com (ThenEmpty {c1} {c2} act next) xs + = let p' = assert_total (doParse {c = c1} com act xs) in + case p' of + Failure com fatal msg ts => Failure com fatal msg ts + EmptyRes com val xs => + case assert_total (doParse com next xs) of + Failure com' fatal msg ts => Failure com' fatal msg ts + EmptyRes com' val xs => EmptyRes com' val xs + NonEmptyRes {xs=xs'} com' val more => + NonEmptyRes {xs=xs'} com' val more + NonEmptyRes {x} {xs=ys} com val more => + case (assert_total (doParse com next more)) of + Failure com' fatal msg ts => Failure com' fatal msg ts + EmptyRes com' val _ => NonEmptyRes {xs=ys} com' val more + NonEmptyRes {x=x1} {xs=xs1} com' val more' => + rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in + NonEmptyRes {xs = ys ++ (x1 :: xs1)} com' val more' +doParse com (ThenEat act next) xs with (doParse com act xs) + doParse com (ThenEat act next) xs | Failure com' fatal msg ts + = Failure com' fatal msg ts + doParse com (ThenEat act next) (x :: (ys ++ more)) | (NonEmptyRes {xs=ys} com' val more) + = let p' = assert_total (doParse com' next more) in + case p' of + Failure com' fatal msg ts => Failure com' fatal msg ts + EmptyRes com' val _ => NonEmptyRes {xs=ys} com' val more + NonEmptyRes {x=x1} {xs=xs1} com' val more' => + rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in + NonEmptyRes {xs = ys ++ (x1 :: xs1)} com' val more' + -- This next line is not strictly necessary, but it stops the coverage -- checker taking a really long time and eating lots of memory... -- doParse _ _ _ = Failure True True "Help the coverage checker!" [] diff --git a/src/Libraries/Text/Parser/Core.idr b/src/Libraries/Text/Parser/Core.idr index cf0fdf7123..4fd32b660b 100644 --- a/src/Libraries/Text/Parser/Core.idr +++ b/src/Libraries/Text/Parser/Core.idr @@ -34,6 +34,14 @@ data Grammar : (tok : Type) -> (consumes : Bool) -> Type -> Type where SeqEmpty : {c1, c2 : Bool} -> Grammar tok c1 a -> (a -> Grammar tok c2 b) -> Grammar tok (c1 || c2) b + + ThenEat : {c2 : Bool} -> + Grammar tok True () -> Inf (Grammar tok c2 a) -> + Grammar tok True a + ThenEmpty : {c1, c2 : Bool} -> + Grammar tok c1 () -> Grammar tok c2 a -> + Grammar tok (c1 || c2) a + Alt : {c1, c2 : Bool} -> Grammar tok c1 ty -> Lazy (Grammar tok c2 ty) -> Grammar tok (c1 && c2) ty @@ -60,8 +68,8 @@ public export %inline %tcinline Grammar tok c1 () -> inf c1 (Grammar tok c2 a) -> Grammar tok (c1 || c2) a -(>>) {c1 = False} ma mb = SeqEmpty ma (const mb) -(>>) {c1 = True} ma mb = SeqEat ma (Delay \ a => mb) +(>>) {c1 = False} = ThenEmpty +(>>) {c1 = True} = ThenEat ||| Sequence two grammars. If either consumes some input, the sequence is ||| guaranteed to consume input. This is an explicitly non-infinite version @@ -94,8 +102,14 @@ Functor (Grammar tok c) where map f (SeqEat act next) = SeqEat act (\val => map f (next val)) map f (SeqEmpty act next) - = SeqEmpty act (\val => map f (next val)) - map {c} f (Bounds act) = rewrite sym $ orFalseNeutral c in SeqEmpty (Bounds act) (Empty . f) -- Bounds (map f act) + = SeqEmpty act (\ val => map f (next val)) + map f (ThenEat act next) + = ThenEat act (map f next) + map f (ThenEmpty act next) + = ThenEmpty act (map f next) + map {c} f (Bounds act) + = rewrite sym $ orFalseNeutral c in + SeqEmpty (Bounds act) (Empty . f) -- Bounds (map f act) -- The remaining constructors (NextIs, EOF, Commit) have a fixed type, -- so a sequence must be used. map {c = False} f p = SeqEmpty p (Empty . f) @@ -160,8 +174,14 @@ mapToken f (Fail fatal msg) = Fail fatal msg mapToken f (Try g) = Try (mapToken f g) mapToken f (MustWork g) = MustWork (mapToken f g) mapToken f Commit = Commit -mapToken f (SeqEat act next) = SeqEat (mapToken f act) (\x => mapToken f (next x)) -mapToken f (SeqEmpty act next) = SeqEmpty (mapToken f act) (\x => mapToken f (next x)) +mapToken f (SeqEat act next) + = SeqEat (mapToken f act) (\x => mapToken f (next x)) +mapToken f (SeqEmpty act next) + = SeqEmpty (mapToken f act) (\x => mapToken f (next x)) +mapToken f (ThenEat act next) + = ThenEat (mapToken f act) (mapToken f next) +mapToken f (ThenEmpty act next) + = ThenEmpty (mapToken f act) (mapToken f next) mapToken f (Alt x y) = Alt (mapToken f x) (mapToken f y) mapToken f (Bounds act) = Bounds (mapToken f act) @@ -278,6 +298,20 @@ mutual case assert_total (doParse com (next v.val) xs) of Failure com' fatal msg ts => Failure com' fatal msg ts Res com' v' xs => Res com' (mergeBounds v v') xs + doParse com (ThenEmpty act next) xs + = case assert_total (doParse com act xs) of + Failure com fatal msg ts => Failure com fatal msg ts + Res com v xs => + case assert_total (doParse com next xs) of + Failure com' fatal msg ts => Failure com' fatal msg ts + Res com' v' xs => Res com' (mergeBounds v v') xs + doParse com (ThenEat act next) xs + = case assert_total (doParse com act xs) of + Failure com fatal msg ts => Failure com fatal msg ts + Res com v xs => + case assert_total (doParse com next xs) of + Failure com' fatal msg ts => Failure com' fatal msg ts + Res com' v' xs => Res com' (mergeBounds v v') xs doParse com (Bounds act) xs = case assert_total (doParse com act xs) of Failure com fatal msg ts => Failure com fatal msg ts From e094fcd9d122cff060895b7426361a27c6256e83 Mon Sep 17 00:00:00 2001 From: Guillaume ALLAIS Date: Sat, 20 Feb 2021 11:54:56 +0000 Subject: [PATCH 08/12] [ fix ] chapter 12 --- tests/typedd-book/chapter12/ArithState.idr | 12 ++++++++++++ tests/typedd-book/chapter12/Traverse.idr | 3 +-- 2 files changed, 13 insertions(+), 2 deletions(-) diff --git a/tests/typedd-book/chapter12/ArithState.idr b/tests/typedd-book/chapter12/ArithState.idr index a01325037e..2ec42acf8e 100644 --- a/tests/typedd-book/chapter12/ArithState.idr +++ b/tests/typedd-book/chapter12/ArithState.idr @@ -48,17 +48,26 @@ export data ConsoleIO : Type -> Type where Quit : a -> ConsoleIO a Do : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b + Seq : Command () -> Inf (ConsoleIO a) -> ConsoleIO a namespace ConsoleDo export (>>=) : Command a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b (>>=) = Do + export + (>>) : Command () -> Inf (ConsoleIO a) -> ConsoleIO a + (>>) = Seq + namespace CommandDo export (>>=) : Command a -> (a -> Command b) -> Command b (>>=) = Bind + export + (>>) : Command () -> Command b -> Command b + ma >> mb = ma >>= \ () => mb + randoms : Int -> Stream Int randoms seed = let seed' = 1664525 * seed + 1013904223 in (seed' `shiftR` 2) :: randoms seed' @@ -99,6 +108,9 @@ run fuel rnds state (Quit val) = do pure (Just val, rnds, state) run (More fuel) rnds state (Do c f) = do (res, newRnds, newState) <- runCommand rnds state c run fuel newRnds newState (f res) +run (More fuel) rnds state (Seq c f) + = do ((), newRnds, newState) <- runCommand rnds state c + run fuel newRnds newState f run Dry rnds state p = pure (Nothing, rnds, state) mutual diff --git a/tests/typedd-book/chapter12/Traverse.idr b/tests/typedd-book/chapter12/Traverse.idr index 91cf0415b3..2da4b30f00 100644 --- a/tests/typedd-book/chapter12/Traverse.idr +++ b/tests/typedd-book/chapter12/Traverse.idr @@ -5,6 +5,5 @@ main : IO () main = do putStr "Display Crew? " x <- getLine when (x == "yes") $ - do traverse putStrLn crew - pure () + do traverse_ putStrLn crew putStrLn "Done" From 19c51ca6fd20d1741c30151c0f525d56ace89134 Mon Sep 17 00:00:00 2001 From: Guillaume ALLAIS Date: Sat, 20 Feb 2021 12:01:16 +0000 Subject: [PATCH 09/12] [ fix ] chapter 13 --- tests/typedd-book/chapter13/Door.idr | 5 +++++ tests/typedd-book/chapter13/Stack.idr | 5 +++++ tests/typedd-book/chapter13/StackIO.idr | 15 +++++++++++++++ tests/typedd-book/chapter13/Vending.idr | 10 ++++++++++ 4 files changed, 35 insertions(+) diff --git a/tests/typedd-book/chapter13/Door.idr b/tests/typedd-book/chapter13/Door.idr index 507acb1fc4..2dbf9a3472 100644 --- a/tests/typedd-book/chapter13/Door.idr +++ b/tests/typedd-book/chapter13/Door.idr @@ -12,6 +12,11 @@ data DoorCmd : Type -> (a -> DoorCmd b state2 state3) -> DoorCmd b state1 state3 +(>>) : DoorCmd () state1 state2 -> + Lazy (DoorCmd a state2 state3) -> + DoorCmd a state1 state3 +ma >> mb = ma >>= \ _ => mb + doorProg : DoorCmd () DoorClosed DoorClosed doorProg = do RingBell Open diff --git a/tests/typedd-book/chapter13/Stack.idr b/tests/typedd-book/chapter13/Stack.idr index 7289d7f417..5665cbdf31 100644 --- a/tests/typedd-book/chapter13/Stack.idr +++ b/tests/typedd-book/chapter13/Stack.idr @@ -10,6 +10,11 @@ data StackCmd : Type -> Nat -> Nat -> Type where (a -> StackCmd b height2 height3) -> StackCmd b height1 height3 +(>>) : StackCmd () height1 height2 -> + Lazy (StackCmd a height2 height3) -> + StackCmd a height1 height3 +ma >> mb = ma >>= \ () => mb + runStack : (stk : Vect inHeight Integer) -> StackCmd ty inHeight outHeight -> (ty, Vect outHeight Integer) diff --git a/tests/typedd-book/chapter13/StackIO.idr b/tests/typedd-book/chapter13/StackIO.idr index fc6095ebfc..3b13833205 100644 --- a/tests/typedd-book/chapter13/StackIO.idr +++ b/tests/typedd-book/chapter13/StackIO.idr @@ -14,6 +14,11 @@ data StackCmd : Type -> Nat -> Nat -> Type where (a -> StackCmd b height2 height3) -> StackCmd b height1 height3 +(>>) : StackCmd () height1 height2 -> + Lazy (StackCmd a height2 height3) -> + StackCmd a height1 height3 +ma >> mb = ma >>= \ () => mb + runStack : (stk : Vect inHeight Integer) -> StackCmd ty inHeight outHeight -> IO (ty, Vect outHeight Integer) @@ -40,6 +45,8 @@ export data StackIO : Nat -> Type where Do : StackCmd a height1 height2 -> (a -> Inf (StackIO height2)) -> StackIO height1 + Seq : StackCmd () height1 height2 -> + Inf (StackIO height2) -> StackIO height1 namespace StackDo export @@ -47,6 +54,11 @@ namespace StackDo (a -> Inf (StackIO height2)) -> StackIO height1 (>>=) = Do + export + (>>) : StackCmd () height1 height2 -> + Inf (StackIO height2) -> StackIO height1 + (>>) = Seq + data Fuel = Dry | More (Lazy Fuel) partial @@ -57,6 +69,9 @@ run : Fuel -> Vect height Integer -> StackIO height -> IO () run Dry _ _ = pure () run (More fuel) stk (Do c f) = do (res, newStk) <- runStack stk c run fuel newStk (f res) +run (More fuel) stk (Seq c k) + = do ((), newStk) <- runStack stk c + run fuel newStk k doAdd : StackCmd () (S (S height)) (S height) doAdd = do val1 <- Pop diff --git a/tests/typedd-book/chapter13/Vending.idr b/tests/typedd-book/chapter13/Vending.idr index e8e704f63e..92d3771b02 100644 --- a/tests/typedd-book/chapter13/Vending.idr +++ b/tests/typedd-book/chapter13/Vending.idr @@ -41,6 +41,9 @@ data MachineIO : VendState -> Type where Do : {state1 : _} -> MachineCmd a state1 state2 -> (a -> Inf (MachineIO state2)) -> MachineIO state1 + Seq : {state1 : _} -> + MachineCmd () state1 state2 -> + Inf (MachineIO state2) -> MachineIO state1 runMachine : {inState : _} -> MachineCmd ty inState outState -> IO ty runMachine InsertCoin = putStrLn "Coin inserted" @@ -66,6 +69,12 @@ namespace MachineDo (a -> Inf (MachineIO state2)) -> MachineIO state1 (>>=) = Do + export + (>>) : {state1 : _} -> + MachineCmd () state1 state2 -> + Inf (MachineIO state2) -> MachineIO state1 + (>>) = Seq + data Fuel = Dry | More (Lazy Fuel) partial @@ -76,6 +85,7 @@ run : Fuel -> MachineIO state -> IO () run (More fuel) (Do c f) = do res <- runMachine c run fuel (f res) +run (More fuel) (Seq c d) = do runMachine c; run fuel d run Dry p = pure () mutual From 595668444f6978c53f8d0e4f3d8c4af9223b49ac Mon Sep 17 00:00:00 2001 From: Guillaume ALLAIS Date: Sat, 20 Feb 2021 12:07:34 +0000 Subject: [PATCH 10/12] [ fix ] chapter 14 --- tests/typedd-book/chapter14/ATM.idr | 5 +++++ tests/typedd-book/chapter14/DoorJam.idr | 5 +++++ tests/typedd-book/chapter14/Hangman.idr | 22 +++++++++++++++++----- 3 files changed, 27 insertions(+), 5 deletions(-) diff --git a/tests/typedd-book/chapter14/ATM.idr b/tests/typedd-book/chapter14/ATM.idr index 30f06bcafe..14776fe6ef 100644 --- a/tests/typedd-book/chapter14/ATM.idr +++ b/tests/typedd-book/chapter14/ATM.idr @@ -31,6 +31,11 @@ data ATMCmd : (ty : Type) -> ATMState -> (ty -> ATMState) -> Type where ((res : a) -> ATMCmd b (state2_fn res) state3_fn) -> ATMCmd b state1 state3_fn +(>>) : ATMCmd () state1 state2_fn -> + Lazy (ATMCmd a (state2_fn ()) state3_fn) -> + ATMCmd a state1 state3_fn +ma >> mb = ma >>= \ () => mb + readVect : (n : Nat) -> IO (Vect n Char) readVect Z = do discard <- getLine -- rest of input up to enter pure [] diff --git a/tests/typedd-book/chapter14/DoorJam.idr b/tests/typedd-book/chapter14/DoorJam.idr index 693a049b88..2e01248275 100644 --- a/tests/typedd-book/chapter14/DoorJam.idr +++ b/tests/typedd-book/chapter14/DoorJam.idr @@ -19,6 +19,11 @@ data DoorCmd : (ty : Type) -> ((res: a) -> DoorCmd b (state2_fn res) state3_fn) -> DoorCmd b state1 state3_fn +(>>) : DoorCmd () state1 state2_fn -> + Lazy (DoorCmd a (state2_fn ()) state3_fn) -> + DoorCmd a state1 state3_fn +ma >> mb = ma >>= \ () => mb + logOpen : DoorCmd DoorResult DoorClosed (\res => case res of OK => DoorOpen diff --git a/tests/typedd-book/chapter14/Hangman.idr b/tests/typedd-book/chapter14/Hangman.idr index 7359695f3c..82e6274315 100644 --- a/tests/typedd-book/chapter14/Hangman.idr +++ b/tests/typedd-book/chapter14/Hangman.idr @@ -41,12 +41,20 @@ data GameCmd : (ty : Type) -> GameState -> (ty -> GameState) -> Type where ((res : a) -> GameCmd b (state2_fn res) state3_fn) -> GameCmd b state1 state3_fn +(>>) : GameCmd () state1 state2_fn -> + Lazy (GameCmd a (state2_fn ()) state3_fn) -> + GameCmd a state1 state3_fn +ma >> mb = ma >>= \ () => mb + namespace Loop public export data GameLoop : (ty : Type) -> GameState -> (ty -> GameState) -> Type where (>>=) : GameCmd a state1 state2_fn -> ((res : a) -> Inf (GameLoop b (state2_fn res) state3_fn)) -> GameLoop b state1 state3_fn + (>>) : GameCmd () state1 state2_fn -> + Inf (GameLoop a (state2_fn ()) state3_fn) -> + GameLoop a state1 state3_fn Exit : GameLoop () NotRunning (const NotRunning) gameLoop : {letters : _} -> {guesses : _} -> @@ -132,9 +140,14 @@ runCmd Dry _ _ = pure OutOfFuel run : Fuel -> Game inState -> GameLoop ty inState outState_fn -> IO (GameResult ty outState_fn) run Dry _ _ = pure OutOfFuel run (More fuel) st Exit = ok () st -run (More fuel) st (cmd >>= next) = do OK cmdRes newSt <- runCmd fuel st cmd - | OutOfFuel => pure OutOfFuel - run fuel newSt (next cmdRes) +run (More fuel) st (cmd >>= next) + = do OK cmdRes newSt <- runCmd fuel st cmd + | OutOfFuel => pure OutOfFuel + run fuel newSt (next cmdRes) +run (More fuel) st (cmd >> next) + = do OK () newSt <- runCmd fuel st cmd + | OutOfFuel => pure OutOfFuel + run fuel newSt next partial forever : Fuel @@ -142,5 +155,4 @@ forever = More forever partial main : IO () -main = do run forever GameStart hangman - pure () +main = do ignore $ run forever GameStart hangman From a5c10163df291daf487973444b47b62740b7a407 Mon Sep 17 00:00:00 2001 From: Guillaume ALLAIS Date: Sat, 20 Feb 2021 12:15:12 +0000 Subject: [PATCH 11/12] [ fix ] hopefully the test suite is fine now --- tests/idris2/with003/Main.idr | 4 +-- tests/idris2/with003/expected | 47 ++++++----------------------------- tests/idris2/with003/input | 2 +- 3 files changed, 11 insertions(+), 42 deletions(-) diff --git a/tests/idris2/with003/Main.idr b/tests/idris2/with003/Main.idr index 677990504a..8bf30d0765 100644 --- a/tests/idris2/with003/Main.idr +++ b/tests/idris2/with003/Main.idr @@ -10,5 +10,5 @@ myPrintLn = printLn -- add some definition of (>>=) in another namespace namespace Other public export - (>>=) : IO a -> IO b -> IO b - (>>=) f x = f *> x + (>>) : IO () -> IO b -> IO b + (>>) f x = f *> x diff --git a/tests/idris2/with003/expected b/tests/idris2/with003/expected index 7b10e70677..525110f8e6 100644 --- a/tests/idris2/with003/expected +++ b/tests/idris2/with003/expected @@ -1,48 +1,17 @@ 1/1: Building Main (Main.idr) -Main> Error: Sorry, I can't find any elaboration which works. All errors: -If Prelude.>>=: Sorry, I can't find any elaboration which works. All errors: -If Prelude.>>=: When unifying ?_ -> IO () and IO ?b. -Mismatch between: ?_ -> IO () and IO ?b. - -(interactive):1:66--1:81 - 1 | do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo" - ^^^^^^^^^^^^^^^ - -If Main.Other.>>=: When unifying ?_ -> IO () and IO ?b. -Mismatch between: ?_ -> IO () and IO ?b. - -(interactive):1:38--1:64 - 1 | do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo" - ^^^^^^^^^^^^^^^^^^^^^^^^^^ - -If Main.Other.>>=: Sorry, I can't find any elaboration which works. All errors: -If Prelude.>>=: When unifying ?_ -> IO () and IO ?b. -Mismatch between: ?_ -> IO () and IO ?b. - -(interactive):1:38--1:64 - 1 | do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo" - ^^^^^^^^^^^^^^^^^^^^^^^^^^ - -If Main.Other.>>=: Sorry, I can't find any elaboration which works. All errors: -If Prelude.>>=: When unifying ?_ -> IO () and IO ?b. -Mismatch between: ?_ -> IO () and IO ?b. - -(interactive):1:66--1:81 - 1 | do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo" - ^^^^^^^^^^^^^^^ - -If Main.Other.>>=: When unifying ?_ -> IO () and IO ?b. -Mismatch between: ?_ -> IO () and IO ?b. +Main> Error: Ambiguous elaboration. Possible results: + Main.myPrintLn "foo" Prelude.>> ?arg + Main.myPrintLn "foo" Main.Other.>> ?arg -(interactive):1:38--1:64 +(interactive):1:4--1:19 1 | do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo" - ^^^^^^^^^^^^^^^^^^^^^^^^^^ + ^^^^^^^^^^^^^^^ Main> Error: Can't find an implementation for Num (). -(interactive):1:61--1:65 - 1 | with Prelude.(>>=) do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo" - ^^^^ +(interactive):1:60--1:64 + 1 | with Prelude.(>>) do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo" + ^^^^ Main> Error: Ambiguous elaboration. Possible results: Prelude.Nil diff --git a/tests/idris2/with003/input b/tests/idris2/with003/input index c77625533f..1b1e3299ab 100644 --- a/tests/idris2/with003/input +++ b/tests/idris2/with003/input @@ -1,5 +1,5 @@ do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo" -with Prelude.(>>=) do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo" +with Prelude.(>>) do myPrintLn "foo"; myPrintLn "boo"; map (+1) (myPrintLn "woo"); myPrintLn "goo"; myPrintLn "foo" :t [] :t with Vect.Nil [] :t with Prelude.Nil [] From 7d2fca140d1643c458c14886d295d50d6a8248de Mon Sep 17 00:00:00 2001 From: Guillaume ALLAIS Date: Sat, 20 Feb 2021 12:34:39 +0000 Subject: [PATCH 12/12] [ refactor ] eta-contract --- libs/contrib/Text/Parser/Core.idr | 14 ++------------ 1 file changed, 2 insertions(+), 12 deletions(-) diff --git a/libs/contrib/Text/Parser/Core.idr b/libs/contrib/Text/Parser/Core.idr index a7b3190785..271ae8d517 100644 --- a/libs/contrib/Text/Parser/Core.idr +++ b/libs/contrib/Text/Parser/Core.idr @@ -264,12 +264,7 @@ doParse com (SeqEmpty {c1} {c2} act next) xs = let p' = assert_total (doParse {c = c1} com act xs) in case p' of Failure com fatal msg ts => Failure com fatal msg ts - EmptyRes com val xs => - case assert_total (doParse com (next val) xs) of - Failure com' fatal msg ts => Failure com' fatal msg ts - EmptyRes com' val xs => EmptyRes com' val xs - NonEmptyRes {xs=xs'} com' val more => - NonEmptyRes {xs=xs'} com' val more + EmptyRes com val xs => assert_total (doParse com (next val) xs) NonEmptyRes {x} {xs=ys} com val more => case (assert_total (doParse com (next val) more)) of Failure com' fatal msg ts => Failure com' fatal msg ts @@ -292,12 +287,7 @@ doParse com (ThenEmpty {c1} {c2} act next) xs = let p' = assert_total (doParse {c = c1} com act xs) in case p' of Failure com fatal msg ts => Failure com fatal msg ts - EmptyRes com val xs => - case assert_total (doParse com next xs) of - Failure com' fatal msg ts => Failure com' fatal msg ts - EmptyRes com' val xs => EmptyRes com' val xs - NonEmptyRes {xs=xs'} com' val more => - NonEmptyRes {xs=xs'} com' val more + EmptyRes com val xs => assert_total (doParse com next xs) NonEmptyRes {x} {xs=ys} com val more => case (assert_total (doParse com next more)) of Failure com' fatal msg ts => Failure com' fatal msg ts