Commit ffd2b30c authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Fix a bug when disambiguating application of polymorphic types in regular expressions.

parent 36ff0c74
Pipeline #168 passed with stages
in 7 minutes and 39 seconds
......@@ -67,7 +67,7 @@ type t = {
ns : Ns.table;
keep_ns : bool;
poly_vars : (U.t * Var.t) list;
mono_vars : Var.Set.t
mono_vars : Var.Set.t;
}
(* Namespaces *)
......@@ -116,7 +116,13 @@ let type_schema env loc name uri =
{ env with ids = Env.add x (ESchema sch) env.ids }
let empty_env =
{ ids = Env.empty; ns = Ns.def_table; keep_ns = false; poly_vars = []; mono_vars = Var.Set.empty }
{
ids = Env.empty;
ns = Ns.def_table;
keep_ns = false;
poly_vars = [];
mono_vars = Var.Set.empty;
}
let enter_id x i env = { env with ids = Env.add x i env.ids }
......@@ -411,11 +417,10 @@ module IType = struct
let to_register = ref []
let clean_params () =
let clean_params () =
current_params := dummy_params;
to_register := []
let clean_on_err () =
all_delayed := [];
clean_params ()
......@@ -463,6 +468,18 @@ module IType = struct
"Invalid instantiation of type '%s' during its recursive definition"
(U.to_string s))
let rec clean_regexp r =
match r with
| Epsilon | Elem _ | Guard _ -> r
| Alt (r1, r2) -> Alt (clean_regexp r1, clean_regexp r2)
| Star r -> Star (clean_regexp r)
| WeakStar r -> WeakStar (clean_regexp r)
| SeqCapture (loc, id, r) -> SeqCapture (loc, id, clean_regexp r)
| Seq (r1, r2) -> (
match clean_regexp r1 with
| Seq (e, rr1) -> Seq (e, clean_regexp (Seq (rr1, r2)))
| e -> Seq (e, clean_regexp r2))
let rec derecurs env p =
match p.descr with
| Poly v ->
......@@ -498,7 +515,7 @@ module IType = struct
| Constant (x, c) ->
mk_constant (ident env.penv_tenv p.loc x) (const env.penv_tenv p.loc c)
| Cst c -> mk_type (Types.constant (const env.penv_tenv p.loc c))
| Regexp r -> rexp (derecurs_regexp env r)
| Regexp r -> rexp (derecurs_regexp env (clean_regexp r))
| Concat (p1, p2) -> mk_concat (derecurs env p1) (derecurs env p2)
| Merge (p1, p2) -> mk_merge (derecurs env p1) (derecurs env p2)
......@@ -508,7 +525,13 @@ module IType = struct
| Guard p -> mk_guard (derecurs env p)
| Seq
( (Elem { descr = PatVar ((id :: rest as ids), []); loc } as p1),
(Elem arg as p2) ) ->
((Elem _| Seq (Elem _, _)) as p2)
) ->
let arg, make = match p2 with
Elem arg -> arg, fun x -> x
| Seq (Elem arg, pp2) -> arg, fun x -> mk_seq x (derecurs_regexp env pp2)
| _ -> assert false
in
let v = ident env.penv_tenv loc id in
let patch_arg =
try
......@@ -522,7 +545,7 @@ module IType = struct
with Not_found -> false
in
if patch_arg then
mk_elem (derecurs env { descr = PatVar (ids, [ arg ]); loc })
make (mk_elem (derecurs env { descr = PatVar (ids, [ arg ]); loc }))
else mk_seq (derecurs_regexp env p1) (derecurs_regexp env p2)
| Seq (p1, p2) -> mk_seq (derecurs_regexp env p1) (derecurs_regexp env p2)
| Alt (p1, p2) -> mk_alt (derecurs_regexp env p1) (derecurs_regexp env p2)
......@@ -569,8 +592,10 @@ module IType = struct
| None ->
raise_loc_generic loc
(Printf.sprintf
"Wrong number of parameters for parametric type %s"
(U.to_string id))
"Wrong number of parameters for parametric type %s (%d, %d)"
(U.to_string id)
(List.length pargs) (List.length args)
)
in
let sub = Types.Subst.from_list l in
let ti = mk_type (Types.Subst.apply_full sub t) in
......@@ -670,7 +695,7 @@ module IType = struct
let vars_args = List.map (fun v -> List.assoc v penv.penv_var) args in
let final_vars =
(* create a sequence 'a -> 'a_0 for all variables *)
List.map (fun v -> v, Var.(mk (name v))) vars_args
List.map (fun v -> (v, Var.(mk (name v)))) vars_args
in
let subst =
Types.Subst.from_list
......@@ -741,10 +766,10 @@ module IType = struct
let d = derec penv t in
let res = aux t.loc d in
List.iter
(fun (cu, name, params, ti, loc) ->
let tti = aux loc ti in
Types.Print.register_global cu name ~params (Types.descr tti))
!to_register;
(fun (cu, name, params, ti, loc) ->
let tti = aux loc ti in
Types.Print.register_global cu name ~params (Types.descr tti))
!to_register;
clean_params ();
res
with exn ->
......@@ -1008,24 +1033,26 @@ and var env loc s =
with Not_found -> raise_loc loc (UnboundId (id, false)))
and abstraction env loc a =
(* When entering a function (fun 'a 'b ... .('a -> 'b -> … ))
for each variable 'x from the interface
- if 'x is in env.poly_vars, it is bound higher in the AST, we need
to keep the associated unique variable
- if 'x is not in env.poly_vars or 'x is in a.fun_poly, a fresh
name must be generated and kept for subsequent use of the variable.
*)
let vset = (* collect all type variables from the interface*)
(* When entering a function (fun 'a 'b ... .('a -> 'b -> … ))
for each variable 'x from the interface
- if 'x is in env.poly_vars, it is bound higher in the AST, we need
to keep the associated unique variable
- if 'x is not in env.poly_vars or 'x is in a.fun_poly, a fresh
name must be generated and kept for subsequent use of the variable.
*)
let vset =
(* collect all type variables from the interface*)
List.fold_left
(fun acc (t1, t2) -> collect_vars (collect_vars acc t1) t2)
USet.empty a.fun_iface
in
let vset = (* remove variables that are in scope *)
let vset =
(* remove variables that are in scope *)
List.fold_left (fun acc (v, _) -> USet.remove v acc) vset env.poly_vars
in
let vset = List.fold_left (fun acc v -> USet.add v acc) vset a.fun_poly in
(* add those that are explicitely polymorphic. *)
let all_vars =
let all_vars =
USet.fold (fun v acc -> (v, Var.mk (U.get_str v)) :: acc) vset env.poly_vars
in
let iface =
......@@ -1056,7 +1083,7 @@ and abstraction env loc a =
Typed.fun_body = body;
Typed.fun_typ = t;
Typed.fun_fv = fv;
Typed.fun_is_poly = not (Var.Set.is_empty (Types.Subst.vars t));
Typed.fun_is_poly = not (Var.Set.is_empty (Types.Subst.vars t));
}
in
exp loc fv e
......@@ -1236,24 +1263,34 @@ and type_check' loc env e constr precise =
ignore (type_check env e t false);
verify loc t constr
| Check (t0, e, t) ->
if Var.Set.is_empty Types.(Subst.vars (descr t)) then
let te = type_check env e Types.any true in
t0 := Types.cup !t0 te;
verify loc (Types.cap te (Types.descr t)) constr
else error loc "Polymorphic type variables cannot occur in dynamic type-checks"
if Var.Set.is_empty Types.(Subst.vars (descr t)) then (
let te = type_check env e Types.any true in
t0 := Types.cup !t0 te;
verify loc (Types.cap te (Types.descr t)) constr)
else
error loc
"Polymorphic type variables cannot occur in dynamic type-checks"
| Abstraction a ->
let t =
if Types.subtype a.fun_typ constr then a.fun_typ
else
let name = match a.fun_name with Some s -> "abstraction " ^ Ident.to_string s| None -> "the abstraction" in
should_have loc constr (Format.asprintf
"but the interface (%a) of %s is not compatible with type
(%a)"
Types.Print.print a.fun_typ
name
Types.Print.print constr)
let name =
match a.fun_name with
| Some s -> "abstraction " ^ Ident.to_string s
| None -> "the abstraction"
in
should_have loc constr
(Format.asprintf
"but the interface (%a) of %s is not compatible with type\n\
\ (%a)" Types.Print.print a.fun_typ name
Types.Print.print constr)
in
let env =
{
env with
mono_vars = Var.Set.cup env.mono_vars (Types.Subst.vars a.fun_typ);
}
in
let env = { env with mono_vars = Var.Set.cup env.mono_vars (Types.Subst.vars a.fun_typ) } in
let env =
match a.fun_name with
| None -> env
......@@ -1287,16 +1324,18 @@ and type_check' loc env e constr precise =
let dom = Types.Arrow.domain t1arrow in
let t2 = type_check env e2 Types.any true in
let res =
if Var.Set.is_empty (Types.Subst.vars t1) &&
Var.Set.is_empty (Types.Subst.vars t2) then
(* TODO don't retype e2 *)
let t2 = type_check env e2 dom true in
Types.Arrow.apply t1arrow t2
else
match Types.Tallying.squareapply env.mono_vars t1 t2 with
None -> raise_loc loc (Constraint(t2, dom))
| Some (_, res) -> res
(*
if
Var.Set.is_empty (Types.Subst.vars t1)
&& Var.Set.is_empty (Types.Subst.vars t2)
then
(* TODO don't retype e2 *)
let t2 = type_check env e2 dom true in
Types.Arrow.apply t1arrow t2
else
match Types.Tallying.squareapply env.mono_vars t1 t2 with
| None -> raise_loc loc (Constraint (t2, dom))
| Some (_, res) -> res
(*
if Types.Arrow.need_arg t1 then
let t2 = type_check env e2 dom true in
Types.Arrow.apply t1 t2
......@@ -1560,17 +1599,19 @@ let type_let_decl env p e =
let decl = let_decl env p e in
let typs = type_let_decl env decl in
report_unused_branches ();
let typs = List.map
(fun (id, t) ->
let tt = Types.Subst.clean_type Var.Set.empty t in
let vars = Types.Subst.vars tt in
if not (Var.Set.is_empty vars) then
raise_loc_generic p.loc
(Format.asprintf "The type of identifier %a is %a.@\nIt contains polymorphic variables that cannot be generalized."
Ident.print id
Types.Print.print tt);
(id, tt)
) typs
let typs =
List.map
(fun (id, t) ->
let tt = Types.Subst.clean_type Var.Set.empty t in
let vars = Types.Subst.vars tt in
if not (Var.Set.is_empty vars) then
raise_loc_generic p.loc
(Format.asprintf
"The type of identifier %a is %a.@\n\
It contains polymorphic variables that cannot be generalized."
Ident.print id Types.Print.print tt);
(id, tt))
typs
in
let env = enter_values typs env in
({ env with mono_vars = Var.Set.empty; poly_vars = [] }, decl, typs)
......
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