diff options
Diffstat (limited to 'engine/evd.mli')
| -rw-r--r-- | engine/evd.mli | 208 |
1 files changed, 109 insertions, 99 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index 911799c4..db2bd4ee 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -28,15 +28,10 @@ open Environ It also contains conversion constraints, debugging information and information about meta variables. *) -(** {5 Existential variables and unification states} *) - -type evar = Evar.t -[@@ocaml.deprecated "use Evar.t"] -(** Existential variables. *) +type econstr +type etypes = econstr -(** {6 Evars} *) -val string_of_existential : Evar.t -> string -[@@ocaml.deprecated "use Evar.print"] +(** {5 Existential variables and unification states} *) (** {6 Evar filters} *) @@ -86,16 +81,16 @@ end type evar_body = | Evar_empty - | Evar_defined of constr + | Evar_defined of econstr module Store : Store.S (** Datatype used to store additional information in evar maps. *) type evar_info = { - evar_concl : constr; + evar_concl : econstr; (** Type of the evar. *) - evar_hyps : named_context_val; + evar_hyps : named_context_val; (** TODO econstr? *) (** Context of the evar. *) evar_body : evar_body; (** Optional content of the evar. *) @@ -105,32 +100,29 @@ type evar_info = { in the solution *) evar_source : Evar_kinds.t located; (** Information about the evar. *) - evar_candidates : constr list option; + evar_candidates : econstr list option; (** List of possible solutions when known that it is a finite list *) 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 -> Context.Named.t -val evar_filtered_context : evar_info -> Context.Named.t +val make_evar : named_context_val -> etypes -> evar_info +val evar_concl : evar_info -> econstr +val evar_context : evar_info -> (econstr, etypes) Context.Named.pt +val evar_filtered_context : evar_info -> (econstr, etypes) Context.Named.pt 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_candidates : evar_info -> constr list option 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 +val map_evar_body : (econstr -> econstr) -> evar_body -> evar_body +val map_evar_info : (econstr -> econstr) -> evar_info -> evar_info (** {6 Unification state} **) -type evar_universe_context = UState.t -[@@ocaml.deprecated "Alias of UState.t"] -(** 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. *) @@ -190,7 +182,7 @@ val raw_map_undefined : (Evar.t -> evar_info -> evar_info) -> evar_map -> evar_m (** Same as {!raw_map}, but restricted to undefined evars. For efficiency reasons. *) -val define : Evar.t-> constr -> evar_map -> evar_map +val define : Evar.t-> econstr -> 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.} @@ -198,7 +190,7 @@ val define : Evar.t-> constr -> evar_map -> evar_map {- All the evars present in the constr should be present in the evar map.} } *) -val cmap : (constr -> constr) -> evar_map -> evar_map +val cmap : (econstr -> econstr) -> evar_map -> evar_map (** Map the function on all terms in the evar map. *) val is_evar : evar_map -> Evar.t-> bool @@ -222,20 +214,26 @@ val drop_all_defined : evar_map -> evar_map exception NotInstantiatedEvar -val existential_value : evar_map -> existential -> constr +val existential_value : evar_map -> econstr pexistential -> econstr (** [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_value0 : evar_map -> existential -> constr + +val existential_type : evar_map -> econstr pexistential -> etypes + +val existential_type0 : evar_map -> existential -> types -val existential_opt_value : evar_map -> existential -> constr option +val existential_opt_value : evar_map -> econstr pexistential -> econstr option (** Same as {!existential_value} but returns an option instead of raising an exception. *) -val evar_instance_array : (Context.Named.Declaration.t -> 'a -> bool) -> evar_info -> +val existential_opt_value0 : evar_map -> existential -> constr option + +val evar_instance_array : (Constr.named_declaration -> 'a -> bool) -> evar_info -> 'a array -> (Id.t * 'a) list -val instantiate_evar_array : evar_info -> constr -> constr array -> constr +val instantiate_evar_array : evar_info -> econstr -> econstr array -> econstr val evars_reset_evd : ?with_conv_pbs:bool -> ?with_univs:bool -> evar_map -> evar_map -> evar_map @@ -243,15 +241,16 @@ val evars_reset_evd : ?with_conv_pbs:bool -> ?with_univs:bool -> (** {6 Misc} *) -val restrict : Evar.t-> Filter.t -> ?candidates:constr list -> +val restrict : Evar.t-> Filter.t -> ?candidates:econstr list -> ?src:Evar_kinds.t located -> evar_map -> evar_map * Evar.t (** Restrict an undefined evar into a new evar by filtering context and - possibly limiting the instances to a set of candidates *) + possibly limiting the instances to a set of candidates (candidates + are filtered according to the filter) *) val is_restricted_evar : evar_info -> Evar.t option (** Tell if an evar comes from restriction of another evar, and if yes, which *) -val downcast : Evar.t-> types -> evar_map -> evar_map +val downcast : Evar.t-> etypes -> 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 *) @@ -341,11 +340,9 @@ val shelve_on_future_goals : Evar.t list -> future_goals -> future_goals 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.Constraints.t -> evar_map +val add_universe_constraints : evar_map -> UnivProblem.Set.t -> evar_map (** Add the given universe unification constraints to the evar map. @raise UniversesDiffer in case a first-order unification fails. @raise UniverseInconsistency . @@ -397,8 +394,8 @@ type 'a freelisted = { rebus : 'a; freemetas : Metaset.t } -val metavars_of : constr -> Metaset.t -val mk_freelisted : constr -> constr freelisted +val metavars_of : econstr -> Metaset.t +val mk_freelisted : econstr -> econstr freelisted val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted (** Status of an instance found by unification wrt to the meta it solves: @@ -436,13 +433,17 @@ 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 + | Cltyp of Name.t * econstr freelisted + | Clval of Name.t * (econstr freelisted * instance_status) * econstr freelisted (** Unification constraints *) type conv_pb = Reduction.conv_pb -type evar_constraint = conv_pb * env * constr * constr +type evar_constraint = conv_pb * env * econstr * econstr + +(** The following two functions are for internal use only, + see [Evarutil.add_unification_pb] for a safe interface. *) val add_conv_pb : ?tail:bool -> evar_constraint -> evar_map -> evar_map +val conv_pbs : evar_map -> evar_constraint list val extract_changed_conv_pbs : evar_map -> (Evar.Set.t -> evar_constraint -> bool) -> @@ -457,7 +458,7 @@ val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t option val evars_of_term : constr -> Evar.Set.t (** including evars in instances of evars *) -val evars_of_named_context : Context.Named.t -> Evar.Set.t +val evars_of_named_context : (econstr, etypes) Context.Named.pt -> Evar.Set.t val evars_of_filtered_evar_info : evar_info -> Evar.Set.t @@ -465,19 +466,20 @@ val evars_of_filtered_evar_info : evar_info -> Evar.Set.t val meta_list : evar_map -> (metavariable * clbinding) list val meta_defined : evar_map -> metavariable -> bool -val meta_value : evar_map -> metavariable -> constr +val meta_value : evar_map -> metavariable -> econstr (** [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_fvalue : evar_map -> metavariable -> econstr freelisted * instance_status +val meta_opt_fvalue : evar_map -> metavariable -> (econstr freelisted * instance_status) option +val meta_type : evar_map -> metavariable -> etypes +val meta_type0 : evar_map -> metavariable -> types +val meta_ftype : evar_map -> metavariable -> etypes freelisted val meta_name : evar_map -> metavariable -> Name.t 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 + metavariable -> etypes -> ?name:Name.t -> evar_map -> evar_map +val meta_assign : metavariable -> econstr * instance_status -> evar_map -> evar_map +val meta_reassign : metavariable -> econstr * instance_status -> evar_map -> evar_map val clear_metas : evar_map -> evar_map @@ -485,10 +487,10 @@ val clear_metas : evar_map -> evar_map 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 -val map_metas : (constr -> constr) -> evar_map -> evar_map +val map_metas_fvalue : (econstr -> econstr) -> evar_map -> evar_map +val map_metas : (econstr -> econstr) -> evar_map -> evar_map -type metabinding = metavariable * constr * instance_status +type metabinding = metavariable * econstr * instance_status val retract_coercible_metas : evar_map -> metabinding list * evar_map @@ -519,48 +521,11 @@ val univ_flexible_alg : rigid type 'a in_evar_universe_context = 'a * UState.t -val evar_universe_context_set : UState.t -> Univ.ContextSet.t -[@@ocaml.deprecated "Alias of UState.context_set"] -val evar_universe_context_constraints : UState.t -> Univ.Constraint.t -[@@ocaml.deprecated "Alias of UState.constraints"] -val evar_context_universe_context : UState.t -> Univ.UContext.t -[@@ocaml.deprecated "alias of UState.context"] - -val evar_universe_context_of : Univ.ContextSet.t -> UState.t -[@@ocaml.deprecated "Alias of UState.of_context_set"] -val empty_evar_universe_context : UState.t -[@@ocaml.deprecated "Alias of UState.empty"] -val union_evar_universe_context : UState.t -> UState.t -> - UState.t -[@@ocaml.deprecated "Alias of UState.union"] -val evar_universe_context_subst : UState.t -> Universes.universe_opt_subst -[@@ocaml.deprecated "Alias of UState.subst"] -val constrain_variables : Univ.LSet.t -> UState.t -> UState.t -[@@ocaml.deprecated "Alias of UState.constrain_variables"] - - -val evar_universe_context_of_binders : - Universes.universe_binders -> UState.t -[@@ocaml.deprecated "Alias of UState.of_binders"] - -val make_evar_universe_context : env -> Misctypes.lident list option -> UState.t -[@@ocaml.deprecated "Use UState.make or UState.make_with_initial_binders"] val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map (** Raises Not_found if not a name for a universe in this map. *) val universe_of_name : evar_map -> Id.t -> Univ.Level.t -val universe_binders : evar_map -> Universes.universe_binders -val add_constraints_context : UState.t -> - Univ.Constraint.t -> UState.t -[@@ocaml.deprecated "Alias of UState.add_constraints"] - - -val normalize_evar_universe_context_variables : UState.t -> - Univ.universe_subst in_evar_universe_context -[@@ocaml.deprecated "Alias of UState.normalize_variables"] - -val normalize_evar_universe_context : UState.t -> UState.t -[@@ocaml.deprecated "Alias of UState.minimize"] +val universe_binders : evar_map -> UnivNames.universe_binders val new_univ_level_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Level.t val new_univ_variable : ?loc:Loc.t -> ?name:Id.t -> rigid -> evar_map -> evar_map * Univ.Universe.t @@ -591,9 +556,11 @@ val set_eq_instances : ?flex:bool -> val check_eq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool val check_leq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool +val check_constraints : evar_map -> Univ.Constraint.t -> bool + val evar_universe_context : evar_map -> UState.t val universe_context_set : evar_map -> Univ.ContextSet.t -val universe_subst : evar_map -> Universes.universe_opt_subst +val universe_subst : evar_map -> UnivSubst.universe_opt_subst val universes : evar_map -> UGraph.t (** [to_universe_context evm] extracts the local universes and @@ -612,13 +579,11 @@ val merge_universe_context : evar_map -> UState.t -> evar_map val set_universe_context : evar_map -> UState.t -> evar_map val merge_context_set : ?loc:Loc.t -> ?sideff:bool -> rigid -> evar_map -> Univ.ContextSet.t -> evar_map -val merge_universe_subst : evar_map -> Universes.universe_opt_subst -> evar_map +val merge_universe_subst : evar_map -> UnivSubst.universe_opt_subst -> evar_map val with_context_set : ?loc:Loc.t -> 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 : UState.t -> UState.t -[@@ocaml.deprecated "Alias of UState.abstract_undefined_variables"] val fix_undefined_variables : evar_map -> evar_map @@ -626,26 +591,24 @@ val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_sub (** Universe minimization *) val minimize_universes : evar_map -> evar_map -val nf_constraints : evar_map -> evar_map -[@@ocaml.deprecated "Alias of Evd.minimize_universes"] val update_sigma_env : evar_map -> env -> evar_map (** Polymorphic universes *) -val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> env -> evar_map -> Sorts.family -> evar_map * Sorts.t +val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> evar_map -> Sorts.family -> evar_map * Sorts.t val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> Constant.t -> evar_map * pconstant val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> evar_map * pinductive val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env -> - evar_map -> Globnames.global_reference -> evar_map * constr + evar_map -> GlobRef.t -> evar_map * econstr (********************************************************************) (* constr with holes and pending resolution of classes, conversion *) (* problems, candidates, etc. *) -type open_constr = evar_map * constr (* Special case when before is empty *) +type open_constr = evar_map * econstr (* Special case when before is empty *) (** Partially constructed constrs. *) @@ -665,3 +628,50 @@ val create_evar_defs : evar_map -> evar_map (** Create an [evar_map] with empty meta map: *) +(** Use this module only to bootstrap EConstr *) +module MiniEConstr : sig + module ESorts : sig + type t + val make : Sorts.t -> t + val kind : evar_map -> t -> Sorts.t + val unsafe_to_sorts : t -> Sorts.t + end + + module EInstance : sig + type t + val make : Univ.Instance.t -> t + val kind : evar_map -> t -> Univ.Instance.t + val empty : t + val is_empty : t -> bool + val unsafe_to_instance : t -> Univ.Instance.t + end + + type t = econstr + + val kind : evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term + val kind_upto : evar_map -> constr -> (constr, types, Sorts.t, Univ.Instance.t) Constr.kind_of_term + val kind_of_type : evar_map -> t -> (t, t) Term.kind_of_type + + val whd_evar : evar_map -> t -> t + + val of_kind : (t, t, ESorts.t, EInstance.t) Constr.kind_of_term -> t + + val of_constr : Constr.t -> t + + val to_constr : ?abort_on_undefined_evars:bool -> evar_map -> t -> Constr.t + + val unsafe_to_constr : t -> Constr.t + + val unsafe_eq : (t, Constr.t) eq + + val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> + (t, t) Context.Named.Declaration.pt + val unsafe_to_named_decl : (t, t) Context.Named.Declaration.pt -> + (Constr.t, Constr.types) Context.Named.Declaration.pt + val unsafe_to_rel_decl : (t, t) Context.Rel.Declaration.pt -> + (Constr.t, Constr.types) Context.Rel.Declaration.pt + val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> + (t, t) Context.Rel.Declaration.pt + val to_rel_decl : evar_map -> (t, t) Context.Rel.Declaration.pt -> + (Constr.t, Constr.types) Context.Rel.Declaration.pt +end |