Commit aac87d17 authored by Julien Lopez's avatar Julien Lopez
Browse files

[TESTS] Let runtime handle type substitutions

parent 5ce3a562
......@@ -66,13 +66,13 @@ 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 "[" sigmalist "]"
| "'" UIDENT
| "[" complex_type_id "]"
| "(" complex_type_id ")"
;;
complex_type_id = UIDENT (* [A-Z][A-Za-z0-9_]* *)
| "'" UIDENT "[" sigmalist "]"
| "'" UIDENT
| complex_type_id "*" complex_type_id
| complex_type_id "|" complex_type_id
| complex_type_id "&" complex_type_id
......
......@@ -121,8 +121,7 @@ and type_of_sigma x s =
and type_of_ptype =
let open Types in function
| Type(t) -> type_of_string t
| PType(t, [[]]) -> var (`Var (Var.make_id t))
| PType(t,s) -> type_of_sigma t s
| PType(t) -> var (`Var (Var.make_id t))
| TPair(t1, t2) -> times (cons (type_of_ptype t1)) (cons (type_of_ptype t2))
| TUnion(t1, t2) -> cup (type_of_ptype t1) (type_of_ptype t2)
| TInter(t1, t2) -> cap (type_of_ptype t1) (type_of_ptype t2)
......
......@@ -31,7 +31,7 @@ let tests_poly_abstr = [
"Abstraction(Dummy,,,,Sel(,([ Char* ] | Int -> [ Char* ] | Int),Comp({},{ { `$A =
Int } ,{ `$A = [ Char* ]
} })))",
"(fun f x : 'A[{A/Int},{A/String}] : 'A[{A/Int},{A/String}] -> x) [{A/Int},{A/String}]";
"(fun f x : 'A : 'A -> x) [{A/Int},{A/String}]";
"Test CDuce.runtime.poly.tail failed",
"Abstraction(Dummy,,,,Sel(,([ (`$A & Int | Char | Atom | (Any,Any) |
......@@ -41,13 +41,13 @@ Int } ,{ `$A = [ Char* ]
(Any,Any) |
<(Any) (Any)>Any |
Arrow)* ]),{}))",
"fun tail x : ['A[{}]] : ['A[{}]] -> match x : ['A[{}]] with | (el : 'A[{}]) :: (rest : ['A[{}]]) -> rest";
"fun tail x : ['A] : ['A] -> match x : ['A] with | (el : 'A) :: (rest : ['A]) -> rest";
"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";
"fun pair x : ('A * 'B) : 'A -> match x : ('A * 'B) with | (z : 'A, y : 'B) -> z";
"Test CDuce.runtime.poly.match_abstr failed", "Apply(Match(Abstraction(Dummy,,,,Sel(,(`$A & Int | Char | Atom | (Any,Any) |
<(Any) (Any)>Any | Arrow -> `$A & Int |
......@@ -58,7 +58,7 @@ Int } ,{ `$A = [ Char* ]
Arrow),{})), {accept_chars=false; brs_disp=<disp>; brs_rhs=[| (2, TVar(Local(0),Comp({},{ { `$A =
Int
} }))) |]; brs_stack_pos=0}),Const(3))",
"(match (fun f x : 'A[{}] : 'A[{}] -> x) : ('A[{}] -> 'A[{}]) with | y : ('A[{}] -> 'A[{}]) -> y[{A/Int}]).3";
"(match (fun f x : 'A : 'A -> x) : ('A -> 'A) with | y : ('A -> 'A) -> y[{A/Int}]).3";
......@@ -68,12 +68,12 @@ let tests_poly_abstr = [
(*
"Test CDuce.lambda.const_abstr failed",
"Abstraction(Dummy,,,,Sel((Int -> Int),{}))",
"fun f x : 'A[{A/Int}] : 'A[{A/Int}] -> 2";
"fun f x : 'A : 'A -> 2";
*)
"Test CDuce.lambda.const_abstr failed",
"Abstraction(Dummy,,,,Sel(,(Int -> Int),{}))",
"fun f x : Int : Int -> 2";
"(fun f x : 'A : 'A -> x)[{A/Int}].2";
];;
let tests_compile = "CDuce compile tests (Typed -> Lambda )" >:::
......@@ -208,10 +208,10 @@ let tests_eval = "CDuce runtime tests (Typed -> Lambda -> Value)" >:::
(Any,Any) |
<(Any) (Any)>Any |
Arrow)* ]),{})"
(run_test_eval "fun map f : ('A[{}]->'B[{}]) x : ['A[{}]] : ['B[{}]] ->
match x : ['A[{}]] with
| (el : 'A[{}]) :: [] -> f.el
| (el : 'A[{}]) :: (rest : ['A[{}]]) -> ((f.el), ((map.f).rest))");
(run_test_eval "fun map f : ('A -> 'B) x : ['A] : ['B] ->
match x : ['A] with
| (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), {}), {})"
......@@ -250,7 +250,7 @@ let tests_eval = "CDuce runtime tests (Typed -> Lambda -> Value)" >:::
| 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]");
| 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(nil), {}), {})"
......@@ -443,7 +443,7 @@ let tests_eval = "CDuce runtime tests (Typed -> Lambda -> Value)" >:::
~printer:(fun x -> x)
"Abstraction((`$A & Int | Char | Atom | (Any,Any) | <(Any) (Any)>Any | Arrow,
`$A & Int | Char | Atom | (Any,Any) | <(Any) (Any)>Any | Arrow),{})"
(run_test_eval "fun f x : 'A[{}] : 'A[{}] -> x");
(run_test_eval "fun f x : 'A : 'A -> x");
assert_equal ~msg:"Test CDuce.runtime.poly.identity failed"
~printer:(fun x -> x)
"Abstraction(([ Char* ] | Int, [ Char* ] | Int),{})"
......@@ -461,12 +461,12 @@ let tests_eval = "CDuce runtime tests (Typed -> Lambda -> Value)" >:::
"Abstraction(([ (`$A & Int | Char | Atom | (Any,Any) | <(Any) (Any)>Any |
Arrow)* ], [ (`$A & Int | Char | Atom | (Any,Any) |
<(Any) (Any)>Any | Arrow)* ]),{})"
(run_test_eval "fun tail x : ['A[{}]] : ['A[{}]] -> match x : ['A[{}]] with
| (_ : 'A[{}]) :: (rest : ['A[{}]]) -> rest");
(run_test_eval "fun tail x : ['A] : ['A] -> match x : ['A] with
| (_ : 'A) :: (rest : ['A]) -> rest");
assert_equal ~msg:"Test CDuce.runtime.poly.tail_applied failed"
~printer:(fun x -> x) "(7, (8, (5, Atom(nil), {}), {}), {})"
(run_test_eval "(fun tail x : ['A[{}]] : ['A[{}]] -> match x : ['A[{}]] with
| (_ : 'A[{}]) :: (rest : ['A[{}]]) -> rest).[3; 7; 8; 5]");
(run_test_eval "(fun tail x : ['A] : ['A] -> match x : ['A] with
| (_ : 'A) :: (rest : ['A]) -> rest).[3; 7; 8; 5]");
);
......
......@@ -23,7 +23,7 @@ and match_value =
| MBool of Loc.t * bool
and ptype =
| Type of string
| PType of string * (string * ptype) list list
| PType of string
| TPair of ptype * ptype
| TUnion of ptype * ptype
| TInter of ptype * ptype
......@@ -147,16 +147,16 @@ module ExprParser = struct
type_id: [
"atom_type" [ t = UIDENT -> Type(t) ]
| [ "'"; t1 = UIDENT; "["; s = LIST0 sigma SEP ","; "]" -> PType(t1, s) ]
| [ "'"; t = UIDENT -> PType(t) ]
| [ "("; t = complex_type_id; ")" -> t ]
| [ "["; t = complex_type_id; "]" -> TSeq(t) ]
];
complex_type_id: [ "complex_type" LEFTA
[ t = UIDENT -> Type(t)
[ t = UIDENT -> Type(t)
| "("; t = SELF; ")" -> t ]
| [ "'"; t1 = UIDENT; "["; s = LIST0 sigma SEP ","; "]" -> PType(t1, s) ]
| [ t1 = SELF; "*"; t2 = SELF -> TPair(t1, t2)
| [ "'"; t = UIDENT -> PType(t) ]
| [ t1 = SELF; "*"; t2 = SELF -> TPair(t1, t2)
| t1 = SELF; "->"; t2 = SELF -> TArrow(t1, t2) ]
| [ t1 = SELF; "|"; t2 = SELF -> TUnion(t1, t2)
| t1 = SELF; "&"; t2 = SELF -> TInter(t1, t2) ]
......
......@@ -22,7 +22,7 @@ and match_value =
| MBool of Loc.t * bool
and ptype =
| Type of string
| PType of string * (string * ptype) list list
| PType of string
| TPair of ptype * ptype
| TUnion of ptype * ptype
| TInter of ptype * ptype
......
......@@ -76,15 +76,15 @@ let tests_typer_list = [
"fun f (Int -> Int) x&Int -> x";
"Test CDuce.typed.fun.identity",
"fun f x : 'A[{}] : 'A[{}] -> x",
"fun f x : 'A : 'A -> x",
"fun f (`$A -> `$A) x -> x";
"Test CDuce.typed.fun.identity.int",
"fun f x : 'A[{A/Int}] : 'A[{A/Int}] -> 2",
"fun f x : 'A : 'A -> 2",
"fun f (`$A -> `$A) x -> x";
"Test CDuce.typed.fun.match",
"fun f x : ('A[{}] | Int) : ('A[{}] | Int) -> x",
"fun f x : ('A | Int) : ('A | Int) -> x",
"fun f (`$A -> `$A) x & Int -> x | x -> x";
]
......
......@@ -25,11 +25,11 @@ let run_test_compile msg expected totest =
let tests_poly_abstr = [
"Test CDuce.lambda.const_abstr failed",
"",
"fun f x : 'A[{A/Int}] : 'A[{A/Int}] -> 2";
"fun f x : 'A : 'A -> 2";
"Test CDuce.lambda.identity",
"",
"(fun f x : 'A[{A/Int}] : 'A[{A/Int}] -> x).2";
"(fun f x : 'A : 'A -> x)[{A/Int}].2";
"Test CDuce.lambda.let",
"",
......
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