Modifs d'interpretation de patterns + exceptions dans le lexer

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

4 files changed, 47 insertions, 23 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 33325bf0b9..841a571e9d 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -567,7 +567,7 @@ let interp_constr1 sigma env lvar lmeta com =
   try
     ise_resolve2 sigma env (rtype lvar) (rtype lmeta) c
   with e -> 
-    Stdpp.raise_with_loc (Ast.loc com) e;;
+    Stdpp.raise_with_loc (Ast.loc com) e
 
 let typed_type_of_com sigma env com =
   let c = interp_rawconstr sigma env com in
@@ -652,45 +652,53 @@ let rec pat_of_ref metas vars = function
   | RAbst _ -> error "pattern_of_rawconstr: not implemented"
   | RVar _ -> assert false (* Capturé dans pattern_of_raw *)
 
-and pat_of_raw metas vars = function
+and pat_of_raw metas vars lvar = function
   | RRef (_,RVar id) -> 
       (try PRel (list_index (Name id) vars)
-       with Not_found -> PRef (RVar id))
+       with Not_found ->
+         (try (List.assoc id lvar)
+          with Not_found -> PRef (RVar id)))
   | RMeta (_,n) ->
       metas := n::!metas; PMeta (Some n)
   | RRef (_,r) ->
       PRef (pat_of_ref metas vars r)
   (* Hack pour ne pas réécrire une interprétation complète des patterns*)
   | RApp (_, RMeta (_,n), cl) when n<0 ->
-      PSoApp (- n, List.map (pat_of_raw metas vars) cl)
+      PSoApp (- n, List.map (pat_of_raw metas vars lvar) cl)
   | RApp (_,c,cl) -> 
-      PApp (pat_of_raw metas vars c,
-	    Array.of_list (List.map (pat_of_raw metas vars) cl))
+      PApp (pat_of_raw metas vars lvar c,
+	    Array.of_list (List.map (pat_of_raw metas vars lvar) cl))
   | RBinder (_,bk,na,c1,c2) ->
-      PBinder (bk, na, pat_of_raw metas vars c1,
-	       pat_of_raw metas (na::vars) c2)
+      PBinder (bk, na, pat_of_raw metas vars lvar c1,
+	       pat_of_raw metas (na::vars) lvar c2)
   | RSort (_,s) ->
       PSort s
   | RHole _ ->
       PMeta None
   | RCast (_,c,t) ->
       warning "Cast not taken into account in constr pattern";
-      pat_of_raw metas vars c
+      pat_of_raw metas vars lvar c
   | ROldCase (_,false,po,c,br) ->
-      PCase (option_app (pat_of_raw metas vars) po, pat_of_raw metas vars c,
-	     Array.map (pat_of_raw metas vars) br)
+      PCase (option_app (pat_of_raw metas vars lvar) po,
+             pat_of_raw metas vars lvar c,
+             Array.map (pat_of_raw metas vars lvar) br)
   | _ ->
       error "pattern_of_rawconstr: not implemented"
 
-let pattern_of_rawconstr c =
+let pattern_of_rawconstr lvar c =
   let metas = ref [] in
-  let p = pat_of_raw metas [] c in
+  let p = pat_of_raw metas [] lvar c in
   (!metas,p)
 
-let interp_constrpattern sigma env com = 
-  let c = dbize CCI sigma (unitize_env (context env)) true [] com in
+let interp_constrpattern_gen sigma env lvar com = 
+  let c =
+    dbize CCI sigma (unitize_env (context env)) true (List.map (fun x ->
+      string_of_id (fst x)) lvar) com
+  and nlvar = List.map (fun (id,c) -> (id,pattern_of_constr c)) lvar in
   try 
-    pattern_of_rawconstr c
+    pattern_of_rawconstr nlvar c
   with e -> 
     Stdpp.raise_with_loc (Ast.loc com) e
 
