Anoma compilation tests now avoid using Partial/failwith

test/Anoma/Compilation/Positive.hs

@@ -100,7 +100,7 @@ allTests =
         []
         $ do
           let l :: Term Natural = [nock| [1 2 nil] |]
-          checkOutput [[nock| false |], [nock| true |], [nock| 0 |], [nock| [1 nil] |], [nock| 1 |], l, l, l],
+          checkOutput [[nock| false |], [nock| true |], [nock| 0 |], [nock| [1 nil] |], [nock| 1 |], l, l],
       mkAnomaCallTest
         "Test008: Recursion"
         $(mkRelDir ".")
@@ -391,7 +391,7 @@ allTests =
         $(mkRelDir ".")
         $(mkRelFile "test052.juvix")
         []
-        $ checkNatOutput [15],
+        $ checkOutput [[nock| [15 nil] |]],
       mkAnomaCallTest
         "Test053: Inlining"
         $(mkRelDir ".")

tests/Anoma/Compilation/positive/test007.juvix

@@ -10,9 +10,11 @@ map' {A B} (f : A → B) : List A → List B :=
     | (h :: t) := f h :: map' f t
   };
 
-terminating
-map'' {A B} {{Partial}} (f : A → B) (x : List A) : List B :=
-  if (null x) nil (f (phead x) :: map'' f (tail x));
+
+-- TODO: Restore when anoma backend supports strings
+-- terminating
+-- map'' {A B} {{Partial}} (f : A → B) (x : List A) : List B :=
+--   if (null x) nil (f (phead x) :: map'' f (tail x));
 
 lst : List Nat := 0 :: 1 :: nil;
 
@@ -23,5 +25,6 @@ main : List Nat :=
     >>> trace (tail lst)
     >>> trace (head 0 (tail lst))
     >>> trace (map ((+) 1) lst)
-    >>> trace (map' ((+) 1) lst)
-    >>> runPartial λ {{{_}} := map'' ((+) 1) lst};
+    >>> map' ((+) 1) lst
+    -- TODO: Restore when anoma backend supports strings
+    -- >>> runPartial λ {{{_}} := map'' ((+) 1) lst};

tests/Anoma/Compilation/positive/test026.juvix

@@ -3,53 +3,77 @@ module test026;
 
 import Stdlib.Prelude open;
 
-type Queue (A : Type) :=
-  | queue : List A → List A → Queue A;
+type Queue (A : Type) := queue : List A → List A → Queue A;
 
 qfst : {A : Type} → Queue A → List A
   | (queue x _) := x;
 
 qsnd : {A : Type} → Queue A → List A
   | (queue _ x) := x;
 
-front {{Partial}} : {A : Type} → Queue A → A
-  | q := phead (qfst q);
+last {A} : List A -> Maybe A
+  | nil := nothing
+  | [x] := just x
+  | (_ :: t) := last t;
 
-pop_front : {A : Type} → Queue A → Queue A
+front : {A : Type} → Queue A → Maybe A
+  | q :=
+    case qfst q of {
+      | nil := last (qsnd q)
+      | x :: _ := just x
+    };
+
+drop_front : {A : Type} → Queue A → Queue A
   | {A} q :=
     let
       q' : Queue A := queue (tail (qfst q)) (qsnd q);
-    in case qfst q'
-      | nil := queue (reverse (qsnd q')) nil
-      | _ := q';
+    in case qfst q' of {
+         | nil := queue (reverse (qsnd q')) nil
+         | _ := q'
+       };
+
+pop_front {A} : Queue A -> Maybe (A × Queue A)
+  | (queue xs ys) :=
+    case xs of {
+      | h :: t := just (h, queue t ys)
+      | [] :=
+        case reverse ys of {
+          | h :: t := just (h, queue t [])
+          | [] := nothing
+        }
+    };
 
 push_back : {A : Type} → Queue A → A → Queue A
   | q x :=
-    case qfst q
+    case qfst q of {
       | nil := queue (x :: nil) (qsnd q)
-      | q' := queue q' (x :: qsnd q);
+      | q' := queue q' (x :: qsnd q)
+    };
 
 is_empty : {A : Type} → Queue A → Bool
   | q :=
-    case qfst q
+    case qfst q of {
       | nil :=
-        (case qsnd q
+        case qsnd q of {
           | nil := true
-          | _ := false)
-      | _ := false;
+          | _ := false
+        }
+      | _ := false
+    };
 
 empty : {A : Type} → Queue A := queue nil nil;
 
 terminating
-g {{Partial}} : List Nat → Queue Nat → List Nat
+g : List Nat → Queue Nat → List Nat
   | acc q :=
-    if (is_empty q) acc (g (front q :: acc) (pop_front q));
+    case pop_front q of {
+      | nothing := acc
+      | just (h, q') := g (h :: acc) q'
+    };
 
--- TODO: remove `terminating` after fixing https://github.com/anoma/juvix/issues/2414
-terminating
-f {{Partial}} : Nat → Queue Nat → List Nat
+f : Nat → Queue Nat → List Nat
   | zero q := g nil q
   | n@(suc n') q := f n' (push_back q n);
 
-main : List Nat := runPartial (λ {{{_}} := f 100 empty});
+main : List Nat := f 100 empty;
 -- list of numbers from 1 to 100

tests/Anoma/Compilation/positive/test052.juvix

@@ -145,10 +145,12 @@ double+1 : Expr := Λ (compose # +1 # double # ! 0);
 
 res : Either Error Val := eval (double+1 # num 7);
 
-main : Nat :=
+-- TODO: Use Partial or failwith in left branches when anoma backend supports
+-- strings
+main : Maybe Nat :=
   case res >>= getNat of {
-    | left (ScopeError n ctx) := failwith "Scope error"
-    | left (ExpectedNat e) := failwith "Expected a natural"
-    | left ExpectedLambda := failwith "ExpectedLambda"
-    | right r := r
+    | left (ScopeError n ctx) := []
+    | left (ExpectedNat e) := []
+    | left ExpectedLambda := []
+    | right r := [r]
   };

tests/Anoma/Compilation/positive/test064.juvix

@@ -7,8 +7,9 @@ import Stdlib.Debug.Fail as Debug;
 {-# inline: false #-}
 f (x y : Nat) : Nat := x + y;
 
+-- TODO: Replace loop with failwith when anoma backend supports strings
 {-# inline: false #-}
-g (x : Bool) : Bool := if x (Debug.failwith "a") true;
+g (x : Bool) : Bool := if x loop true;
 
 {-# inline: false #-}
 h (x : Bool) : Bool := if (g x) false true;
@@ -29,7 +30,7 @@ odd : Nat -> Bool
   | (suc n) := even n;
 
 terminating
-loop : Nat := loop;
+loop {A} : A := loop;
 
 {-# inline: false #-}
 even' : Nat -> Bool := even;