Commit b59a4797 authored by Pietro Abate's avatar Pietro Abate

Propagate gamma in the compilation environment

parent bc4ad733
......@@ -347,6 +347,15 @@ let run_show ~run ~show tenv cenv codes ids =
let let_decl ~run ~show (tenv,cenv,codes) p e =
let (tenv,decl,ids) = Typer.type_let_decl tenv p e in
let (cenv,code) = compile_let_decl cenv decl in
(* XXX I've the impression I'm duplicating information here
* as cenv.gamma == tenv.gamma *)
let cenv = {cenv with gamma =
List.fold_left (fun acc (id,_) ->
(* an old binding is showed by a new one *)
IdMap.add id (Types.cons (Typer.find_value id tenv)) (IdMap.remove id acc)
) cenv.gamma ids;
}
in
run_show ~run ~show tenv cenv code ids;
(tenv,cenv,List.rev_append code codes)
......
......@@ -160,9 +160,15 @@ let find_id_comp env0 env loc x =
let enter_value id t env =
{ env with ids = Env.add id (Val t) env.ids }
let enter_values l env =
{ env with ids =
List.fold_left (fun accu (id,t) -> Env.add id (Val t) accu) env.ids l }
List.fold_left (fun accu (id,t) -> Env.add id (Val t) accu) env.ids l;
gamma = List.fold_left (fun acc (id,t) ->
IdMap.add id (Types.cons t) (IdMap.remove id acc)
) env.gamma l;
}
let enter_values_dummy l env =
{ env with ids =
List.fold_left (fun accu id -> Env.add id (Val Types.empty) accu) env.ids l }
......@@ -178,7 +184,6 @@ let iter_values env f =
function Val t -> f x t;
| _ -> ()) env.ids
let register_types cu env =
Env.iter (fun x t -> match t with
| Type t -> Types.Print.register_global cu (Ident.value x) t
......@@ -900,18 +905,18 @@ and type_check' loc env ed constr precise = match ed with
(ed,verify loc (Types.cap te (Types.descr t)) constr)
| Abstraction a ->
(* freshen type variables from the environment to avoid capture with
variables defined in the interface of a *)
let env = {
(* freshen type variables from the environment to avoid capture with
variables defined in the interface of a *)
env with
ids = Env.map
(fun v ->
let open Types in
match v with
| Val t -> Val (Positive.substitutefree env.delta t)
| EVal (a,b,t) -> EVal (a,b,Positive.substitutefree env.delta t)
| x -> x)
env.ids }
ids = Env.map
(fun v ->
let open Types in
match v with
| Val t -> Val (Positive.substitutefree env.delta t)
| EVal (a,b,t) -> EVal (a,b,Positive.substitutefree env.delta t)
| x -> x)
env.ids }
in
let t =
(* try Types.Arrow.check_strenghten a.fun_typ constr *)
......@@ -937,8 +942,8 @@ and type_check' loc env ed constr precise = match ed with
match a.fun_iface with
|[] -> Var.Set.empty
|head::tail ->
List.fold_left (fun acc inf ->
Var.Set.inter (union inf) acc
List.fold_left (fun acc intf ->
Var.Set.inter (union intf) acc
) (union head) tail
in
......@@ -993,10 +998,9 @@ and type_check' loc env ed constr precise = match ed with
(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
let t1arrow = Types.Arrow.get t1 in
let t1 = Types.Positive.substitutefree env.delta t1 in
let t1 = type_check env e1 Types.Arrow.any true in
let t1arrow = Types.Arrow.get t1 in
let t1 = Types.Positive.substitutefree env.delta t1 in
(* t [_delta 0 -> 1 *)
begin try
ignore(Types.Tallying.tallying env.delta [(t1,Types.Arrow.any)])
......@@ -1217,25 +1221,25 @@ and branches_aux loc env targ tres constr precise = function
let env' = enter_values (IdMap.get res) env in
(* Xi_j : a map from term variables in the pattern to type variables *)
let xj =
IdMap.fold (fun x t acc ->
let s = Var.Set.diff (Types.all_vars t) env'.delta in
IdMap.add x s acc
) res IdMap.empty
in
(* all polymorphic variables not in \Delta associated with a term
* variable x in p_j*)
b.br_vars_poly <- xj;
let t = type_check env' b.br_body constr precise in (* s_i^j *)
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
(* Xi_j : a map from term variables in the pattern to type variables *)
let xj =
IdMap.fold (fun x t acc ->
let s = Var.Set.diff (Types.all_vars t) env'.delta in
IdMap.add x s acc
) res IdMap.empty
in
(* all polymorphic variables not in \Delta associated with a term
* variable x in p_j*)
b.br_vars_poly <- xj;
let t = type_check env' b.br_body constr precise in (* s_i^j *)
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