Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; rparation de la protection contre les clauses indiscernables de TACTIC EXTEND et VERNAC COMMAND EXTEND; rparation des grammaires de Extraction, EAuto, TextMode, KillProof et Derive Dependent Inversion

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

8 files changed, 298 insertions, 51 deletions

diff --git a/Makefile b/Makefile
index a92321969d..b5ff0809bf 100644
--- a/Makefile
+++ b/Makefile
@@ -785,7 +785,8 @@ tags:
 ML4FILES += parsing/lexer.ml4 parsing/q_util.ml4 parsing/q_coqast.ml4 \
             parsing/g_prim.ml4 parsing/pcoq.ml4
 
-CAMLP4EXTENSIONS= parsing/tacextend.cmo parsing/vernacextend.cmo 
+CAMLP4EXTENSIONS= parsing/argextend.cmo parsing/tacextend.cmo \
+	   parsing/vernacextend.cmo 
 
 GRAMMARCMO=lib/pp_control.cmo lib/pp.cmo lib/util.cmo \
 	   lib/dyn.cmo lib/options.cmo \
@@ -808,7 +809,7 @@ clean::
 ML4FILES +=parsing/g_basevernac.ml4 parsing/g_minicoq.ml4 \
 	   parsing/g_vernac.ml4 parsing/g_proofs.ml4 parsing/g_cases.ml4 \
 	   parsing/g_constr.ml4 parsing/g_tactic.ml4 parsing/g_ltac.ml4 \
-	   parsing/tacextend.ml4 parsing/vernacextend.ml4
+	   parsing/argextend.ml4 parsing/tacextend.ml4 parsing/vernacextend.ml4
 
 # beforedepend:: $(GRAMMARCMO)
 
diff --git a/contrib/extraction/g_extraction.ml4 b/contrib/extraction/g_extraction.ml4
index 1fe4ee7058..84f0f663b9 100644
--- a/contrib/extraction/g_extraction.ml4
+++ b/contrib/extraction/g_extraction.ml4
@@ -13,31 +13,23 @@
 open Vernacexpr
 open Pcoq
 open Genarg
+open Pp
 
-let wit_mlname, rawwit_mlname = Genarg.create_arg "mlname"
-let mlname = create_generic_entry "mlname" rawwit_mlname
-let _ = Tacinterp.add_genarg_interp "mlname"
-  (fun ist x ->
-    (in_gen wit_mlname
-      (out_gen wit_string
-	(Tacinterp.genarg_interp ist
-	  (in_gen rawwit_string
-	    (out_gen rawwit_mlname x))))))
-
-GEXTEND Gram
-  GLOBAL: mlname;
-  mlname:
-  [ [ id = IDENT -> id
-    | s = STRING -> s ] ]
-  ;
+VERNAC ARGUMENT EXTEND mlname
+| [ preident(id) ] -> [ id ]
+| [ string(s) ] -> [ s ]
 END
 
-(* Extraction commands *)
-
 open Table
 open Extract_env
-open Pcoq.Constr
-open Pcoq.Prim
+
+VERNAC ARGUMENT EXTEND language
+| [ "Ocaml" ] -> [ Ocaml ]
+| [ "Haskell" ] -> [ Haskell ]
+| [ "Toplevel" ] -> [ Toplevel ]
+END
+
+(* Extraction commands *)
 
 VERNAC COMMAND EXTEND Extraction
 (* Extraction in the Coq toplevel *)
@@ -47,44 +39,58 @@ VERNAC COMMAND EXTEND Extraction
 (* Monolithic extraction to a file *)
 | [ "Extraction" string(f) ne_qualid_list(l) ] 
   -> [ extraction_file f l ]
+END
 
 (* Modular extraction (one Coq module = one ML module) *)
+VERNAC COMMAND EXTEND ExtractionModule
 | [ "Extraction" "Module" ident(m) ]
   -> [ extraction_module m ]
+END
+
+VERNAC COMMAND EXTEND RecursiveExtractionModule
 | [ "Recursive" "Extraction" "Module" ident(m) ]
   -> [ recursive_extraction_module m ]
+END
 
 (* Target Language *)
+VERNAC COMMAND EXTEND ExtractionLanguage
+| [ "Extraction" "Language" language(l) ] 
+  -> [ extraction_language l ]
+END
 
-| [ "Extraction" "Language" "Ocaml" ] 
-  -> [ extraction_language Ocaml ]
-| [ "Extraction" "Language" "Haskell" ] 
-  -> [ extraction_language Haskell ]
-| [ "Extraction" "Language" "Toplevel" ] 
-  -> [ extraction_language Toplevel ]
-
+VERNAC COMMAND EXTEND ExtractionInline
 (* Custom inlining directives *)
 | [ "Extraction" "Inline" ne_qualid_list(l) ] 
   -> [ extraction_inline true l ]
