From d5e97ad44a11aa8410f57aa8391e3b43ff766df0 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 4 Nov 2007 17:24:52 +0000 Subject: [PATCH] All names are now qualified. This avoids the need for "open" statements. --- .../cic_exportation/cicExportation.ml | 58 ++++++++++++++----- 1 file changed, 42 insertions(+), 16 deletions(-) diff --git a/helm/software/components/cic_exportation/cicExportation.ml b/helm/software/components/cic_exportation/cicExportation.ml index 8acb873a9..b493c4e40 100644 --- a/helm/software/components/cic_exportation/cicExportation.ml +++ b/helm/software/components/cic_exportation/cicExportation.ml @@ -84,11 +84,26 @@ let rec get_nth l n = | (_,_) -> raise NotEnoughElements ;; +let qualified_name_of_uri current_module_name ?(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 + name + else + String.capitalize filename ^ "." ^ name +;; + (* pp t l *) (* 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 ?metasenv = +let pp current_module_name ?metasenv = let rec pp t context = let module C = Cic in match t with @@ -104,7 +119,8 @@ let rec pp t context = NotEnoughElements -> string_of_int (List.length context - n) end | C.Var (uri,exp_named_subst) -> - UriManager.name_of_uri uri ^ pp_exp_named_subst exp_named_subst context + qualified_name_of_uri current_module_name uri ^ + pp_exp_named_subst exp_named_subst context | C.Meta (n,l1) -> (match metasenv with None -> @@ -165,13 +181,17 @@ let rec pp t context = | C.Appl li -> "(" ^ String.concat " " (clean_args context li) ^ ")" | C.Const (uri,exp_named_subst) -> - ppid (UriManager.name_of_uri uri) ^ pp_exp_named_subst exp_named_subst context + qualified_name_of_uri current_module_name 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 - ppid name ^ pp_exp_named_subst exp_named_subst context + qualified_name_of_uri current_module_name + (UriManager.uri_of_string + (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con")) ^ + pp_exp_named_subst exp_named_subst context | _ -> raise CicExportationInternalError with Sys.Break as exn -> raise exn @@ -181,9 +201,12 @@ let rec pp t context = (try match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with C.InductiveDefinition (dl,_,_,_) -> - let (_,_,_,cons) = get_nth dl (n1+1) in - let (id,_) = get_nth cons n2 in - String.capitalize id ^ pp_exp_named_subst exp_named_subst context + let _,_,_,cons = get_nth dl (n1+1) in + let id,_ = get_nth cons n2 in + qualified_name_of_uri current_module_name ~capitalize:true + (UriManager.uri_of_string + (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")) ^ + pp_exp_named_subst exp_named_subst context | _ -> raise CicExportationInternalError with Sys.Break as exn -> raise exn @@ -207,7 +230,10 @@ let rec pp t context = | C.Prod (_,_,bo) -> 1 + count_prods 0 bo | _ -> 0 in - String.capitalize id, count_prods paramsno ty + qualified_name_of_uri current_module_name ~capitalize:true + (UriManager.uri_of_string + (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")), + count_prods paramsno ty ) cons | _ -> raise CicExportationInternalError ) @@ -299,7 +325,7 @@ in (* ppinductiveType (typename, inductive, arity, cons) *) (* pretty-prints a single inductive definition *) (* (typename, inductive, arity, cons) *) -let ppinductiveType (typename, inductive, arity, cons) = +let ppinductiveType current_module_name (typename, inductive, arity, cons) = let abstr,scons = List.fold_right (fun (id,ty) (abstr,i) -> @@ -320,7 +346,7 @@ let ppinductiveType (typename, inductive, arity, cons) = args | `Type -> let abstr,args = args ((Some (n,Cic.Decl s))::context) t in - abstr,pp s context::args) + abstr,pp current_module_name s context::args) | _ -> [],[] in let abstr',sargs = args [] ty in @@ -338,11 +364,10 @@ let ppinductiveType (typename, inductive, arity, cons) = "type " ^ abstr ^ typename ^ " =\n" ^ scons ;; -(* ppobj obj returns a string with describing the cic object obj in a syntax *) -(* similar to the one used by Coq *) -let ppobj obj = +let ppobj current_module_name obj = let module C = Cic in let module U = UriManager in + let pp = pp current_module_name in match obj with C.Constant (name, Some t1, t2, params, _) -> (match analyze_type [] t2 with @@ -392,10 +417,11 @@ let ppobj obj = "\n" ^ pp ~metasenv:conjectures value [] ^ " : " ^ pp ~metasenv:conjectures ty [] | C.InductiveDefinition (l, params, nparams, _) -> - List.fold_right (fun x i -> ppinductiveType x ^ i) l "\n" + List.fold_right + (fun x i -> ppinductiveType current_module_name x ^ i) l "\n" ;; -let ppobj obj = - let res = ppobj obj in +let ppobj current_module_name obj = + let res = ppobj current_module_name obj in if res = "" then "" else res ^ ";;\n" ;; -- 2.39.2