More comments in Genarg.

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

2 files changed, 107 insertions, 73 deletions

diff --git a/interp/genarg.ml b/interp/genarg.ml
index 5d61de508..eb5287b32 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -81,12 +81,15 @@ type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type
 
 (* Dynamics but tagged by a type expression *)
 
-type 'a generic_argument = argument_type * Obj.t
-
 type rlevel
 type glevel
 type tlevel
 
+type 'a generic_argument = argument_type * Obj.t
+type raw_generic_argument = rlevel generic_argument
+type glob_generic_argument = glevel generic_argument
+type typed_generic_argument = tlevel generic_argument
+
 let rawwit t = t
 let glbwit t = t
 let topwit t = t
@@ -203,6 +206,9 @@ let in_generic t x = (t, Obj.repr x)
 let dyntab = ref ([] : (string * glevel generic_argument option) list)
 
 type ('a,'b) abstract_argument_type = argument_type
+type 'a raw_abstract_argument_type = ('a,rlevel) abstract_argument_type
+type 'a glob_abstract_argument_type = ('a,glevel) abstract_argument_type
+type 'a typed_abstract_argument_type = ('a,tlevel) abstract_argument_type
 
 let create_arg v s =
   if List.mem_assoc s !dyntab then
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 0f6ffddd9..7f9d39907 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -20,6 +20,7 @@ open Term
 open Evd
 open Misctypes
 
