Commit 95f1a9ed authored by Pietro Abate's avatar Pietro Abate

Remove gamma from typer

parent 7608d9a5
......@@ -51,27 +51,23 @@ type item =
type t = {
ids : item Env.t;
delta : Var.Set.t;
gamma : Types.Node.t id_map;
ns: Ns.table;
keep_ns: bool
}
let pp_env ppf env =
(*
let pp_item ppf = function
|Type t | Val t -> Types.Print.pp_type ppf t
(*
|ECDuce _ -> Format.fprintf ppf "ECDuce"
|ESchema _ -> Format.fprintf ppf "ESchema"
|ENamespace _ -> Format.fprintf ppf "ENamespace"
*)
|_ -> ()
in
*)
Format.printf "{gamma=%a; delta=%a}"
(Ident.pp_idmap Types.Print.pp_node) env.gamma
Var.Set.pp env.delta
(*
Format.printf "{ids=%a;delta=%a}"
(Ident.pp_env pp_item) env.ids
*)
Var.Set.pp env.delta
;;
(* Namespaces *)
......@@ -121,9 +117,8 @@ let type_schema env loc name uri =
{ env with ids = Env.add x (ESchema sch) env.ids }
let empty_env = {
ids = Env.empty;
ids = Env.empty; (* map from expression variables to items *)
delta = Var.Set.empty; (* set of bounded type variables *)
gamma = IdMap.empty; (* map from expression variables to types *)
ns = Ns.def_table;
keep_ns = false
}
......@@ -164,9 +159,6 @@ let enter_value id t env =
let enter_values l env =
{ env with ids =
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 =
......@@ -897,7 +889,9 @@ and type_check' loc env ed constr precise = match ed with
ignore (type_check env e t false);
(ed,verify loc t constr)
| Subst (e, sigma) -> (* (ed,type_check env e constr precise) *) assert false
| Subst (e,sl) ->
let t = type_check env e constr precise in
(ed,verify loc t constr)
| Check (t0,e,t) ->
let te = type_check env e Types.any true in
......@@ -928,8 +922,8 @@ and type_check' loc env ed constr precise = match ed with
"but the interface of the abstraction is not compatible"
in
let env = match a.fun_name with
| None -> env
| Some f -> enter_value f a.fun_typ env
| None -> env
| Some f -> enter_value f a.fun_typ env
in
(* update \delta with all variables in t1 -> t2 *)
......@@ -1010,34 +1004,39 @@ and type_check' loc env ed constr precise = match ed with
let dom = Types.Arrow.domain(t1arrow) in
let t2 = type_check env e2 Types.any true in
let res =
let (sl,res) =
if not (Types.no_var dom) ||
not (Types.no_var t2) then
(* get t2 without constraint check *)
let (sl,res) =
(* s [_delta dom(t) *)
try Types.squareapply env.delta t1 t2
with Types.Tallying.UnSatConstr msg ->
raise_loc loc (Constraint (t2,dom))
in
res
(* s [_delta dom(t) *)
try Types.squareapply env.delta t1 t2
with Types.Tallying.UnSatConstr msg ->
raise_loc loc (Constraint (t2,dom))
else begin
(* Monomorphic case as before *)
let sl = Types.Tallying.identity in
if Types.Arrow.need_arg t1arrow then
let t2 = type_check env e2 dom true in
Types.Arrow.apply t1arrow t2
(sl,Types.Arrow.apply t1arrow t2)
else begin
(ignore (type_check env e2 dom true);
Types.Arrow.apply_noarg t1arrow)
(sl,Types.Arrow.apply_noarg t1arrow))
end
end
in
(Apply(e1,e2),verify loc res constr)
let e = exp' loc ed in
e.exp_typ <- res;
(Subst(e,sl),verify loc res constr)
| Var s ->
(ed,verify loc (find_value s env) constr)
let t = find_value s env in
let vars = Types.all_vars t in
if Var.Set.subset vars env.delta then
(Var s,verify loc t constr)
else
(TVar s,verify loc t constr)
| TVar s ->
| TVar s -> (* error loc "Cannot bind polymorphic variable in pattern" *)
(ed,verify loc (find_value s env) constr)
| ExtVar (cu,s,t) ->
......@@ -1207,39 +1206,34 @@ and branches_aux loc env targ tres constr precise = function
else begin
b.br_used <- true;
let res = Patterns.filter targ' p in (* t^i_j // p_j *)
(* update gamma \Gamma, t^i_j // p_j*)
let env = { env with
gamma = IdMap.merge (fun _ v2 -> v2) env.gamma res }
let res = IdMap.map Types.descr res in
b.br_vars_empty <-
IdMap.domain (
IdMap.filter (fun _ t -> Types.subtype t Sequence.nil_type)
(IdMap.restrict res b.br_vars_empty)
);
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
let res = IdMap.map Types.descr res in
b.br_vars_empty <-
IdMap.domain (
IdMap.filter (fun _ t -> Types.subtype t Sequence.nil_type)
(IdMap.restrict res b.br_vars_empty)
);
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
(* 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