diff --git a/test/Anoma/Compilation/Positive.hs b/test/Anoma/Compilation/Positive.hs index a635a44c8c..0cec9338b3 100644 --- a/test/Anoma/Compilation/Positive.hs +++ b/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 ".") diff --git a/tests/Anoma/Compilation/positive/test007.juvix b/tests/Anoma/Compilation/positive/test007.juvix index a0c8d91291..cd6d7ab6cc 100644 --- a/tests/Anoma/Compilation/positive/test007.juvix +++ b/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}; diff --git a/tests/Anoma/Compilation/positive/test026.juvix b/tests/Anoma/Compilation/positive/test026.juvix index 74f36eba8c..dbb5f40566 100644 --- a/tests/Anoma/Compilation/positive/test026.juvix +++ b/tests/Anoma/Compilation/positive/test026.juvix @@ -3,8 +3,7 @@ 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; @@ -12,44 +11,69 @@ qfst : {A : Type} → Queue A → List A 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 diff --git a/tests/Anoma/Compilation/positive/test052.juvix b/tests/Anoma/Compilation/positive/test052.juvix index e16068fbed..4d897f86c3 100644 --- a/tests/Anoma/Compilation/positive/test052.juvix +++ b/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] }; diff --git a/tests/Anoma/Compilation/positive/test064.juvix b/tests/Anoma/Compilation/positive/test064.juvix index ea2f3ced8b..e52005dc82 100644 --- a/tests/Anoma/Compilation/positive/test064.juvix +++ b/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;