+END
 
+VERNAC COMMAND EXTEND ExtractionNoInline
 | [ "Extraction" "NoInline" ne_qualid_list(l) ] 
   -> [ extraction_inline false l ]
+END
 
+VERNAC COMMAND EXTEND PrintExtractionInline
 | [ "Print" "Extraction" "Inline" ]
   -> [ print_extraction_inline () ]
+END
 
+VERNAC COMMAND EXTEND ResetExtractionInline
 | [ "Reset" "Extraction" "Inline" ]
   -> [ reset_extraction_inline () ]
+END
 
 (* Overriding of a Coq object by an ML one *)
+VERNAC COMMAND EXTEND ExtractionConstant
 | [ "Extract" "Constant" qualid(x) "=>" mlname(y) ]
   -> [ extract_constant_inline false x y ]
+END
 
+VERNAC COMMAND EXTEND ExtractionInlinedConstant
 | [ "Extract" "Inlined" "Constant" qualid(x) "=>" mlname(y) ]
   -> [ extract_constant_inline true x y ]
+END
 
+VERNAC COMMAND EXTEND ExtractionInductive
 | [ "Extract" "Inductive" qualid(x) "=>" mlname(id) "[" mlname_list(idl) "]" ]
   -> [ extract_inductive x (id,idl) ]
-
-
 END
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index e1ef0ecc15..92f6f285f8 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -484,10 +484,14 @@ let kill_node_verbose n =
 
 let set_text_mode s = text_proof_flag := s
 
+VERNAC ARGUMENT EXTEND text_mode
+| [ "fr" ] -> [ "fr" ]
+| [ "en" ] -> [ "en" ]
+| [ "Off" ] -> [ "off" ]
+END
+
 VERNAC COMMAND EXTEND TextMode
-| [ "Text" "Mode" "fr" ] -> [ set_text_mode "fr" ]
-| [ "Text" "Mode" "en" ] -> [ set_text_mode "en" ]
-| [ "Text" "Mode" "Off" ] -> [ set_text_mode "off" ]
+| [ "Text" "Mode" text_mode(s) ] -> [ set_text_mode s ]
 END
 
 VERNAC COMMAND EXTEND OutputGoal
@@ -498,8 +502,11 @@ VERNAC COMMAND EXTEND OutputGoal
   [ "Goal" "Cmd" natural(n) "with" tactic(tac) ] -> [ simulate_solve n tac ]
 END
 
-VERNAC COMMAND EXTEND KillProof
+VERNAC COMMAND EXTEND KillProofAfter
 | [ "Kill" "Proof" "after"  natural(n) ] -> [ kill_node_verbose n ]
