adds constructs to handle notations in patterns

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

3 files changed, 47 insertions, 16 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 1a23883ae..5132c94aa 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -154,7 +154,7 @@ and ct_COMMAND =
   | CT_unsethyp
   | CT_unsetundo
   | CT_user_vernac of ct_ID * ct_VARG_LIST
-  | CT_variable of ct_VAR * ct_BINDER_LIST
+  | CT_variable of ct_VAR * ct_BINDER_NE_LIST
   | CT_write_module of ct_ID * ct_STRING_OPT
 and ct_COMMAND_LIST =
     CT_command_list of ct_COMMAND * ct_COMMAND list
@@ -226,6 +226,7 @@ and ct_FIX_TAC_LIST =
 and ct_FORMULA =
     CT_coerce_BINARY_to_FORMULA of ct_BINARY
   | CT_coerce_ID_to_FORMULA of ct_ID
+  | CT_coerce_NUM_to_FORMULA of ct_NUM
   | CT_coerce_SORT_TYPE_to_FORMULA of ct_SORT_TYPE
   | CT_coerce_TYPED_FORMULA_to_FORMULA of ct_TYPED_FORMULA
   | CT_appc of ct_FORMULA * ct_FORMULA_NE_LIST
@@ -238,7 +239,6 @@ and ct_FORMULA =
   | CT_fixc of ct_ID * ct_FIX_BINDER_LIST
   | CT_if of ct_FORMULA_OPT * ct_FORMULA * ct_FORMULA * ct_FORMULA
   | CT_inductive_let of ct_FORMULA_OPT * ct_ID_OPT_NE_LIST * ct_FORMULA * ct_FORMULA
-  | CT_int_encapsulator of string
   | CT_lambdac of ct_BINDER_NE_LIST * ct_FORMULA
   | CT_letin of ct_DEF * ct_FORMULA
   | CT_notation of ct_STRING * ct_FORMULA_LIST
@@ -362,8 +362,13 @@ and ct_MATCHED_FORMULA_NE_LIST =
     CT_matched_formula_ne_list of ct_MATCHED_FORMULA * ct_MATCHED_FORMULA list
 and ct_MATCH_PATTERN =
     CT_coerce_ID_OPT_to_MATCH_PATTERN of ct_ID_OPT
+  | CT_coerce_NUM_to_MATCH_PATTERN of ct_NUM
   | CT_pattern_app of ct_MATCH_PATTERN * ct_MATCH_PATTERN_NE_LIST
   | CT_pattern_as of ct_MATCH_PATTERN * ct_ID_OPT
+  | CT_pattern_delimitors of ct_NUM_TYPE * ct_MATCH_PATTERN
+  | CT_pattern_notation of ct_STRING * ct_MATCH_PATTERN_LIST
+and ct_MATCH_PATTERN_LIST =
+    CT_match_pattern_list of ct_MATCH_PATTERN list
 and ct_MATCH_PATTERN_NE_LIST =
     CT_match_pattern_ne_list of ct_MATCH_PATTERN * ct_MATCH_PATTERN list
 and ct_MATCH_TAC_RULE =
@@ -376,6 +381,8 @@ and ct_NATURAL_FEATURE =
   | CT_nat_transparent
 and ct_NONE =
     CT_none
+and ct_NUM =
+    CT_int_encapsulator of string
 and ct_NUM_TYPE =
     CT_num_type of string
 and ct_OMEGA_FEATURE =
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 31134653c..1edafcfad 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -434,7 +434,7 @@ and fCOMMAND = function
    fNODE "user_vernac" 2
 | CT_variable(x1, x2) ->
    fVAR x1;
-   fBINDER_LIST x2;
+   fBINDER_NE_LIST x2;
    fNODE "variable" 2
 | CT_write_module(x1, x2) ->
    fID x1;
@@ -573,6 +573,7 @@ and fFIX_TAC_LIST = function
 and fFORMULA = function
 | CT_coerce_BINARY_to_FORMULA x -> fBINARY x
 | CT_coerce_ID_to_FORMULA x -> fID x
+| CT_coerce_NUM_to_FORMULA x -> fNUM x
 | CT_coerce_SORT_TYPE_to_FORMULA x -> fSORT_TYPE x
 | CT_coerce_TYPED_FORMULA_to_FORMULA x -> fTYPED_FORMULA x
 | CT_appc(x1, x2) ->
@@ -619,9 +620,7 @@ and fFORMULA = function
    fFORMULA x3;
    fFORMULA x4;
    fNODE "inductive_let" 4
-| CT_int_encapsulator x -> fATOM "int_encapsulator";
-   (f_atom_string x);
-   print_string "\n"| CT_lambdac(x1, x2) ->
+| CT_lambdac(x1, x2) ->
    fBINDER_NE_LIST x1;
    fFORMULA x2;
    fNODE "lambdac" 2
@@ -845,6 +844,7 @@ and fMATCHED_FORMULA_NE_LIST = function
    fNODE "matched_formula_ne_list" (1 + (List.length l))
 and fMATCH_PATTERN = function
 | CT_coerce_ID_OPT_to_MATCH_PATTERN x -> fID_OPT x
