From 77c2a38d7ad4098eed354f68456411227230a3a2 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 5 Nov 2007 12:10:34 +0000 Subject: [PATCH] Filenames are now fully mangled (e.g. matita_nat_nat.ml) to avoid file name clashes. --- components/cic_exportation/cicExportation.ml | 44 ++++++++++--------- components/cic_exportation/cicExportation.mli | 2 +- matita/matitacLib.ml | 29 +++++++++--- 3 files changed, 48 insertions(+), 27 deletions(-) diff --git a/components/cic_exportation/cicExportation.ml b/components/cic_exportation/cicExportation.ml index 94cd982fe..7297dd56a 100644 --- 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" ;; diff --git a/components/cic_exportation/cicExportation.mli b/components/cic_exportation/cicExportation.mli index 1f68e4e75..4d1c82c86 100644 --- a/components/cic_exportation/cicExportation.mli +++ b/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/matita/matitacLib.ml b/matita/matitacLib.ml index c458f2567..3a6335cb1 100644 --- a/matita/matitacLib.ml +++ b/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 -- 2.39.2