[ termination ] faithful implementation of size-change graph termination analysis

- call sequences in termination errors now carry location information - new error message (`BadPath`) for late-starting loops - [ fix ] transitive closure of size-change graphs no longer ignores function arguments - update existing tests accordingly
2024-12-25 04:33:45 +03:00 · 2023-02-06 17:37:41 +00:00 · 2023-02-06 17:37:41 +00:00 · 914d68858b
commit 914d68858b
parent 9fd28bc130
15 changed files with 293 additions and 155 deletions
--- a/src/Core/Binary.idr
+++ b/src/Core/Binary.idr
@ -29,7 +29,7 @@ import public Libraries.Utils.Binary
 ||| version number if you're changing the version more than once in the same day.
 export
 ttcVersion : Int
-ttcVersion = 20220930 * 100 + 0
+ttcVersion = 20230118 * 100 + 0

 export
 checkTTCVersion : String -> Int -> Int -> Core ()
--- a/src/Core/Context.idr
+++ b/src/Core/Context.idr
@ -647,11 +647,13 @@ export
 HasNames PartialReason where
  full gam NotStrictlyPositive = pure NotStrictlyPositive
  full gam (BadCall ns) = pure $ BadCall !(traverse (full gam) ns)
-  full gam (RecPath ns) = pure $ RecPath !(traverse (full gam) ns)
+  full gam (BadPath init n) = pure $ BadPath !(traverse (traversePair (full gam)) init) !(full gam n)
+  full gam (RecPath loop) = pure $ RecPath !(traverse (traversePair (full gam)) loop)

  resolved gam NotStrictlyPositive = pure NotStrictlyPositive
  resolved gam (BadCall ns) = pure $ BadCall !(traverse (resolved gam) ns)
-  resolved gam (RecPath ns) = pure $ RecPath !(traverse (resolved gam) ns)
+  resolved gam (BadPath init n) = pure $ BadPath !(traverse (traversePair (resolved gam)) init) !(resolved gam n)
+  resolved gam (RecPath loop) = pure $ RecPath !(traverse (traversePair (resolved gam)) loop)

 export
 HasNames Terminating where
--- a/src/Core/Context/Context.idr
+++ b/src/Core/Context/Context.idr
@ -294,6 +294,7 @@ record SCCall where
        -- (in the calling function), and how its size changed in the call.
        -- 'Nothing' if it's not related to any of the calling function's
        -- arguments
+     fnLoc : FC

 export
 Show SCCall where
--- a/src/Core/TT.idr
+++ b/src/Core/TT.idr
@ -1144,7 +1144,9 @@ public export
 data PartialReason
       = NotStrictlyPositive
       | BadCall (List Name)
-       | RecPath (List Name)
+       -- sequence of mutually-recursive function calls leading to a non-terminating function
+       | BadPath (List (FC, Name)) Name
+       | RecPath (List (FC, Name))

 export
 Show PartialReason where
@ -1153,8 +1155,12 @@ Show PartialReason where
      = "possibly not terminating due to call to " ++ show n
  show (BadCall ns)
      = "possibly not terminating due to calls to " ++ showSep ", " (map show ns)
-  show (RecPath ns)
-      = "possibly not terminating due to recursive path " ++ showSep " -> " (map show ns)
+  show (BadPath [_] n)
+      = "possibly not terminating due to call  to " ++ show n
+  show (BadPath init n)
+      = "possibly not terminating due to function " ++ show n ++ " being reachable via " ++ showSep " -> " (map show init)
+  show (RecPath loop)
+      = "possibly not terminating due to recursive path " ++ showSep " -> " (map (show . snd) loop)

 export
 Pretty Void PartialReason where
@ -1163,8 +1169,14 @@ Pretty Void PartialReason where
    = reflow "possibly not terminating due to call to" <++> pretty n
  pretty (BadCall ns)
    = reflow "possibly not terminating due to calls to" <++> concatWith (surround (comma <+> space)) (pretty <$> ns)
-  pretty (RecPath ns)
-    = reflow "possibly not terminating due to recursive path" <++> concatWith (surround (pretty " -> ")) (pretty <$> ns)
+  pretty (BadPath [_] n)
+    = reflow "possibly not terminating due to call to" <++> pretty n
+  pretty (BadPath init n)
+    = reflow "possibly not terminating due to function" <++> pretty n
+      <++> reflow "being reachable via"
+      <++> concatWith (surround (pretty " -> ")) (pretty <$> map snd init)
+  pretty (RecPath loop)
+    = reflow "possibly not terminating due to recursive path" <++> concatWith (surround (pretty " -> ")) (pretty <$> map snd loop)

 public export
 data Terminating
