add negative test

anoma · Aug 29, 2023 · d4340ea · d4340ea
1 parent 218941c
commit d4340ea
Show file tree

Hide file tree

Showing 5 changed files with 13 additions and 3 deletions.
diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs
@@ -752,7 +752,7 @@ instance (SingI s) => PrettyPrint (AxiomDef s) where
       ?<> ppCode _axiomKw
       <+> axiomName'
       <+> ppCode _axiomColonKw
-      <+> ppExpressionType _axiomType
+      <+> nest (ppExpressionType _axiomType)
 
 instance PrettyPrint BuiltinInductive where
   ppCode i = ppCode Kw.kwBuiltin <+> keywordText (P.prettyText i)

diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Error/Types.hs
@@ -335,7 +335,7 @@ instance ToGenericError UnsupportedTypeFunction where
             <+> ppCode opts (_unsupportedTypeFunction ^. funDefName)
               <> "."
               <> line
-              <> "Only functions with a single clause and no pattern matching are supported."
+              <> "Only terminating functions with a single clause and no pattern matching are supported."
     return
       GenericError
         { _genericErrorLoc = i,

diff --git a/test/Termination/Negative.hs b/test/Termination/Negative.hs
@@ -73,6 +73,12 @@ tests =
       "Quicksort is not terminating"
       $(mkRelDir ".")
       $(mkRelFile "Data/QuickSort.juvix")
+      $ \case
+        ErrNoLexOrder {} -> Nothing,
+    NegTest
+      "Loop in axiom type"
+      $(mkRelDir ".")
+      $(mkRelFile "Axiom.juvix")
       $ \case
         ErrNoLexOrder {} -> Nothing
   ]
diff --git a/tests/negative/Termination/Axiom.juvix b/tests/negative/Termination/Axiom.juvix
@@ -0,0 +1,5 @@
+module Axiom;
+
+axiom A : let
+    x : Type := x;
+  in x;
diff --git a/tests/negative/Termination/Ord.juvix b/tests/negative/Termination/Ord.juvix
@@ -17,4 +17,3 @@ addord : Ord -> Ord -> Ord
 aux-addord : (ℕ -> Ord) -> Ord -> ℕ -> Ord
 
   | f y z := addord (f z) y;
-
Original file line number	Diff line number	Diff line change
Expand Up		@@ -17,4 +17,3 @@ addord : Ord -> Ord -> Ord
		aux-addord : (ℕ -> Ord) -> Ord -> ℕ -> Ord

		\| f y z := addord (f z) y;