Filenames are now fully mangled (e.g. matita_nat_nat.ml) to avoid file name

clashes.

diff --git a/helm/software/components/cic_exportation/cicExportation.ml b/helm/software/components/cic_exportation/cicExportation.ml
index 94cd982fe3a1b4f02718eabf24fd6219936b7e74..7297dd56a8fb2ce375f087077d348532cfac4826 100644 (file)
--- a/helm/software/components/cic_exportation/cicExportation.ml
+++ b/helm/software/components/cic_exportation/cicExportation.ml
@@ -86,16 +86,18 @@ let rec get_nth l n =
   | (_,_) -> raise NotEnoughElements
 ;;
 
-let qualified_name_of_uri current_module_name ?(capitalize=false) uri =
+let qualified_name_of_uri current_module_uri ?(capitalize=false) uri =
  let name =
   if capitalize then
    String.capitalize (UriManager.name_of_uri uri)
   else
    ppid (UriManager.name_of_uri uri) in
- let buri = UriManager.buri_of_uri uri in
- let index = String.rindex buri '/' in
- let filename = String.sub buri (index + 1) (String.length buri - index - 1) in
-  if current_module_name = filename then
+  let filename =
+   let suri = UriManager.buri_of_uri uri in
+   let s = String.sub suri 5 (String.length suri - 5) in
+   let s = Pcre.replace ~pat:"/" ~templ:"_" s in
+    String.uncapitalize s in
+  if current_module_uri = UriManager.buri_of_uri uri then
    name
   else
    String.capitalize filename ^ "." ^ name
@@ -105,7 +107,7 @@ let qualified_name_of_uri current_module_name ?(capitalize=false) uri =
 (* pretty-prints a term t of cic in an environment l where l is a list of  *)
 (* identifier names used to resolve DeBrujin indexes. The head of l is the *)
 (* name associated to the greatest DeBrujin index in t                     *)
-let pp current_module_name ?metasenv =
+let pp current_module_uri ?metasenv =
 let rec pp t context =
  let module C = Cic in
    match t with
@@ -121,7 +123,7 @@ let rec pp t context =
          NotEnoughElements -> string_of_int (List.length context - n)
        end
     | C.Var (uri,exp_named_subst) ->
