Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et commandes vernaculaires (cf dev/changements.txt pour plus de précisions)

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

5 files changed, 92 insertions, 223 deletions

diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v
deleted file mode 100644
index 0f69bce4a4..0000000000
--- a/contrib/extraction/Extraction.v
+++ /dev/null
@@ -1,86 +0,0 @@
-(***********************************************************************)
-(*  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       *)
-(***********************************************************************)
-
-Grammar vernac vernac : ast :=
-
-(* Extraction in the Coq toplevel *)
-  extr_constr [ "Extraction" constrarg($c) "." ] -> 
-              [ (Extraction $c) ]
-| extr_list   [ "Recursive" "Extraction" ne_qualidarg_list($l) "." ] ->
-              [ (ExtractionRec ($LIST $l)) ]
-
-(* Monolithic extraction to a file *)
-| extr_file
-     [ "Extraction" stringarg($f) ne_qualidarg_list($l) "." ] 
-  -> [ (ExtractionFile $f ($LIST $l)) ]
-
-(* Modular extraction (one Coq module = one ML module) *)
-| extr_module 
-     [ "Extraction" "Module" identarg($m) "." ]
-  -> [ (ExtractionModule $m) ]
-| rec_extr_module 
-     [ "Recursive" "Extraction" "Module" identarg($m) "." ]
-  -> [ (RecursiveExtractionModule $m) ]
-
-(* Target Language *)
-
-| extr_language 
-     [ "Extraction" "Language" extraction_language($l) "." ] 
-  -> [ (ExtractionLang $l) ]
-
-(* Custom inlining directives *)
-| inline_constant
-     [ "Extraction" "Inline" ne_qualidarg_list($l) "." ] 
-  -> [ (ExtractionInline ($LIST $l)) ]
-     
-| no_inline_constant 
-     [ "Extraction" "NoInline" ne_qualidarg_list($l) "." ] 
-  -> [ (ExtractionNoInline ($LIST $l)) ]
-
-| print_inline_constant 
-     [ "Print" "Extraction" "Inline" "."]
-  -> [ (PrintExtractionInline) ]
-
-| reset_inline_constant 
-     [ "Reset" "Extraction" "Inline" "."]
-  -> [ (ResetExtractionInline) ]
-
-(* Overriding of a Coq object by an ML one *)
-| extract_constant 
-     [ "Extract" "Constant" qualidarg($x) "=>" idorstring($y) "." ]
-  -> [ (ExtractConstant $x $y) ]
-
-| extract_inlined_constant 
-     [ "Extract" "Inlined" "Constant" qualidarg($x) 
-      "=>" idorstring($y) "." ]
-  -> [ (ExtractInlinedConstant $x $y) ]
-
-| extract_inductive 
-     [ "Extract" "Inductive" qualidarg($x) "=>" mindnames($y) "."]
-  -> [ (ExtractInductive $x $y) ]
-
-(* Utility entries *)
-with mindnames : ast :=
-  mlconstr [ idorstring($id) "[" idorstring_list($idl) "]" ]
-        -> [(VERNACARGLIST $id ($LIST $idl))]
-
-with idorstring_list: ast list :=
-  ids_nil  [ ] -> [ ]
-| ids_cons [ idorstring($x) idorstring_list($l) ] -> [ $x ($LIST $l) ]
-
-with idorstring : ast :=
-  ids_ident  [ identarg($id) ] -> [ $id ]
-| ids_string [ stringarg($s) ] -> [ $s ]
-
-with extraction_language : ast := 
-  ocaml [ "Ocaml" ] -> [ "Ocaml" ]
-| haskell [ "Haskell" ] -> [ "Haskell" ]
-| toplevel [ "Toplevel" ] -> [ "Toplevel" ]
-
-.
-
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index ecfd5e2ea8..db2e7d4f93 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -241,40 +241,33 @@ let extract_reference r =
       else List.find (decl_in_r r) decls
       in msgnl (pp_decl d)
 
