Généralisation du type ltac Identifier en IntroPattern; prise en compte des IntroPattern au parsing, à l'interprétation, à la traduction

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

2 files changed, 50 insertions, 9 deletions

diff --git a/interp/genarg.ml b/interp/genarg.ml
index 80248f7e5e..4ef21df452 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -8,8 +8,10 @@
 
 (* $Id$ *)
 
+open Pp
 open Util
 open Names
+open Nameops
 open Nametab
 open Rawterm
 open Topconstr
@@ -22,6 +24,7 @@ type argument_type =
   | IntOrVarArgType
   | StringArgType
   | PreIdentArgType
+  | IntroPatternArgType
   | IdentArgType
   | RefArgType
   (* Specific types *)
@@ -61,6 +64,25 @@ let create_arg s =
 
 let exists_argtype s = List.mem s !dyntab
 
+type intro_pattern_expr =
+  | IntroOrAndPattern of case_intro_pattern_expr
+  | IntroWildcard
+  | IntroIdentifier of identifier
+and case_intro_pattern_expr = intro_pattern_expr list list
+
+let rec pr_intro_pattern = function
+  | IntroOrAndPattern pll -> pr_case_intro_pattern pll
+  | IntroWildcard -> str "_"
+  | IntroIdentifier id -> pr_id id
+
+and pr_case_intro_pattern = function
+  | [_::_ as pl] ->
+      str "(" ++ hv 0 (prlist_with_sep pr_coma pr_intro_pattern pl) ++ str ")"
+  | pll ->
+      str "[" ++
+      hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll)
+      ++ str "]"
+
 type open_constr = Evd.evar_map * Term.constr
 type open_constr_expr = constr_expr
 type open_rawconstr = rawconstr_and_expr
@@ -81,14 +103,18 @@ let rawwit_string = StringArgType
 let globwit_string = StringArgType
 let wit_string = StringArgType
 
-let rawwit_ident = IdentArgType
-let globwit_ident = IdentArgType
-let wit_ident = IdentArgType
-
 let rawwit_pre_ident = PreIdentArgType
 let globwit_pre_ident = PreIdentArgType
 let wit_pre_ident = PreIdentArgType
 
+let rawwit_intro_pattern = IntroPatternArgType
+let globwit_intro_pattern = IntroPatternArgType
+let wit_intro_pattern = IntroPatternArgType
+
+let rawwit_ident = IdentArgType
+let globwit_ident = IdentArgType
+let wit_ident = IdentArgType
+
 let rawwit_ref = RefArgType
 let globwit_ref = RefArgType
 let wit_ref = RefArgType
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 23e1b5377d..18f1e33fbc 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -28,6 +28,15 @@ type open_constr = Evd.evar_map * Term.constr
 type open_constr_expr = constr_expr
 type open_rawconstr = rawconstr_and_expr
 
+type intro_pattern_expr =
+  | IntroOrAndPattern of case_intro_pattern_expr
+  | IntroWildcard
+  | IntroIdentifier of identifier
+and case_intro_pattern_expr = intro_pattern_expr list list
+
+val pr_intro_pattern : intro_pattern_expr -> Pp.std_ppcmds
+val pr_case_intro_pattern : case_intro_pattern_expr -> Pp.std_ppcmds
+
 (* The route of a generic argument, from parsing to evaluation
 
               parsing        in_raw                           out_raw
@@ -52,8 +61,9 @@ BoolArgType                    bool                     bool
 IntArgType                     int                      int
 IntOrVarArgType                int or_var               int
 StringArgType                  string (parsed w/ "")    string
-IdentArgType                   identifier               identifier         
 PreIdentArgType                string (parsed w/o "")   string
+IdentArgType                   identifier               identifier         
+IntroPatternArgType            intro_pattern_expr       intro_pattern_expr
 RefArgType                     reference                global_reference
 ConstrArgType                  constr_expr              constr
 ConstrMayEvalArgType           constr_expr may_eval     constr
@@ -85,14 +95,18 @@ val rawwit_string : (string,'co,'ta) abstract_argument_type
 val globwit_string : (string,'co,'ta) abstract_argument_type
 val wit_string : (string,'co,'ta) abstract_argument_type
 
-val rawwit_ident : (identifier,'co,'ta) abstract_argument_type
-val globwit_ident : (identifier,'co,'ta) abstract_argument_type
-val wit_ident : (identifier,'co,'ta) abstract_argument_type
-
 val rawwit_pre_ident : (string,'co,'ta) abstract_argument_type
 val globwit_pre_ident : (string,'co,'ta) abstract_argument_type
 val wit_pre_ident : (string,'co,'ta) abstract_argument_type
 
+val rawwit_intro_pattern : (intro_pattern_expr,'co,'ta) abstract_argument_type
+val globwit_intro_pattern : (intro_pattern_expr,'co,'ta) abstract_argument_type
+val wit_intro_pattern : (intro_pattern_expr,'co,'ta) abstract_argument_type
+
+val rawwit_ident : (identifier,'co,'ta) abstract_argument_type
+val globwit_ident : (identifier,'co,'ta) abstract_argument_type
+val wit_ident : (identifier,'co,'ta) abstract_argument_type
+
 val rawwit_ref : (reference,constr_expr,'ta) abstract_argument_type
 val globwit_ref : (global_reference located or_var,rawconstr_and_expr,'ta) abstract_argument_type
 val wit_ref : (global_reference,constr,'ta) abstract_argument_type
@@ -198,6 +212,7 @@ type argument_type =
   | IntOrVarArgType
   | StringArgType
   | PreIdentArgType
+  | IntroPatternArgType
   | IdentArgType
   | RefArgType
   (* Specific types *)