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

Quickfix on some files; sigma added to tests/lambda

parent 2fd36622
......@@ -138,7 +138,8 @@ and compile_abstr env a =
let env = { env with vars = fun_env; stack_size = 0; max_stack = ref 0 } in
let body = compile_branches env a.Typed.fun_body in
let sigma = (* `Sel (x,t,env.sigma) *) `List [] in
if equal (inter vars(t) dom(env.sigma)) empty then
(* TODO: Fix this line *)
if (*equal (inter vars(t) dom(env.sigma)) empty*) true then
Abstraction (slots, a.Typed.fun_iface, body, !(env.max_stack), false, sigma)
else
Abstraction (slots, a.Typed.fun_iface, body, !(env.max_stack), true, sigma)
......@@ -155,9 +156,10 @@ and compile_branches env (brs : Typed.branches) =
}
(* p_i / t_i br.Typed.br_pat / br.Typed.br_type *)
(* TODO: Fix this function *)
and compile_branch env br =
let env = List.fold_left enter_local env (Patterns.fv br.Typed.br_pat) in
(br.Typed.br_pat, br.Typed.br_type, compile env br.Typed.br_body)
(br.Typed.br_pat(*, br.Typed.br_type*), compile env br.Typed.br_body)
let enter_globals env n = match env.cu with
| None -> List.fold_left enter_global_toplevel env n
......
open Ident
open Encodings
type sigma = [
| `List of Types.Tallying.CS.sl
| `Comp of (sigma * sigma)
| `Sel of (fv * Types.t * sigma) ]
val esigma : sigma
type t =
(* Canonical representation *)
| Pair of t * t
| Xml of t * t * t
| XmlNs of t * t * t * Ns.table
| Record of t Imap.t
| Pair of t * t * sigma
| Xml of t * t * t * sigma
| XmlNs of t * t * t * Ns.table * sigma
| Record of t Imap.t * sigma
| Atom of Atoms.V.t
| Integer of Intervals.V.t
| Char of Chars.V.t
| Abstraction of (Types.descr * Types.descr) list option * (t -> t)
| Abstraction of (Types.descr * Types.descr) list option * (t -> t) * sigma
| Abstract of Types.Abstract.V.t
(* Derived forms *)
| String_latin1 of int * int * string * t
| String_utf8 of U.uindex * U.uindex * U.t * t
| String_utf8 of Utf8.uindex * Utf8.uindex * Utf8.t * t
| Concat of t * t
(* Special value for absent record fields, and failed pattern matching *)
| Absent
module ValueSet: Set.S with type elt = t
......
......@@ -4,10 +4,14 @@ expr = id
| abstr
| expr "." expr
| expr "," expr
| expr "{" id "/" type_id sigma "}"
| "(" expr ")"
| "[" listexpr "]"
| "match" expr ":" type_id "with" "|" match_value "->" expr branches
sigma = (* empty *)
| ";" id "/" type_id
listexpr = (* empty *)
| expr
| listexpr ";" listexpr
......
......@@ -45,7 +45,11 @@ let rec _to_typed env l expr =
(* From Camlp4 locations to CDuce locations *)
let loc = caml_loc_to_cduce (get_loc expr) in
match expr with
| Parse.Apply (_, e1, e2) ->
| 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 [])) }
| Apply (_, 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=empty; exp_descr=Apply(e1, e2) }
......@@ -85,6 +89,11 @@ 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 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 =
let brloc = caml_loc_to_cduce (get_loc body) in
......
......@@ -142,6 +142,19 @@ let tests = "CDuce runtime tests" >:::
| x : String -> \"Piece of cake\").\"test\"");
);
"poly" >:: ( fun test_ctxt ->
assert_equal ~msg:"Test CDuce.runtime.poly.identity failed"
~printer:(fun x -> x) "Abstraction((Any, Any))"
(run_test "((fun f x : 'A : 'A -> 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");
(* 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");
);
]
let _ = run_test_tt_main tests
......@@ -2,6 +2,7 @@ open Printf
open Camlp4.PreCast
type expr =
| Subst of Loc.t * expr * (string * ptype) list
| Apply of Loc.t * expr * expr
| Abstr of Loc.t * fun_name * params * ptype * expr
| Match of Loc.t * expr * ptype * branches
......@@ -38,7 +39,7 @@ module ExprParser = struct
expression:
[
"abstr" RIGHTA
"abstr" RIGHTA
[ "fun"; x = LIDENT; p = LIST1 param; ":"; t = type_id; "->";
e = SELF -> Abstr(_loc, x, p, t, e)
| "match"; e = SELF; ":"; t = type_id; "with"; b = LIST1 branch ->
......@@ -51,8 +52,13 @@ module ExprParser = struct
| "var" [ x = LIDENT -> Var(_loc, x) ]
| "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) ]
];
sigma: [[ ";"; x = UIDENT; "/"; t = type_id -> x, t ]];
listexpr:[ "rec" RIGHTA [ l1=SELF; ";"; l2=SELF -> Pair(_loc, l1, l2) ]
| [ e=expression -> e]];
......@@ -93,6 +99,7 @@ module ExprParser = struct
end
let get_loc expr = match expr with
| Subst (loc, _, _) -> loc
| Apply (loc, _, _) -> loc
| Abstr (loc, _, _, _, _) -> loc
| Match (loc, _, _, _) -> loc
......
open Camlp4.PreCast
type expr =
| Subst of Loc.t * expr * (string * ptype) list
| Apply of Loc.t * expr * expr
| Abstr of Loc.t * fun_name * params * ptype * expr
| Match of Loc.t * expr * ptype * branches
......
......@@ -113,15 +113,15 @@ let print_env env = match Ident.Env.is_empty env with
| false -> Ident.Env.iter print_binding env
let rec print_value v = match v with
| Value.Pair(v1, v2) -> printf "("; print_value v1; printf ", ";
| Value.Pair(v1, v2, _) -> printf "("; print_value v1; printf ", ";
print_value v2; printf ")"
| Xml(_,_,_) -> printf "Xml"
| XmlNs(_,_,_,_) -> printf "XmlNs"
| Xml(_) -> printf "Xml"
| XmlNs(_) -> printf "XmlNs"
| Record(_) -> printf "Record"
| Atom(_) -> printf "Atom"
| Integer(i) -> printf "%d" (Big_int.int_of_big_int i)
| Char(i) -> printf "Char()"
| Abstraction(_, _) -> printf "Abstraction()"
| Abstraction(_) -> printf "Abstraction()"
| Abstract((name, _)) -> printf "Abstract(%s)" name
| String_latin1(i1, i2, s, v) -> printf "String_latin1(%d, %d, %s)" i1 i2 s;
print_value v
......@@ -131,15 +131,15 @@ let rec print_value v = match v with
| Absent -> printf "Absent"
let rec value_to_string v = match v with
| Value.Pair(v1, v2) -> "(" ^ (value_to_string v1) ^ ", "
| Value.Pair(v1, v2, _) -> "(" ^ (value_to_string v1) ^ ", "
^ (value_to_string v2) ^ ")"
| Xml(_,_,_) -> "Xml"
| XmlNs(_,_,_,_) -> "XmlNs"
| Xml(_) -> "Xml"
| XmlNs(_) -> "XmlNs"
| Record(_) -> "Record"
| Atom(_) -> "Atom"
| Integer(i) -> string_of_int (Big_int.int_of_big_int i)
| Char(i) -> "Char()"
| Abstraction(t, _) ->
| Abstraction(t, _, _) ->
let t = match t with | Some t -> iface t | None -> "None" in
"Abstraction(" ^ t ^ ")"
| Abstract((name, _)) -> "Abstract(" ^ name ^ ")"
......
......@@ -868,6 +868,9 @@ and type_check' loc env e constr precise = match e with
ignore (type_check env e t false);
verify loc t constr
(* TODO: Fix this branch *)
| Subst (e, sigma) -> type_check env e constr precise
| Check (t0,e,t) ->
let te = type_check env e Types.any true in
t0 := Types.cup !t0 te;
......
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