Jonathan Graveline pushed to branch graveline at Stefan / Typer

Commits: 124601a5 by Jonathan Graveline at 2018-07-03T22:19:55Z Corrected indentation in case.typer; table.typer rewriten with unit tests/table_test.ml

- - - - -

5 changed files:

- btl/pervasive.typer - samples/case.typer - samples/table.typer - tests/eval_test.ml - + tests/table_test.ml

Changes:

===================================== btl/pervasive.typer ===================================== --- a/btl/pervasive.typer +++ b/btl/pervasive.typer @@ -216,6 +216,10 @@ chain-decl : Sexp -> Sexp -> Sexp; chain-decl a b = Sexp_node (Sexp_symbol "_;_") (cons a (cons b nil));

+chain-decl3 : Sexp -> Sexp -> Sexp -> Sexp; +chain-decl3 a b c = + Sexp_node (Sexp_symbol "_;_") (cons a (cons b (cons c nil))); + %% Build datacons: %% ctor-name = datacons type-name ctor-name; make-cons : Sexp -> Sexp -> Sexp; @@ -263,6 +267,28 @@ type-impl = lambda (x : List Sexp) -> kerr % Integer kerr % Float kerr; % List of Sexp + + get-args : Sexp -> List Sexp; + get-args sxp = + Sexp_dispatch sxp + (lambda _ args -> args) % Nodes + (lambda _ -> (nil : List Sexp)) % Symbol + (lambda _ -> (nil : List Sexp)) % String + (lambda _ -> (nil : List Sexp)) % Integer + (lambda _ -> (nil : List Sexp)) % Float + (lambda _ -> (nil : List Sexp)); % List of Sexp + + get-type : Sexp -> Sexp; + get-type sxp = + Sexp_dispatch sxp + (lambda s ss -> case (Sexp_eq s (Sexp_symbol "_:_")) + | true => List_nth 1 ss Sexp_error + | false => sxp) + (lambda _ -> sxp) + (lambda _ -> Sexp_error) + (lambda _ -> Sexp_error) + (lambda _ -> Sexp_error) + (lambda _ -> Sexp_error);

get-head = List_head Sexp_error;

@@ -282,6 +308,14 @@ type-impl = lambda (x : List Sexp) -> %% Create the inductive type definition. inductive = Sexp_node (Sexp_symbol "typecons") (cons name ctor); + + %% Declare the inductive type as a function + %% Useful for recursive type + type-decl = quote ((uquote (get-name name)) : (uquote ( + (List_foldl (lambda args arg -> + Sexp_node (Sexp_symbol "_->_") (cons (get-type arg) (cons args nil))) + (Sexp_symbol "Type") (List_reverse (get-args name) nil)) + )));

decl = make-decl type-name inductive;

@@ -296,10 +330,10 @@ type-impl = lambda (x : List Sexp) -> | nil => acc in for-each ctor (Sexp_node (Sexp_symbol "_;_") nil)

- %% return decls - in chain-decl decl % inductive type declaration - ctors; % constructor declarations - + %% return decls + in chain-decl3 type-decl % type as a function declaration + decl % inductive type declaration + ctors; % constructor declarations

