fix internal to core tests

anoma · Dec 19, 2023 · 21f0e9d · 21f0e9d
1 parent 858d1e1
commit 21f0e9d
Show file tree

Hide file tree

Showing 28 changed files with 44 additions and 43 deletions.
diff --git a/test/Internal/Eval/Base.hs b/test/Internal/Eval/Base.hs
@@ -16,7 +16,7 @@ internalCoreAssertion :: Path Abs Dir -> Path Abs File -> Path Abs File -> (Stri
 internalCoreAssertion root' mainFile expectedFile step = do
   step "Translate to Core"
   entryPoint <- testDefaultEntryPointIO root' mainFile
-  PipelineResult r _ <- snd <$> testRunIO entryPoint upToCore
+  PipelineResult r _ <- snd <$> testRunIO entryPoint upToStoredCore
   let m = etaExpansionApps (r ^. Core.coreResultModule)
       tab = computeCombinedInfoTable m
   case (tab ^. infoMain) >>= ((tab ^. identContext) HashMap.!?) of

diff --git a/tests/Internal/Core/positive/out/test006.out b/tests/Internal/Core/positive/out/test006.out
@@ -1 +1 @@
-suc (suc zero)
+2
diff --git a/tests/Internal/Core/positive/out/test011.out b/tests/Internal/Core/positive/out/test011.out
@@ -1 +1 @@
-suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))))))))))))))))))))))))))))
+34
diff --git a/tests/Internal/positive/AsPatterns.juvix b/tests/Internal/positive/AsPatterns.juvix
@@ -16,13 +16,16 @@ f2 : List Nat -> List Nat
   | _ := nil;
 
 f3 : Nat -> List Nat -> List Nat
