From: Claudio Sacerdoti Coen Date: Tue, 16 Jun 2009 22:35:03 +0000 (+0000) Subject: 1) NCicLibrary (which is untrusted) moved after NCicUntrusted. X-Git-Tag: make_still_working~3860 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=134d8273511016e9b6de3423d301a080046f3948;p=helm.git 1) NCicLibrary (which is untrusted) moved after NCicUntrusted. NCicLibrary registers get_obj to NCicEnvironemnt (and to NCicPp) 2) URIs are now refreshed when objects are included from disk Observation: even NCicPp is untrusted. Thus its implementation should be put at the end and some references set to one early module. Which one? Two choices: NCic or NCicPp (two modules, one with the implementation follows). Could the same be done for NCicLibrary too in order to bring back the explicit dependency of NCicEnvironment over NCicLibrary? [ In that case, remember to change back the exception caught by GrafiteDisambiguate ] --- diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index b302da1f2..64c4c8ebe 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -170,7 +170,7 @@ let nlookup_in_library ) references @ lookup_in_library interactive_user_uri_choice input_or_locate_uri item with - NCicLibrary.ObjectNotFound _ -> + NCicEnvironment.ObjectNotFound _ -> lookup_in_library interactive_user_uri_choice input_or_locate_uri item) | _ -> lookup_in_library interactive_user_uri_choice input_or_locate_uri item ;; diff --git a/helm/software/components/ng_kernel/.depend b/helm/software/components/ng_kernel/.depend index 5ec40b8c1..eb185c828 100644 --- a/helm/software/components/ng_kernel/.depend +++ b/helm/software/components/ng_kernel/.depend @@ -1,13 +1,14 @@ +nUri.cmi: nReference.cmi: nUri.cmi nCicUtils.cmi: nCic.cmo nCicSubstitution.cmi: nCic.cmo oCic2NCic.cmi: nUri.cmi nReference.cmi nCic.cmo nCic2OCic.cmi: nUri.cmi nReference.cmi nCic.cmo -nCicLibrary.cmi: nUri.cmi nReference.cmi nCic.cmo nCicPp.cmi: nReference.cmi nCic.cmo nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmo nCicReduction.cmi: nCic.cmo nCicTypeChecker.cmi: nUri.cmi nReference.cmi nCic.cmo +nCicLibrary.cmi: nUri.cmi nReference.cmi nCic.cmo nCicUntrusted.cmi: nCic.cmo nCic.cmo: nUri.cmi nReference.cmi nCic.cmx: nUri.cmx nReference.cmx @@ -27,18 +28,12 @@ oCic2NCic.cmx: nUri.cmx nReference.cmx nCicSubstitution.cmx nCic.cmx \ oCic2NCic.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 nReference.cmi nCic2OCic.cmi nCic.cmo \ - nCicLibrary.cmi -nCicLibrary.cmx: oCic2NCic.cmx nUri.cmx nReference.cmx nCic2OCic.cmx nCic.cmx \ - nCicLibrary.cmi nCicPp.cmo: nUri.cmi nReference.cmi nCicSubstitution.cmi nCicLibrary.cmi \ - nCic.cmo nCicPp.cmi + nCicEnvironment.cmi nCic.cmo nCicPp.cmi nCicPp.cmx: nUri.cmx nReference.cmx nCicSubstitution.cmx nCicLibrary.cmx \ - nCic.cmx nCicPp.cmi -nCicEnvironment.cmo: nUri.cmi nReference.cmi nCicLibrary.cmi nCic.cmo \ - nCicEnvironment.cmi -nCicEnvironment.cmx: nUri.cmx nReference.cmx nCicLibrary.cmx nCic.cmx \ - nCicEnvironment.cmi + nCicEnvironment.cmx nCic.cmx nCicPp.cmi +nCicEnvironment.cmo: nUri.cmi nReference.cmi nCic.cmo nCicEnvironment.cmi +nCicEnvironment.cmx: nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi nCicReduction.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \ nCicPp.cmi nCicEnvironment.cmi nCic.cmo nCicReduction.cmi nCicReduction.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ @@ -49,6 +44,12 @@ 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 +nCicLibrary.cmo: oCic2NCic.cmi nUri.cmi nReference.cmi nCicUtils.cmi \ + nCicUntrusted.cmi nCicEnvironment.cmi nCic2OCic.cmi nCic.cmo \ + nCicLibrary.cmi +nCicLibrary.cmx: oCic2NCic.cmx nUri.cmx nReference.cmx nCicUtils.cmx \ + nCicUntrusted.cmx nCicEnvironment.cmx nCic2OCic.cmx nCic.cmx \ + nCicLibrary.cmi nCicUntrusted.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \ nCicReduction.cmi nCic.cmo nCicUntrusted.cmi nCicUntrusted.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ diff --git a/helm/software/components/ng_kernel/.depend.opt b/helm/software/components/ng_kernel/.depend.opt index a6ea216ac..7a854657e 100644 --- a/helm/software/components/ng_kernel/.depend.opt +++ b/helm/software/components/ng_kernel/.depend.opt @@ -4,12 +4,12 @@ nCicUtils.cmi: nCic.cmx nCicSubstitution.cmi: nCic.cmx oCic2NCic.cmi: nUri.cmi nReference.cmi nCic.cmx nCic2OCic.cmi: nUri.cmi nReference.cmi nCic.cmx -nCicLibrary.cmi: nUri.cmi nReference.cmi nCic.cmx nCicPp.cmi: nReference.cmi nCic.cmx nCicEnvironment.cmi: nUri.cmi nReference.cmi nCic.cmx nCicReduction.cmi: nCic.cmx nCicTypeChecker.cmi: nUri.cmi nReference.cmi nCic.cmx -nCicUntrusted.cmi: nUri.cmi nCic.cmx +nCicLibrary.cmi: nUri.cmi nReference.cmi nCic.cmx +nCicUntrusted.cmi: nCic.cmx nCic.cmo: nUri.cmi nReference.cmi nCic.cmx: nUri.cmx nReference.cmx nUri.cmo: nUri.cmi @@ -28,18 +28,12 @@ oCic2NCic.cmx: nUri.cmx nReference.cmx nCicSubstitution.cmx nCic.cmx \ oCic2NCic.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 nReference.cmi nCic2OCic.cmi nCic.cmx \ - nCicLibrary.cmi -nCicLibrary.cmx: oCic2NCic.cmx nUri.cmx nReference.cmx nCic2OCic.cmx nCic.cmx \ - nCicLibrary.cmi nCicPp.cmo: nUri.cmi nReference.cmi nCicSubstitution.cmi nCicLibrary.cmi \ - nCic.cmx nCicPp.cmi + nCicEnvironment.cmi nCic.cmx nCicPp.cmi nCicPp.cmx: nUri.cmx nReference.cmx nCicSubstitution.cmx nCicLibrary.cmx \ - nCic.cmx nCicPp.cmi -nCicEnvironment.cmo: nUri.cmi nReference.cmi nCicLibrary.cmi nCic.cmx \ - nCicEnvironment.cmi -nCicEnvironment.cmx: nUri.cmx nReference.cmx nCicLibrary.cmx nCic.cmx \ - nCicEnvironment.cmi + nCicEnvironment.cmx nCic.cmx nCicPp.cmi +nCicEnvironment.cmo: nUri.cmi nReference.cmi nCic.cmx nCicEnvironment.cmi +nCicEnvironment.cmx: nUri.cmx nReference.cmx nCic.cmx nCicEnvironment.cmi nCicReduction.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \ nCicPp.cmi nCicEnvironment.cmi nCic.cmx nCicReduction.cmi nCicReduction.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ @@ -50,9 +44,13 @@ 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 -nCicUntrusted.cmo: nReference.cmi nCicUtils.cmi nCicTypeChecker.cmi \ - nCicSubstitution.cmi nCicReduction.cmi nCicEnvironment.cmi nCic.cmx \ - nCicUntrusted.cmi -nCicUntrusted.cmx: nReference.cmx nCicUtils.cmx nCicTypeChecker.cmx \ - nCicSubstitution.cmx nCicReduction.cmx nCicEnvironment.cmx nCic.cmx \ - nCicUntrusted.cmi +nCicLibrary.cmo: oCic2NCic.cmi nUri.cmi nReference.cmi nCicUtils.cmi \ + nCicUntrusted.cmi nCicEnvironment.cmi nCic2OCic.cmi nCic.cmx \ + nCicLibrary.cmi +nCicLibrary.cmx: oCic2NCic.cmx nUri.cmx nReference.cmx nCicUtils.cmx \ + nCicUntrusted.cmx nCicEnvironment.cmx nCic2OCic.cmx nCic.cmx \ + nCicLibrary.cmi +nCicUntrusted.cmo: nReference.cmi nCicUtils.cmi nCicSubstitution.cmi \ + nCicReduction.cmi nCic.cmx nCicUntrusted.cmi +nCicUntrusted.cmx: nReference.cmx nCicUtils.cmx nCicSubstitution.cmx \ + nCicReduction.cmx nCic.cmx nCicUntrusted.cmi diff --git a/helm/software/components/ng_kernel/Makefile b/helm/software/components/ng_kernel/Makefile index fedcaa4d8..d533c8f73 100644 --- a/helm/software/components/ng_kernel/Makefile +++ b/helm/software/components/ng_kernel/Makefile @@ -8,12 +8,12 @@ INTERFACE_FILES = \ nCicSubstitution.mli \ oCic2NCic.mli \ nCic2OCic.mli \ - nCicLibrary.mli \ - nCicPp.mli \ nCicEnvironment.mli \ + nCicPp.mli \ nCicReduction.mli \ nCicTypeChecker.mli \ - nCicUntrusted.mli + nCicUntrusted.mli \ + nCicLibrary.mli IMPLEMENTATION_FILES = \ nCic.ml $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml index f31c4e9b1..ef3bca22d 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.ml +++ b/helm/software/components/ng_kernel/nCicEnvironment.ml @@ -19,6 +19,9 @@ exception ObjectNotFound of string Lazy.t;; exception BadDependency of string Lazy.t * exn;; exception BadConstraint of string Lazy.t;; +let get_obj = ref (fun _ -> assert false);; +let set_get_obj f = get_obj := f;; + let type0 = [] let max l1 l2 = @@ -125,17 +128,13 @@ let get_checked_obj u = Not_found -> let saved_frozen_list = !frozen_list in try - let obj = - try NCicLibrary.get_obj u - with - NCicLibrary.ObjectNotFound m -> raise (ObjectNotFound m) - in - frozen_list := (u,obj)::saved_frozen_list; - !typecheck_obj obj; - frozen_list := saved_frozen_list; - let obj = `WellTyped obj in - NUri.UriHash.add cache u obj; - obj + let obj = !get_obj u in + frozen_list := (u,obj)::saved_frozen_list; + !typecheck_obj obj; + frozen_list := saved_frozen_list; + let obj = `WellTyped obj in + NUri.UriHash.add cache u obj; + obj with Sys.Break as e -> frozen_list := saved_frozen_list; diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli index 4604bd2fd..862d71484 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.mli +++ b/helm/software/components/ng_kernel/nCicEnvironment.mli @@ -16,6 +16,8 @@ exception ObjectNotFound of string Lazy.t;; exception BadDependency of string Lazy.t * exn;; exception BadConstraint of string Lazy.t;; +val set_get_obj: (NUri.uri -> NCic.obj) -> unit + val get_checked_obj: NUri.uri -> NCic.obj val get_relevance: NReference.reference -> bool list diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml index d28b0da6c..80b0911b2 100644 --- a/helm/software/components/ng_kernel/nCicLibrary.ml +++ b/helm/software/components/ng_kernel/nCicLibrary.ml @@ -11,7 +11,6 @@ (* $Id$ *) -exception ObjectNotFound of string Lazy.t exception LibraryOutOfSync of string Lazy.t type timestamp = @@ -60,6 +59,22 @@ let serialize ~baseuri dump = time_travel time0 ;; +let refresh_uri uri = NUri.uri_of_string (NUri.string_of_uri uri);; + +let rec refresh_uri_in_term = + function + NCic.Const (NReference.Ref (u,spec)) -> + NCic.Const (NReference.reference_of_spec (refresh_uri u) spec) + | t -> NCicUtils.map (fun _ _ -> ()) () (fun _ -> refresh_uri_in_term) t +;; + +let refresh_uri_in_obj (uri,height,metasenv,subst,obj_kind) = + assert (metasenv = []); + assert (subst = []); + uri,height,metasenv,subst, + NCicUntrusted.map_obj_kind refresh_uri_in_term obj_kind +;; + module type Serializer = sig type status @@ -97,11 +112,9 @@ let decompile ~baseuri = (* WE ARE NOT REMOVING ALL THE OBJECTS YET! *) ;; -(* the miracles of Marshal... *) let fetch_obj uri = let obj = require0 ~baseuri:uri in - (* here we need to refresh the URIs! *) - obj + refresh_uri_in_obj obj ;; let resolve name = @@ -109,7 +122,7 @@ let resolve name = HExtlib.filter_map (fun (_,name',nref) -> if name'=name then Some nref else None) !aliases with - Not_found -> raise (ObjectNotFound (lazy name)) + Not_found -> raise (NCicEnvironment.ObjectNotFound (lazy name)) ;; let aliases_of uri = @@ -117,7 +130,7 @@ let aliases_of uri = HExtlib.filter_map (fun (uri',_,nref) -> if NUri.eq uri' uri then Some nref else None) !aliases with - Not_found -> raise (ObjectNotFound (lazy (NUri.string_of_uri uri))) + Not_found -> raise (NCicEnvironment.ObjectNotFound (lazy (NUri.string_of_uri uri))) ;; let add_obj u obj = @@ -168,8 +181,11 @@ let get_obj u = List.iter (fun (u,_,_,_,_ as o) -> cache:= NUri.UriMap.add u o !cache) l; HExtlib.list_last l with CicEnvironment.Object_not_found u -> - raise (ObjectNotFound + raise (NCicEnvironment.ObjectNotFound (lazy (NUri.string_of_uri (OCic2NCic.nuri_of_ouri u)))) ;; let clear_cache () = cache := NUri.UriMap.empty;; + +NCicEnvironment.set_get_obj get_obj;; +NCicPp.set_get_obj get_obj;; diff --git a/helm/software/components/ng_kernel/nCicLibrary.mli b/helm/software/components/ng_kernel/nCicLibrary.mli index f94c65682..2d04b7d11 100644 --- a/helm/software/components/ng_kernel/nCicLibrary.mli +++ b/helm/software/components/ng_kernel/nCicLibrary.mli @@ -11,7 +11,6 @@ (* $Id$ *) -exception ObjectNotFound of string Lazy.t exception LibraryOutOfSync of string Lazy.t type timestamp @@ -20,6 +19,7 @@ val time0: timestamp val add_obj: NUri.uri -> NCic.obj -> timestamp val aliases_of: NUri.uri -> NReference.reference list val resolve: string -> NReference.reference list +(* warning: get_obj may raise (NCicEnvironment.ObjectNotFoud l) *) val get_obj: NUri.uri -> NCic.obj (* changes the current timestamp *) val clear_cache : unit -> unit diff --git a/helm/software/components/ng_kernel/nCicPp.ml b/helm/software/components/ng_kernel/nCicPp.ml index 27b46431e..258e83c94 100644 --- a/helm/software/components/ng_kernel/nCicPp.ml +++ b/helm/software/components/ng_kernel/nCicPp.ml @@ -18,26 +18,29 @@ module F = Format let head_beta_reduce = ref (fun ~upto:_ _ -> assert false);; let set_head_beta_reduce = (:=) head_beta_reduce;; +let get_obj = ref (fun _ -> assert false);; +let set_get_obj f = get_obj := f;; + let r2s pp_fix_name r = try match r with | R.Ref (u,R.Ind (_,i,_)) -> - (match NCicLibrary.get_obj u with + (match !get_obj u with | _,_,_,_, C.Inductive (_,_,itl,_) -> let _,name,_,_ = List.nth itl i in name | _ -> assert false) | R.Ref (u,R.Con (i,j,_)) -> - (match NCicLibrary.get_obj u with + (match !get_obj u with | _,_,_,_, C.Inductive (_,_,itl,_) -> let _,_,_,cl = List.nth itl i in let _,name,_ = List.nth cl (j-1) in name | _ -> assert false) | R.Ref (u,(R.Decl | R.Def _)) -> - (match NCicLibrary.get_obj u with + (match !get_obj u with | _,_,_,_, C.Constant (_,name,_,_,_) -> name | _ -> assert false) | R.Ref (u,(R.Fix (i,_,_)|R.CoFix i)) -> - (match NCicLibrary.get_obj u with + (match !get_obj u with | _,_,_,_, C.Fixpoint (_,fl,_) -> if pp_fix_name then let _,name,_,_,_ = List.nth fl i in name @@ -45,7 +48,7 @@ let r2s pp_fix_name r = NUri.name_of_uri u ^"("^ string_of_int i ^ ")" | _ -> assert false) with - | NCicLibrary.ObjectNotFound _ + | NCicEnvironment.ObjectNotFound _ | Failure "nth" | Invalid_argument "List.nth" -> R.string_of_reference r diff --git a/helm/software/components/ng_kernel/nCicPp.mli b/helm/software/components/ng_kernel/nCicPp.mli index ccac8dff6..c260e8c61 100644 --- a/helm/software/components/ng_kernel/nCicPp.mli +++ b/helm/software/components/ng_kernel/nCicPp.mli @@ -12,6 +12,7 @@ (* $Id$ *) val set_head_beta_reduce: (upto:int -> NCic.term -> NCic.term) -> unit +val set_get_obj: (NUri.uri -> NCic.obj) -> unit val r2s: bool -> NReference.reference -> string