| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/pretyping/ (Beweissystem des Inria Version 9.1.0©) Datei vom 15.8.2025 mit Größe 7 kB |
|
Quelle evarsolve.mli Sprache: SML |
|||||||||
|
(************************************************************************)
(* * The Rocq Prover / The Rocq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) open EConstr open Evd open Environ type alias val of_alias : alias -> EConstr.t module AllowedEvars : sig type t (** Represents the set of evars that can be defined by the pretyper *) val all : t (** All evars can be defined *) val mem : t -> Evar.t -> bool (** [mem allowed evk] is true iff evk can be defined *) val from_pred : (Evar.t -> bool) -> t (** [from_pred p] means evars satisfying p can be defined *) val except : Evar.Set.t -> t (** [except evars] means all evars can be defined except the ones in [evars] *) val remove : Evar.t -> t -> t (** [remove evk allowed] removes [evk] from the set of evars allowed by [allowed] *) end type unify_flags = { modulo_betaiota : bool; (* Enable beta-iota reductions during unification *) open_ts : TransparentState.t; (* Enable delta reduction according to open_ts for open terms *) closed_ts : TransparentState.t; (* Enable delta reduction according to closed_ts for closed terms (when calling conversion) * subterm_ts : TransparentState.t; (* Enable delta reduction according to subterm_ts for selection of subterms during higher-or unifications. *) allowed_evars : AllowedEvars.t; (* Disallowed evars are treated like rigid variables during unification: they can not be insta with_cs : bool (* Enable canonical structure resolution during unification *) } type unification_result = | Success of evar_map | UnifFailure of evar_map * Pretype_errors.unification_error val is_success : unification_result -> bool val is_evar_allowed : unify_flags -> Evar.t -> bool (** Replace the vars and rels that are aliases to other vars and rels by their representative that is most ancient in the context *) val expand_vars_in_term : env -> evar_map -> constr -> constr (** One might want to use different conversion strategies for types and terms: e.g. preventing delta reductions when doing term unifications but allowing arbitrary delta conversion when checking the types of evar instances. *) type unification_kind = | TypeUnification | TermUnification (** A unification function parameterized by: - unification flags - the kind of unification - environment - sigma - conversion problem - the two terms to unify. *) type unifier = unify_flags -> unification_kind -> env -> evar_map -> conv_pb -> constr -> constr -> unification_result (** A conversion function: parameterized by the kind of unification, environment, sigma, conversion problem and the two terms to convert. Conversion is not allowed to instantiate evars contrary to unification. *) type conversion_check = unify_flags -> unification_kind -> env -> evar_map -> conv_pb -> constr -> constr -> bool (** [instantiate_evar unify flags env sigma ev c] defines the evar [ev] with [c], checking that the type of [c] is unifiable with [ev]'s declared type first. Preconditions: - [ev] does not occur in [c]. - [c] does not contain any Meta(_) If [ev] and [c] have non inferably convertible types, an exception [IllTypedInstance] is raised *) val instantiate_evar : unifier -> unify_flags -> env -> evar_map -> Evar.t -> constr -> evar_map (** [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]), possibly solving related unification problems, possibly leaving open some problems that cannot be solved in a unique way (except if choose is true); fails if the instance is not valid for the given [ev]; If [ev] and [c] have non inferably convertible types, an exception [IllTypedInstance] is raised *) val evar_define : unifier -> unify_flags -> ?choose:bool -> ?imitate_defs:bool -> env -> evar_map -> bool option -> existential -> constr -> evar_map val refresh_universes : ?status:Evd.rigid -> ?onlyalg:bool (* Only algebraic universes *) -> ?refreshset:bool -> (* Also refresh Prop and Set universes, so that the returned type can be any supertype of the original type *) bool option (* direction: true for levels lower than the existing levels *) -> env -> evar_map -> types -> evar_map * types val solve_refl : ?can_drop:bool -> conversion_check -> unify_flags -> env -> evar_map -> bool option -> Evar.t -> constr SList.t -> constr SList.t -> evar_map val solve_evar_evar : ?force:bool -> (env -> evar_map -> bool option -> existential -> constr -> evar_map) -> unifier -> unify_flags -> env -> evar_map -> bool option -> existential -> existential -> evar_map (** The two evars are expected to be in inferably convertible types; if not, an exception IllTypedInstance is raised *) (* [solve_simple_eqn unifier flags env evd (direction,?ev[inst],t)] makes progresses on problems of the form [?ev[inst] := t] (or [?ev[inst] :<= t], or [?ev[inst] :>= t]). It uses imitation and a limited form of projection. At the time of writing this comment, only rels/vars (possibly indirectly via a chain of evars) and constructors are used for projection. For instance [?e[x,S 0] := x + S 0] will be solved by imitating [+] and projecting [x] and [S 0] (so that [?e[a,b]:=a+b]) but in [?e[0+0] := 0+0], the possible imitation will not be seen. [choose] tells to make an irreversible choice when two valid projections are competing. It is to be used when no more reversible progress can be done. It is [false] by default. [imitate_defs] tells to expand local definitions if they cannot be projected. It is [true] by default. *) val solve_simple_eqn : unifier -> unify_flags -> ?choose:bool -> ?imitate_defs:bool -> env -> evar bool option * existential * constr -> unification_result val reconsider_unif_constraints : unifier -> unify_flags -> evar_map -> unification_result val is_unification_pattern_evar : env -> evar_map -> existential -> constr list -> constr -> alias list option val is_unification_pattern : env * int -> evar_map -> constr -> constr list -> constr -> alias list option val solve_pattern_eqn : env -> evar_map -> alias list -> constr -> constr val noccur_evar : env -> evar_map -> Evar.t -> constr -> bool exception IllTypedInstance of env * evar_map * types option * types val check_evar_instance : unifier -> unify_flags -> env -> evar_map -> Evar.t -> constr -> evar_map (** May raise IllTypedInstance if types are not convertible *) val remove_instance_local_defs : evar_map -> Evar.t -> 'a list -> 'a list val get_type_of_refresh : ?lax:bool -> env -> evar_map -> constr -> evar_map * types val checked_appvect_hook : (env -> evar_map -> constr -> constr array -> evar_map * constr) Hook.t ¤ Dauer der Verarbeitung: 0.23 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28