Jonathan Graveline pushed to branch graveline at Stefan / Typer

Commits: bedf45c5 by Jonathan Graveline at 2018-08-03T20:45:49Z Correction in polyfun.typer; unit test in Typer for macro `_|_`

- - - - - afe315b8 by Jonathan Graveline at 2018-08-06T15:52:15Z `Env.value_equal`: using structural equality when comparing constructor name

- - - - - ffe322a7 by Jonathan Graveline at 2018-08-06T16:26:56Z Rewrote unit test for `Bbst` and `Table` in Typer code

- - - - - e9a91eba by Jonathan Graveline at 2018-08-06T23:14:53Z An attempt to fix a problem with `load_`

- - - - -

12 changed files:

- btl/pervasive.typer - btl/polyfun.typer - samples/bbst.typer - + samples/bbst_test.typer - + samples/polyfun_test.typer - samples/table.typer - + samples/table_test.typer - src/env.ml - src/opslexp.ml - − tests/bbst_test.ml - tests/macro_do_test.ml - − tests/table_test.ml

Changes:

===================================== btl/pervasive.typer ===================================== @@ -405,13 +405,10 @@ __.__ = nil); branch = Sexp_node (Sexp_symbol "_=>_") (cons pattern (cons (Sexp_symbol "v") nil)); - tmp-fix def = quote (let - (uquote (Sexp_symbol "%tuple element%")) = (uquote def) in - (uquote (Sexp_symbol "%tuple element%"))); - in tmp-fix (Sexp_node (Sexp_symbol "case_") + in Sexp_node (Sexp_symbol "case_") (cons (Sexp_node (Sexp_symbol "_|_") (cons o (cons branch nil))) - nil)) + nil) in macro (lambda args -> IO_return case args @@ -534,16 +531,13 @@ define-operator "<-" 80 96; %%%%

%% `List` is the type and `list` is the module (tuple) - list = load_ "btl/list.typer";

%% macro `do` for easier series of IO operation - do = let lib = load_ "btl/do.typer" in lib.do;

%% various macro for tuple %% used by `case_` - tuple-lib = load_ "btl/tuple.typer";

%% get nth element @@ -556,15 +550,13 @@ _<-_ = tuple-lib.assign-tuple; _,_ = tuple-lib.make-tuple;

%% macro `case` for a little more complex pattern matching - case_ = let lib = load_ "btl/case.typer" in lib.case-macro;

%%%% plain-let - -%% Not recursive and not sequential +%%%% Not recursive and not sequential

define-operator "plain-let" () 3; -%% define-operator "in" 3 67; +%% define-operator "in" 3 67;

plain-let_in_ = let lib = load_ "btl/plain-let.typer" in lib.plain-let-macro;

===================================== btl/polyfun.typer ===================================== @@ -4,17 +4,16 @@ %%%% (Just a `case` at function definition level) %%%%

+serr : (a : Type) ≡> a -> Sexp; serr = lambda _ -> Sexp_error;

-xserr = lambda a ≡> lambda s -> (nil : List a); +xserr : (a : Type) ≡> a -> List Sexp; +xserr = lambda _ -> (nil : List Sexp);

%% List_nth = list.nth; %% List_map = list.map; %% List_tail = list.tail;

-%% Not working because of `_=_` and `_;_` -%% I don't know what the right syntax for the declaration to be top-level - fun-decl : Sexp -> Sexp -> Sexp; fun-decl decl body = Sexp_node (Sexp_symbol "_;_") (cons (quote ( (uquote decl) = (uquote body) @@ -41,41 +40,41 @@ fun-args decl = Sexp_dispatch decl in List_map mf ss) xserr xserr xserr xserr xserr;

-fun-cases : List Sexp -> List (Pair (List Sexp) Sexp); +fun-cases : List Sexp -> List (Pair Sexp Sexp); fun-cases args = let

- node2list : Sexp -> List Sexp; - node2list node = Sexp_dispatch node - (lambda s ss -> cons s ss) - xserr xserr xserr xserr xserr; - - mf : Sexp -> Pair (List Sexp) Sexp; + mf : Sexp -> Pair Sexp Sexp; mf arg = let

- err = lambda _ -> pair nil Sexp_error; + err = lambda _ -> pair Sexp_error Sexp_error;

in Sexp_dispatch arg (lambda s ss -> if (Sexp_eq s (Sexp_symbol "_=>_")) then - (pair (node2list (List_nth 0 ss Sexp_error)) (List_nth 1 ss Sexp_error)) + (pair (List_nth 0 ss Sexp_error) (List_nth 1 ss Sexp_error)) else (err ())) err err err err err;

in List_map mf args;

-cases-to-sexp : List Sexp -> List (Pair (List Sexp) Sexp) -> Sexp; +cases-to-sexp : List Sexp -> List (Pair Sexp Sexp) -> Sexp; cases-to-sexp vars cases = let

- mf : Pair (List Sexp) Sexp -> Sexp; - mf p = case p | pair xs body => + mf : Pair Sexp Sexp -> Sexp; + mf p = case p | pair pat body => Sexp_node (Sexp_symbol "_=>_") - (cons (Sexp_node (Sexp_symbol "_,_") xs) - (cons body nil)); + (cons pat (cons body nil)); + + tup : Bool; + tup = Int_< 1 (List_length vars);

in Sexp_node (Sexp_symbol "case_") (cons (Sexp_node (Sexp_symbol "_|_") (cons - (Sexp_node (Sexp_symbol "_,_") vars) + (if tup then + (Sexp_node (Sexp_symbol "_,_") vars) + else + (List_nth 0 vars Sexp_error)) (List_map mf cases))) nil);

_|_ = macro (lambda args -> let @@ -86,7 +85,7 @@ _|_ = macro (lambda args -> let fargs : List Sexp; fargs = fun-args decl;

- cases : List (Pair (List Sexp) Sexp); + cases : List (Pair Sexp Sexp); cases = fun-cases (List_tail args);

in do {

===================================== samples/bbst.typer ===================================== @@ -771,6 +771,13 @@ odict-is-empty t = is-empty t; int-comp : Int -> Int -> Bool; int-comp x y = Int_<= x y;

+%% +%% Empty Int tree +%% + +int-empty : Bbst Int; +int-empty = empty int-comp; + %% %% Construct a set with Int in interval [min,max[ %%

===================================== samples/bbst_test.typer ===================================== @@ -0,0 +1,98 @@ +%%%% +%%%% Tests on Bbst +%%%% + +t0 : Bbst Int; +t0 = int-range1 0 100; + +t1 : Bbst Int; +t1 = remove-range 25 75 t0; + +t2 : Bbst Int; +t2 = insert (-1) (insert 50 (insert 100 t1)); + +t3 : Bbst Int; +t3 = insert 100 (insert (-1) (insert 50 t2)); + +t4 : Bbst Int; +t4 = remove (-1) (remove 10 (remove 100 t3)); + +t5 : Bbst Int; +t5 = remove (-2) (remove 101 (remove 10 t4)); + +e0 : Bbst Int; +e0 = int-empty; + +e1 : Bbst Int; +e1 = insert 777 e0; + +e2 : Bbst Int; +e2 = remove 777 e1; + +%% insert and remove doesn't need to be tested: +%% every test will fail if those are broken + +test-length = do { + Test_info "BBST" "length"; + + r0 <- Test_eq "t0" (length t0) 100; + r1 <- Test_eq "t1" (length t1) 50; + r2 <- Test_eq "t2" (length t2) 53; + r3 <- Test_eq "t3" (length t3) 53; + r4 <- Test_eq "t4" (length t4) 50; + r5 <- Test_eq "t5" (length t5) 50; + r6 <- Test_true "e0" (is-empty e0); + r7 <- Test_eq "e1" (length e1) 1; + r8 <- Test_eq "e2" (length e2) 0; + + if (and r0 (and r1 (and r2 (and r3 (and r4 (and r5 (and r6 (and r7 r8)))))))) then + (Test_info "BBST" "length test succeeded") + else + (Test_warning "BBST" "length test failed"); +}; + +test-find = do { + Test_info "BBST" "find"; + + r0 <- Test_eq "10 in t0" (find 10 t0) (some 10); + r1 <- Test_eq "25 not in t1" (find 25 t1) none; + r2 <- Test_eq "-1 in t2" (find (-1) t2) (some (-1)); + r3 <- Test_eq "50 in t3" (find 50 t3) (some 50); + r4 <- Test_eq "10 not in t4" (find 10 t4) none; + r5 <- Test_eq "-2 not in t5" (find (-2) t5) none; + r6 <- Test_eq "10 not in e0" (find 10 e0) none; + r7 <- Test_eq "777 in e1" (find 777 e1) (some 777); + r8 <- Test_eq "777 not in e2" (find 777 e2) none; + + if (and r0 (and r1 (and r2 (and r3 (and r4 (and r5 (and r6 (and r7 r8)))))))) then + (Test_info "BBST" "find test succeeded") + else + (Test_warning "BBST" "find test failed"); +}; + +%% member is just a wrapped version of find so not need to test it +%% in the actual implementation + +test-fold = do { + Test_info "BBST" "order"; + + v0 <- IO_return (foldl + (lambda o e -> if (Int_> o e) then 1000 else e) + (-1000) t5); + + v1 <- IO_return (foldr + (lambda o e -> if (Int_< o e) then (-1000) else e) + (1000) t5); + + r0 <- Test_false "v0" (Int_eq v0 1000); + r1 <- Test_false "v1" (Int_eq v1 (-1000)); + + if (and r0 r1) then + (Test_info "BBST" "order test succeeded") + else + (Test_warning" BBST" "order test failed"); +}; + +u = (IO_run test-length) (); +u = (IO_run test-find) (); +u = (IO_run test-fold) ();

===================================== samples/polyfun_test.typer ===================================== @@ -0,0 +1,84 @@ + +my-and (x : Bool) (y : Bool) + | (true,true) => true + | (_,_) => false; + +my-or : Bool -> Bool -> Bool; +my-or x y + | (true,_) => true + | (_,true) => true + | (_,_) => false; + +my-not (x : Option Bool) + | some true => none + | some false => some true + | none => some false; + +my-merge : List Int -> List Int -> List (Pair Int Int); +my-merge xs ys + | (nil,nil) => nil + | (cons x xs, cons y ys) => cons (pair x y) (my-merge xs ys) + | (_,_) => nil; + +test-and = do { + Test_info "POLYFUN" "my-and, basic test with type on arguments"; + + r0 <- Test_true "my-and true true" (my-and true true); + r1 <- Test_false "my-and false false" (my-and false false); + r2 <- Test_false "my-and true false" (my-and true false); + r3 <- Test_false "my-and false true" (my-and false true); + + if (and r0 (and r1 (and r2 r3))) then + (Test_info "POLYFUN" "test on my-and succeeded") + else + (Test_warning "POLYFUN" "test on my-and failed"); +}; + +test-or = do { + Test_info "POLYFUN" "my-or, basic test with function declaration"; + + r0 <- Test_true "my-or true true" (my-or true true); + r1 <- Test_false "my-or false false" (my-or false false); + r2 <- Test_true "my-or true false" (my-or true false); + r3 <- Test_true "my-or false true" (my-or false true); + + if (and r0 (and r1 (and r2 r3))) then + (Test_info "POLYFUN" "test on my-or succeeded") + else + (Test_warning "POLYFUN" "test on my-or failed"); +}; + +test-not = do { + Test_info "POLYFUN" "my-not, test with one variable, sub pattern and type on argument"; + + r0 <- Test_eq "my-not (some true)" (my-not (some true)) none; + r1 <- Test_eq "my-not (some false)" (my-not (some false)) (some true); + r2 <- Test_eq "my-not none" (my-not none) (some false); + + if (and r0 (and r1 r2)) then + (Test_info "POLYFUN" "test on my-not succeeded") + else + (Test_info "POLYFUN" "test on my-not failed"); +}; + +test-rec = do { + Test_info "POLYFUN" "my-merge, function declaraction and recursion"; + + r0 <- Test_eq "my-merge nil nil" (my-merge nil nil) nil; + r1 <- Test_eq "my-merge nil (cons 1 nil)" (my-merge nil (cons 1 nil)) nil; + r2 <- Test_eq "my-merge (cons 777 nil) (cons 999 nil)" + (my-merge (cons 777 nil) (cons 999 nil)) (cons (pair 777 999) nil); + r3 <- Test_eq "my-merge (cons 0 (cons 1 nil)) (cons 1 (cons 0 nil))" + (my-merge (cons 0 (cons 1 nil)) (cons 1 (cons 0 nil))) + (cons (pair 0 1) (cons (pair 1 0) nil)); + + if (and r0 (and r1 (and r2 r3))) then + (Test_info "POLYFUN" "test on my-merge succeeded") + else + (Test_info "POLYFUN" "test on my-merge failed"); +}; + +u = (IO_run test-and) (); +u = (IO_run test-or) (); +u = (IO_run test-not) (); +u = (IO_run test-rec) ();

===================================== samples/table.typer ===================================== @@ -263,6 +263,13 @@ int-comp x y = Int_eq x y; int-hash : Int -> Int; int-hash x = x;

+%% +%% Empty Int Table +%% + +int-empty : Table Int; +int-empty = empty int-comp int-hash; + %% %% Construct a set with Int in interval [min,max[ %%

===================================== samples/table_test.typer ===================================== @@ -0,0 +1,78 @@ +%%%% +%%%% Tests on Table +%%%% + +t0 : Table Int; +t0 = int-range 0 100; + +t1 : Table Int; +t1 = remove-range 25 75 t0; + +t2 : Table Int; +t2 = insert (-1) (insert 50 (insert 100 t1)); + +t3 : Table Int; +t3 = insert 100 (insert (-1) (insert 50 t2)); + +t4 : Table Int; +t4 = remove (-1) (remove 10 (remove 100 t3)); + +t5 : Table Int; +t5 = remove (-2) (remove 101 (remove 10 t4)); + +e0 : Table Int; +e0 = int-empty; + +e1 : Table Int; +e1 = insert 777 e0; + +e2 : Table Int; +e2 = remove 777 e1; + +%% insert and remove doesn't need to be tested: +%% every test will fail if those are broken + +test-length = do { + Test_info "TABLE" "length"; + + r0 <- Test_eq "t0" (length t0) 100; + r1 <- Test_eq "t1" (length t1) 50; + r2 <- Test_eq "t2" (length t2) 53; + r3 <- Test_eq "t3" (length t3) 53; + r4 <- Test_eq "t4" (length t4) 50; + r5 <- Test_eq "t5" (length t5) 50; + %% r6 <- Test_eq "e0" (is-empty e0) true; + r6 <- Test_true "e0" (is-empty e0); + r7 <- Test_eq "e1" (length e1) 1; + r8 <- Test_eq "e2" (length e2) 0; + + if (and r0 (and r1 (and r2 (and r3 (and r4 (and r5 (and r6 (and r7 r8)))))))) then + (Test_info "TABLE" "length test succeeded") + else + (Test_warning "TABLE" "length test failed"); +}; + +test-find = do { + Test_info "TABLE" "find"; + + r0 <- Test_eq "10 in t0" (find 10 t0) (some 10); + r1 <- Test_eq "25 not in t1" (find 25 t1) none; + r2 <- Test_eq "-1 in t2" (find (-1) t2) (some (-1)); + r3 <- Test_eq "50 in t3" (find 50 t3) (some 50); + r4 <- Test_eq "10 not in t4" (find 10 t4) none; + r5 <- Test_eq "-2 not in t5" (find (-2) t5) none; + r6 <- Test_eq "10 not in e0" (find 10 e0) none; + r7 <- Test_eq "777 in e1" (find 777 e1) (some 777); + r8 <- Test_eq "777 not in e2" (find 777 e2) none; + + if (and r0 (and r1 (and r2 (and r3 (and r4 (and r5 (and r6 (and r7 r8)))))))) then + (Test_info "TABLE" "find test succeeded") + else + (Test_warning "TABLE" "find test failed"); +}; + +%% member is just a wrapped version of find so not need to test it +%% in the actual implementation + +u = (IO_run test-length) (); +u = (IO_run test-find) ();

===================================== src/env.ml ===================================== @@ -89,7 +89,7 @@ let rec value_equal a b = if (s1 != s2) then false else true

| Vcons ((_, ct1), a1), Vcons ((_, ct2), a2) - -> if (ct1 != ct2) then false else + -> if not (ct1 = ct2) then false else not (List.exists2 (fun a b -> not (value_equal a b)) a1 a2)

===================================== src/opslexp.ml ===================================== @@ -279,6 +279,9 @@ let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = | _,_ -> false in l1 == l2 && conv_args ctx vs' args1 args2 | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> l1 = l2 && conv_p t1 t2 + (* I'm not sure to understand how to compare two Metavar * + * Should I do a `lookup`? Or is it that simple: *) + | (Metavar (id1,_,_), Metavar (id2,_,_)) -> id1 = id2 (* FIXME: Various missing cases, such as Case. *) | (_, _) -> false

===================================== tests/bbst_test.ml deleted ===================================== @@ -1,207 +0,0 @@ - -open Util -open Utest_lib - -open Sexp -open Lexp - -open Eval (* reset_eval_trace *) - -open Builtin -open Env - -(* default environment *) -let ectx = Elab.default_ectx -let rctx = Elab.default_rctx - -(* TODO : use special form "load" *) -let bbst_decl = let read_file filename = - let lines = ref [] in - let chan = open_in filename in - try - while true; do - lines := input_line chan :: !lines - done; !lines - with End_of_file -> - close_in chan; - List.rev !lines - -in String.concat "\n" (read_file "samples/bbst.typer") - -(* eval bbst.typer only once! *) -let rctx, ectx = Elab.eval_decl_str bbst_decl ectx rctx - -(* really basic tests *) - -(* first part of this file is mostly identical to table_test.ml *) - -let _ = (add_test "BBST" "length" (fun () -> - - (* it's hard to test int-range1 alone *) - let dcode = " - a = length (int-range1 0 0); - b = length (int-range1 0 1); - c = length (int-range1 0 2); - d = length (int-range1 0 100); - e = length (int-range1 1111 2222); - " in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "a; b; c; d; e;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Vint 0; Vint 1; Vint 2; Vint 100; Vint 1111] -> success () - | _ -> failure ()) -) - -let _ = (add_test "BBST" "find" (fun () -> - let dcode = " - a = find 5 (int-range1 0 100); - a = case a | some a => a | none => 777; - - b = find 101 (int-range1 0 100); - b = case b | some b => b | none => 777; - " in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "a; b;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Vint 5; Vint 777] -> success () - | _ -> failure ()) -) - -let _ = (add_test "BBST" "insert" (fun () -> - let dcode = " - a = find 777 (insert 777 (int-range1 0 0)); - a = case a | some a => a | none => 11111; - - b = find 101 (insert 101 (int-range1 0 100)); - b = case b | some b => b | none => 11111; - " in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "a; b;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Vint 777; Vint 101] -> success () - | _ -> failure ()) -) - -let _ = (add_test "BBST" "member" (fun () -> - let dcode = " - a = member 0 (int-range1 0 0); - a = case a | true => 1 | false => 0; - - b = member 15 (int-range1 15 75); - b = case b | true => 1 | false => 0; - - c = member 50 (int-range1 0 100); - c = case c | true => 1 | false => 0; - " in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "a; b; c;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Vint 0; Vint 1; Vint 1] -> success () - | _ -> failure ()) -) - -let _ = (add_test "BBST" "remove" (fun () -> - let dcode = " - t = int-range1 15 75; - - a = (length t) - (length (remove 50 t)); - - b = member 50 t; - b = case b | true => 1 | false => 0; - - c = member 50 (remove 50 t); - c = case c | true => 1 | false => 0; - " in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "a; b; c;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Vint 1; Vint 1; Vint 0] -> success () - | _ -> failure ()) -) - -(* next part isn't in table_test.ml *) - -(* foldr and foldl should work only if the tree is correctly ordered *) - -let _ = (add_test "BBST" "order and fold" (fun () -> - let dcode = " - t1 = int-range1 15 75; % max is 74, min is 15 - - t2 = int-range2 11 91; % max is 90, min is 11 - - a = foldl - (lambda o e -> if_then_else_ (Int_> o e) (75) (e)) - (14) t1; - - b = foldr - (lambda o e -> if_then_else_ (Int_< o e) (14) (e)) - (75) t1; - - c = foldl - (lambda o e -> if_then_else_ (Int_> o e) (91) (e)) - (10) t2; - - d = foldr - (lambda o e -> if_then_else_ (Int_< o e) (10) (e)) - (91) t2; - - t3 = remove-range 20 70 t1; % max is still 74, min is still 15 - - t4 = remove-range 20 80 t2; % max is still 90, min is still 11 - - e = foldl - (lambda o e -> if_then_else_ (Int_> o e) (75) (e)) - (14) t3; - - f = foldr - (lambda o e -> if_then_else_ (Int_< o e) (14) (e)) - (75) t3; - - g = foldl - (lambda o e -> if_then_else_ (Int_> o e) (91) (e)) - (10) t4; - - h = foldr - (lambda o e -> if_then_else_ (Int_< o e) (10) (e)) - (91) t4; - " in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "a; b; c; d; e; f; g; h;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Vint 74; Vint 15; Vint 90; Vint 11; Vint 74; Vint 15; Vint 90; Vint 11] -> success () - | _ -> failure ()) -) - - -(* run all tests *) -let _ = run_all ()

===================================== tests/macro_do_test.ml ===================================== @@ -128,8 +128,8 @@ let _ = (add_test "DO MACROS" "assignement with type declaration" (fun () ->

(f : Bool) <- return false;

- return (if_then_else_ f 333 - (if_then_else_ t 777 333)); + return (if f then 333 else + (if t then 777 else 333)); };" in

let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in

===================================== tests/table_test.ml deleted ===================================== @@ -1,147 +0,0 @@ - -open Util -open Utest_lib - -open Sexp -open Lexp - -open Eval (* reset_eval_trace *) - -open Builtin -open Env - -(* default environment *) -let ectx = Elab.default_ectx -let rctx = Elab.default_rctx - -(* TODO : use special form "load" *) -let table_decl = let read_file filename = - let lines = ref [] in - let chan = open_in filename in - try - while true; do - lines := input_line chan :: !lines - done; !lines - with End_of_file -> - close_in chan; - List.rev !lines - -in String.concat "\n" (read_file "samples/table.typer") - -(* eval table.typer only once! *) -let rctx, ectx = Elab.eval_decl_str table_decl ectx rctx - -(* really basic tests *) - -let _ = (add_test "TABLE" "length" (fun () -> - - (* it's hard to test int-range alone *) - let dcode = " - a = length (int-range 0 0); - b = length (int-range 0 1); - c = length (int-range 0 2); - d = length (int-range 0 100); - e = length (int-range 1111 2222); - " in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "a; b; c; d; e;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Vint 0; Vint 1; Vint 2; Vint 100; Vint 1111] -> success () - | _ -> failure ()) -) - -let _ = (add_test "TABLE" "find" (fun () -> - let dcode = " - a = find 5 (int-range 0 100); - a = case a | some a => a | none => 777; - - b = find 101 (int-range 0 100); - b = case b | some b => b | none => 777; - " in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "a; b;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Vint 5; Vint 777] -> success () - | _ -> failure ()) -) - -let _ = (add_test "TABLE" "insert" (fun () -> - let dcode = " - a = find 777 (insert 777 (int-range 0 0)); - a = case a | some a => a | none => 11111; - - b = find 101 (insert 101 (int-range 0 100)); - b = case b | some b => b | none => 11111; - " in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "a; b;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Vint 777; Vint 101] -> success () - | _ -> failure ()) -) - -let _ = (add_test "TABLE" "member" (fun () -> - let dcode = " - a = member 0 (int-range 0 0); - a = case a | true => 1 | false => 0; - - b = member 15 (int-range 15 75); - b = case b | true => 1 | false => 0; - - c = member 50 (int-range 0 100); - c = case c | true => 1 | false => 0; - " in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "a; b; c;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Vint 0; Vint 1; Vint 1] -> success () - | _ -> failure ()) -) - -let _ = (add_test "TABLE" "remove" (fun () -> - let dcode = " - t = int-range 15 75; - - a = (length t) - (length (remove 50 t)); - - b = member 50 t; - b = case b | true => 1 | false => 0; - - c = member 50 (remove 50 t); - c = case c | true => 1 | false => 0; - " in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "a; b; c;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Vint 1; Vint 1; Vint 0] -> success () - | _ -> failure ()) -) - - -(* run all tests *) -let _ = run_all ()

View it on GitLab: https://gitlab.com/monnier/typer/compare/d63644ece795190ad8cd3d7e7691beb16aa...