return_type_impl : List Sexp -> IO Sexp; return_type_impl = lambda args -> IO_return (type-impl args); @@ -333,7 +367,8 @@ BoolMod = (##datacons cons) (_ := Bool) (_ := true) (_ := false);

-Pair = typecons (Pair (a : Type) (b : Type)) (cons (x :: a) (y :: b)); +Pair = typecons (Pair (a : Type) (b : Type)) (pair (fst : a) (snd : b)); +pair = datacons Pair pair;

__.__ = let mksel o f = @@ -379,7 +414,7 @@ Decidable = typecons (Decidable (prop : Type))

%% Testing generalization in inductive type constructors. LList : (a : Type) -> Int -> Type; %FIXME: `LList : ?` should be sufficient! -type LList (a : Type) n +type LList (a : Type) (n : Int) | vnil (p ::: Eq n 0) | vcons a (LList a ?n1) (p ::: Eq n (?n1 + 1)); %FIXME: Unsound wraparound!

===================================== samples/case.typer ===================================== --- a/samples/case.typer +++ b/samples/case.typer @@ -259,8 +259,8 @@ expand_cases pats = let expand : VarTest -> IO (List VarTest); expand test = let

- % I don't expect to use multiple not_unique_sym at the same time - % so the name may be reused + %% I don't expect to use multiple not_unique_sym at the same time + %% so the name may be reused

not_unique_sym : Sexp; not_unique_sym = Sexp_symbol " %not gensym% "; @@ -367,13 +367,8 @@ pattern_to_sexp vars pats = let | some fail => (quote (##case_ (_|_ (uquote var) (_=>_ (uquote ctor) (uquote succ)) (_=>_ _ (uquote fail))))) - | none => % if_then_else_ (Sexp_eq ctor (Sexp_symbol "_")) - (quote (##case_ (_|_ (uquote var) - (_=>_ (uquote ctor) (uquote succ))))); - % "?" doesn't seem to help - % (quote (##case_ (_|_ (uquote var) - % (_=>_ (uquote ctor) (uquote succ))) - % (_=>_ _ ?))); + | none => (quote (##case_ (_|_ (uquote var) + (_=>_ (uquote ctor) (uquote succ)))));

push : Int -> List Sexp -> List Sexp; push n vars = if_then_else_ (Int_<= n 1) @@ -439,8 +434,8 @@ pattern_to_sexp vars pats = let last_test_fun vars pat = (quote (lambda (_ : Unit) -> (uquote (last_to_sexp vars pat))));

- % Same thing as not_unique_sym, I can reuse the name because - % only the last defined is important + %% Same thing as not_unique_sym, I can reuse the name because + %% only the last defined is important

fail_sym : Sexp; fail_sym = Sexp_symbol " %fail sym% "; @@ -511,7 +506,7 @@ case_ = macro (lambda args -> let vars_wrap free_vars num_vars f; };

- % Only the Sexp after "_|_" are interesting + %% Only the Sexp after "_|_" are interesting

case1 : Sexp -> List Sexp -> IO Sexp; case1 s ss = if_then_else_ (Sexp_eq (Sexp_symbol "_|_") s) @@ -520,7 +515,7 @@ case_ = macro (lambda args -> let

err = (lambda _ -> IO_return Sexp_error);

-% Expecting only one Sexp_node containing a case with arguments +%% Expecting only one Sexp_node containing a case with arguments

in (Sexp_dispatch (List_nth 0 args Sexp_error) case1 err err err err err)

===================================== samples/table.typer ===================================== --- a/samples/table.typer +++ b/samples/table.typer @@ -1,116 +1,51 @@ %%% -%%% Table as a B tree +%%% Table as a tree %%%

%% -%% Just a Pair type returned by some function and use in the tree. -%% Prefer use of "data" and "key" for access in case the internal change. -%% - -type Vec2 (a : Type) (b : Type) - | vec2 a b; - -%% -%% Access function -%% - -data : (a : Type) ≡> (k : Type) ≡> Vec2 a k -> a; - -data e = case e - | vec2 d _ => d; - -key : (a : Type) ≡> (k : Type) ≡> Vec2 a k -> k; - -key e = case e - | vec2 _ k => k; - -%% %% a : element type -%% k : key type -%% s : size as a base of 2 (e.g. s = 5 <=> size = 32) -%% c : compare function (for key) -%% h : hash function (for key) +%% c : compare function +%% h : hash function %% -%% Many things are specified but there will be -%% some predefined table at the end of this file. +%% (Hint : use a Pair type with custom compare and hash to create a dictionary +%% rather than a set) +%% +%% hash in table-leaf only keep tail of hash %%

-TableData : Type -> Type -> Type; - -type TableData (a : Type) (k : Type) - | table-node (left : TableData a k) (right : TableData a k) - | table-leaf (elems : List (Vec2 a k)) +type TableTree (a : Type) + | table-node (left : TableTree a) (right : TableTree a) + | table-leaf (hash : Int) (elems : List a) | table-nil;

-type Table (a : Type) (k : Type) - | table (s : Int) (c : k -> k -> Bool) (h : k -> Int) (t : TableData a k); +type Table (a : Type) + | table (c : a -> a -> Bool) (h : a -> Int) (t : TableTree a);

%% %% fold left in an unspecified order %%

-foldl : (b : Type) ≡> (a : Type) ≡> (k : Type) ≡> - (b -> (Vec2 a k) -> b) -> b -> Table a k -> b; - +foldl : (b : Type) ≡> (a : Type) ≡> (b -> a -> b) -> b -> Table a -> b; foldl f o t = let

- helper : (b : Type) ≡> (a : Type) ≡> (k : Type) ≡> - (b -> (Vec2 a k) -> b) -> b -> TableData a k -> b; - + helper : (b : Type) ≡> (a : Type) ≡> (b -> a -> b) -> b -> TableTree a -> b; helper f o t = case t - | table-node l r => ( let + | table-node l r => let o1 = helper f o l; o2 = helper f o1 r; - in o2 ) - | table-leaf xs => List_foldl f o xs + in o2 + | table-leaf _ xs => List_foldl f o xs | table-nil => o;

in case t - | table _ _ _ t => helper f o t; - -%% -%% This function is for internal use only (used in shrink) -%% - -tabledata-length : (a : Type) ≡> (k : Type) ≡> Int -> TableData a k -> Int; -tabledata-length o tree = case tree - | table-node l r => ( let - o1 = tabledata-length o l; - o2 = tabledata-length o1 r; - in o2 ) - | table-leaf xs => o + (List_length xs) - | table-nil => o; - -%% -%% After many "insert" and "remove" there may be useless node which -%% are still in the tree. Use "shrink" to remove useless node. -%% -%% (there may be a way to do it efficiently within "remove") -%% - -shrink : (a : Type) ≡> (k : Type) ≡> Table a k -> Table a k; -shrink tree = let - - helper : (a : Type) ≡> (k : Type) ≡> TableData a k -> TableData a k; - helper tree = case tree - | table-node l r => ( let - l1 = helper l; - r1 = helper r; - l2 = if_then_else_ (Int_eq (tabledata-length 0 l1) 0) - (table-nil) (l); - r2 = if_then_else_ (Int_eq (tabledata-length 0 r1) 0) - (table-nil) (r); - in table-node l2 r2 ) - | table-leaf xs => if_then_else_ (Int_eq (List_length xs) 0) - (table-nil) (table-leaf xs) - | table-nil => table-nil; - -in case tree - | table s c h t => table s c h (helper t); + | table _ _ t => helper f o t;

%% %% Get the number of element in the tree %% +%% (we could easily keep track of element inserted and removed) +%% (currently O(n)) +%%

length t = let fold-fun len _ = len + 1; @@ -123,203 +58,185 @@ in foldl fold-fun 0 t; is-empty t = Int_eq (length t) 0;

%% -%% Insert a data/key pair (vec2) in the tree +%% Insert an element in the tree %%

-insert : (a : Type) ≡> (k : Type) ≡> a -> k -> Table a k -> Table a k; -insert elem key tree = let +insert : (a : Type) ≡> a -> Table a -> Table a; +insert elem tree = let

- choose-fun : (k -> k -> Bool) -> (Vec2 a k) -> (Vec2 a k) -> (Vec2 a k); - choose-fun comp p0 p1 = case p0 - | vec2 e0 k0 => ( case p1 - | vec2 e1 k1 => if_then_else_ (comp k1 k0) (p1) (p0) - ); - - is-key-in : (k -> k -> Bool) -> k -> List (Vec2 a k) -> Bool; - is-key-in comp k0 xs = let - - fold-fun : Bool -> (Vec2 a k) -> Bool; - fold-fun b x = ( case b - | true => true - | false => ( case x - | vec2 _ k1 => comp k0 k1 - ) - ); - - in List_foldl fold-fun false xs; + replace-or-add : a -> (a -> a -> Bool) -> List a -> List a; + replace-or-add e c es = case es + | cons e1 es => if_then_else_ (c e e1) + (cons e es) + (cons e1 (replace-or-add e c es)) + | nil => (cons e nil);

- helper : Int -> Int -> (k -> k -> Bool) -> TableData a k -> TableData a k; - - helper count hash comp tree = case tree - | table-node l r => if_then_else_ (Int_eq (Int_and hash 1) 0) - (table-node (helper (count - 1) (Int_lsr hash 1) comp l) r) - (table-node l (helper (count - 1) (Int_lsr hash 1) comp r)) - | table-leaf elems => if_then_else_ (is-key-in comp key elems) - (table-leaf (List_foldl (lambda es e -> - (cons (choose-fun comp e (vec2 elem key)) es)) nil elems)) - (table-leaf (cons (vec2 elem key) elems)) - | table-nil => if_then_else_ (Int_eq count 0) - (table-leaf (cons (vec2 elem key) nil)) - (helper count hash comp - (table-node table-nil table-nil)); + helper : a -> (a -> a -> Bool) -> Int -> TableTree a -> TableTree a; + helper e c h t = case t + | table-node l r => if_then_else_ (Int_eq 0 (Int_and h 1)) + (table-node (helper e c (Int_lsr h 1) l) r) + (table-node l (helper e c (Int_lsr h 1) r)) + | table-leaf h1 es => if_then_else_ (Int_eq h h1) + (table-leaf h1 (replace-or-add e c es)) + (if_then_else_ (Int_eq 0 (Int_and h1 1)) + (helper e c h + (table-node (table-leaf (Int_lsr h1 1) es) table-nil)) + (helper e c h + (table-node table-nil (table-leaf (Int_lsr h1 1) es)))) + | table-nil => table-leaf h (cons e nil);

in case tree - | table s c h t => table s c h (helper s (Int_mod (h key) (Int_lsl 1 s)) c t); + | table c h t => table c h (helper elem c (h elem) t);

%% -%% Remove a data/key pair associated with a given key from the tree. +%% Remove an element from the tree. %%

-remove : (a : Type) ≡> (k : Type) ≡> k -> Table a k -> Table a k; +remove : (a : Type) ≡> a -> Table a -> Table a; +remove elem tree = let

-remove key tree = let - - to-remove : (k -> k -> Bool) -> (Vec2 a k) -> Bool; - to-remove comp elem = case elem - | vec2 _ key0 => comp key key0; + is-empty : TableTree a -> Bool; + is-empty t = case t + | table-node l r => if_then_else_ (is-empty l) + (is-empty r) + (false) + | table-leaf _ es => Int_eq 0 (List_length es) + | table-nil => true;

- helper : Int -> Int -> (k -> k -> Bool) -> TableData a k -> TableData a k; + pop-empty : TableTree a -> TableTree a; + pop-empty t = if_then_else_ (is-empty t) + (table-nil) + (t);

- helper count hash comp tree = case tree - | table-node l r => if_then_else_ (Int_eq (Int_and hash 1) 0) - (table-node (helper (count - 1) (Int_lsr hash 1) comp l) r) - (table-node l (helper (count - 1) (Int_lsr hash 1) comp r)) - | table-leaf elems => (table-leaf (List_foldl (lambda es e -> - (if_then_else_ (to-remove comp e) (es) (cons e es)) - ) nil elems)) - | table-nil => table-nil; + remove : a -> (a -> a -> Bool) -> List a -> List a; + remove e c es = case es + | cons e1 es => if_then_else_ (c e e1) + (es) + (cons e1 (remove e c es)) + | nil => nil; % element not found + + helper : a -> (a -> a -> Bool) -> Int -> TableTree a -> TableTree a; + helper e c h t = case t + | table-node l r => if_then_else_ (Int_eq 0 (Int_and h 1)) + (pop-empty (table-node (helper e c (Int_lsr h 1) l) r)) + (pop-empty (table-node l (helper e c (Int_lsr h 1) r))) + | table-leaf h1 es => if_then_else_ (Int_eq h h1) + (pop-empty (table-leaf h1 (remove e c es))) + (table-leaf h1 es) % element not found + | table-nil => table-nil; % element not found

in case tree - | table s c h t => table s c h (helper s (Int_mod (h key) (Int_lsl 1 s)) c t); + | table c h t => table c h (helper elem c (h elem) t);

%% -%% Change a data associated with a given key +%% Change an element +%% +%% Use in case the compare function isn't a total equality +%% (e.g. use a Pair type to create a dictionary) %% %% Should be faster to use this than "remove" and then "insert" %%

-update : (a : Type) ≡> (k : Type) ≡> a -> k -> Table a k -> Table a k; - -update elem key tree = let - - to-update : (k -> k -> Bool) -> (Vec2 a k) -> Bool; - to-update comp elem = case elem - | vec2 _ key0 => comp key key0; - - helper : Int -> Int -> (k -> k -> Bool) -> TableData a k -> TableData a k; - - helper count hash comp tree = case tree - | table-node l r => if_then_else_ (Int_eq (Int_and hash 1) 0) - (table-node (helper (count - 1) (Int_lsr hash 1) comp l) r) - (table-node l (helper (count - 1) (Int_lsr hash 1) comp r)) - | table-leaf elems => (table-leaf (List_foldl (lambda es e -> - (if_then_else_ (to-update comp e) (cons (vec2 elem key) es) (cons e es)) - ) nil elems)) - | table-nil => table-nil; - -in case tree - | table s c h t => table s c h (helper s (Int_mod (h key) (Int_lsl 1 s)) c t); +update : (a : Type) ≡> a -> Table a -> Table a; +update elem tree = insert elem tree; % used to be more complicated

%% -%% Is there a data associated with key in the tree? +%% Is this element in the tree? %%

-member : (a : Type) ≡> (k : Type) ≡> k -> Table a k -> Bool; -member key tree = let - - searched : (k -> k -> Bool) -> (Vec2 a k) -> Bool; - searched comp elem = case elem - | vec2 _ key0 => comp key key0; - - search-fun : (k -> k -> Bool) -> Bool -> Vec2 a k -> Bool; - search-fun comp b e = if_then_else_ b true (searched comp e); +member : (a : Type) ≡> a -> Table a -> Bool; +member elem tree = let

- helper : Int -> Int -> (k -> k -> Bool) -> TableData a k -> Bool; - - helper count hash comp tree = case tree - | table-node l r => if_then_else_ (Int_eq (Int_and hash 1) 0) - (helper (count - 1) (Int_lsr hash 1) comp l) - (helper (count - 1) (Int_lsr hash 1) comp r) - | table-leaf elems => (List_foldl (search-fun comp) false elems) - | table-nil => false; + is-in : a -> (a -> a -> Bool) -> List a -> Bool; + is-in e c es = case es + | cons e1 es => if_then_else_ (c e e1) (true) (is-in e c es) + | nil => false; + + helper : a -> (a -> a -> Bool) -> Int -> TableTree a -> Bool; + helper e c h t = case t + | table-node l r => if_then_else_ (Int_eq 0 (Int_and h 1)) + (helper e c (Int_lsr h 1) l) + (helper e c (Int_lsr h 1) r) + | table-leaf h1 es => if_then_else_ (Int_eq h h1) + (is-in e c es) + (false) % element not found + | table-nil => false; % element not found

in case tree - | table s c h t => helper s (Int_mod (h key) (Int_lsl 1 s)) c t; + | table c h t => (helper elem c (h elem) t);

%% -%% Find a data/key pair in the tree and return it -%% -%% You should then use "data" or "key" to access value in the pair +%% Find an element in the tree and return it %%

-find : (a : Type) ≡> (k : Type) ≡> k -> Table a k -> Option (Vec2 a k); +find : (a : Type) ≡> a -> Table a -> Option a; +find elem tree = let

-find key tree = let - - searched : (k -> k -> Bool) -> (Vec2 a k) -> Bool; - searched comp elem = case elem - | vec2 _ key0 => comp key key0; - - search : (k -> k -> Bool) -> List (Vec2 a k) -> Option (Vec2 a k); - search comp xs = case xs - | cons x xs => if_then_else_ (searched comp x) (some x) (search comp xs) + get : a -> (a -> a -> Bool) -> List a -> Option a; + get e c es = case es + | cons e1 es => if_then_else_ (c e e1) (some e1) (get e c es) | nil => none;

- helper : Int -> Int -> (k -> k -> Bool) -> TableData a k -> Option (Vec2 a k); - - helper count hash comp tree = case tree - | table-node l r => if_then_else_ (Int_eq (Int_and hash 1) 0) - (helper (count - 1) (Int_lsr hash 1) comp l) - (helper (count - 1) (Int_lsr hash 1) comp r) - | table-leaf elems => search comp elems - | table-nil => none; + helper : a -> (a -> a -> Bool) -> Int -> TableTree a -> Option a; + helper e c h t = case t + | table-node l r => if_then_else_ (Int_eq 0 (Int_and h 1)) + (helper e c (Int_lsr h 1) l) + (helper e c (Int_lsr h 1) r) + | table-leaf h1 es => if_then_else_ (Int_eq h h1) + (get e c es) + (none) % element not found + | table-nil => none; % element not found

in case tree - | table s c h t => helper s (Int_mod (h key) (Int_lsl 1 s)) c t; - -%% -%% Find a data/key pair in the tree and return the data only -%% - -at : (a : Type) ≡> (k : Type) ≡> k -> Table a k -> Option a; - -at key tree = case (find key tree) - | some x => some (data x) - | none => none; + | table c h t => (helper elem c (h elem) t);

%% %% An empty tree with a key compare function and a key hash function as argument %%

-empty : (a : Type) ≡> (k : Type) ≡> (k -> k -> Bool) -> (k -> Int) -> Table a k; -empty comp-fun hash-fun = table 8 comp-fun hash-fun table-nil; +empty : (a : Type) ≡> (a -> a -> Bool) -> (a -> Int) -> Table a; +empty comp-fun hash-fun = table comp-fun hash-fun table-nil;

%%% -%%% Test helper and default definition will follow +%%% Test helper %%%

+%% +%% Compare function for Int +%% + int-comp : Int -> Int -> Bool; int-comp x y = Int_eq x y;

+%% +%% Hash function for Int +%% + int-hash : Int -> Int; int-hash x = x;

-int-range : Int -> Int -> Table Int Int; +%% +%% Construct a set with Int in interval [min,max[ +%%

+int-range : Int -> Int -> Table Int; int-range min max = let

- helper : Int -> Int -> Table Int Int -> Table Int Int; - helper min max tree = if_then_else_ (Int_eq min max) - (tree) (helper (min + 1) max (insert min min tree)); + helper : Int -> Table Int -> Table Int; + helper min tree = if_then_else_ (Int_eq min max) + (tree) (helper (min + 1) (insert min tree));

-in helper min max (empty int-comp int-hash); +in helper min (empty int-comp int-hash);

-remove-range : Int -> Int -> Table Int Int -> Table Int Int; +%% +%% Remove Int inside interval [min,max[ from the Table +%%

+remove-range : Int -> Int -> Table Int -> Table Int; remove-range min max tree = let

- helper : Int -> Int -> Table Int Int -> Table Int Int; - helper min max tree = if_then_else_ (Int_eq min max) - (tree) (helper (min + 1) max (remove min tree)); + helper : Int -> Table Int -> Table Int; + helper min tree = if_then_else_ (Int_eq min max) + (tree) (helper (min + 1) (remove min tree));

-in helper min max tree; +in helper min tree;

===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -372,9 +372,11 @@ let _ = test_eval_eqv_named p = lambda a ≡> lambda x notx -> notx x; tP : Decidable P; tP = (datacons Decidable true) (prop := P) (p := p); + + PairTest = typecons (Pair (a : Type) (b : Type)) (cons (x :: a) (y :: b));

- ptest : Pair Int String; - ptest = (##datacons Pair cons) (x := 4) (y := "hello"); + ptest : PairTest Int String; + ptest = (##datacons PairTest cons) (x := 4) (y := "hello");

px = case ptest | (##datacons ? cons) (x := v) => v;

===================================== tests/table_test.ml ===================================== --- /dev/null +++ b/tests/table_test.ml @@ -0,0 +1,144 @@ + +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") + +(* really basic tests *) + +let _ = (add_test "TABLE" "length" (fun () -> + + (* it's hard to test int-range alone *) + let dcode = table_decl^" + 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 = table_decl^" + 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 = table_decl^" + 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 = table_decl^" + 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 = table_decl^" + 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/commit/124601a5ba7e451dbe8c5f33e01e7ba3e019...