-        qualified_name_of_uri current_module_name uri ^
+        qualified_name_of_uri current_module_uri uri ^
          pp_exp_named_subst exp_named_subst context
     | C.Meta (n,l1) ->
        (match metasenv with
@@ -189,14 +191,14 @@ let rec pp t context =
     | C.Appl li ->
        "(" ^ String.concat " " (clean_args context li) ^ ")"
     | C.Const (uri,exp_named_subst) ->
-       qualified_name_of_uri current_module_name uri ^
+       qualified_name_of_uri current_module_uri uri ^
         pp_exp_named_subst exp_named_subst context
     | C.MutInd (uri,n,exp_named_subst) ->
        (try
          match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
             C.InductiveDefinition (dl,_,_,_) ->
              let (name,_,_,_) = get_nth dl (n+1) in
-              qualified_name_of_uri current_module_name
+              qualified_name_of_uri current_module_uri
                (UriManager.uri_of_string
                  (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con")) ^
               pp_exp_named_subst exp_named_subst context
@@ -211,7 +213,7 @@ let rec pp t context =
             C.InductiveDefinition (dl,_,_,_) ->
              let _,_,_,cons = get_nth dl (n1+1) in
               let id,_ = get_nth cons n2 in
-               qualified_name_of_uri current_module_name ~capitalize:true
+               qualified_name_of_uri current_module_uri ~capitalize:true
                 (UriManager.uri_of_string
                   (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")) ^
                pp_exp_named_subst exp_named_subst context
@@ -248,7 +250,7 @@ let rec pp t context =
                           | C.Prod (_,_,bo) -> 1 + count_prods 0 bo
                           | _ -> 0
                         in
-                         qualified_name_of_uri current_module_name
+                         qualified_name_of_uri current_module_uri
                           ~capitalize:true
                           (UriManager.uri_of_string
                             (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")),
@@ -355,7 +357,7 @@ in
  pp
 ;;
 
-let ppty current_module_name =
+let ppty current_module_uri =
  let rec args context =
   function
      Cic.Prod (n,s,t) ->
@@ -379,7 +381,7 @@ let ppty current_module_name =
               args
          | `Type ->
              let abstr,args = args ((Some (n,Cic.Decl s))::context) t in
-              abstr,pp current_module_name s context::args)
+              abstr,pp current_module_uri s context::args)
    | _ -> [],[]
  in
   args
@@ -388,7 +390,7 @@ let ppty current_module_name =
 (* ppinductiveType (typename, inductive, arity, cons)                       *)
 (* pretty-prints a single inductive definition                              *)
 (* (typename, inductive, arity, cons)                                       *)
-let ppinductiveType current_module_name nparams (typename, inductive, arity, cons)
+let ppinductiveType current_module_uri nparams (typename, inductive, arity, cons)
 =
  match analyze_type [] arity with
     `Sort Cic.Prop -> ""
@@ -401,7 +403,7 @@ let ppinductiveType current_module_name nparams (typename, inductive, arity, con
      let abstr,scons =
       List.fold_right
        (fun (id,ty) (_abstr,i) -> (* we should verify _abstr = abstr' *)
-          let abstr',sargs = ppty current_module_name [] ty in
+          let abstr',sargs = ppty current_module_uri [] ty in
           let sargs = String.concat " * " sargs in
            abstr',
            String.capitalize id ^
@@ -416,10 +418,10 @@ let ppinductiveType current_module_name nparams (typename, inductive, arity, con
        "type " ^ abstr ^ String.uncapitalize typename ^ " =\n" ^ scons ^ "\n")
 ;;
 
-let ppobj current_module_name obj =
+let ppobj current_module_uri obj =
  let module C = Cic in
  let module U = UriManager in
-  let pp = pp current_module_name in
+  let pp = pp current_module_uri in
   match obj with
     C.Constant (name, Some t1, t2, params, _) ->
       (match analyze_type [] t2 with
@@ -430,7 +432,7 @@ let ppobj current_module_name obj =
             match analyze_type [] t1 with
                `Sort Cic.Prop -> ""
              | _ ->
-               let abstr,args = ppty current_module_name [] t1 in
+               let abstr,args = ppty current_module_uri [] t1 in
                let abstr =
                 let s = String.concat "," abstr in
                 if s = "" then "" else "(" ^ s ^ ") "
@@ -482,10 +484,10 @@ let ppobj current_module_name obj =
           pp ~metasenv:conjectures ty [] 
    | C.InductiveDefinition (l, params, nparams, _) ->
       List.fold_right
-       (fun x i -> ppinductiveType current_module_name nparams x ^ i) l ""
+       (fun x i -> ppinductiveType current_module_uri nparams x ^ i) l ""
 ;;
 
-let ppobj current_module_name obj =
- let res = ppobj current_module_name obj in
+let ppobj current_module_uri obj =
+ let res = ppobj current_module_uri obj in
   if res = "" then "" else res ^ ";;\n\n"
 ;;

diff --git a/helm/software/components/cic_exportation/cicExportation.mli b/helm/software/components/cic_exportation/cicExportation.mli
index 1f68e4e75e57e8e62e9e8f11f24db67050e0ac16..4d1c82c868ad19816e0a7c00142d7c54819f847c 100644 (file)
--- a/helm/software/components/cic_exportation/cicExportation.mli
+++ b/helm/software/components/cic_exportation/cicExportation.mli
@@ -25,5 +25,5 @@
 
 (* $Id: cicPp.ml 7413 2007-05-29 15:30:53Z tassi $ *)
 
-(* ppobj current_module_name obj *)
+(* ppobj current_module_uri obj *)
 val ppobj : string -> Cic.obj -> string

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index c458f2567c414da2903ac7d6930324697549c9a3..3a6335cb14e65355df7e313abad09e9c484956be 100644 (file)
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -304,13 +304,32 @@ let main ~mode =
   MatitaInit.initialize_all ();
   (* must be called after init since args are set by cmdline parsing *)
   let fname = fname () in
-  if false then
-   let basename = Filename.chop_extension fname in
-   let f = open_out (basename ^ ".ml") in
+  if true then
+   let basename = Filename.basename (Filename.chop_extension fname) in
+   let baseuri =
+    (* This does not work yet :-(
+       let baseuri =
+        GrafiteTypes.get_string_option
+        (match !grafite_status with None -> assert false | Some s -> s)
+        "baseuri" in*)
+    lazy
+     (fst (DependenciesParser.baseuri_of_script ~include_paths:[] fname)) in
+   let mangled_baseuri =
+    lazy
+     ( let baseuri = Lazy.force baseuri in
+       let baseuri = String.sub baseuri 5 (String.length baseuri - 5) in
+       let baseuri = Pcre.replace ~pat:"/" ~templ:"_" baseuri in
+        String.uncapitalize baseuri
+     ) in
+   let f =
+    lazy
+     (open_out
+       (Filename.dirname fname ^ "/" ^ Lazy.force mangled_baseuri ^ ".ml")) in
     LibrarySync.set_object_declaration_hook
      (fun _ obj ->
-       output_string f (CicExportation.ppobj (Filename.basename basename) obj);
-       flush f);
+       output_string (Lazy.force f)
+        (CicExportation.ppobj (Lazy.force baseuri) obj);
+       flush (Lazy.force f));
   let system_mode =  Helm_registry.get_bool "matita.system" in
   let bench_mode =  Helm_registry.get_bool "matita.bench" in
   if bench_mode then