--- a/src/Core/TTC.idr
+++ b/src/Core/TTC.idr
@ -509,7 +509,8 @@ export
 TTC PartialReason where
  toBuf b NotStrictlyPositive = tag 0
  toBuf b (BadCall xs) = do tag 1; toBuf b xs
-  toBuf b (RecPath xs) = do tag 2; toBuf b xs
+  toBuf b (BadPath xs n) = do tag 2; toBuf b xs; toBuf b n
+  toBuf b (RecPath xs) = do tag 3; toBuf b xs

  fromBuf b
      = case !getTag of
@ -517,6 +518,9 @@ TTC PartialReason where
             1 => do xs <- fromBuf b
                     pure (BadCall xs)
             2 => do xs <- fromBuf b
+                     n <- fromBuf b
+                     pure (BadPath xs n)
+             3 => do xs <- fromBuf b
                     pure (RecPath xs)
             _ => corrupt "PartialReason"

@ -1073,11 +1077,12 @@ TTC SizeChange where

 export
 TTC SCCall where
-  toBuf b c = do toBuf b (fnCall c); toBuf b (fnArgs c)
+  toBuf b c = do toBuf b (fnCall c); toBuf b (fnArgs c); toBuf b (fnLoc c)
  fromBuf b
      = do fn <- fromBuf b
           args <- fromBuf b
-           pure (MkSCCall fn args)
+           loc <- fromBuf b
+           pure (MkSCCall fn args loc)

 export
 TTC GlobalDef where
--- a/src/Core/Termination.idr
+++ b/src/Core/Termination.idr
@ -9,6 +9,7 @@ import Core.Value

 import Libraries.Data.NameMap
 import Libraries.Data.SortedMap
+import Libraries.Data.SortedSet
 import Data.List
 import Data.String

@ -393,7 +394,8 @@ mutual
              (do scs <- traverse (findSC defs env g pats) args
                  pure ([MkSCCall fn
                           (expandToArity arity
-                                (map (mkChange defs aSmaller pats) args))]
+                                (map (mkChange defs aSmaller pats) args))
+                           fc]
                           ++ concat scs))

  findInCase : {auto c : Ref Ctxt Defs} ->
@ -435,142 +437,258 @@ calculateSizeChange loc n
         getSC defs (definition def)

 Arg : Type
-Arg = Int
+Arg = Nat

-data APos : Type where
+Change : Type
+Change = List (Maybe (Arg, SizeChange))

-firstArg : Arg
-firstArg = 0
+Path : Type
+Path = List (FC, Name)

-nextArg : Arg -> Arg
-nextArg x = x + 1
+record ArgChange where
+  constructor MkArgChange
+  change : Change
+  path : Path