+let interp_constrpattern sigma env com =
+  interp_constrpattern_gen sigma env [] com
diff --git a/parsing/astterm.mli b/parsing/astterm.mli
index 6c50a5ebd5..285f997ceb 100644
--- a/parsing/astterm.mli
+++ b/parsing/astterm.mli
@@ -34,6 +34,12 @@ val interp_casted_constr1 :
   'a evar_map -> env -> (identifier * constr) list ->
     (int * constr) list -> Coqast.t -> constr -> constr
 
+(*Interprets constr patterns according to a list of instantiations
+  (variables)*)
+val interp_constrpattern_gen :
+  'a evar_map -> env -> (identifier * constr) list -> Coqast.t ->
+    int list * constr_pattern
+
 val interp_constrpattern : 
   'a evar_map -> env -> Coqast.t -> int list * constr_pattern
 
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 9a64fd03c1..37f47b6f0b 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -247,6 +247,7 @@ GEXTEND Gram
       | IDENT "Repeat"; ta = tactic_atom -> <:ast< (REPEAT $ta) >>
       |	IDENT "Idtac" -> <:ast< (IDTAC) >>
       |	IDENT "Fail" -> <:ast<(FAIL)>>
+      |	IDENT "Fail"; n = numarg -> <:ast<(FAIL $n)>>
       |	ta0 = tactic_atom; "Orelse"; ta1 = tactic_atom ->
           <:ast< (ORELSE $ta0 $ta1) >>
       |	st = simple_tactic -> st
@@ -255,7 +256,7 @@ GEXTEND Gram
   tactic_arg:
     [ [ "()" -> <:ast< (VOID) >>
       | n = pure_numarg -> n
-      |	c=constrarg -> 
+      |	c = constrarg ->
           (match c with
             Coqast.Node(_,"COMMAND",[Coqast.Nvar(_,s)]) -> <:ast<($VAR $s)>>
            |_ -> c) ] ]
diff --git a/parsing/lexer.mll b/parsing/lexer.mll
index dca9a2fdd7..10ed3ab86a 100644
--- a/parsing/lexer.mll
+++ b/parsing/lexer.mll
@@ -119,9 +119,8 @@ let firstchar =
 let identchar = 
   ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' 
    '\'' '0'-'9']
-let 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']+
@@ -136,10 +135,20 @@ rule token = parse
   | decimal_literal | hex_literal | oct_literal | bin_literal
       { ("INT", Lexing.lexeme lexbuf) }
   | "(" | ")" | "[" | "]" | "{" | "}" | "." | "_" | ";"| "`" | "()" | "'("
-  | "->"
-      { ("", Lexing.lexeme lexbuf) }
-  | symbolchar+
+  | "->" | "\\/" | "/\\" | "|-" | ":=" | "<->" | extrachar
       { ("", Lexing.lexeme lexbuf) }
+  | ('\\' (symbolchar | '\\' | '-' | '>' | '|' | ':' | '?' | '=' | '<')+ |
+     '/'  (symbolchar | '/'  | '-' | '>' | '|' | ':' | '?' | '=' | '<')+ |
+     '-'  (symbolchar | '\\' | '/' | '-' | '|' | ':' | '?' | '=' | '<')+ |
+     '|'  (symbolchar | '\\' | '/' | '|' | '>' | ':' | '?' | '=' | '<')+ |
+     '='  (symbolchar | '\\' | '/' | '|' | '-' | '>' | ':' | '=' | '<')+ |
+     ':'  (symbolchar | '\\' | '/' | '|' | '-' | '>' | ':' | '=' | '<')+ |
+     '<'  (symbolchar | '\\' | '/' | '|' | '>' | '?' | ':' | '=' | '<')+ |
+     "<-" (symbolchar | '\\' | '/' | '|' | '-' | '?' | ':' | '=' | '<')+ |
+     '>' | '?') extrachar* | "<-"
+    { ("", Lexing.lexeme lexbuf) }
+  | symbolchar+ extrachar*
+    { ("", Lexing.lexeme lexbuf) }
   (***
   | '`' [^'`']* '`'
       { let s = Lexing.lexeme lexbuf in