Parsing

- Typage renforcé dans les grammaires (distinction des vars et des metavars)
- Disparition de SLAM au profit de ABSTRACT
- Paths primitifs dans les quotations (syntaxe concrète à base de .)
- Mise en place de identifier dès le type ast
- Protection de identifier contre les effets de bord via un String.copy
- Utilisation de module_ident (= identifier) dans les dir_path (au
  lieu de string)

Table des noms qualifiés

- Remplacement de la table de visibilité par une table qui ne cache
  plus les noms de modules et sections mais seulement les noms des
  constantes (e.g. Require A. ne cachera plus le contenu d'un éventuel
  module A déjà existant : seuls les noms de constructions de l'ancien
  A qui existent aussi dans le nouveau A seront cachés)
- Renoncement à la possibilité d'accéder les formes non déchargées des
  constantes définies à l'intérieur de sections et simplification
  connexes (suppression de END-SECTION, une seule table de noms qui ne
  survit pas au discharge)
- Utilisation de noms longs pour les modules, de noms qualifiés pour
  Require and co, tests de cohérence; pour être cohérent avec la non
  survie des tables de noms à la sortie des section, les require à
  l'intérieur d'une section eux aussi sont refaits à la fermeture de la
  section


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

4 files changed, 12 insertions, 9 deletions

diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index da3d464bbd..ba4c4a6163 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -215,6 +215,7 @@ let _ =
     those having an ML extraction. *)
 
 let extract_module m =
+  let m = Nametab.locate_loaded_library (Nametab.make_qualid [] m) in
   let seg = Library.module_segment (Some m) in
   let get_reference = function
     | sp, Leaf o ->
@@ -242,10 +243,10 @@ let _ =
     (function 
        | [VARG_STRING lang; VARG_VARGLIST o; VARG_IDENTIFIER m] ->
 	   (fun () -> 
-	      let m = Names.string_of_id m in
-	      Ocaml.current_module := m;
-	      let f = (String.uncapitalize m) ^ (file_suffix lang) in
-	      let prm = interp_options lang [] true m o in
+	      Ocaml.current_module := Some m;
+	      let ms = Names.string_of_id m in
+	      let f = (String.uncapitalize ms) ^ (file_suffix lang) in
+	      let prm = interp_options lang [] true ms o in
 	      let rl = extract_module m in 
 	      let decls = optimize prm (decl_of_refs rl) in
 	      let decls = List.filter (decl_mem rl) decls in
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 827381d1c5..98ea283c71 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -385,7 +385,8 @@ module ModularParams = struct
     in
     let m = list_last (dirpath sp) in
     id_of_string 
-      (if m = !current_module then s else (String.capitalize m) ^ "." ^ s)
+      (if Some m = !current_module then s
+      else (String.capitalize (string_of_id m)) ^ "." ^ s)
 
   let rename_type_global r = 
     let id = Environ.id_of_global (Global.env()) r in 
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 750afc7822..960edb58a1 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -395,7 +395,7 @@ module MonoPp = Make(MonoParams)
 
 (*s Renaming issues in a modular extraction. *)
 
-let current_module = ref ""
+let current_module = ref None
 
 module ModularParams = struct
 
@@ -424,7 +424,8 @@ module ModularParams = struct
     in
     let m = list_last (dirpath sp) in
     id_of_string 
-      (if m = !current_module then s else (String.capitalize m) ^ "." ^ s)
+      (if Some m = !current_module then s 
+       else (String.capitalize (string_of_id m)) ^ "." ^ s)
 
   let rename_type_global r = 
     let id = Environ.id_of_global (Global.env()) r in 
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index 057d909fa4..6ab76aded6 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -22,7 +22,7 @@ val collect_lambda : ml_ast -> identifier list * ml_ast
 val push_vars : identifier list -> identifier list * Idset.t ->
   identifier list * (identifier list * Idset.t)
 
-val current_module : string ref
+val current_module : identifier option ref
 
 (*s Production of Ocaml syntax. We export both a functor to be used for 
     extraction in the Coq toplevel and a function to extract some 
@@ -32,7 +32,7 @@ open Mlutil
 
 module Make : functor(P : Mlpp_param) -> Mlpp
 
-val current_module : string ref
+val current_module : Names.identifier option ref
 val extract_to_file : string -> extraction_params -> ml_decl list -> unit