Commit 779c1aba authored by Kim Nguyễn's avatar Kim Nguyễn

Merge branch 'feature/pattern-refinement'

parents 9ca493cc e0984cd5
...@@ -187,7 +187,7 @@ OBJECTS = \ ...@@ -187,7 +187,7 @@ OBJECTS = \
parser/cduce_loc.cmo parser/url.cmo \ parser/cduce_loc.cmo parser/url.cmo \
parser/ulexer.cmo parser/ast.cmo parser/parser.cmo \ parser/ulexer.cmo parser/ast.cmo parser/parser.cmo \
\ \
typing/typed.cmo typing/typepat.cmo types/externals.cmo typing/typer.cmo \ typing/typepat.cmo typing/typed.cmo types/externals.cmo typing/typer.cmo \
compile/compile.cmo \ compile/compile.cmo \
\ \
schema/schema_parser.cmo schema/schema_converter.cmo \ schema/schema_parser.cmo schema/schema_converter.cmo \
......
...@@ -57,11 +57,9 @@ compile/auto_pat.cmo : types/types.cmi types/ident.cmo types/chars.cmi \ ...@@ -57,11 +57,9 @@ compile/auto_pat.cmo : types/types.cmi types/ident.cmo types/chars.cmi \
compile/auto_pat.cmx : types/types.cmx types/ident.cmx types/chars.cmx \ compile/auto_pat.cmx : types/types.cmx types/ident.cmx types/chars.cmx \
types/atoms.cmx compile/auto_pat.cmi types/atoms.cmx compile/auto_pat.cmi
types/type_tallying.cmo : types/var.cmi misc/utils.cmo types/types.cmi \ types/type_tallying.cmo : types/var.cmi misc/utils.cmo types/types.cmi \
types/intervals.cmi misc/custom.cmo types/chars.cmi types/atoms.cmi \ misc/custom.cmo types/type_tallying.cmi
types/type_tallying.cmi
types/type_tallying.cmx : types/var.cmx misc/utils.cmx types/types.cmx \ types/type_tallying.cmx : types/var.cmx misc/utils.cmx types/types.cmx \
types/intervals.cmx misc/custom.cmx types/chars.cmx types/atoms.cmx \ misc/custom.cmx types/type_tallying.cmi
types/type_tallying.cmi
types/sequence.cmo : types/types.cmi misc/custom.cmo types/chars.cmi \ types/sequence.cmo : types/types.cmi misc/custom.cmo types/chars.cmi \
types/atoms.cmi types/sequence.cmi types/atoms.cmi types/sequence.cmi
types/sequence.cmx : types/types.cmx misc/custom.cmx types/chars.cmx \ types/sequence.cmx : types/types.cmx misc/custom.cmx types/chars.cmx \
...@@ -177,15 +175,15 @@ parser/parser.cmx : types/var.cmx parser/ulexer.cmx types/types.cmx \ ...@@ -177,15 +175,15 @@ parser/parser.cmx : types/var.cmx parser/ulexer.cmx types/types.cmx \
misc/encodings.cmx types/chars.cmx parser/cduce_loc.cmx types/atoms.cmx \ misc/encodings.cmx types/chars.cmx parser/cduce_loc.cmx types/atoms.cmx \
parser/ast.cmx parser/parser.cmi parser/ast.cmx parser/parser.cmi
typing/typed.cmo : types/var.cmi misc/utils.cmo misc/upool.cmi \ typing/typed.cmo : types/var.cmi misc/utils.cmo misc/upool.cmi \
types/types.cmi types/type_tallying.cmi schema/schema_validator.cmi \ types/types.cmi typing/typepat.cmi types/type_tallying.cmi \
types/patterns.cmi misc/ns.cmi types/intervals.cmi types/ident.cmo \ schema/schema_validator.cmi types/patterns.cmi misc/ns.cmi \
misc/encodings.cmi types/compunit.cmi types/chars.cmi \ types/intervals.cmi types/ident.cmo misc/encodings.cmi types/compunit.cmi \
parser/cduce_loc.cmi types/atoms.cmi types/chars.cmi parser/cduce_loc.cmi types/atoms.cmi
typing/typed.cmx : types/var.cmx misc/utils.cmx misc/upool.cmx \ typing/typed.cmx : types/var.cmx misc/utils.cmx misc/upool.cmx \
types/types.cmx types/type_tallying.cmx schema/schema_validator.cmx \ types/types.cmx typing/typepat.cmx types/type_tallying.cmx \
types/patterns.cmx misc/ns.cmx types/intervals.cmx types/ident.cmx \ schema/schema_validator.cmx types/patterns.cmx misc/ns.cmx \
misc/encodings.cmx types/compunit.cmx types/chars.cmx \ types/intervals.cmx types/ident.cmx misc/encodings.cmx types/compunit.cmx \
parser/cduce_loc.cmx types/atoms.cmx types/chars.cmx parser/cduce_loc.cmx types/atoms.cmx
typing/typepat.cmo : types/types.cmi types/sequence.cmi types/patterns.cmi \ typing/typepat.cmo : types/types.cmi types/sequence.cmi types/patterns.cmi \
types/ident.cmo misc/encodings.cmi types/chars.cmi typing/typepat.cmi types/ident.cmo misc/encodings.cmi types/chars.cmi typing/typepat.cmi
typing/typepat.cmx : types/types.cmx types/sequence.cmx types/patterns.cmx \ typing/typepat.cmx : types/types.cmx types/sequence.cmx types/patterns.cmx \
...@@ -389,9 +387,9 @@ compile/auto_pat.cmi : types/types.cmi types/ident.cmo types/chars.cmi \ ...@@ -389,9 +387,9 @@ compile/auto_pat.cmi : types/types.cmi types/ident.cmo types/chars.cmi \
types/type_tallying.cmi : types/var.cmi types/types.cmi types/type_tallying.cmi : types/var.cmi types/types.cmi
types/sequence.cmi : types/types.cmi types/atoms.cmi types/sequence.cmi : types/types.cmi types/atoms.cmi
types/builtin_defs.cmi : types/types.cmi types/ident.cmo types/atoms.cmi types/builtin_defs.cmi : types/types.cmi types/ident.cmo types/atoms.cmi
runtime/value.cmi : types/types.cmi types/type_tallying.cmi misc/ns.cmi \ runtime/value.cmi : types/types.cmi misc/ns.cmi types/intervals.cmi \
types/intervals.cmi misc/imap.cmi types/ident.cmo misc/encodings.cmi \ misc/imap.cmi types/ident.cmo misc/encodings.cmi types/chars.cmi \
types/chars.cmi types/atoms.cmi types/atoms.cmi
schema/schema_pcre.cmi : misc/encodings.cmi schema/schema_pcre.cmi : misc/encodings.cmi
schema/schema_types.cmi : runtime/value.cmi misc/ns.cmi misc/encodings.cmi \ schema/schema_types.cmi : runtime/value.cmi misc/ns.cmi misc/encodings.cmi \
types/atoms.cmi types/atoms.cmi
...@@ -407,8 +405,8 @@ types/patterns.cmi : types/types.cmi types/ident.cmo misc/custom.cmo \ ...@@ -407,8 +405,8 @@ types/patterns.cmi : types/types.cmi types/ident.cmo misc/custom.cmo \
compile/auto_pat.cmi compile/auto_pat.cmi
compile/print_auto.cmi : compile/auto_pat.cmi compile/print_auto.cmi : compile/auto_pat.cmi
compile/lambda.cmi : runtime/value.cmi types/types.cmi \ compile/lambda.cmi : runtime/value.cmi types/types.cmi \
types/type_tallying.cmi schema/schema_validator.cmi misc/ns.cmi \ schema/schema_validator.cmi misc/ns.cmi misc/imap.cmi types/ident.cmo \
misc/imap.cmi types/ident.cmo types/compunit.cmi compile/auto_pat.cmi types/compunit.cmi compile/auto_pat.cmi
runtime/run_dispatch.cmi : runtime/value.cmi compile/auto_pat.cmi runtime/run_dispatch.cmi : runtime/value.cmi compile/auto_pat.cmi
runtime/explain.cmi : runtime/value.cmi compile/auto_pat.cmi runtime/explain.cmi : runtime/value.cmi compile/auto_pat.cmi
runtime/eval.cmi : runtime/value.cmi misc/ns.cmi compile/lambda.cmi \ runtime/eval.cmi : runtime/value.cmi misc/ns.cmi compile/lambda.cmi \
......
(* Typed abstract syntax *) (* Typed abstract syntax *)
(* Some sub-expression may have to be type-checked several times. (* Some sub-expression may have to be type-checked several times.
We first build the ``skeleton'' of the typed ast We first build the ``skeleton'' of the typed ast
...@@ -17,14 +17,14 @@ type ttyp = Types.Node.t ...@@ -17,14 +17,14 @@ type ttyp = Types.Node.t
type sigma = Types.Subst.t list type sigma = Types.Subst.t list
type texpr = type texpr =
{ exp_loc : loc; { exp_loc : loc;
mutable exp_typ : Types.t; mutable exp_typ : Types.t;
(* Currently exp_typ is not used. It will be used for compilation ! *) (* Currently exp_typ is not used. It will be used for compilation ! *)
mutable exp_descr : texpr'; mutable exp_descr : texpr';
} }
and texpr' = and texpr' =
| Forget of texpr * ttyp | Forget of texpr * ttyp
| Check of (Types.t ref) * texpr * ttyp | Check of (Types.t ref) * texpr * ttyp
(* CDuce is a Lambda-calculus ... *) (* CDuce is a Lambda-calculus ... *)
...@@ -36,14 +36,14 @@ and texpr' = ...@@ -36,14 +36,14 @@ and texpr' =
| ExtVar of Compunit.t * id * Types.t | ExtVar of Compunit.t * id * Types.t
| Apply of texpr * texpr | Apply of texpr * texpr
| Abstraction of abstr | Abstraction of abstr
(* Data constructors *) (* Data constructors *)
| Cst of Types.const | Cst of Types.const
| Pair of texpr * texpr | Pair of texpr * texpr
| Xml of texpr * texpr * Ns.table option | Xml of texpr * texpr * Ns.table option
| RecordLitt of texpr label_map | RecordLitt of texpr label_map
| String of U.uindex * U.uindex * U.t * texpr | String of U.uindex * U.uindex * U.t * texpr
(* Data destructors *) (* Data destructors *)
| Match of texpr * branches | Match of texpr * branches
| Map of texpr * branches | Map of texpr * branches
...@@ -61,8 +61,8 @@ and texpr' = ...@@ -61,8 +61,8 @@ and texpr' =
| Op of string * int * texpr list | Op of string * int * texpr list
| NsTable of Ns.table * texpr' | NsTable of Ns.table * texpr'
and abstr = { and abstr = {
fun_name : id option; fun_name : id option;
fun_iface : (Types.t * Types.t) list; fun_iface : (Types.t * Types.t) list;
fun_body : branches; fun_body : branches;
fun_typ : Types.t; fun_typ : Types.t;
...@@ -74,22 +74,61 @@ and let_decl = { ...@@ -74,22 +74,61 @@ and let_decl = {
let_body : texpr; let_body : texpr;
} }
and branches = { and branches = {
mutable br_typ : Types.t; (* Type of values that can flow to branches *) mutable br_typ : Types.t; (* Type of values that can flow to branches *)
br_accept : Types.t; (* Type accepted by all branches *) br_accept : Types.t; (* Type accepted by all branches *)
br_branches: branch list; br_branches: branch list;
} }
and branch = { and branch = {
br_loc : loc; br_loc : loc;
mutable br_used : bool; mutable br_used : bool;
br_ghost : bool; br_ghost : bool;
mutable br_vars_empty : fv; mutable br_vars_empty : fv;
mutable br_vars_poly : Var.Set.t IdMap.map; mutable br_vars_poly : Var.Set.t IdMap.map;
br_pat : tpat; br_pat : tpat;
(* this field is mutable because we need to add substitutions *) (* this field is mutable because we need to add substitutions *)
mutable br_body : texpr mutable br_body : texpr
} }
let pat_list_of_expr e =
let max_occ = ref ~-1 in
let open Typepat in
let module HashId = Hashtbl.Make(Id) in
let any_pat = mk_type Types.any in
let mk_pat i e =
let map = HashId.create 17 in
let rec loop e =
match e.exp_descr with
Var id ->
let occ =
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
List.rev (loop 1 [])
module Print = struct module Print = struct
let rec pp_const ppf cst = let rec pp_const ppf cst =
......
...@@ -1175,7 +1175,7 @@ and type_check' loc env ed constr precise = match ed with ...@@ -1175,7 +1175,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 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
...@@ -1195,11 +1195,13 @@ and type_check' loc env ed constr precise = match ed with ...@@ -1195,11 +1195,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
(ed,type_check_branches loc env t b constr precise) let pargs = pat_list_of_expr e in
(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 tb = type_check_branches loc env Types.any b constr precise in let pargs = pat_list_of_expr e 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) ->
...@@ -1301,12 +1303,13 @@ and type_check' loc env ed constr precise = match ed with ...@@ -1301,12 +1303,13 @@ 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_list_of_expr e in
let t = let t =
try try
Sequence.map_tree constr Sequence.map_tree constr
(fun cstr t -> (fun cstr t ->
let resid = Types.diff t b.br_accept in let resid = Types.diff t b.br_accept in
let res = type_check_branches loc env t b cstr true in let res = type_check_branches loc env t parg b cstr true in
(res,resid) (res,resid)
) t ) t
with (Sequence.Error _) as exn -> with (Sequence.Error _) as exn ->
...@@ -1420,16 +1423,17 @@ and type_record loc env r constr precise = ...@@ -1420,16 +1423,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 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 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 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 +1441,7 @@ and branches_aux loc env targ tres constr precise = function ...@@ -1437,7 +1441,7 @@ and branches_aux loc env targ 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 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,9 +1451,18 @@ and branches_aux loc env targ tres constr precise = function ...@@ -1447,9 +1451,18 @@ and branches_aux loc env targ 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' = enter_values (IdMap.get res) env in List.fold_left (fun env_acc ip ->
if Types.subtype targ' (Types.descr (Patterns.accept ip)) then
let res_parg = Patterns.filter targ' ip in
let res_parg = IdMap.map Types.descr res_parg in
IdMap.merge Types.cap env_acc res_parg
else
env_acc
) IdMap.empty pargs
in
let env_parg = enter_values (IdMap.get env_parg) env 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 =
IdMap.fold (fun x t acc -> IdMap.fold (fun x t acc ->
...@@ -1465,7 +1478,7 @@ and branches_aux loc env targ tres constr precise = function ...@@ -1465,7 +1478,7 @@ and branches_aux loc env targ 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'' tres constr precise rem branches_aux loc env targ'' pargs tres constr precise rem
else else
tres tres
end end
...@@ -1473,7 +1486,7 @@ and branches_aux loc env targ tres constr precise = function ...@@ -1473,7 +1486,7 @@ and branches_aux loc env targ 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 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:
...@@ -1484,7 +1497,7 @@ and type_map loc env def e b constr precise = ...@@ -1484,7 +1497,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 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