+(** FIXME: nothing to do there. *)
 val loc_of_or_by_notation : ('a -> Loc.t) -> 'a or_by_notation -> Loc.t
 
 (** In globalize tactics, we need to keep the initial [constr_expr] to recompute
@@ -92,7 +93,7 @@ ExtraArgType of string         '_a                      '_b
 {% \end{%}verbatim{% }%}
 *)
 
-(** {5 Base type combinators} *)
+(** {5 Generic types} *)
 
 type ('raw, 'glob, 'top) genarg_type
 (** Generic types. ['raw] is the OCaml lowest level, ['glob] is the globalized
@@ -105,68 +106,6 @@ val create_arg : 'raw option -> string -> ('raw, 'glob, 'top) genarg_type
 (** Create a new generic type of argument: force to associate
    unique ML types at each of the three levels. *)
 
-(** {6 Type constructors} *)
-
-val wit_bool : bool uniform_genarg_type
-
-val wit_int : int uniform_genarg_type
-
-val wit_int_or_var : int or_var uniform_genarg_type
-
-val wit_string : string uniform_genarg_type
-
-val wit_pre_ident : string uniform_genarg_type
-
-val wit_intro_pattern : intro_pattern_expr located uniform_genarg_type
-
-val wit_ident : Id.t uniform_genarg_type
-
-val wit_pattern_ident : Id.t uniform_genarg_type
-
-val wit_ident_gen : bool -> Id.t uniform_genarg_type
-
-val wit_var : (Id.t located, Id.t located, Id.t) genarg_type
-
-val wit_ref : (reference, global_reference located or_var, global_reference) genarg_type
-
-val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
-
-val wit_sort : (glob_sort, glob_sort, sorts) genarg_type
-
-val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type
-
-val wit_constr_may_eval :
-  ((constr_expr,reference or_by_notation,constr_expr) may_eval,
-  (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) may_eval,
-  constr) genarg_type
-
-val wit_open_constr_gen : bool -> (open_constr_expr, open_glob_constr, open_constr) genarg_type
-
-val wit_open_constr : (open_constr_expr, open_glob_constr, open_constr) genarg_type
-
-val wit_casted_open_constr : (open_constr_expr, open_glob_constr, open_constr) genarg_type
-
-val wit_constr_with_bindings :
-  (constr_expr with_bindings,
-  glob_constr_and_expr with_bindings,
-  constr with_bindings sigma) genarg_type
-
-val wit_bindings :
-  (constr_expr bindings,
-  glob_constr_and_expr bindings,
-  constr bindings sigma) genarg_type
-
-val wit_red_expr :
-  ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
-  (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
-  (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
-
-val wit_list0 : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type
-val wit_list1 : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type
-val wit_opt : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type
-val wit_pair : ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type ->
-  ('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type
-
 (** {5 Specialized types} *)
 
 (** All of [rlevel], [glevel] and [tlevel] must be non convertible
@@ -183,13 +122,24 @@ type tlevel
 type ('a, 'co) abstract_argument_type
 (** Type at level ['co] represented by an OCaml value of type ['a]. *)
 
-val rawwit : ('a, 'b, 'c) genarg_type -> ('a, 'co) abstract_argument_type
+type 'a raw_abstract_argument_type = ('a, rlevel) abstract_argument_type
+(** Specialized type at raw level. *)
+
+type 'a glob_abstract_argument_type = ('a, glevel) abstract_argument_type
+(** Specialized type at globalized level. *)
+
+type 'a typed_abstract_argument_type = ('a, tlevel) abstract_argument_type
+(** Specialized type at internalized level. *)
+
+(** {6 Projections} *)
+
+val rawwit : ('a, 'b, 'c) genarg_type -> ('a, rlevel) abstract_argument_type
 (** Projection on the raw type constructor. *)
 
-val glbwit : ('a, 'b, 'c) genarg_type -> ('b, 'co) abstract_argument_type
+val glbwit : ('a, 'b, 'c) genarg_type -> ('b, glevel) abstract_argument_type
 (** Projection on the globalized type constructor. *)
 
-val topwit : ('a, 'b, 'c) genarg_type -> ('c, 'co) abstract_argument_type
+val topwit : ('a, 'b, 'c) genarg_type -> ('c, tlevel) abstract_argument_type
 (** Projection on the internalized type constructor. *)
 
 (** {5 Generic arguments} *)
@@ -198,6 +148,19 @@ type 'a generic_argument
 (** A inhabitant of ['level generic_argument] is a inhabitant of some type at
     level ['level], together with the representation of this type. *)
 
+type raw_generic_argument = rlevel generic_argument
+type glob_generic_argument = glevel generic_argument
+type typed_generic_argument = tlevel generic_argument
+
+(** {6 Constructors} *)
+
+val in_gen : ('a, 'co) abstract_argument_type -> 'a -> 'co generic_argument
+(** [in_gen t x] embeds an argument of type [t] into a generic argument. *)
+
+val out_gen : ('a, 'co) abstract_argument_type -> 'co generic_argument -> 'a
+(** [out_gen t x] recovers an argument of type [t] from a generic argument. It
+    fails if [x] has not the right dynamic type. *)
+
 (** {6 Manipulation of generic arguments}
 
 Those functions fail if they are applied to an argument which has not the right
@@ -233,6 +196,8 @@ val app_pair :
       ('a generic_argument -> 'b generic_argument)
    -> 'a generic_argument -> 'b generic_argument
 
+(** {6 Type reification} *)
+
 type argument_type =
   (** Basic types *)
   | BoolArgType
@@ -263,12 +228,75 @@ val argument_type_eq : argument_type -> argument_type -> bool
 
 val genarg_tag : 'a generic_argument -> argument_type
 
-val unquote : ('a,'co) abstract_argument_type -> argument_type
+val unquote : ('a, 'co) abstract_argument_type -> argument_type
+
+(** {5 Basic generic type constructors} *)
+
+(** {6 Ground types} *)
+
+val wit_bool : bool uniform_genarg_type
+
+val wit_int : int uniform_genarg_type
+
+val wit_int_or_var : int or_var uniform_genarg_type
+
+val wit_string : string uniform_genarg_type
+
+val wit_pre_ident : string uniform_genarg_type
+
+val wit_intro_pattern : intro_pattern_expr located uniform_genarg_type
+
+val wit_ident : Id.t uniform_genarg_type
+
+val wit_pattern_ident : Id.t uniform_genarg_type
+
+val wit_ident_gen : bool -> Id.t uniform_genarg_type
+
+val wit_var : (Id.t located, Id.t located, Id.t) genarg_type
+
+val wit_ref : (reference, global_reference located or_var, global_reference) genarg_type
+
+val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
+
+val wit_sort : (glob_sort, glob_sort, sorts) genarg_type
+
+val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type
+
+val wit_constr_may_eval :
+  ((constr_expr,reference or_by_notation,constr_expr) may_eval,
+  (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) may_eval,
+  constr) genarg_type
+
+val wit_open_constr_gen : bool -> (open_constr_expr, open_glob_constr, open_constr) genarg_type
+
+val wit_open_constr : (open_constr_expr, open_glob_constr, open_constr) genarg_type
+
+val wit_casted_open_constr : (open_constr_expr, open_glob_constr, open_constr) genarg_type
+
+val wit_constr_with_bindings :
+  (constr_expr with_bindings,
+  glob_constr_and_expr with_bindings,
+  constr with_bindings sigma) genarg_type
+
+val wit_bindings :
+  (constr_expr bindings,
+  glob_constr_and_expr bindings,
+  constr bindings sigma) genarg_type
+
+val wit_red_expr :
+  ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
+  (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
+  (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
+
+(** {6 Parameterized types} *)
+
+val wit_list0 : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type
+val wit_list1 : ('a, 'b, 'c) genarg_type -> ('a list, 'b list, 'c list) genarg_type
+val wit_opt : ('a, 'b, 'c) genarg_type -> ('a option, 'b option, 'c option) genarg_type
+val wit_pair : ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type ->
+  ('a1 * 'a2, 'b1 * 'b2, 'c1 * 'c2) genarg_type
 
-val in_gen :
-  ('a,'co) abstract_argument_type -> 'a -> 'co generic_argument
-val out_gen :
-  ('a,'co) abstract_argument_type -> 'co generic_argument -> 'a
+(** {5 Magic used by the parser} *)
 
 (** [in_generic] is used in combination with camlp4 [Gramext.action] magic