From 43812b827ee7e7e6234ccb2a448a39d619f3b227 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Thu, 16 Feb 2023 15:18:39 +0900 Subject: remove reified_var_counter --- typing/ctype.ml | 38 ++++++++++++++++++++++---------------- typing/ctype.mli | 1 - typing/typetexp.ml | 1 - 3 files changed, 22 insertions(+), 18 deletions(-) diff --git a/typing/ctype.ml b/typing/ctype.ml index f92f1efd4b..6224ef50d8 100644 --- a/typing/ctype.ml +++ b/typing/ctype.ml @@ -307,6 +307,11 @@ let can_assume_injective () = | Expression | Subst -> false | Pattern { assume_injective } -> assume_injective +let in_counterexample () = + match !umode with + | Expression | Subst -> false + | Pattern { allow_recursive_equations } -> allow_recursive_equations + let allow_recursive_equations () = !Clflags.recursive_types || match !umode with @@ -1210,20 +1215,21 @@ let instance_list schl = For_copy.with_scope (fun copy_scope -> List.map (fun t -> copy copy_scope t) schl) -let reified_var_counter = ref Vars.empty -let reset_reified_var_counter () = - reified_var_counter := Vars.empty - -(* names given to new type constructors. - Used for existential types and - local constraints *) -let get_new_abstract_name s = - let index = - try Vars.find s !reified_var_counter + 1 - with Not_found -> 0 in - reified_var_counter := Vars.add s index !reified_var_counter; - if index = 0 && s <> "" && s.[String.length s - 1] <> '$' then s else - Printf.sprintf "%s%d" s index +(* Create unique names to new type constructors. + Used for existential types and local constraints. *) +let get_new_abstract_name env s = + (* unique names are needed only for error messages *) + if in_counterexample () then s else + let rec loop index = + let name = + if index = 0 && s <> "" && s.[String.length s - 1] <> '$' then s else + Printf.sprintf "%s%d" s index + in + match Env.find_type_by_name (Longident.Lident name) env with + | _ -> loop (index + 1) + | exception Not_found -> name + in + loop 0 let new_local_type ?(loc = Location.none) ?manifest_and_scope () = let manifest, expansion_scope = @@ -1267,7 +1273,7 @@ let instance_constructor existential_treatment cstr = let decl = new_local_type () in let name = existential_name cstr existential in let (id, new_env) = - Env.enter_type (get_new_abstract_name name) decl !env + Env.enter_type (get_new_abstract_name !env name) decl !env ~scope:fresh_constr_scope in env := new_env; let to_unify = newty (Tconstr (Path.Pident id,[],ref Mnil)) in @@ -2163,7 +2169,7 @@ let reify env t = let name = match name with Some s -> "$'"^s | _ -> "$" in let decl = new_local_type () in let (id, new_env) = - Env.enter_type (get_new_abstract_name name) decl !env + Env.enter_type (get_new_abstract_name !env name) decl !env ~scope:fresh_constr_scope in let path = Path.Pident id in let t = newty2 ~level:lev (Tconstr (path,[],ref Mnil)) in diff --git a/typing/ctype.mli b/typing/ctype.mli index 212e6ce4a7..d252f8a622 100644 --- a/typing/ctype.mli +++ b/typing/ctype.mli @@ -447,7 +447,6 @@ val collapse_conj_params: Env.t -> type_expr list -> unit val get_current_level: unit -> int val wrap_trace_gadt_instances: Env.t -> ('a -> 'b) -> 'a -> 'b -val reset_reified_var_counter: unit -> unit val immediacy : Env.t -> type_expr -> Type_immediacy.t diff --git a/typing/typetexp.ml b/typing/typetexp.ml index 3b7b06e52f..3316933700 100644 --- a/typing/typetexp.ml +++ b/typing/typetexp.ml @@ -152,7 +152,6 @@ end = struct let reset () = reset_global_level (); - Ctype.reset_reified_var_counter (); type_variables := TyVarMap.empty let is_in_scope name = -- cgit v1.2.1 From a600872c94879ed9ed7cdb5a1aa1591cf78a7163 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Wed, 15 Mar 2023 16:27:21 +0900 Subject: use Misc.find_first_mono --- typing/ctype.ml | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/typing/ctype.ml b/typing/ctype.ml index 6224ef50d8..bec19ae528 100644 --- a/typing/ctype.ml +++ b/typing/ctype.ml @@ -1220,16 +1220,17 @@ let instance_list schl = let get_new_abstract_name env s = (* unique names are needed only for error messages *) if in_counterexample () then s else - let rec loop index = - let name = - if index = 0 && s <> "" && s.[String.length s - 1] <> '$' then s else - Printf.sprintf "%s%d" s index - in - match Env.find_type_by_name (Longident.Lident name) env with - | _ -> loop (index + 1) - | exception Not_found -> name + let name index = + if index = 0 && s <> "" && s.[String.length s - 1] <> '$' then s else + Printf.sprintf "%s%d" s index + in + let check index = + match Env.find_type_by_name (Longident.Lident (name index)) env with + | _ -> false + | exception Not_found -> true in - loop 0 + let index = Misc.find_first_mono check in + name index let new_local_type ?(loc = Location.none) ?manifest_and_scope () = let manifest, expansion_scope = -- cgit v1.2.1 From ae10a642822dc83bdeee1e8aeddabad286498569 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Thu, 16 Feb 2023 15:21:36 +0900 Subject: changes --- Changes | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Changes b/Changes index eaa42f8ca0..aa47de2f94 100644 --- a/Changes +++ b/Changes @@ -566,6 +566,9 @@ Working version (Sébastien Hinderer, review by Xavier Leroy, Nicolás Ojeda Bär and Hugo Heuzard) +- #12011: remove Ctype.reified_var_counter + (Takafumi Saikawa and Jacques Garrigue, review by Gabriel Scherer) + - #12012: move calls to Typetexp.TyVarEnv.reset inside with_local_level etc. (Jacques Garrigue and Takafumi Saikawa, review by Gabriel Scherer) -- cgit v1.2.1