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

CHANGELOG_NEXT.md

@@ -92,6 +92,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.

docs/source/reference/pragmas.rst

@@ -62,6 +62,13 @@ definition.
 Set how deep nested ambiguous names can be before Idris gives up. The default is 3, increashing this
 will effect compiler performance. For more details, see :ref:`ambiguous-name-resolution`.
 
+``%totality_depth``
+-------------------
+
+Set the number of matching constructors Idris will look under when checking totality.  For instance
+`Just xs` is smaller than `Just (x :: xs)` if Idris looks under the matching constructor. The default
+value is 5.  Increasing the value may slow down totality checking.
+
 ``%auto_implicit_depth``
 ------------------------
 

src/Core/Context.idr

@@ -2252,6 +2252,11 @@ setAmbigLimit : {auto c : Ref Ctxt Defs} ->
                 Nat -> Core ()
 setAmbigLimit max = update Ctxt { options->elabDirectives->ambigLimit := max }
 
+export
+setTotalLimit : {auto c : Ref Ctxt Defs} ->
+                Nat -> Core ()
+setTotalLimit max = update Ctxt { options->elabDirectives->totalLimit := max }
+
 export
 setAutoImplicitLimit : {auto c : Ref Ctxt Defs} ->
                        Nat -> Core ()

src/Core/Options.idr

@@ -127,6 +127,7 @@ record ElabDirectives where
   ambigLimit : Nat
   autoImplicitLimit : Nat
   nfThreshold : Nat
+  totalLimit : Nat
   --
   -- produce traditional (prefix) record projections,
   -- in addition to postfix (dot) projections
@@ -232,7 +233,7 @@ defaultSession = MkSessionOpts False CoveringOnly False False Chez [] 1000 False
 
 export
 defaultElab : ElabDirectives
-defaultElab = MkElabDirectives True True CoveringOnly 3 50 25 True
+defaultElab = MkElabDirectives True True CoveringOnly 3 50 25 5 True
 
 -- FIXME: This turns out not to be reliably portable, since different systems
 -- may have tools with the same name but different required arugments. We

src/Core/Termination/CallGraph.idr

@@ -1,11 +1,14 @@
 module Core.Termination.CallGraph
 
+import Core.Case.CaseTree
 import Core.Context
 import Core.Context.Log
 import Core.Env
 import Core.Normalise
+import Core.Options
 import Core.Value
 
+import Libraries.Data.IntMap
 import Libraries.Data.SparseMatrix
 
 import Data.String
@@ -134,56 +137,108 @@ 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} ->
+                Nat -> -- backtracking fuel
+                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} -> Nat -> Term vars -> Term vars -> Core Bool
+  sizeCompareTyCon : {auto defs : Defs} -> Nat -> Term vars -> Term vars -> Core Bool
+  sizeCompareConArgs : {auto defs : Defs} -> Nat -> Term vars -> List (Term vars) -> Core Bool
+  sizeCompareApp : {auto defs : Defs} -> Nat -> Term vars -> Term vars -> Core SizeChange
 
-  sizeCompare s (Erased _ (Dotted t)) = sizeCompare s t
-  sizeCompare _ (Erased _ _) = Unknown -- incomparable!
+  sizeCompare fuel s (Erased _ (Dotted t)) = sizeCompare fuel s t
+  sizeCompare fuel _ (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)
-  sizeCompare s t
-     = if sizeCompareCon s t
-          then Smaller
-          else knownOr (sizeCompareApp s t) (if sizeEq s t then Same else Unknown)
-
-  sizeCompareCon s t
+  sizeCompare fuel s (As _ _ p t)
+      = knownOr (sizeCompare fuel s p) (sizeCompare fuel s t)
+  sizeCompare fuel (As _ _ p s) t
+      = knownOr (sizeCompare fuel p t) (sizeCompare fuel s t)
+  -- if they're both metas, let sizeEq check if they're the same
+  sizeCompare fuel s@(Meta _ _ _ _) t@(Meta _ _ _ _) = pure (if sizeEq s t then Same else Unknown)
+  -- otherwise try to expand RHS meta
+  sizeCompare fuel 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 fuel 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 fuel s t
+     = if !(sizeCompareTyCon fuel s t) then pure Same
+       else if !(sizeCompareCon fuel s t)
+          then pure Smaller
+          else knownOr (sizeCompareApp fuel s t) (pure $ if sizeEq s t then Same else Unknown)
+
+  sizeCompareProdConArgs : {auto defs : Defs} -> Nat -> List (Term vars) -> List (Term vars) -> Core SizeChange
+  sizeCompareProdConArgs _ [] [] = pure Same
+  sizeCompareProdConArgs fuel (x :: xs) (y :: ys) =
+    case !(sizeCompare fuel x y) of
+      Unknown => pure Unknown
+      t => (t |*|) <$> sizeCompareProdConArgs fuel xs ys
+  sizeCompareProdConArgs _ _ _ = pure Unknown
+
+  sizeCompareTyCon fuel 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' => if cn == cn'
+            then (Unknown /=) <$> sizeCompareProdConArgs fuel args' args
+            else pure False
+        _ => pure False
+      _ => pure False
+
+  sizeCompareCon fuel s t
       = let (f, args) = getFnArgs t in
         case f of
