Imported Upstream snapshot 8.3~beta0+13298

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 ***)