Unverified Commit b3563ac2 authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

Tests for lists

parent 495d4c0e
Pipeline #167999151 failed with stage
in 12 minutes and 54 seconds
......@@ -3,6 +3,9 @@
def assert : { b : bool } -> {} =
if b then noop else failwith {} end
def assert_not : { b : bool } -> {} =
b = ~b; {} = assert{b=b}
#define ASSERT_EQ(A, B) a = A; b = B; r = a == b; {} = assert{b=r}
// Unit
......@@ -201,6 +204,158 @@ def test_ternary : {} -> {} =
{n=n} = choice_to_nat{c=c};
ASSERT_EQ(n, 2)
// Lists
def is_nil : {l : list nat} -> {b : bool} =
match l with [] -> b = true | hd :: tl -> drop hd; drop tl; b = false end
def assert_nil : {l : list nat} -> {} =
{b=b} = is_nil{l=l}; {} = assert{b=b}
def assert_not_nil : {l : list nat} -> {} =
{b=b} = is_nil{l=l}; {} = assert_not{b=b}
def test_is_nil : {} -> {} =
// test is_nil (pattern matching) and the various ways to define a list
l = ([] : list nat); {} = assert_nil{l=l};
l = ([0] : list nat); {} = assert_not_nil{l=l};
l = ([0; 1] : list nat); {} = assert_not_nil{l=l};
l = ([1; 0] : list nat); {} = assert_not_nil{l=l};
z = 0; l = ([] : list nat); l = z :: l; {} = assert_not_nil{l=l}
def test_size : {} -> {} =
// test the size primitive on lists
l = ([] : list nat); n = size l; ASSERT_EQ(n, 0);
l = ([0] : list nat); n = size l; ASSERT_EQ(n, 1);
l = ([0; 1] : list nat); n = size l; ASSERT_EQ(n, 2)
def assert_head : {l : list nat; hd : nat} -> {tl : list nat} =
match l with [] -> failwith {} | hd0 :: tl -> ASSERT_EQ(hd0, hd) end
def assert_list_eq: {l1 : list nat; l2 : list nat} -> {} =
for x in l1 do {tl=l2} = assert_head {l=l2; hd=x} done; {} = assert_nil{l=l2}
// Example of use:
def test_list_eq: {} -> {} =
l1 = ([] : list nat);
l2 = ([] : list nat);
{} = assert_list_eq{l1=l1; l2=l2};
l1 = ([42] : list nat);
l2 = ([42] : list nat);
{} = assert_list_eq{l1=l1; l2=l2};
l1 = ([0; 1; 2; 3] : list nat);
l2 = ([0; 1; 2; 3] : list nat);
{} = assert_list_eq{l1=l1; l2=l2}
def drop_list : {l : list nat} -> {} =
for x in l do drop x done
def test_drop_list : {} -> {} =
l = ([] : list nat); {} = drop_list{l=l};
l = ([0; 1; 2] : list nat); {} = drop_list{l=l}
def sum : {l : list nat} -> {n : nat} =
n = 0; for x in l do n = n + x done
def test_sum : {} -> {} =
l = ([] : list nat); {n=n} = sum{l=l}; ASSERT_EQ(n, 0);
l = ([0; 1] : list nat); {n=n} = sum{l=l}; ASSERT_EQ(n, 1);
l = ([1; 0] : list nat); {n=n} = sum{l=l}; ASSERT_EQ(n, 1);
l = ([1; 1; 1] : list nat); {n=n} = sum{l=l}; ASSERT_EQ(n, 3)
def nth : {l : list nat; n : int; default : nat} -> {r : nat} =
r = default;
for x in l do
(n, n0) = dup n;
z = +0;
b = n0 == z;
if b then drop r; r = x else drop x end;
one = 1;
n = n - one
done;
drop n
def test_nth : {} -> {} =
// test the nth function used to test other functions
l = ([2; 3; 4] : list nat);
n = -1;
default = 0;
{r=r} = nth{l=l; n=n; default=default};
ASSERT_EQ(r, 0);
l = ([2; 3; 4] : list nat);
n = +0;
default = 0;
{r=r} = nth{l=l; n=n; default=default};
ASSERT_EQ(r, 2);
l = ([2; 3; 4] : list nat);
n = +1;
default = 0;
{r=r} = nth{l=l; n=n; default=default};
ASSERT_EQ(r, 3);
l = ([2; 3; 4] : list nat);
n = +2;
default = 0;
{r=r} = nth{l=l; n=n; default=default};
ASSERT_EQ(r, 4);
l = ([2; 3; 4] : list nat);
n = +3;
default = 0;
{r=r} = nth{l=l; n=n; default=default};
ASSERT_EQ(r, 0)
def rev_append : {l1 : list nat; l2 : list nat} -> {l : list nat} =
for x in l1 do l2 = x :: l2 done; l = l2
def rev : {l : list nat} -> {l : list nat} =
l2 = ([] : list nat);
{l=l} = rev_append{l1=l; l2=l2}
def test_rev : {} -> {} =
l = ([] : list nat); {l=l1} = rev{l=l};
l2 = ([] : list nat); {} = assert_list_eq{l1=l1; l2=l2};
l = ([42] : list nat); {l=l1} = rev{l=l};
l2 = ([42] : list nat); {} = assert_list_eq{l1=l1; l2=l2};
l = ([0; 1; 2; 3] : list nat); {l=l1} = rev{l=l};
l2 = ([3; 2; 1; 0] : list nat); {} = assert_list_eq{l1=l1; l2=l2}
def map_size : {l : list string} -> {l : list nat} =
l = map x in l do size x done
def test_map_size : {} -> {} =
l = (["hello"; "world"; "!"] : list string);
{l=l1} = map_size{l=l};
l2 = ([5; 5; 1] : list nat);
{} = assert_list_eq{l1=l1; l2=l2}
def double_nat : {n : nat} -> nat =
two = 2;
n = two * n;
return n
def double : {l : list nat} -> {l : list nat} =
l = map x in l do double_nat{n=x} done
def test_double : {} -> {} =
l = ([2; 3] : list nat); {l=l2} = double{l=l};
l1 = ([4; 6] : list nat);
{} = assert_list_eq{l1=l1; l2=l2}
def test_list : {} -> {} =
{} = test_is_nil{};
{} = test_size{};
{} = test_list_eq{};
{} = test_drop_list{};
{} = test_sum{};
{} = test_nth{};
{} = test_map_size{};
{} = test_double{};
{} = test_rev{};
noop
def main : { param : unit; storage : unit } -> { op : list operation; storage: unit } =
drop param;
{} = test_pair {} ;
......@@ -208,4 +363,5 @@ def main : { param : unit; storage : unit } -> { op : list operation; storage: u
{} = test_option {} ;
{} = test_wrapped_nat {};
{} = test_fake_bool {};
{} = test_list {};
op = ([] : list operation)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment