Skip to content

GitLab

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

[TESTS][LAMBDA] Fix on sigmas

parent 5bd01019
Hide whitespace changes
Inline Side-by-side
tests/lambda/GRAMMAR
View file @ e70c61c0
......@@ -13,13 +13,17 @@ expr = id
| expr "/" expr
| expr "%" expr
| expr "@" expr
| expr "{" UIDENT "/" type_id sigma "}" (* type substitutions *)
| expr "[" sigmalist "]" (* type substitutions *)
| "(" expr ")"
| "[" "]" (* nil *)
| "[" listexpr "]"
| "match" expr ":" type_id "with" "|" match_value "->" expr branches
;;
sigmalist = (* empty *)
| "{" "}" "," sigmalist
| "{" UIDENT "/" type_id sigma "}" "," sigmalist
sigma = (* empty *)
| ";" UIDENT "/" type_id
;;
......@@ -58,13 +62,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 "{" sigma "}"
| "'" UIDENT "[" sigmalist "]"
| "[" complex_type_id "]"
| "(" complex_type_id ")"
;;
complex_type_id = UIDENT (* [A-Z][A-Za-z0-9_]* *)
| "'" UIDENT "{" sigma "}"
| "'" UIDENT "[" sigmalist "]"
| complex_type_id "*" complex_type_id
| complex_type_id "|" complex_type_id
| complex_type_id "&" complex_type_id
......
tests/lambda/src/compute.ml
View file @ e70c61c0
......@@ -99,20 +99,24 @@ let rec _to_typed env l expr =
raise Error
and make_sigma s =
let rec aux acc = function
let rec aux2 acc = function
| (name, ptype) :: rest ->
aux ([`Var (Var.make_id name), type_of_ptype ptype] :: acc) rest
| [] -> acc
in
aux2 ((Var.mk name, type_of_ptype ptype) :: acc) rest
| [] -> acc in
let rec aux acc = function
| l :: rest -> aux (acc @ [aux2 [] l]) rest
| [] -> acc in
aux [] s
and type_of_sigma x s =
let rec aux x acc = function
let rec aux2 x acc = function
| [] -> acc
| (id, t2) :: rest when id = x ->
aux x (Types.cup acc (type_of_ptype t2)) rest
| _ :: rest -> aux x acc rest
in
aux2 x (Types.cap acc (type_of_ptype t2)) rest
| _ :: rest -> aux2 x acc rest in
let rec aux x acc = function
| [] -> acc
| l :: rest -> aux x (Types.cup acc (aux2 x Types.any l)) rest in
aux x Types.empty s
and type_of_ptype =
......
tests/lambda/src/main.ml
View file @ e70c61c0
......@@ -28,8 +28,8 @@ let tests_poly_abstr = [
"Test CDuce.lambda.poly.identity failed",
"Abstraction(Dummy,,,,Sel(,([ Char* ] | Int -> [ Char* ] | Int),Comp({},{ { (`$A/
[ Char* ]) } ,{ (`$A/Int) } })))",
"(fun f x : 'A{A/Int;A/String} : 'A{A/Int;A/String} -> x) {A/Int;A/String}";
Int) } ,{ (`$A/[ Char* ]) } })))",
"(fun f x : 'A[{A/Int},{A/String}] : 'A[{A/Int},{A/String}] -> x) [{A/Int},{A/String}]";
"Test CDuce.runtime.poly.tail failed",
"Abstraction(Dummy,,,,Sel(,([ (`$A & Int | Char | Atom | (Any,Any) |
......@@ -39,16 +39,16 @@ let tests_poly_abstr = [
(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 (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";
......@@ -186,16 +186,16 @@ 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), {}), {})"
(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))
(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
......@@ -204,9 +204,9 @@ let tests_eval = "CDuce runtime tests (Typed -> Lambda -> Value)" >:::
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))
(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
......@@ -221,20 +221,20 @@ let tests_eval = "CDuce runtime tests (Typed -> Lambda -> Value)" >:::
(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))
(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]");
| 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), {}), {})"
(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))
(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) & (Bool -> Bool) & ((!(Int|Bool)) -> (!(Int|Bool))))
| x : Int -> `true
| x : Bool -> `false
......@@ -242,9 +242,9 @@ let tests_eval = "CDuce runtime tests (Typed -> Lambda -> Value)" >:::
assert_equal ~msg:"Test CDuce.runtime.misc.map_is_int_medium failed"
~printer:(fun x -> x)
"(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))
(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) & (Bool -> Bool) & ((!(Int|Bool)) -> (!(Int|Bool))))
| x : Int -> `true
| x : Bool -> `false
......@@ -344,18 +344,18 @@ let tests_eval = "CDuce runtime tests (Typed -> Lambda -> Value)" >:::
| (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
(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)
| (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}]) ->
(run_test_eval "(fun nth l : ['A[{A/(Int|Bool)}]] n : Int : 'A[{A/(Int|Bool)}] ->
match l : ['A[{A/(Int|Bool)}]] with
| (el : 'A[{A/(Int|Bool)}]) :: [] -> el
| (el : 'A[{A/(Int|Bool)}]) :: (rest : ['A[{A/(Int|Bool)}]]) ->
(match n : Int with | 0 -> el | _ : Int -> (nth.rest).(n-1))).[1; 2; 5; `true; 2].2");
);
......@@ -410,30 +410,30 @@ 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),{})"
(run_test_eval "(fun f x : 'A{A/Int;A/String} : 'A{A/Int;A/String} -> x)
{A/Int;A/String}");
(run_test_eval "(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_eval "((fun f x : 'A{A/Int;A/String} : 'A{A/Int;A/String} -> x)
{A/Int;A/String}).2");
(run_test_eval "((fun f x : 'A[{A/Int},{A/String}] : 'A[{A/Int},{A/String}] -> x)
[{A/Int},{A/String}]).2");
assert_equal ~msg:"Test CDuce.runtime.poly.identity_applied2 failed"
~printer:(fun x -> x) "2"
(run_test_eval "((fun f x : 'A{A/String} : 'A{A/String} -> x){A/String}).2");
(run_test_eval "((fun f x : 'A[{A/String}] : 'A[{A/String}] -> x)[{A/String}]).2");
assert_equal ~msg:"Test CDuce.runtime.poly.tail 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_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]");
);
......
tests/lambda/src/parse.ml
View file @ e70c61c0
......@@ -2,7 +2,7 @@ open Printf
open Camlp4.PreCast
type expr =
| Subst of Loc.t * expr * (string * ptype) list
| Subst of Loc.t * expr * (string * ptype) list list
| Apply of Loc.t * expr * expr
| Abstr of Loc.t * fun_name * ptype * fv * branches
| Match of Loc.t * expr * ptype * branches
......@@ -22,7 +22,7 @@ and match_value =
| MString of Loc.t * string
and ptype =
| Type of string
| PType of string * (string * ptype) list
| PType of string * (string * ptype) list list
| TPair of ptype * ptype
| TUnion of ptype * ptype
| TInter of ptype * ptype
......@@ -86,10 +86,12 @@ module ExprParser = struct
| "string" [ x = STRING -> String(_loc, x) ]
| "bool" [ "`"; x = LIDENT -> Bool(_loc, x) ]
| "subst" NONA
[ e = SELF; "{"; s = LIST1 sigma SEP ";"; "}" -> Subst(_loc, e, s) ]
[ e = SELF; "["; s = LIST0 sigma SEP ","; "]" -> Subst(_loc, e, s) ]
];
sigma: [[ x = UIDENT; "/"; t = type_id -> x, t ]];
sigma:[[ "{"; l = LIST0 subst SEP ";"; "}" -> l ]];
subst:[[ x = UIDENT; "/"; t = type_id -> x, t ]];
param:[[p = LIDENT; ":"; t = type_id -> _loc, p, t]];
......@@ -110,14 +112,14 @@ module ExprParser = struct
type_id: [ "atom_type"
[ t = UIDENT -> Type(t) ]
| [ "'"; t1 = UIDENT; "{"; s = LIST0 sigma SEP ";"; "}" -> PType(t1, s) ]
| [ "'"; 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 ]
| [ "'"; t1 = UIDENT; "{"; s = LIST0 sigma SEP ";"; "}" -> PType(t1, s) ]
| [ "'"; 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) | t1 = SELF; "&"; t2 = SELF -> TInter(t1, t2) ]
| [ "!"; t = SELF -> TNot(t) ]
......
tests/lambda/src/parse.mli
View file @ e70c61c0
open Camlp4.PreCast
type expr =
| Subst of Loc.t * expr * (string * ptype) list
| Subst of Loc.t * expr * (string * ptype) list list
| Apply of Loc.t * expr * expr
| Abstr of Loc.t * fun_name * ptype * fv * branches
| Match of Loc.t * expr * ptype * branches
......@@ -21,7 +21,7 @@ and match_value =
| MString of Loc.t * string
and ptype =
| Type of string
| PType of string * (string * ptype) list
| PType of string * (string * ptype) list 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