Plus de piquants dans les actions des grammaires; nom de la grammaire pris comme parseur par defaut; le type List devient AstList

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

6 files changed, 69 insertions, 24 deletions

diff --git a/parsing/ast.ml b/parsing/ast.ml
index e7c6cb23c7..d154b79701 100755
--- a/parsing/ast.ml
+++ b/parsing/ast.ml
@@ -544,16 +544,12 @@ let rec act_of_ast vars etyp ast =
            | ETastl ->
                let acl = List.map (caselist vars etyp) cl in
                Acaselist (pa,acl))
-    | Node(_,"ASTLIST",al) ->
-        (match (etyp,al) with
-           | (ETast,[a]) -> Aast (val_of_ast vars a)
-           | (ETastl,_) -> Aastlist (vall_of_astl vars al)
-           | (ETast,_) -> user_err_loc
-                 (loc ast,"Ast.act_of_ast",
-                  [< 'sTR
-                       "entry type is Ast, but the right hand side is a list"
-                  >]))
-    | _ -> invalid_arg_loc (loc ast,"Ast.act_of_ast: ill-formed")
+    | Node(_,"ASTLIST",al) when etyp = ETastl ->
+	Aastlist (vall_of_astl vars al)
+    | a when etyp = ETast ->
+	  Aast (val_of_ast vars a)
+    | _ ->
+	invalid_arg_loc (loc ast,"Ast.act_of_ast: ill-typed")
 
 and case vars etyp ast =
   match ast with
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 002925e167..9065d565c7 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -418,12 +418,17 @@ let dbize k sigma env allow_soapp lvar =
 	    else 
 	      (RHole None)::(aux (n+1) l' args)
 	  else 
-	    error "Bad explicitation number"
+	    if i<>n then
+	      error ("Bad explicitation number: found "^
+		   (string_of_int j)^" but was expecting a regular argument")
+	    else
+	      error ("Bad explicitation number: found "^
+		   (string_of_int j)^" but was expecting "^(string_of_int i))
       | (i::l',a::args') -> 
 	  if i=n then 
 	    (RHole None)::(aux (n+1) l' args)
 	  else 
-	    (dbrec env a)::(aux (n+1) l' args')
+	    (dbrec env a)::(aux (n+1) l args')
       | ([],args) -> List.map (dbrec env) args
       | (_,[]) -> []
     in 
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index ad1fbd1b55..b8534a8730 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -172,10 +172,15 @@ END;
 GEXTEND Gram
   GLOBAL: syntax Prim.syntax_entry Prim.grammar_entry;
 
+  grammar_univ:
+  [ [ univ = IDENT ->
+	let _ = set_default_action_parser_by_name univ in univ ] ]
+  ;
   syntax:
    [ [ "Token"; s = STRING; "." -> <:ast< (TOKEN ($STR $s)) >>
 
-     | "Grammar"; univ=IDENT; tl=LIST1 Prim.grammar_entry SEP "with"; "." ->
+     | "Grammar"; univ = grammar_univ;
+       tl = LIST1 Prim.grammar_entry SEP "with"; "." ->
          <:ast< (GRAMMAR ($VAR univ) (ASTLIST ($LIST tl))) >>
 
      | "Syntax"; whatfor=IDENT; el=LIST1 Prim.syntax_entry SEP ";"; "." ->
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 7be07ea0d1..239277828f 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -60,14 +60,18 @@ GEXTEND Gram
       | IDENT "case"; a = action; et = entry_type; "of";
         cl = LIST1 case SEP "|"; IDENT "esac" ->
           Node(loc,"$CASE",a::et::cl)
-      | "["; al = astlist; "]" -> al ] ]
+      | "["; al = default_action_parser; "]" -> al ] ]
   ;
   case:
     [[ p = astlist; "->"; a = action -> Node(loc,"CASE",[p;a]) ]]
   ;
   entry_type:
-    [[ ":"; IDENT "List" -> Id(loc,"LIST")
-     | ":"; IDENT "Ast" -> Id(loc,"AST")
+    [[ ":"; IDENT "AstList" -> 
+	 let _ = set_default_action_parser astlist in Id(loc,"LIST")
+     | ":"; IDENT "List" -> (* For compatibility *)
+	 let _ = set_default_action_parser astlist in Id(loc,"LIST")
+     | ":"; IDENT "Ast" ->
+	 let _ = set_default_action_parser ast in Id(loc,"AST")
      | -> Id(loc,"AST") ]]
   ;
 END
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 951a576c8f..a80952480e 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -390,20 +390,49 @@ END
 (* Quotations *)
 
 open Prim
+open Constr
+open Tactic
+open Vernac
 
 let define_quotation default s e =
   (if default then
     GEXTEND Gram
       ast: [ [ "<<"; c = e; ">>" -> c ] ];
+     (* Uncomment this to keep compatibility with old grammar syntax
+     constr: [ [ "<<"; c = e; ">>" -> c ] ];
+     vernac: [ [ "<<"; c = e; ">>" -> c ] ];
+     tactic: [ [ "<<"; c = e; ">>" -> c ] ];
+     *)
    END);
   (GEXTEND Gram
-     GLOBAL: ast;
+     GLOBAL: ast constr vernac tactic;
      ast:
-       [ [ _ = langle_colon; IDENT $s$; _ = colon_langle; c = e; ">>" -> c ] ];
-     langle_colon:
-       [ [ "<"; ":" -> ()
-	 | "<:" -> () ] ];  (* Maximal token rule *)
-     colon_langle:
-       [ [ ":"; "<" -> ()
-	 | ":<" -> () ] ]; (* Maximal token rule *)
+       [ [ "<:"; IDENT $s$; ":<"; c = e; ">>" -> c ] ];
+     (* Uncomment this to keep compatibility with old grammar syntax
+     constr:
+       [ [ "<:"; IDENT $s$; ":<"; c = e; ">>" -> c ] ];
+     vernac:
+       [ [ "<:"; IDENT $s$; ":<"; c = e; ">>" -> c ] ];
+     tactic:
+       [ [ "<:"; IDENT $s$; ":<"; c = e; ">>" -> c ] ];
+     *)
    END)
+
+let _ = define_quotation false "ast" ast in ()
+
+let default_action_parser_ref = ref ast
+
+let get_default_action_parser () = !default_action_parser_ref
+
+let set_default_action_parser f = (default_action_parser_ref := f)
+
+let set_default_action_parser_by_name = function
+  | "constr" -> set_default_action_parser Constr.constr
+  | "tactic" -> set_default_action_parser Tactic.tactic
+  | "vernac" -> set_default_action_parser Vernac.vernac
+  | _ -> set_default_action_parser ast
+
+let default_action_parser =
+  Gram.Entry.of_parser "default_action_parser" 
+    (fun strm -> Gram.Entry.parse_token (get_default_action_parser ()) strm)
+
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index a60bfec5e8..2d486e5617 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -52,6 +52,12 @@ val force_entry_type : string * gram_universe -> string ->
 
 val define_quotation : bool -> string -> (Coqast.t Gram.Entry.e) -> unit
 
+(* The default parser for actions in grammar rules *)
+
+val default_action_parser : Coqast.t Gram.Entry.e
+val set_default_action_parser : Coqast.t Gram.Entry.e -> unit
+val set_default_action_parser_by_name : string -> unit
+
 (* The main entry: reads an optional vernac command *)
 
 val main_entry : Coqast.t option Gram.Entry.e