Commit 3aab1b01 authored by Kim Nguyễn's avatar Kim Nguyễn

Implement a safety-check to guarantee that recursive parametric types

remain regular. Within their recursive definitions, parametric types
must always be instantiated with their original parameters and all
types of mutually recursive definitions must have the same parameters.

We use Tarjan's strongly connected components algorithm to group type definitions accordingly.
parent 64b01477
......@@ -113,11 +113,18 @@ and ppat' =
| Arrow of ppat * ppat
| Optional of ppat
| Record of bool * (label * (ppat * ppat option)) list
(* Record (o, (l,(p1, p2)) list )
o : true => open record
l : field label
p1 : pattern expression (Optional if l=?pat )
p2 : Some p3 => else p3 *)
| Constant of U.t * pexpr
| Regexp of regexp
| Concat of ppat * ppat
| Merge of ppat * ppat
and regexp =
| Epsilon
| Elem of ppat
......@@ -160,3 +167,36 @@ let rec print_re fmt e =
| WeakStar (e0) -> Format.fprintf fmt "WeakStar(%a)" print_re e0
| SeqCapture (_, e0) -> Format.fprintf fmt "SeqCapture(_, %a)" print_re e0
| Arg (e0) -> Format.fprintf fmt "Arg(%a)" print_re e0
let rec pat_fold f acc p =
let nacc = f acc p in
match p.descr with
| PatVar _ | Cst _ | NsT _
| Internal _ | Constant _ -> nacc
| Recurs (p0, pl) ->
List.fold_left (fun acc (_,_,pi) -> pat_fold f acc pi) (pat_fold f nacc p0) pl
| Or (p1, p2) | And (p1, p2)
| Diff (p1, p2) | Prod (p1, p2)
| XmlT (p1, p2) | Arrow (p1, p2)
| Concat (p1, p2) | Merge (p1, p2) -> pat_fold f (pat_fold f nacc p1) p2
| Optional p0 -> pat_fold f nacc p0
| Record (_, pl) -> List.fold_left (fun acc (_,(p1, op2)) ->
let acc1 = pat_fold f nacc p1 in
match op2 with None -> acc1 | Some p2 -> pat_fold f acc1 p2) nacc pl
| Regexp e -> re_fold (fun acc e -> match e with Elem p -> pat_fold f acc p | _ -> acc) nacc e
and re_fold f acc e =
let nacc = f acc e in
match e with
| Epsilon | Elem _ | Guard _ -> nacc
| Seq (e1, e2)
| Alt (e1, e2) -> re_fold f (re_fold f nacc e1) e2
| Star (e0) | WeakStar (e0)
| SeqCapture (_, e0) | Arg (e0) -> re_fold f nacc e0
let pat_iter f p = pat_fold (fun () p -> f p) () p
let re_iter f e = re_fold (fun () e -> f e) () e
......@@ -243,7 +243,7 @@ let navig loc env0 (env,comp) id =
let rec find_global env loc ids =
match ids with
| id::rest ->
let comp = find_id env env loc true id in
let comp = find_id env env loc (*true*) (rest != []) id in
snd (List.fold_left (navig loc env) (env,comp) rest)
| _ -> assert false
......@@ -309,6 +309,82 @@ module IType = struct
(* From AST to the intermediate representation *)
(* We need to be careful about the order of type definitions in case
of polymorphic types. Mutually recursive polymorphic types
cannot be recursively called with different parameters within
their recursive groups. We build a graph from the type
definitions and use Tarjan's algorithm to find all strongly
connected components in topological order. Then we translate the
AST into intermediate representation in that order. *)
let scc defs =
let module Info =
struct
type t =
{ mutable index : int;
mutable lowlink : int;
mutable is_removed : bool;
def : (loc * U.t) * U.t list * ppat;
}
let empty = { index = -1; lowlink = -1;
is_removed = false;
def = ((noloc,U.empty), [],
(mknoloc (Internal(Types.empty)))) }
end
in
let open Info in
let index = ref 0 and stack = ref [] in
let res = ref [] and map = Hashtbl.create 17 and rank = ref ~-1 in
let g = Hashtbl.create 17 in
List.iter (fun (((_, v), _, _) as def) ->
Hashtbl.add g v { empty with def = def }) defs;
let rec strong_connect v vinfo =
vinfo.index <- !index;
vinfo.lowlink <- !index;
incr index;
stack := v :: !stack;
vinfo.is_removed <- false;
let _,_, vdef = vinfo.def in
pat_iter (fun p ->
match p.descr with
| PatVar ([ w ], _) ->
let winfo = try Some (Hashtbl.find g w) with Not_found -> None in begin
match winfo with Some winfo ->
if winfo.index == -1 then begin
strong_connect w winfo;
vinfo.lowlink <- min vinfo.lowlink winfo.lowlink
end else if not winfo.is_removed then
vinfo.lowlink <- min vinfo.lowlink winfo.index
| _ -> ()
end
| _ -> ()
) vdef;
if vinfo.lowlink == vinfo.index then
let cc = ref [] in incr rank;
while let w = List.hd !stack in
stack := List.tl !stack;
let winfo = Hashtbl.find g w in
let _, params, _ = winfo.def in
Hashtbl.add map w (!rank, params);
cc := winfo.def :: !cc;
winfo.is_removed <- true;
not (U.equal w v) do () done;
res := !cc :: !res
in
let () = List.iter
(fun ((_, v), _, _) ->
let vinfo = Hashtbl.find g v in
if vinfo.index == -1 then
strong_connect v vinfo) defs
in
(*
Format.eprintf "SCC of type definitions are :@\n";
List.iter (fun l ->
Format.eprintf "%a@\n"
(Utils.pp_list (fun ppf ((_,v),_,_) -> U.print ppf v)) l ) res;
*)
List.rev !res, map
type penv = {
penv_tenv : t;
penv_derec : (node * U.t list) Env.t;
......@@ -318,8 +394,13 @@ module IType = struct
let penv tenv = { penv_tenv = tenv; penv_derec = Env.empty ; penv_var = Hashtbl.create 17 }
let all_delayed = ref []
let dummy_params = (-1, [], Hashtbl.create 0)
let current_params = ref dummy_params
let clean_on_err () = all_delayed := []
let clean_params () = current_params := dummy_params
let clean_on_err () =
all_delayed := [];
clean_params ()
let delayed loc =
let s = mk_delayed () in
......@@ -334,7 +415,6 @@ module IType = struct
all_delayed := [];
List.iter check_one_delayed l
let seq_to_list e =
let rec loop e acc =
match e with
......@@ -367,6 +447,15 @@ module IType = struct
| Arg e0 -> clean_re e0
| _ -> e
let rec comp_var_pat vl pl =
match vl, pl with
[], [] -> true
| v :: vll, { descr = Internal (p); _ } :: pll ->
Types.is_var p
&& (U.equal v (U.mk(Var.(id (Set.choose (Types.all_vars p))))))
&& comp_var_pat vll pll
| _ -> false
(* Ast -> symbolic type *)
let rec derecurs env p =
match p.descr with
......@@ -412,7 +501,7 @@ module IType = struct
Array.length (snd (find_local_type env.penv_tenv loc id))
else
Array.length (snd (find_global_type env.penv_tenv loc ids))
with Not_found -> 0
with _ -> 0
in
if nargs != 0 then (* instantiation *)
mk_elem (derecurs env { loc; descr = PatVar(ids, prod_to_list t2) })
......@@ -429,20 +518,31 @@ module IType = struct
and derecurs_var env loc ids =
match ids with
| ([v],a) ->
let v = ident env.penv_tenv loc v in
| ((id :: rest) as ids, args) ->
let cidx, cparams, cmap = !current_params in
let v = ident env.penv_tenv loc id in
begin
try fst (Env.find v env.penv_derec)
try
let node = fst (Env.find v env.penv_derec) in
if args == [] || comp_var_pat cparams args then node else
raise_loc_generic loc (Printf.sprintf "Invalid instantiation of type %s during its recursive definition" (U.to_string id))
with Not_found ->
try
let (t,pargs) = find_local_type env.penv_tenv loc v in
try
let (t, pargs), tidx =
if rest == [] then
(find_local_type env.penv_tenv loc v,
try fst (Hashtbl.find cmap id) with Not_found -> ~-1)
else (find_global_type env.penv_tenv loc ids, ~-1)
in
let palen = Array.length pargs in
if palen <> List.length a then
if palen <> List.length args then
raise_loc_generic loc
(Printf.sprintf "Parametric type %s is not fully instanciated" (Ident.to_string v));
let a = Array.of_list a in
(Printf.sprintf "Wrong number of parameters for parametric type %s" (U.to_string id));
if cidx >= 0 && tidx == cidx && not (comp_var_pat cparams args) then
raise_loc_generic loc (Printf.sprintf "Invalid instantiation of type %s during its recursive definition" (U.to_string id));
let a = Array.of_list args in
let l = ref [] in
for i=0 to (Array.length pargs) - 1 do
for i = 0 to (Array.length pargs) - 1 do
try
let err s = Error s in
let tai = typ ~err (derecurs env a.(i)) in
......@@ -453,14 +553,14 @@ module IType = struct
done;
mk_type (Types.Positive.substitute_list t !l)
with Not_found ->
if List.length a >= 1 then
assert (rest == []);
if args != [] then
raise_loc_generic loc
(Printf.sprintf "Parametric type %s does not exists" (Ident.to_string v))
(Printf.sprintf "Unknown parametric type %s" (U.to_string id))
else
mk_capture v
end
| (ids,_) ->
mk_type (fst(find_global_type env.penv_tenv loc ids))
| _ -> assert false
and derecurs_def env b =
let seen = ref IdSet.empty in
......@@ -546,8 +646,34 @@ module IType = struct
) b;
enter_types b env
let equal_params l1 l2 =
try
List.for_all2 U.equal l1 l2
with _ -> false
let check_params l =
match l with
| [] -> assert false
| [ ((_, u),_,_) ] -> u
| ((loc1,u),p,_) :: r ->
try
let (loc2,v),_,_ =
List.find (fun (_,q,_) -> not (equal_params p q)) r
in
let loc = merge_loc loc1 loc2 in
error loc (Printf.sprintf "mutually recursive types %s and %s have different type parameters" (U.to_string u) (U.to_string v))
with Not_found -> u
let type_defs env b =
try type_defs env b
try
let b, map = scc b in
let r = List.fold_left (fun env b ->
let u = check_params b in
let idx, params = Hashtbl.find map u in
current_params := (idx,params,map);
type_defs env b
) env b in
clean_params (); r
with exn -> clean_on_err (); raise exn
let typ env t =
......
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