[ fix #758 ] desugar non-binding sequencing in do blocks to (>>)

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)

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)

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

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

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

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

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
 

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,

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 `>>=`.

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.

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

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"

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

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.

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

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 <idris_support.h> // 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