[ 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/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

@@ -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
 
@@ -37,6 +43,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} = 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
 ||| of `>>=`.
@@ -75,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)
@@ -120,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.
@@ -186,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
@@ -236,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
@@ -260,6 +283,30 @@ 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 => 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
+                          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!" []

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 () -> Lazy (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