+END
+
+VERNAC COMMAND EXTEND KillProofAt
 | [ "Kill" "Proof" "at"  natural(n) ] -> [ kill_node_verbose n ]
 END
 
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
new file mode 100644
index 0000000000..54eeca7542
--- /dev/null
+++ b/parsing/argextend.ml4
@@ -0,0 +1,200 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Genarg
+open Q_util
+open Q_coqast
+open Ast
+
+let join_loc (deb1,_) (_,fin2) = (deb1,fin2)
+let loc = (0,0)
+let default_loc = <:expr< (0,0) >>
+
+let rec make_rawwit loc = function
+  | BoolArgType -> <:expr< Genarg.rawwit_bool >>
+  | IntArgType -> <:expr< Genarg.rawwit_int >>
+  | IntOrVarArgType -> <:expr< Genarg.rawwit_int_or_var >>
+  | StringArgType -> <:expr< Genarg.rawwit_string >>
+  | PreIdentArgType -> <:expr< Genarg.rawwit_pre_ident >>
+  | IdentArgType -> <:expr< Genarg.rawwit_ident >>
+  | QualidArgType -> <:expr< Genarg.rawwit_qualid >>
+  | ConstrArgType -> <:expr< Genarg.rawwit_constr >>
+  | ConstrMayEvalArgType -> <:expr< Genarg.rawwit_constr_may_eval >>
+  | QuantHypArgType -> <:expr< Genarg.rawwit_quant_hyp >>
+  | TacticArgType -> <:expr< Genarg.rawwit_tactic >>
+  | RedExprArgType -> <:expr< Genarg.rawwit_red_expr >>
+  | CastedOpenConstrArgType -> <:expr< Genarg.rawwit_casted_open_constr >>
+  | ConstrWithBindingsArgType -> <:expr< Genarg.rawwit_constr_with_bindings >>
+  | List0ArgType t -> <:expr< Genarg.wit_list0 $make_rawwit loc t$ >>
+  | List1ArgType t -> <:expr< Genarg.wit_list1 $make_rawwit loc t$ >>
+  | OptArgType t -> <:expr< Genarg.wit_opt $make_rawwit loc t$ >>
+  | PairArgType (t1,t2) -> 
+      <:expr< Genarg.wit_pair $make_rawwit loc t1$ $make_rawwit loc t2$ >>
+  | ExtraArgType s -> <:expr< $lid:"rawwit_"^s$ >>
+
+let rec make_wit loc = function
+  | BoolArgType -> <:expr< Genarg.wit_bool >>
+  | IntArgType -> <:expr< Genarg.wit_int >>
+  | IntOrVarArgType -> <:expr< Genarg.wit_int_or_var >>
+  | StringArgType -> <:expr< Genarg.wit_string >>
+  | PreIdentArgType -> <:expr< Genarg.wit_pre_ident >>
+  | IdentArgType -> <:expr< Genarg.wit_ident >>
+  | QualidArgType -> <:expr< Genarg.wit_qualid >>
+  | QuantHypArgType -> <:expr< Genarg.wit_quant_hyp >>
+  | ConstrArgType -> <:expr< Genarg.wit_constr >>
+  | ConstrMayEvalArgType -> <:expr< Genarg.wit_constr_may_eval >>
+  | TacticArgType -> <:expr< Genarg.wit_tactic >>
+  | RedExprArgType -> <:expr< Genarg.wit_red_expr >>
+  | CastedOpenConstrArgType -> <:expr< Genarg.wit_casted_open_constr >>
+  | ConstrWithBindingsArgType -> <:expr< Genarg.wit_constr_with_bindings >>
+  | List0ArgType t -> <:expr< Genarg.wit_list0 $make_wit loc t$ >>
+  | List1ArgType t -> <:expr< Genarg.wit_list1 $make_wit loc t$ >>
+  | OptArgType t -> <:expr< Genarg.wit_opt $make_wit loc t$ >>
+  | PairArgType (t1,t2) -> 
+      <:expr< Genarg.wit_pair $make_wit loc t1$ $make_wit loc t2$ >>
+  | ExtraArgType s -> <:expr< $lid:"wit_"^s$ >>
+
+let make_act loc act pil =
+  let rec make = function
+    | [] -> <:expr< Gramext.action (fun loc -> ($act$ : 'a)) >>
+    | None :: tl -> <:expr< Gramext.action (fun _ -> $make tl$) >>
+    | Some (p, t) :: tl ->
+	<:expr<
+          Gramext.action 
+            (fun $lid:p$ -> let _ = in_gen $make_rawwit loc t$ $lid:p$ in $make tl$)
+        >> in
+  make (List.rev pil)
+
+let make_rule loc (prods,act) =
+  let (symbs,pil) = List.split prods in
+  <:expr< ($mlexpr_of_list (fun x -> x) symbs$,$make_act loc act pil$) >>
+
+let declare_tactic_argument loc s typ pr f rawtyppr cl =
+  let interp = match f with
+    | None -> <:expr< Tacinterp.genarg_interp >>
+    | Some f -> <:expr< $lid:f$>> in
+  let rawtyp, rawpr = match rawtyppr with
+    | None -> typ,pr
+    | Some (t,p) -> t,p in
+  let se = mlexpr_of_string s in
+  let wit = <:expr< $lid:"wit_"^s$ >> in
+  let rawwit = <:expr< $lid:"rawwit_"^s$ >> in
+  let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in
+  <:str_item<
+    declare
+      value ($lid:"wit_"^s$, $lid:"rawwit_"^s$) = Genarg.create_arg $se$;
+      value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$;
+      Tacinterp.add_genarg_interp $se$
+        (fun ist x ->
+          (in_gen $wit$
+             (out_gen $make_wit loc typ$
+          	($interp$ ist
+         	  (in_gen $make_rawwit loc rawtyp$
+	             (out_gen $rawwit$ x))))));
+      Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.Entry.e 'a) None 
+        [(None, None, $rules$)];
+      Pptactic.declare_extra_genarg_pprule
+        ($rawwit$, $lid:rawpr$)
+        ($wit$, $lid:pr$);
+    end
+  >>
+
+let declare_vernac_argument loc s cl =
+  let se = mlexpr_of_string s in
+  let typ = ExtraArgType s in
+  let wit = <:expr< $lid:"wit_"^s$ >> in
+  let rawwit = <:expr< $lid:"rawwit_"^s$ >> in
+  let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in
+  <:str_item<
+    declare
+      value $lid:"rawwit_"^s$ = snd (Genarg.create_arg $se$);
+      value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$;
+      Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.Entry.e 'a) None 
+        [(None, None, $rules$)];
+    end
+  >>
+
+open Vernacexpr
+open Pcoq
+
+let rec interp_entry_name loc s =
+  let l = String.length s in
+  if l > 8 & String.sub s 0 3 = "ne_" & String.sub s (l-5) 5 = "_list" then
+    let t, g = interp_entry_name loc (String.sub s 3 (l-8)) in
+    List1ArgType t, <:expr< Gramext.Slist1 $g$ >>
+  else if l > 5 & String.sub s (l-5) 5 = "_list" then
+    let t, g = interp_entry_name loc (String.sub s 0 (l-5)) in
+    List0ArgType t, <:expr< Gramext.Slist0 $g$ >>
+  else if l > 4 & String.sub s (l-4) 4 = "_opt" then
+    let t, g = interp_entry_name loc (String.sub s 0 (l-4)) in
+    OptArgType t, <:expr< Gramext.Sopt $g$ >>
+  else 
+    let t, se =
+      match Pcoq.entry_type (Pcoq.get_univ "prim") s with
+	| Some _ as x -> x, <:expr< Prim. $lid:s$ >>
+	| None -> 
+      match Pcoq.entry_type (Pcoq.get_univ "constr") s with
+	| Some _ as x -> x, <:expr< Constr. $lid:s$ >>
+	| None -> 
+      match Pcoq.entry_type (Pcoq.get_univ "tactic") s with
+	| Some _ as x -> x, <:expr< Tactic. $lid:s$ >>
+	| None -> None, <:expr< $lid:s$ >> in
+    let t =
+      match t with
+	| Some (GenAstType t) -> t
+	| Some _ -> 
+	    failwith "Only entries of generic type can be used in extension"
+	| None ->
+(*	    Pp.warning_with Pp_control.err_ft
+            ("Unknown primitive grammar entry: "^s);*)
+	    ExtraArgType s
+    in t, <:expr< Gramext.Snterm (Pcoq.Gram.Entry.obj $se$) >>
+
+open Pcaml
+
+EXTEND
+  GLOBAL: str_item;
+  str_item:
+    [ [ "ARGUMENT"; "EXTEND"; s = [ UIDENT | LIDENT ];
+        "TYPED"; "AS"; typ = argtype;
+        "PRINTED"; "BY"; pr = LIDENT;
+        f = OPT [ "INTERPRETED"; "BY"; f = LIDENT -> f ];
+        rawtyppr =
+          OPT [ "RAW"; "TYPED"; "AS"; t = argtype; 
+                "RAW"; "PRINTED"; "BY"; pr = LIDENT -> (t,pr) ];
+        OPT "|"; l = LIST1 argrule SEP "|";
+        "END" ->
+	  if String.capitalize s = s then
+	    failwith "Argument entry names must be lowercase";
+         declare_tactic_argument loc s typ pr f rawtyppr l
+      | "VERNAC"; "ARGUMENT"; "EXTEND"; s = [ UIDENT | LIDENT ];
+        OPT "|"; l = LIST1 argrule SEP "|";
+        "END" ->
+	  if String.capitalize s = s then
+	    failwith "Argument entry names must be lowercase";
+         declare_vernac_argument loc s l ] ]
+  ;
+  argtype:
+    [ [ e = LIDENT -> fst (interp_entry_name loc e) ] ]
+  ;
+  argrule:
+    [ [ "["; l = LIST0 genarg; "]"; "->"; "["; e = Pcaml.expr; "]" -> (l,e) ] ]
+  ;
+  genarg:
+    [ [ e = LIDENT; "("; s = LIDENT; ")" ->
+        let t, g = interp_entry_name loc e in (g, Some (s,t))
+      | s = STRING ->
+	  if String.length s > 0 && Util.is_letter s.[0] then
+	    Pcoq.lexer.Token.using ("", s);
+        (<:expr< (Gramext.Stoken (Extend.terminal $str:s$)) >>, None)
+    ] ]
+  ;
+  END
+
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index 718df16197..eb95779021 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -69,13 +69,22 @@ let rec make_let e = function
 let add_clause s (_,pt,e) l =
   let p = make_patt pt in
   let w = Some (make_when (MLast.loc_of_expr e) pt) in
-  if List.exists (fun (p',w',_) -> p=p' & w=w') l then
+  (p, w, make_let e pt)::l
+
+let rec extract_signature = function
+  | [] -> []
+  | TacNonTerm (_,t,_,_) :: l -> t :: extract_signature l
+  | _::l -> extract_signature l
+
+let check_unicity s l =
+  let l' = List.map (fun (_,l,_) -> extract_signature l) l in
+  if not (Util.list_distinct l') then
     Pp.warning_with Pp_control.err_ft
       ("Two distinct rules of tactic entry "^s^" have the same\n"^
-      "non-terminals in the same order: put them in distinct tactic entries");
-  (p, w, make_let e pt)::l
+      "non-terminals in the same order: put them in distinct tactic entries")
 
 let make_clauses s l =
+  check_unicity s l;
   let default =
     (<:patt< _ >>,None,<:expr< failwith "Tactic extension: cannot occur" >>) in
   List.fold_right (add_clause s) l [default]
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 099bfb3e58..8ab6d23ab5 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -380,6 +380,9 @@ let _ =
 TACTIC EXTEND EAuto
 | [ "EAuto" int_or_var_opt(n) int_or_var_opt(p) hintbases(db) ] ->
     [ gen_eauto false (make_dimension n p) db ]
+END
+
+TACTIC EXTEND EAutoDebug
 | [ "EAutod" int_or_var_opt(n) int_or_var_opt(p) hintbases(db) ] ->
     [ gen_eauto true (make_dimension n p) db ]
 END
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 4a2917c4d7..fd732563a5 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -16,6 +16,17 @@ open Genarg
 
 (* Rewriting orientation *)
 
+let _ = Metasyntax.add_token_obj "<-"
+let _ = Metasyntax.add_token_obj "->"
+
+let pr_orient = function true -> Pp.str " ->" | false -> Pp.str " <-"
+
+ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient
+| [ "->" ] -> [ true ]
+| [ "<-" ] -> [ false ]
+| [ ] -> [ true ]
+END
+(*
 let wit_orient, rawwit_orient = Genarg.create_arg "orient"
 let orient = Pcoq.create_generic_entry "orient" rawwit_orient
 let _ = Tacinterp.add_genarg_interp "orient"
@@ -43,10 +54,30 @@ let _ =
   Pptactic.declare_extra_genarg_pprule
     (rawwit_orient, pr_orient)
     (wit_orient, pr_orient)
-
+*)
  
 (* with_constr *)
 
+open Tacinterp
+
+let pr_with_constr_gen prc = function 
+  | None -> Pp.mt ()
+  | Some c -> Pp.str " with" ++ prc c
+
+let rawpr_with_constr = pr_with_constr_gen Ppconstr.pr_constr
+let pr_with_constr = pr_with_constr_gen Printer.prterm
+
+ARGUMENT EXTEND with_constr
+  TYPED AS constr_opt 
+  PRINTED BY pr_with_constr 
+  INTERPRETED BY genarg_interp
+  RAW TYPED AS constr_opt
+  RAW PRINTED BY rawpr_with_constr
+| [ "with" constr(c) ] -> [ Some c ]
+| [ ] -> [ None ]
+END
+
+(*
 let wit_with_constr, rawwit_with_constr = Genarg.create_arg "with_constr"
 let with_constr = Pcoq.create_generic_entry "with_constr" rawwit_with_constr
 let _ = Tacinterp.add_genarg_interp "with_constr"
@@ -72,16 +103,4 @@ let _ =
   Pptactic.declare_extra_genarg_pprule
     (rawwit_with_constr, pr_with_constr Ppconstr.pr_constr)
     (wit_with_constr, pr_with_constr Printer.prterm)
-
-(*
-(* Clause *)
-let wit_clause, rawwit_clause = Genarg.create_arg "clause"
-let clause = Pcoq.create_generic_entry "clause" rawwit_clause
-let _ = Tacinterp.add_genarg_interp "clause"
-  (fun ist x ->
-    (in_gen wit_clause
-      (out_gen (wit_opt wit_constr)
-	(Tacinterp.genarg_interp ist
-	  (in_gen (wit_opt rawwit_constr)
-	    (out_gen rawwit_clause x))))))
 *)
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index bef676b6ac..8ff06745fd 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -208,7 +208,9 @@ END
 VERNAC COMMAND EXTEND DeriveDependentInversion
 | [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort(s) ]
   -> [ add_inversion_lemma_exn na c s true half_dinv_tac ]
+    END
 
+VERNAC COMMAND EXTEND DeriveDependentInversionClear
 | [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort(s) ]
   -> [ add_inversion_lemma_exn na c s true dinv_clear_tac ]
 END