-  | _ a@(x :: x' :: xs) := a;
+  | _ a@(x :: x' :: xs) := a
+  | _ _ := nil;
 
 f4 : Nat -> List Nat -> Nat
-  | y (x :: a@(x' :: xs)) := y;
+  | y (x :: a@(x' :: xs)) := y
+  | _ _ := zero;
 
 f5 : List Nat -> List Nat -> List Nat
-  | (x :: a@(x' :: xs)) (y :: b@(y' :: ys)) := b;
+  | (x :: a@(x' :: xs)) (y :: b@(y' :: ys)) := b
+  | a b := a;
 
 l1 : List Nat := zero :: suc zero :: nil;
 

diff --git a/tests/Internal/positive/BuiltinInductive.juvix b/tests/Internal/positive/BuiltinInductive.juvix
@@ -1,7 +1,5 @@
 module BuiltinInductive;
 
-builtin string
-axiom MyString : Type;
+type MyString := str;
 
 main : Type := MyString;
-
diff --git a/tests/Internal/positive/FunctionType.juvix b/tests/Internal/positive/FunctionType.juvix
@@ -1,7 +1,7 @@
 module FunctionType;
 
-type A :=
-  | a : A;
+type A' :=
+  | a : A';
 
 main : Type := (A : Type) -> (B : Type) -> A -> B;
 
diff --git a/tests/Internal/positive/IdenFunctionArgs.juvix b/tests/Internal/positive/IdenFunctionArgs.juvix
@@ -6,4 +6,3 @@ f : Nat → Nat → Nat
   | x y := x;
 
 main : Nat := f 100 200;
-
diff --git a/tests/Internal/positive/IdenFunctionArgsImplicit.juvix b/tests/Internal/positive/IdenFunctionArgsImplicit.juvix
@@ -6,4 +6,3 @@ f : {A : Type} → Nat → A → Nat
   | x y := x;
 
 main : Nat := f 100 200;
-
diff --git a/tests/Internal/positive/Import/out/Importer.out b/tests/Internal/positive/Import/out/Importer.out
@@ -1 +1 @@
-suc zero
+1
diff --git a/tests/Internal/positive/NatMatch1.juvix b/tests/Internal/positive/NatMatch1.juvix
@@ -4,7 +4,8 @@ import Stdlib.Prelude open;
 
 f : Nat → Nat → Nat
   | zero k := 100
-  | (suc n) (suc (suc m)) := m;
+  | (suc n) (suc (suc m)) := m
+  | _ _ := 0;
 
 n : Nat := suc (suc (suc (suc (suc zero))));
 

diff --git a/tests/Internal/positive/NatMatch2.juvix b/tests/Internal/positive/NatMatch2.juvix
@@ -4,7 +4,8 @@ import Stdlib.Prelude open;
 
 f : Nat → Nat → Nat
   | zero k := zero
-  | n (suc (suc m)) := n;
+  | n (suc (suc m)) := n
+  | _ _ := zero;
 
 n : Nat := suc (suc (suc (suc (suc zero))));
 

diff --git a/tests/Internal/positive/PatternArgs.juvix b/tests/Internal/positive/PatternArgs.juvix
@@ -5,8 +5,8 @@ import Stdlib.Prelude open;
 f : Nat -> Nat -> Nat
   | zero zero := zero
   | n1@(suc m1) n2@(suc m2) :=
-    n1 + m1 + suc (suc zero) * (n2 + m2);
+    n1 + m1 + suc (suc zero) * (n2 + m2)
+  | _ _ := zero;
 
 main : IO :=
   printNatLn (f (suc (suc zero)) (suc (suc (suc zero))));
-
diff --git a/tests/Internal/positive/out/AsPatterns.out b/tests/Internal/positive/out/AsPatterns.out
@@ -1,5 +1,5 @@
-zero :: suc zero :: nil
-suc zero :: nil
-zero :: suc zero :: nil
-zero
-suc zero :: suc (suc zero) :: suc (suc (suc zero)) :: nil
+0 :: 1 :: nil
+1 :: nil
+0 :: 1 :: nil
+0
+1 :: 2 :: 3 :: nil
diff --git a/tests/Internal/positive/out/BuiltinAdd.out b/tests/Internal/positive/out/BuiltinAdd.out
@@ -1 +1 @@
-suc (suc (suc zero))
+3
diff --git a/tests/Internal/positive/out/Church.out b/tests/Internal/positive/out/Church.out
@@ -1 +1 @@
-suc zero
+1
diff --git a/tests/Internal/positive/out/HigherOrderLambda.out b/tests/Internal/positive/out/HigherOrderLambda.out
@@ -1 +1 @@
-suc (suc (suc zero))
+3
diff --git a/tests/Internal/positive/out/IdenFunctionArgs.out b/tests/Internal/positive/out/IdenFunctionArgs.out
@@ -1 +1 @@
-suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+100
diff --git a/tests/Internal/positive/out/IdenFunctionArgsImplicit.out b/tests/Internal/positive/out/IdenFunctionArgsImplicit.out
@@ -1 +1 @@
-suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+100
diff --git a/tests/Internal/positive/out/IdenFunctionIntegerLiteral.out b/tests/Internal/positive/out/IdenFunctionIntegerLiteral.out
@@ -1 +1 @@
-suc zero
+1
diff --git a/tests/Internal/positive/out/IntegerLiteral.out b/tests/Internal/positive/out/IntegerLiteral.out
@@ -1 +1 @@
-suc zero
+1
diff --git a/tests/Internal/positive/out/Lambda.out b/tests/Internal/positive/out/Lambda.out
@@ -1,5 +1,5 @@
-zero
-suc (suc zero)
-zero
-suc (suc zero)
-suc (suc (suc (suc (suc (suc zero)))))
+0
+2
+0
+2
+6
diff --git a/tests/Internal/positive/out/LitInteger.out b/tests/Internal/positive/out/LitInteger.out
@@ -1 +1 @@
-suc (suc (suc zero))
+3
diff --git a/tests/Internal/positive/out/LitIntegerToNat.out b/tests/Internal/positive/out/LitIntegerToNat.out
@@ -1,2 +1,2 @@
-suc (suc zero)
-zero
+2
+0
diff --git a/tests/Internal/positive/out/MatchConstructor.out b/tests/Internal/positive/out/MatchConstructor.out
@@ -1 +1 @@
-suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+200
diff --git a/tests/Internal/positive/out/NatMatch1.out b/tests/Internal/positive/out/NatMatch1.out
@@ -1 +1 @@
-suc (suc (suc zero))
+3
diff --git a/tests/Internal/positive/out/NatMatch2.out b/tests/Internal/positive/out/NatMatch2.out
@@ -1 +1 @@
-suc (suc (suc (suc (suc zero))))
+5
diff --git a/tests/Internal/positive/out/PatternArgs.out b/tests/Internal/positive/out/PatternArgs.out
@@ -1 +1 @@
-suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))))))
+13
diff --git a/tests/Internal/positive/out/QuickSort.out b/tests/Internal/positive/out/QuickSort.out
@@ -1 +1 @@
-:: (Nat) (suc (suc zero)) (:: (Nat) (suc (suc (suc zero))) (:: (Nat) (suc (suc (suc (suc zero)))) (:: (Nat) (suc (suc (suc (suc (suc zero))))) (:: (Nat) (suc (suc (suc (suc (suc (suc zero)))))) (:: (Nat) (suc (suc (suc (suc (suc (suc (suc zero))))))) (nil (Nat)))))))
+:: Int 2 (:: Int 3 (:: Int 4 (:: Int 5 (:: Int 6 (:: Int 7 (nil Int))))))