aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/eConstr.ml3
-rw-r--r--engine/eConstr.mli2
-rw-r--r--engine/evarutil.ml22
-rw-r--r--engine/evarutil.mli10
-rw-r--r--engine/evd.ml50
-rw-r--r--engine/evd.mli15
-rw-r--r--engine/uState.ml29
-rw-r--r--engine/uState.mli2
8 files changed, 81 insertions, 52 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 334c23c963..36297fe243 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -743,6 +743,9 @@ let match_named_context_val :
match unsafe_eq with
| Refl -> match_named_context_val
+let identity_subst_val : named_context_val -> t list =
+ match unsafe_eq with Refl -> fun ctx -> ctx.env_named_var
+
let fresh_global ?loc ?rigid ?names env sigma reference =
let (evd,t) = Evd.fresh_global ?loc ?rigid ?names env sigma reference in
evd, t
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index d0f675319d..a018f4064f 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -326,6 +326,8 @@ val map_rel_context_in_env :
val match_named_context_val :
named_context_val -> (named_declaration * lazy_val * named_context_val) option
+val identity_subst_val : named_context_val -> t list
+
(* XXX Missing Sigma proxy *)
val fresh_global :
?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env ->
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index b4b2032dd2..01c4e5fd72 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -386,14 +386,12 @@ let push_rel_decl_to_named_context
let push_rel_context_to_named_context ?hypnaming env sigma typ =
(* compute the instances relative to the named context and rel_context *)
- let open Context.Named.Declaration in
let open EConstr in
- let ids = List.map get_id (named_context env) in
- let inst_vars = List.map mkVar ids in
+ let inst_vars = EConstr.identity_subst_val (named_context_val env) in
if List.is_empty (Environ.rel_context env) then
(named_context_val env, typ, inst_vars, empty_csubst)
else
- let avoid = List.fold_right Id.Set.add ids Id.Set.empty in
+ let avoid = Environ.ids_of_named_context_val (named_context_val env) in
let inst_rels = List.rev (rel_list 0 (nb_rel env)) in
(* move the rel context to a named context and extend the named instance *)
(* with vars of the rel context *)
@@ -409,8 +407,9 @@ let push_rel_context_to_named_context ?hypnaming env sigma typ =
let default_source = Loc.tag @@ Evar_kinds.InternalHole
-let new_pure_evar ?(src=default_source) ?(filter = Filter.identity) ?(abstract_arguments = Abstraction.identity)
- ?candidates ?(naming = IntroAnonymous) ?typeclass_candidate ?(principal=false) sign evd typ =
+let new_pure_evar ?(src=default_source) ?(filter = Filter.identity) ?identity
+ ?(abstract_arguments = Abstraction.identity) ?candidates
+ ?(naming = IntroAnonymous) ?typeclass_candidate ?(principal=false) sign evd typ =
let name = match naming with
| IntroAnonymous -> None
| IntroIdentifier id -> Some id
@@ -419,6 +418,10 @@ let new_pure_evar ?(src=default_source) ?(filter = Filter.identity) ?(abstract_a
let id = Namegen.next_ident_away_from id has_name in
Some id
in
+ let identity = match identity with
+ | None -> Identity.none ()
+ | Some inst -> Identity.make inst
+ in
let evi = {
evar_hyps = sign;
evar_concl = typ;
@@ -426,7 +429,9 @@ let new_pure_evar ?(src=default_source) ?(filter = Filter.identity) ?(abstract_a
evar_filter = filter;
evar_abstract_arguments = abstract_arguments;
evar_source = src;
- evar_candidates = candidates }
+ evar_candidates = candidates;
+ evar_identity = identity;
+ }
in
let typeclass_candidate = if principal then Some false else typeclass_candidate in
let (evd, newevk) = Evd.new_evar evd ?name ?typeclass_candidate evi in
@@ -447,7 +452,8 @@ let new_evar ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_can
match filter with
| None -> instance
| Some filter -> Filter.filter_list filter instance in
- let (evd, evk) = new_pure_evar sign evd typ' ?src ?filter ?abstract_arguments ?candidates ?naming
+ let identity = if Int.equal (Environ.nb_rel env) 0 then Some instance else None in
+ let (evd, evk) = new_pure_evar sign evd typ' ?src ?filter ?identity ?abstract_arguments ?candidates ?naming
?typeclass_candidate ?principal in
(evd, EConstr.mkEvar (evk, instance))
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 41b58d38b0..a8fc9ef5e2 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -40,8 +40,18 @@ val new_evar :
?principal:bool -> ?hypnaming:naming_mode ->
env -> evar_map -> types -> evar_map * EConstr.t
+(** Low-level interface to create an evar.
+ @param src User-facing source for the evar
+ @param filter See {!Evd.Filter}, must be the same length as [named_context_val]
+ @param identity See {!Evd.Identity}, must be the name projection of [named_context_val]
+ @param naming A naming scheme for the evar
+ @param principal Whether the evar is the principal goal
+ @param named_context_val The context of the evar
+ @param types The type of conclusion of the evar
+*)
val new_pure_evar :
?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
+ ?identity:EConstr.t list ->
?abstract_arguments:Abstraction.t -> ?candidates:constr list ->
?naming:intro_pattern_naming_expr ->
?typeclass_candidate:bool ->
diff --git a/engine/evd.ml b/engine/evd.ml
index c570f75c6b..92657c41a9 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -139,6 +139,29 @@ module Abstraction = struct
let abstract_last l = Abstract :: l
end
+module Identity :
+sig
+ type t
+ val make : econstr list -> t
+ val none : unit -> t
+ val repr : named_context_val -> Filter.t -> t -> econstr list
+ val is_identity : econstr list -> t -> bool
+end =
+struct
+ type t = econstr list option ref
+ let make s = ref (Some s)
+ let none () = ref None
+ let repr sign filter s = match !s with
+ | None ->
+ let ans = Filter.filter_list filter sign.env_named_var in
+ let () = s := Some ans in
+ ans
+ | Some s -> s
+ let is_identity l s = match !s with
+ | None -> false
+ | Some s -> s == l
+end
+
(* The kinds of existential variables are now defined in [Evar_kinds] *)
(* The type of mappings for existential variables *)
@@ -158,7 +181,9 @@ type evar_info = {
evar_filter : Filter.t;
evar_abstract_arguments : Abstraction.t;
evar_source : Evar_kinds.t Loc.located;
- evar_candidates : constr list option; (* if not None, list of allowed instances *)}
+ evar_candidates : constr list option; (* if not None, list of allowed instances *)
+ evar_identity : Identity.t;
+}
let make_evar hyps ccl = {
evar_concl = ccl;
@@ -167,7 +192,9 @@ let make_evar hyps ccl = {
evar_filter = Filter.identity;
evar_abstract_arguments = Abstraction.identity;
evar_source = Loc.tag @@ Evar_kinds.InternalHole;
- evar_candidates = None; }
+ evar_candidates = None;
+ evar_identity = Identity.none ();
+}
let instance_mismatch () =
anomaly (Pp.str "Signature and its instance do not match.")
@@ -216,6 +243,9 @@ let evar_filtered_env env evi = match Filter.repr (evar_filter evi) with
in
make_env filter (evar_context evi)
+let evar_identity_subst evi =
+ Identity.repr evi.evar_hyps evi.evar_filter evi.evar_identity
+
let map_evar_body f = function
| Evar_empty -> Evar_empty
| Evar_defined d -> Evar_defined (f d)
@@ -256,7 +286,9 @@ let evar_instance_array test_id info args =
instrec filter (evar_context info) args
let make_evar_instance_array info args =
- evar_instance_array (NamedDecl.get_id %> isVarId) info args
+ if Identity.is_identity args info.evar_identity then []
+ else
+ evar_instance_array (NamedDecl.get_id %> isVarId) info args
let instantiate_evar_array info c args =
let inst = make_evar_instance_array info args in
@@ -779,16 +811,17 @@ let declare_restricted_evar evar_flags evk evk' =
let restrict evk filter ?candidates ?src evd =
let evk' = new_untyped_evar () in
let evar_info = EvMap.find evk evd.undf_evars in
+ let id_inst = Filter.filter_list filter evar_info.evar_hyps.env_named_var in
let evar_info' =
{ evar_info with evar_filter = filter;
evar_candidates = candidates;
- evar_source = (match src with None -> evar_info.evar_source | Some src -> src) } in
+ evar_source = (match src with None -> evar_info.evar_source | Some src -> src);
+ evar_identity = Identity.make id_inst;
+ } in
let last_mods = match evd.conv_pbs with
| [] -> evd.last_mods
| _ -> Evar.Set.add evk evd.last_mods in
let evar_names = EvNames.reassign_name_defined evk evk' evd.evar_names in
- let ctxt = Filter.filter_list filter (evar_context evar_info) in
- let id_inst = List.map (NamedDecl.get_id %> mkVar) ctxt in
let body = mkEvar(evk',id_inst) in
let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
let evar_flags = declare_restricted_evar evd.evar_flags evk evk' in
@@ -987,11 +1020,6 @@ let check_constraints evd csts =
let fix_undefined_variables evd =
{ evd with universes = UState.fix_undefined_variables evd.universes }
-let refresh_undefined_universes evd =
- let uctx', subst = UState.refresh_undefined_univ_variables evd.universes in
- let evd' = cmap (subst_univs_level_constr subst) {evd with universes = uctx'} in
- evd', subst
-
let nf_univ_variables evd =
let subst, uctx' = UState.normalize_variables evd.universes in
let evd' = {evd with universes = uctx'} in
diff --git a/engine/evd.mli b/engine/evd.mli
index 679173ca72..d338b06e0e 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -89,6 +89,15 @@ module Abstraction : sig
val abstract_last : t -> t
end
+module Identity :
+sig
+ type t
+ (** Identity substitutions *)
+
+ val make : econstr list -> t
+ val none : unit -> t
+end
+
(** {6 Evar infos} *)
type evar_body =
@@ -114,6 +123,9 @@ type evar_info = {
(** Information about the evar. *)
evar_candidates : econstr list option;
(** List of possible solutions when known that it is a finite list *)
+ evar_identity : Identity.t;
+ (** Default evar instance, i.e. a list of Var nodes projected from the
+ filtered environment. *)
}
val make_evar : named_context_val -> etypes -> evar_info
@@ -127,6 +139,7 @@ val evar_candidates : evar_info -> constr list option
val evar_filter : evar_info -> Filter.t
val evar_env : env -> evar_info -> env
val evar_filtered_env : env -> evar_info -> env
+val evar_identity_subst : evar_info -> econstr list
val map_evar_body : (econstr -> econstr) -> evar_body -> evar_body
val map_evar_info : (econstr -> econstr) -> evar_info -> evar_info
@@ -643,8 +656,6 @@ val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst
val fix_undefined_variables : evar_map -> evar_map
-val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_subst
-
(** Universe minimization *)
val minimize_universes : evar_map -> evar_map
diff --git a/engine/uState.ml b/engine/uState.ml
index d4cb59da26..ca0a21acf7 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -718,35 +718,6 @@ let fix_undefined_variables uctx =
{ uctx with univ_variables = vars';
univ_algebraic = algs' }
-let refresh_undefined_univ_variables uctx =
- let subst, ctx' = UnivGen.fresh_universe_context_set_instance uctx.local in
- let subst_fn u = subst_univs_level_level subst u in
- let alg = LSet.fold (fun u acc -> LSet.add (subst_fn u) acc)
- uctx.univ_algebraic LSet.empty
- in
- let vars =
- LMap.fold
- (fun u v acc ->
- LMap.add (subst_fn u)
- (Option.map (subst_univs_level_universe subst) v) acc)
- uctx.univ_variables LMap.empty
- in
- let weak = UPairSet.fold (fun (u,v) acc -> UPairSet.add (subst_fn u, subst_fn v) acc) uctx.weak_constraints UPairSet.empty in
- let lbound = uctx.universes_lbound in
- let declare g = LSet.fold (fun u g -> UGraph.add_universe u ~lbound ~strict:false g)
- (ContextSet.levels ctx') g in
- let initial = declare uctx.initial_universes in
- let univs = declare UGraph.initial_universes in
- let uctx' = {names = uctx.names;
- local = ctx';
- seff_univs = uctx.seff_univs;
- univ_variables = vars; univ_algebraic = alg;
- universes = univs;
- universes_lbound = lbound;
- initial_universes = initial;
- weak_constraints = weak; } in
- uctx', subst
-
let minimize uctx =
let open UnivMinim in
let lbound = uctx.universes_lbound in
diff --git a/engine/uState.mli b/engine/uState.mli
index 45a0f9964e..607c6c9452 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -154,8 +154,6 @@ val abstract_undefined_variables : t -> t
val fix_undefined_variables : t -> t
-val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst
-
(** Universe minimization *)
val minimize : t -> t
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 05:55:38 +0000