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 b302da1f254227777be6945055ad98ac934c7a2c..64c4c8ebe9e2d84043224b891aee6ca861575804 100644 (file)
--- 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 5ec40b8c1b002a95133bfb47268cc3d52e97b183..eb185c828f38c669fdf6bddc679367542b90ff57 100644 (file)
--- 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 a6ea216acd3ce238d974ba7c94a9ae01547ff14d..7a854657ef07ad47e5aa415bfda270cf53364e08 100644 (file)
--- 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 fedcaa4d8b3d6ec9fdbf3fef3ad03013fa627da6..d533c8f73512415d56b78279c620576279927a73 100644 (file)
--- 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 f31c4e9b1ebbc71416ced0dbbc120e4bf60c7448..ef3bca22d06941ebfa20fe883d4423eb7ec87e0e 100644 (file)
--- 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 4604bd2fdf2fe4a49537862fe88fc3f53f2ebf9b..862d7148432f5a6ba7525780d5e0b8d04f36b3f9 100644 (file)
--- 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 d28b0da6ce3c423f348c1c423aef745c20c6780e..80b0911b2d41453ef2ff3b8789af110933e99806 100644 (file)
--- 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 f94c656827dc48d6fe0c205c15a4305c7406b319..2d04b7d11f97caf667e4361387ccd29e8a7faa58 100644 (file)
--- 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 27b46431ed49b1eedf2e3be8f52386e0ecc3fc92..258e83c949da272dd1b412faa010fe5d7b558b4f 100644 (file)
--- 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 ccac8dff67e78112bf8b5379082dbfb5826bed65..c260e8c61a70c9f1c29f80e9b0f3c6367bb10eea 100644 (file)
--- 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