Documentation of Evd.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16763 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 180 insertions, 116 deletions

diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 8dfc81fe8f..354a5b533f 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -17,92 +17,55 @@ open Libnames
 open Mod_subst
 open Termops
 
-(********************************************************************
-   Meta map *)
-
-module Metaset : Set.S with type elt = metavariable
-module Metamap : Map.ExtS with type key = metavariable and module Set := Metaset
-
-type 'a freelisted = {
-  rebus : 'a;
-  freemetas : Metaset.t }
-
-val metavars_of : constr -> Metaset.t
-val mk_freelisted : constr -> constr freelisted
-val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted
-
-(** Status of an instance found by unification wrt to the meta it solves:
-  - a supertype of the meta (e.g. the solution to ?X <= T is a supertype of ?X)
-  - a subtype of the meta (e.g. the solution to T <= ?X is a supertype of ?X)
-  - a term that can be eta-expanded n times while still being a solution
-    (e.g. the solution [P] to [?X u v = P u v] can be eta-expanded twice)
-*)
-
-type instance_constraint = IsSuperType | IsSubType | Conv
-
-val eq_instance_constraint :
-  instance_constraint -> instance_constraint -> bool
-
-(** Status of the unification of the type of an instance against the type of
-     the meta it instantiates:
-   - CoerceToType means that the unification of types has not been done
-     and that a coercion can still be inserted: the meta should not be
-     substituted freely (this happens for instance given via the
-     "with" binding clause).
-   - TypeProcessed means that the information obtainable from the
-     unification of types has been extracted.
-   - TypeNotProcessed means that the unification of types has not been
-     done but it is known that no coercion may be inserted: the meta
-     can be substituted freely.
-*)
-
-type instance_typing_status =
-    CoerceToType | TypeNotProcessed | TypeProcessed
-
-(** Status of an instance together with the status of its type unification *)
-
-type instance_status = instance_constraint * instance_typing_status
-
-(** Clausal environments *)
-
-type clbinding =
-  | Cltyp of Name.t * constr freelisted
-  | Clval of Name.t * (constr freelisted * instance_status) * constr freelisted
-
-val map_clb : (constr -> constr) -> clbinding -> clbinding
+(** {5 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.
 
-(********************************************************************
-  ** Existential variables and unification states ***)
+    It also contains conversion constraints, debugging information and
+    information about meta variables. *)
 
-(** 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. *)
+(** {6 Evars} *)
 
-(** Information about existential variables. *)
 type evar = existential_key
+(** Existential variables. TODO: Should be made opaque one day. *)
 
 val string_of_existential : evar -> string
 val existential_of_int : int -> evar
 
+module ExistentialSet : Set.S with type elt = existential_key
+module ExistentialMap : Map.ExtS
+  with type key = existential_key and module Set := ExistentialSet
+
+(** {6 Evar infos} *)
+
 type evar_body =
   | Evar_empty
   | Evar_defined of constr
 
 module Store : Store.S
+(** Datatype used to store additional information in evar maps. *)
 
 type evar_info = {
   evar_concl : constr;
+  (** Type of the evar. *)
   evar_hyps : named_context_val;
+  (** Context of the evar. *)
   evar_body : evar_body;
+  (** Optional content of the evar. *)
   evar_filter : bool list;
+  (** Boolean mask over {!evar_hyps}. Should have the same length.
+      TODO: document me more. *)
   evar_source : Evar_kinds.t located;
+  (** Information about the evar. *)
   evar_candidates : constr list option;
-  evar_extra : Store.t }
+  (** TODO: document this *)
+  evar_extra : Store.t
+  (** Extra store, used for clever hacks. *)
+}
 
 val eq_evar_info : evar_info -> evar_info -> bool
 
@@ -117,69 +80,102 @@ val evar_filter : evar_info -> bool list
 val evar_env :  evar_info -> env
 val evar_filtered_env :  evar_info -> env
 
-(*** Unification state ***)
-type evar_map
-
-module ExistentialSet : Set.S with type elt = existential_key
-module ExistentialMap : Map.ExtS
-  with type key = existential_key and module Set := ExistentialSet
+(** {6 Unification state} **)
 
-(** Unification state and existential variables *)
+type evar_map
+(** Type of unification state. Essentially a bunch of state-passing data needed
+    to handle incremental term construction. *)
 
