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

13 files changed, 41 insertions, 37 deletions

diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index ecc17253a..d13be7720 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -48,7 +48,7 @@ let tuple_n n =
       (fun i -> 
 	 let id = id_of_string 
 		    ("proj_" ^ string_of_int n ^ "_" ^ string_of_int i) in
-	 (false, (id, true, Ast.nvar ("T" ^ string_of_int i))))
+	 (false, (id, true, Ast.nvar (id_of_string ("T" ^ string_of_int i)))))
       l1n 
   in
   let cons = id_of_string ("Build_tuple_" ^ string_of_int n) in
diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index d6a15959b..c885242bd 100644
--- a/contrib/correctness/pmisc.ml
+++ b/contrib/correctness/pmisc.ml
@@ -120,23 +120,19 @@ let subst_in_constr alist =
   replace_vars alist'
 
 let subst_in_ast alist ast =
-  let alist' = 
-    List.map (fun (id,id') -> (string_of_id id,string_of_id id')) alist in
   let rec subst = function
-      Nvar(l,s) -> Nvar(l,try List.assoc s alist' with Not_found -> s)
+      Nvar(l,s) -> Nvar(l,try List.assoc s alist with Not_found -> s)
     | Node(l,s,args) -> Node(l,s,List.map subst args)
-    | Slam(l,so,a) -> Slam(l,so,subst a) (* TODO:enlever so de alist' ? *)
+    | Slam(l,so,a) -> Slam(l,so,subst a) (* TODO:enlever so de alist ? *)
     | x -> x
   in
     subst ast
 
 let subst_ast_in_ast alist ast =
-  let alist' = 
-    List.map (fun (id,a) -> (string_of_id id,a)) alist in
   let rec subst = function
-      Nvar(l,s) as x -> (try List.assoc s alist' with Not_found -> x)
+      Nvar(l,s) as x -> (try List.assoc s alist with Not_found -> x)
     | Node(l,s,args) -> Node(l,s,List.map subst args)
-    | Slam(l,so,a) -> Slam(l,so,subst a) (* TODO:enlever so de alist' ? *)
+    | Slam(l,so,a) -> Slam(l,so,subst a) (* TODO:enlever so de alist ? *)
     | x -> x
   in
     subst ast
@@ -146,7 +142,8 @@ let real_subst_in_constr = replace_vars
 
 (* Coq constants *)
 
-let coq_constant d s = make_path ("Coq" :: d) (id_of_string s) CCI
+let coq_constant d s =
+  make_path (List.map id_of_string ("Coq" :: d)) (id_of_string s) CCI
 
 let bool_sp = coq_constant ["Init"; "Datatypes"] "bool"
 let coq_true = mkMutConstruct (((bool_sp,0),1), [||])
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index 5e0f9ad42..fc09cfa69 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -561,7 +561,7 @@ open Vernac
 GEXTEND Gram
   Pcoq.Vernac_.vernac:
   [ [ IDENT "Global"; "Variable"; 
-      l = LIST1 IDENT SEP ","; ":"; t = type_v; "." ->
+      l = LIST1 ident SEP ","; ":"; t = type_v; "." ->
 	let idl = List.map Ast.nvar l in
 	let d = Ast.dynamic (in_typev t) in
 	  <:ast< (PROGVARIABLE (VERNACARGLIST ($LIST $idl)) (VERNACDYN $d)) >>
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index da3d464bb..ba4c4a616 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 827381d1c..98ea283c7 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 750afc782..960edb58a 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 057d909fa..6ab76aded 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
 
 
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index 19b8534d1..926ca7951 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -23,7 +23,7 @@ let constr_of com = Astterm.interp_constr Evd.empty (Global.env()) com
 
 (* Construction of constants *)
 let constant dir s =
-  let dir = "Coq"::"field"::dir in
+  let dir = make_dirpath (List.map id_of_string ("Coq"::"field"::dir)) in
   let id = id_of_string s in
   try 
     Declare.global_reference_in_absolute_module dir id
@@ -115,7 +115,7 @@ let field g =
       | [|-(eq ?1 ? ?)] -> ?1
       |	[|-(eqT ?1 ? ?)] -> ?1>>) in
   let th = VArg (Constr (lookup typ)) in
-  (tac_interp [("FT",th)] [] (get_debug ()) <:tactic<Field_Gen FT>>) g
+  (tac_interp [(id_of_string "FT",th)] [] (get_debug ()) <:tactic<Field_Gen FT>>) g
 
 (* Declaration of Field *)
 let _ = hide_tactic "Field" (function _ -> field)
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 7307075be..7bf6441f7 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -220,7 +220,7 @@ let recognize_number t =
  This is the right way to access to Coq constants in tactics ML code *)
 
 let constant dir s =
-  let dir = "Coq"::dir in
+  let dir = make_dirpath (List.map id_of_string ("Coq"::dir)) in
   let id = id_of_string s in
   try 
     Declare.global_reference_in_absolute_module dir id
@@ -384,7 +384,7 @@ let coq_imp_simp = lazy (logic_constant ["Decidable"] "imp_simp")
 (* Section paths for unfold *)
 open Closure
 let make_coq_path dir s =
-  let dir = "Coq"::dir in
+  let dir = make_dirpath (List.map id_of_string ("Coq"::dir)) in
   let id = id_of_string s in
   let ref = 
     try Nametab.locate_in_absolute_module dir id 
diff --git a/contrib/ring/Setoid_ring_normalize.v b/contrib/ring/Setoid_ring_normalize.v
index 04e2aa16a..e49be3272 100644
--- a/contrib/ring/Setoid_ring_normalize.v
+++ b/contrib/ring/Setoid_ring_normalize.v
@@ -456,6 +456,8 @@ Proof.
   NewDestruct l;Trivial.
 Save.
 
+(* Hints Resolve ivl_aux_ok ics_aux_ok interp_m_ok. *)
+
 Lemma canonical_sum_merge_ok : (x,y:canonical_sum)
   (Aequiv (interp_cs (canonical_sum_merge x y))
   (Aplus (interp_cs x) (interp_cs y))).
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index 7908af7ec..10ca06b78 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -120,7 +120,7 @@ open Proof_type
   the constants are loaded in the environment *)
 
 let constant dir s =
-  let dir = "Coq"::"ring"::dir in
+  let dir = make_dirpath (List.map id_of_string ("Coq"::"ring"::dir)) in
   let id = id_of_string s in
   try 
     Declare.global_reference_in_absolute_module dir id
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index fad760cba..720c5a862 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -34,7 +34,7 @@ let mt_evd = Evd.empty
 let constr_of com = Astterm.interp_constr mt_evd (Global.env()) com
 
 let constant dir s =
-  let dir = "Coq"::dir in
+  let dir = make_dirpath (List.map id_of_string ("Coq"::dir)) in
   let id = id_of_string s in
   try 
     Declare.global_reference_in_absolute_module dir id
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 95a93cde7..6e7548596 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -100,7 +100,8 @@ let could_have_namesakes o sp =      (* namesake = omonimo in italian *)
 let uri_of_path sp tag =
  let module N = Names in
   let ext_of_sp sp = ext_of_tag tag in
-   "cic:/" ^ (String.concat "/" (N.wd_of_sp sp)) ^ "." ^ (ext_of_sp sp)
+  let dir = List.map N.string_of_id (N.wd_of_sp sp) in
+   "cic:/" ^ (String.concat "/" dir) ^ "." ^ (ext_of_sp sp)
 ;;
 
 let string_of_sort =
@@ -795,8 +796,8 @@ let mkfilename dn sp ext =
    match dn with
       None         -> None
     | Some basedir ->
-       Some (basedir ^ join_dirs basedir (N.wd_of_sp sp) ^
-        "." ^ ext)
+	let dir = List.map N.string_of_id (N.wd_of_sp sp) in
+       Some (basedir ^ join_dirs basedir dir ^ "." ^ ext)
 ;;
 
 (* print_object leaf_object id section_path directory_name formal_vars      *)
@@ -914,9 +915,10 @@ and print_node n id sp bprintleaf dn =
            print_if_verbose ("Suppongo gia' stampato " ^ Names.string_of_id id ^ "\n")
           end
        end
-   | L.OpenedSection (s,_) -> print_if_verbose ("OpenDir " ^ s ^ "\n")
-   | L.ClosedSection (_,s,state) ->
-      print_if_verbose("ClosedDir " ^ s ^ "\n") ;
+   | L.OpenedSection (id,_) ->
+       print_if_verbose ("OpenDir " ^ Names.string_of_id id ^ "\n")
+   | L.ClosedSection (_,id,state) ->
+      print_if_verbose("ClosedDir " ^ Names.string_of_id id ^ "\n") ;
       if bprintleaf then
        begin
         (* open a new scope *)
@@ -963,12 +965,12 @@ let printModule id dn =
  let module X = Xml in
   let str = N.string_of_id id in 
   let sp = Lib.make_path id N.OBJ in
-  let ls = L.module_segment (Some str) in
+  let ls = L.module_segment (Some [id]) in
    print_if_verbose ("MODULE_BEGIN " ^ str ^ " " ^ N.string_of_path sp ^ " " ^
-    (snd (L.module_filename str)) ^ "\n") ;
+    (L.module_full_filename [id]) ^ "\n") ;
    print_closed_section str (List.rev ls) dn ;
    print_if_verbose ("MODULE_END " ^ str ^ " " ^ N.string_of_path sp ^ " " ^
-    (snd (L.module_filename str)) ^ "\n")
+    (L.module_full_filename [id]) ^ "\n")
 ;;
 
 (* printSection identifier directory_name                                    *)
@@ -982,18 +984,18 @@ let printSection id dn =
  let module L = Library in
  let module N = Names in
  let module X = Xml in
-  let str = N.string_of_id id in 
   let sp = Lib.make_path id N.OBJ in
   let ls =
    let rec find_closed_section =
     function
        [] -> raise Not_found
-     | (_,Lib.ClosedSection (_,str',ls))::_ when str' = str -> ls
+     | (_,Lib.ClosedSection (_,id',ls))::_ when id' = id -> ls
      | _::t -> find_closed_section t
    in
     print_string ("Searching " ^ Names.string_of_path sp ^ "\n") ;
     find_closed_section (Lib.contents_after None)
   in
+  let str = N.string_of_id id in 
    print_if_verbose ("SECTION_BEGIN " ^ str ^ " " ^ N.string_of_path sp ^ "\n");
    print_closed_section str ls dn ;
    print_if_verbose ("SECTION_END " ^ str ^ " " ^ N.string_of_path sp ^ "\n")