[ fix #1859 ] Undo my mistakes (#1866)

Author: gallais

libs/contrib/System/Console/GetOpt.idr

@@ -237,7 +237,7 @@ getOpt :  ArgOrder a                         -- non-option handling
 getOpt _        _        []         =  emptyRes
 getOpt ordering descs (arg::args)   =
   let (opt,rest) = getNext (unpack arg) args descs
-      res        = getOpt ordering descs rest
+      res        = getOpt ordering descs (assert_smaller args rest)
    in case (opt,ordering) of
            (Opt x, _)                   => {options $= (x::)} res
            (UnreqOpt x, _)              => {unrecognized $= (x::)} res

libs/contrib/Text/Lexer/Tokenizer.idr

@@ -121,7 +121,7 @@ tokenise reject tokenizer line col acc str
               end = endFn tag
               beginTok'' = MkBounded (mapBegin beginTok') False (MkBounds line col line' col')
               (midToks, (reason, line'', col'', rest'')) =
-                    tokenise end middle line' col' [] rest
+                    assert_total (tokenise end middle line' col' [] rest)
            in case reason of
                    (ComposeNotClosing _ _) => Left reason
                    _ => let Just (endTok', lineEnd, colEnd, restEnd) =

libs/contrib/Text/PrettyPrint/Prettyprinter/SimpleDocTree.idr

@@ -70,10 +70,10 @@ sdocToTreeParser (SLine i rest) = case sdocToTreeParser rest of
 sdocToTreeParser (SAnnPush ann rest) = case sdocToTreeParser rest of
   (tree, Nothing) => (Nothing, Nothing)
   (Just tree, Nothing) => (Just $ STAnn ann tree, Nothing)
-  (Just tree, Just rest') => case sdocToTreeParser rest' of
+  (Just tree, Just rest') => case sdocToTreeParser (assert_smaller rest rest') of
     (Just tree', rest'') => (Just $ STConcat [STAnn ann tree, tree'], rest'')
     (Nothing, rest'') => (Just $ STAnn ann tree, rest'')
-  (Nothing, Just rest') => assert_total $ sdocToTreeParser rest'
+  (Nothing, Just rest') => sdocToTreeParser (assert_smaller rest rest')
   (Nothing, Nothing) => (Nothing, Nothing)
 sdocToTreeParser (SAnnPop rest) = (Nothing, Just rest)
 

src/Core/Termination.idr

@@ -384,13 +384,11 @@ mutual
            log "totality.termination.sizechange" 10 $ "Looking under " ++ show !(toFullNames fn)
            aSmaller <- resolved (gamma defs) (NS builtinNS (UN "assert_smaller"))
            cond [(fn == NS builtinNS (UN "assert_total"), pure [])
-              -- #1782: this breaks totality!
-              -- ,(caseFn fn,
-              --     do mps <- getCasePats defs fn pats args
-              --        case mps of
-              --             Nothing => pure Prelude.Nil
-              --             Just ps => do scs <- traverse (findInCase defs g) ps
-              --                           pure (concat scs))
+                ,(caseFn fn,
+                    do scs1 <- traverse (findSC defs env g pats) args
+                       mps  <- getCasePats defs fn pats args
+                       scs2 <- traverse (findInCase defs g) $ fromMaybe [] mps
+                       pure (concat (scs1 ++ scs2)))
               ]
               (do scs <- traverse (findSC defs env g pats) args
                   pure ([MkSCCall fn

src/Libraries/Text/Lexer/Tokenizer.idr

@@ -121,7 +121,7 @@ tokenise reject tokenizer line col acc str
               end = endFn tag
               beginTok'' = MkBounded (mapBegin beginTok') False (MkBounds line col line' col')
               (midToks, (reason, line'', col'', rest'')) =
-                    tokenise end middle line' col' [] rest
+                    assert_total $ tokenise end middle line' col' [] rest
            in case reason of
                    (ComposeNotClosing _ _) => Left reason
                    _ => let Just (endTok', lineEnd, colEnd, restEnd) =

src/Libraries/Text/PrettyPrint/Prettyprinter/SimpleDocTree.idr

@@ -71,10 +71,10 @@ sdocToTreeParser (SLine i rest) = case sdocToTreeParser rest of
 sdocToTreeParser (SAnnPush ann rest) = case sdocToTreeParser rest of
   (tree, Nothing) => (Nothing, Nothing)
   (Just tree, Nothing) => (Just $ STAnn ann tree, Nothing)
-  (Just tree, Just rest') => case sdocToTreeParser rest' of
+  (Just tree, Just rest') => case sdocToTreeParser (assert_smaller rest rest') of
     (Just tree', rest'') => (Just $ STConcat [STAnn ann tree, tree'], rest'')
     (Nothing, rest'') => (Just $ STAnn ann tree, rest'')
-  (Nothing, Just rest') => assert_total $ sdocToTreeParser rest'
+  (Nothing, Just rest') => sdocToTreeParser (assert_smaller rest rest')
   (Nothing, Nothing) => (Nothing, Nothing)
 sdocToTreeParser (SAnnPop rest) = (Nothing, Just rest)
 

tests/idris2/total011/Issue1859-2.idr

@@ -0,0 +1,11 @@
+%default total
+
+tailRecId : (a -> Either a b) -> a -> b
+tailRecId f a = case f a of
+  Left a2 => tailRecId f a2
+  Right b => b
+
+iamvoid : Void
+iamvoid = tailRecId go ()
+  where go : () -> Either () Void
+        go () = Left ()

tests/idris2/total011/Issue1859.idr

@@ -0,0 +1,6 @@
+%default total
+
+fix : Void
+fix = case the (Either () Void) (Left ()) of
+        Left () => fix
+        Right p => absurd p

tests/idris2/total011/expected

@@ -14,3 +14,31 @@ Issue1460:3:1--3:43
  3 | nonproductive : Stream a -> (Stream a, ())
      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
+1/1: Building Issue1859 (Issue1859.idr)
+Error: fix is not total, possibly not terminating due to recursive path Main.fix -> Main.fix
+
+Issue1859:3:1--3:11
+ 1 | %default total
+ 2 | 
+ 3 | fix : Void
+     ^^^^^^^^^^
+
+1/1: Building Issue1859-2 (Issue1859-2.idr)
+Error: iamvoid is not total, possibly not terminating due to recursive path Main.iamvoid -> Main.tailRecId -> Main.tailRecId
+
+Issue1859-2:8:1--8:15
+ 4 | tailRecId f a = case f a of
+ 5 |   Left a2 => tailRecId f a2
+ 6 |   Right b => b
+ 7 | 
+ 8 | iamvoid : Void
+     ^^^^^^^^^^^^^^
+
+Error: tailRecId is not total, possibly not terminating due to recursive path Main.iamvoid -> Main.tailRecId -> Main.tailRecId
+
+Issue1859-2:3:1--3:40
+ 1 | %default total
+ 2 | 
+ 3 | tailRecId : (a -> Either a b) -> a -> b
+     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+

tests/idris2/total011/run

@@ -2,3 +2,5 @@ rm -rf build
 
 $1 --no-color --console-width 0 Issue1782.idr --check
 $1 --no-color --console-width 0 Issue1460.idr --check
+$1 --no-color --console-width 0 Issue1859.idr --check
+$1 --no-color --console-width 0 Issue1859-2.idr --check