Cache intermediate results in totality checking

This saves a lot of unnecessary exploring of size change graphs, which
can get over the top quite quickly if there's complex mutual
definitions, or even just a single function with an interesting variety
of recursive calls.

Fixes #1365
Fixes #1277
Fixes #645

Author: edwinb

src/Core/Termination.idr

@@ -11,6 +11,7 @@ import Core.Value
 import Control.Monad.State
 
 import Libraries.Data.NameMap
+import Libraries.Data.SortedMap
 import Data.List
 
 %default covering
@@ -438,27 +439,41 @@ initArgs (S k)
          args' <- initArgs k
          pure (Just (arg, Same) :: args')
 
+data Explored : Type where
+
+-- 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
+
 -- 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 log "totality.termination.sizechange" 7 $ "Checking Size Change Graph: " ++ show !(toFullNames f)
+   = do exp <- get Explored
+        log "totality.termination.sizechange" 7 $ "Checking Size Change Graph: " ++ show !(toFullNames f)
         let pos = (f, map (map Builtin.fst) args)
-        if pos `elem` path
-           then do log "totality.termination.sizechange.inPath" 8 $ "Checking arguments: " ++ show !(toFullNames f)
-                   toFullNames $ checkDesc (mapMaybe (map Builtin.snd) args) path
-           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)
+        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)
   where
     -- Look for something descending in the list of size changes
     checkDesc : List SizeChange -> List (Name, List (Maybe Arg)) -> Terminating
@@ -488,14 +503,14 @@ checkSC defs f args path
 
     checkCall : List (Name, List (Maybe Arg)) -> SCCall -> Core Terminating
     checkCall path sc
-        = do let inpath = fnCall sc `elem` map fst path
-             Just gdef <- lookupCtxtExact (fnCall sc) (gamma defs)
+        = 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 _) =>
@@ -505,7 +520,9 @@ checkSC defs f args path
                           -- 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))
-                             checkSC defs (fnCall sc) args' path
+                             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))
@@ -535,6 +552,7 @@ calcTerminating loc n
                         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
   where

tests/Main.idr

@@ -121,7 +121,8 @@ idrisTestsPerformance : TestPool
 idrisTestsPerformance = MkTestPool "Performance" []
        -- Performance: things which have been slow in the past, or which
        -- pose interesting challenges for the elaborator
-      ["perf001", "perf002", "perf003", "perf004", "perf005", "perf006"]
+      ["perf001", "perf002", "perf003", "perf004", "perf005", "perf006",
+       "perf007"]
 
 idrisTestsRegression : TestPool
 idrisTestsRegression = MkTestPool "Various regressions" []

tests/idris2/error013/expected

@@ -1,5 +1,5 @@
 1/1: Building Issue361 (Issue361.idr)
-Error: main is not total, possibly not terminating due to recursive path Main.main -> Main.Eq implementation at Issue361.idr:5:1--5:11 -> Main.== -> Main./= -> Main.==
+Error: main is not total, possibly not terminating due to call to Main./=
 
 Issue361.idr:7:1--7:13
  3 | data S = T | F
@@ -9,7 +9,7 @@ Issue361.idr:7:1--7:13
  7 | main : IO ()
      ^^^^^^^^^^^^
 
-Error: /= is not total, possibly not terminating due to recursive path Main./= -> Main.== -> Main./= -> Main.==
+Error: /= is not total, possibly not terminating due to recursive path Main.main -> Main.Eq implementation at Issue361.idr:5:1--5:11 -> Main.== -> Main./= -> Main.==
 
 Issue361.idr:5:1--5:11
  1 | %default total

tests/idris2/perf007/Slooow.idr

@@ -0,0 +1,28 @@
+%default total
+
+data TTy : Nat -> Nat -> Nat -> Nat -> Bool -> Type where
+
+  TA : TTy p1 r1 i1 i2 False ->
+       TTy i1 i2 i1 u2 False ->
+       TTy i1 i2 p2 b1 b2    ->
+       TTy p1 r1 p1 i2 False
+
+  TB : TTy v1 r1 v2 r2 bt ->
+       TTy v1 r1 v1 r2 (be && bt)
+
+  TC : TTy p1 r1 v2 r2 False ->
+       TTy v2 r2 v3 r3 b2    ->
+       TTy p1 r1 v3 r3 b2
+
+n : Nat -> Nat
+n = (+ 2)
+                              
+showInd : (indent : Nat) -> TTy p1 r1 v3 r3 br -> String
+showInd i (TA x1 x2 x3) = if False
+                            then (if False then show' i else show' i)
+                            else showInd (n i) x1 ++ show' (n i)
+                            where
+                              show' : Nat -> String
+                              show' i = showInd (n i) x3 ++ if False then "" else showInd (n i) x2
+showInd i (TB x) = showInd (n i) x ++ if False then "" else showInd (n i) x
+showInd i (TC x y) = if False then showInd i y else showInd i x ++ showInd i y

tests/idris2/perf007/expected

@@ -0,0 +1 @@
+1/1: Building Slooow (Slooow.idr)

tests/idris2/perf007/run

@@ -0,0 +1,3 @@
+$1 --check Slooow.idr
+
+rm -rf build

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 -> Main.pfoom
+Yaffle> Main.pfoom is possibly not terminating due to recursive path Main.pfoom -> Main.pfoom
 Yaffle> Bye for now!