Commit 9c97ce5a authored by Pietro Abate's avatar Pietro Abate
Browse files

Fix definition of Xi in typed and compile

parent 3517a2b3
......@@ -6,7 +6,7 @@ type env = {
vars: var_loc Env.t; (* Id.t to var_loc *)
sigma : sigma; (* symbolic substitutions (Lambda.sigma) *)
gamma : Types.Node.t IdMap.map; (* map of type variables to types *)
xi : Var.Set.t;
xi : Var.Set.t IdMap.map;
stack_size: int;
max_stack: int ref;
global_size: int
......@@ -19,7 +19,7 @@ let mk cu = {
vars = Env.empty;
sigma = Lambda.Identity;
gamma = IdMap.empty;
xi = Var.Set.empty;
xi = IdMap.empty;
stack_size = 0;
max_stack = ref 0;
global_size = 0
......@@ -120,7 +120,7 @@ and compile_aux env = function
let v = find x env in
let ts = Types.all_vars (Types.descr (IdMap.assoc x env.gamma)) in
let is_mono () =
let d = Var.Set.inter env.xi (domain(env.sigma)) in
let d = Var.Set.inter (IdMap.assoc x env.xi) (domain(env.sigma)) in
Var.Set.is_empty (Var.Set.inter ts d)
in
if Var.Set.is_empty ts then Var (v) else
......@@ -259,7 +259,7 @@ and compile_branch env br =
let env =
{ env with
gamma = IdMap.union_disj m env.gamma;
xi = Var.Set.union env.xi br.Typed.br_vars_poly
xi = IdMap.merge (fun _ v2 -> v2) env.xi br.Typed.br_vars_poly
}
in
(br.Typed.br_pat, compile env br.Typed.br_body)
......
......@@ -193,7 +193,7 @@ and parse_branches env l toptype acc btype = function
br_used = br_used;
br_ghost = false;
br_vars_empty = [];
br_vars_poly = Var.Set.empty;
br_vars_poly = Ident.IdMap.empty;
br_pat = tpat;
br_body = br_body}
in
......
......@@ -84,7 +84,7 @@ and branch = {
mutable br_used : bool;
br_ghost : bool;
mutable br_vars_empty : fv;
mutable br_vars_poly : Var.Set.t;
mutable br_vars_poly : Var.Set.t IdMap.map;
br_pat : tpat;
(* this field is mutable because we need to add substitutions *)
mutable br_body : texpr
......@@ -198,7 +198,7 @@ module Print = struct
"\n{used:%b; ghost:%b; br_vars_poly:[%a];br_vars_empty:[%a];\npat:{%a};\nbody:{typ:%a, descr:%a}}"
br.br_used
br.br_ghost
Var.Set.print br.br_vars_poly
pp_vars_poly br.br_vars_poly
pp_fv br.br_vars_empty
Patterns.pp_node br.br_pat
Types.Print.print br.br_body.exp_typ
......@@ -211,5 +211,10 @@ module Print = struct
and pp_fv ppf fv = print_lst pp_v ppf fv
and pp_vars_poly ppf m =
let l = IdMap.fold (fun x s acc -> (x,s)::acc) m [] in
let pp_aux ppf (x,s) = Format.fprintf ppf "%a : %a" Ident.print x Var.Set.print s in
print_lst pp_aux ppf m
let typed_to_string = print_to_string pp_typed
end
......@@ -597,14 +597,14 @@ and if_then_else loc cond yes no =
Typed.br_used = false;
Typed.br_ghost = false;
Typed.br_vars_empty = Fv.empty;
Typed.br_vars_poly = Var.Set.empty;
Typed.br_vars_poly = IdMap.empty;
Typed.br_pat = pat_true;
Typed.br_body = yes };
{ Typed.br_loc = no.Typed.exp_loc;
Typed.br_used = false;
Typed.br_ghost = false;
Typed.br_vars_empty = Fv.empty;
Typed.br_vars_poly = Var.Set.empty;
Typed.br_vars_poly = IdMap.empty;
Typed.br_pat = pat_false;
Typed.br_body = no } ];
Typed.br_accept = Builtin_defs.bool;
......@@ -729,7 +729,7 @@ and branches env b =
Typed.br_used = ghost;
Typed.br_ghost = ghost;
Typed.br_vars_empty = fvp;
Typed.br_vars_poly = Var.Set.empty;
Typed.br_vars_poly = IdMap.empty;
Typed.br_pat = p;
Typed.br_body = e } in
cur_branch := Branch (br, !cur_branch) :: cur_br;
......@@ -772,7 +772,7 @@ and select_from_where env loc e from where =
Typed.br_used = false;
Typed.br_ghost = false;
Typed.br_vars_empty = fvp;
Typed.br_vars_poly = Var.Set.empty;
Typed.br_vars_poly = IdMap.empty;
Typed.br_pat = p;
Typed.br_body = rest } in
cur_branch := [ Branch (br, !cur_branch) ];
......@@ -1135,18 +1135,16 @@ and branches_aux loc env targ tres constr precise = function
b.br_vars_empty <-
IdMap.domain (
IdMap.filter (fun _ t -> Types.subtype t Sequence.nil_type)
(IdMap.restrict res b.br_vars_empty));
(IdMap.restrict res b.br_vars_empty)
);
let env' = enter_values (IdMap.get res) env in
(* Xi_j *)
(* Xi_j : a map from term variables in the pattern to type variables *)
let xj =
let pattpolyvars =
IdMap.fold (fun _ t acc ->
Var.Set.union acc (Types.all_vars (Types.descr t))
) env'.gamma Var.Set.empty
in
Var.Set.diff pattpolyvars env'.delta
IdMap.fold (fun x t acc ->
IdMap.add x (Var.Set.diff (Types.all_vars t) env'.delta) acc
) res IdMap.empty
in
(* all poly variables associated with the pattern p_j that are not in \Delta *)
b.br_vars_poly <- xj;
......
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