Commit 1f8f3aab by Kim Nguyễn

Preliminary implementation of the pattern refinement feature.

parent 6b733b5a
......@@ -189,7 +189,7 @@ OBJECTS = \
parser/cduce_loc.cmo parser/url.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 \
\
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 \
compile/auto_pat.cmx : types/types.cmx types/ident.cmx types/chars.cmx \
types/atoms.cmx compile/auto_pat.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 \
types/type_tallying.cmi
misc/custom.cmo types/type_tallying.cmi
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 \
types/type_tallying.cmi
misc/custom.cmx types/type_tallying.cmi
types/sequence.cmo : types/types.cmi misc/custom.cmo types/chars.cmi \
types/atoms.cmi types/sequence.cmi
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 \
misc/encodings.cmx types/chars.cmx parser/cduce_loc.cmx types/atoms.cmx \
parser/ast.cmx parser/parser.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/patterns.cmi misc/ns.cmi types/intervals.cmi types/ident.cmo \
misc/encodings.cmi types/compunit.cmi types/chars.cmi \
parser/cduce_loc.cmi types/atoms.cmi
types/types.cmi typing/typepat.cmi types/type_tallying.cmi \
schema/schema_validator.cmi types/patterns.cmi misc/ns.cmi \
types/intervals.cmi types/ident.cmo misc/encodings.cmi types/compunit.cmi \
types/chars.cmi parser/cduce_loc.cmi types/atoms.cmi
typing/typed.cmx : types/var.cmx misc/utils.cmx misc/upool.cmx \
types/types.cmx types/type_tallying.cmx schema/schema_validator.cmx \
types/patterns.cmx misc/ns.cmx types/intervals.cmx types/ident.cmx \
misc/encodings.cmx types/compunit.cmx types/chars.cmx \
parser/cduce_loc.cmx types/atoms.cmx
types/types.cmx typing/typepat.cmx types/type_tallying.cmx \
schema/schema_validator.cmx types/patterns.cmx misc/ns.cmx \
types/intervals.cmx types/ident.cmx misc/encodings.cmx types/compunit.cmx \
types/chars.cmx parser/cduce_loc.cmx types/atoms.cmx
typing/typepat.cmo : types/types.cmi types/sequence.cmi types/patterns.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 \
......@@ -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/sequence.cmi : types/types.cmi 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 \
types/intervals.cmi misc/imap.cmi types/ident.cmo misc/encodings.cmi \
types/chars.cmi types/atoms.cmi
runtime/value.cmi : types/types.cmi misc/ns.cmi types/intervals.cmi \
misc/imap.cmi types/ident.cmo misc/encodings.cmi types/chars.cmi \
types/atoms.cmi
schema/schema_pcre.cmi : misc/encodings.cmi
schema/schema_types.cmi : runtime/value.cmi misc/ns.cmi misc/encodings.cmi \
types/atoms.cmi
......@@ -407,8 +405,8 @@ types/patterns.cmi : types/types.cmi types/ident.cmo misc/custom.cmo \
compile/auto_pat.cmi
compile/print_auto.cmi : compile/auto_pat.cmi
compile/lambda.cmi : runtime/value.cmi types/types.cmi \
types/type_tallying.cmi schema/schema_validator.cmi misc/ns.cmi \
misc/imap.cmi types/ident.cmo types/compunit.cmi compile/auto_pat.cmi
schema/schema_validator.cmi misc/ns.cmi misc/imap.cmi types/ident.cmo \
types/compunit.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/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.
We first build the ``skeleton'' of the typed ast
......@@ -17,14 +17,14 @@ type ttyp = Types.Node.t
type sigma = Types.Subst.t list
type texpr =
{ exp_loc : loc;
mutable exp_typ : Types.t;
type texpr =
{ exp_loc : loc;
mutable exp_typ : Types.t;
(* Currently exp_typ is not used. It will be used for compilation ! *)
mutable exp_descr : texpr';
}
and texpr' =
and texpr' =
| Forget of texpr * ttyp
| Check of (Types.t ref) * texpr * ttyp
(* CDuce is a Lambda-calculus ... *)
......@@ -36,14 +36,14 @@ and texpr' =
| ExtVar of Compunit.t * id * Types.t
| Apply of texpr * texpr
| Abstraction of abstr
(* Data constructors *)
| Cst of Types.const
| Pair of texpr * texpr
| Xml of texpr * texpr * Ns.table option
| RecordLitt of texpr label_map
| String of U.uindex * U.uindex * U.t * texpr
(* Data destructors *)
| Match of texpr * branches
| Map of texpr * branches
......@@ -61,8 +61,8 @@ and texpr' =
| Op of string * int * texpr list
| NsTable of Ns.table * texpr'
and abstr = {
fun_name : id option;
and abstr = {
fun_name : id option;
fun_iface : (Types.t * Types.t) list;
fun_body : branches;
fun_typ : Types.t;
......@@ -74,22 +74,36 @@ and let_decl = {
let_body : texpr;
}
and branches = {
and branches = {
mutable br_typ : Types.t; (* Type of values that can flow to branches *)
br_accept : Types.t; (* Type accepted by all branches *)
br_branches: branch list;
}
and branch = {
and branch = {
br_loc : loc;
mutable br_used : bool;
mutable br_used : bool;
br_ghost : bool;
mutable br_vars_empty : fv;
mutable br_vars_poly : Var.Set.t IdMap.map;
br_pat : tpat;
(* this field is mutable because we need to add substitutions *)
mutable br_body : texpr
mutable br_body : texpr
}
let pat_of_expr e =
let open Typepat in
let any_pat = mk_type Types.any in
let rec loop e =
match e.exp_descr with
Var id -> mk_capture id
| 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)
module Print = struct
let rec pp_const ppf cst =
......
......@@ -1172,7 +1172,7 @@ and type_check' loc env ed constr precise = match ed with
let acc = a.fun_body.br_accept in
if not (Types.subtype t1 acc) then
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 (Typepat.(pat_node (mk_type Types.any))) a.fun_body t2 true in
try
(Type_tallying.squaresubtype env.delta t t2)::tacc (* H_j *)
with
......@@ -1192,11 +1192,13 @@ and type_check' loc env ed constr precise = match ed with
| Match (e,b) ->
let t = type_check env e b.br_accept true in
(ed,type_check_branches loc env t b constr precise)
let parg = pat_of_expr e in
(ed,type_check_branches loc env t parg b constr precise)
| Try (e,b) ->
let te = type_check env e constr precise in
let tb = type_check_branches loc env Types.any b constr precise in
let parg = pat_of_expr e in
let tb = type_check_branches loc env Types.any parg b constr precise in
(ed,Types.cup te tb)
| Pair (e1,e2) ->
......@@ -1298,12 +1300,13 @@ and type_check' loc env ed constr precise = match ed with
| Xtrans (e,b) ->
let t = type_check env e Sequence.any true in
let parg = pat_of_expr e in
let t =
try
Sequence.map_tree constr
(fun cstr t ->
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)
) t
with (Sequence.Error _) as exn ->
......@@ -1417,16 +1420,16 @@ and type_record loc env r constr precise =
else constr
(* 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 parg brs constr precise =
if Types.is_empty targ then Types.empty
else begin
brs.br_typ <- Types.cup brs.br_typ targ;
branches_aux loc env targ
branches_aux loc env targ parg
(if precise then Types.empty else constr)
constr precise brs.br_branches
end
and branches_aux loc env targ tres constr precise = function
and branches_aux loc env targ parg tres constr precise = function
| [] -> tres
| b :: rem ->
let p = b.br_pat in
......@@ -1434,7 +1437,7 @@ and branches_aux loc env targ tres constr precise = function
let targ' = Types.cap targ acc in
if Types.is_empty targ' then
(* this branch cannot be selected: we ignore it *)
branches_aux loc env targ tres constr precise rem
branches_aux loc env targ parg tres constr precise rem
else begin
b.br_used <- true;
let res = Patterns.filter targ' p in (* t^i_j // p_j *)
......@@ -1445,8 +1448,15 @@ and branches_aux loc env targ tres constr precise = function
(IdMap.restrict res b.br_vars_empty)
);
let env' = enter_values (IdMap.get res) env in
let env_parg =
if Types.subtype targ' (Types.descr (Patterns.accept parg)) then
let res_parg = Patterns.filter targ' parg in
let res_parg = IdMap.map Types.descr res_parg in
enter_values (IdMap.get res_parg) env
else
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 *)
let xj =
IdMap.fold (fun x t acc ->
......@@ -1462,7 +1472,7 @@ and branches_aux loc env targ tres constr precise = function
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
branches_aux loc env targ'' parg tres constr precise rem
else
tres
end
......@@ -1470,7 +1480,7 @@ and branches_aux loc env targ tres constr precise = function
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 t = type_check env e acc true in
let parg = pat_of_expr e in
let constr' = Sequence.approx (Types.cap Sequence.any constr) in
let exact = Types.subtype (Sequence.star constr') constr in
(* Note:
......@@ -1481,7 +1491,7 @@ and type_map loc env def e b constr precise =
Sequence.map
(fun t ->
let res =
type_check_branches loc env t b constr' (precise || (not exact)) in
type_check_branches loc env t parg b constr' (precise || (not exact)) in
if def && not (Types.subtype t b.br_accept)
then (require loc Sequence.nil_type constr'; Types.cup res Sequence.nil_type)
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