-             Ref _ (DataCon t a) cn => sizeCompareConArgs s args
-             _ => False
-
-  sizeCompareConArgs s [] = False
-  sizeCompareConArgs s (t :: ts)
-      = case sizeCompare s t of
-          Unknown => sizeCompareConArgs s ts
-          _ => True
-
-  sizeCompareApp (App _ f _) t = sizeCompare f t
-  sizeCompareApp _ t = Unknown
-
-  sizeCompareAsserted : Maybe (Term vars) -> Term vars -> SizeChange
-  sizeCompareAsserted (Just s) t
-      = case sizeCompare s t of
+             Ref _ (DataCon t a) cn =>
+                -- if s is smaller or equal to an arg, then it is smaller than t
+                if !(sizeCompareConArgs (minus fuel 1) s args) then pure True
+                else let (g, args') = getFnArgs s in
+                    case (fuel, g) of
+                        (S k, Ref _ (DataCon t' a') cn') => do
+                                -- 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 (Smaller ==) <$> sizeCompareProdConArgs k args' args
+                                  else pure False
+                        _ => pure $ False
+             _ => pure False
+
+  sizeCompareConArgs _ s [] = pure False
+  sizeCompareConArgs fuel s (t :: ts)
+      = case !(sizeCompare fuel s t) of
+          Unknown => sizeCompareConArgs fuel s ts
+          _ => pure True
+
+  sizeCompareApp fuel (App _ f _) t = sizeCompare fuel f t
+  sizeCompareApp _ _ t = pure Unknown
+
+  sizeCompareAsserted : {auto defs : Defs} -> Nat -> Maybe (Term vars) -> Term vars -> Core SizeChange
+  sizeCompareAsserted fuel (Just s) t
+      = pure $ case !(sizeCompare fuel 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 +255,10 @@ 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
+    = let fuel = defs.options.elabDirectives.totalLimit
+      in traverse (\p => plusLazy (sizeCompareAsserted fuel (asserted aSmaller arg) p) (sizeCompare fuel 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 +366,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))
 

src/Idris/Desugar.idr

@@ -1321,6 +1321,7 @@ mutual
              PrefixRecordProjections b => do
                pure [IPragma fc [] (\nest, env => setPrefixRecordProjections b)]
              AmbigDepth n => pure [IPragma fc [] (\nest, env => setAmbigLimit n)]
+             TotalityDepth n => pure [IPragma fc [] (\next, env => setTotalLimit n)]
              AutoImplicitDepth n => pure [IPragma fc [] (\nest, env => setAutoImplicitLimit n)]
              NFMetavarThreshold n => pure [IPragma fc [] (\nest, env => setNFThreshold n)]
              SearchTimeout n => pure [IPragma fc [] (\nest, env => setSearchTimeout n)]

src/Idris/Parser.idr

@@ -1471,6 +1471,10 @@ directive fname indents
          b <- onoff
          atEnd indents
          pure (PrefixRecordProjections b)
+  <|> do decoratedPragma fname "totality_depth"
+         lvl <- decorate fname Keyword $ intLit
+         atEnd indents
+         pure (TotalityDepth (fromInteger lvl))
   <|> do decoratedPragma fname "ambiguity_depth"
          lvl <- decorate fname Keyword $ intLit
          atEnd indents

src/Idris/Syntax.idr

@@ -370,6 +370,7 @@ mutual
        LazyOn : Bool -> Directive
        UnboundImplicits : Bool -> Directive
        AmbigDepth : Nat -> Directive
+       TotalityDepth: Nat -> Directive
        PairNames : Name -> Name -> Name -> Directive
        RewriteName : Name -> Name -> Directive
        PrimInteger : Name -> Directive

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/Issue3353.idr

@@ -0,0 +1,12 @@
+import Data.Fin
+
+covering
+g : Fin 64 -> Unit
+g FZ      = ()
+g (FS i') = g $ weaken i'
+
+total
+g' : Fin 64 -> Unit
+g' FZ        = ()
+g' i@(FS i') = g' $ assert_smaller i $ weaken i'
+

tests/idris2/total/total025/Pragma.idr

@@ -0,0 +1,14 @@
+%default total
+
+%totality_depth 1
+
+failing "not total"
+  one : List a -> Nat
+  one (a :: b :: c :: es) = one (a :: b :: es)
+  one _ = 0
+
+%totality_depth 3
+
+two : List a -> Nat
+two (a :: b :: c :: es) = two (a :: b :: es)
+two _ = 0

tests/idris2/total/total025/Totality.idr

@@ -0,0 +1,50 @@
+%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 ([], _) = []
+
+
+failing "not total"
+  -- If we didn't check all of the arguments of MkTuple for
+  -- Same/Smaller, then this would be incorrectly accepted as total
+  first : (List Nat, List Nat) -> Nat
+  second : (List Nat, List Nat) -> Nat
+
+  first (x :: xs, ys) = second (xs, Z :: ys)
+  first _ = Z
+
+  second (xs, y :: ys) = first (1 :: xs, ys)
+  second _ = Z

tests/idris2/total/total025/expected

@@ -0,0 +1,4 @@
+1/1: Building Issue3317 (Issue3317.idr)
+1/1: Building Totality (Totality.idr)
+1/1: Building Issue3353 (Issue3353.idr)
+1/1: Building Pragma (Pragma.idr)

tests/idris2/total/total025/run

@@ -0,0 +1,6 @@
+. ../../../testutils.sh
+
+idris2 --check Issue3317.idr
+idris2 --check Totality.idr
+idris2 --check Issue3353.idr
+idris2 --check Pragma.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!