Pattern matching de sous-termes + exceptions dans le lexer

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

8 files changed, 140 insertions, 29 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index e9ed83a54..d685b292a 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -17,8 +17,10 @@ GEXTEND Gram
   ;
   constr:
     [ [ c = constr8 -> c 
-      | IDENT "Eval"; rtc=Tactic.red_tactic; "in"; c=constr8 ->
-        <:ast<(EVAL $c (REDEXP $rtc))>> ] ]
+      | IDENT "Context"; id = ident; IDENT "With"; c = constr8 ->
+        <:ast< (CONTEXT $id $c) >>
+      | IDENT "Eval"; rtc = Tactic.red_tactic; "in"; c = constr8 ->
+        <:ast< (EVAL $c (REDEXP $rtc)) >> ] ]
   ;
   lconstr:
     [ [ c = constr10 -> c ] ]
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 37f47b6f0..d0e3a8a76 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -4,8 +4,8 @@
 open Pp
 open Ast
 open Pcoq
-
 open Tactic
+open Util
 
 (* Please leave several GEXTEND for modular compilation under PowerPC *)
 
@@ -193,23 +193,42 @@ GEXTEND Gram
     [ [ name = identarg; it = LIST1 input_fun; "->"; body = tactic_expr ->
           <:ast< (RECCLAUSE $name (FUNVAR ($LIST $it)) $body) >> ] ]
   ;
