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

[TESTS][LAMBDA] Sigma is now mandatory for a polymorphic variable

parent 31fd33bc
......@@ -36,11 +36,13 @@ id = [a-z_][A-Za-z0-9_]*
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 "]"
| "(" 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 "*" complex_type_id
| complex_type_id "|" complex_type_id
| complex_type_id "&" complex_type_id
......
......@@ -17,30 +17,6 @@ let type_of_string s = match s with
| "Char" -> char Chars.any
| _ -> empty
let rec type_of_ptype arg = match arg with
| Type(t) -> type_of_string t
| PType(t) -> var (`Var (Var.make_id t)) (* TODO: Add sigma *)
| 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)
| TNot(t) -> neg (type_of_ptype t)
| TArrow(t1, t2) -> arrow (cons (type_of_ptype t1)) (cons (type_of_ptype t2))
| TSeq(t) -> Sequence.star (type_of_ptype t)
let rec type_of_iface iface rtype =
let rec _type_of_iface iface rtype res =
match iface with
| (_, pname, ptype) :: rest -> _type_of_iface rest rtype
(arrow (cons res) (cons (type_of_ptype ptype)))
| [] -> arrow (cons res) (cons rtype)
in
match iface with
| (_, pname, ptype) :: [] -> arrow (cons (type_of_ptype ptype)) (cons rtype)
| (_, pname, ptype) :: (_, pname2, ptype2) :: rest ->
let res = type_of_ptype ptype2 in
arrow (cons (type_of_ptype ptype)) (cons (_type_of_iface rest rtype res))
| [] -> assert false
let rec _to_typed env l expr =
(* From Camlp4 locations to CDuce locations *)
let loc = caml_loc_to_cduce (get_loc expr) in
......@@ -48,7 +24,7 @@ let rec _to_typed env l expr =
| Subst (_, e, s) ->
let _, _, e = _to_typed env l e in
env, l, { exp_loc=loc; exp_typ=empty;
exp_descr=(Subst (e, make_sigma s [])) }
exp_descr=(Subst (e, make_sigma s)) }
| Apply (_, e1, e2) ->
let _, _, e1 = _to_typed env l e1 in
let _, _, e2 = _to_typed env l e2 in
......@@ -89,10 +65,47 @@ let rec _to_typed env l expr =
env, l, { exp_loc=loc; exp_typ=(type_of_string "String");
exp_descr=Cst s }
and make_sigma s res = match s with
| (name, ptype) :: rest ->
make_sigma rest ([`Var (Var.make_id name), type_of_ptype ptype] :: res)
| [] -> res
and make_sigma s =
let rec _make_sigma s res = match s with
| (name, ptype) :: rest ->
_make_sigma rest ([`Var (Var.make_id name), type_of_ptype ptype] :: res)
| [] -> res
in
_make_sigma s []
and type_of_sigma x s =
let rec _type_of_sigma x s res = match s with
| [] -> res
| (id, t2) :: rest ->
if id = x then _type_of_sigma x rest (cup res (type_of_ptype t2))
else _type_of_sigma x rest res
in
_type_of_sigma x s empty
and type_of_ptype arg = match arg with
| Type(t) -> type_of_string t
| PType(t, s) ->
if s = [] then var (`Var (Var.make_id t)) else type_of_sigma t s
| 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)
| TNot(t) -> neg (type_of_ptype t)
| TArrow(t1, t2) -> arrow (cons (type_of_ptype t1)) (cons (type_of_ptype t2))
| TSeq(t) -> Sequence.star (type_of_ptype t)
and type_of_iface iface rtype =
let rec _type_of_iface iface rtype res =
match iface with
| (_, pname, ptype) :: rest -> _type_of_iface rest rtype
(arrow (cons res) (cons (type_of_ptype ptype)))
| [] -> arrow (cons res) (cons rtype)
in
match iface with
| (_, pname, ptype) :: [] -> arrow (cons (type_of_ptype ptype)) (cons rtype)
| (_, pname, ptype) :: (_, pname2, ptype2) :: rest ->
let res = type_of_ptype ptype2 in
arrow (cons (type_of_ptype ptype)) (cons (_type_of_iface rest rtype res))
| [] -> assert false
and parse_abstr env l fv loc fun_name params rtype body =
let rec _parse_abstr env l oldfv loc fun_name params rtype body nb =
......
......@@ -143,19 +143,17 @@ let tests = "CDuce runtime tests" >:::
);
"poly" >:: ( fun test_ctxt ->
(* TODO: Abstraction((`$A & Int | [Char*], `$A & Int | [Char*])) *)
assert_equal ~msg:"Test CDuce.runtime.poly.identity failed"
~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 "((fun f x : 'A : 'A -> x){A/Int;A/String})");
"Abstraction(([ Char* ] | Int, [ Char* ] | Int))"
(run_test "((fun f x : 'A{A/Int;A/String} : 'A{A/Int;A/String} -> x){A/Int;A/String})");
assert_equal ~msg:"Test CDuce.runtime.poly.identity_applied failed"
~printer:(fun x -> x) "2"
(run_test "((fun f x : 'A : 'A -> x){A/Int;A/String}).2");
(run_test "((fun f x : 'A{A/Int;A/String} : 'A{A/Int;A/String} -> x){A/Int;A/String}).2");
(* TODO: Should have error (?) *)
assert_equal ~msg:"Test CDuce.runtime.poly.identity_applied2 failed"
~printer:(fun x -> x) "2"
(run_test "((fun f x : 'A : 'A -> x){A/String}).2");
(run_test "((fun f x : 'A{A/String} : 'A{A/String} -> x){A/String}).2");
);
]
......
......@@ -20,7 +20,7 @@ and match_value =
| MString of Loc.t * string
and ptype =
| Type of string
| PType of string
| PType of string * (string * ptype) list
| TPair of ptype * ptype
| TUnion of ptype * ptype
| TInter of ptype * ptype
......@@ -53,11 +53,10 @@ module ExprParser = struct
| "int" [ x = INT -> Int(_loc, int_of_string x) ]
| "string" [ x = STRING -> String(_loc, x) ]
| "subst" NONA
[ e = SELF; "{"; x = UIDENT; "/"; t = type_id; s = LIST0 sigma;
"}" -> Subst(_loc, e, (x,t) :: s) ]
[ e = SELF; "{"; s = LIST1 sigma SEP ";"; "}" -> Subst(_loc, e, s) ]
];
sigma: [[ ";"; x = UIDENT; "/"; t = type_id -> x, t ]];
sigma: [[ x = UIDENT; "/"; t = type_id -> x, t ]];
listexpr:[ "rec" RIGHTA [ l1=SELF; ";"; l2=SELF -> Pair(_loc, l1, l2) ]
| [ e=expression -> e]];
......@@ -78,13 +77,15 @@ module ExprParser = struct
];
type_id: [ "atom_type" [ t = UIDENT -> Type(t) ]
| [ "'"; t = UIDENT -> PType(t) ]
| [ "'"; t1 = UIDENT; "{"; s = LIST0 sigma SEP ";"; "}" ->
PType(t1, s) ]
| [ "("; t = complex_type_id; ")" -> t ]
| [ "["; t = complex_type_id; "]" -> TSeq(t) ]];
complex_type_id: [ "complex_type" LEFTA [ t = UIDENT -> Type(t)
| "("; t = SELF; ")" -> t ]
| [ "'"; t = UIDENT -> PType(t) ]
| [ "'"; t1 = UIDENT; "{"; s = LIST0 sigma SEP ";"; "}" ->
PType(t1, s) ]
| [ t1 = SELF; "*"; t2 = SELF -> TPair(t1, t2)
| t1 = SELF; "->"; t2 = SELF -> TArrow(t1, t2) ]
| [ t1 = SELF; "|"; t2 = SELF -> TUnion(t1, t2)
......
......@@ -19,7 +19,7 @@ and match_value =
| MString of Loc.t * string
and ptype =
| Type of string
| PType of string
| PType of string * (string * ptype) list
| TPair of ptype * ptype
| TUnion of ptype * ptype
| TInter of ptype * ptype
......
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