Commit 7d0521c9 authored by Pietro Abate's avatar Pietro Abate

WIP

parent 9c8651cd
......@@ -4,6 +4,8 @@ open Lambda
type env = {
cu: Compunit.t option; (* None: toplevel *)
vars: var_loc Env.t;
sigma : sigma;
gamma : var_loc Env.t;
stack_size: int;
max_stack: int ref;
global_size: int
......@@ -55,7 +57,11 @@ and compile_aux env = function
let d = Patterns.Compile.make_checker !t0 (Types.descr t) in
Check (compile env e, d)
| Typed.Var x -> Var (find x env)
| Typed.TVar x -> Var (find x env)
| Typed.TVar x ->
let v = find x env in
if env.sigma = [[]] && not (find v dom(env.sigma)) then Var (v)
else TVar(x,env.sigma)
| Typed.Subst(e,sl) -> compile { env with sigma = Comp(env.sigma,List sl) } e
| Typed.ExtVar (cu,x,_) -> Var (find_ext cu x)
| Typed.Apply (e1,e2) -> Apply (compile env e1, compile env e2)
| Typed.Abstraction a -> compile_abstr env a
......@@ -122,22 +128,27 @@ and compile_abstr env a =
let slots = Array.of_list (List.rev slots) in
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
Abstraction (slots, a.Typed.fun_iface, body, !(env.max_stack), true, List [[]])
let sigma = Sel (x,t,env.sigma) in
if equal (inter vars(t) dom(env.sigma)) empty 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)
and compile_branches env (brs : Typed.branches) =
(* Don't compile unused branches, because they have not been
type checked. *)
(* Don't compile unused branches, because they have not been type checked. *)
let used = List.filter (fun br -> br.Typed.br_used) brs.Typed.br_branches in
let b = List.map (compile_branch env) used in
let (disp,rhs) = Patterns.Compile.make_branches brs.Typed.br_typ b in
{ brs_stack_pos = env.stack_size;
brs_accept_chars = not (Types.Char.is_empty brs.Typed.br_accept);
brs_disp = disp;
brs_rhs = rhs }
brs_rhs = rhs
}
(* p_i / t_i br.Typed.br_pat / br.Typed.br_type *)
and compile_branch env br =
let env = List.fold_left enter_local env (Patterns.fv br.Typed.br_pat) in
(br.Typed.br_pat, 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
......
......@@ -29,16 +29,16 @@ type sigma =
type expr =
| Var of var_loc
| PVar of (var_loc * sigma)
| TVar of (var_loc * sigma)
| Apply of expr * expr
| Abstraction of var_loc array * (Types.t * Types.t) list * branches * int * bool * sigma
(* environment, interface, branches, size of locals *)
(* environment, interface, branches, size of locals, eval flag, substitutions *)
| Check of expr * Auto_pat.state
| Const of Value.t
| Pair of expr * expr
| Xml of expr * expr * expr
| XmlNs of expr * expr * expr * Ns.table
| Record of expr Imap.t
| Pair of expr * expr * sigma
| Xml of expr * expr * expr * sigma
| XmlNs of expr * expr * expr * Ns.table * sigma
| Record of expr Imap.t * sigma
| String of U.uindex * U.uindex * U.t * expr
| Match of expr * branches
| Map of expr * branches
......
......@@ -29,7 +29,7 @@ type sigma =
type expr =
| Var of var_loc
| PVar of (var_loc * sigma)
| TVar of (var_loc * sigma)
| Apply of expr * expr
| Abstraction of var_loc array * (Types.t * Types.t) list * branches * int * bool * sigma
(* environment, interface, branches, size of locals *)
......
......@@ -15,7 +15,6 @@ let make_accu () = Value.Pair(nil,Absent)
let get_accu a = snd (Obj.magic a)
let map f v = let acc0 = make_accu () in set_cdr (f acc0 v) nil; get_accu acc0
let rec ensure a i =
let n = Array.length !a in
if i >= n then (
......@@ -34,7 +33,6 @@ let set a i x =
let globs = ref (Array.create 64 Value.Absent)
let nglobs = ref 0
let get_globals = ref (fun cu -> assert false)
let get_external = ref (fun cu pos -> assert false)
let set_external = ref (fun cu pos -> assert false)
......@@ -66,6 +64,7 @@ let eval_var env locals = function
let tag_op_resolved = Obj.tag (Obj.repr (OpResolved ((fun _ -> assert false), [])))
let tag_const = Obj.tag (Obj.repr (Const (Obj.magic 0)))
(* env is an array implementing de bruines indexes *)
let rec eval env locals = function
| Var ((Global _ | Ext _ | External _ | Builtin _) as x) as e ->
let v = eval_var env locals x in
......@@ -73,10 +72,10 @@ let rec eval env locals = function
Obj.set_tag (Obj.repr e) tag_const;
v
(* variable evaluation will be split in PEnv and Env.
* PEnv and Env belong to the runtime labmda language
* PEnv and Env belong to the runtime lambda language
* from the parsing ast + typing information *)
| Var x -> eval_var env locals x
| PVar (x,sigma) -> eval_var env locals x
| TVar (x,sigma) -> eval_var env locals x
| Apply (e1,e2) ->
let v1 = eval env locals e1 in
let v2 = eval env locals e2 in
......
......@@ -193,11 +193,10 @@ let norm_tests () = [
"(`$A , Int) | (`$B , Bool))","(Int , (Int | Bool))", mk_s [
[P(V "A","Int");P(V "B","Int")]
];
(*
"(`$A1 -> `$B1) -> [ `$A1 ] -> [ `$B1 ]", "((Int -> Bool) | ((`$A \\ Int) -> (`$B \\ Int))) -> `$G", mk_s [
"(`$A -> `$B) -> [ `$A ] -> [ `$B ]", "((Int -> Bool) | ((`$A \\ Int) -> (`$B \\ Int))) -> `$Gamma", mk_s [
[P(V "A","Empty")]
];
*)
"Int -> Bool", "`$A", mk_s [[N("Int -> Bool",V "A")]];
"((`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))",Tallying.CS.sat;
......@@ -307,7 +306,8 @@ let tallying_tests = [
[("((`$A , Int) & (`$B , Bool))","(Int , (Int & Bool))")], [[]];
(* map even *)
[("(`$A -> `$B) -> [`$A] -> [`$B]","(Int -> Bool) & ((`$A \\ Int) -> (`$A \\ Int))")], [[]];
[("(`$A -> `$B) -> [`$A* ] -> [`$B* ]","((Int -> Bool) & ((`$A \\ Int) -> (`$A \\ Int)))")], [[]];
[("(`$A -> `$A)", "((Int -> Int) & (Bool -> Bool)) -> `$T")], mk_e []
]
let test_tallying =
......
......@@ -298,11 +298,12 @@ let memo_filter = ref MemoFilter.empty
let rec filter_descr t (_,fv,d) : Types.Positive.v id_map =
(* TODO: avoid is_empty t when t is not changing (Cap) *)
if Types.is_empty t
then empty_res fv
if Types.is_empty t then empty_res fv
else
match d with
| Constr _ -> IdMap.empty
| Constr t0 ->
if Types.subtype t t0 then IdMap.empty
else (empty_res fv) (* omega *)
| Cup ((a,_,_) as d1,d2) ->
IdMap.merge cup_res
(filter_descr (Types.cap t a) d1)
......@@ -330,7 +331,6 @@ and filter_prod ?kind fv p1 p2 t =
(empty_res fv)
(Types.Product.normal ?kind t)
and filter_node t p : Types.Positive.v id_map =
try MemoFilter.find (t,p) !memo_filter
with Not_found ->
......@@ -345,12 +345,12 @@ let filter t p =
let r = filter_node t p in
memo_filter := MemoFilter.empty;
IdMap.map Types.Positive.solve r
let filter_descr t p =
let r = filter_descr t p in
memo_filter := MemoFilter.empty;
IdMap.get (IdMap.map Types.Positive.solve r)
(* Factorization of capture variables and constant patterns *)
module Factorize = struct
......
......@@ -36,7 +36,6 @@ end
val accept : node -> Types.Node.t
val filter : Types.t -> node -> Types.Node.t id_map
(* Pattern matching: compilation *)
module Compile: sig
......@@ -44,5 +43,3 @@ module Compile: sig
val make_branches : Types.t -> (node * 'a) list -> state * 'a rhs array
val make_checker : Types.t -> Types.t -> state
end
......@@ -192,8 +192,8 @@ module TLV = struct
let print ppf x = if x.b then Set.print ";" ppf x.s
let dump ppf x =
Format.fprintf ppf "<b = %b ; f = {%a} ; s = {%a}>"
x.b Var.Set.dump x.f (Set.print ";") x.s
Format.fprintf ppf "<b = %b ; f = {%a} ; s = {%a}>"
x.b Var.Set.print x.f (Set.print ";") x.s
let mem v x = Set.mem v x.s
end
......
......@@ -161,7 +161,7 @@ sig
val times: v -> v -> v
val xml: v -> v -> v
val decompose : t -> v
(* val decompose : t -> v *)
val substitute : t -> (Var.var * t) -> t
val substituterec : t -> Var.var -> t
val solve: v -> Node.t
......
......@@ -19,8 +19,9 @@ type texpr =
{ exp_loc : loc;
mutable exp_typ : Types.t;
(* Currently exp_typ is not used. It will be used for compilation ! *)
exp_descr : texpr';
mutable exp_descr : texpr';
}
and texpr' =
| Forget of texpr * ttyp
| Check of (Types.t ref) * texpr * ttyp
......@@ -28,6 +29,8 @@ and texpr' =
| Var of id
(* polymorphic variable *)
| TVar of id
(* lazy substutiutions *)
| Subst of (texpr * Types.Tallying.CS.sl)
| ExtVar of Compunit.t * id * Types.t
| Apply of texpr * texpr
| Abstraction of abstr
......@@ -79,7 +82,8 @@ and branch = {
mutable br_used : bool;
br_ghost : bool;
mutable br_vars_empty : fv;
br_pat : tpat;
br_pat : tpat;
mutable br_type : Types.t; (* Type accepted by this branch *)
br_body : texpr
}
......@@ -50,6 +50,8 @@ type item =
type t = {
ids : item Env.t;
delta : Var.Set.t;
gamma : Var.var Env.t;
ns: Ns.table;
keep_ns: bool
}
......@@ -105,6 +107,8 @@ let type_schema env loc name uri =
let empty_env = {
ids = Env.empty;
delta = Var.Set.empty; (* set of bounded type variables *)
gamma = Env.empty; (* map from expression variables to types *)
ns = Ns.def_table;
keep_ns = false
}
......@@ -478,7 +482,7 @@ type branch = Branch of Typed.branch * branch list
let cur_branch : branch list ref = ref []
let exp' loc e =
{ Typed.exp_loc = loc; Typed.exp_typ = Types.empty; Typed.exp_descr = e; }
{ Typed.exp_loc = loc; Typed.exp_typ = Types.empty; Typed.exp_descr = e }
let exp loc fv e = fv, exp' loc e
......@@ -725,7 +729,8 @@ and branches env b =
let x = Ident.to_string x in
warning br_loc
("The capture variable " ^ x ^
" is declared in the pattern but not used in the body of this branch. It might be a misspelled or undeclared type or name (if it isn't, use _ instead)."));
" is declared in the pattern but not used in the body of this branch." ^
" It might be a misspelled or undeclared type or name (if it isn't, use _ instead)."));
let fv2 = Fv.diff fv2 fvp in
fv := Fv.cup !fv fv2;
accept := Types.cup !accept (Types.descr (Patterns.accept p));
......@@ -818,10 +823,10 @@ let let_decl env p e =
open Typed
let localize loc f x =
try f x
with
| (Error _ | Constraint (_,_)) as exn -> raise (Cduce_loc.Location (loc,`Full,exn))
| Warning (s,t) -> warning loc s; t
try f x with
| (Error _ | Constraint (_,_)) as exn ->
raise (Cduce_loc.Location (loc,`Full,exn))
| Warning (s,t) -> warning loc s; t
let require loc t s =
if not (Types.subtype t s) then raise_loc loc (Constraint (t, s))
......@@ -857,31 +862,31 @@ let flatten arg constr precise =
let rec type_check env e constr precise =
let d = type_check' e.exp_loc env e.exp_descr constr precise in
let (ed,d) = type_check' e.exp_loc env e.exp_descr constr precise in
let d = if precise then d else constr in
e.exp_typ <- Types.cup e.exp_typ d;
e.exp_descr <- ed;
d
and type_check' loc env e constr precise = match e with
and type_check' loc env ed constr precise = match ed with
| Forget (e,t) ->
let t = Types.descr t in
ignore (type_check env e t false);
verify loc t constr
(ed,verify loc t constr)
| Check (t0,e,t) ->
let te = type_check env e Types.any true in
t0 := Types.cup !t0 te;
verify loc (Types.cap te (Types.descr t)) constr
(ed,verify loc (Types.cap te (Types.descr t)) constr)
| Abstraction a ->
let t =
try Types.Arrow.check_strenghten a.fun_typ constr
with Not_found ->
should_have loc constr
"but the interface of the abstraction is not compatible"
try Types.Arrow.check_strenghten a.fun_typ constr
with Not_found ->
should_have loc constr
"but the interface of the abstraction is not compatible"
in
let env =
match a.fun_name with
let env = match a.fun_name with
| None -> env
| Some f -> enter_value f a.fun_typ env
in
......@@ -891,31 +896,31 @@ and type_check' loc env e constr precise = match e with
raise_loc loc (NonExhaustive (Types.diff t1 acc));
ignore (type_check_branches loc env t1 a.fun_body t2 false)
) a.fun_iface;
t
(ed,t)
| Match (e,b) ->
let t = type_check env e b.br_accept true in
type_check_branches loc env t b constr precise
(Match(e.exp_descr,b),type_check_branches loc env t b constr precise)
| Try (e,b) ->
let te = type_check env e constr precise in
let tb = type_check_branches loc env Types.any b constr precise in
Types.cup te tb
(ed,Types.cup te tb)
| Pair (e1,e2) ->
type_check_pair loc env e1 e2 constr precise
(ed,type_check_pair loc env e1 e2 constr precise)
| Xml (e1,e2,_) ->
type_check_pair ~kind:`XML loc env e1 e2 constr precise
(ed,type_check_pair ~kind:`XML loc env e1 e2 constr precise)
| RecordLitt r ->
type_record loc env r constr precise
(ed,type_record loc env r constr precise)
| Map (e,b) ->
type_map loc env false e b constr precise
(ed,type_map loc env false e b constr precise)
| Transform (e,b) ->
localize loc (flatten (type_map loc env true e b) constr) precise
(ed,localize loc (flatten (type_map loc env true e b) constr) precise)
| Apply (e1,e2) ->
let t1 = type_check env e1 Types.Arrow.any true in
......@@ -925,46 +930,51 @@ and type_check' loc env e constr precise = match e with
if Types.Arrow.need_arg t1 then
let t2 = type_check env e2 dom true in
Types.Arrow.apply t1 t2
else
(ignore (type_check env e2 dom false); Types.Arrow.apply_noarg t1)
else begin
ignore (type_check env e2 dom false);
Types.Arrow.apply_noarg t1
end
in
verify loc res constr
(ed,verify loc res constr)
| Var s ->
verify loc (find_value s env) constr
(ed,verify loc (find_value s env) constr)
| TVar s ->
verify loc (find_value s env) constr
(ed,verify loc (find_value s env) constr)
| ExtVar (cu,s,t) ->
verify loc t constr
(ed,verify loc t constr)
| Cst c ->
verify loc (Types.constant c) constr
(ed,verify loc (Types.constant c) constr)
| String (i,j,s,e) ->
type_check_string loc env 0 s i j e constr precise
(ed,type_check_string loc env 0 s i j e constr precise)
| Dot (e,l) ->
let expect_rec = Types.record l (Types.cons constr) in
let expect_elt =
Types.xml
Types.any_node
(Types.cons (Types.times (Types.cons expect_rec) Types.any_node)) in
(Types.cons (Types.times (Types.cons expect_rec) Types.any_node))
in
let t = type_check env e (Types.cup expect_rec expect_elt) precise in
let t_elt =
let t = Types.Product.pi2 (Types.Product.get ~kind:`XML t) in
let t = Types.Product.pi1 (Types.Product.get t) in
t in
if not precise then constr
else
(try Types.Record.project (Types.cup t t_elt) l
with Not_found -> assert false)
let t = Types.Product.pi2 (Types.Product.get ~kind:`XML t) in
let t = Types.Product.pi1 (Types.Product.get t)
in t
in
let t' =
if not precise then constr else
(try Types.Record.project (Types.cup t t_elt) l
with Not_found -> assert false)
in (ed,t')
| RemoveField (e,l) ->
let t = type_check env e Types.Record.any true in
let t = Types.Record.remove_field t l in
verify loc t constr
(ed,verify loc t constr)
| Xtrans (e,b) ->
let t = type_check env e Sequence.any true in
......@@ -990,24 +1000,24 @@ and type_check' loc env e constr precise = match e with
raise (Cduce_loc.Location (loc,precise,exn))
with Not_found ->
raise_loc loc exn
in
verify loc t constr
in
(ed,verify loc t constr)
| Validate (e, t, _) ->
ignore (type_check env e Types.any false);
verify loc t constr
(ed,verify loc t constr)
| Ref (e,t) ->
ignore (type_check env e (Types.descr t) false);
verify loc (Builtin_defs.ref_type t) constr
(ed,verify loc (Builtin_defs.ref_type t) constr)
| External (t,_) ->
verify loc t constr
(ed,verify loc t constr)
| Op (op,_,args) ->
let args = List.map (type_check env) args in
let t = localize loc (typ_op op args constr) precise in
verify loc t constr
(ed,verify loc t constr)
| NsTable (ns,e) ->
type_check' loc env e constr precise
......@@ -1093,11 +1103,11 @@ and branches_aux loc env targ tres constr precise = function
let acc = Types.descr (Patterns.accept p) in
let targ' = Types.cap targ acc in
if Types.is_empty targ'
then branches_aux loc env targ tres constr precise rem
else
( b.br_used <- true;
let res = Patterns.filter targ' p in
if Types.is_empty targ' then
branches_aux loc env targ tres constr precise rem
else begin
b.br_used <- true;
let res = Patterns.filter targ' p in (* t_
let res = IdMap.map Types.descr res in
b.br_vars_empty <-
......@@ -1107,13 +1117,14 @@ and branches_aux loc env targ tres constr precise = function
let env' = enter_values (IdMap.get res) env in
let t = type_check env' b.br_body constr precise in
b.br_typ <- t;
let tres = if precise then Types.cup t tres else tres in
let targ'' = Types.diff targ acc in
if (Types.non_empty targ'') then
branches_aux loc env targ'' tres constr precise rem
else
tres
)
end
and type_map loc env def e b constr precise =
let acc = if def then Sequence.any else Sequence.star b.br_accept in
......
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