summaryrefslogtreecommitdiff
path: root/pretyping/evd.mli
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /pretyping/evd.mli
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'pretyping/evd.mli')
-rw-r--r--pretyping/evd.mli278
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 ***)