+val progress_evar_map : evar_map -> evar_map -> bool
 (** 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
+(** The empty evar map. *)
+
 val is_empty : evar_map -> bool
+(** Whether an evarmap is empty. *)
+
+val has_undefined : evar_map -> bool
 (** [has_undefined sigma] is [true] if and only if
     there are uninstantiated evars in [sigma]. *)
-val has_undefined : evar_map -> bool
 
+val add : evar_map -> evar -> evar_info -> evar_map
 (** [add sigma ev info] adds [ev] with evar info [info] in sigma.
     Precondition: ev must not preexist in [sigma]. *)
-val add : evar_map -> evar -> evar_info -> evar_map
 
 val find : evar_map -> evar -> evar_info
+(** Recover the data associated to an evar. *)
+
 val find_undefined : evar_map -> evar -> evar_info
+(** Same as {!find} but restricted to undefined evars. For efficiency
+    reasons. *)
+
 val remove : evar_map -> evar -> evar_map
+(** Remove an evar from an evar map. Use with caution. *)
+
 val mem : evar_map -> evar -> bool
+(** Whether an evar is present in an evarmap. *)
+
 val to_list : evar_map -> (evar * evar_info) list
+(** Recover the evars as a list. This should not be used. *)
+
 val fold : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
+(** Apply a function to all evars and their associated info in an evarmap. *)
 
 val fold_undefined : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a
-(** [fold_undefined f m] iterates ("folds") function [f] over the undefined
-    evars (that is, whose value is [Evar_empty]) of map [m].
-    It optimizes the call of {!Evd.fold} to [f] and [undefined_evars m] *)
+(** Same as {!fold}, but restricted to undefined evars. For efficiency
+    reasons. *)
 
 val define : evar -> constr -> evar_map -> evar_map
+(** Set the body of an evar to the given constr. It is expected that:
+    {ul
+      {- The evar is already present in the evarmap.}
+      {- The evar is not defined in the evarmap yet.}
+      {- All the evars present in the constr should be present in the evar map.}
+    } *)
 
 val is_evar : evar_map -> evar -> bool
+(** Alias for {!mem}. *)
 
 val is_defined : evar_map -> evar -> bool
+(** Whether an evar is defined in an evarmap. *)
+
 val is_undefined : evar_map -> evar -> bool
+(** Whether an evar is not defined in an evarmap. *)
 
 val add_constraints : evar_map -> Univ.constraints -> evar_map
+(** Add universe constraints in an evar map. *)
 
 val undefined_map : evar_map -> evar_info ExistentialMap.t
+(** Access the undefined evar mapping directly. *)
+
 val defined_map : evar_map -> evar_info ExistentialMap.t
+(** Access the defined evar mapping directly. *)
 
-(** {6 ... } *)
-(** [existential_value sigma ev] raises [NotInstantiatedEvar] if [ev] has
-    no body and [Not_found] if it does not exist in [sigma] *)
+(** {6 Instantiating partial terms} *)
 
 exception NotInstantiatedEvar
+
 val existential_value : evar_map -> existential -> constr
+(** [existential_value sigma ev] raises [NotInstantiatedEvar] if [ev] has
+    no body and [Not_found] if it does not exist in [sigma] *)
+
 val existential_type : evar_map -> existential -> types
+
 val existential_opt_value : evar_map -> existential -> constr option
+(** Same as {!existential_value} but returns an option instead of raising an
+    exception. *)
 
 val instantiate_evar : named_context -> constr -> constr list -> constr
 
-(** Assume empty universe constraints in [evar_map] and [conv_pbs] *)
 val subst_evar_defs_light : substitution -> evar_map -> evar_map
+(** Assume empty universe constraints in [evar_map] and [conv_pbs] *)
 
+val evars_reset_evd : ?with_conv_pbs:bool -> evar_map ->  evar_map -> evar_map
 (** spiwack: this function seems to somewhat break the abstraction. *)
-val evars_reset_evd  : ?with_conv_pbs:bool -> evar_map ->  evar_map -> evar_map
+
+(** {6 Misc} *)
 
 val undefined_evars : evar_map -> evar_map
 val defined_evars : evar_map -> evar_map
@@ -188,7 +184,99 @@ val defined_evars : evar_map -> evar_map
 val evar_declare :
   named_context_val -> evar -> types -> ?src:Loc.t * Evar_kinds.t ->
       ?filter:bool list -> ?candidates:constr list -> evar_map -> evar_map
+(** Convenience function. Just a wrapper around {!add}. *)
+
 val evar_source : existential_key -> evar_map -> Evar_kinds.t located
+(** Convenience function. Wrapper around {!find} to recover the source of an
+    evar in a given evar map. *)
+
+(** {5 Sort variables}
+
+    Evar maps also keep track of the universe constraints defined at a given
+    point. This section defines the relevant manipulation functions. *)
+
+val new_univ_variable : evar_map -> evar_map * Univ.universe
+val new_sort_variable : evar_map -> evar_map * sorts
+val is_sort_variable : evar_map -> sorts -> bool
+val whd_sort_variable : evar_map -> constr -> constr
+val set_leq_sort : evar_map -> sorts -> sorts -> evar_map
+val set_eq_sort : evar_map -> sorts -> sorts -> evar_map
+
+(** {5 Enriching with evar maps} *)
+
+type 'a sigma = {
+  it : 'a ;
+  (** The base object. *)
+  eff : Declareops.side_effects;
+  (** Sideffects to be handled by the state machine. *)
+  sigma : evar_map
+  (** The added unification state. *)
+}
+(** The type constructor ['a sigma] adds an evar map to an object of type
+    ['a]. *)
+
+val sig_it  : 'a sigma -> 'a
+val sig_eff : 'a sigma -> Declareops.side_effects
+val sig_sig : 'a sigma -> evar_map
+val emit_side_effects : Declareops.side_effects -> 'a sigma -> 'a sigma
+
+(** {5 Meta machinery}
+
+    These functions are almost deprecated. They were used before the
+    introduction of the full-fledged evar calculus. In an ideal world, they
+    should be removed. Alas, some parts of the code still use them. Do not use
+    in newly-written code. *)
+
+module Metaset : Set.S with type elt = metavariable
+module Metamap : Map.ExtS with type key = metavariable and module Set := Metaset
+
+type 'a freelisted = {
+  rebus : 'a;
+  freemetas : Metaset.t }
+
+val metavars_of : constr -> Metaset.t
+val mk_freelisted : constr -> constr freelisted
+val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted
+
+(** Status of an instance found by unification wrt to the meta it solves:
+  - a supertype of the meta (e.g. the solution to ?X <= T is a supertype of ?X)
+  - a subtype of the meta (e.g. the solution to T <= ?X is a supertype of ?X)
+  - a term that can be eta-expanded n times while still being a solution
+    (e.g. the solution [P] to [?X u v = P u v] can be eta-expanded twice)
+*)
+
+type instance_constraint = IsSuperType | IsSubType | Conv
+
+val eq_instance_constraint :
+  instance_constraint -> instance_constraint -> bool
+
+(** Status of the unification of the type of an instance against the type of
+     the meta it instantiates:
+   - CoerceToType means that the unification of types has not been done
+     and that a coercion can still be inserted: the meta should not be
+     substituted freely (this happens for instance given via the
+     "with" binding clause).
+   - TypeProcessed means that the information obtainable from the
+     unification of types has been extracted.
+   - TypeNotProcessed means that the unification of types has not been
+     done but it is known that no coercion may be inserted: the meta
+     can be substituted freely.
+*)
+
+type instance_typing_status =
+    CoerceToType | TypeNotProcessed | TypeProcessed
+
+(** Status of an instance together with the status of its type unification *)
+
+type instance_status = instance_constraint * instance_typing_status
+
+(** Clausal environments *)
+
+type clbinding =
+  | Cltyp of Name.t * constr freelisted
+  | Clval of Name.t * (constr freelisted * instance_status) * constr freelisted
+
+val map_clb : (constr -> constr) -> clbinding -> clbinding
 
 (** Unification constraints *)
 type conv_pb = Reduction.conv_pb
@@ -208,9 +296,10 @@ val collect_evars : constr -> ExistentialSet.t
 val meta_list : evar_map -> (metavariable * clbinding) list
 val meta_defined : evar_map -> metavariable -> bool
 
+val meta_value     : evar_map -> metavariable -> constr
 (** [meta_fvalue] raises [Not_found] if meta not in map or [Anomaly] if
    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
@@ -233,51 +322,26 @@ type metabinding = metavariable * constr * instance_status
 val retract_coercible_metas : evar_map -> metabinding list * evar_map
 val subst_defined_metas : metabinding list -> constr -> constr option
 
-(*********************************************************
-   Sort variables *)
-
-val new_univ_variable : evar_map -> evar_map * Univ.universe
-val new_sort_variable : evar_map -> evar_map * sorts
-val is_sort_variable : evar_map -> sorts -> bool
-val whd_sort_variable : evar_map -> constr -> constr
-val set_leq_sort : evar_map -> sorts -> sorts -> evar_map
-val set_eq_sort : evar_map -> sorts -> sorts -> evar_map
+(** {5 FIXME: Nothing to do here} *)
 
-(********************************************************************
-   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 ;
-  eff : Declareops.side_effects;
-  sigma : evar_map
-}
-
-val sig_it  : 'a sigma -> 'a
-val sig_eff : 'a sigma -> Declareops.side_effects
-val sig_sig : 'a sigma -> evar_map
-val emit_side_effects : Declareops.side_effects -> 'a sigma -> 'a sigma
-
-(*********************************************************
-   Failure explanation *)
+(** Partially constructed constrs. *)
 
 type unsolvability_explanation = SeveralInstancesFound of int
+(** Failure explanation. *)
 
-(********************************************************************
-   debug pretty-printer: *)
+(** {5 Debug pretty-printers} *)
 
 val pr_evar_info : evar_info -> Pp.std_ppcmds
 val pr_evar_map_constraints : evar_map -> Pp.std_ppcmds
 val pr_evar_map : int option -> evar_map -> Pp.std_ppcmds
 val pr_metaset : Metaset.t -> Pp.std_ppcmds
 
+(** {5 Deprecated functions} *)
 
-(*** /!\Deprecated /!\ **
-   create an [evar_map] with empty meta map: *)
 val create_evar_defs      : evar_map -> evar_map
+(** Create an [evar_map] with empty meta map: *)
+
 val create_goal_evar_defs : evar_map -> evar_map
+
 val subst_evar_map : substitution -> evar_map -> evar_map
-(*** /Deprecaded ***)