[ new ] totality checking can look under constructors (#3328)

* [ total ] Consider (x :: zs) to be smaller than (x :: y :: zs)

* Expand RHS metas in totality checking

CHANGELOG_NEXT.md

@@ -74,6 +74,9 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 * The compiler now parses `~x.fun` as unquoting `x` rather than `x.fun`
   and `~(f 5).fun` as unquoting `(f 5)` rather than `(f 5).fun`.
 
+* Totality checking will now look under data constructors, so `Just xs` will
+  be considered smaller than `Just (x :: xs)`.
+
 * LHS of `with`-applications are parsed as `PWithApp` instead of `PApp`. As a
   consequence, `IWithApp` appears in `TTImp` values in elaborator scripts instead
   of `IApp`, as it should have been.

src/Core/Termination/CallGraph.idr

@@ -1,11 +1,13 @@
 module Core.Termination.CallGraph
 
+import Core.Case.CaseTree
 import Core.Context
 import Core.Context.Log
 import Core.Env
 import Core.Normalise
 import Core.Value
 
+import Libraries.Data.IntMap
 import Libraries.Data.SparseMatrix
 
 import Data.String
@@ -134,56 +136,100 @@ mutual
                     else pure $ Ref fc Func n
         conIfGuarded tm = pure tm
 
-  knownOr : SizeChange -> Lazy SizeChange -> SizeChange
-  knownOr Unknown y = y
-  knownOr x _ = x
+  knownOr : Core SizeChange -> Core SizeChange -> Core SizeChange
+  knownOr x y = case !x of Unknown => y; _ => x
 
-  plusLazy : SizeChange -> Lazy SizeChange -> SizeChange
-  plusLazy Smaller _ = Smaller
-  plusLazy x y = x |+| y
+  plusLazy : Core SizeChange -> Core SizeChange -> Core SizeChange
+  plusLazy x y = case !x of Smaller => pure Smaller; x => pure $ x |+| !y
 
   -- Return whether first argument is structurally smaller than the second.
-  sizeCompare : Term vars -> -- RHS: term we're checking
+  sizeCompare : {auto defs : Defs} ->
+                Term vars -> -- RHS: term we're checking
                 Term vars -> -- LHS: argument it might be smaller than
-                SizeChange
+                Core SizeChange
 
-  sizeCompareCon : Term vars -> Term vars -> Bool
-  sizeCompareConArgs : Term vars -> List (Term vars) -> Bool
-  sizeCompareApp : Term vars -> Term vars -> SizeChange
+  sizeCompareCon : {auto defs : Defs} -> Term vars -> Term vars -> Core Bool
+  sizeCompareTyCon : {auto defs : Defs} -> Term vars -> Term vars -> Bool
+  sizeCompareConArgs : {auto defs : Defs} -> Term vars -> List (Term vars) -> Core Bool
+  sizeCompareApp : {auto defs : Defs} -> Term vars -> Term vars -> Core SizeChange
 
   sizeCompare s (Erased _ (Dotted t)) = sizeCompare s t
-  sizeCompare _ (Erased _ _) = Unknown -- incomparable!
+  sizeCompare _ (Erased _ _) = pure Unknown -- incomparable!
   -- for an as pattern, it's smaller if it's smaller than either part
   sizeCompare s (As _ _ p t)
       = knownOr (sizeCompare s p) (sizeCompare s t)
   sizeCompare (As _ _ p s) t
       = knownOr (sizeCompare p t) (sizeCompare s t)
+  -- if they're both metas, let sizeEq check if they're the same
+  sizeCompare s@(Meta _ _ _ _) t@(Meta _ _ _ _) = pure (if sizeEq s t then Same else Unknown)
+  -- otherwise try to expand RHS meta
+  sizeCompare s@(Meta n _ i args) t = do
+    Just gdef <- lookupCtxtExact (Resolved i) (gamma defs) | _ => pure Unknown
+    let (PMDef _ [] (STerm _ tm) _ _) = definition gdef | _ => pure Unknown
+    tm <- substMeta (embed tm) args zero []
+    sizeCompare tm t
+    where
+      substMeta : {0 drop, vs : _} ->
+                  Term (drop ++ vs) -> List (Term vs) ->
+                  SizeOf drop -> SubstEnv drop vs ->
+                  Core (Term vs)
+      substMeta (Bind bfc n (Lam _ c e ty) sc) (a :: as) drop env
+          = substMeta sc as (suc drop) (a :: env)
+      substMeta (Bind bfc n (Let _ c val ty) sc) as drop env
+          = substMeta (subst val sc) as drop env
+      substMeta rhs [] drop env = pure (substs drop env rhs)
+      substMeta rhs _ _ _ = throw (InternalError ("Badly formed metavar solution \{show n}"))
+
   sizeCompare s t
-     = if sizeCompareCon s t
-          then Smaller
-          else knownOr (sizeCompareApp s t) (if sizeEq s t then Same else Unknown)
+     = if sizeCompareTyCon s t then pure Same
+       else if !(sizeCompareCon s t)
+          then pure Smaller
+          else knownOr (sizeCompareApp s t) (pure $ if sizeEq s t then Same else Unknown)
+
+  -- consider two types the same size
+  sizeCompareTyCon s t =
+    let (f, args) = getFnArgs t in
+    let (g, args') = getFnArgs s in
+    case f of
+      Ref _ (TyCon _ _) cn => case g of
+        Ref _ (TyCon _ _) cn' => cn == cn'
+        _ => False
+      _ => False
 
   sizeCompareCon s t
       = let (f, args) = getFnArgs t in
         case f of
-             Ref _ (DataCon t a) cn => sizeCompareConArgs s args
-             _ => False
-
-  sizeCompareConArgs s [] = False
+             Ref _ (DataCon t a) cn =>
+                -- if s is smaller or equal to an arg, then it is smaller than t
+                if !(sizeCompareConArgs s args) then pure True
+                else let (g, args') = getFnArgs s in
+                    case g of
+                        Ref _ (DataCon t' a') cn' =>
+                                -- if s is a matching DataCon, applied to same number of args,
+                                -- no Unknown args, and at least one Smaller
+                                if cn == cn' && length args == length args'
+                                  then do
+                                       sizes <- traverse (uncurry sizeCompare) (zip args' args)
+                                       pure $ Smaller == foldl (|*|) Same sizes
+                                  else pure False
+                        _ => pure $ False
+             _ => pure False
+
+  sizeCompareConArgs s [] = pure False
   sizeCompareConArgs s (t :: ts)
-      = case sizeCompare s t of
+      = case !(sizeCompare s t) of
           Unknown => sizeCompareConArgs s ts
-          _ => True
+          _ => pure True
 
   sizeCompareApp (App _ f _) t = sizeCompare f t
-  sizeCompareApp _ t = Unknown
+  sizeCompareApp _ t = pure Unknown
 
-  sizeCompareAsserted : Maybe (Term vars) -> Term vars -> SizeChange
+  sizeCompareAsserted : {auto defs : Defs} -> Maybe (Term vars) -> Term vars -> Core SizeChange
   sizeCompareAsserted (Just s) t
-      = case sizeCompare s t of
+      = pure $ case !(sizeCompare s t) of
           Unknown => Unknown
           _ => Smaller
-  sizeCompareAsserted Nothing _ = Unknown
+  sizeCompareAsserted Nothing _ = pure Unknown
 
   -- if the argument is an 'assert_smaller', return the thing it's smaller than
   asserted : Name -> Term vars -> Maybe (Term vars)
@@ -200,9 +246,9 @@ mutual
   mkChange : Defs -> Name ->
              (pats : List (Term vars)) ->
              (arg : Term vars) ->
-             List SizeChange
+             Core (List SizeChange)
   mkChange defs aSmaller pats arg
-    = map (\p => plusLazy (sizeCompareAsserted (asserted aSmaller arg) p) (sizeCompare arg p)) pats
+    = traverse (\p => plusLazy (sizeCompareAsserted (asserted aSmaller arg) p) (sizeCompare arg p)) pats
 
   -- Given a name of a case function, and a list of the arguments being
   -- passed to it, update the pattern list so that it's referring to the LHS
@@ -310,7 +356,7 @@ mutual
               (do scs <- traverse (findSC defs env g pats) args
                   pure ([MkSCCall fn
                            (fromListList
-                                (map (mkChange defs aSmaller pats) args))
+                                !(traverse (mkChange defs aSmaller pats) args))
                            fc]
                            ++ concat scs))
 

tests/idris2/total/total004/expected

@@ -6,7 +6,7 @@ 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> Main.pfoom is total
 Main> Main.even is total
 Main> Main.vtrans is possibly not terminating due to recursive path Main.vtrans -> Main.vtrans
 Main> Main.GTree is total

tests/idris2/total/total025/Issue3317.idr

@@ -0,0 +1,5 @@
+total
+f : (a, List a) -> ()
+f (_, []) = ()
+f (x, _::xs) = f (x, xs)
+

tests/idris2/total/total025/Totality.idr

@@ -0,0 +1,38 @@
+%default total
+
+-- This one needed withHoles on tcOnly (instead of withArgHoles)
+-- or the solved implicit for the (ty : Type) on Maybe would not be
+-- substituted.
+length : Maybe (List a) -> Nat
+length Nothing = 0
+length (Just []) = 0
+length (Just (x :: xs)) = 1 + length (Just xs)
+
+one : List a -> Nat
+one (x :: y :: zs) = one (x :: zs)
+one _ = 0
+
+two : List a -> Nat
+two (a :: b :: c :: d :: es) = two (a :: c :: es)
+two _ = 0
+
+three : List a -> Nat
+three (a :: b :: c :: d :: es) = three (b :: c :: es)
+three _ = 0
+
+failing "not total"
+  four : List Nat -> Nat
+  four (a :: b :: c :: es) = four (b :: c :: a :: es)
+  four _ = 0
+
+-- also needs withHoles
+five : (List a, List a) -> List a
+five (a :: as, bs) = a :: five (as, bs)
+five ([], _) = []
+
+-- This is total, but not supported
+failing "not total"
+  six : (List a, List a) -> List a
+  six (a :: as, bs) = a :: six (bs, as)
+  six ([], _) = []
+

tests/idris2/total/total025/expected

@@ -0,0 +1,2 @@
+1/1: Building Issue3317 (Issue3317.idr)
+1/1: Building Totality (Totality.idr)

tests/idris2/total/total025/run

@@ -0,0 +1,4 @@
+. ../../../testutils.sh
+
+idris2 --check Issue3317.idr
+idris2 --check Totality.idr

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
+Yaffle> Main.pfoom is total
 Yaffle> Bye for now!