Prise en compte des délimiteurs dans les motifs de Cases

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

5 files changed, 36 insertions, 19 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 40c2162daa..e1efe655a7 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -192,7 +192,7 @@ let may_allow_variable loc allow_var l =
         str "This reference does not denote a constructor: " ++
         str (string_of_qualid (interp_qualid l)))
 
-let maybe_constructor allow_var env = function
+let maybe_constructor allow_var = function
   | Node(loc,"QUALID",l) ->
       let qid = interp_qualid l in
       (try match extended_locate qid with
@@ -352,16 +352,16 @@ let message_redundant_alias (s1,s2) =
   warning ("Alias variable "^(string_of_id s1)
 	   ^" is merged with "^(string_of_id s2))
 
-let rec ast_to_pattern (_,_,scopes as env) aliases = function
+let rec ast_to_pattern scopes aliases = function
   | Node(_,"PATTAS",[Nvar (loc,s); p]) ->
       let aliases' = merge_aliases aliases (name_of_nvar s) in
-      ast_to_pattern env aliases' p
+      ast_to_pattern scopes aliases' p
 
   | Node(_,"PATTCONSTRUCT", head::((_::_) as pl)) ->
-      (match maybe_constructor false env head with
+      (match maybe_constructor false head with
 	 | ConstrPat (loc,c) ->
 	     let (idsl,pl') =
-	       List.split (List.map (ast_to_pattern env ([],[])) pl) in
+	       List.split (List.map (ast_to_pattern scopes ([],[])) pl) in
 	     (aliases::(List.flatten idsl),
 	      PatCstr (loc,c,pl',alias_of aliases))
 	 | VarPat (loc,s) ->
@@ -379,8 +379,11 @@ let rec ast_to_pattern (_,_,scopes as env) aliases = function
       Symbols.interp_numeral_as_pattern loc (Bignat.NEG (Bignat.of_string n))
 	(alias_of aliases) scopes)
 
+  | Node(_,"PATTDELIMITERS", [Str(_,sc);e]) ->
+      ast_to_pattern (sc::scopes) aliases e
+
   | ast ->
-      (match maybe_constructor true env ast with
+      (match maybe_constructor true ast with
 	 | ConstrPat (loc,c) -> ([aliases], PatCstr (loc,c,[],alias_of aliases))
 	 | VarPat (loc,s) ->
 	     let aliases = merge_aliases aliases (name_of_nvar s) in
@@ -577,7 +580,7 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
   and ast_to_eqn n (ids,impls,scopes as env) = function
     | Node(loc,"EQN",rhs::lhs) ->
 	let (idsl_substl_list,pl) =
-	  List.split (List.map (ast_to_pattern env ([],[])) lhs) in
+	  List.split (List.map (ast_to_pattern scopes ([],[])) lhs) in
 	let idsl, substl = List.split (List.flatten idsl_substl_list) in
 	let eqn_ids = List.flatten idsl in
 	let subst = List.flatten substl in 
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 2d7c966ecc..d72a06f2a2 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -494,6 +494,7 @@ let gecdyn s =
   Hashtbl.add (snd uconstr) s (inDynamicAstType e); e
 
 let dynconstr = gecdyn "dynconstr"
+let dyncasespattern = gecdyn "dyncasespattern"
 let dyntactic = gecdyn "dyntactic"
 let dynvernac = gecdyn "dynvernac"
 let dynastlist = gecdyn "dynastlist"
@@ -504,6 +505,7 @@ let set_globalizer f = globalizer := f
 
 GEXTEND Gram
   dynconstr: [ [ a = Constr.constr -> !globalizer (PureAstNode a) ] ];
+  dyncasespattern: [ [ a = Constr.pattern -> !globalizer (PureAstNode a) ] ];
 (*
   dyntactic: [ [ a = Tactic.tactic -> !globalizer (TacticAstNode a) ] ];
   dynvernac: [ [ a = Vernac_.vernac -> !globalizer(VernacAstNode a) ] ];
@@ -520,6 +522,7 @@ type parser_type =
   | AstListParser
   | AstParser
   | ConstrParser
+  | CasesPatternParser
   | TacticParser
   | VernacParser
 
@@ -539,6 +542,7 @@ let entry_type_of_parser =  function
 
 let parser_type_from_name =  function
   | "constr" -> ConstrParser
+  | "cases_pattern" -> CasesPatternParser
   | "tactic" -> TacticParser
   | "vernac" -> VernacParser
   | s -> AstParser
@@ -547,6 +551,7 @@ let set_default_action_parser = function
   | AstListParser -> default_action_parser_ref := dynastlist
   | AstParser -> default_action_parser_ref := dynast
   | ConstrParser  -> default_action_parser_ref := dynconstr
+  | CasesPatternParser  -> default_action_parser_ref := dyncasespattern
   | TacticParser -> default_action_parser_ref := dyntactic
   | VernacParser -> default_action_parser_ref := dynvernac
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index f6bd506375..eb49b403c6 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -76,6 +76,7 @@ type parser_type =
   | AstListParser
   | AstParser
   | ConstrParser
+  | CasesPatternParser
   | TacticParser
   | VernacParser
 
diff --git a/theories/Init/PeanoSyntax.v b/theories/Init/PeanoSyntax.v
index ddef417515..3a2b63a37b 100644
--- a/theories/Init/PeanoSyntax.v
+++ b/theories/Init/PeanoSyntax.v
@@ -93,7 +93,7 @@ Grammar constr constr0 :=
 | natural_nat110 [ "(" "110" ")" ] -> [ 'N: 110 ' ]
 .
 
-Grammar constr pattern :=
+Grammar constr pattern : cases_pattern :=
   natural_pat0 [ "(" "0" ")" ] -> [ 'N: 0 ' ]
 | natural_pat1 [ "(" "1" ")" ] -> [ 'N: 1 ' ]
 | natural_pat2 [ "(" "2" ")" ] -> [ 'N: 2 ' ]
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 1ffbb18889..67eb2d379d 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -207,7 +207,8 @@ let prec_assoc = function
 
 let constr_tab =
   [| "constr0"; "constr1"; "constr2"; "constr3"; "lassoc_constr4";
-     "constr5"; "constr6"; "constr7"; "constr8"; "constr9"; "constr10" |]
+     "constr5"; "constr6"; "constr7"; "constr8"; "constr9"; "constr10";
+     "pattern" |]
   
 let constr_rule (n,p) =
   if p = E then constr_tab.(n) else constr_tab.(max (n-1) 0)
@@ -420,13 +421,14 @@ let add_infix assoc n inf qid sc =
   add_notation assoc n ("x "^(quote inf)^" y") ast sc
 
 (* Delimiters *)
-let load_delimiters _ (_,(gram_rule,scope,dlm)) =
+let load_delimiters _ (_,(_,_,scope,dlm)) =
   Symbols.declare_scope scope
 
-let open_delimiters i (_,(gram_rule,scope,dlm)) =
+let open_delimiters i (_,(gram_rule,pat_gram_rule,scope,dlm)) =
   if i=1 then begin
-    Egrammar.extend_grammar gram_rule;   (* For parsing *)
-    Symbols.declare_delimiters scope dlm (* For printing *)
+    Egrammar.extend_grammar gram_rule;      (* For parsing terms *)
+    Egrammar.extend_grammar pat_gram_rule;  (* For parsing patterns *)
+    Symbols.declare_delimiters scope dlm    (* For printing *)
   end
 
 let cache_delimiters o =
@@ -440,12 +442,18 @@ let (inDelim,outDelim) =
       load_function = load_delimiters;
       export_function = (fun x -> Some x) }
 
+let make_delimiter_rule (l,r as dlms) scope inlevel outlevel dlmname fname =
+  let symbols = [Terminal l; NonTerminal ((inlevel,E),"$e"); Terminal r] in
+  let prod = make_production symbols in
+  let args = Pcons(Pquote (string scope), Pcons (Pmeta ("$e",Tany), Pnil)) in
+  let action = Act (PureAstPat (Pnode(dlmname,args))) in
+  make_constr_grammar_rule outlevel fname prod action
+
 let add_delimiters scope (l,r as dlms) =
   if l = "" or r = "" then error "Delimiters cannot be empty";
   let fname = scope^"_delimiters" in
-  let symbols = [Terminal l; NonTerminal ((8,E),"$e"); Terminal r] in
-  let prod = make_production symbols in
-  let args = Pcons(Pquote (string scope), Pcons (Pmeta ("$e",Tany), Pnil)) in
-  let action = Act (PureAstPat (Pnode("DELIMITERS",args))) in
-  let gram_rule = make_constr_grammar_rule 0 fname prod action in
-  Lib.add_anonymous_leaf (inDelim(gram_rule,scope,dlms))
+  let gram_rule = make_delimiter_rule dlms scope 8 0 "DELIMITERS" fname in
+  let pfname = scope^"_patdelimiters" in
+  let pat_gram_rule = (* 11 is for "pattern" *)
+    make_delimiter_rule dlms scope 11 11 "PATTDELIMITERS" pfname in
+  Lib.add_anonymous_leaf (inDelim(gram_rule,pat_gram_rule,scope,dlms))