Detect nested patterns as smaller in the termination checker (#1524)

src/Juvix/Compiler/Abstract/Extra/Functions.hs

@@ -34,12 +34,26 @@ idenName = \case
   IdenInductive (InductiveRef i) -> i
   IdenAxiom (AxiomRef a) -> a
 
-smallerPatternVariables :: Traversal' Pattern VarName
-smallerPatternVariables f p = case p of
+-- | A fold over all transitive children, including self
+patternCosmos :: SimpleFold Pattern Pattern
+patternCosmos f p = case p of
+  PatternVariable {} -> f p
+  PatternWildcard {} -> f p
+  PatternEmpty {} -> f p
+  PatternConstructorApp (ConstructorApp r args) ->
+    f p *> do
+      args' <- traverse (traverseOf patternArgPattern (patternCosmos f)) args
+      pure (PatternConstructorApp (ConstructorApp r args'))
+
+-- | A fold over all transitive children, excluding self
+patternSubCosmos :: SimpleFold Pattern Pattern
+patternSubCosmos f p = case p of
   PatternVariable {} -> pure p
   PatternWildcard {} -> pure p
   PatternEmpty {} -> pure p
-  PatternConstructorApp app -> PatternConstructorApp <$> appVariables f app
+  PatternConstructorApp (ConstructorApp r args) -> do
+    args' <- traverse (traverseOf patternArgPattern (patternCosmos f)) args
+    pure (PatternConstructorApp (ConstructorApp r args'))
 
 viewApp :: Expression -> (Expression, [ApplicationArg])
 viewApp e =

src/Juvix/Compiler/Internal/Translation/FromAbstract/Analysis/Termination/Data/SizeInfo.hs

@@ -1,13 +1,12 @@
 module Juvix.Compiler.Internal.Translation.FromAbstract.Analysis.Termination.Data.SizeInfo where
 
-import Data.HashMap.Strict qualified as HashMap
 import Juvix.Compiler.Abstract.Extra
 import Juvix.Prelude
 
 -- | i = SizeInfo [v] ⇔ v is smaller than argument i of the caller function.
 -- Indexes are 0 based
 data SizeInfo = SizeInfo
-  { _sizeSmaller :: HashMap VarName Int,
+  { _sizeSmaller :: [[Pattern]],
     _sizeEqual :: [Pattern]
   }
 
@@ -21,15 +20,12 @@ emptySizeInfo =
     }
 
 mkSizeInfo :: [PatternArg] -> SizeInfo
-mkSizeInfo ps = SizeInfo {..}
+mkSizeInfo args = SizeInfo {..}
   where
-    ps' :: [Pattern]
-    ps' = map (^. patternArgPattern) (filter (not . isBrace) ps)
+    ps :: [Pattern]
+    ps = map (^. patternArgPattern) (filter (not . isBrace) args)
     isBrace :: PatternArg -> Bool
     isBrace = (== Implicit) . (^. patternArgIsImplicit)
-    _sizeEqual = map (^. patternArgPattern) ps
-    _sizeSmaller :: HashMap VarName Int
-    _sizeSmaller =
-      HashMap.fromList
-        [ (v, i) | (i, p) <- zip [0 ..] ps', v <- p ^.. smallerPatternVariables
-        ]
+    _sizeEqual = ps
+    _sizeSmaller :: [[Pattern]]
+    _sizeSmaller = map (^.. patternSubCosmos) ps

src/Juvix/Compiler/Internal/Translation/FromAbstract/Analysis/Termination/FunctionCall.hs

@@ -22,20 +22,20 @@ viewCall = \case
     where
       callArg :: Sem r (CallRow, Expression)
       callArg = do
-        lt <- lessThan
-        eq <- equalTo
-        return (CallRow ((lt ^. callRow) `mplus` (eq ^. callRow)), x)
+        lt <- (^. callRow) <$> lessThan
+        eq <- (^. callRow) <$> equalTo
+        return (CallRow (lt `mplus` eq), x)
         where
           lessThan :: Sem r CallRow
-          lessThan = case x of
-            ExpressionIden (IdenVar v) -> do
-              s :: Maybe Int <- asks (HashMap.lookup v . (^. sizeSmaller))
+          lessThan = case viewExpressionAsPattern x of
+            Nothing -> return (CallRow Nothing)
+            Just x' -> do
+              s <- asks (findIndex (elem x') . (^. sizeSmaller))
               return $ case s of
                 Nothing -> CallRow Nothing
                 Just s' -> CallRow (Just (s', RLe))
-            _ -> return (CallRow Nothing)
           equalTo :: Sem r CallRow
-          equalTo = do
+          equalTo =
             case viewExpressionAsPattern x of
               Just x' -> do
                 s <- asks (elemIndex x' . (^. sizeEqual))

test/Termination/Positive.hs

@@ -53,6 +53,7 @@ testDescrFlag N.NegTest {..} =
 tests :: [PosTest]
 tests =
   [ PosTest "Ackerman nice def. is terminating" "." "Ack.juvix",
+    PosTest "Fibonacci with nested pattern" "." "Fib.juvix",
     PosTest "Recursive functions on Lists" "." "Data/List.juvix"
   ]
 

tests/positive/Termination/Fib.juvix

@@ -0,0 +1,18 @@
+module Fib;
+
+inductive Nat {
+  zero : Nat;
+  suc : Nat → Nat;
+};
+
+infixl 6 +;
++ : Nat → Nat → Nat;
++ zero b ≔ b;
++ (suc a) b ≔ suc (a + b);
+
+fib : Nat -> Nat;
+fib zero := zero;
+fib (suc (zero)) := suc zero;
+fib (suc (suc n)) := fib (suc n) + fib n;
+
+end;