-let _ = 
-  vinterp_add "Extraction"
-    (function 
-       | [VARG_CONSTR ast] ->
-	   (fun () -> 
-	      set_globals ();
-	      let c = Astterm.interp_constr Evd.empty (Global.env()) ast in
-	      match kind_of_term c with
-		(* If it is a global reference, then output the declaration *)
-		| Const sp -> extract_reference (ConstRef sp)
-		| Ind ind -> extract_reference (IndRef ind)
-		| Construct cs -> extract_reference (ConstructRef cs)
-		(* Otherwise, output the ML type or expression *)
-		| _ ->
-		    match extract_constr (Global.env()) c with
-		      | Emltype (t,_,_) -> msgnl (pp_type t ++ fnl ())
-		      | Emlterm a -> msgnl (pp_ast (normalize a) ++ fnl ()))
-       | _ -> assert false)
+let extraction rawconstr =
+  set_globals ();
+  let c = Astterm.interp_constr Evd.empty (Global.env()) rawconstr in
+  match kind_of_term c with
+    (* If it is a global reference, then output the declaration *)
+    | Const sp -> extract_reference (ConstRef sp)
+    | Ind ind -> extract_reference (IndRef ind)
+    | Construct cs -> extract_reference (ConstructRef cs)
+    (* Otherwise, output the ML type or expression *)
+    | _ ->
+	match extract_constr (Global.env()) c with
+	  | Emltype (t,_,_) -> msgnl (pp_type t ++ fnl ())
+	  | Emlterm a -> msgnl (pp_ast (normalize a) ++ fnl ())
 
 (*s Recursive extraction in the Coq toplevel. The vernacular command is
     \verb!Recursive Extraction! [qualid1] ... [qualidn]. We use [extract_env]
     to get the saturated environment to extract. *)
 
 let mono_extraction (f,m) vl = 
-  let refs = refs_of_vargl vl in
+  let refs = List.map Nametab.global vl in
   let prm = {modular=false; mod_name = m; to_appear= refs} in
   let decls = decl_of_refs refs in 
   let decls = add_ml_decls prm decls in 
   let decls = optimize prm decls in
   extract_to_file f prm decls
 
-let _ = 
-  vinterp_add "ExtractionRec"
-    (fun vl () -> mono_extraction (None,id_of_string "Main") vl)
+let extraction_rec = mono_extraction (None,id_of_string "Main")
 
 (*s Extraction to a file (necessarily recursive). 
     The vernacular command is \verb!Extraction "file"! [qualid1] ... [qualidn].
@@ -297,14 +290,9 @@ let lang_error () =
      ++ fnl () ++
      str "You should use Extraction Language Ocaml or Haskell before.") 
 
-let _ = 
-  vinterp_add "ExtractionFile"
-    (function 
-       | VARG_STRING f :: vl ->
-	   (fun () -> 
-	      if lang () = Toplevel then lang_error () 
-	      else mono_extraction (filename f) vl) 
-       | _ -> assert false)
+let extraction_file f vl =
+  if lang () = Toplevel then lang_error () 
+  else mono_extraction (filename f) vl
 
 (*s Extraction of a module. The vernacular command is 
   \verb!Extraction Module! [M]. *) 
@@ -322,48 +310,37 @@ let module_file_name m = match lang () with
   | Haskell -> (String.capitalize (string_of_id m)) ^ ".hs"
   | Toplevel -> assert false
 
-let _ = 
-  vinterp_add "ExtractionModule"
-    (function 
-       | [VARG_IDENTIFIER m] ->
-	   (fun () -> 
-	      if lang () = Toplevel then lang_error () 
-	      else 
-		let dir_m = module_of_id m in 
-		let f = module_file_name m in
-		let prm = {modular=true; mod_name=m; to_appear=[]} in 
-		let rl = extract_module dir_m in 
-		let decls = optimize prm (decl_of_refs rl) in
-		let decls = add_ml_decls prm decls in 
-		check_one_module dir_m decls; 
-		let decls = List.filter (decl_in_m dir_m) decls in
-		extract_to_file (Some f) prm decls)
-       | _ -> assert false)
+let extraction_module m =
+  if lang () = Toplevel then lang_error () 
+  else 
+    let dir_m = module_of_id m in 
+    let f = module_file_name m in
+    let prm = {modular=true; mod_name=m; to_appear=[]} in 
+    let rl = extract_module dir_m in 
+    let decls = optimize prm (decl_of_refs rl) in
+    let decls = add_ml_decls prm decls in 
+    check_one_module dir_m decls; 
+    let decls = List.filter (decl_in_m dir_m) decls in
+    extract_to_file (Some f) prm decls
 
 (*s Recursive Extraction of all the modules [M] depends on. 
   The vernacular command is \verb!Recursive Extraction Module! [M]. *) 
 
