Commit 04a5751b authored by Pietro Abate's avatar Pietro Abate
Browse files

Add substitutions in Typed abstractions

parent 70914ae2
...@@ -86,6 +86,7 @@ and branch = { ...@@ -86,6 +86,7 @@ and branch = {
mutable br_vars_empty : fv; mutable br_vars_empty : fv;
mutable br_vars_poly : fv; mutable br_vars_poly : fv;
br_pat : tpat; br_pat : tpat;
br_body : texpr (* this field is mutable because we need to add substitutions *)
mutable br_body : texpr
} }
...@@ -851,6 +851,7 @@ let flatten arg constr precise = ...@@ -851,6 +851,7 @@ let flatten arg constr precise =
let rec type_check env e constr precise = let rec type_check env e constr precise =
Printf.printf "aaaa\n%!";
let (ed,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 let d = if precise then d else constr in
e.exp_typ <- Types.cup e.exp_typ d; e.exp_typ <- Types.cup e.exp_typ d;
...@@ -862,8 +863,9 @@ and type_check' loc env ed constr precise = match ed with ...@@ -862,8 +863,9 @@ and type_check' loc env ed constr precise = match ed with
let t = Types.descr t in let t = Types.descr t in
ignore (type_check env e t false); ignore (type_check env e t false);
(ed,verify loc t constr) (ed,verify loc t constr)
(*
| Subst (e, sigma) -> (ed,type_check env e constr precise) | Subst (e, sigma) -> (ed,type_check env e constr precise)
*)
| Check (t0,e,t) -> | Check (t0,e,t) ->
let te = type_check env e Types.any true in let te = type_check env e Types.any true in
...@@ -884,18 +886,25 @@ and type_check' loc env ed constr precise = match ed with ...@@ -884,18 +886,25 @@ and type_check' loc env ed constr precise = match ed with
(* update \delta with all variables in t1 -> t2 *) (* update \delta with all variables in t1 -> t2 *)
(* I check the body with all possible t1 -> t2 types *) (* I check the body with all possible t1 -> t2 types *)
List.iter (fun (t1,t2) -> let sl_list =
let acc = a.fun_body.br_accept in List.fold_left (fun tacc (t1,t2) ->
if not (Types.subtype t1 acc) then let acc = a.fun_body.br_accept in
raise_loc loc (NonExhaustive (Types.diff t1 acc)); if not (Types.subtype t1 acc) then
let t = type_check_branches loc env t1 a.fun_body t2 false in raise_loc loc (NonExhaustive (Types.diff t1 acc));
let sigma = Types.abstr t t2 in (* H_j *) let t = type_check_branches loc env t1 a.fun_body t2 false in
(* (Types.abstr t t2)::tacc (* H_j *)
List.iter (fun br -> ) [] a.fun_iface
br.br_body.exp_descr <- Subst(br.br_body,sigma); in
) a.fun_body.br_branches List.iter (function
*) () (* If sigma empty (sat, we do not need any subst ...
) a.fun_iface; | sigma when Types.Tallying.CS. sigma -> () *)
| sigma ->
List.iter (fun br ->
let e = br.br_body in
let loc = br.br_body.exp_loc in
br.br_body <- exp' loc (Subst(e,sigma));
) a.fun_body.br_branches
) (List.rev sl_list);
(ed,t) (ed,t)
| Match (e,b) -> | Match (e,b) ->
......
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