Skip to content

GitLab

Commit 337588ee authored by Pietro Abate's avatar Pietro Abate
Browse files

Merge branch 'eval-test' of https://git.cduce.org/cduce into eval-test

parents e6237c90 71c094b0
Expand all Hide whitespace changes
Inline Side-by-side
compile/compile.ml
View file @ 337588ee
......@@ -177,10 +177,18 @@ and compile_branches env (brs : Typed.branches) =
(* p_i / t_i -> br.Typed.br_pat / br.Typed.br_type
* p_i / t_i is used here to add elements to env.gamma *)
and compile_branch env br =
let env = List.fold_left enter_local env (Patterns.fv br.Typed.br_pat) in
let m = Patterns.filter (Types.descr (Patterns.accept br.Typed.br_pat)) br.Typed.br_pat in
(* We add a fresh variable "pat<nb>:x" for each pattern
TODO: Add a fresh variable for cap too. *)
let t, _, d = br.Typed.br_pat.Patterns.descr in
let fv = match d with
| Patterns.Constr(_) | Patterns.Cap(_) -> Patterns.fv br.Typed.br_pat
| _ -> incr Patterns.counter; (Patterns.fv br.Typed.br_pat)
@ [!Patterns.counter, "pat" ^ (string_of_int !Patterns.counter) ^ ":x"] in
let pat = { br.Typed.br_pat with Patterns.descr=(t,fv,d); Patterns.fv=fv } in
let env = List.fold_left enter_local env fv in
let m = Patterns.filter (Types.descr (Patterns.accept pat)) pat in
let env = { env with gamma = IdMap.union_disj m env.gamma } in
(br.Typed.br_pat, compile env br.Typed.br_body )
(pat, compile env br.Typed.br_body )
let enter_globals env n = match env.cu with
| None -> List.fold_left enter_global_toplevel env n
......
tests/lambda/GRAMMAR
View file @ 337588ee
......@@ -5,21 +5,29 @@ expr = id
| STRING
| abstr
| "let" LIDENT ":" type_id "=" expr "in" expr ":" type_id
| "if" expr "then" expr
| "if" expr "then" expr "else" expr
| expr "." expr
| expr "," expr
| expr "=" expr
| expr "+" expr
| expr "-" expr
| expr "*" expr
| 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 +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 "{" 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 @ 337588ee
......@@ -99,27 +99,31 @@ 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 =
let open Types in function
| Type(t) -> type_of_string t
| PType(t, s) ->
if s = [] then var (`Var (Var.make_id t)) else type_of_sigma 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)
......@@ -248,6 +252,20 @@ and parse_match_value env l list toptype = function
let is_subtype = Types.subtype (type_of_string "String")
(type_of_ptype toptype) in
(t, Patterns.Constr(t), list, l, is_subtype)
| MBool (origloc, b) ->
let t = match b with
| "true" -> Types.atom (Atoms.atom (Atoms.V.mk_ascii "true"))
| "false" -> Types.atom (Atoms.atom (Atoms.V.mk_ascii "false"))
| _ ->
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
Printf.eprintf
"File %s, line %d, characters %d-%d:\nError: Unknown special term %s\n"
(Loc.file_name origloc) line cbegin cend b;
raise Error in
let is_subtype = Types.subtype t (type_of_ptype toptype) in
(t, Patterns.Constr(t), list, l, is_subtype)
let arith_op f = function
| Value.Integer(x) :: Value.Integer(y) :: [] ->
......@@ -255,6 +273,12 @@ let arith_op f = function
(Big_int.int_of_big_int y)))
| _ -> raise Error
let equal = function
| Value.Integer(x) :: Value.Integer(y) :: [] ->
let b = if Big_int.int_of_big_int x = Big_int.int_of_big_int y then "true"
else "false" in Value.Atom(Atoms.V.mk_ascii b)
| _ -> raise Error
let concat =
let rec add_to_tail y = function
| Value.Pair(x, nil, s) ->
......@@ -276,6 +300,7 @@ let to_typed expr =
Eval.register_op "*" (arith_op ( * ));
Eval.register_op "/" (arith_op ( / ));
Eval.register_op "%" (arith_op ( mod ));
Eval.register_op "=" equal;
Eval.register_op "@" concat;
let env, _, expr = _to_typed Compile.empty_toplevel Locals.empty expr in
env, expr
tests/lambda/src/main.ml
View file @ 337588ee
......@@ -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
......@@ -295,6 +295,10 @@ let tests_eval = "CDuce runtime tests (Typed -> Lambda -> Value)" >:::
~printer:(fun x -> x) "3"
(run_test_eval "(fun f x : Int : Int ->
match x : Int with | 1 -> 3 | _ : Int -> f.1).2");
assert_equal ~msg:"Test CDuce.runtime.match.desugar_if failed"
~printer:(fun x -> x) "0"
(run_test_eval "((fun f x : Int y : Int : Int ->
match (x = y) : Bool with | `true -> 0 | `false -> 1).2).2");
);
"string" >:: ( fun test_ctxt ->
......@@ -344,19 +348,26 @@ 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}]) ->
(match n : Int with | 0 -> el | _ : Int -> (nth.rest).(n-1))).[1; 2; 5; `true; 2].2");
(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)}]]) ->
(if n = 0 then el else nth.rest.(n-1))).[1; 2; 5; `true; 2].2");
assert_equal ~msg:"Test CDuce.runtime.list.rev failed"
~printer:(fun x -> x) "(2, (Atom(true), (5, (2, (1, Atom(nil), {}), {}), {}), {}), {})"
(run_test_eval "(fun rev l : ['A[{A/(Int|Bool)}]] : ['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)}]]) ->
(rev.rest) @ [el]).[1; 2; 5; `true; 2]");
);
"union" >:: ( fun test_ctxt ->
......@@ -410,30 +421,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 @ 337588ee
......@@ -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
......@@ -20,9 +20,10 @@ and match_value =
| MVar of Loc.t * string * ptype
| MInt of Loc.t * int
| MString of Loc.t * string
| MBool 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
......@@ -61,8 +62,18 @@ module ExprParser = struct
| "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])
| "if"; e1 = SELF; "then"; e2 = SELF ->
let b = [(_loc, MBool(_loc, "true"), e2);
(_loc, MBool(_loc, "false"), Var(_loc, "`nil"))] in
Match(_loc, e1, Type("Bool"), b)
| "if"; e1 = SELF; "then"; e2 = SELF; "else"; e3 = SELF ->
let b = [(_loc, MBool(_loc, "true"), e2);
(_loc, MBool(_loc, "false"), e3)] in
Match(_loc, e1, Type("Bool"), b)
| "match"; e = SELF; ":"; t = type_id; "with"; b = LIST1 branch ->
Match(_loc, e, t, b) ]
| "egal" LEFTA
[ e1 = SELF; "="; e2 = SELF -> Op(_loc, "=", e1, e2) ]
| "add" LEFTA
[ e1 = SELF; "+"; e2 = SELF -> Op(_loc, "+", e1, e2)
| e1 = SELF; "-"; e2 = SELF -> Op(_loc, "-", e1, e2) ]
......@@ -86,10 +97,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]];
......@@ -105,19 +118,20 @@ 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) ]
| "bool" [ "`"; x = LIDENT -> MBool(_loc, x) ]
| "empty" [ "["; "]" -> MVar(_loc, "`nil", Type("Any")) ]
];
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 @ 337588ee
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
......@@ -19,9 +19,10 @@ and match_value =
| MVar of Loc.t * string * ptype
| MInt of Loc.t * int
| MString of Loc.t * string
| MBool 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
......
types/types.ml
View file @ 337588ee
This diff is collapsed.
types/types.mli
View file @ 337588ee
......@@ -428,4 +428,10 @@ end
val apply : t -> t -> Tallying.CS.sl
val apply_full : t -> t -> t
val apply_raw : t -> t -> Tallying.CS.sl * (t*t)
val apply_raw : t -> t -> Tallying.CS.sl * t * t * t
(* apply_raw s t returns the 4-tuple (subst,ss, tt, res) where
subst is the set of substitution that make the application succeed,
ss and tt are the expansions of s and t corresponding to that substitution
and res is the type of the result of the application
*)
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