Commit e0984cd5 authored by Kim Nguyễn's avatar Kim Nguyễn

Improve the refinement of the type of variables to handle the case of multiple occurrences.

parent 1f8f3aab
...@@ -91,18 +91,43 @@ and branch = { ...@@ -91,18 +91,43 @@ and branch = {
} }
let pat_of_expr e = let pat_list_of_expr e =
let max_occ = ref ~-1 in
let open Typepat in let open Typepat in
let module HashId = Hashtbl.Make(Id) in
let any_pat = mk_type Types.any in let any_pat = mk_type Types.any in
let rec loop e = let mk_pat i e =
match e.exp_descr with let map = HashId.create 17 in
Var id -> mk_capture id let rec loop e =
| Pair (e1, e2) -> mk_prod (loop e1) (loop e2) match e.exp_descr with
| Xml (e1, e2, None) -> mk_xml (loop e1) (loop e2) (* TODO : check the inpact of Ns.table *) Var id ->
| RecordLitt emap -> mk_record false (LabelMap.map (fun e -> loop e, None) emap) let occ =
| _ -> any_pat try
HashId.find map id
with Not_found -> 1
in
if occ > !max_occ then max_occ := occ;
HashId.replace map id (occ + 1);
if i = occ then
mk_capture id
else
any_pat
| Pair (e1, e2) -> mk_prod (loop e1) (loop e2)
| Xml (e1, e2, None) -> mk_xml (loop e1) (loop e2) (* TODO : check the inpact of Ns.table *)
| RecordLitt emap -> mk_record false (LabelMap.map (fun e -> loop e, None) emap)
| _ -> any_pat
in
pat_node (loop e)
in
let rec loop i acc =
let acc = (mk_pat i e) :: acc in
if !max_occ == 0 then [] else
if i < !max_occ then loop (i+1) acc
else acc
in in
pat_node (loop e) List.rev (loop 1 [])
module Print = struct module Print = struct
......
...@@ -1172,7 +1172,7 @@ and type_check' loc env ed constr precise = match ed with ...@@ -1172,7 +1172,7 @@ and type_check' loc env ed constr precise = match ed with
let acc = a.fun_body.br_accept in let acc = a.fun_body.br_accept in
if not (Types.subtype t1 acc) then if not (Types.subtype t1 acc) then
raise_loc loc (NonExhaustive (Types.diff t1 acc)); raise_loc loc (NonExhaustive (Types.diff t1 acc));
let t = type_check_branches loc env t1 (Typepat.(pat_node (mk_type Types.any))) a.fun_body t2 true in let t = type_check_branches loc env t1 [] a.fun_body t2 true in
try try
(Type_tallying.squaresubtype env.delta t t2)::tacc (* H_j *) (Type_tallying.squaresubtype env.delta t t2)::tacc (* H_j *)
with with
...@@ -1192,13 +1192,13 @@ and type_check' loc env ed constr precise = match ed with ...@@ -1192,13 +1192,13 @@ and type_check' loc env ed constr precise = match ed with
| Match (e,b) -> | Match (e,b) ->
let t = type_check env e b.br_accept true in let t = type_check env e b.br_accept true in
let parg = pat_of_expr e in let pargs = pat_list_of_expr e in
(ed,type_check_branches loc env t parg b constr precise) (ed,type_check_branches loc env t pargs b constr precise)
| Try (e,b) -> | Try (e,b) ->
let te = type_check env e constr precise in let te = type_check env e constr precise in
let parg = pat_of_expr e in let pargs = pat_list_of_expr e in
let tb = type_check_branches loc env Types.any parg b constr precise in let tb = type_check_branches loc env Types.any pargs b constr precise in
(ed,Types.cup te tb) (ed,Types.cup te tb)
| Pair (e1,e2) -> | Pair (e1,e2) ->
...@@ -1300,7 +1300,7 @@ and type_check' loc env ed constr precise = match ed with ...@@ -1300,7 +1300,7 @@ and type_check' loc env ed constr precise = match ed with
| Xtrans (e,b) -> | Xtrans (e,b) ->
let t = type_check env e Sequence.any true in let t = type_check env e Sequence.any true in
let parg = pat_of_expr e in let parg = pat_list_of_expr e in
let t = let t =
try try
Sequence.map_tree constr Sequence.map_tree constr
...@@ -1420,16 +1420,17 @@ and type_record loc env r constr precise = ...@@ -1420,16 +1420,17 @@ and type_record loc env r constr precise =
else constr else constr
(* i \in I , \forall j \in J \cup s^i_j *) (* i \in I , \forall j \in J \cup s^i_j *)
and type_check_branches loc env targ parg brs constr precise = and type_check_branches loc env targ pargs brs constr precise =
let pargs = pargs in
if Types.is_empty targ then Types.empty if Types.is_empty targ then Types.empty
else begin else begin
brs.br_typ <- Types.cup brs.br_typ targ; brs.br_typ <- Types.cup brs.br_typ targ;
branches_aux loc env targ parg branches_aux loc env targ pargs
(if precise then Types.empty else constr) (if precise then Types.empty else constr)
constr precise brs.br_branches constr precise brs.br_branches
end end
and branches_aux loc env targ parg tres constr precise = function and branches_aux loc env targ pargs tres constr precise = function
| [] -> tres | [] -> tres
| b :: rem -> | b :: rem ->
let p = b.br_pat in let p = b.br_pat in
...@@ -1437,7 +1438,7 @@ and branches_aux loc env targ parg tres constr precise = function ...@@ -1437,7 +1438,7 @@ and branches_aux loc env targ parg tres constr precise = function
let targ' = Types.cap targ acc in let targ' = Types.cap targ acc in
if Types.is_empty targ' then if Types.is_empty targ' then
(* this branch cannot be selected: we ignore it *) (* this branch cannot be selected: we ignore it *)
branches_aux loc env targ parg tres constr precise rem branches_aux loc env targ pargs tres constr precise rem
else begin else begin
b.br_used <- true; b.br_used <- true;
let res = Patterns.filter targ' p in (* t^i_j // p_j *) let res = Patterns.filter targ' p in (* t^i_j // p_j *)
...@@ -1447,15 +1448,17 @@ and branches_aux loc env targ parg tres constr precise = function ...@@ -1447,15 +1448,17 @@ and branches_aux loc env targ parg tres constr precise = function
IdMap.filter (fun _ t -> Types.subtype t Sequence.nil_type) 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_parg = let env_parg =
if Types.subtype targ' (Types.descr (Patterns.accept parg)) then List.fold_left (fun env_acc ip ->
let res_parg = Patterns.filter targ' parg in if Types.subtype targ' (Types.descr (Patterns.accept ip)) then
let res_parg = IdMap.map Types.descr res_parg in let res_parg = Patterns.filter targ' ip in
enter_values (IdMap.get res_parg) env let res_parg = IdMap.map Types.descr res_parg in
else IdMap.merge Types.cap env_acc res_parg
env else
env_acc
) IdMap.empty pargs
in in
let env_parg = enter_values (IdMap.get env_parg) env in
let env' = enter_values (IdMap.get res) env_parg in let env' = enter_values (IdMap.get res) env_parg in
(* Xi_j : a map from term variables in the pattern to type variables *) (* Xi_j : a map from term variables in the pattern to type variables *)
let xj = let xj =
...@@ -1472,7 +1475,7 @@ and branches_aux loc env targ parg tres constr precise = function ...@@ -1472,7 +1475,7 @@ and branches_aux loc env targ parg tres constr precise = function
let tres = if precise then Types.cup t tres else tres in let tres = if precise then Types.cup t tres else tres in
let targ'' = Types.diff targ acc in let targ'' = Types.diff targ acc in
if (Types.non_empty targ'') then if (Types.non_empty targ'') then
branches_aux loc env targ'' parg tres constr precise rem branches_aux loc env targ'' pargs tres constr precise rem
else else
tres tres
end end
...@@ -1480,7 +1483,7 @@ and branches_aux loc env targ parg tres constr precise = function ...@@ -1480,7 +1483,7 @@ and branches_aux loc env targ parg tres constr precise = function
and type_map loc env def e b constr precise = and type_map loc env def e b constr precise =
let acc = if def then Sequence.any else Sequence.star b.br_accept in let acc = if def then Sequence.any else Sequence.star b.br_accept in
let t = type_check env e acc true in let t = type_check env e acc true in
let parg = pat_of_expr e in let pargs = pat_list_of_expr e in
let constr' = Sequence.approx (Types.cap Sequence.any constr) in let constr' = Sequence.approx (Types.cap Sequence.any constr) in
let exact = Types.subtype (Sequence.star constr') constr in let exact = Types.subtype (Sequence.star constr') constr in
(* Note: (* Note:
...@@ -1491,7 +1494,7 @@ and type_map loc env def e b constr precise = ...@@ -1491,7 +1494,7 @@ and type_map loc env def e b constr precise =
Sequence.map Sequence.map
(fun t -> (fun t ->
let res = let res =
type_check_branches loc env t parg b constr' (precise || (not exact)) in type_check_branches loc env t pargs b constr' (precise || (not exact)) in
if def && not (Types.subtype t b.br_accept) if def && not (Types.subtype t b.br_accept)
then (require loc Sequence.nil_type constr'; Types.cup res Sequence.nil_type) then (require loc Sequence.nil_type constr'; Types.cup res Sequence.nil_type)
else res) else res)
......
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