diff options
Diffstat (limited to 'pretyping/evd.mli')
| -rw-r--r-- | pretyping/evd.mli | 278 |
1 files changed, 153 insertions, 125 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli index b9cb2142..46f13d5f 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: evd.mli 11865 2009-01-28 17:34:30Z herbelin $ i*) +(*i $Id$ i*) (*i*) open Util @@ -20,84 +20,6 @@ open Mod_subst open Termops (*i*) -(* The type of mappings for existential variables. - The keys are integers and the associated information is a record - containing the type of the evar ([evar_concl]), the context under which - it was introduced ([evar_hyps]) and its definition ([evar_body]). - [evar_info] is used to add any other kind of information. *) - -type evar = existential_key - -type evar_body = - | Evar_empty - | Evar_defined of constr - -type evar_info = { - evar_concl : constr; - evar_hyps : named_context_val; - evar_body : evar_body; - evar_filter : bool list; - evar_extra : Dyn.t option} - -val eq_evar_info : evar_info -> evar_info -> bool - -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_body : evar_info -> evar_body -val evar_filter : evar_info -> bool list -val evar_unfiltered_env : evar_info -> env -val evar_env : evar_info -> env - -type evar_map -val eq_evar_map : evar_map -> evar_map -> bool - -val empty : evar_map - -val add : evar_map -> evar -> evar_info -> evar_map - -val dom : evar_map -> evar list -val find : evar_map -> evar -> evar_info -val remove : evar_map -> evar -> evar_map -val mem : 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 merge : evar_map -> evar_map -> evar_map - -val define : evar_map -> evar -> constr -> evar_map - -val is_evar : evar_map -> evar -> bool - -val is_defined : evar_map -> evar -> bool - -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 *) @@ -122,7 +44,7 @@ val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted (e.g. the solution [P] to [?X u v = P u v] can be eta-expanded twice) *) -type instance_constraint = +type instance_constraint = IsSuperType | IsSubType | ConvUpToEta of int | UserGiven (* Status of the unification of the type of an instance against the type of @@ -153,19 +75,9 @@ type clbinding = val map_clb : (constr -> constr) -> clbinding -> clbinding -(*********************************************************************) -(* Unification state *) -type evar_defs - -(* Assume empty [evar_map] and [conv_pbs] *) -val subst_evar_defs_light : substitution -> evar_defs -> evar_defs -(* create an [evar_defs] with empty meta map: *) -val create_evar_defs : evar_map -> evar_defs -val create_goal_evar_defs : evar_map -> evar_defs -val empty_evar_defs : evar_defs -val evars_of : evar_defs -> evar_map -val evars_reset_evd : evar_map -> evar_defs -> evar_defs +(*********************************************************************) +(*** Kinds of existential variables ***) (* Should the obligation be defined (opaque or transparent (default)) or defined transparent and expanded in the term? *) @@ -174,7 +86,7 @@ type obligation_definition_status = Define of bool | Expand (* Evars *) type hole_kind = - | ImplicitArg of global_reference * (int * identifier option) + | ImplicitArg of global_reference * (int * identifier option) * bool (* Force inference *) | BinderType of name | QuestionMark of obligation_definition_status | CasesType @@ -182,54 +94,148 @@ type hole_kind = | TomatchTypeParameter of inductive * int | GoalEvar | ImpossibleCase -val is_defined_evar : evar_defs -> existential -> bool -val is_undefined_evar : evar_defs -> constr -> bool -val undefined_evars : evar_defs -> evar_defs + | MatchingVar of bool * identifier + +(*********************************************************************) +(*** 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. *) + +(* Information about existential variables. *) +type evar = existential_key + +val string_of_existential : evar -> string +val existential_of_int : int -> evar + +type evar_body = + | Evar_empty + | Evar_defined of constr + +type evar_info = { + evar_concl : constr; + evar_hyps : named_context_val; + evar_body : evar_body; + evar_filter : bool list; + evar_source : hole_kind located; + evar_extra : Dyn.t option} + +val eq_evar_info : evar_info -> evar_info -> bool + +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_body : evar_info -> evar_body +val evar_filter : evar_info -> bool list +val evar_unfiltered_env : evar_info -> env +val evar_env : evar_info -> env + +(*** Unification state ***) +type evar_map + +(* Unification state and existential variables *) + +(* Assuming that the second map extends the first one, this says if + some existing evar has been refined *) +val progress_evar_map : evar_map -> evar_map -> bool + +val empty : evar_map +val is_empty : evar_map -> bool + +val add : evar_map -> evar -> evar_info -> evar_map + +val dom : evar_map -> evar list +val find : evar_map -> evar -> evar_info +val remove : evar_map -> evar -> evar_map +val mem : 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 merge : evar_map -> evar_map -> evar_map + +val define : evar -> constr -> evar_map -> evar_map + +val is_evar : evar_map -> evar -> bool + +val is_defined : evar_map -> evar -> bool + +(*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 + +(* Assume empty universe constraints in [evar_map] and [conv_pbs] *) +val subst_evar_defs_light : substitution -> evar_map -> evar_map + +(* spiwack: this function seems to somewhat break the abstraction. *) +val evars_reset_evd : evar_map -> evar_map -> evar_map + + +(* spiwack: [is_undefined_evar] should be considered a candidate + for moving to evarutils *) +val is_undefined_evar : evar_map -> constr -> bool +val undefined_evars : evar_map -> evar_map val evar_declare : named_context_val -> evar -> types -> ?src:loc * hole_kind -> - ?filter:bool list -> evar_defs -> evar_defs -val evar_define : evar -> constr -> evar_defs -> evar_defs -val evar_source : existential_key -> evar_defs -> loc * hole_kind + ?filter:bool list -> evar_map -> evar_map +val evar_source : existential_key -> evar_map -> loc * hole_kind + +(* spiwack: this function seems to somewhat break the abstraction. *) +(* [evar_merge evd ev1] extends the evars of [evd] with [evd1] *) +val evar_merge : evar_map -> evar_map -> evar_map -(* [evar_merge evd evars] extends the evars of [evd] with [evars] *) -val evar_merge : evar_defs -> evar_map -> evar_defs +val evar_list : evar_map -> constr -> existential list (* Unification constraints *) type conv_pb = Reduction.conv_pb type evar_constraint = conv_pb * env * constr * constr -val add_conv_pb : evar_constraint -> evar_defs -> evar_defs -val extract_changed_conv_pbs : evar_defs -> - (existential_key list -> evar_constraint -> bool) -> - evar_defs * evar_constraint list -val extract_all_conv_pbs : evar_defs -> evar_defs * evar_constraint list +val add_conv_pb : evar_constraint -> evar_map -> evar_map + +module ExistentialSet : Set.S with type elt = existential_key +val extract_changed_conv_pbs : evar_map -> + (ExistentialSet.t -> evar_constraint -> bool) -> + evar_map * evar_constraint list +val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list (* Metas *) -val find_meta : evar_defs -> metavariable -> clbinding -val meta_list : evar_defs -> (metavariable * clbinding) list -val meta_defined : evar_defs -> metavariable -> bool +val find_meta : evar_map -> metavariable -> clbinding +val meta_list : evar_map -> (metavariable * clbinding) list +val meta_defined : evar_map -> 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 * instance_status -val meta_opt_fvalue : evar_defs -> metavariable -> (constr freelisted * instance_status) option -val meta_ftype : evar_defs -> metavariable -> constr freelisted -val meta_name : evar_defs -> metavariable -> name -val meta_with_name : evar_defs -> identifier -> metavariable + meta has no value *) +val meta_value : evar_map -> metavariable -> constr +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 +val meta_with_name : evar_map -> identifier -> metavariable val meta_declare : - metavariable -> types -> ?name:name -> evar_defs -> evar_defs -val meta_assign : metavariable -> constr * instance_status -> evar_defs -> evar_defs -val meta_reassign : metavariable -> constr * instance_status -> evar_defs -> evar_defs + metavariable -> types -> ?name:name -> 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 (* [meta_merge evd1 evd2] returns [evd2] extended with the metas of [evd1] *) -val meta_merge : evar_defs -> evar_defs -> evar_defs +val meta_merge : evar_map -> evar_map -> evar_map -val undefined_metas : evar_defs -> metavariable list -val metas_of : evar_defs -> metamap -val map_metas_fvalue : (constr -> constr) -> evar_defs -> evar_defs +val undefined_metas : evar_map -> metavariable list +val metas_of : evar_map -> meta_type_map +val map_metas_fvalue : (constr -> constr) -> evar_map -> evar_map type metabinding = metavariable * constr * instance_status -val retract_coercible_metas : evar_defs -> metabinding list * evar_defs +val retract_coercible_metas : evar_map -> metabinding list * evar_map val subst_defined_metas : metabinding list -> constr -> constr option (**********************************************************) @@ -241,6 +247,20 @@ 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 +(*********************************************************************) +(* 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 + (**********************************************************) (* Failure explanation *) @@ -250,7 +270,15 @@ type unsolvability_explanation = SeveralInstancesFound of int (* 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_evar_map : evar_map -> Pp.std_ppcmds val pr_sort_constraints : evar_map -> Pp.std_ppcmds val pr_metaset : Metaset.t -> Pp.std_ppcmds + + +(*** /!\Deprecated /!\ ***) +(* create an [evar_map] with empty meta map: *) +val create_evar_defs : evar_map -> evar_map +val create_goal_evar_defs : evar_map -> evar_map +val is_defined_evar : evar_map -> existential -> bool +val subst_evar_map : substitution -> evar_map -> evar_map +(*** /Deprecaded ***) |