+  match_pattern:
+    [ [ id = constrarg; "["; pc = constrarg; "]" ->
+          (match id with
+          | Coqast.Node(_,"COMMAND",[Coqast.Nvar(_,s)]) ->
+            <:ast< (SUBTERM ($VAR $s) $pc) >>
+          | _ ->
+            errorlabstrm "Gram.match_pattern" [<'sTR "Not a correct SUBTERM">])
+      | "["; pc = constrarg; "]" -> <:ast< (SUBTERM $pc) >>
+      | pc = constrarg -> <:ast< (TERM $pc) >> ] ]
+  ;
   match_hyps:
-    [ [ id = identarg; ":"; pc = constrarg ->
-          <:ast< (MATCHCONTEXTHYPS $id $pc) >>
-      | IDENT "_"; ":"; pc = constrarg -> <:ast< (MATCHCONTEXTHYPS $pc) >> ] ]
+    [ [ id = identarg; ":"; mp =  match_pattern ->
+          <:ast< (MATCHCONTEXTHYPS $id $mp) >>
+      | IDENT "_"; ":"; mp = match_pattern ->
+          <:ast< (MATCHCONTEXTHYPS $mp) >> ] ]
   ;
   match_context_rule:
-    [ [ "["; largs = LIST0 match_hyps SEP ";"; "|-"; pc = constrarg; "]"; "->";
-          te = tactic_expr ->
-            <:ast< (MATCHCONTEXTRULE ($LIST $largs) $pc $te) >> 
+    [ [ "["; largs = LIST0 match_hyps SEP ";"; "|-"; mp = match_pattern; "]";
+        "->"; te = tactic_expr ->
+            <:ast< (MATCHCONTEXTRULE ($LIST $largs) $mp $te) >> 
       | IDENT "_"; "->"; te = tactic_expr -> <:ast< (MATCHCONTEXTRULE $te) >>
     ] ]
   ;
+  match_context_list:
+    [ [ mrl = LIST1 match_context_rule SEP "|" -> mrl
+      | "|"; mrl = LIST1 match_context_rule SEP "|" -> mrl ] ]
+  ;
   match_rule:
-    [ [ "["; com = constrarg; "]"; "->"; te = tactic_expr ->
-          <:ast<(MATCHRULE $com $te)>>
+    [ [ "["; mp = match_pattern; "]"; "->"; te = tactic_expr ->
+        <:ast<(MATCHRULE $mp $te)>>
       | IDENT "_"; "->"; te = tactic_expr -> <:ast< (MATCHRULE $te) >> ] ]
   ;
+  match_list:
+    [ [ mrl = LIST1 match_rule SEP "|" -> mrl
+      | "|"; mrl = LIST1 match_rule SEP "|" -> mrl ] ]
+  ;
   tactic_expr:
     [ [ ta0 = tactic_expr; ";"; ta1 = tactic_expr ->
          <:ast< (TACTICLIST $ta0 $ta1) >>
@@ -229,11 +248,10 @@ GEXTEND Gram
             <:ast< (REC (RECDECL $rc ($LIST $rcl)) $body) >>
       | IDENT "Let"; llc = LIST1 let_clause SEP IDENT "And"; IDENT "In";
           u = tactic_expr -> <:ast< (LET (LETDECL ($LIST $llc)) $u) >>
-      |	IDENT "Match"; IDENT "Context"; IDENT "With";
-          mrl = LIST1 match_context_rule SEP "|" ->
-            <:ast< (MATCHCONTEXT ($LIST $mrl)) >>
-      |	IDENT "Match"; com = constrarg; IDENT "With";
-          mrl = LIST1 match_rule SEP "|" -> <:ast< (MATCH $com ($LIST $mrl)) >>
+      |	IDENT "Match"; IDENT "Context"; IDENT "With"; mrl = match_context_list
+        -> <:ast< (MATCHCONTEXT ($LIST $mrl)) >>
+      |	IDENT "Match"; com = constrarg; IDENT "With"; mrl = match_list ->
+        <:ast< (MATCH $com ($LIST $mrl)) >>
       |	"'("; te = tactic_expr; ")" -> te
       |	"'("; te = tactic_expr; tel=LIST1 tactic_expr; ")" ->
           <:ast< (APP $te ($LIST tel)) >>
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 187c75c07..7c91cbf90 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -428,13 +428,16 @@ GEXTEND Gram
 
 (* Proof commands *)
 GEXTEND Gram
-  GLOBAL: command;
+  GLOBAL: command ne_constrarg_list;
 
   destruct_location :
   [ [ IDENT "Conclusion"  -> <:ast< (CONCL)>>
     | IDENT "Discardable"; "Hypothesis"  -> <:ast< (DiscardableHYP)>>
     | "Hypothesis"   -> <:ast< (PreciousHYP)>> ]]
   ;
+  ne_constrarg_list:
+  [ [ l = LIST1 constrarg -> l ] ]
+  ;
   opt_identarg_list:
   [ [ -> []
     | ":"; l = LIST1 identarg -> l ] ]
diff --git a/parsing/lexer.mll b/parsing/lexer.mll
index 10ed3ab86..54cb8285c 100644
--- a/parsing/lexer.mll
+++ b/parsing/lexer.mll
@@ -119,8 +119,8 @@ let firstchar =
 let identchar = 
   ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' 
    '\'' '0'-'9']
-let symbolchar = ['!' '$' '%' '&' '*' '+' ',' '@' '^' '~' '#']
-let extrachar = symbolchar | ['\\' '/' '-' '<' '>' '|' ':' '?' '=']
+let symbolchar = ['!' '$' '%' '&' '*' '+' ',' '@' '^' '#']
+let extrachar = symbolchar | ['\\' '/' '-' '<' '>' '|' ':' '?' '=' '~']
 let decimal_literal = ['0'-'9']+
 let hex_literal = '0' ['x' 'X'] ['0'-'9' 'A'-'F' 'a'-'f']+
 let oct_literal = '0' ['o' 'O'] ['0'-'7']+
@@ -137,14 +137,15 @@ rule token = parse
   | "(" | ")" | "[" | "]" | "{" | "}" | "." | "_" | ";"| "`" | "()" | "'("
   | "->" | "\\/" | "/\\" | "|-" | ":=" | "<->" | extrachar
       { ("", Lexing.lexeme lexbuf) }
-  | ('\\' (symbolchar | '\\' | '-' | '>' | '|' | ':' | '?' | '=' | '<')+ |
-     '/'  (symbolchar | '/'  | '-' | '>' | '|' | ':' | '?' | '=' | '<')+ |
-     '-'  (symbolchar | '\\' | '/' | '-' | '|' | ':' | '?' | '=' | '<')+ |
-     '|'  (symbolchar | '\\' | '/' | '|' | '>' | ':' | '?' | '=' | '<')+ |
-     '='  (symbolchar | '\\' | '/' | '|' | '-' | '>' | ':' | '=' | '<')+ |
-     ':'  (symbolchar | '\\' | '/' | '|' | '-' | '>' | ':' | '=' | '<')+ |
-     '<'  (symbolchar | '\\' | '/' | '|' | '>' | '?' | ':' | '=' | '<')+ |
-     "<-" (symbolchar | '\\' | '/' | '|' | '-' | '?' | ':' | '=' | '<')+ |
+  | ('\\'(symbolchar | '\\' | '-' | '>' | '|' | ':' | '?' | '=' | '<' | '~')+ |
+     '/' (symbolchar | '/'  | '-' | '>' | '|' | ':' | '?' | '=' | '<' | '~')+ |
+     '-' (symbolchar | '\\' | '/' | '-' | '|' | ':' | '?' | '=' | '<' | '~')+ |
+     '|' (symbolchar | '\\' | '/' | '|' | '>' | ':' | '?' | '=' | '<' | '~')+ |
+     '=' (symbolchar | '\\' | '/' | '|' | '-' | '>' | ':' | '=' | '<' | '~')+ |
+     '<' (symbolchar | '\\' | '/' | '|' | '>' | '?' | ':' | '=' | '<' | '~')+ |
+     "<-"(symbolchar | '\\' | '/' | '|' | '-' | '?' | ':' | '=' | '<' | '~')+ |
+     '~' (symbolchar | '\\' | '/' | '|' | '-' | '>' | ':' | '=' | '<' )+      |
+     ':' (symbolchar | '\\' | '/' | '|' | '-' | '>' | ':' | '=' | '<' )+      |
      '>' | '?') extrachar* | "<-"
     { ("", Lexing.lexeme lexbuf) }
   | symbolchar+ extrachar*
diff --git a/parsing/pattern.ml b/parsing/pattern.ml
index 6d3c362d6..e3fa611ed 100644
--- a/parsing/pattern.ml
+++ b/parsing/pattern.ml
@@ -189,7 +189,7 @@ let matches_core convert pat c =
 	  if is_conv env evars (mkConst (sp1,ctxt1)) cT then sigma
 	  else raise PatternMatchingFailure
 
-      | PCase (_,a1,br1), IsMutCase (ci,p2,a2,br2) ->
+      | PCase (_,a1,br1), IsMutCase (_,_,a2,br2) ->
 	  (* On ne teste pas le prédicat *)
 	  array_fold_left2 (sorec stk) (sorec stk sigma a1 a2)
 	    br1 br2
@@ -204,6 +204,79 @@ let matches_core convert pat c =
 
 let matches = matches_core None
 
+(* To skip to the next occurrence *)
+exception NextOccurrence of int
+
+(* Tells if it is an authorized occurrence *)
+let authorized_occ nocc mres =
+  if nocc = 0 then mres
+  else raise (NextOccurrence nocc)
+
+(* Tries matches according to the occurrence *)
+let rec try_matches nocc pat = function
+  | [] -> raise (NextOccurrence nocc)
+  | c::tl ->
+    (try authorized_occ nocc (matches pat c) with
+    | PatternMatchingFailure -> (try_matches nocc pat tl)
+    | NextOccurrence nocc -> (try_matches (nocc - 1) pat tl))
+
+(* Tries to match a subterm of [c] with [pat] *)
+let rec sub_match nocc pat c =
+  match c with
+  | DOP2 (Cast,c1,c2) ->
+    (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with
+    | PatternMatchingFailure ->
+      let (lm,lc) = try_sub_match nocc pat [c1] in
+      (lm,DOP2 (Cast,List.hd lc,c2))
+    | NextOccurrence nocc ->
+      let (lm,lc) = try_sub_match (nocc - 1) pat [c1] in
+      (lm,DOP2 (Cast,List.hd lc,c2)))
+  | DOP2 (ne,c1,DLAM (x,c2)) ->
+    (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with
+    | PatternMatchingFailure ->
+      let (lm,lc) = try_sub_match nocc pat [c1;c2] in
+      (lm,DOP2 (ne,List.hd lc,DLAM (x,List.nth lc 1)))
+    | NextOccurrence nocc ->
+      let (lm,lc) = try_sub_match (nocc - 1) pat [c1;c2] in
+      (lm,DOP2 (ne,List.hd lc,DLAM (x,List.nth lc 1))))
+  | DOPN (AppL,a) when Array.length a <> 0 ->
+    let c1 = a.(0)
+    and lc = List.tl (Array.to_list a) in
+    (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with
+    | PatternMatchingFailure ->
+      let (lm,le) = try_sub_match nocc pat (c1::lc) in
+      (lm,DOPN (AppL,Array.of_list le))
+    | NextOccurrence nocc ->
+      let (lm,le) = try_sub_match (nocc - 1) pat (c1::lc) in
+      (lm,DOPN (AppL,Array.of_list le)))
+  | DOPN (MutCase ci,v) ->
+    let hd = v.(0)
+    and c1 = v.(1)
+    and lc = Array.to_list (Array.sub v 2 (Array.length v - 2)) in
+    (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with
+    | PatternMatchingFailure ->
+      let (lm,le) = try_sub_match nocc pat (c1::lc) in
+      (lm,DOPN (MutCase ci,Array.of_list (hd::le)))
+    | NextOccurrence nocc ->
+      let (lm,le) = try_sub_match (nocc - 1) pat (c1::lc) in
+      (lm,DOPN (MutCase ci,Array.of_list (hd::le))))
+  | c ->
+    (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with
+    | PatternMatchingFailure -> raise (NextOccurrence nocc)
+    | NextOccurrence nocc -> raise (NextOccurrence (nocc - 1)))
+
+(* Tries [sub_match] for all terms in the list *)
+and try_sub_match nocc pat lc =
+  let rec try_sub_match_rec nocc pat lacc = function
+    | [] -> raise (NextOccurrence nocc)
+    | c::tl ->
+      (try 
+         let (lm,ce) = sub_match nocc pat c in
+         (lm,lacc@(ce::tl))
+       with
+      | NextOccurrence nocc -> try_sub_match_rec nocc pat (lacc@[c]) tl) in
+  try_sub_match_rec nocc pat [] lc
+
 let is_matching pat n =
   try let _ = matches pat n in true
   with PatternMatchingFailure -> false
diff --git a/parsing/pattern.mli b/parsing/pattern.mli
index b725d9044..803e4fffe 100644
--- a/parsing/pattern.mli
+++ b/parsing/pattern.mli
@@ -69,9 +69,15 @@ val is_matching      :
 val matches_conv :
   env -> 'a Evd.evar_map -> constr_pattern -> constr -> (int * constr) list
 
+(* To skip to the next occurrence *)
+exception NextOccurrence of int
+
+(* Tries to match a subterm of [c] with [pat] *)
+val sub_match :
+  int -> constr_pattern -> constr -> ((int * constr) list * constr)
+
 (* [is_matching_conv env sigma pat c] tells if [c] matches against [pat]
    up to conversion for constants in patterns *)
 
 val is_matching_conv :
   env -> 'a Evd.evar_map -> constr_pattern -> constr -> bool
-
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index a80952480..9d2b8e931 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -286,7 +286,10 @@ module Tactic =
     let clausearg = gec "clausearg"
     let match_context_rule = gec "match_context_rule"
     let match_hyps = gec "match_hyps"
+    let match_pattern = gec "match_pattern"
+    let match_context_list = gec_list "match_context_list"
     let match_rule = gec "match_rule"
+    let match_list = gec_list "match_list"
     let ne_identarg_list = gec_list "ne_identarg_list"
     let ne_num_list = gec_list "ne_num_list"
     let ne_pattern_list = gec_list "ne_pattern_list"
@@ -343,6 +346,7 @@ module Vernac =
     let stringarg = gec "stringarg"
     let ne_stringarg_list = gec_list "ne_stringarg_list"
     let constrarg = gec "constrarg"
+    let ne_constrarg_list = gec_list "ne_constrarg_list"
     let tacarg = gec "tacarg"
     let sortarg = gec "sortarg"
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 2d486e561..e3ccced7d 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -113,7 +113,10 @@ module Tactic :
     val let_clause : Coqast.t Gram.Entry.e
     val match_context_rule : Coqast.t Gram.Entry.e
     val match_hyps : Coqast.t Gram.Entry.e
+    val match_pattern : Coqast.t Gram.Entry.e
+    val match_context_list : Coqast.t list Gram.Entry.e
     val match_rule : Coqast.t Gram.Entry.e
+    val match_list : Coqast.t list Gram.Entry.e
     val ne_identarg_list : Coqast.t list Gram.Entry.e
     val ne_intropattern : Coqast.t Gram.Entry.e
     val ne_num_list : Coqast.t list Gram.Entry.e
@@ -152,6 +155,7 @@ module Vernac :
     val stringarg : Coqast.t Gram.Entry.e
     val ne_stringarg_list : Coqast.t list Gram.Entry.e
     val constrarg : Coqast.t Gram.Entry.e
+    val ne_constrarg_list : Coqast.t list Gram.Entry.e
     val tacarg : Coqast.t Gram.Entry.e
     val sortarg : Coqast.t Gram.Entry.e