X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_exportation%2FcicExportation.ml;h=7297dd56a8fb2ce375f087077d348532cfac4826;hb=77c2a38d7ad4098eed354f68456411227230a3a2;hp=94cd982fe3a1b4f02718eabf24fd6219936b7e74;hpb=127781aeff80e54f2c5d80ef6ffbe4ef27b24b38;p=helm.git 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" ;;