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

[helm.git] / components / cic_exportation / cicExportation.ml

diff --git a/components/cic_exportation/cicExportation.ml b/components/cic_exportation/cicExportation.ml
index 94cd982fe3a1b4f02718eabf24fd6219936b7e74..7297dd56a8fb2ce375f087077d348532cfac4826 100644 (file)
--- a/components/cic_exportation/cicExportation.ml
+++ b/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"
 ;;