Fix termination with as-patterns (#1787)

src/Juvix/Compiler/Abstract/Data/Name.hs

@@ -51,10 +51,7 @@ instance HasNameKind Name where
   getNameKind = (^. nameKind)
 
 instance Pretty Name where
-  pretty n =
-    pretty (n ^. namePretty)
-      <> "@"
-      <> pretty (n ^. nameId)
+  pretty n = pretty (n ^. namePretty)
 
 addNameIdTag :: Bool -> NameId -> Doc a -> Doc a
 addNameIdTag showNameId nid

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

@@ -45,6 +45,20 @@ patternCosmos f p = case p of
       args' <- traverse (traverseOf patternArgPattern (patternCosmos f)) args
       pure (PatternConstructorApp (ConstructorApp r args'))
 
+patternArgNameFold :: SimpleFold (Maybe Name) Pattern
+patternArgNameFold f = \case
+  Nothing -> mempty
+  Just n -> Const (getConst (f (PatternVariable n)))
+
+-- | A fold over all transitive children, including self
+patternArgCosmos :: SimpleFold PatternArg Pattern
+patternArgCosmos f p = do
+  _patternArgPattern <- patternCosmos f (p ^. patternArgPattern)
+  _patternArgName <- patternArgNameFold f (p ^. patternArgName)
+  pure PatternArg {..}
+  where
+    _patternArgIsImplicit = p ^. patternArgIsImplicit
+
 -- | A fold over all transitive children, excluding self
 patternSubCosmos :: SimpleFold Pattern Pattern
 patternSubCosmos f p = case p of
@@ -52,7 +66,7 @@ patternSubCosmos f p = case p of
   PatternWildcard {} -> pure p
   PatternEmpty {} -> pure p
   PatternConstructorApp (ConstructorApp r args) -> do
-    args' <- traverse (traverseOf patternArgPattern (patternCosmos f)) args
+    args' <- traverse (patternArgCosmos f) args
     pure (PatternConstructorApp (ConstructorApp r args'))
 
 viewApp :: Expression -> (Expression, [ApplicationArg])

src/Juvix/Compiler/Internal/Translation/FromAbstract/Analysis/Termination/Error/Types.hs

@@ -24,7 +24,7 @@ instance ToGenericError NoLexOrder where
       i = getLoc name
 
       msg :: Doc Ann
-      msg =
+      msg = do
         "The function"
           <+> code (pretty name)
           <+> "fails the termination checker."

test/Termination/Positive.hs

@@ -50,8 +50,6 @@ testDescrFlag N.NegTest {..} =
             (void . runIO' iniState entryPoint) upToInternal
         }
 
---------------------------------------------------------------------------------
-
 tests :: [PosTest]
 tests =
   [ PosTest
@@ -65,7 +63,11 @@ tests =
     PosTest
       "Recursive functions on Lists"
       $(mkRelDir ".")
-      $(mkRelFile "Data/List.juvix")
+      $(mkRelFile "Data/List.juvix"),
+    PosTest
+      "Recursive function on a tree"
+      $(mkRelDir ".")
+      $(mkRelFile "TreeGen.juvix")
   ]
 
 testsWithKeyword :: [PosTest]
@@ -83,8 +85,6 @@ testsWithKeyword =
 negTests :: [N.NegTest]
 negTests = N.tests
 
---------------------------------------------------------------------------------
-
 allTests :: TestTree
 allTests =
   testGroup

tests/positive/Termination/TreeGen.juvix

@@ -0,0 +1,17 @@
+module TreeGen;
+  open import Stdlib.Prelude;
+
+  type Tree :=
+    | leaf : Tree
+    | node : Tree → Tree → Tree;
+
+  gen : Nat → Tree;
+  gen zero := leaf;
+  gen (suc zero) := node leaf leaf;
+  gen (suc (suc n')) := node (gen n') (gen (suc n'));
+
+  gen2 : Nat → Tree;
+  gen2 zero := leaf;
+  gen2 (suc zero) := node leaf leaf;
+  gen2 (suc n@(suc n')) := node (gen2 n') (gen2 n);
+end;