-let _ = 
-  vinterp_add "RecursiveExtractionModule"
-        (function 
-       | [VARG_IDENTIFIER m] ->
-	   (fun () -> 
-	      if lang () = Toplevel then lang_error () 
-	      else 
-		let dir_m = module_of_id m in 
-		let modules,refs = 
-		  modules_extract_env dir_m in
-		check_modules modules; 
-		let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in
-		let decls = optimize dummy_prm (decl_of_refs refs) in
-		let decls = add_ml_decls dummy_prm decls in
-		Dirset.iter 
-		  (fun m ->
-		     let short_m = snd (split_dirpath m) in
-		     let f = module_file_name short_m in 
-		     let prm = {modular=true;mod_name=short_m;to_appear=[]} in 
-		     let decls = List.filter (decl_in_m m) decls in
-		     if decls <> [] then extract_to_file (Some f) prm decls)
-		  modules)
-       | _ -> assert false)
-
+let recursive_extraction_module m =
+  if lang () = Toplevel then lang_error () 
+  else 
+    let dir_m = module_of_id m in 
+    let modules,refs = 
+      modules_extract_env dir_m in
+    check_modules modules; 
+    let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in
+    let decls = optimize dummy_prm (decl_of_refs refs) in
+    let decls = add_ml_decls dummy_prm decls in
+    Dirset.iter 
+      (fun m ->
+	let short_m = snd (split_dirpath m) in
+	let f = module_file_name short_m in 
+	let prm = {modular=true;mod_name=short_m;to_appear=[]} in 
+	let decls = List.filter (decl_in_m m) decls in
+	if decls <> [] then extract_to_file (Some f) prm decls)
+      modules
diff --git a/contrib/extraction/extract_env.mli b/contrib/extraction/extract_env.mli
index 710e801d12..1cdb5c02c3 100644
--- a/contrib/extraction/extract_env.mli
+++ b/contrib/extraction/extract_env.mli
@@ -10,3 +10,12 @@
 
 (*s This module declares the extraction commands. *)
 
+open Util
+open Names
+open Nametab
+
+val extraction : Genarg.constr_ast -> unit
+val extraction_rec : qualid located list -> unit
+val extraction_file : string -> qualid located list -> unit
+val extraction_module : identifier -> unit
+val recursive_extraction_module : identifier -> unit
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 896203486b..ee7267f3f6 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -13,6 +13,7 @@ open Lib
 open Libobject
 open Goptions
 open Vernacinterp
+open Extend
 open Names
 open Util
 open Pp
@@ -66,21 +67,25 @@ let check_constant r =
   else errorlabstrm "extract_constant"
 	(Printer.pr_global r ++ spc () ++ str "is not a constant.") 
 
+(*
 let string_of_varg = function
   | VARG_IDENTIFIER id -> string_of_id id
   | VARG_STRING s -> s
   | _ -> assert false
+*)
 
 let no_such_reference q =
   errorlabstrm "reference_of_varg" 
     (str "There is no such reference " ++ Nametab.pr_qualid q ++ str ".")
 
+(*
 let reference_of_varg = function
   | VARG_QUALID q -> 
       (try Nametab.locate q with Not_found -> no_such_reference q)
   | _ -> assert false
 
 let refs_of_vargl = List.map reference_of_varg
+*)
 
 (*s Target Language *)
 
@@ -103,18 +108,7 @@ let _ = declare_summary "Extraction Lang"
 	    init_function = (fun () -> lang_ref := Ocaml);
 	    survive_section = true }  
 
-let lang_to_lang = function 
-    "Ocaml" -> Ocaml 
-  | "Haskell" -> Haskell 
-  | "Toplevel" -> Toplevel
-  | _ -> assert false
-
-let _ = 
-  vinterp_add "ExtractionLang" 
-     (function 
-	  [VARG_STRING l] -> 
-	    (fun () -> add_anonymous_leaf (extr_lang (lang_to_lang l)))
-	| _ -> assert false)
+let extraction_language x = add_anonymous_leaf (extr_lang x)
 
 (*s Table for custom inlining *)
 
@@ -150,21 +144,13 @@ let _ = declare_summary "Extraction Inline"
 
 (*s Grammar entries. *)
 
-let _ = 
-  vinterp_add "ExtractionInline"
-    (fun vl () -> 
-       let refs = List.map check_constant (refs_of_vargl vl) in 
-       add_anonymous_leaf (inline_extraction (true,refs)))
-
-let _ = 
-  vinterp_add "ExtractionNoInline"
-    (fun vl () -> 
-       let refs = List.map check_constant (refs_of_vargl vl) in 
-       add_anonymous_leaf (inline_extraction (false,refs)))
+let extraction_inline b vl =
+  let refs = List.map (fun x -> check_constant (Nametab.global x)) vl in 
+  add_anonymous_leaf (inline_extraction (true,refs))
 
 (*s Printing part *)
 
