From: Claudio Sacerdoti Coen Date: Wed, 14 May 2008 15:36:26 +0000 (+0000) Subject: nuri_of_ouri, ouri_of_nuri, reference_of_ouri, ouri_of_reference moved X-Git-Tag: make_still_working~5212 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=738ff6e752f9e5facba4e92bdb64453062f52c7d;p=helm.git nuri_of_ouri, ouri_of_nuri, reference_of_ouri, ouri_of_reference moved to NCic2OCic or to OCic2NCic. The kernel is now clean of conversion functions. --- diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend index 901398ade..22002034a 100644 --- a/helm/software/components/ng_kernel/.depend +++ b/helm/software/components/ng_kernel/.depend @@ -1,13 +1,13 @@ nReference.cmi: nUri.cmi nCicUtils.cmi: nCic.cmo nCicSubstitution.cmi: nCic.cmo -oCic2NCic.cmi: nCic.cmo +oCic2NCic.cmi: nUri.cmi nReference.cmi nCic.cmo +nCic2OCic.cmi: nUri.cmi nReference.cmi nCic.cmo nCicLibrary.cmi: nUri.cmi nCic.cmo nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmo nCicPp.cmi: nCic.cmo nCicReduction.cmi: nCic.cmo nCicTypeChecker.cmi: nUri.cmi nCic.cmo -nCic2OCic.cmi: nCic.cmo nCic.cmo: nUri.cmi nReference.cmi nCic.cmx: nUri.cmx nReference.cmx nUri.cmo: nUri.cmi @@ -22,8 +22,10 @@ oCic2NCic.cmo: nUri.cmi nReference.cmi nCicSubstitution.cmi nCic.cmo \ oCic2NCic.cmi oCic2NCic.cmx: nUri.cmx nReference.cmx nCicSubstitution.cmx nCic.cmx \ oCic2NCic.cmi -nCicLibrary.cmo: oCic2NCic.cmi nUri.cmi nCicLibrary.cmi -nCicLibrary.cmx: oCic2NCic.cmx nUri.cmx nCicLibrary.cmi +nCic2OCic.cmo: nUri.cmi nReference.cmi nCic.cmo nCic2OCic.cmi +nCic2OCic.cmx: nUri.cmx nReference.cmx nCic.cmx nCic2OCic.cmi +nCicLibrary.cmo: oCic2NCic.cmi nUri.cmi nCic2OCic.cmi nCicLibrary.cmi +nCicLibrary.cmx: oCic2NCic.cmx nUri.cmx nCic2OCic.cmx nCicLibrary.cmi nCicEnvironment.cmo: nUri.cmi nReference.cmi nCicLibrary.cmi nCic.cmo \ nCicEnvironment.cmi nCicEnvironment.cmx: nUri.cmx nReference.cmx nCicLibrary.cmx nCic.cmx \ @@ -40,5 +42,3 @@ nCicTypeChecker.cmo: nUri.cmi nReference.cmi nCicUtils.cmi \ nCicTypeChecker.cmx: nUri.cmx nReference.cmx nCicUtils.cmx \ nCicSubstitution.cmx nCicReduction.cmx nCicPp.cmx nCicEnvironment.cmx \ nCic.cmx nCicTypeChecker.cmi -nCic2OCic.cmo: nUri.cmi nReference.cmi nCic.cmo nCic2OCic.cmi -nCic2OCic.cmx: nUri.cmx nReference.cmx nCic.cmx nCic2OCic.cmi diff --git a/helm/software/components/ng_kernel/.depend.opt b/helm/software/components/ng_kernel/.depend.opt index 8396f2c58..8b8fee22f 100644 --- a/helm/software/components/ng_kernel/.depend.opt +++ b/helm/software/components/ng_kernel/.depend.opt @@ -1,13 +1,13 @@ nReference.cmi: nUri.cmi nCicUtils.cmi: nCic.cmx nCicSubstitution.cmi: nCic.cmx -oCic2NCic.cmi: nCic.cmx +oCic2NCic.cmi: nUri.cmi nReference.cmi nCic.cmx +nCic2OCic.cmi: nUri.cmi nReference.cmi nCic.cmx nCicLibrary.cmi: nUri.cmi nCic.cmx nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmx nCicPp.cmi: nCic.cmx nCicReduction.cmi: nCic.cmx nCicTypeChecker.cmi: nUri.cmi nCic.cmx -nCic2OCic.cmi: nCic.cmx nCic.cmo: nUri.cmi nReference.cmi nCic.cmx: nUri.cmx nReference.cmx nUri.cmo: nUri.cmi @@ -22,8 +22,10 @@ oCic2NCic.cmo: nUri.cmi nReference.cmi nCicSubstitution.cmi nCic.cmx \ oCic2NCic.cmi oCic2NCic.cmx: nUri.cmx nReference.cmx nCicSubstitution.cmx nCic.cmx \ oCic2NCic.cmi -nCicLibrary.cmo: oCic2NCic.cmi nUri.cmi nCicLibrary.cmi -nCicLibrary.cmx: oCic2NCic.cmx nUri.cmx nCicLibrary.cmi +nCic2OCic.cmo: nUri.cmi nReference.cmi nCic.cmx nCic2OCic.cmi +nCic2OCic.cmx: nUri.cmx nReference.cmx nCic.cmx nCic2OCic.cmi +nCicLibrary.cmo: oCic2NCic.cmi nUri.cmi nCic2OCic.cmi nCicLibrary.cmi +nCicLibrary.cmx: oCic2NCic.cmx nUri.cmx nCic2OCic.cmx nCicLibrary.cmi nCicEnvironment.cmo: nUri.cmi nReference.cmi nCicLibrary.cmi nCic.cmx \ nCicEnvironment.cmi nCicEnvironment.cmx: nUri.cmx nReference.cmx nCicLibrary.cmx nCic.cmx \ @@ -40,5 +42,3 @@ nCicTypeChecker.cmo: nUri.cmi nReference.cmi nCicUtils.cmi \ nCicTypeChecker.cmx: nUri.cmx nReference.cmx nCicUtils.cmx \ nCicSubstitution.cmx nCicReduction.cmx nCicPp.cmx nCicEnvironment.cmx \ nCic.cmx nCicTypeChecker.cmi -nCic2OCic.cmo: nUri.cmi nReference.cmi nCic.cmx nCic2OCic.cmi -nCic2OCic.cmx: nUri.cmx nReference.cmx nCic.cmx nCic2OCic.cmi diff --git a/helm/software/components/ng_kernel/Makefile b/helm/software/components/ng_kernel/Makefile index 5afff33cf..3d1c59cac 100644 --- a/helm/software/components/ng_kernel/Makefile +++ b/helm/software/components/ng_kernel/Makefile @@ -7,12 +7,12 @@ INTERFACE_FILES = \ nCicUtils.mli \ nCicSubstitution.mli \ oCic2NCic.mli \ + nCic2OCic.mli \ nCicLibrary.mli \ nCicEnvironment.mli \ nCicPp.mli \ nCicReduction.mli \ - nCicTypeChecker.mli \ - nCic2OCic.mli + nCicTypeChecker.mli IMPLEMENTATION_FILES = \ nCic.ml $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml index d0c18e6a7..9fefb3c99 100644 --- a/helm/software/components/ng_kernel/check.ml +++ b/helm/software/components/ng_kernel/check.ml @@ -133,7 +133,7 @@ let _ = prerr_endline "ranked...."; HExtlib.profiling_enabled := false; List.iter (fun uu -> - let uu= NUri.nuri_of_ouri uu in + let uu= OCic2NCic.nuri_of_ouri uu in indent := 0; let o = NCicLibrary.get_obj uu in try @@ -156,7 +156,7 @@ let _ = let prima = Unix.gettimeofday () in List.iter (fun u -> - let u= NUri.nuri_of_ouri u in + let u= OCic2NCic.nuri_of_ouri u in indent := 0; NCicTypeChecker.typecheck_obj (NCicLibrary.get_obj u)) alluris; diff --git a/helm/software/components/ng_kernel/nCic2OCic.ml b/helm/software/components/ng_kernel/nCic2OCic.ml index 3348d31cd..57465b074 100644 --- a/helm/software/components/ng_kernel/nCic2OCic.ml +++ b/helm/software/components/ng_kernel/nCic2OCic.ml @@ -11,6 +11,10 @@ (* $Id$ *) +let ouri_of_nuri u = UriManager.uri_of_string (NUri.string_of_uri u);; + +let ouri_of_reference (NReference.Ref (_,u,_)) = ouri_of_nuri u;; + let nn_2_on = function | "_" -> Cic.Anonymous | s -> Cic.Name s @@ -32,21 +36,21 @@ let convert_term uri n_fl t = | NCic.Sort (NCic.Type _) -> Cic.Sort (Cic.Type (CicUniv.fresh ())) | NCic.Implicit _ -> assert false | NCic.Const (NReference.Ref (_,u,NReference.Ind (_,i))) -> - Cic.MutInd (NUri.ouri_of_nuri u,i,[]) + Cic.MutInd (ouri_of_nuri u,i,[]) | NCic.Const (NReference.Ref (_,u,NReference.Con (i,j))) -> - Cic.MutConstruct (NUri.ouri_of_nuri u,i,j,[]) + Cic.MutConstruct (ouri_of_nuri u,i,j,[]) | NCic.Const (NReference.Ref (_,u,NReference.Def)) | NCic.Const (NReference.Ref (_,u,NReference.Decl)) -> - Cic.Const (NUri.ouri_of_nuri u,[]) + Cic.Const (ouri_of_nuri u,[]) | NCic.Match (NReference.Ref (_,u,NReference.Ind (_,i)),oty,t,pl) -> - Cic.MutCase (NUri.ouri_of_nuri u,i, convert_term k oty, convert_term k t, + Cic.MutCase (ouri_of_nuri u,i, convert_term k oty, convert_term k t, List.map (convert_term k) pl) | NCic.Const (NReference.Ref (_,u,NReference.Fix (i,_))) | NCic.Const (NReference.Ref (_,u,NReference.CoFix i)) -> if NUri.eq u uri then Cic.Rel (n_fl - i + k) else - let ouri = NUri.ouri_of_nuri u in + let ouri = ouri_of_nuri u in let ouri = UriManager.uri_of_string (UriManager.buri_of_uri ouri ^ "/" ^ @@ -79,16 +83,16 @@ let convert_fix is_fix uri k fl = let convert_nobj = function | u,_,_,_,NCic.Constant (_, name, Some bo, ty, _) -> - [NUri.ouri_of_nuri u,Cic.Constant + [ouri_of_nuri u,Cic.Constant (name, Some (convert_term u 0 bo), convert_term u 0 ty, [],[])] | u,_,_,_,NCic.Constant (_, name, None, ty, _) -> - [NUri.ouri_of_nuri u,Cic.Constant (name, None, convert_term u 0 ty, [],[])] + [ouri_of_nuri u,Cic.Constant (name, None, convert_term u 0 ty, [],[])] | u,_,_,_,NCic.Fixpoint (is_fix, fl, _) -> List.map (fun nth -> let name = - UriManager.name_of_uri (NUri.ouri_of_nuri u) ^ string_of_int nth in - let buri = UriManager.buri_of_uri (NUri.ouri_of_nuri u) in + UriManager.name_of_uri (ouri_of_nuri u) ^ string_of_int nth in + let buri = UriManager.buri_of_uri (ouri_of_nuri u) in let uri = UriManager.uri_of_string (buri ^"/"^name^".con") in uri, Cic.Constant (name, diff --git a/helm/software/components/ng_kernel/nCic2OCic.mli b/helm/software/components/ng_kernel/nCic2OCic.mli index 2159aaeec..db6349ee7 100644 --- a/helm/software/components/ng_kernel/nCic2OCic.mli +++ b/helm/software/components/ng_kernel/nCic2OCic.mli @@ -11,4 +11,8 @@ (* $Id$ *) +val ouri_of_nuri: NUri.uri -> UriManager.uri + +val ouri_of_reference: NReference.reference -> UriManager.uri + val convert_nobj: NCic.obj -> (UriManager.uri * Cic.obj) list diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml index a5ecefad8..fa2816773 100644 --- a/helm/software/components/ng_kernel/nCicLibrary.ml +++ b/helm/software/components/ng_kernel/nCicLibrary.ml @@ -19,7 +19,7 @@ let get_obj u = try NUri.UriHash.find cache u with Not_found -> (* in the final implementation should get it from disk *) - let ouri = NUri.ouri_of_nuri u in + let ouri = NCic2OCic.ouri_of_nuri u in let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph ouri in let l = OCic2NCic.convert_obj ouri o in List.iter (fun (u,_,_,_,_ as o) -> diff --git a/helm/software/components/ng_kernel/nReference.ml b/helm/software/components/ng_kernel/nReference.ml index bd171ef29..bdf4f98a7 100644 --- a/helm/software/components/ng_kernel/nReference.ml +++ b/helm/software/components/ng_kernel/nReference.ml @@ -118,11 +118,3 @@ let mk_cofix i = function reference_of_string (string_of_reference (Ref (d, u, CoFix i))) | _ -> assert false ;; - -let reference_of_ouri u indinfo = - let u = NUri.nuri_of_ouri u in - reference_of_string (string_of_reference (Ref (max_int,u,indinfo))) -;; - -let ouri_of_reference (Ref (_,u,_)) = NUri.ouri_of_nuri u;; - diff --git a/helm/software/components/ng_kernel/nReference.mli b/helm/software/components/ng_kernel/nReference.mli index b73239465..7f43c13e7 100644 --- a/helm/software/components/ng_kernel/nReference.mli +++ b/helm/software/components/ng_kernel/nReference.mli @@ -25,13 +25,9 @@ type reference = private Ref of int * NUri.uri * spec val eq: reference -> reference -> bool val string_of_reference: reference -> string +val reference_of_string: string -> reference (* given the reference of an inductive type, returns the i-th contructor *) val mk_constructor: int -> reference -> reference val mk_fix: int -> int -> reference -> reference val mk_cofix: int -> reference -> reference - - -(* CACCA *) -val reference_of_ouri: UriManager.uri -> spec -> reference -val ouri_of_reference: reference -> UriManager.uri diff --git a/helm/software/components/ng_kernel/nUri.ml b/helm/software/components/ng_kernel/nUri.ml index 16fd7e489..e4dcddc0d 100644 --- a/helm/software/components/ng_kernel/nUri.ml +++ b/helm/software/components/ng_kernel/nUri.ml @@ -48,7 +48,3 @@ module HT = struct end;; module UriHash = Hashtbl.Make(HT);; - -let ouri_of_nuri u = UriManager.uri_of_string (string_of_uri u);; -let nuri_of_ouri o = uri_of_string (UriManager.string_of_uri o);; - diff --git a/helm/software/components/ng_kernel/nUri.mli b/helm/software/components/ng_kernel/nUri.mli index b08abbbfb..a11e4a1d2 100644 --- a/helm/software/components/ng_kernel/nUri.mli +++ b/helm/software/components/ng_kernel/nUri.mli @@ -18,7 +18,3 @@ val uri_of_string: string -> uri val eq: uri -> uri -> bool module UriHash: Hashtbl.S with type key = uri - -(* CACCA *) -val ouri_of_nuri: uri -> UriManager.uri -val nuri_of_ouri: UriManager.uri -> uri diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index cfc2816cb..9f0bfc211 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -13,6 +13,16 @@ module Ref = NReference +let nuri_of_ouri o = NUri.uri_of_string (UriManager.string_of_uri o);; + +(* porcatissima *) +type reference = Ref of int * NUri.uri * NReference.spec +let reference_of_ouri u indinfo = + let u = nuri_of_ouri u in + NReference.reference_of_string + (NReference.string_of_reference (Obj.magic (Ref (max_int,u,indinfo)))) +;; + type ctx = | Ce of (NCic.hypothesis * NCic.obj list) Lazy.t | Fix of (Ref.reference * string * NCic.term) Lazy.t @@ -412,7 +422,7 @@ let convert_term uri t = List.fold_right (fun (name,ty,_) (bctx, fixpoints, tys, idx) -> let ty, fixpoints_ty = aux true octx ctx n_fix uri ty in - let r = Ref.reference_of_ouri buri(Ref.CoFix idx) in + let r = reference_of_ouri buri(Ref.CoFix idx) in bctx @ [Fix (lazy (r,name,ty))], fixpoints_ty @ fixpoints,ty::tys,idx-1) fl ([], [], [], List.length fl-1) @@ -436,10 +446,10 @@ let convert_term uri t = fl tys ([],fixpoints_tys) in let obj = - NUri.nuri_of_ouri buri,0,[],[], + nuri_of_ouri buri,0,[],[], NCic.Fixpoint (false, fl, (`Generated, `Definition)) in - let r = Ref.reference_of_ouri buri (Ref.CoFix cofixno) in + let r = reference_of_ouri buri (Ref.CoFix cofixno) in let obj,r = let _,name,_,_,_ = List.nth fl cofixno in match find_in_cache name obj r with @@ -461,7 +471,7 @@ let convert_term uri t = (fun (name,recno,ty,_) (bctx, fixpoints, tys, idx) -> let ty, fixpoints_ty = aux true octx ctx n_fix uri ty in let r = (* recno is dummy here, must be lifted by the ctx len *) - Ref.reference_of_ouri buri (Ref.Fix (idx,recno)) + reference_of_ouri buri (Ref.Fix (idx,recno)) in bctx @ [Fix (lazy (r,name,ty))], fixpoints_ty@fixpoints,ty::tys,idx-1) @@ -472,7 +482,7 @@ let convert_term uri t = let bctx = List.map (function ce -> match strictify ce with | `Fix (Ref.Ref (_,_,Ref.Fix (idx, recno)),name, ty) -> - Fix (lazy (Ref.reference_of_ouri buri + Fix (lazy (reference_of_ouri buri (Ref.Fix (idx,recno+free_decls)),name,ty)) | _ -> assert false) bad_bctx @ ctx in @@ -497,9 +507,9 @@ let convert_term uri t = fl tys ([],fixpoints_tys,0) in let obj = - NUri.nuri_of_ouri buri,max_int,[],[], + nuri_of_ouri buri,max_int,[],[], NCic.Fixpoint (true, fl, (`Generated, `Definition)) in - let r = Ref.reference_of_ouri buri (Ref.Fix (fixno,!rno_fixno)) in + let r = reference_of_ouri buri (Ref.Fix (fixno,!rno_fixno)) in let obj,r = let _,name,_,_,_ = List.nth fl fixno in match find_in_cache name obj r with @@ -577,9 +587,9 @@ let convert_term uri t = aux_ens k curi octx ctx n_fix uri ens (match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with | Cic.Constant (_,Some _,_,_,_) -> - NCic.Const (Ref.reference_of_ouri curi Ref.Def) + NCic.Const (reference_of_ouri curi Ref.Def) | Cic.Constant (_,None,_,_,_) -> - NCic.Const (Ref.reference_of_ouri curi Ref.Decl) + NCic.Const (reference_of_ouri curi Ref.Decl) | _ -> assert false) | Cic.MutInd (curi, tyno, ens) -> let is_inductive = @@ -589,10 +599,10 @@ let convert_term uri t = | _ -> assert false in aux_ens k curi octx ctx n_fix uri ens - (NCic.Const (Ref.reference_of_ouri curi (Ref.Ind (is_inductive,tyno)))) + (NCic.Const (reference_of_ouri curi (Ref.Ind (is_inductive,tyno)))) | Cic.MutConstruct (curi, tyno, consno, ens) -> aux_ens k curi octx ctx n_fix uri ens - (NCic.Const (Ref.reference_of_ouri curi (Ref.Con (tyno,consno)))) + (NCic.Const (reference_of_ouri curi (Ref.Con (tyno,consno)))) | Cic.Var (curi, ens) -> (match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with Cic.Variable (_,Some bo,_,_,_) -> @@ -604,7 +614,7 @@ let convert_term uri t = Cic.InductiveDefinition ([],_,_,_) -> true | Cic.InductiveDefinition ((_,b,_,_)::_,_,_,_) -> b | _ -> assert false in - let r = Ref.reference_of_ouri curi (Ref.Ind (is_inductive,tyno)) in + let r = reference_of_ouri curi (Ref.Ind (is_inductive,tyno)) in let outty, fixpoints_outty = aux k octx ctx n_fix uri outty in let t, fixpoints_t = aux k octx ctx n_fix uri t in let branches, fixpoints = @@ -723,6 +733,6 @@ let convert_obj_aux uri = function let convert_obj uri obj = reset_seed (); let o, fixpoints = convert_obj_aux uri obj in - let obj = NUri.nuri_of_ouri uri,max_int, [], [], o in + let obj = nuri_of_ouri uri,max_int, [], [], o in fixpoints @ [obj] ;; diff --git a/helm/software/components/ng_kernel/oCic2NCic.mli b/helm/software/components/ng_kernel/oCic2NCic.mli index 965086a38..7ee5cb11d 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.mli +++ b/helm/software/components/ng_kernel/oCic2NCic.mli @@ -11,4 +11,8 @@ (* $Id$ *) +val nuri_of_ouri: UriManager.uri -> NUri.uri + +val reference_of_ouri: UriManager.uri -> NReference.spec -> NReference.reference + val convert_obj: UriManager.uri -> Cic.obj -> NCic.obj list