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

Perform a more aggressive memoization of substituted types and register the...

Perform a more aggressive memoization of substituted types and register the name if the original type was named.
Make the pretty-printer re-entrant.
parent 6149608a
let string_of_formatter pp t = let string_of_formatter pp t =
ignore (Format.flush_str_formatter ());
Format.fprintf Format.str_formatter "%a" pp t; Format.fprintf Format.str_formatter "%a" pp t;
Format.flush_str_formatter () Format.flush_str_formatter ()
...@@ -11,4 +12,3 @@ let pp_list ?(delim=("[","]")) ?(sep=",") f ppf l = ...@@ -11,4 +12,3 @@ let pp_list ?(delim=("[","]")) ?(sep=",") f ppf l =
match l with match l with
|[] -> Format.fprintf ppf "%s%s" (fst delim) (snd delim) |[] -> Format.fprintf ppf "%s%s" (fst delim) (snd delim)
|_ -> Format.fprintf ppf "%s%a%s" (fst delim) aux l (snd delim) |_ -> Format.fprintf ppf "%s%a%s" (fst delim) aux l (snd delim)
...@@ -171,7 +171,7 @@ let load_schema schema_name uri = ...@@ -171,7 +171,7 @@ let load_schema schema_name uri =
let schema_name = schema_name ^ "." in let schema_name = schema_name ^ "." in
let log_schema_component kind name cd_type = let log_schema_component kind name cd_type =
if not (Schema_builtin.is name) then begin if not (Schema_builtin.is name) then begin
Types.Print.register_global (schema_name,name,[||]) cd_type; Types.Print.register_global (schema_name,name,[]) cd_type;
(* Format.fprintf Format.std_formatter "Registering schema %s: %a@." kind (* Format.fprintf Format.std_formatter "Registering schema %s: %a@." kind
Ns.QName.print name; *) Ns.QName.print name; *)
......
...@@ -32,7 +32,7 @@ let env = ...@@ -32,7 +32,7 @@ let env =
List.fold_left List.fold_left
(fun accu (n,t) -> (fun accu (n,t) ->
let n = (Ns.empty, Ident.U.mk n) in let n = (Ns.empty, Ident.U.mk n) in
Types.Print.register_global ("",n,[||]) t; Types.Print.register_global ("",n,[]) t;
Typer.enter_type (Ident.ident n) t accu Typer.enter_type (Ident.ident n) t accu
) )
Typer.empty_env Typer.empty_env
......
...@@ -1642,7 +1642,7 @@ module Print = struct ...@@ -1642,7 +1642,7 @@ module Print = struct
let is_regexp t = subtype t seqs_descr let is_regexp t = subtype t seqs_descr
type gname = string * Ns.QName.t * t array type gname = string * Ns.QName.t * (Var.var * t) list
type nd = { type nd = {
id : int; id : int;
...@@ -2315,10 +2315,25 @@ module Print = struct ...@@ -2315,10 +2315,25 @@ module Print = struct
| r -> (List.rev accu,Some r) | r -> (List.rev accu,Some r)
and print_gname ppf = function and print_gname ppf = function
|(cu,n,[||]) -> Format.fprintf ppf "%s%a" cu Ns.QName.print n |(cu,n,[]) -> Format.fprintf ppf "@[%s%a@]" cu Ns.QName.print n
|(cu,n,al) -> |(cu,n,al) ->
Format.fprintf ppf "%s%a(%s)" cu Ns.QName.print n let local_pp ppf t =
(String.concat "," (List.map (Utils.string_of_formatter pp_type) (Array.to_list al))) let old_to_print = !to_print in
let old_count_name = !count_name in
let old_memo = DescrHash.copy memo in
to_print := [];
count_name := 0;
DescrHash.clear memo;
pp_type ppf t;
to_print := old_to_print;
count_name := old_count_name;
DescrHash.iter (fun k v -> DescrHash.add memo k v) old_memo
in
Format.fprintf ppf "@[%s%a " cu Ns.QName.print n;
Utils.pp_list ~delim:("(",")") local_pp ppf
(List.map snd al);
Format.fprintf ppf "@]"
and pp_type ppf t = and pp_type ppf t =
let t = uniq t in let t = uniq t in
...@@ -2814,7 +2829,9 @@ module Positive = struct ...@@ -2814,7 +2829,9 @@ module Positive = struct
apply_subst ~subst:subst ~after:(fun y -> define x y;x) t apply_subst ~subst:subst ~after:(fun y -> define x y;x) t
(* Pre-condition : alpha \not\in \delta *) (* Pre-condition : alpha \not\in \delta *)
module MemoSubst = Hashtbl.Make (struct module MemoSubst =
struct
include Hashtbl.Make (struct
type t = descr * (Var.t * descr) list type t = descr * (Var.t * descr) list
let hash (t, l) = let hash (t, l) =
List.fold_left List.fold_left
...@@ -2826,23 +2843,13 @@ module Positive = struct ...@@ -2826,23 +2843,13 @@ module Positive = struct
Var.equal v1 v2 && Descr.equal t1 t2) l1 l2 with _ -> false) Var.equal v1 v2 && Descr.equal t1 t2) l1 l2 with _ -> false)
end) end)
let memo_subst = MemoSubst.create 17 end
let () = at_exit (fun () ->
Format.eprintf "%i@\n%!" (MemoSubst.length memo_subst))
let substitute t (alpha,s) =
let k = (t, [(alpha, s)]) in
try
MemoSubst.find memo_subst k
with Not_found ->
let r =
let vs = ty s in
let subst d = if Var.equal d alpha then vs else var d in
apply_subst ~subst:subst t
in
MemoSubst.add memo_subst k r; r
let substitute_list t l = let memo_subst = MemoSubst.create 17
let rec substitute_list t l =
if no_var t || l == [] then t else
let k = (t,l) in let k = (t,l) in
try try
MemoSubst.find memo_subst k MemoSubst.find memo_subst k
...@@ -2857,7 +2864,20 @@ module Positive = struct ...@@ -2857,7 +2864,20 @@ module Positive = struct
in in
apply_subst ~subst:subst t apply_subst ~subst:subst t
in in
MemoSubst.add memo_subst k r; r let () =
try
let (cu, name, subst) = DescrMap.find t !Print.named in
let _nsubst =
List.map (fun (v, vt) -> v, substitute_list vt l) subst
in
Print.register_global (cu, name, _nsubst) r;
with Not_found -> ()
in
MemoSubst.add memo_subst k r;
r
let substitute t s = substitute_list t [s]
let substitute_free delta t = let substitute_free delta t =
......
...@@ -321,7 +321,7 @@ val cond_partition: t -> (t * t) list -> t list ...@@ -321,7 +321,7 @@ val cond_partition: t -> (t * t) list -> t list
to answer all the questions. *) to answer all the questions. *)
module Print : sig module Print : sig
type gname = string * Ns.QName.t * t array type gname = string * Ns.QName.t * (Var.var * t) list
val register_global : gname -> t -> unit val register_global : gname -> t -> unit
val pp_const : Format.formatter -> const -> unit val pp_const : Format.formatter -> const -> unit
val pp_type: Format.formatter -> t -> unit val pp_type: Format.formatter -> t -> unit
......
module V = struct module V = struct
type t = { id : Ident.U.t ; fr : int ; kind : int } type t = { id : Ident.U.t ; fr : int ; kind : int }
type kind = int type kind = int
......
...@@ -30,7 +30,7 @@ type schema = { ...@@ -30,7 +30,7 @@ type schema = {
type item = type item =
(* These are really exported by CDuce units: *) (* These are really exported by CDuce units: *)
| Type of (Types.t * Var.t array) | Type of (Types.t * Var.t list)
| Val of Types.t | Val of Types.t
| ECDuce of Compunit.t | ECDuce of Compunit.t
| ESchema of schema | ESchema of schema
...@@ -51,10 +51,10 @@ type t = { ...@@ -51,10 +51,10 @@ type t = {
let pp_env ppf env = let pp_env ppf env =
let pp_item ppf (s,t) = match t with let pp_item ppf (s,t) = match t with
|Val t -> Format.fprintf ppf "val %s : %a" s Types.Print.pp_type t |Val t -> Format.fprintf ppf "val %s : %a" s Types.Print.pp_type t
|Type (t,[||]) -> Format.fprintf ppf "type %s = %a" s Types.Print.pp_noname t |Type (t,[]) -> Format.fprintf ppf "type %s = %a" s Types.Print.pp_noname t
|Type (t,al) -> |Type (t,al) ->
Format.fprintf ppf "type %s(%a) = %a" s Format.fprintf ppf "type %s(%a) = %a" s
(Utils.pp_list ~delim:("","") Var.pp) (Array.to_list al) (Utils.pp_list ~delim:("","") Var.pp) al
Types.Print.pp_noname t Types.Print.pp_noname t
|_ -> () |_ -> ()
in in
...@@ -138,11 +138,11 @@ let type_using env loc x cu = ...@@ -138,11 +138,11 @@ let type_using env loc x cu =
with Not_found -> with Not_found ->
error loc ("Cannot find external unit " ^ (U.to_string cu)) error loc ("Cannot find external unit " ^ (U.to_string cu))
let enter_type id t env = enter_id id (Type (t,[||])) env let enter_type id t env = enter_id id (Type (t,[])) env
let enter_types l env = let enter_types l env =
{ env with ids = { env with ids =
List.fold_left (fun accu (id,t,al) -> List.fold_left (fun accu (id,t,al) ->
Env.add id (Type (t,al)) accu Env.add id (Type (t,List.map fst al)) accu
) env.ids l ) env.ids l
} }
...@@ -186,7 +186,9 @@ let iter_values env f = ...@@ -186,7 +186,9 @@ let iter_values env f =
let register_types cu env = let register_types cu env =
Env.iter (fun x -> function Env.iter (fun x -> function
| Type (t,_) -> Types.Print.register_global (cu,(Ident.value x),[||]) t | Type (t,vars) ->
let subst = List.map (fun x -> x, Types.var x) vars in
Types.Print.register_global (cu,(Ident.value x), subst) t
| _ -> () | _ -> ()
) env.ids ) env.ids
...@@ -265,7 +267,7 @@ let type_ns env loc p ns = ...@@ -265,7 +267,7 @@ let type_ns env loc p ns =
let find_global_type env loc ids = let find_global_type env loc ids =
match find_global env loc ids with match find_global env loc ids with
| Type (t,pargs) -> (t,pargs) | Type (t,pargs) -> (t,pargs)
| ESchemaComponent (t,_) -> (t,[||]) (* XXX *) | ESchemaComponent (t,_) -> (t,[]) (* XXX *)
| _ -> error loc "This path does not refer to a type" | _ -> error loc "This path does not refer to a type"
let find_global_schema_component env loc ids = let find_global_schema_component env loc ids =
...@@ -498,9 +500,9 @@ module IType = struct ...@@ -498,9 +500,9 @@ module IType = struct
let id = ident env.penv_tenv loc id in let id = ident env.penv_tenv loc id in
try List.length (snd (Env.find id env.penv_derec)) try List.length (snd (Env.find id env.penv_derec))
with Not_found -> with Not_found ->
Array.length (snd (find_local_type env.penv_tenv loc id)) List.length (snd (find_local_type env.penv_tenv loc id))
else else
Array.length (snd (find_global_type env.penv_tenv loc ids)) List.length (snd (find_global_type env.penv_tenv loc ids))
with _ -> 0 with _ -> 0
in in
if nargs != 0 then (* instantiation *) if nargs != 0 then (* instantiation *)
...@@ -534,24 +536,19 @@ module IType = struct ...@@ -534,24 +536,19 @@ module IType = struct
try fst (Hashtbl.find cmap id) with Not_found -> ~-1) try fst (Hashtbl.find cmap id) with Not_found -> ~-1)
else (find_global_type env.penv_tenv loc ids, ~-1) else (find_global_type env.penv_tenv loc ids, ~-1)
in in
let palen = Array.length pargs in
if palen <> List.length args then
raise_loc_generic loc
(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 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)); 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 err s = Error s in
let l = ref [] in let l =
for i = 0 to (Array.length pargs) - 1 do
try try
let err s = Error s in List.map2
let tai = typ ~err (derecurs env a.(i)) in (fun v p -> (v, typ ~err (derecurs env p))) pargs args
l := (pargs.(i), tai )::!l with Invalid_argument _ ->
with raise_loc_generic loc
|Error s -> raise_loc_generic loc s (Printf.sprintf "Wrong number of parameters for parametric type %s" (U.to_string id));
|_ -> assert false | Error s -> raise_loc_generic loc s
done; in
mk_type (Types.Positive.substitute_list t !l) mk_type (Types.Positive.substitute_list t l)
with Not_found -> with Not_found ->
assert (rest == []); assert (rest == []);
if args != [] then if args != [] then
...@@ -572,15 +569,15 @@ module IType = struct ...@@ -572,15 +569,15 @@ module IType = struct
("Multiple definitions for the type identifer " ^ ("Multiple definitions for the type identifer " ^
(Ident.to_string v)); (Ident.to_string v));
seen := IdSet.add v !seen; seen := IdSet.add v !seen;
(v,args,p,delayed loc) (v,loc,args,p,delayed loc)
) b ) b
in in
let n = List.fold_left let n = List.fold_left
(fun env (v,a,p,s) -> Env.add v (s,a) env) (fun env (v,_,a,p,s) -> Env.add v (s,a) env)
env.penv_derec b env.penv_derec b
in in
let env = { env with penv_derec = n } in let env = { env with penv_derec = n } in
List.iter (fun (v,_, p,s) -> link s (derecurs env p)) b; List.iter (fun (v,_,_, p,s) -> link s (derecurs env p)) b;
(env, b) (env, b)
let derec penv p = let derec penv p =
...@@ -600,7 +597,7 @@ module IType = struct ...@@ -600,7 +597,7 @@ module IType = struct
("Capture variable not allowed: " ^ (Ident.to_string x)) ("Capture variable not allowed: " ^ (Ident.to_string x))
let type_defs env b = let type_defs env b =
let _,b' = derecurs_def (penv env) b in let _, b = derecurs_def (penv env) b in
elim_concats (); elim_concats ();
check_delayed (); check_delayed ();
let aux loc d = let aux loc d =
...@@ -610,39 +607,31 @@ module IType = struct ...@@ -610,39 +607,31 @@ module IType = struct
with Patterns.Error s -> raise_loc_generic loc s with Patterns.Error s -> raise_loc_generic loc s
in in
let b = let b =
List.map2 (fun ((loc,v),pl,p) (v',_,_, d) -> List.map (fun (v, loc, args, _, d) ->
let t_rhs = aux loc d in let t_rhs = aux loc d in
if (loc <> noloc) && (Types.is_empty t_rhs) then if (loc <> noloc) && (Types.is_empty t_rhs) then
warning loc warning loc
("This definition yields an empty type for " ^ (U.to_string v)); ("This definition yields an empty type for " ^ (Ident.to_string v));
let vars_rhs = Types.all_vars t_rhs in let vars_rhs = Types.all_vars t_rhs in
if List.exists (fun x -> not (Var.Set.mem (Var.mk (U.to_string x)) vars_rhs)) args then
raise_loc_generic loc
(Printf.sprintf "Definition of type %s contains unbound type variables"
(Ident.to_string v));
let vars_mapping = (* create a sequence 'a -> 'a_0 for all variables *) let vars_mapping = (* create a sequence 'a -> 'a_0 for all variables *)
List.map (fun v -> let vv = Var.mk (Ident.U.to_string v) in vv, Var.fresh vv) pl List.map (fun v -> let vv = Var.mk (U.to_string v) in vv, Var.fresh vv) args
in
let vars_lhs =
List.fold_left (fun acc (v, _) -> Var.Set.add v acc) Var.Set.empty vars_mapping
in in
if not (Var.Set.subset vars_rhs vars_lhs) then let sub_list = List.map (fun (v,vt) -> v, Types.var vt) vars_mapping in
error loc
(Printf.sprintf "Definition of type %s contains unbound type variables"
(U.to_string v));
let t_rhs = let t_rhs =
Types.Positive.substitute_list t_rhs Types.Positive.substitute_list t_rhs sub_list
(List.map (fun (v,vt) -> v, Types.var vt) vars_mapping)
in in
let al = let nargs = List.map2 (fun (_, v) (_, vt) -> v, vt) vars_mapping sub_list
let a = Array.make (List.length pl) (Var.mk "dummy") in
List.iteri (fun i (_,v) -> a.(i) <- v) vars_mapping;
a
in in
(v',t_rhs,al) (v,t_rhs,nargs)
) (List.rev b) (List.rev b') ) (List.rev b)
in in
List.iter (fun (v,t,al) -> List.iter (fun (v,t,al) ->
Types.Print.register_global ("",v,Array.map Types.var al) t Types.Print.register_global ("",v, al) t
) b; ) b;
enter_types b env enter_types b env
......
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