diff options
Diffstat (limited to 'pretyping/evd.mli')
| -rw-r--r-- | pretyping/evd.mli | 621 |
1 files changed, 0 insertions, 621 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli deleted file mode 100644 index 0b4f1853..00000000 --- a/pretyping/evd.mli +++ /dev/null @@ -1,621 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Util -open Loc -open Names -open Term -open Context -open Environ - -(** {5 Existential variables and unification states} - - A unification state (of type [evar_map]) is primarily a finite mapping - from existential variables to records containing the type of the evar - ([evar_concl]), the context under which it was introduced ([evar_hyps]) - and its definition ([evar_body]). [evar_extra] is used to add any other - kind of information. - - It also contains conversion constraints, debugging information and - information about meta variables. *) - -(** {6 Evars} *) - -type evar = existential_key -(** Existential variables. TODO: Should be made opaque one day. *) - -val string_of_existential : evar -> string - -(** {6 Evar filters} *) - -module Filter : -sig - type t - (** Evar filters, seen as bitmasks. *) - - val equal : t -> t -> bool - (** Equality over filters *) - - val identity : t - (** The identity filter. *) - - val filter_list : t -> 'a list -> 'a list - (** Filter a list. Sizes must coincide. *) - - val filter_array : t -> 'a array -> 'a array - (** Filter an array. Sizes must coincide. *) - - val extend : int -> t -> t - (** [extend n f] extends [f] on the left with [n]-th times [true]. *) - - val compose : t -> t -> t - (** Horizontal composition : [compose f1 f2] only keeps parts of [f2] where - [f1] is set. In particular, [f1] and [f2] must have the same length. *) - - val apply_subfilter : t -> bool list -> t - (** [apply_subfilter f1 f2] applies filter [f2] where [f1] is [true]. In - particular, the length of [f2] is the number of times [f1] is [true] *) - - val restrict_upon : t -> int -> (int -> bool) -> t option - (** Ad-hoc primitive. *) - - val map_along : (bool -> 'a -> bool) -> t -> 'a list -> t - (** Apply the function on the filter and the list. Sizes must coincide. *) - - val make : bool list -> t - (** Create out of a list *) - - val repr : t -> bool list option - (** Observe as a bool list. *) - -end - -(** {6 Evar infos} *) - -type evar_body = - | Evar_empty - | Evar_defined of constr - - -module Store : Store.S -(** Datatype used to store additional information in evar maps. *) - -type evar_info = { - evar_concl : constr; - (** Type of the evar. *) - evar_hyps : named_context_val; - (** Context of the evar. *) - evar_body : evar_body; - (** Optional content of the evar. *) - evar_filter : Filter.t; - (** Boolean mask over {!evar_hyps}. Should have the same length. - TODO: document me more. *) - evar_source : Evar_kinds.t located; - (** Information about the evar. *) - evar_candidates : constr list option; - (** TODO: document this *) - evar_extra : Store.t - (** Extra store, used for clever hacks. *) -} - -val make_evar : named_context_val -> types -> evar_info -val evar_concl : evar_info -> constr -val evar_context : evar_info -> named_context -val evar_filtered_context : evar_info -> named_context -val evar_hyps : evar_info -> named_context_val -val evar_filtered_hyps : evar_info -> named_context_val -val evar_body : evar_info -> evar_body -val evar_filter : evar_info -> Filter.t -val evar_env : evar_info -> env -val evar_filtered_env : evar_info -> env - -val map_evar_body : (constr -> constr) -> evar_body -> evar_body -val map_evar_info : (constr -> constr) -> evar_info -> evar_info - -(** {6 Unification state} **) - -type evar_universe_context -(** The universe context associated to an evar map *) - -type evar_map -(** Type of unification state. Essentially a bunch of state-passing data needed - to handle incremental term construction. *) - -val empty : evar_map -(** The empty evar map. *) - -val from_env : env -> evar_map -(** The empty evar map with given universe context, taking its initial - universes from env. *) - -val from_ctx : evar_universe_context -> evar_map -(** The empty evar map with given universe context *) - -val is_empty : evar_map -> bool -(** Whether an evarmap is empty. *) - -val has_undefined : evar_map -> bool -(** [has_undefined sigma] is [true] if and only if - there are uninstantiated evars in [sigma]. *) - -val add : evar_map -> evar -> evar_info -> evar_map -(** [add sigma ev info] adds [ev] with evar info [info] in sigma. - Precondition: ev must not preexist in [sigma]. *) - -val find : evar_map -> evar -> evar_info -(** Recover the data associated to an evar. *) - -val find_undefined : evar_map -> evar -> evar_info -(** Same as {!find} but restricted to undefined evars. For efficiency - reasons. *) - -val remove : evar_map -> evar -> evar_map -(** Remove an evar from an evar map. Use with caution. *) - -val mem : evar_map -> evar -> bool -(** Whether an evar is present in an evarmap. *) - -val fold : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a -(** Apply a function to all evars and their associated info in an evarmap. *) - -val fold_undefined : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a -(** Same as {!fold}, but restricted to undefined evars. For efficiency - reasons. *) - -val raw_map : (evar -> evar_info -> evar_info) -> evar_map -> evar_map -(** Apply the given function to all evars in the map. Beware: this function - expects the argument function to preserve the kind of [evar_body], i.e. it - must send [Evar_empty] to [Evar_empty] and [Evar_defined c] to some - [Evar_defined c']. *) - -val raw_map_undefined : (evar -> evar_info -> evar_info) -> evar_map -> evar_map -(** Same as {!raw_map}, but restricted to undefined evars. For efficiency - reasons. *) - -val define : evar -> constr -> evar_map -> evar_map -(** Set the body of an evar to the given constr. It is expected that: - {ul - {- The evar is already present in the evarmap.} - {- The evar is not defined in the evarmap yet.} - {- All the evars present in the constr should be present in the evar map.} - } *) - -val cmap : (constr -> constr) -> evar_map -> evar_map -(** Map the function on all terms in the evar map. *) - -val is_evar : evar_map -> evar -> bool -(** Alias for {!mem}. *) - -val is_defined : evar_map -> evar -> bool -(** Whether an evar is defined in an evarmap. *) - -val is_undefined : evar_map -> evar -> bool -(** Whether an evar is not defined in an evarmap. *) - -val add_constraints : evar_map -> Univ.constraints -> evar_map -(** Add universe constraints in an evar map. *) - -val undefined_map : evar_map -> evar_info Evar.Map.t -(** Access the undefined evar mapping directly. *) - -val drop_all_defined : evar_map -> evar_map - -(** {6 Instantiating partial terms} *) - -exception NotInstantiatedEvar - -val existential_value : evar_map -> existential -> constr -(** [existential_value sigma ev] raises [NotInstantiatedEvar] if [ev] has - no body and [Not_found] if it does not exist in [sigma] *) - -val existential_type : evar_map -> existential -> types - -val existential_opt_value : evar_map -> existential -> constr option -(** Same as {!existential_value} but returns an option instead of raising an - exception. *) - -val evar_instance_array : (named_declaration -> 'a -> bool) -> evar_info -> - 'a array -> (Id.t * 'a) list - -val instantiate_evar_array : evar_info -> constr -> constr array -> constr - -val evars_reset_evd : ?with_conv_pbs:bool -> ?with_univs:bool -> - evar_map -> evar_map -> evar_map -(** spiwack: this function seems to somewhat break the abstraction. *) - -(** {6 Misc} *) - -val evar_declare : - named_context_val -> evar -> types -> ?src:Loc.t * Evar_kinds.t -> - ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> evar_map -> evar_map -(** Convenience function. Just a wrapper around {!add}. *) - -val restrict : evar -> evar -> Filter.t -> ?candidates:constr list -> - evar_map -> evar_map -(** Restrict an undefined evar into a new evar by filtering context and - possibly limiting the instances to a set of candidates *) - -val downcast : evar -> types -> evar_map -> evar_map -(** Change the type of an undefined evar to a new type assumed to be a - subtype of its current type; subtyping must be ensured by caller *) - -val evar_source : existential_key -> evar_map -> Evar_kinds.t located -(** Convenience function. Wrapper around {!find} to recover the source of an - evar in a given evar map. *) - -val evar_ident : existential_key -> evar_map -> Id.t - -val rename : existential_key -> Id.t -> evar_map -> evar_map - -val evar_key : Id.t -> evar_map -> existential_key - -val evar_source_of_meta : metavariable -> evar_map -> Evar_kinds.t located - -val dependent_evar_ident : existential_key -> evar_map -> Id.t - -(** {5 Side-effects} *) - -val emit_side_effects : Safe_typing.private_constants -> evar_map -> evar_map -(** Push a side-effect into the evar map. *) - -val eval_side_effects : evar_map -> Safe_typing.private_constants -(** Return the effects contained in the evar map. *) - -val drop_side_effects : evar_map -> evar_map -(** This should not be used. For hacking purposes. *) - -(** {5 Future goals} *) - -val declare_future_goal : Evar.t -> evar_map -> evar_map -(** Adds an existential variable to the list of future goals. For - internal uses only. *) - -val declare_principal_goal : Evar.t -> evar_map -> evar_map -(** Adds an existential variable to the list of future goals and make - it principal. Only one existential variable can be made principal, an - error is raised otherwise. For internal uses only. *) - -val future_goals : evar_map -> Evar.t list -(** Retrieves the list of future goals. Used by the [refine] primitive - of the tactic engine. *) - -val principal_future_goal : evar_map -> Evar.t option -(** Retrieves the name of the principal existential variable if there - is one. Used by the [refine] primitive of the tactic engine. *) - -val reset_future_goals : evar_map -> evar_map -(** Clears the list of future goals (as well as the principal future - goal). Used by the [refine] primitive of the tactic engine. *) - -val restore_future_goals : evar_map -> Evar.t list -> Evar.t option -> evar_map -(** Sets the future goals (including the principal future goal) to a - previous value. Intended to be used after a local list of future - goals has been consumed. Used by the [refine] primitive of the - tactic engine. *) - -(** {5 Sort variables} - - Evar maps also keep track of the universe constraints defined at a given - point. This section defines the relevant manipulation functions. *) - -val whd_sort_variable : evar_map -> constr -> constr - -exception UniversesDiffer - -val add_universe_constraints : evar_map -> Universes.universe_constraints -> evar_map -(** Add the given universe unification constraints to the evar map. - @raises UniversesDiffer in case a first-order unification fails. - @raises UniverseInconsistency -*) - -(** {5 Extra data} - - Evar maps can contain arbitrary data, allowing to use an extensible state. - As evar maps are theoretically used in a strict state-passing style, such - additional data should be passed along transparently. Some old and bug-prone - code tends to drop them nonetheless, so you should keep cautious. - -*) - -val get_extra_data : evar_map -> Store.t -val set_extra_data : Store.t -> evar_map -> evar_map - -(** {5 Enriching with evar maps} *) - -type 'a sigma = { - it : 'a ; - (** The base object. *) - sigma : evar_map - (** The added unification state. *) -} -(** The type constructor ['a sigma] adds an evar map to an object of type - ['a]. *) - -val sig_it : 'a sigma -> 'a -val sig_sig : 'a sigma -> evar_map -val on_sig : 'a sigma -> (evar_map -> evar_map * 'b) -> 'a sigma * 'b - -(** {5 The state monad with state an evar map} *) - -module MonadR : Monad.S with type +'a t = evar_map -> evar_map * 'a -module Monad : Monad.S with type +'a t = evar_map -> 'a * evar_map - - -(** {5 Meta machinery} - - These functions are almost deprecated. They were used before the - introduction of the full-fledged evar calculus. In an ideal world, they - should be removed. Alas, some parts of the code still use them. Do not use - in newly-written code. *) - -module Metaset : Set.S with type elt = metavariable -module Metamap : Map.ExtS with type key = metavariable and module Set := Metaset - -type 'a freelisted = { - rebus : 'a; - freemetas : Metaset.t } - -val metavars_of : constr -> Metaset.t -val mk_freelisted : constr -> constr freelisted -val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted - -(** Status of an instance found by unification wrt to the meta it solves: - - a supertype of the meta (e.g. the solution to ?X <= T is a supertype of ?X) - - a subtype of the meta (e.g. the solution to T <= ?X is a supertype of ?X) - - a term that can be eta-expanded n times while still being a solution - (e.g. the solution [P] to [?X u v = P u v] can be eta-expanded twice) -*) - -type instance_constraint = IsSuperType | IsSubType | Conv - -val eq_instance_constraint : - instance_constraint -> instance_constraint -> bool - -(** Status of the unification of the type of an instance against the type of - the meta it instantiates: - - CoerceToType means that the unification of types has not been done - and that a coercion can still be inserted: the meta should not be - substituted freely (this happens for instance given via the - "with" binding clause). - - TypeProcessed means that the information obtainable from the - unification of types has been extracted. - - TypeNotProcessed means that the unification of types has not been - done but it is known that no coercion may be inserted: the meta - can be substituted freely. -*) - -type instance_typing_status = - CoerceToType | TypeNotProcessed | TypeProcessed - -(** Status of an instance together with the status of its type unification *) - -type instance_status = instance_constraint * instance_typing_status - -(** Clausal environments *) - -type clbinding = - | Cltyp of Name.t * constr freelisted - | Clval of Name.t * (constr freelisted * instance_status) * constr freelisted - -(** Unification constraints *) -type conv_pb = Reduction.conv_pb -type evar_constraint = conv_pb * env * constr * constr -val add_conv_pb : ?tail:bool -> evar_constraint -> evar_map -> evar_map - -val extract_changed_conv_pbs : evar_map -> - (Evar.Set.t -> evar_constraint -> bool) -> - evar_map * evar_constraint list -val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list -val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t - -(** The following functions return the set of evars immediately - contained in the object; need the term to be evar-normal otherwise - defined evars are returned too. *) - -val evar_list : constr -> existential list - (** excluding evars in instances of evars and collected with - redundancies from right to left (used by tactic "instantiate") *) - -val evars_of_term : constr -> Evar.Set.t - (** including evars in instances of evars *) - -val evars_of_named_context : named_context -> Evar.Set.t - -val evars_of_filtered_evar_info : evar_info -> Evar.Set.t - -(** Metas *) -val meta_list : evar_map -> (metavariable * clbinding) list -val meta_defined : evar_map -> metavariable -> bool - -val meta_value : evar_map -> metavariable -> constr -(** [meta_fvalue] raises [Not_found] if meta not in map or [Anomaly] if - meta has no value *) - -val meta_fvalue : evar_map -> metavariable -> constr freelisted * instance_status -val meta_opt_fvalue : evar_map -> metavariable -> (constr freelisted * instance_status) option -val meta_type : evar_map -> metavariable -> types -val meta_ftype : evar_map -> metavariable -> types freelisted -val meta_name : evar_map -> metavariable -> Name.t -val meta_with_name : evar_map -> Id.t -> metavariable -val meta_declare : - metavariable -> types -> ?name:Name.t -> evar_map -> evar_map -val meta_assign : metavariable -> constr * instance_status -> evar_map -> evar_map -val meta_reassign : metavariable -> constr * instance_status -> evar_map -> evar_map - -val clear_metas : evar_map -> evar_map - -(** [meta_merge evd1 evd2] returns [evd2] extended with the metas of [evd1] *) -val meta_merge : ?with_univs:bool -> evar_map -> evar_map -> evar_map - -val undefined_metas : evar_map -> metavariable list -val map_metas_fvalue : (constr -> constr) -> evar_map -> evar_map - -type metabinding = metavariable * constr * instance_status - -val retract_coercible_metas : evar_map -> metabinding list * evar_map -val subst_defined_metas_evars : metabinding list * ('a * existential * constr) list -> constr -> constr option - -(** {5 FIXME: Nothing to do here} *) - -(********************************************************* - Sort/universe variables *) - -(** Rigid or flexible universe variables *) - -type rigid = - | UnivRigid - | UnivFlexible of bool (** Is substitution by an algebraic ok? *) - -val univ_rigid : rigid -val univ_flexible : rigid -val univ_flexible_alg : rigid - -type 'a in_evar_universe_context = 'a * evar_universe_context - -val evar_universe_context_set : Univ.universe_context -> evar_universe_context -> Univ.universe_context_set -val evar_universe_context_constraints : evar_universe_context -> Univ.constraints -val evar_context_universe_context : evar_universe_context -> Univ.universe_context -val evar_universe_context_of : Univ.universe_context_set -> evar_universe_context -val empty_evar_universe_context : evar_universe_context -val union_evar_universe_context : evar_universe_context -> evar_universe_context -> - evar_universe_context -val evar_universe_context_subst : evar_universe_context -> Universes.universe_opt_subst - -val evar_universe_context_of_binders : - Universes.universe_binders -> evar_universe_context - -val make_evar_universe_context : env -> (Id.t located) list option -> evar_universe_context -val restrict_universe_context : evar_map -> Univ.universe_set -> evar_map -(** Raises Not_found if not a name for a universe in this map. *) -val universe_of_name : evar_map -> string -> Univ.universe_level -val add_universe_name : evar_map -> string -> Univ.universe_level -> evar_map - -val universes : evar_map -> Univ.universes - -val add_constraints_context : evar_universe_context -> - Univ.constraints -> evar_universe_context - - -val normalize_evar_universe_context_variables : evar_universe_context -> - Univ.universe_subst in_evar_universe_context - -val normalize_evar_universe_context : evar_universe_context -> - evar_universe_context - -val new_univ_level_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe_level -val new_univ_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe -val new_sort_variable : ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * sorts -val add_global_univ : evar_map -> Univ.Level.t -> evar_map - -val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map -val is_sort_variable : evar_map -> sorts -> Univ.universe_level option -(** [is_sort_variable evm s] returns [Some u] or [None] if [s] is - not a local sort variable declared in [evm] *) -val is_flexible_level : evar_map -> Univ.Level.t -> bool - -val whd_sort_variable : evar_map -> constr -> constr -(* val normalize_universe_level : evar_map -> Univ.universe_level -> Univ.universe_level *) -val normalize_universe : evar_map -> Univ.universe -> Univ.universe -val normalize_universe_instance : evar_map -> Univ.universe_instance -> Univ.universe_instance - -val set_leq_sort : env -> evar_map -> sorts -> sorts -> evar_map -val set_eq_sort : env -> evar_map -> sorts -> sorts -> evar_map -val has_lub : evar_map -> Univ.universe -> Univ.universe -> evar_map -val set_eq_level : evar_map -> Univ.universe_level -> Univ.universe_level -> evar_map -val set_leq_level : evar_map -> Univ.universe_level -> Univ.universe_level -> evar_map -val set_eq_instances : ?flex:bool -> - evar_map -> Univ.universe_instance -> Univ.universe_instance -> evar_map - -val check_eq : evar_map -> Univ.universe -> Univ.universe -> bool -val check_leq : evar_map -> Univ.universe -> Univ.universe -> bool - -val evar_universe_context : evar_map -> evar_universe_context -val universe_context_set : evar_map -> Univ.universe_context_set -val universe_context : ?names:(Id.t located) list -> evar_map -> - (Id.t * Univ.Level.t) list * Univ.universe_context -val universe_subst : evar_map -> Universes.universe_opt_subst -val universes : evar_map -> Univ.universes - - -val merge_universe_context : evar_map -> evar_universe_context -> evar_map -val set_universe_context : evar_map -> evar_universe_context -> evar_map - -val merge_context_set : ?sideff:bool -> rigid -> evar_map -> Univ.universe_context_set -> evar_map -val merge_universe_subst : evar_map -> Universes.universe_opt_subst -> evar_map - -val with_context_set : rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a - -val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst -val abstract_undefined_variables : evar_universe_context -> evar_universe_context - -val fix_undefined_variables : evar_map -> evar_map - -val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_subst - -val nf_constraints : evar_map -> evar_map - -val update_sigma_env : evar_map -> env -> evar_map - -(** Polymorphic universes *) - -val fresh_sort_in_family : ?rigid:rigid -> env -> evar_map -> sorts_family -> evar_map * sorts -val fresh_constant_instance : env -> evar_map -> constant -> evar_map * pconstant -val fresh_inductive_instance : env -> evar_map -> inductive -> evar_map * pinductive -val fresh_constructor_instance : env -> evar_map -> constructor -> evar_map * pconstructor - -val fresh_global : ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map -> - Globnames.global_reference -> evar_map * constr - -(******************************************************************** - Conversion w.r.t. an evar map, not unifying universes. See - [Reductionops.infer_conv] for conversion up-to universes. *) - -val test_conversion : env -> evar_map -> conv_pb -> constr -> constr -> bool -(** WARNING: This does not allow unification of universes *) - -val eq_constr_univs : evar_map -> constr -> constr -> evar_map * bool -(** Syntactic equality up to universes, recording the associated constraints *) - -val e_eq_constr_univs : evar_map ref -> constr -> constr -> bool -(** Syntactic equality up to universes. *) - -(********************************************************************) -(* constr with holes and pending resolution of classes, conversion *) -(* problems, candidates, etc. *) - -type pending = (* before: *) evar_map * (* after: *) evar_map - -type pending_constr = pending * constr - -type open_constr = evar_map * constr (* Special case when before is empty *) - -(** Partially constructed constrs. *) - -type unsolvability_explanation = SeveralInstancesFound of int -(** Failure explanation. *) - -val pr_existential_key : evar_map -> evar -> Pp.std_ppcmds - -(** {5 Debug pretty-printers} *) - -val pr_evar_info : evar_info -> Pp.std_ppcmds -val pr_evar_constraints : evar_constraint list -> Pp.std_ppcmds -val pr_evar_map : ?with_univs:bool -> int option -> evar_map -> Pp.std_ppcmds -val pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> evar_info -> bool) -> - evar_map -> Pp.std_ppcmds -val pr_metaset : Metaset.t -> Pp.std_ppcmds -val pr_evar_universe_context : evar_universe_context -> Pp.std_ppcmds -val pr_evd_level : evar_map -> Univ.Level.t -> Pp.std_ppcmds - -(** {5 Deprecated functions} *) - -val create_evar_defs : evar_map -> evar_map -(** Create an [evar_map] with empty meta map: *) - -val create_goal_evar_defs : evar_map -> evar_map |