diff options
Diffstat (limited to 'pretyping/evd.mli')
| -rw-r--r-- | pretyping/evd.mli | 57 |
1 files changed, 38 insertions, 19 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli index fe785a83..5c508419 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -129,10 +129,13 @@ type evar_map val empty : evar_map (** The empty evar map. *) -val from_env : ?ctx:evar_universe_context -> env -> 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. *) @@ -258,10 +261,10 @@ val dependent_evar_ident : existential_key -> evar_map -> Id.t (** {5 Side-effects} *) -val emit_side_effects : Declareops.side_effects -> evar_map -> evar_map +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 -> Declareops.side_effects +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 @@ -310,6 +313,19 @@ val add_universe_constraints : evar_map -> Universes.universe_constraints -> eva @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 = { @@ -462,7 +478,7 @@ val univ_flexible_alg : rigid type 'a in_evar_universe_context = 'a * evar_universe_context -val evar_universe_context_set : evar_universe_context -> Univ.universe_context_set +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 @@ -471,6 +487,11 @@ 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 @@ -487,9 +508,11 @@ val normalize_evar_universe_context_variables : evar_universe_context -> val normalize_evar_universe_context : evar_universe_context -> evar_universe_context -val new_univ_level_variable : ?name:string -> rigid -> evar_map -> evar_map * Univ.universe_level -val new_univ_variable : ?name:string -> rigid -> evar_map -> evar_map * Univ.universe -val new_sort_variable : ?name:string -> rigid -> evar_map -> evar_map * sorts +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 @@ -514,7 +537,8 @@ 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 : evar_map -> Univ.universe_context +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 @@ -522,7 +546,7 @@ 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 : rigid -> evar_map -> Univ.universe_context_set -> 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 @@ -536,6 +560,8 @@ val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_sub 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 @@ -547,14 +573,11 @@ 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: might generate universe unifications - that are kept in the evarmap. - Raises [NotConvertible]. *) - -val conversion : env -> evar_map -> conv_pb -> constr -> constr -> evar_map + 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 -(** This one forgets about the assignemts of universes. *) +(** 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 *) @@ -562,10 +585,6 @@ val eq_constr_univs : evar_map -> constr -> constr -> evar_map * bool val e_eq_constr_univs : evar_map ref -> constr -> constr -> bool (** Syntactic equality up to universes. *) -val eq_constr_univs_test : evar_map -> constr -> constr -> bool -(** Syntactic equality up to universes, throwing away the (consistent) constraints - in case of success. *) - (********************************************************************) (* constr with holes and pending resolution of classes, conversion *) (* problems, candidates, etc. *) |