diff options
Diffstat (limited to 'pretyping/evd.mli')
| -rw-r--r-- | pretyping/evd.mli | 123 |
1 files changed, 120 insertions, 3 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli index f66667aa..40ecce6e 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -6,12 +6,15 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: evd.mli,v 1.3.2.1 2004/07/16 19:30:44 herbelin Exp $ i*) +(*i $Id: evd.mli 8688 2006-04-07 15:08:12Z msozeau $ i*) (*i*) +open Util open Names open Term open Sign +open Libnames +open Mod_subst (*i*) (* The type of mappings for existential variables. @@ -28,9 +31,11 @@ type evar_body = type evar_info = { evar_concl : constr; - evar_hyps : named_context; + evar_hyps : Environ.named_context_val; evar_body : evar_body} +val eq_evar_info : evar_info -> evar_info -> bool +val evar_context : evar_info -> named_context type evar_map val empty : evar_map @@ -43,15 +48,127 @@ val rmv : evar_map -> evar -> evar_map val remap : evar_map -> evar -> evar_info -> evar_map val in_dom : evar_map -> evar -> bool val to_list : evar_map -> (evar * evar_info) list +val fold : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a val define : evar_map -> evar -> constr -> evar_map -val non_instantiated : evar_map -> (evar * evar_info) list val is_evar : evar_map -> evar -> bool val is_defined : evar_map -> evar -> bool val evar_body : evar_info -> evar_body +val evar_env : evar_info -> Environ.env val string_of_existential : evar -> string val existential_of_int : int -> evar + +(*s [existential_value sigma ev] raises [NotInstantiatedEvar] if [ev] has + no body and [Not_found] if it does not exist in [sigma] *) + +exception NotInstantiatedEvar +val existential_value : evar_map -> existential -> constr +val existential_type : evar_map -> existential -> types +val existential_opt_value : evar_map -> existential -> constr option + +(*********************************************************************) +(* constr with holes *) +type open_constr = evar_map * constr + +(*********************************************************************) +(* The type constructor ['a sigma] adds an evar map to an object of + type ['a] *) +type 'a sigma = { + it : 'a ; + sigma : evar_map} + +val sig_it : 'a sigma -> 'a +val sig_sig : 'a sigma -> evar_map + +(*********************************************************************) +(* Meta map *) + +module Metaset : Set.S with type elt = metavariable + +val meta_exists : (metavariable -> bool) -> Metaset.t -> bool + +type 'a freelisted = { + rebus : 'a; + freemetas : Metaset.t } + +val mk_freelisted : constr -> constr freelisted +val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted + +type clbinding = + | Cltyp of name * constr freelisted + | Clval of name * constr freelisted * constr freelisted + +val map_clb : (constr -> constr) -> clbinding -> clbinding + +(*********************************************************************) +(* Unification state *) +type evar_defs + +(* Substitution is not applied to the [evar_map] *) +val subst_evar_defs : substitution -> evar_defs -> evar_defs + +(* create an [evar_defs] with empty meta map: *) +val create_evar_defs : evar_map -> evar_defs +val evars_of : evar_defs -> evar_map +val evars_reset_evd : evar_map -> evar_defs -> evar_defs + +(* Evars *) +type hole_kind = + | ImplicitArg of global_reference * (int * identifier option) + | BinderType of name + | QuestionMark + | CasesType + | InternalHole + | TomatchTypeParameter of inductive * int +val is_defined_evar : evar_defs -> existential -> bool +val is_undefined_evar : evar_defs -> constr -> bool +val undefined_evars : evar_defs -> evar_defs +val evar_declare : + Environ.named_context_val -> evar -> types -> ?src:loc * hole_kind -> + evar_defs -> evar_defs +val evar_define : evar -> constr -> evar_defs -> evar_defs +val evar_source : existential_key -> evar_defs -> loc * hole_kind + +(* Unification constraints *) +type conv_pb = Reduction.conv_pb +type evar_constraint = conv_pb * constr * constr +val add_conv_pb : evar_constraint -> evar_defs -> evar_defs +val get_conv_pbs : evar_defs -> (evar_constraint -> bool) -> + evar_defs * evar_constraint list + +(* Metas *) +val meta_list : evar_defs -> (metavariable * clbinding) list +val meta_defined : evar_defs -> metavariable -> bool +(* [meta_fvalue] raises [Not_found] if meta not in map or [Anomaly] if + meta has no value *) +val meta_fvalue : evar_defs -> metavariable -> constr freelisted +val meta_ftype : evar_defs -> metavariable -> constr freelisted +val meta_name : evar_defs -> metavariable -> name +val meta_with_name : evar_defs -> identifier -> metavariable +val meta_declare : + metavariable -> types -> ?name:name -> evar_defs -> evar_defs +val meta_assign : metavariable -> constr -> evar_defs -> evar_defs + +(* [meta_merge evd1 evd2] returns [evd2] extended with the metas of [evd1] *) +val meta_merge : evar_defs -> evar_defs -> evar_defs + +(**********************************************************) +(* Sort variables *) + +val new_sort_variable : evar_map -> sorts * evar_map +val is_sort_variable : evar_map -> sorts -> bool +val whd_sort_variable : evar_map -> constr -> constr +val set_leq_sort_variable : evar_map -> sorts -> sorts -> evar_map +val define_sort_variable : evar_map -> sorts -> sorts -> evar_map + +(*********************************************************************) +(* debug pretty-printer: *) + +val pr_evar_info : evar_info -> Pp.std_ppcmds +val pr_evar_map : evar_map -> Pp.std_ppcmds +val pr_evar_defs : evar_defs -> Pp.std_ppcmds +val pr_sort_constraints : evar_map -> Pp.std_ppcmds |