Skip to content

Commit

Permalink
Fix anoma tests to use failwith instead of partial
Browse files Browse the repository at this point in the history
  • Loading branch information
paulcadman committed Feb 22, 2024
1 parent a3d888d commit 2a22b2f
Show file tree
Hide file tree
Showing 2 changed files with 11 additions and 8 deletions.
6 changes: 3 additions & 3 deletions tests/Anoma/Compilation/positive/test007.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -11,8 +11,8 @@ map' {A B} (f : A → B) : List A → List B :=
};

terminating
map'' {A B} {{Partial}} (f : A → B) (x : List A) : List B :=
if (null x) nil (f (phead x) :: map'' f (tail x));
map'' {A B} (f : A → B) (x : List A) : List B :=
if (null x) nil (f (head (failwith "head: empty list") x) :: map'' f (tail x));

lst : List Nat := 0 :: 1 :: nil;

Expand All @@ -24,4 +24,4 @@ main : List Nat :=
>>> trace (head 0 (tail lst))
>>> trace (map ((+) 1) lst)
>>> trace (map' ((+) 1) lst)
>>> runPartial λ {{{_}} := map'' ((+) 1) lst};
>>> map'' ((+) 1) lst;
13 changes: 8 additions & 5 deletions tests/Anoma/Compilation/positive/test026.juvix
Original file line number Diff line number Diff line change
@@ -1,7 +1,10 @@
-- functional queues
module test026;

import Stdlib.Prelude open;
import Stdlib.Prelude open hiding {phead};
import Stdlib.Debug open;

phead {A} : List A -> A := head (failwith "head: empty list");

type Queue (A : Type) :=
| queue : List A → List A → Queue A;
Expand All @@ -12,7 +15,7 @@ qfst : {A : Type} → Queue A → List A
qsnd : {A : Type} → Queue A → List A
| (queue _ x) := x;

front {{Partial}} : {A : Type} → Queue A → A
front : {A : Type} → Queue A → A
| q := phead (qfst q);

pop_front : {A : Type} → Queue A → Queue A
Expand Down Expand Up @@ -41,15 +44,15 @@ is_empty : {A : Type} → Queue A → Bool
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));

-- 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

0 comments on commit 2a22b2f

Please sign in to comment.