Commit ebe77f50 authored by Pietro Abate's avatar Pietro Abate
Browse files

Merge branch 'eval-test' into typing-test

parents aa812436 e8106d00
......@@ -145,7 +145,7 @@ and compile_abstr env a =
let slots = Array.of_list (List.rev slots) in
let env = { env with vars = fun_env; gamma = (env.gamma @ fun_name);
let env = { env with vars = fun_env; gamma = IdMap.merge (fun _ v2 -> v2) env.gamma fun_name;
stack_size = 0; max_stack = ref 0 } in
let body = compile_branches env a.Typed.fun_body in
let sigma = `Sel(a.Typed.fun_fv,a.Typed.fun_iface,env.sigma) in
......
expr = id
| integer
| `true
| `false
| string
| "`true"
| "`false"
| STRING
| abstr
| "let" LIDENT ":" type_id "=" expr "in" expr ":" type_id
| expr "." expr
| expr "," expr
| expr "{" id "/" type_id sigma "}"
| expr "+" expr
| expr "-" expr
| expr "*" expr
| expr "/" expr
| expr "%" expr
| expr "@" expr
| expr "{" UIDENT "/" type_id sigma "}" (* type substitutions *)
| "(" expr ")"
| "[" "]" (* nil *)
| "[" listexpr "]"
| "match" expr ":" type_id "with" "|" match_value "->" expr branches
;;
sigma = (* empty *)
| ";" id "/" type_id
| ";" UIDENT "/" type_id
;;
listexpr = (* empty *)
| expr
listexpr = expr
| listexpr ";" listexpr
;;
abstr = "fun" id id ":" type_id params ":" type_id "->" expr
| "fun" "_" id ":" type_id params ":" type_id "->" expr
| "fun" type_id "|" match_value "->" expr branches
;;
match_value = id ":" type_id
| integer
| string
| STRING
| match_value "," match_value
| match_value "::" match_value
| "(" match_value ")"
;;
params = (* empty *)
| id ":" type_id params
;;
branches = (* empty *)
| "|" match_value "->" expr branches
;;
id = [a-z_][A-Za-z0-9_]*
(* Note: The first character of an id is lower case (or '_'), the first
character of a type is upper case *)
type_id = [A-Z][A-Za-z0-9_]*
| "'"[A-Z][A-Za-z0-9_]*
| "'"[A-Z][A-Za-z0-9_]* "{" id "/" type_id sigma "}"
id = LIDENT (* [a-z_][A-Za-z0-9_]* *)
;;
(* One must precise a set of type substitutions on a type variable, at least a
empty one: α = 'A{} *)
type_id = UIDENT
| "'" UIDENT "{" sigma "}"
| "[" complex_type_id "]"
| "(" complex_type_id ")"
;;
complex_type_id = [A-Z][A-Za-z0-9_]*
| "'"[A-Z][A-Za-z0-9_]*
| "'"[A-Z][A-Za-z0-9_]* "{" id "/" type_id sigma "}"
complex_type_id = UIDENT (* [A-Z][A-Za-z0-9_]* *)
| "'" UIDENT "{" sigma "}"
| complex_type_id "*" complex_type_id
| complex_type_id "|" complex_type_id
| complex_type_id "&" complex_type_id
| "!" complex_type_id
| complex_type_id -> complex_type_id
| complex_type_id "->" complex_type_id
| "[" complex_type_id "]"
| "(" complex_type_id ")"
;;
integer = [0-9]+
integer = INTEGER (* [0-9]+ *)
......@@ -25,7 +25,7 @@ RM ?= rm -f
OUT ?= main.native
OUTDEBUG ?= main.byte
.PHONY: clean check test _import
.PHONY: clean _import tests
all: _import
$(COMPILER) -use-ocamlfind $(OUT)
......@@ -33,6 +33,9 @@ all: _import
debug: _import
$(COMPILER) -use-ocamlfind -tag debug $(OUTDEBUG)
tests:
make -C tests
_import:
@echo -n "Copying external files..."
@test -d $(EXTDIR) || mkdir $(EXTDIR)
......@@ -40,5 +43,6 @@ _import:
@echo "done"
clean:
make -C tests clean
$(COMPILER) -clean
test $(EXTDIR) = "src" || test $(EXTDIR) = "." || $(RM) -r $(EXTDIR)
......@@ -45,15 +45,24 @@ let rec _to_typed env l expr =
let _, _, e2 = _to_typed env l e2 in
let t = Types.times (Types.cons e1.exp_typ) (Types.cons e2.exp_typ) in
env, l, { exp_loc=loc; exp_typ=t; exp_descr=Pair(e1, e2) }
| Op (_, op, e1, e2) ->
let _, _, e1 = _to_typed env l e1 in
let _, _, e2 = _to_typed env l e2 in
env, l, { exp_loc=loc; exp_typ=type_of_string "Int";
exp_descr=Op(op, 0, [e1; e2]) }
| Var (origloc, vname) ->
let line = Loc.start_line origloc in
let cbegin = Loc.start_off origloc - Loc.start_bol origloc in
let cend = Loc.stop_off origloc - Loc.start_bol origloc in
if vname = "`nil" then
let nil_atom = Atoms.V.mk_ascii "nil" in
env, l, { exp_loc=loc; exp_typ=(Types.atom (Atoms.atom nil_atom));
exp_descr=(Cst (Types.Atom nil_atom)) }
else if vname = "_" then
(Printf.eprintf
"File %s, line %d, characters %d-%d:\nError: Invalid reference to special variable %s\n"
(Loc.file_name origloc) line cbegin cend vname; raise Error)
else
let line = Loc.start_line origloc in
let cbegin = Loc.start_off origloc - Loc.start_bol origloc in
let cend = Loc.stop_off origloc - Loc.start_bol origloc in
let index, vtype =
try Locals.find vname l
with Not_found -> Printf.eprintf
......@@ -212,14 +221,22 @@ and parse_match_value env l list toptype = function
Patterns.Times (make_patterns t1 list1 d1, make_patterns t2 list2 d2),
(list1 @ list2), l, b1 && b2;
| MVar (_, mname, mtype) ->
let lsize = Locals.cardinal l in
let l = Locals.add mname (lsize, type_of_ptype mtype) l in
let list = list @ [lsize, mname] in
let d1 = Types.any, list, Patterns.Capture(lsize, mname) in
let t2 = type_of_ptype mtype in
let d2 = t2, [], Patterns.Constr(t2) in
let is_subtype = Types.subtype t2 (type_of_ptype toptype) in
(t2, Patterns.Cap(d1, d2), list, l, is_subtype)
if mname = "`nil" then
let nil_atom = Atoms.V.mk_ascii "nil" in
let t = Types.atom (Atoms.atom nil_atom) in
(t, Patterns.Constr(t), list, l, true)
else if mname = "_" then
let t = type_of_ptype mtype in
(t, Patterns.Constr(t), list, l, true)
else
let lsize = Locals.cardinal l in
let l = Locals.add mname (lsize, type_of_ptype mtype) l in
let list = list @ [lsize, mname] in
let d1 = Types.any, list, Patterns.Capture(lsize, mname) in
let t2 = type_of_ptype mtype in
let d2 = t2, [], Patterns.Constr(t2) in
let is_subtype = Types.subtype t2 (type_of_ptype toptype) in
(t2, Patterns.Cap(d1, d2), list, l, is_subtype)
| MInt (_, i) ->
let t = Types.constant (Types.Integer(Big_int.big_int_of_int i)) in
let is_subtype = Types.subtype (type_of_string "Int")
......@@ -232,6 +249,33 @@ and parse_match_value env l list toptype = function
(type_of_ptype toptype) in
(t, Patterns.Constr(t), list, l, is_subtype)
let arith_op f = function
| Value.Integer(x) :: Value.Integer(y) :: [] ->
Value.Integer(Big_int.big_int_of_int (f (Big_int.int_of_big_int x)
(Big_int.int_of_big_int y)))
| _ -> raise Error
let concat =
let rec add_to_tail y = function
| Value.Pair(x, nil, s) ->
if nil = Value.Atom(Atoms.V.mk_ascii "nil")
then Value.Pair(x, y, s) else Value.Pair(x, add_to_tail y nil, s)
| _ -> raise Error in
function
| (Value.Pair(_, _, _) as x) :: (Value.Pair(_) as y) :: [] ->
add_to_tail y x
| x :: y :: [] ->
if x = Value.Atom(Atoms.V.mk_ascii "nil") then y
else if y = Value.Atom(Atoms.V.mk_ascii "nil") then x
else raise Error
| _ -> raise Error
let to_typed expr =
Eval.register_op "+" (arith_op ( + ));
Eval.register_op "-" (arith_op ( - ));
Eval.register_op "*" (arith_op ( * ));
Eval.register_op "/" (arith_op ( / ));
Eval.register_op "%" (arith_op ( mod ));
Eval.register_op "@" concat;
let env, _, expr = _to_typed Compile.empty_toplevel Locals.empty expr in
env, expr
......@@ -41,10 +41,13 @@ let tests_poly_abstr = [
Arrow)* ]),{}))",
"fun tail x : ['A{}] : ['A{}] -> match x : ['A{}] with | (el : 'A{}) :: (rest : ['A{}]) -> rest";
"Test CDuce.runtime.poly.pair failed", "",
"fun pair x : ('A{} * 'B{}) : 'A{} -> match x : ('A{} * 'B{}) with | (x : 'A{}, y : 'B{}) -> x";
"Test CDuce.runtime.poly.pair failed", "Abstraction(Dummy,,,,Sel(,((`$A & Int | Char | Atom | (Any,Any) |
<(Any) (Any)>Any | Arrow,`$B & Int | Char |
Atom | (Any,Any) | <(Any) (Any)>Any | Arrow) ->
`$A & Int | Char | Atom | (Any,Any) | <(Any) (Any)>Any | Arrow),{}))",
"fun pair x : ('A{} * 'B{}) : 'A{} -> match x : ('A{} * 'B{}) with | (z : 'A{}, y : 'B{}) -> z";
"Test CDuce.runtime.poly.match_abstr failed", "",
"Test CDuce.runtime.poly.match_abstr failed", "Apply(,)",
"(match (fun f x : 'A{} : 'A{} -> x) : ('A{} -> 'A{}) with | y : ('A{} -> 'A{}) -> y{A/Int}).3";
......@@ -74,6 +77,23 @@ let run_test_eval str =
let tests_eval = "CDuce runtime tests (Typed -> Lambda -> Value)" >:::
[
"abstr" >:: ( fun test_ctxt ->
assert_equal ~msg:"Test CDuce.runtime.abstr.let_simple failed"
~printer:(fun x -> x) "3"
(run_test_eval "let x : Int = 3 in x : Int");
assert_equal ~msg:"Test CDuce.runtime.abstr.let_medium failed"
~printer:(fun x -> x) "2"
(run_test_eval "let f : (Int -> Int) = (fun (Int -> Int) | x : Int -> x)
in (f.f.2) : Int");
assert_equal ~msg:"Test CDuce.runtime.abstr.let_nested_simple failed"
~printer:(fun x -> x) "3"
(run_test_eval "let f : (Int -> Int) = (fun (Int -> Int) | x : Int -> x + 1)
in (let x : Int = f.2
in x : Int) : Int");
assert_equal ~msg:"Test CDuce.runtime.abstr.let_nested_medium failed"
~printer:(fun x -> x) "4"
(run_test_eval "let f : (Int -> Int) = (fun (Int -> Int) | x : Int -> x + 1)
in (let x : Int = f.2
in f.x : Int) : Int");
assert_equal ~msg:"Test CDuce.runtime.abstr.simple failed"
~printer:(fun x -> x) "Abstraction((Int, Int),{})"
(run_test_eval "fun f x : Int : Int -> 2");
......@@ -96,6 +116,38 @@ let tests_eval = "CDuce runtime tests (Typed -> Lambda -> Value)" >:::
);
"misc" >:: ( fun test_ctxt ->
assert_equal ~msg:"Test CDuce.runtime.misc.even failed"
~printer:(fun x -> x)
"Abstraction((Int, Bool) ,(Any \\ (Int), Any \\ (Int)),{})"
(run_test_eval "fun ((Int -> Bool) & ((!Int) -> (!Int)))
| x : Int -> (match (x % 2) : Int with
| 0 -> `true
| 1 -> `false)
| x : (!Int) -> x");
assert_equal ~msg:"Test CDuce.runtime.misc.even_applied1 failed"
~printer:(fun x -> x)
"Atom(false)"
(run_test_eval "(fun ((Int -> Bool) & ((!Int) -> (!Int)))
| x : Int -> (match (x % 2) : Int with
| 0 -> `true
| 1 -> `false)
| x : (!Int) -> x).5");
assert_equal ~msg:"Test CDuce.runtime.misc.even_applied2 failed"
~printer:(fun x -> x)
"Atom(true)"
(run_test_eval "(fun ((Int -> Bool) & ((!Int) -> (!Int)))
| x : Int -> (match (x % 2) : Int with
| 0 -> `true
| 1 -> `false)
| x : (!Int) -> x).8");
assert_equal ~msg:"Test CDuce.runtime.misc.even_applied3 failed"
~printer:(fun x -> x)
"(2, (3, Atom(nil), {}), {})"
(run_test_eval "(fun ((Int -> Bool) & ((!Int) -> (!Int)))
| x : Int -> (match (x % 2) : Int with
| 0 -> `true
| 1 -> `false)
| x : (!Int) -> x).[2; 3]");
assert_equal ~msg:"Test CDuce.runtime.misc.is_int failed"
~printer:(fun x -> x)
"Abstraction((Int, Bool) ,(Bool, Bool) ,(Any \\ (Int | Bool), Any \\ (Int | Bool)),{})"
......@@ -119,7 +171,7 @@ let tests_eval = "CDuce runtime tests (Typed -> Lambda -> Value)" >:::
| x : (!(Int|Bool)) -> x).`true");
assert_equal ~msg:"Test CDuce.runtime.misc.is_int_applied3 failed"
~printer:(fun x -> x)
"(2, 3, {})"
"(2, (3, Atom(nil), {}), {})"
(run_test_eval "(fun ((Int -> Bool) & (Bool -> Bool) & ((!(Int|Bool)) -> (!(Int|Bool))))
| x : Int -> `true
| x : Bool -> `false
......@@ -136,25 +188,64 @@ let tests_eval = "CDuce runtime tests (Typed -> Lambda -> Value)" >:::
Arrow)* ]),{})"
(run_test_eval "fun map f : ('A{}->'B{}) x : ['A{}] : ['B{}] ->
match x : ['A{}] with
| (el : 'A{}) :: (rest : ['A{}]) -> [f.el; (map.f).rest]
| el : ['A{}] -> f.el");
| (el : 'A{}) :: [] -> f.el
| (el : 'A{}) :: (rest : ['A{}]) -> ((f.el), ((map.f).rest))");
assert_equal ~msg:"Test CDuce.runtime.misc.map_even_simple failed"
~printer:(fun x -> x)
"(\"hey\", (Atom(false), Atom(nil), {}), {})"
(run_test_eval "(fun map f : ('A{A/Int;A/Bool}->'B{A/Int;A/Bool}) x : ['A{A/Int;A/Bool}] : ['B{A/Int;A/Bool}] ->
match x : ['A{A/Int;A/Bool}] with
| (el : 'A{A/Int;A/Bool}) :: (rest : ['A{A/Int;A/Bool}]) -> ((f.el), ((map.f).rest))
| [] -> []).(fun ((Int -> Bool) & ((!Int) -> (!Int)))
| x : Int -> (match (x % 2) : Int with
| 0 -> `true
| 1 -> `false)
| x : (!Int) -> x).[\"hey\"; 3]");
assert_equal ~msg:"Test CDuce.runtime.misc.map_even_medium failed"
~printer:(fun x -> x)
"(Atom(true), (\"hey\", (Atom(false), (Atom(true), Atom(nil), {}), {}), {}), {})"
(run_test_eval "(fun map f : ('A{A/Int;A/Bool}->'B{A/Int;A/Bool}) x : ['A{A/Int;A/Bool}] : ['B{A/Int;A/Bool}] ->
match x : ['A{A/Int;A/Bool}] with
| (el : 'A{A/Int;A/Bool}) :: (rest : ['A{A/Int;A/Bool}]) -> ((f.el), ((map.f).rest))
| [] -> []).(fun ((Int -> Bool) & ((!Int) -> (!Int)))
| x : Int -> (match (x % 2) : Int with
| 0 -> `true
| 1 -> `false)
| x : (!Int) -> x).[4; \"hey\"; 3; 2]");
assert_equal ~msg:"Test CDuce.runtime.misc.map_even_hard failed"
~printer:(fun x -> x)
"(Atom(true), (\"hey\", ((3, (5, Atom(nil), {}), {}), (Atom(true), (Abstraction((
`$C & Int | Char | Atom | (Any,Any) | <(Any) (Any)>Any | Arrow, `$C & Int |
Char |
Atom |
(Any,Any) |
<(Any) (Any)>Any |
Arrow),{}), (Atom(false), Atom(nil), {}), {}), {}), {}), {}), {})"
(run_test_eval "(fun map f : ('A{A/Int;A/Bool}->'B{A/Int;A/Bool}) x : ['A{A/Int;A/Bool}] : ['B{A/Int;A/Bool}] ->
match x : ['A{A/Int;A/Bool}] with
| (el : 'A{A/Int;A/Bool}) :: (rest : ['A{A/Int;A/Bool}]) -> ((f.el), ((map.f).rest))
| [] -> []).(fun ((Int -> Bool) & ((!Int) -> (!Int)))
| x : Int -> (match (x % 2) : Int with
| 0 -> `true
| 1 -> `false)
| x : (!Int) -> x).[4; \"hey\"; [3; 5]; 2; (fun ('C{} -> 'C{}) | x : 'C{} -> x); 3+4]");
assert_equal ~msg:"Test CDuce.runtime.misc.map_is_int_simple failed"
~printer:(fun x -> x)
"(Atom(false), Atom(true), {})"
"(Atom(false), (Atom(true), Atom(nil), {}), {})"
(run_test_eval "(fun map f : ('A{A/Int;A/Bool}->'B{A/Int;A/Bool}) x : ['A{A/Int;A/Bool}] : ['B{A/Int;A/Bool}] ->
match x : ['A{A/Int;A/Bool}] with
| (el : 'A{A/Int;A/Bool}) :: (rest : ['A{A/Int;A/Bool}]) -> [f.el; (map.f).rest]
| el : ['A{A/Int;A/Bool}] -> f.el).(fun ((Int -> Bool) & (Bool -> Bool) & ((!(Int|Bool)) -> (!(Int|Bool))))
| (el : 'A{A/Int;A/Bool}) :: (rest : ['A{A/Int;A/Bool}]) -> ((f.el), ((map.f).rest))
| [] -> []).(fun ((Int -> Bool) & (Bool -> Bool) & ((!(Int|Bool)) -> (!(Int|Bool))))
| x : Int -> `true
| x : Bool -> `false
| x : (!(Int|Bool)) -> x).[`true; 3]");
assert_equal ~msg:"Test CDuce.runtime.misc.map_is_int_medium failed"
~printer:(fun x -> x)
"(Atom(false), Atom(true), Atom(false), {})"
"(Atom(false), (Atom(true), (Atom(false), Atom(nil), {}), {}), {})"
(run_test_eval "(fun map f : ('A{A/Int;A/Bool}->'B{A/Int;A/Bool}) x : ['A{A/Int;A/Bool}] : ['B{A/Int;A/Bool}] ->
match x : ['A{A/Int;A/Bool}] with
| (el : 'A{A/Int;A/Bool}) :: (rest : ['A{A/Int;A/Bool}]) -> [f.el; (map.f).rest]
| el : ['A{A/Int;A/Bool}] -> f.el).(fun ((Int -> Bool) & (Bool -> Bool) & ((!(Int|Bool)) -> (!(Int|Bool))))
| (el : 'A{A/Int;A/Bool}) :: (rest : ['A{A/Int;A/Bool}]) -> ((f.el), ((map.f).rest))
| [] -> []).(fun ((Int -> Bool) & (Bool -> Bool) & ((!(Int|Bool)) -> (!(Int|Bool))))
| x : Int -> `true
| x : Bool -> `false
| x : (!(Int|Bool)) -> x).[`true; 3; `true]");
......@@ -179,26 +270,31 @@ let tests_eval = "CDuce runtime tests (Typed -> Lambda -> Value)" >:::
f.x).2).(fun g x : Int : Int -> x)");
);
"arith" >:: ( fun test_ctxt ->
assert_equal ~msg:"Test CDuce.runtime.arith.simple failed"
~printer:(fun x -> x) "5"
(run_test_eval "2+3");
assert_equal ~msg:"Test CDuce.runtime.arith.complete failed"
~printer:(fun x -> x) "1"
(run_test_eval "2+5*7%2-8/4");
);
"match" >:: ( fun test_ctxt ->
assert_equal ~msg:"Test CDuce.runtime.match.simple failed"
~printer:(fun x -> x) "1"
(run_test_eval "match 1 : Int with | 1 -> 1 | \"true\" -> \"true\"");
assert_equal ~msg:"Test CDuce.runtime.match.unused_branches failed"
~printer:(fun x -> x) "1"
(run_test_eval "match 1 : Int with
| s : String -> s | b : Bool -> b | i : Int -> i");
(run_test_eval "match 1 : Int with | 1 -> 1");
assert_equal ~msg:"Test CDuce.runtime.match.simple_var failed"
~printer:(fun x -> x) "2"
(run_test_eval "(fun f x : Int : Int ->
match x : Int with | y : Int -> x).2");
match x : Int with | _ : Int -> x).2");
assert_equal ~msg:"Test CDuce.runtime.match.medium failed"
~printer:(fun x -> x) "2"
(run_test_eval "(fun f x : Int : Int ->
match x : Int with | 1 -> 3 | x : Int -> x).2");
match x : Int with | 1 -> 3 | _ : Int -> x).2");
assert_equal ~msg:"Test CDuce.runtime.match.rec failed"
~printer:(fun x -> x) "3"
(run_test_eval "(fun f x : Int : Int ->
match x : Int with | 1 -> 3 | x : Int -> f.1).2");
match x : Int with | 1 -> 3 | _ : Int -> f.1).2");
);
"string" >:: ( fun test_ctxt ->
......@@ -211,27 +307,56 @@ let tests_eval = "CDuce runtime tests (Typed -> Lambda -> Value)" >:::
assert_equal ~msg:"Test CDuce.runtime.list.simple failed"
~printer:(fun x -> x) "1"
(run_test_eval "match [1; 2] : [Int] with
| (el : Int) :: (rest : [Int]) -> el
| x : Int -> 3");
| (el : Int) :: (_ : [Int]) -> el
| [] -> 3");
assert_equal ~msg:"Test CDuce.runtime.list.simple2 failed"
~printer:(fun x -> x) "3"
(run_test_eval "match 2 : Int with
| (el : Int) :: (rest : [Int]) -> el
| x : Int -> 3");
(run_test_eval "match [] : [Int] with
| (el : Int) :: (_ : [Int]) -> el
| [] -> 3");
assert_equal ~msg:"Test CDuce.runtime.list.tail failed"
~printer:(fun x -> x) "Abstraction(([ Int* ], [ Int* ]),{})"
(run_test_eval "fun tail x : [Int] : [Int] -> match x : [Int] with
| (el : Int) :: (rest : [Int]) -> rest");
| (_ : Int) :: (rest : [Int]) -> rest");
assert_equal ~msg:"Test CDuce.runtime.list.tail.eval failed"
~printer:(fun x -> x) "(2, 5, {})"
~printer:(fun x -> x) "(2, (5, Atom(nil), {}), {})"
(run_test_eval "(fun tail x : [Int] : [Int] -> match x : [Int] with
| (el : Int) :: (rest : [Int]) -> rest).[1; 2; 5]");
(* TODO: Fix this test, we need to define [] aka `nil *)
| (_ : Int) :: (rest : [Int]) -> rest).[1; 2; 5]");
assert_equal ~msg:"Test CDuce.runtime.list.last failed"
~printer:(fun x -> x) "7"
(run_test_eval "(fun f x : [Int] : [Int] -> match x : [Int] with
| (el : Int) :: (rest : [Int]) -> f.rest
| el : [Int] -> el).[1; 2; 5; 4; 8; 7]");
| (el : Int) :: [] -> el
| (_ : Int) :: (rest : [Int]) -> f.rest).[1; 2; 5; 4; 8; 7]");
assert_equal ~msg:"Test CDuce.runtime.list.plusone failed"
~printer:(fun x -> x) "(2, (3, (6, (5, (9, 8, {}), {}), {}), {}), {})"
(run_test_eval "(fun f x : [Int] : [Int] -> match x : [Int] with
| (el : Int) :: [] -> el+1
| (el : Int) :: (rest : [Int]) -> ((el+1), (f.rest))).[1; 2; 5; 4; 8; 7]");
assert_equal ~msg:"Test CDuce.runtime.list.concat failed"
~printer:(fun x -> x) "(1, (2, (5, (4, (8, (7, (2, (3, (4, Atom(nil), {}), {}), {}), {}), {}), {}), {}), {}), {})"
(run_test_eval "(fun concat x : [[Int]] : [Int] -> match x : [[Int]] with
| (el : [Int]) :: [] -> el
| (el : [Int]) :: (rest : [[Int]]) -> (el@(concat.rest))).[[1; 2; 5; 4; 8; 7]; [2; 3; 4]]");
assert_equal ~msg:"Test CDuce.runtime.list.length_easy failed"
~printer:(fun x -> x) "6"
(run_test_eval "(fun length x : [Int] : Int -> match x : [Int] with
| [] -> 0
| (el : Int) :: (rest : [Int]) -> length.rest + 1).[1; 2; 5; 4; 8; 7]");
assert_equal ~msg:"Test CDuce.runtime.list.length_hard failed"
~printer:(fun x -> x) "((6, 0, {}), 2, {})"
(run_test_eval "let length : (['A{A/Int; A/Bool}] -> Int) =
(fun f l : ['A{A/Int; A/Bool}] : Int -> match l : ['A{A/Int; A/Bool}] with
| [] -> 0
| (el : 'A{A/Int; A/Bool}) :: (rest : ['A{A/Int; A/Bool}]) -> f.rest + 1)
in
(length.[1; 2; 5; 4; 8; 7], length.[], length.[`true; 2]) : (Int*Int*Int)");
assert_equal ~msg:"Test CDuce.runtime.list.nth failed"
~printer:(fun x -> x) "5"
(run_test_eval "(fun nth l : ['A{A/Int; A/Bool}] n : Int : 'A{A/Int; A/Bool} ->
match l : ['A{A/Int; A/Bool}] with
| (el : 'A{A/Int; A/Bool}) :: [] -> el
| (el : 'A{A/Int; A/Bool}) :: (rest : ['A{A/Int; A/Bool}]) ->
(match n : Int with | 0 -> el | _ : Int -> (nth.rest).(n-1))).[1; 2; 5; `true; 2].2");
);
"union" >:: ( fun test_ctxt ->
......@@ -242,20 +367,20 @@ let tests_eval = "CDuce runtime tests (Typed -> Lambda -> Value)" >:::
~printer:(fun x -> x) "Abstraction(([ Char* ] | Int, [ Char* ] | Int),{})"
(run_test_eval "fun f x : (Int | String) : (Int | String) ->
match x : (Int | String) with
| x : Int -> 2
| x : String -> \"Piece of cake\"");
| _ : Int -> 2
| _ : String -> \"Piece of cake\"");
assert_equal ~msg:"Test CDuce.runtime.union.match_applied failed"
~printer:(fun x -> x) "2"
(run_test_eval "(fun f x : (Int | String) : (Int | String) ->
match x : (Int | String) with
| x : Int -> 2
| x : String -> \"Piece of cake\").5");
| _ : Int -> 2
| _ : String -> \"Piece of cake\").5");
assert_equal ~msg:"Test CDuce.runtime.union.match_applied2 failed"
~printer:(fun x -> x) "\"Piece of cake\""
(run_test_eval "(fun f x : (Int | String) : (Int | String) ->
match x : (Int | String) with
| x : Int -> 2
| x : String -> \"Piece of cake\").\"test\"");
| _ : Int -> 2
| _ : String -> \"Piece of cake\").\"test\"");
);
"union_precise" >:: ( fun test_ctxt ->
......@@ -304,11 +429,11 @@ let tests_eval = "CDuce runtime tests (Typed -> Lambda -> Value)" >:::
Arrow)* ], [ (`$A & Int | Char | Atom | (Any,Any) |
<(Any) (Any)>Any | Arrow)* ]),{})"
(run_test_eval "fun tail x : ['A{}] : ['A{}] -> match x : ['A{}] with
| (el : 'A{}) :: (rest : ['A{}]) -> rest");
| (_ : 'A{}) :: (rest : ['A{}]) -> rest");
assert_equal ~msg:"Test CDuce.runtime.poly.tail_applied failed"
~printer:(fun x -> x) "(7, (8, 5, {}), {})"
~printer:(fun x -> x) "(7, (8, (5, Atom(nil), {}), {}), {})"
(run_test_eval "(fun tail x : ['A{}] : ['A{}] -> match x : ['A{}] with
| (el : 'A{}) :: (rest : ['A{}]) -> rest).[3; 7; 8; 5]");
| (_ : 'A{}) :: (rest : ['A{}]) -> rest).[3; 7; 8; 5]");
);
......@@ -322,4 +447,3 @@ let _ =
]
)
;;
......@@ -7,6 +7,7 @@ type expr =
| Abstr of Loc.t * fun_name * ptype * fv * branches
| Match of Loc.t * expr * ptype * branches
| Pair of Loc.t * expr * expr
| Op of Loc.t * string * expr * expr
| Var of Loc.t * string
| Int of Loc.t * int
| String of Loc.t * string
......@@ -52,18 +53,33 @@ module ExprParser = struct
| (loc, pname, ptype) :: rest ->
let t = TArrow(ptype, t) in
let newfv = match fv with | _ :: rest -> rest | [] -> assert false in
aux (Abstr(_loc, x, t, fv, [_loc, MVar(loc, pname, ptype), acc]))
aux (Abstr(_loc, "_", t, fv, [_loc, MVar(loc, pname, ptype), acc]))
t newfv rest
| [] -> acc
in
aux e t (make_fv [] 1 p) (List.rev p)
aux e t (make_fv [0, x] 1 p) (List.rev p)
| "fun"; t = type_id; b = LIST1 branch -> Abstr(_loc, "_", t, [], b)
| "let"; x = LIDENT; ":"; t = type_id; "="; v = SELF; "in"; e = SELF;
":"; te = type_id -> Match(_loc, v, t, [_loc, MVar(_loc, x, t), e])
| "match"; e = SELF; ":"; t = type_id; "with"; b = LIST1 branch ->
Match(_loc, e, t, b) ]
| "pair" LEFTA
[ e1 = SELF; ","; e2 = SELF -> Pair(_loc, e1, e2)
| e1 = SELF ; "."; e2 = SELF -> Apply(_loc, e1, e2) ]
| "list" LEFTA [ "["; le = listexpr; "]" -> le ]
| "add" LEFTA
[ e1 = SELF; "+"; e2 = SELF -> Op(_loc, "+", e1, e2)
| e1 = SELF; "-"; e2 = SELF -> Op(_loc, "-", e1, e2) ]
| "mult" LEFTA
[ e1 = SELF; "*"; e2 = SELF -> Op(_loc, "*", e1, e2)
| e1 = SELF; "/"; e2 = SELF -> Op(_loc, "/", e1, e2)
| e1 = SELF; "%"; e2 = SELF -> Op(_loc, "%", e1, e2) ]
| "concat" LEFTA [ e1 = SELF; "@"; e2 = SELF -> Op(_loc, "@", e1, e2) ]
| "pair" LEFTA [ e1 = SELF; ","; e2 = SELF -> Pair(_loc, e1, e2) ]
| "apply" [ e1 = SELF ; "."; e2 = SELF -> Apply(_loc, e1, e2) ]
| "list" LEFTA
[ "["; le = LIST0 SELF SEP ";"; "]" ->
let rec make_seq res = function
| e :: rest -> make_seq (Pair(_loc, e, res)) rest
| [] -> res in
make_seq (Var(_loc, "`nil")) (List.rev le)
]
| "paren" [ "("; e = SELF; ")" -> e ]
| "var" [ x = LIDENT -> Var(_loc, x) ]
| "int" [ x = INT -> Int(_loc, int_of_string x) ]
......@@ -75,9 +91,6 @@ module ExprParser = struct
sigma: [[ x = UIDENT; "/"; t = type_id -> x, t ]];
listexpr:[ "rec" RIGHTA [ l1=SELF; ";"; l2=SELF -> Pair(_loc, l1, l2) ]
| [ e=expression -> e]];
param:[[p = LIDENT; ":"; t = type_id -> _loc, p, t]];
branch:[ "branch"
......@@ -92,6 +105,7 @@ module ExprParser = struct
| "var" [ x = LIDENT; ":"; t = type_id -> MVar(_loc, x, t) ]
| "int" [ x = INT -> MInt(_loc, int_of_string x) ]
| "string" [ x = STRING -> MString(_loc, x) ]
| "empty" [ "["; "]" -> MVar(_loc, "`nil", Type("Any")) ]
];
type_id: [ "atom_type"
......@@ -122,6 +136,7 @@ let get_loc expr = match expr with
| Abstr (loc, _, _, _, _) -> loc
| Match (loc, _, _, _) -> loc
| Pair (loc, _, _) -> loc
| Op (loc, _, _, _) -> loc