Suppression du type 'tac dans les abstract_argument_type: devenu inutile

suite à l'adoption du modèle rlevel,glevel,tlevel et au passage des 
wit_tactic en types créés dynamiquement (révisions 8917 et 8926).


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

2 files changed, 126 insertions, 113 deletions

diff --git a/interp/genarg.ml b/interp/genarg.ml
index e5713a6e28..303278f18d 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -48,7 +48,7 @@ type rawconstr_and_expr = rawconstr * constr_expr option
 
 (* Dynamics but tagged by a type expression *)
 
-type ('a,'b) generic_argument = argument_type * Obj.t
+type 'a generic_argument = argument_type * Obj.t
 
 let dyntab = ref ([] : string list)
 
@@ -56,7 +56,7 @@ type rlevel = constr_expr
 type glevel = rawconstr_and_expr
 type tlevel = constr
 
-type ('a,'b,'c) abstract_argument_type = argument_type
+type ('a,'b) abstract_argument_type = argument_type
 
 let create_arg s =
   if List.mem s !dyntab then
diff --git a/interp/genarg.mli b/interp/genarg.mli
index d2aa750cc5..3530bd27ce 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -40,21 +40,34 @@ val pr_case_intro_pattern : case_intro_pattern_expr -> Pp.std_ppcmds
 (* The route of a generic argument, from parsing to evaluation
 
 \begin{verbatim}
-              parsing        in_raw                           out_raw
-    char stream ----> rawtype ----> rawconstr generic_argument ---->
-                                                                   |
-                                                                   | interp
-                                                                   V
-                          type  <---- constr generic_argument  <----
-                                  out                            in
+             parsing        in_raw                              out_raw
+   char stream ----> rawtype ----> constr_expr generic_argument --------|
+                          encapsulation                         decaps  |
+                                                                        |
+                                                                        V
+                                                                     rawtype
+                                                                        |
+                                                         globalization  |
+                                                                        V
+                                                                    glob_type
+                                                                        |
+                                                                 encaps |
+                                                                in_glob |
+                                                                        V
+                                                     rawconstr generic_argument
+                                                                        |
+        out                          in                        out_glob |
+  type <--- constr generic_argument <---- type <------ rawtype <--------|
+    |  decaps                       encaps      interp           decaps
+    |
+    V
+effective use
 \end{verbatim}
 
-To distinguish between the uninterpreted (raw) and the interpreted
-worlds, we annotate the type [generic_argument] by a phantom argument
-which is either [constr_expr] or [constr] (actually we add also a second
-argument [raw_tactic_expr] and [tactic], but this is only for technical
-reasons, because these types are undefined at the type of compilation
-of [Genarg]).
+To distinguish between the uninterpreted (raw), globalized and 
+interpreted worlds, we annotate the type [generic_argument] by a
+phantom argument which is either [constr_expr], [rawconstr] or
+[constr].
 
 Transformation for each type :
 \begin{verbatim}
@@ -84,8 +97,8 @@ ExtraArgType of string         '_a                      '_b
 
 (* All of [rlevel], [glevel] and [tlevel] must be non convertible 
    to ensure the injectivity of the type inference from type
-   [('co,'ta) generic_argument] to [('a,'co,'ta) abstract_argument_type]
-   is injective; this guarantees that, for 'b fixed, the type of
+   ['co generic_argument] to [('a,'co) abstract_argument_type];
+   this guarantees that, for 'co fixed, the type of
    out_gen is monomorphic over 'a, hence type-safe 
 *)
 
@@ -93,138 +106,137 @@ type rlevel = constr_expr
 type glevel = rawconstr_and_expr
 type tlevel = constr
 
-type ('a,'co,'ta) abstract_argument_type
+type ('a,'co) abstract_argument_type
 
-val rawwit_bool : (bool,rlevel,'ta) abstract_argument_type
-val globwit_bool : (bool,glevel,'ta) abstract_argument_type
-val wit_bool : (bool,tlevel,'ta) abstract_argument_type
+val rawwit_bool : (bool,rlevel) abstract_argument_type
+val globwit_bool : (bool,glevel) abstract_argument_type
+val wit_bool : (bool,tlevel) abstract_argument_type
 
-val rawwit_int : (int,rlevel,'ta) abstract_argument_type
-val globwit_int : (int,glevel,'ta) abstract_argument_type
-val wit_int : (int,tlevel,'ta) abstract_argument_type
+val rawwit_int : (int,rlevel) abstract_argument_type
+val globwit_int : (int,glevel) abstract_argument_type
+val wit_int : (int,tlevel) abstract_argument_type
 
-val rawwit_int_or_var : (int or_var,rlevel,'ta) abstract_argument_type
-val globwit_int_or_var : (int or_var,glevel,'ta) abstract_argument_type
-val wit_int_or_var : (int or_var,tlevel,'ta) abstract_argument_type
+val rawwit_int_or_var : (int or_var,rlevel) abstract_argument_type
+val globwit_int_or_var : (int or_var,glevel) abstract_argument_type
+val wit_int_or_var : (int or_var,tlevel) abstract_argument_type
 
-val rawwit_string : (string,rlevel,'ta) abstract_argument_type
-val globwit_string : (string,glevel,'ta) abstract_argument_type
-val wit_string : (string,tlevel,'ta) abstract_argument_type
+val rawwit_string : (string,rlevel) abstract_argument_type
+val globwit_string : (string,glevel) abstract_argument_type
+val wit_string : (string,tlevel) abstract_argument_type
 
-val rawwit_pre_ident : (string,rlevel,'ta) abstract_argument_type
-val globwit_pre_ident : (string,glevel,'ta) abstract_argument_type
-val wit_pre_ident : (string,tlevel,'ta) abstract_argument_type
+val rawwit_pre_ident : (string,rlevel) abstract_argument_type
+val globwit_pre_ident : (string,glevel) abstract_argument_type
+val wit_pre_ident : (string,tlevel) abstract_argument_type
 
-val rawwit_intro_pattern : (intro_pattern_expr,rlevel,'ta) abstract_argument_type
-val globwit_intro_pattern : (intro_pattern_expr,glevel,'ta) abstract_argument_type
-val wit_intro_pattern : (intro_pattern_expr,tlevel,'ta) abstract_argument_type
+val rawwit_intro_pattern : (intro_pattern_expr,rlevel) abstract_argument_type
+val globwit_intro_pattern : (intro_pattern_expr,glevel) abstract_argument_type
+val wit_intro_pattern : (intro_pattern_expr,tlevel) abstract_argument_type
 
-val rawwit_ident : (identifier,rlevel,'ta) abstract_argument_type
-val globwit_ident : (identifier,glevel,'ta) abstract_argument_type
-val wit_ident : (identifier,tlevel,'ta) abstract_argument_type
+val rawwit_ident : (identifier,rlevel) abstract_argument_type
+val globwit_ident : (identifier,glevel) abstract_argument_type
+val wit_ident : (identifier,tlevel) abstract_argument_type
 
-val rawwit_var : (identifier located,rlevel,'ta) abstract_argument_type
-val globwit_var : (identifier located,glevel,'ta) abstract_argument_type
-val wit_var : (identifier,tlevel,'ta) abstract_argument_type
+val rawwit_var : (identifier located,rlevel) abstract_argument_type
+val globwit_var : (identifier located,glevel) abstract_argument_type
+val wit_var : (identifier,tlevel) abstract_argument_type
 
-val rawwit_ref : (reference,rlevel,'ta) abstract_argument_type
-val globwit_ref : (global_reference located or_var,glevel,'ta) abstract_argument_type
-val wit_ref : (global_reference,tlevel,'ta) abstract_argument_type
+val rawwit_ref : (reference,rlevel) abstract_argument_type
+val globwit_ref : (global_reference located or_var,glevel) abstract_argument_type
+val wit_ref : (global_reference,tlevel) abstract_argument_type
 
-val rawwit_quant_hyp : (quantified_hypothesis,rlevel,'ta) abstract_argument_type
-val globwit_quant_hyp : (quantified_hypothesis,glevel,'ta) abstract_argument_type
-val wit_quant_hyp : (quantified_hypothesis,tlevel,'ta) abstract_argument_type
+val rawwit_quant_hyp : (quantified_hypothesis,rlevel) abstract_argument_type
+val globwit_quant_hyp : (quantified_hypothesis,glevel) abstract_argument_type
+val wit_quant_hyp : (quantified_hypothesis,tlevel) abstract_argument_type
 
-val rawwit_sort : (rawsort,rlevel,'ta) abstract_argument_type
-val globwit_sort : (rawsort,glevel,'ta) abstract_argument_type
-val wit_sort : (sorts,tlevel,'ta) abstract_argument_type
+val rawwit_sort : (rawsort,rlevel) abstract_argument_type
+val globwit_sort : (rawsort,glevel) abstract_argument_type
+val wit_sort : (sorts,tlevel) abstract_argument_type
 
-val rawwit_constr : (constr_expr,rlevel,'ta) abstract_argument_type
-val globwit_constr : (rawconstr_and_expr,glevel,'ta) abstract_argument_type
-val wit_constr : (constr,tlevel,'ta) abstract_argument_type
+val rawwit_constr : (constr_expr,rlevel) abstract_argument_type
+val globwit_constr : (rawconstr_and_expr,glevel) abstract_argument_type
+val wit_constr : (constr,tlevel) abstract_argument_type
 
-val rawwit_constr_may_eval : ((constr_expr,reference) may_eval,rlevel,'ta) abstract_argument_type
-val globwit_constr_may_eval : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) may_eval,glevel,'ta) abstract_argument_type
-val wit_constr_may_eval : (constr,tlevel,'ta) abstract_argument_type
+val rawwit_constr_may_eval : ((constr_expr,reference) may_eval,rlevel) abstract_argument_type
+val globwit_constr_may_eval : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) may_eval,glevel) abstract_argument_type
+val wit_constr_may_eval : (constr,tlevel) abstract_argument_type
 
-val rawwit_open_constr_gen : bool -> (open_constr_expr,rlevel,'ta) abstract_argument_type
-val globwit_open_constr_gen : bool -> (open_rawconstr,glevel,'ta) abstract_argument_type
-val wit_open_constr_gen : bool -> (open_constr,tlevel,'ta) abstract_argument_type
+val rawwit_open_constr_gen : bool -> (open_constr_expr,rlevel) abstract_argument_type
+val globwit_open_constr_gen : bool -> (open_rawconstr,glevel) abstract_argument_type
+val wit_open_constr_gen : bool -> (open_constr,tlevel) abstract_argument_type
 
-val rawwit_open_constr : (open_constr_expr,rlevel,'ta) abstract_argument_type
-val globwit_open_constr : (open_rawconstr,glevel,'ta) abstract_argument_type
-val wit_open_constr : (open_constr,tlevel,'ta) abstract_argument_type
+val rawwit_open_constr : (open_constr_expr,rlevel) abstract_argument_type
+val globwit_open_constr : (open_rawconstr,glevel) abstract_argument_type
+val wit_open_constr : (open_constr,tlevel) abstract_argument_type
 
-val rawwit_casted_open_constr : (open_constr_expr,rlevel,'ta) abstract_argument_type
-val globwit_casted_open_constr : (open_rawconstr,glevel,'ta) abstract_argument_type
-val wit_casted_open_constr : (open_constr,tlevel,'ta) abstract_argument_type
+val rawwit_casted_open_constr : (open_constr_expr,rlevel) abstract_argument_type
+val globwit_casted_open_constr : (open_rawconstr,glevel) abstract_argument_type
+val wit_casted_open_constr : (open_constr,tlevel) abstract_argument_type
 
-val rawwit_constr_with_bindings : (constr_expr with_bindings,rlevel,'ta) abstract_argument_type
-val globwit_constr_with_bindings : (rawconstr_and_expr with_bindings,glevel,'ta) abstract_argument_type
-val wit_constr_with_bindings : (constr with_bindings,tlevel,'ta) abstract_argument_type
+val rawwit_constr_with_bindings : (constr_expr with_bindings,rlevel) abstract_argument_type
+val globwit_constr_with_bindings : (rawconstr_and_expr with_bindings,glevel) abstract_argument_type
+val wit_constr_with_bindings : (constr with_bindings,tlevel) abstract_argument_type
 
-val rawwit_bindings : (constr_expr bindings,rlevel,'ta) abstract_argument_type
-val globwit_bindings : (rawconstr_and_expr bindings,glevel,'ta) abstract_argument_type
-val wit_bindings : (constr bindings,tlevel,'ta) abstract_argument_type
+val rawwit_bindings : (constr_expr bindings,rlevel) abstract_argument_type
+val globwit_bindings : (rawconstr_and_expr bindings,glevel) abstract_argument_type
+val wit_bindings : (constr bindings,tlevel) abstract_argument_type
 
-val rawwit_red_expr : ((constr_expr,reference) red_expr_gen,rlevel,'ta) abstract_argument_type
-val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) red_expr_gen,glevel,'ta) abstract_argument_type
-val wit_red_expr : ((constr,evaluable_global_reference) red_expr_gen,tlevel,'ta) abstract_argument_type
+val rawwit_red_expr : ((constr_expr,reference) red_expr_gen,rlevel) abstract_argument_type
+val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) red_expr_gen,glevel) abstract_argument_type
+val wit_red_expr : ((constr,evaluable_global_reference) red_expr_gen,tlevel) abstract_argument_type
 
 val wit_list0 :
-  ('a,'co,'ta) abstract_argument_type -> ('a list,'co,'ta) abstract_argument_type
+  ('a,'co) abstract_argument_type -> ('a list,'co) abstract_argument_type
 
 val wit_list1 :
-  ('a,'co,'ta) abstract_argument_type -> ('a list,'co,'ta) abstract_argument_type
+  ('a,'co) abstract_argument_type -> ('a list,'co) abstract_argument_type
 
 val wit_opt :
-  ('a,'co,'ta) abstract_argument_type -> ('a option,'co,'ta) abstract_argument_type
+  ('a,'co) abstract_argument_type -> ('a option,'co) abstract_argument_type
 
 val wit_pair :
-  ('a,'co,'ta) abstract_argument_type ->
-  ('b,'co,'ta) abstract_argument_type ->
-      ('a * 'b,'co,'ta) abstract_argument_type
+  ('a,'co) abstract_argument_type ->
+  ('b,'co) abstract_argument_type ->
+      ('a * 'b,'co) abstract_argument_type
 
 (* ['a generic_argument] = (Sigma t:type. t[[constr/'a]]) *)
-type ('a,'b) generic_argument
+type 'a generic_argument
 
 val fold_list0 : 
- (('a,'b) generic_argument -> 'c -> 'c) -> ('a,'b) generic_argument -> 'c -> 'c
+ ('a generic_argument -> 'c -> 'c) -> 'a generic_argument -> 'c -> 'c
 
 val fold_list1 : 
- (('a,'b) generic_argument -> 'c -> 'c) -> ('a,'b) generic_argument -> 'c -> 'c
+ ('a generic_argument -> 'c -> 'c) -> 'a generic_argument -> 'c -> 'c
 
 val fold_opt :
- (('a,'b) generic_argument -> 'c) -> 'c -> ('a,'b) generic_argument -> 'c
+ ('a generic_argument -> 'c) -> 'c -> 'a generic_argument -> 'c
 
 val fold_pair :
- (('a,'b) generic_argument -> ('a,'b) generic_argument -> 'c) -> 
-      ('a,'b) generic_argument -> 'c
+ ('a generic_argument -> 'a generic_argument -> 'c) -> 
+      'a generic_argument -> 'c
 
 (* [app_list0] fails if applied to an argument not of tag [List0 t]
     for some [t]; it's the responsability of the caller to ensure it *)
 
-val app_list0 : (('a,'b) generic_argument -> ('c,'d) generic_argument) -> 
-('a,'b) generic_argument -> ('c,'d) generic_argument
+val app_list0 : ('a generic_argument -> 'b generic_argument) -> 
+'a generic_argument -> 'b generic_argument
 
-val app_list1 : (('a,'b) generic_argument -> ('c,'d) generic_argument) -> 
-('a,'b) generic_argument -> ('c,'d) generic_argument
+val app_list1 : ('a generic_argument -> 'b generic_argument) -> 
+'a generic_argument -> 'b generic_argument
 
-val app_opt : (('a,'b) generic_argument -> ('c,'d) generic_argument) -> 
-('a,'b) generic_argument -> ('c,'d) generic_argument
+val app_opt : ('a generic_argument -> 'b generic_argument) -> 
+'a generic_argument -> 'b generic_argument
 
 val app_pair :
-  (('a,'b) generic_argument -> ('c,'d) generic_argument) ->
-      (('a,'b) generic_argument -> ('c,'d) generic_argument)
-   -> ('a,'b) generic_argument -> ('c,'d) generic_argument
+  ('a generic_argument -> 'b generic_argument) ->
+      ('a generic_argument -> 'b generic_argument)
+   -> 'a generic_argument -> 'b generic_argument
 
-(* Manque l'ordre supérieur, on aimerait ('co,'ta) 'a; manque aussi le
-   polymorphism, on aimerait que 'b et 'c restent polymorphes à l'appel
-   de create *)
+(* create a new generic type of argument: force to associate
+   unique ML types at each of the three levels *)
 val create_arg : string ->
-      ('a,tlevel,'ta) abstract_argument_type
-      * ('globa,glevel,'globta) abstract_argument_type
-      * ('rawa,rlevel,'rawta) abstract_argument_type
+      ('a,tlevel) abstract_argument_type
+      * ('globa,glevel) abstract_argument_type
+      * ('rawa,rlevel) abstract_argument_type
 
 val exists_argtype : string -> bool
 
@@ -254,15 +266,21 @@ type argument_type =
   | PairArgType of argument_type * argument_type
   | ExtraArgType of string
 
-val genarg_tag : ('a,'b) generic_argument -> argument_type
+val genarg_tag : 'a generic_argument -> argument_type
 
-val unquote : ('a,'co,'ta) abstract_argument_type -> argument_type
+val unquote : ('a,'co) abstract_argument_type -> argument_type
 
-(* We'd like
+val in_gen :
+  ('a,'co) abstract_argument_type -> 'a -> 'co generic_argument
+val out_gen :
+  ('a,'co) abstract_argument_type -> 'co generic_argument -> 'a 
+
+
+(* [in_generic] is used in combination with camlp4 [Gramext.action] magic
 
-  [in_generic: !b:type, !a:argument_type -> (f a) -> b generic_argument]
+   [in_generic: !l:type, !a:argument_type -> |a|_l -> 'l generic_argument]
 
-   with f a = b if a is Constr, f a = c if a is Tactic, otherwise f a = |a|
+   where |a|_l is the interpretation of a at level l
 
    [in_generic] is not typable; we replace the second argument by an absurd
    type (with no introduction rule)
@@ -270,9 +288,4 @@ val unquote : ('a,'co,'ta) abstract_argument_type -> argument_type
 type an_arg_of_this_type
 
 val in_generic : 
-  argument_type -> an_arg_of_this_type -> ('a,'b) generic_argument
-
-val in_gen :
-  ('a,'co,'ta) abstract_argument_type -> 'a -> ('co,'ta) generic_argument
-val out_gen :
-  ('a,'co,'ta) abstract_argument_type -> ('co,'ta) generic_argument -> 'a 
+  argument_type -> an_arg_of_this_type -> 'co generic_argument