+| CT_coerce_NUM_to_MATCH_PATTERN x -> fNUM x
 | CT_pattern_app(x1, x2) ->
    fMATCH_PATTERN x1;
    fMATCH_PATTERN_NE_LIST x2;
@@ -853,6 +853,18 @@ and fMATCH_PATTERN = function
    fMATCH_PATTERN x1;
    fID_OPT x2;
    fNODE "pattern_as" 2
+| CT_pattern_delimitors(x1, x2) ->
+   fNUM_TYPE x1;
+   fMATCH_PATTERN x2;
+   fNODE "pattern_delimitors" 2
+| CT_pattern_notation(x1, x2) ->
+   fSTRING x1;
+   fMATCH_PATTERN_LIST x2;
+   fNODE "pattern_notation" 2
+and fMATCH_PATTERN_LIST = function
+| CT_match_pattern_list l ->
+   (List.iter fMATCH_PATTERN l);
+   fNODE "match_pattern_list" (List.length l)
 and fMATCH_PATTERN_NE_LIST = function
 | CT_match_pattern_ne_list(x,l) ->
    fMATCH_PATTERN x;
@@ -874,7 +886,10 @@ and fNATURAL_FEATURE = function
 | CT_nat_transparent -> fNODE "nat_transparent" 0
 and fNONE = function
 | CT_none -> fNODE "none" 0
-and fNUM_TYPE = function
+and fNUM = function
+| CT_int_encapsulator x -> fATOM "int_encapsulator";
+   (f_atom_string x);
+   print_string "\n"and fNUM_TYPE = function
 | CT_num_type x -> fATOM "num_type";
    (f_atom_string x);
    print_string "\n"and fOMEGA_FEATURE = function
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 265975dc0..ee4e5a654 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -263,9 +263,15 @@ let rec xlate_match_pattern =
     | CPatAlias  (_,  pattern, id) ->
      CT_pattern_as
       (xlate_match_pattern pattern, CT_coerce_ID_to_ID_OPT (xlate_ident id))
-    | CPatDelimiters(_, _, _) -> xlate_error "CPatDelimitors"
-    | CPatNumeral(_,_) -> xlate_error "CPatNumeral"
-    | CPatNotation _ -> xlate_error "CPatNotation";;
+    | CPatDelimiters(_, key, p) -> 
+	CT_pattern_delimitors(CT_num_type key, xlate_match_pattern p)
+    | CPatNumeral(_,n) ->
+ 	CT_coerce_NUM_to_MATCH_PATTERN
+	  (CT_int_encapsulator(Bignat.bigint_to_string n))
+    | CPatNotation(_, s, l) -> 
+	CT_pattern_notation(CT_string s,
+			    CT_match_pattern_list(List.map xlate_match_pattern l))
+;;
 
 
 let xlate_id_opt_aux = function
@@ -360,12 +366,14 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
 		  CT_formula_list(List.map xlate_formula l))
    | CSort(_, s) -> CT_coerce_SORT_TYPE_to_FORMULA(xlate_sort s)
    | CNotation(_, s, l) -> notation_to_formula s (List.map xlate_formula l)
-   | CNumeral(_, i) -> CT_int_encapsulator(Bignat.bigint_to_string i)
+   | CNumeral(_, i) -> 
+       CT_coerce_NUM_to_FORMULA(CT_int_encapsulator(Bignat.bigint_to_string i))
    | CHole _ -> CT_existvarc 
 (* I assume CDynamic has been inserted to make free form extension of
    the language possible, but this would go agains the logic of pcoq anyway. *)
    | CDynamic (_, _) -> assert false
-   | CDelimiters (_, key, num) -> CT_num_encapsulator(CT_num_type key , xlate_formula  num)
+   | CDelimiters (_, key, num) -> 
+	 CT_num_encapsulator(CT_num_type key , xlate_formula  num)
    | CCast (_, e, t) -> 
        CT_coerce_TYPED_FORMULA_to_FORMULA
 	 (CT_typed_formula(xlate_formula e, xlate_formula t))
@@ -1330,9 +1338,9 @@ let cvt_vernac_binder = function
          xlate_formula c)
   | ([],_) -> xlate_error "Empty list of vernac binder"
 
-let cvt_vernac_binders args =
-  CT_binder_list(List.map cvt_vernac_binder args)
-
+let cvt_vernac_binders = function
+    a::args -> CT_binder_ne_list(cvt_vernac_binder a, List.map cvt_vernac_binder args)
+  | [] -> assert false;;
 
 
 let xlate_comment = function
@@ -1340,7 +1348,8 @@ let xlate_comment = function
   | CommentString s -> CT_coerce_ID_OR_STRING_to_SCOMMENT_CONTENT
       (CT_coerce_STRING_to_ID_OR_STRING(CT_string s))
   | CommentInt n ->
-      CT_coerce_FORMULA_to_SCOMMENT_CONTENT(CT_int_encapsulator (string_of_int n));;
+      CT_coerce_FORMULA_to_SCOMMENT_CONTENT
+	(CT_coerce_NUM_to_FORMULA(CT_int_encapsulator (string_of_int n)));;
 
 let xlate_vernac =
  function