slight representation change

master
Thomas Refis 2018-02-12 16:37:35 +00:00
parent d43ccfc5d4
commit f509125318
16 changed files with 94 additions and 88 deletions

Binary file not shown.

Binary file not shown.

Binary file not shown.

View File

@ -683,15 +683,8 @@ let forward_try_expand_once = (* Forward declaration *)
module M = struct type t let _ = (x : t list ref) end
(without this constraint, the type system would actually be unsound.)
*)
let get_path_scope env p =
try
match (Env.find_type p env).type_newtype_level with
| None -> Path.binding_time p
| Some (x, _) -> x
with
| Not_found ->
(* no newtypes in predef *)
Path.binding_time p
let get_path_scope p =
Path.binding_time p
let rec normalize_package_path env p =
let t =
@ -730,7 +723,7 @@ let rec update_level env level expand ty =
| None -> ()
end;
match ty.desc with
Tconstr(p, _tl, _abbrev) when level < get_path_scope env p ->
Tconstr(p, _tl, _abbrev) when level < get_path_scope p ->
(* Try first to replace an abbreviation by its expansion. *)
begin try
(* if is_newtype env p then raise Cannot_expand; *)
@ -738,8 +731,8 @@ let rec update_level env level expand ty =
update_level env level expand ty
with Cannot_expand ->
(* +++ Levels should be restored... *)
(* Format.printf "update_level: %i < %i@." level (get_path_scope env p); *)
if level < get_path_scope env p then raise (Unify [(ty, newvar2 level)]);
(* Format.printf "update_level: %i < %i@." level (get_path_scope p); *)
if level < get_path_scope p then raise (Unify [(ty, newvar2 level)]);
iter_type_expr (update_level env level expand) ty
end
| Tconstr(_, _ :: _, _) when expand ->
@ -756,13 +749,13 @@ let rec update_level env level expand ty =
log_type ty; ty.desc <- Tpackage (p', nl, tl);
update_level env level expand ty
| Tobject(_, ({contents=Some(p, _tl)} as nm))
when level < get_path_scope env p ->
when level < get_path_scope p ->
set_name nm None;
update_level env level expand ty
| Tvariant row ->
let row = row_repr row in
begin match row.row_name with
| Some (p, _tl) when level < get_path_scope env p ->
| Some (p, _tl) when level < get_path_scope p ->
log_type ty;
ty.desc <- Tvariant {row with row_name = None}
| _ -> ()
@ -1118,7 +1111,7 @@ let get_new_abstract_name s =
if index = 0 && s <> "" && s.[String.length s - 1] <> '$' then s else
Printf.sprintf "%s%d" s index
let new_declaration newtype manifest =
let new_declaration expansion_scope manifest =
{
type_params = [];
type_arity = 0;
@ -1126,7 +1119,8 @@ let new_declaration newtype manifest =
type_private = Public;
type_manifest = manifest;
type_variance = [];
type_newtype_level = newtype;
type_is_newtype = true;
type_expansion_scope = expansion_scope;
type_loc = Location.none;
type_attributes = [];
type_immediate = false;
@ -1136,9 +1130,9 @@ let new_declaration newtype manifest =
let instance_constructor ?in_pattern cstr =
begin match in_pattern with
| None -> ()
| Some (env, newtype_lev) ->
| Some (env, expansion_scope) ->
let process existential =
let decl = new_declaration (Some (newtype_lev, newtype_lev)) None in
let decl = new_declaration (Some expansion_scope) None in
let name =
match repr existential with
{desc = Tvar (Some name)} -> "$" ^ cstr.cstr_name ^ "_'" ^ name
@ -1931,26 +1925,19 @@ let deep_occur t0 ty =
information is indeed lost, but it probably does not worth it.
*)
let newtype_level = ref None
let get_newtype_level () =
match !newtype_level with
| None -> assert false
| Some x -> x
(* a local constraint can be added only if the rhs
of the constraint does not contain any Tvars.
They need to be removed using this function *)
let reify env t =
let newtype_level = get_newtype_level () in
let create_fresh_constr lev name =
let decl = new_declaration (Some (newtype_level, newtype_level)) None in
let name = match name with Some s -> "$'"^s | _ -> "$" in
let path = Path.Pident (Ident.create (get_new_abstract_name name)) in
let binding_time = Ident.current_time () in
let decl = new_declaration (Some binding_time) None in
let new_env = Env.add_local_type path decl !env in
let t = newty2 lev (Tconstr (path,[],ref Mnil)) in
env := new_env;
t
t, binding_time
in
let visited = ref TypeSet.empty in
let rec iterator ty =
@ -1959,9 +1946,9 @@ let reify env t =
visited := TypeSet.add ty !visited;
match ty.desc with
Tvar o ->
let t = create_fresh_constr ty.level o in
let t, binding_time = create_fresh_constr ty.level o in
link_type ty t;
if ty.level < newtype_level then
if ty.level < binding_time then
raise (Unify [t, newvar2 ty.level])
| Tvariant r ->
let r = row_repr r in
@ -1970,11 +1957,11 @@ let reify env t =
let m = r.row_more in
match m.desc with
Tvar o ->
let t = create_fresh_constr m.level o in
let t, binding_time = create_fresh_constr m.level o in
let row =
{r with row_fields=[]; row_fixed=true; row_more = t} in
link_type m (newty2 m.level (Tvariant row));
if m.level < newtype_level then
if m.level < binding_time then
raise (Unify [t, newvar2 m.level])
| _ -> assert false
end;
@ -1990,14 +1977,14 @@ let reify env t =
let is_newtype env p =
try
let decl = Env.find_type p env in
decl.type_newtype_level <> None &&
decl.type_expansion_scope <> None &&
decl.type_kind = Type_abstract &&
decl.type_private = Public
with Not_found -> false
let non_aliasable p decl =
(* in_pervasives p || (subsumed by in_current_module) *)
in_current_module p && decl.type_newtype_level = None
in_current_module p && not decl.type_is_newtype
let is_instantiable env p =
try
@ -2240,20 +2227,25 @@ let find_lowest_level ty =
end
in find ty; unmark_type ty; !lowest
let find_expansion_level env path =
(* always guarded by a call to [is_newtype], so we *always* have a newtype
level. *)
match (Env.find_type path env).type_newtype_level with
| Some (_, x) -> x
let find_expansion_scope env path =
match (Env.find_type path env).type_expansion_scope with
| Some x -> x
| None -> assert false
let gadt_equations_level = ref None
let get_gadt_equations_level () =
match !gadt_equations_level with
| None -> assert false
| Some x -> x
let add_gadt_equation env source destination =
if local_non_recursive_abbrev !env source destination then begin
let destination = duplicate_type destination in
let source_lev = get_path_scope !env source in
let decl =
new_declaration (Some (source_lev, get_newtype_level ())) (Some destination)
let expansion_scope =
max (Path.binding_time source) (get_gadt_equations_level ())
in
let decl = new_declaration (Some expansion_scope) (Some destination) in
env := Env.add_local_type source decl !env;
cleanup_abbrev ()
end
@ -2400,7 +2392,7 @@ let rec unify (env:Env.t ref) t1 t2 =
&& is_newtype !env p1 && is_newtype !env p2 ->
(* Do not use local constraints more than necessary *)
begin try
if find_expansion_level !env p1 > find_expansion_level !env p2 then
if find_expansion_scope !env p1 > find_expansion_scope !env p2 then
unify env t1 (try_expand_once !env t2)
else
unify env (try_expand_once !env t1) t2
@ -2520,7 +2512,7 @@ and unify3 env t1 t1' t2 t2' =
when is_instantiable !env path && is_instantiable !env path'
&& !generate_equations ->
let source, destination =
if get_path_scope !env path > get_path_scope !env path'
if get_path_scope path > get_path_scope path'
then path , t2'
else path', t1'
in
@ -2848,16 +2840,16 @@ let unify env ty1 ty2 =
undo_compress snap;
raise (Unification_recursive_abbrev (expand_trace !env [(ty1,ty2)]))
let unify_gadt ~newtype_level:lev (env:Env.t ref) ty1 ty2 =
let unify_gadt ~equations_level:lev (env:Env.t ref) ty1 ty2 =
try
univar_pairs := [];
newtype_level := Some lev;
gadt_equations_level := Some lev;
set_mode_pattern ~generate:true ~injective:true
(fun () -> unify env ty1 ty2);
newtype_level := None;
gadt_equations_level := None;
TypePairs.clear unify_eq_set;
with e ->
newtype_level := None;
gadt_equations_level := None;
TypePairs.clear unify_eq_set;
raise e
@ -4471,7 +4463,8 @@ let nondep_type_decl env mid id is_covariant decl =
type_manifest = tm;
type_private = priv;
type_variance = decl.type_variance;
type_newtype_level = None;
type_is_newtype = false;
type_expansion_scope = None;
type_loc = decl.type_loc;
type_attributes = decl.type_attributes;
type_immediate = decl.type_immediate;

View File

@ -164,7 +164,7 @@ val enforce_constraints: Env.t -> type_expr -> unit
val unify: Env.t -> type_expr -> type_expr -> unit
(* Unify the two types given. Raise [Unify] if not possible. *)
val unify_gadt: newtype_level:int -> Env.t ref -> type_expr -> type_expr -> unit
val unify_gadt: equations_level:int -> Env.t ref -> type_expr -> type_expr -> unit
(* Unify the two types given and update the environment with the
local constraints. Raise [Unify] if not possible. *)
val unify_var: Env.t -> type_expr -> type_expr -> unit

View File

@ -85,7 +85,8 @@ let constructor_args priv cd_args cd_res path rep =
type_private = priv;
type_manifest = None;
type_variance = List.map (fun _ -> Variance.full) type_params;
type_newtype_level = None;
type_is_newtype = false;
type_expansion_scope = None;
type_loc = Location.none;
type_attributes = [];
type_immediate = false;

View File

@ -1056,7 +1056,7 @@ let find_type_expansion path env =
| Some body when decl.type_private = Public
|| decl.type_kind <> Type_abstract
|| Btype.has_constr_row body ->
(decl.type_params, body, may_map snd decl.type_newtype_level)
(decl.type_params, body, decl.type_expansion_scope)
(* The manifest type of Private abstract data types without
private row are still considered unknown to the type system.
Hence, this case is caught by the following clause that also handles
@ -1072,7 +1072,8 @@ let find_type_expansion_opt path env =
match decl.type_manifest with
(* The manifest type of Private abstract data types can still get
an approximation using their manifest type. *)
| Some body -> (decl.type_params, body, may_map snd decl.type_newtype_level)
| Some body ->
(decl.type_params, body, decl.type_expansion_scope)
| _ -> raise Not_found
let find_modtype_expansion path env =

View File

@ -125,7 +125,8 @@ let decl_abstr =
type_private = Asttypes.Public;
type_manifest = None;
type_variance = [];
type_newtype_level = None;
type_is_newtype = false;
type_expansion_scope = None;
type_attributes = [];
type_immediate = false;
type_unboxed = unboxed_false_default_false;

View File

@ -1283,7 +1283,8 @@ let filter_rem_sig item rem =
let dummy =
{ type_params = []; type_arity = 0; type_kind = Type_abstract;
type_private = Public; type_manifest = None; type_variance = [];
type_newtype_level = None; type_loc = Location.none;
type_is_newtype = false; type_expansion_scope = None;
type_loc = Location.none;
type_attributes = [];
type_immediate = false;
type_unboxed = unboxed_false_default_false;

View File

@ -299,7 +299,8 @@ let type_declaration s decl =
end;
type_private = decl.type_private;
type_variance = decl.type_variance;
type_newtype_level = None;
type_is_newtype = false;
type_expansion_scope = None;
type_loc = loc s decl.type_loc;
type_attributes = attrs s decl.type_attributes;
type_immediate = decl.type_immediate;

View File

@ -1282,7 +1282,8 @@ let temp_abbrev loc env id arity =
type_private = Public;
type_manifest = Some ty;
type_variance = Misc.replicate_list Variance.full arity;
type_newtype_level = None;
type_is_newtype = false;
type_expansion_scope = None;
type_loc = loc;
type_attributes = []; (* or keep attrs from the class decl? *)
type_immediate = false;
@ -1530,7 +1531,8 @@ let class_infos define_class kind
type_private = Public;
type_manifest = Some obj_ty;
type_variance = List.map (fun _ -> Variance.full) obj_params;
type_newtype_level = None;
type_is_newtype = false;
type_expansion_scope = None;
type_loc = cl.pci_loc;
type_attributes = []; (* or keep attrs from cl? *)
type_immediate = false;
@ -1549,7 +1551,8 @@ let class_infos define_class kind
type_private = Public;
type_manifest = Some cl_ty;
type_variance = List.map (fun _ -> Variance.full) cl_params;
type_newtype_level = None;
type_is_newtype = false;
type_expansion_scope = None;
type_loc = cl.pci_loc;
type_attributes = []; (* or keep attrs from cl? *)
type_immediate = false;

View File

@ -406,22 +406,16 @@ let unify_exp_types loc env ty expected_ty =
raise(Typetexp.Error(loc, env, Typetexp.Variant_tags (l1, l2)))
(* level at which to create the local type declarations *)
let newtype_level = ref None
let get_newtype_level () =
match !newtype_level with
let gadt_equations_level = ref None
let get_gadt_equations_level () =
match !gadt_equations_level with
Some y -> y
| None -> assert false
let unify_pat_types_gadt loc env ty ty' =
let newtype_level =
match !newtype_level with
| None -> assert false
| Some x -> x
in
try
unify_gadt ~newtype_level env ty ty'
try unify_gadt ~equations_level:(get_gadt_equations_level ()) env ty ty'
with
Unify trace ->
| Unify trace ->
raise(Error(loc, !env, Pattern_type_clash(trace)))
| Tags(l1,l2) ->
raise(Typetexp.Error(loc, !env, Typetexp.Variant_tags (l1, l2)))
@ -1210,7 +1204,8 @@ and type_pat_aux ~constrs ~labels ~no_existentials ~mode ~explode ~env
raise(Error(loc, !env, Constructor_arity_mismatch(lid.txt,
constr.cstr_arity, List.length sargs)));
let (ty_args, ty_res) =
instance_constructor ~in_pattern:(env, get_newtype_level ()) constr
instance_constructor ~in_pattern:(env, get_gadt_equations_level ())
constr
in
(* PR#7214: do not use gadt unification for toplevel lets *)
if not constr.cstr_generalized || mode = Inside_or || no_existentials
@ -1434,16 +1429,16 @@ and type_pat_aux ~constrs ~labels ~no_existentials ~mode ~explode ~env
let type_pat ?(allow_existentials=false) ?constrs ?labels ?(mode=Normal)
?(explode=0) ?(lev=get_current_level()) env sp expected_ty =
newtype_level := Some lev;
gadt_equations_level := Some lev;
try
let r =
type_pat ~no_existentials:(not allow_existentials) ~constrs ~labels
~mode ~explode ~env sp expected_ty (fun x -> x) in
iter_pattern (fun p -> p.pat_env <- !env) r;
newtype_level := None;
gadt_equations_level := None;
r
with e ->
newtype_level := None;
gadt_equations_level := None;
raise e
@ -3658,7 +3653,6 @@ and type_expect_
(* remember original level *)
begin_def ();
(* Create a fake abstract type declaration for name. *)
let level = get_current_level () in
let decl = {
type_params = [];
type_arity = 0;
@ -3666,7 +3660,8 @@ and type_expect_
type_private = Public;
type_manifest = None;
type_variance = [];
type_newtype_level = Some (level, level);
type_is_newtype = true;
type_expansion_scope = None;
type_loc = loc;
type_attributes = [];
type_immediate = false;
@ -4573,7 +4568,7 @@ and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
begin_def ();
Ident.set_current_time (get_current_level ());
let lev = Ident.current_time () in
Ctype.init_def (lev+1000); (* up to 1000 existentials *)
Ctype.init_def (lev+100000); (* up to 1000 existentials *)
lev
in
let lev =
@ -4703,16 +4698,20 @@ and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
else
Partial
in
let unused_check () =
let unused_check do_init =
let lev =
if do_init then init_env () else get_current_level ()
in
List.iter (fun (pat, _, (env, _)) -> check_absent_variant env pat)
pat_env_list;
check_unused ~lev env (instance ty_arg_check) cases ;
if do_init then end_def ();
Parmatch.check_ambiguous_bindings cases
in
if contains_polyvars || do_init then
add_delayed_check unused_check
add_delayed_check (fun () -> unused_check do_init)
else
unused_check ();
unused_check false;
(* Check for unused cases, do not delay because of gadts *)
if do_init then begin
end_def ();

View File

@ -104,7 +104,8 @@ let enter_type rec_flag env sdecl id =
begin match sdecl.ptype_manifest with None -> None
| Some _ -> Some(Ctype.newvar ()) end;
type_variance = List.map (fun _ -> Variance.full) sdecl.ptype_params;
type_newtype_level = None;
type_is_newtype = false;
type_expansion_scope = None;
type_loc = sdecl.ptype_loc;
type_attributes = sdecl.ptype_attributes;
type_immediate = false;
@ -518,7 +519,8 @@ let transl_declaration env sdecl id =
type_private = sdecl.ptype_private;
type_manifest = man;
type_variance = List.map (fun _ -> Variance.full) params;
type_newtype_level = None;
type_is_newtype = false;
type_expansion_scope = None;
type_loc = sdecl.ptype_loc;
type_attributes = sdecl.ptype_attributes;
type_immediate = false;
@ -1848,7 +1850,8 @@ let transl_with_constraint env id row_path orig_decl sdecl =
type_private = priv;
type_manifest = man;
type_variance = [];
type_newtype_level = None;
type_is_newtype = false;
type_expansion_scope = None;
type_loc = sdecl.ptype_loc;
type_attributes = sdecl.ptype_attributes;
type_immediate = false;
@ -1896,7 +1899,8 @@ let abstract_type_decl arity =
type_private = Public;
type_manifest = None;
type_variance = replicate_list Variance.full arity;
type_newtype_level = None;
type_is_newtype = false;
type_expansion_scope = None;
type_loc = Location.none;
type_attributes = [];
type_immediate = false;

View File

@ -359,7 +359,8 @@ let merge_constraint initial_env loc sg constr =
)
sdecl.ptype_params;
type_loc = sdecl.ptype_loc;
type_newtype_level = None;
type_is_newtype = false;
type_expansion_scope = None;
type_attributes = [];
type_immediate = false;
type_unboxed = unboxed_false_default_false;

View File

@ -150,7 +150,8 @@ type type_declaration =
type_private: private_flag;
type_manifest: type_expr option;
type_variance: Variance.t list;
type_newtype_level: (int * int) option;
type_is_newtype: bool;
type_expansion_scope: int option;
type_loc: Location.t;
type_attributes: Parsetree.attributes;
type_immediate: bool;

View File

@ -295,8 +295,8 @@ type type_declaration =
type_manifest: type_expr option;
type_variance: Variance.t list;
(* covariant, contravariant, weakly contravariant, injective *)
type_newtype_level: (int * int) option;
(* definition level * expansion level *)
type_is_newtype: bool;
type_expansion_scope: int option;
type_loc: Location.t;
type_attributes: Parsetree.attributes;
type_immediate: bool; (* true iff type should not be a pointer *)