Factorisation de la grammaire pour Extraction Language.

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

2 files changed, 20 insertions, 19 deletions

diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v
index e18e48efd..0f69bce4a 100644
--- a/contrib/extraction/Extraction.v
+++ b/contrib/extraction/Extraction.v
@@ -29,15 +29,9 @@ Grammar vernac vernac : ast :=
 
 (* Target Language *)
 
-| extraction_ocaml 
-     [ "Extraction" "Language" "Ocaml" "." ] 
-  -> [ (ExtractionLangOcaml) ]
-| extraction_haskell 
-     [ "Extraction" "Language" "Haskell" "." ] 
-  -> [ (ExtractionLangHaskell) ]
-| extraction_toplevel
-     [ "Extraction" "Language" "Toplevel" "." ] 
-  -> [ (ExtractionLangToplevel) ]
+| extr_language 
+     [ "Extraction" "Language" extraction_language($l) "." ] 
+  -> [ (ExtractionLang $l) ]
 
 (* Custom inlining directives *)
 | inline_constant
@@ -82,5 +76,11 @@ with idorstring_list: ast list :=
 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/table.ml b/contrib/extraction/table.ml
index 21e74334d..896203486 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -90,7 +90,7 @@ let lang_ref = ref Ocaml
 
 let lang () = !lang_ref
 
-let (extraction_language,_) = 
+let (extr_lang,_) = 
   declare_object ("Extraction Lang", 
 		  {cache_function = (fun (_,l) -> lang_ref := l);
 		   load_function = (fun (_,l) -> lang_ref := l);
@@ -103,17 +103,18 @@ let _ = declare_summary "Extraction Lang"
 	    init_function = (fun () -> lang_ref := Ocaml);
 	    survive_section = true }  
 
-let _ = 
-  vinterp_add "ExtractionLangOcaml" 
-     (fun _ () -> add_anonymous_leaf (extraction_language Ocaml))
-    
-let _ = 
-  vinterp_add "ExtractionLangHaskell" 
-     (fun _ () -> add_anonymous_leaf (extraction_language Haskell))
+let lang_to_lang = function 
+    "Ocaml" -> Ocaml 
+  | "Haskell" -> Haskell 
+  | "Toplevel" -> Toplevel
+  | _ -> assert false
 
 let _ = 
-  vinterp_add "ExtractionLangToplevel" 
-     (fun _ () -> add_anonymous_leaf (extraction_language Toplevel))
+  vinterp_add "ExtractionLang" 
+     (function 
+	  [VARG_STRING l] -> 
+	    (fun () -> add_anonymous_leaf (extr_lang (lang_to_lang l)))
+	| _ -> assert false)
 
 (*s Table for custom inlining *)