-initArgs : {auto a : Ref APos Arg} ->
-           Nat -> Core (List (Maybe (Arg, SizeChange)))
-initArgs Z = pure []
-initArgs (S k)
-    = do arg <- get APos
-         put APos (nextArg arg)
-         args' <- initArgs k
-         pure (Just (arg, Same) :: args')
+-- ignore path
+Eq ArgChange where
+  (==) a1 a2 = a1.change == a2.change

-data Explored : Type where
+Ord ArgChange where
+  compare a1 a2 = compare a1.change a2.change

-- Cached results of exploring the size change graph, so that if we visit a
-- node again, we don't have to re-explore the whole thing
-SizeChanges : Type
-SizeChanges = SortedMap (Name, List (Maybe Arg)) Terminating
+Show ArgChange where
+  show a = show a.change ++ " @" ++ show a.path

-- Traverse the size change graph. When we reach a point we've seen before,
-- at least one of the arguments must have got smaller, otherwise it's
-- potentially non-terminating
-checkSC : {auto a : Ref APos Arg} ->
-          {auto c : Ref Ctxt Defs} ->
-          {auto e : Ref Explored SizeChanges} ->
-          Defs ->
-          Name -> -- function we're checking
-          List (Maybe (Arg, SizeChange)) -> -- functions arguments and change
-          List (Name, List (Maybe Arg)) -> -- calls we've seen so far
-          Core Terminating
-checkSC defs f args path
-   = do exp <- get Explored
-        log "totality.termination.sizechange" 7 $ "Checking Size Change Graph: " ++ show !(toFullNames f)
-        let pos = (f, map (map Builtin.fst) args)
-        case lookup pos exp of
-             Just done => pure done -- already explored this bit of tree
-             Nothing =>
-                if pos `elem` path
-                   then do log "totality.termination.sizechange.inPath" 8 $ "Checking arguments: " ++ show !(toFullNames f)
-                           res <- toFullNames $ checkDesc (mapMaybe (map Builtin.snd) args) path
-                           put Explored (insert pos res exp)
-                           pure res
-                   else case !(lookupCtxtExact f (gamma defs)) of
-                             Nothing => do log "totality.termination.sizechange.isTerminating" 8 $ "Size Change Graph is Terminating for: " ++ show !(toFullNames f)
-                                           pure IsTerminating
-                             Just def => do log "totality.termination.sizechange.needsChecking" 8 $ "Size Change Graph needs traversing: " ++ show !(toFullNames f)
-                                            continue (sizeChange def) (pos :: path)
+-- sc-graphs to be added
+WorkList : Type
+WorkList = SortedSet (Name, Name, ArgChange)
+
+-- transitively-closed (modulo work list) set of sc-graphs
+SCSet : Type
+SCSet = NameMap (NameMap (SortedSet ArgChange))
+
+lookupMap : Name -> NameMap (NameMap v) -> NameMap v
+lookupMap n m = fromMaybe empty (lookup n m)
+
+lookupSet : Ord v => Name -> NameMap (SortedSet v) -> SortedSet v
+lookupSet n m = fromMaybe empty (lookup n m)
+
+lookupGraphs : Name -> Name -> SCSet -> SortedSet ArgChange
+lookupGraphs f g = lookupSet g . lookupMap f
+
+selectDom : Name -> SCSet -> SCSet
+selectDom f s = insert f (lookupMap f s) empty
+
+selectCod : Name -> SCSet -> SCSet
+selectCod g s = map (\m => insert g (lookupSet g m) empty) s
+
+foldl : (acc -> Name -> Name -> ArgChange -> acc) -> acc -> SCSet -> acc
+foldl f_acc acc
+    = foldlNames (\acc, f =>
+        foldlNames (\acc, g =>
+          foldl (\acc, c => f_acc acc f g c) acc)
+          acc)
+        acc
+
+insertGraph : Name -> Name -> ArgChange -> SCSet -> SCSet
+insertGraph f g ch s
+  = let s_f = lookupMap f s in
+    let s_fg = lookupSet g s_f in
+    insert f (insert g (insert ch s_fg) s_f) s
+
+composeChange : Change -> Change -> Change
+composeChange c1 c2
+    = map ((=<<) (\(i, r) => updateArg r <$> getArg i c1)) c2
  where
-    -- Look for something descending in the list of size changes
-    checkDesc : List SizeChange -> List (Name, List (Maybe Arg)) -> Terminating
-    checkDesc [] path = NotTerminating (RecPath (reverse (map fst path)))
-    checkDesc (Smaller :: _) _ = IsTerminating
-    checkDesc (_ :: xs) path = checkDesc xs path
+    getArg : forall a . Nat -> List (Maybe a) -> Maybe a
+    getArg _ [] = Nothing
+    getArg Z (x :: xs) = x
+    getArg (S k) (x :: xs) = getArg k xs

-    getPos : forall a . List a -> Nat -> Maybe a
-    getPos [] _ = Nothing
-    getPos (x :: xs) Z = Just x
-    getPos (x :: xs) (S k) = getPos xs k
+    updateArg : SizeChange -> (Arg, SizeChange) -> (Arg, SizeChange)
+    updateArg c arg@(_, Unknown) = arg
+    updateArg Unknown (i, _) = (i, Unknown)
+    updateArg c (i, Same) = (i, c)
+    updateArg c arg@(_, Smaller) = arg

-    updateArg : SizeChange -> Maybe (Arg, SizeChange) -> Maybe (Arg, SizeChange)
-    updateArg c Nothing = Nothing
-    updateArg c arg@(Just (i, Unknown)) = arg
-    updateArg Unknown (Just (i, _)) = Just (i, Unknown)
-    updateArg c (Just (i, Same)) = Just (i, c)
-    updateArg c arg = arg
+composeArgChange : ArgChange -> ArgChange -> ArgChange
+composeArgChange a1 a2
+    = MkArgChange
+        (composeChange a1.change a2.change)
+        (a1.path ++ a2.path)

-    mkArgs : List (Maybe (Nat, SizeChange)) -> List (Maybe (Arg, SizeChange))
-    mkArgs [] = []
-    mkArgs (Nothing :: xs) = Nothing :: mkArgs xs
-    mkArgs (Just (pos, c) :: xs)
-        = case getPos args pos of
-               Nothing => Nothing :: mkArgs xs
-               Just arg => updateArg c arg :: mkArgs xs
+preCompose : Name -> ArgChange ->
+             SCSet ->
+             WorkList ->
+             Name -> Name -> ArgChange ->
+             WorkList
+preCompose f ch1 s work _ h ch2
+   = let ch = composeArgChange ch1 ch2 in
+     if contains ch (lookupGraphs f h s) then
+       work
+     else
+       insert (f, h, ch) work

-    checkCall : List (Name, List (Maybe Arg)) -> SCCall -> Core Terminating
-    checkCall path sc
-        = do Just gdef <- lookupCtxtExact (fnCall sc) (gamma defs)
-                  | Nothing => pure IsTerminating -- nothing to check
-             let Unchecked = isTerminating (totality gdef)
-                  | IsTerminating => pure IsTerminating
-                  | _ => pure (NotTerminating (BadCall [fnCall sc]))
-             log "totality.termination.sizechange.checkCall" 8 $
-                "CheckCall Size Change Graph: " ++ show !(toFullNames (fnCall sc))
-             term <- checkSC defs (fnCall sc) (mkArgs (fnArgs sc)) path
-             let inpath = fnCall sc `elem` map fst path
-             if not inpath
-                then case term of
-                       NotTerminating (RecPath _) =>
-                          -- might have lost information while assuming this
-                          -- was mutually recursive, so start again with new
-                          -- arguments (that is, where we'd start if the
-                          -- function was the top level thing we were checking)
-                          do log "totality.termination.sizechange.checkCall.inPathNot.restart" 9 $ "ReChecking Size Change Graph: " ++ show !(toFullNames (fnCall sc))
-                             args' <- initArgs (length (fnArgs sc))
-                             t <- checkSC defs (fnCall sc) args' path
-                             setTerminating emptyFC (fnCall sc) t
-                             pure t
-                       t => do log "totality.termination.sizechange.checkCall.inPathNot.return" 9 $ "Have result: " ++ show !(toFullNames (fnCall sc))
-                               pure t
-                else do log "totality.termination.sizechange.checkCall.inPath" 9 $ "Have Result: " ++ show !(toFullNames (fnCall sc))
-                        pure term
+postCompose : Name -> ArgChange ->
+              SCSet ->
+              WorkList ->
+              Name -> Name -> ArgChange ->
+              WorkList
+postCompose h ch2 s work f _ ch1
+   = let ch = composeArgChange ch1 ch2 in
+     if contains ch (lookupGraphs f h s) then
+       work
+     else
+       insert (f, h, ch) work

-    getWorst : Terminating -> List Terminating -> Terminating
-    getWorst term [] = term
-    getWorst term (IsTerminating :: xs) = getWorst term xs
-    getWorst term (Unchecked :: xs) = getWorst Unchecked xs
-    getWorst term (bad :: xs) = bad
+mutual
+  addGraph : {auto c : Ref Ctxt Defs} ->
+             Name -> Name -> ArgChange ->
+             WorkList ->
+             SCSet ->
+             SCSet
+  addGraph f g ch work s_in
+      = let s = insertGraph f g ch s_in
+            after = selectDom g s
+            work_pre = foldl (preCompose f ch s) work after
+            before = selectCod f s
+            work_post = foldl (postCompose g ch s) work_pre before in
+        transitiveClosure work_post s

-    continue : List SCCall -> List (Name, List (Maybe Arg)) -> Core Terminating
-    continue scs path
-        = do allTerm <- traverse (checkCall path) scs
-             pure (getWorst IsTerminating allTerm)
+  transitiveClosure : {auto c : Ref Ctxt Defs} ->
+                      WorkList ->
+                      SCSet ->
+                      SCSet
+  transitiveClosure work s
+      = case pop work of
+             Nothing => s
+             Just ((f, g, ch), work) =>
+               addGraph f g ch work s
+
+-- find (potential) chain of calls to given function (inclusive)
+prefixPath : NameMap (FC, Name) -> Name -> Path
+prefixPath pred g = go g []
+  where
+    go : Name -> Path -> Path
+    go g path
+        = let Just (l, f) = lookup g pred
+             | Nothing => path in
+          if f == g then -- we've reached the entry point!
+            path
+          else
+            go f ((l, g) :: path)
+
+findLoops : {auto c : Ref Ctxt Defs} -> SCSet -> Core (NameMap (Maybe Path))
+findLoops s
+    = do let loops = filterEndos (\a => composeChange a.change a.change == a.change) s
+         log "totality.termination.calc" 7 $ "Loops: " ++ show loops
+         let terms = map (foldMap (\a => checkDesc a.change a.path)) loops
+         pure terms
+    where
+      filterEndos : (ArgChange -> Bool) -> SCSet -> NameMap (List ArgChange)
+      filterEndos p = mapWithKey (\f, m => filter p (Data.SortedSet.toList (lookupSet f m)))
+
+      checkDesc : Change -> Path -> Maybe Path
+      checkDesc [] p = Just p
+      checkDesc (Just (_, Smaller) :: _) p = Nothing
+      checkDesc (_ :: xs) p = checkDesc xs p
+
+findNonTerminatingLoop : {auto c : Ref Ctxt Defs} -> SCSet -> Core (Maybe (Name, Path))
+findNonTerminatingLoop s
+    = do loops <- findLoops s
+         pure $ findNonTerminating loops
+    where
+      findNonTerminating : NameMap (Maybe Path) -> Maybe (Name, Path)
+      findNonTerminating = foldlNames (\acc, g, m => map (g,) m <+> acc) empty
+
+setPrefixTerminating : {auto c : Ref Ctxt Defs} ->
+        Path -> Name -> Core ()
+setPrefixTerminating [] g = pure ()
+setPrefixTerminating (_ :: []) g = pure ()
+setPrefixTerminating ((l, f) :: p) g
+    = do setTerminating l f (NotTerminating (BadPath p g))
+         setPrefixTerminating p g
+
+addFunctions : {auto c : Ref Ctxt Defs} ->
+              Defs ->
+              List GlobalDef -> -- functions we're adding
+              NameMap (FC, Name) -> -- functions we've already seen (and their predecessor)
+              WorkList ->
+              Core (Either Terminating (WorkList, NameMap (FC, Name)))
+addFunctions defs [] pred work
+    = pure $ Right (work, pred)
+addFunctions defs (d1 :: ds) pred work
+    = do log "totality.termination.calc" 8 $ "Adding function: " ++ show d1.fullname
+         calls <- foldlC resolveCall [] d1.sizeChange
+         let Nothing = find isNonTerminating calls
+            | Just (d2, l, _) => do let g = d2.fullname
+                                    log "totality.termination.calc" 7 $ "Non-terminating function call: " ++ show g
+                                    let init = prefixPath pred d1.fullname ++ [(l, g)]
+                                    setPrefixTerminating init g
+                                    pure $ Left (NotTerminating (BadPath init g))
+         let (ds, pred, work) = foldl addCall (ds, pred, work) (filter isUnchecked calls)
+         addFunctions defs ds pred work
+  where
+    resolveCall : List (GlobalDef, FC, (Name, Name, ArgChange)) ->
+                  SCCall ->
+                  Core (List (GlobalDef, FC, (Name, Name, ArgChange)))
+    resolveCall calls (MkSCCall g ch l)
+        = do Just d2 <- lookupCtxtExact g (gamma defs)
+                | Nothing => do log "totality.termination.calc" 7 $ "Not found: " ++ show g
+                                pure calls
+             pure ((d2, l, (d1.fullname, d2.fullname, MkArgChange ch [(l, d2.fullname)])) :: calls)
+
+    addCall : (List GlobalDef, NameMap (FC, Name), WorkList) ->
+                  (GlobalDef, FC, (Name, Name, ArgChange)) ->
+                  (List GlobalDef, NameMap (FC, Name), WorkList)
+    addCall (ds, pred, work_in) (d2, l, c)
+        = let work = insert c work_in in
+          case lookup d2.fullname pred of
+               Just _ =>
+                 (ds, pred, work)
+               Nothing =>
+                 (d2 :: ds, insert d2.fullname (l, d1.fullname) pred, work)
+
+    isNonTerminating : (GlobalDef, _, _) -> Bool
+    isNonTerminating (d2, _, _)
+        = case d2.totality.isTerminating of
+               NotTerminating _ => True
+               _ => False
+
+    isUnchecked : (GlobalDef, _, _) -> Bool
+    isUnchecked (d2, _, _)
+        = case d2.totality.isTerminating of
+               Unchecked => True
+               _ => False
+
+initWork : {auto c : Ref Ctxt Defs} ->
+           Defs ->
+           GlobalDef -> -- entry
+           Core (Either Terminating (WorkList, NameMap (FC, Name)))
+initWork defs def = addFunctions defs [def] (insert def.fullname (def.location, def.fullname) empty) empty

 calcTerminating : {auto c : Ref Ctxt Defs} ->
                  FC -> Name -> Core Terminating
 calcTerminating loc n
    = do defs <- get Ctxt
         log "totality.termination.calc" 7 $ "Calculating termination: " ++ show !(toFullNames n)
-         case !(lookupCtxtExact n (gamma defs)) of
-              Nothing => undefinedName loc n
-              Just def =>
-                case !(totRefs defs (nub !(addCases defs (keys (refersTo def))))) of
-                     IsTerminating =>
-                        do let ty = type def
-                           a <- newRef APos firstArg
-                           args <- initArgs !(getArity defs [] ty)
-                           e <- newRef Explored empty
-                           checkSC defs n args []
-                     bad => pure bad
+         Just def <- lookupCtxtExact n (gamma defs)
+            | Nothing => undefinedName loc n
+         IsTerminating <- totRefs defs (nub !(addCases defs (keys (refersTo def))))
+            | bad => pure bad
+         Right (work, pred) <- initWork defs def
+            | Left bad => pure bad
+         let s = transitiveClosure work empty
+         Nothing <- findNonTerminatingLoop s
+           | Just (g, loop) =>
+               ifThenElse (def.fullname == g)
+                 (pure $ NotTerminating (RecPath loop))
+                 (do setTerminating EmptyFC g (NotTerminating (RecPath loop))
+                     let init = prefixPath pred g
+                     setPrefixTerminating init g
+                     pure $ NotTerminating (BadPath init g))
+         pure IsTerminating
  where
    addCases' : Defs -> NameMap () -> List Name -> Core (List Name)
    addCases' defs all [] = pure (keys all)
--- a/tests/idris2/error013/expected
+++ b/tests/idris2/error013/expected
@ -1,5 +1,5 @@
 1/1: Building Issue361 (Issue361.idr)
-Error: main is not total, possibly not terminating due to call to Main.(/=)
+Error: main is not total, possibly not terminating due to function Main.(==) being reachable via Main.Eq implementation at Issue361:5:1--5:11 -> Main.(==)

 Issue361:7:1--7:13
 3 | data S = T | F
@ -9,7 +9,7 @@ Issue361:7:1--7:13
 7 | main : IO ()
     ^^^^^^^^^^^^

-Error: /= is not total, possibly not terminating due to recursive path Main.main -> Main.Eq implementation at Issue361:5:1--5:11 -> Main.(==) -> Main.(/=) -> Main.(==)
+Error: /= is not total, possibly not terminating due to call to Main.Eq implementation at Issue361:5:1--5:11

 Issue361:5:1--5:11
 1 | %default total
@ -19,7 +19,7 @@ Issue361:5:1--5:11
 5 | Eq S where
     ^^^^^^^^^^

-Error: == is not total, possibly not terminating due to call to Main.(/=)
+Error: == is not total, possibly not terminating due to recursive path Main.(/=) -> Main.(==)

 Issue361:5:1--5:11
 1 | %default total
--- a/tests/idris2/failing003/FailingTotality.idr
+++ b/tests/idris2/failing003/FailingTotality.idr
@ -9,7 +9,7 @@ failing "x is not covering."


 failing "x is not total, possibly not terminating due to recursive
-         path FailingTotality.x -> FailingTotality.x"
+         path FailingTotality.x"

  x : Bool
  x = x
--- a/tests/idris2/termination001/expected
+++ b/tests/idris2/termination001/expected
@ -1,5 +1,5 @@
 1/1: Building AgdaIssue6059 (AgdaIssue6059.idr)
-Error: f is not total, possibly not terminating due to call to Main.f
+Error: f is not total, possibly not terminating due to call to Main.g

 AgdaIssue6059:23:3--23:21
 19 | lem 0 = Refl
@ -9,7 +9,7 @@ AgdaIssue6059:23:3--23:21
 23 |   f : (x : D) -> P x
        ^^^^^^^^^^^^^^^^^^

-Error: g is not total, possibly not terminating due to call to Main.f
+Error: g is not total, possibly not terminating due to recursive path Main.f -> Main.g

 AgdaIssue6059:31:3--31:32
 27 |   -- Base cases:
@ -19,7 +19,7 @@ AgdaIssue6059:31:3--31:32
 31 |   g : (h : Nat -> D) -> P (h 2)
        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

-Error: f is not total, possibly not terminating due to call to Main.f
+Error: f is not total, possibly not terminating due to call to Main.g

 AgdaIssue6059:23:3--23:21
 19 | lem 0 = Refl
@ -29,7 +29,7 @@ AgdaIssue6059:23:3--23:21
 23 |   f : (x : D) -> P x
        ^^^^^^^^^^^^^^^^^^

-Error: g is not total, possibly not terminating due to call to Main.f
+Error: g is not total, possibly not terminating due to recursive path Main.f -> Main.g

 AgdaIssue6059:31:3--31:32
 27 |   -- Base cases:
--- a/tests/idris2/total004/expected
+++ b/tests/idris2/total004/expected
@ -6,12 +6,12 @@ Main> Main.bar is total
 Main> Main.swapR is total
 Main> Main.loopy is possibly not terminating due to recursive path Main.loopy
 Main> Main.foom is total
-Main> Main.pfoom is possibly not terminating due to recursive path Main.pfoom -> Main.pfoom
+Main> Main.pfoom is possibly not terminating due to recursive path Main.pfoom
 Main> Main.even is total
-Main> Main.vtrans is possibly not terminating due to recursive path Main.vtrans -> Main.vtrans
+Main> Main.vtrans is possibly not terminating due to recursive path Main.vtrans
 Main> Main.GTree is total
 Main> Main.size is total
-Main> Main.qsortBad is possibly not terminating due to recursive path Main.qsortBad -> Main.qsortBad
+Main> Main.qsortBad is possibly not terminating due to recursive path Main.qsortBad
 Main> Main.qsort is total
 Main> Main.qsort' is total
 Main> Main.mySorted is total
--- a/tests/idris2/total006/expected
+++ b/tests/idris2/total006/expected
@ -2,7 +2,7 @@
 Main> Main.streamCount is total
 Main> Main.badCount is possibly not terminating due to recursive path Main.badCount
 Main> Main.process is total
-Main> Main.badProcess is possibly not terminating due to recursive path Main.badProcess -> Main.badProcess -> Main.badProcess
+Main> Main.badProcess is possibly not terminating due to recursive path Main.badProcess -> Main.badProcess
 Main> Main.doubleInt is total
 Main> Main.main is total
 Main> Bye for now!
--- a/tests/idris2/total007/expected
+++ b/tests/idris2/total007/expected
@ -8,7 +8,7 @@ partial:5:1--6:19
 Missing cases:
    foo Nothing

-Error: qsortBad is not total, possibly not terminating due to recursive path Main.qsortBad -> Main.qsortBad -> Main.qsortBad
+Error: qsortBad is not total, possibly not terminating due to recursive path Main.qsortBad

 partial:13:1--14:37
 13 | total
--- a/tests/idris2/total011/expected
+++ b/tests/idris2/total011/expected
@ -1,12 +1,12 @@
 1/1: Building Issue1782 (Issue1782.idr)
-Error: hack is not total, possibly not terminating due to recursive path Main.hack -> Main.hack
+Error: hack is not total, possibly not terminating due to recursive path Main.hack

 Issue1782:8:1--9:27
 8 | total
 9 | hack : Nat -> (Void, Void)

 1/1: Building Issue1460 (Issue1460.idr)
-Error: nonproductive is not total, possibly not terminating due to recursive path Main.nonproductive -> Main.nonproductive -> Main.nonproductive
+Error: nonproductive is not total, possibly not terminating due to recursive path Main.nonproductive

 Issue1460:3:1--3:43
 1 | %default total
@ -15,7 +15,7 @@ Issue1460:3:1--3:43
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

 1/1: Building Issue1859 (Issue1859.idr)
-Error: fix is not total, possibly not terminating due to recursive path Main.fix -> Main.fix
+Error: fix is not total, possibly not terminating due to recursive path Main.fix

 Issue1859:3:1--3:11
 1 | %default total
@ -24,7 +24,7 @@ Issue1859:3:1--3:11
     ^^^^^^^^^^

 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
+Error: iamvoid is not total, possibly not terminating due to call to Main.tailRecId

 Issue1859-2:8:1--8:15
 4 | tailRecId f a = case f a of
@ -34,7 +34,7 @@ Issue1859-2:8:1--8:15
 8 | iamvoid : Void
     ^^^^^^^^^^^^^^

-Error: tailRecId is not total, possibly not terminating due to recursive path Main.iamvoid -> Main.tailRecId -> Main.tailRecId
+Error: tailRecId is not total, possibly not terminating due to recursive path Main.tailRecId

 Issue1859-2:3:1--3:40
 1 | %default total
@ -43,7 +43,7 @@ Issue1859-2:3:1--3:40
     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

 1/1: Building Issue1828 (Issue1828.idr)
-Error: caseTest is not total, possibly not terminating due to recursive path Main.caseTest -> Main.dummy -> Main.caseTest
+Error: caseTest is not total, possibly not terminating due to call to Main.dummy

 Issue1828:4:3--4:25
 1 | %default total
@ -52,7 +52,7 @@ Issue1828:4:3--4:25
 4 |   caseTest : Nat -> Bool
       ^^^^^^^^^^^^^^^^^^^^^^

-Error: dummy is not total, possibly not terminating due to recursive path Main.caseTest -> Main.dummy -> Main.caseTest
+Error: dummy is not total, possibly not terminating due to recursive path Main.caseTest -> Main.dummy

 Issue1828:8:3--8:14
 4 |   caseTest : Nat -> Bool
@ -62,7 +62,7 @@ Issue1828:8:3--8:14
 8 |   dummy : Nat
       ^^^^^^^^^^^

-Error: caseTest is not total, possibly not terminating due to recursive path Main.caseTest -> Main.dummy -> Main.caseTest
+Error: caseTest is not total, possibly not terminating due to call to Main.dummy

 Issue1828:4:3--4:25
 1 | %default total
@ -71,7 +71,7 @@ Issue1828:4:3--4:25
 4 |   caseTest : Nat -> Bool
       ^^^^^^^^^^^^^^^^^^^^^^

-Error: dummy is not total, possibly not terminating due to recursive path Main.caseTest -> Main.dummy -> Main.caseTest
+Error: dummy is not total, possibly not terminating due to recursive path Main.caseTest -> Main.dummy

 Issue1828:8:3--8:14
 4 |   caseTest : Nat -> Bool
--- a/tests/idris2/total012/expected
+++ b/tests/idris2/total012/expected
@ -3,14 +3,14 @@ LOG totality.requirement:10: Checking totality requirement of Issue1828.idr (mai
 LOG totality.requirement:20: Reading totalReq from build/ttc/Issue1828.ttc
 LOG totality.requirement:20: Got covering and expected total: we should rebuild
 1/1: Building Issue1828 (Issue1828.idr)
-Error: caseTest is not total, possibly not terminating due to recursive path Main.caseTest -> Main.dummy -> Main.caseTest
+Error: caseTest is not total, possibly not terminating due to call to Main.dummy

 Issue1828:2:3--2:25
 1 | mutual
 2 |   caseTest : Nat -> Bool
       ^^^^^^^^^^^^^^^^^^^^^^

-Error: dummy is not total, possibly not terminating due to recursive path Main.caseTest -> Main.dummy -> Main.caseTest
+Error: dummy is not total, possibly not terminating due to recursive path Main.caseTest -> Main.dummy

 Issue1828:6:3--6:14
 2 |   caseTest : Nat -> Bool
@ -20,14 +20,14 @@ Issue1828:6:3--6:14
 6 |   dummy : Nat
       ^^^^^^^^^^^

-Error: caseTest is not total, possibly not terminating due to recursive path Main.caseTest -> Main.dummy -> Main.caseTest
+Error: caseTest is not total, possibly not terminating due to call to Main.dummy

 Issue1828:2:3--2:25
 1 | mutual
 2 |   caseTest : Nat -> Bool
       ^^^^^^^^^^^^^^^^^^^^^^

-Error: dummy is not total, possibly not terminating due to recursive path Main.caseTest -> Main.dummy -> Main.caseTest
+Error: dummy is not total, possibly not terminating due to recursive path Main.caseTest -> Main.dummy

 Issue1828:6:3--6:14
 2 |   caseTest : Nat -> Bool
--- a/tests/ttimp/total002/expected
+++ b/tests/ttimp/total002/expected
@ -5,5 +5,5 @@ Yaffle> Main.ack is total
 Yaffle> Main.foo is total
 Yaffle> Main.foo' is total
 Yaffle> Main.foom is total
-Yaffle> Main.pfoom is possibly not terminating due to recursive path Main.pfoom -> Main.pfoom
+Yaffle> Main.pfoom is possibly not terminating due to recursive path Main.pfoom
 Yaffle> Bye for now!