-let print_inline () = 
+let print_extraction_inline () = 
   let (i,n)= !inline_table in 
   let i'= Refset.filter is_constant i in 
   msg 
@@ -177,9 +163,6 @@ let print_inline () =
        (fun r p -> 
 	  (p ++ str "   " ++ Printer.pr_global r ++ fnl ())) n (mt ()))
 
-let _ = vinterp_add "PrintExtractionInline" (fun _ -> print_inline)
-
-
 (*s Reset part *)
 
 let (reset_inline,_) = 
@@ -189,10 +172,8 @@ let (reset_inline,_) =
 	load_function = (fun (_,_)-> inline_table :=  empty_inline_table); 
 	open_function = (fun _ -> ());
 	export_function = (fun x -> Some x) })
-	
-let _ = vinterp_add "ResetExtractionInline" 
-	  (fun _ () -> add_anonymous_leaf (reset_inline ()))
-	  
+
+let reset_extraction_inline () = add_anonymous_leaf (reset_inline ())
 
 (*s Table for direct ML extractions. *)
 
@@ -235,30 +216,13 @@ let _ = declare_summary "ML extractions"
 
 (*s Grammar entries. *)
 
-let _ = 
-  vinterp_add "ExtractConstant"
-    (function 
-       | [id; vs] -> 
-	   (fun () -> 
-	      let r = check_constant (reference_of_varg id) in 
-	      let s = string_of_varg vs in 
-	      add_anonymous_leaf (inline_extraction (false,[r]));
-	      add_anonymous_leaf (in_ml_extraction (r,s)))
-       | _ -> assert false)
-
-let _ = 
-  vinterp_add "ExtractInlinedConstant"
-    (function 
-       | [id; vs] -> 
-	   (fun () -> 
-	      let r = check_constant (reference_of_varg id) in 
-	      let s = string_of_varg vs in 
-	      add_anonymous_leaf (inline_extraction (true,[r]));
-	      add_anonymous_leaf (in_ml_extraction (r,s)))
-       | _ -> assert false)
-
-
-let extract_inductive r (id2,l2) = match r with
+let extract_constant_inline inline qid s =
+  let r = check_constant (Nametab.global qid) in
+  add_anonymous_leaf (inline_extraction (inline,[r]));
+  add_anonymous_leaf (in_ml_extraction (r,s))
+
+let extract_inductive r (id2,l2) =
+  let r = Nametab.global r in match r with
   | IndRef ((sp,i) as ip) ->
       let mib = Global.lookup_mind sp in
       let n = Array.length mib.mind_packets.(i).mind_consnames in
@@ -273,13 +237,3 @@ let extract_inductive r (id2,l2) = match r with
   | _ -> 
       errorlabstrm "extract_inductive"
 	(Printer.pr_global r ++ spc () ++ str "is not an inductive type.")
-
-let _ = 
-  vinterp_add "ExtractInductive"
-    (function 
-       | [q1; VARG_VARGLIST (id2 :: l2)] ->
-	   (fun () -> 
-	      extract_inductive (reference_of_varg q1) 
-		(string_of_varg id2, List.map string_of_varg l2))
-       | _ -> assert false)
-
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index a6cde3c5f2..9fa7142ce8 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -28,7 +28,7 @@ module Refset : Set.S with type elt = global_reference
 		      
 val check_constant : global_reference -> global_reference
 
-val refs_of_vargl : vernac_arg list -> global_reference list
+(*val refs_of_vargl : Extend.vernac_arg list -> global_reference list*)
 
 (*s Target language. *)
 
@@ -52,3 +52,18 @@ val ml_extractions : unit -> Refset.t
 
 val sorted_ml_extractions : unit -> (global_reference * string) list
 
+(*s Extraction commands. *)
+
+open Util
+
+val extraction_language : lang -> unit
+
+val extraction_inline : bool -> qualid located list -> unit
+
+val print_extraction_inline : unit -> unit
+
+val reset_extraction_inline : unit -> unit
+
+val extract_constant_inline : bool -> qualid located -> string -> unit
+
+val extract_inductive : qualid located -> string * string list -> unit