X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicLibrary.ml;h=e7d7c3b11d21a71b677713a5725801995f299ef0;hb=ddd6560f4e70ec3306d223738a441d5f1dd3eac9;hp=fa96a69b44224ff44c3642ae02d323152aa48c45;hpb=e02c6eaf8d50025c3be8bbf6988ab8b2a37b40da;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicLibrary.ml b/helm/software/components/ng_kernel/nCicLibrary.ml
index fa96a69b4..e7d7c3b11 100644
--- a/helm/software/components/ng_kernel/nCicLibrary.ml
+++ b/helm/software/components/ng_kernel/nCicLibrary.ml
@@ -11,71 +11,334 @@
 
 (* $Id$ *)
 
-exception ObjectNotFound of string Lazy.t
+exception LibraryOutOfSync of string Lazy.t
 
+let magic = 2;;
+
+let refresh_uri uri = NUri.uri_of_string (NUri.string_of_uri uri);;
+
+let refresh_uri_in_universe =
+ List.map (fun (x,u) -> x, refresh_uri u)
+;;
+
+let rec refresh_uri_in_term =
+ function
+  | NCic.Meta (i,(n,NCic.Ctx l)) ->
+     NCic.Meta (i,(n,NCic.Ctx (List.map refresh_uri_in_term l)))
+  | NCic.Meta _ as t -> t
+  | NCic.Const (NReference.Ref (u,spec)) ->
+     NCic.Const (NReference.reference_of_spec (refresh_uri u) spec)
+  | NCic.Sort (NCic.Type l) -> NCic.Sort (NCic.Type (refresh_uri_in_universe l))
+  | NCic.Match (NReference.Ref (uri,spec),outtype,term,pl) ->
+     let r = NReference.reference_of_spec (refresh_uri uri) spec in
+     let outtype = refresh_uri_in_term outtype in
+     let term = refresh_uri_in_term term in
+     let pl = List.map refresh_uri_in_term pl in
+      NCic.Match (r,outtype,term,pl)
+  | 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 = []);
+ refresh_uri uri,height,metasenv,subst,
+  NCicUntrusted.map_obj_kind refresh_uri_in_term obj_kind
+;;
+
+let path_of_baseuri ?(no_suffix=false) baseuri =
+ let uri = NUri.string_of_uri baseuri in
+ let path = String.sub uri 4 (String.length uri - 4) in
+ let path = Helm_registry.get "matita.basedir" ^ path in
+ let dirname = Filename.dirname path in
+  HExtlib.mkdir dirname;
+  if no_suffix then
+   path
+  else
+   path ^ ".ng"
+;;
+
+let require_path path =
+ let ch = open_in path in
+ let mmagic,dump = Marshal.from_channel ch in
+  close_in ch;
+  if mmagic <> magic then
+   raise (LibraryOutOfSync (lazy "The library is out of sync with the implementation. Please recompile the library."))
+  else
+   dump
+;;
+
+let require0 ~baseuri = require_path (path_of_baseuri baseuri);;
+
+let db_path () = Helm_registry.get "matita.basedir" ^ "/ng_db.ng";;
+
+
+type timestamp =
+ [ `Obj of NUri.uri * NCic.obj 
+ | `Constr of NCic.universe * NCic.universe] list *
+ (NUri.uri * string * NReference.reference) list *
+ NCic.obj NUri.UriMap.t *
+ NUri.uri list
+;;
+
+let time0 = [],[],NUri.UriMap.empty,[];;
 let storage = ref [];;
+let local_aliases = ref [];;
+let cache = ref NUri.UriMap.empty;;
+let includes = ref [];;
+
+let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps=
+ let global_aliases = ref [] in
+ let rev_includes_map = ref NUri.UriMap.empty in
+ let store_db () =
+  let ch = open_out (db_path ()) in
+  Marshal.to_channel ch (magic,(!global_aliases,!rev_includes_map)) [];
+  close_out ch in
+ let load_db () =
+  HExtlib.mkdir (Helm_registry.get "matita.basedir");
+  try
+   let ga,im = require_path (db_path ()) in
+   let ga =
+    List.map
+     (fun (uri,name,NReference.Ref (uri2,spec)) ->
+       refresh_uri uri,name,NReference.reference_of_spec (refresh_uri uri2) spec
+     ) ga in
+   let im =
+    NUri.UriMap.fold
+     (fun u l im -> NUri.UriMap.add (refresh_uri u) (List.map refresh_uri l) im
+     ) im NUri.UriMap.empty
+   in
+    global_aliases := ga;
+    rev_includes_map := im
+  with
+   Sys_error _ -> () in
+ let get_deps u =
+  let get_deps_one_step u =
+    try NUri.UriMap.find u !rev_includes_map with Not_found -> [] in
+  let rec aux res =
+   function
+      [] -> res
+    | he::tl ->
+       if List.mem he res then
+        aux res tl
+       else
+        aux (he::res) (get_deps_one_step he @ tl)
+  in
+   aux [] [u] in
+ let remove_deps u =
+  rev_includes_map := NUri.UriMap.remove u !rev_includes_map;
+  rev_includes_map :=
+   NUri.UriMap.map
+    (fun l -> List.filter (fun uri -> not (NUri.eq u uri)) l) !rev_includes_map;
+  store_db ()
+ in
+  load_db,
+  (fun ga -> global_aliases := ga; store_db ()),
+  (fun () -> !global_aliases),
+  (fun u l ->
+    rev_includes_map := NUri.UriMap.add u (l @ get_deps u) !rev_includes_map;
+    store_db ()),
+  get_deps,
+  remove_deps
+;;
+
+let init = load_db;;
+
+class type g_status =
+ object
+  method timestamp: timestamp
+ end
 
-let aliases = ref [];;
+class status =
+ object
+  val timestamp = (time0 : timestamp)
+  method timestamp = timestamp
+  method set_timestamp v = {< timestamp = v >}
+  method set_library_status
+   : 'status. #g_status as 'status -> 'self
+   = fun o -> {< timestamp = o#timestamp >}
+ end
+
+let time_travel status =
+ let sto,ali,cac,inc = status#timestamp in
+  let diff_len = List.length !storage - List.length sto in
+  let to_be_deleted,_ = HExtlib.split_nth diff_len !storage in
+   if List.length to_be_deleted > 0 then
+     NCicEnvironment.invalidate_item (HExtlib.list_last to_be_deleted);
+   storage := sto; local_aliases := ali; cache := cac; includes := inc
+;;
+
+let serialize ~baseuri dump =
+ let ch = open_out (path_of_baseuri baseuri) in
+ Marshal.to_channel ch (magic,dump) [];
+ close_out ch;
+ List.iter
+  (function 
+   | `Obj (uri,obj) ->
+       let ch = open_out (path_of_baseuri uri) in
+       Marshal.to_channel ch (magic,obj) [];
+       close_out ch
+   | `Constr _ -> ()
+  ) !storage;
+ set_global_aliases (!local_aliases @ get_global_aliases ());
+ List.iter (fun u -> add_deps u [baseuri]) !includes;
+ time_travel (new status)
+;;
+
+module type Serializer =
+ sig
+  type status
+  type obj
+  val register:
+   string ->
+    ('a -> refresh_uri_in_universe:(NCic.universe -> NCic.universe) -> refresh_uri_in_term:(NCic.term -> NCic.term) -> status -> status) ->
+    ('a -> obj)
+  val serialize: baseuri:NUri.uri -> obj list -> unit
+  val require: baseuri:NUri.uri -> status -> status
+ end
+
+module Serializer(S: sig type status end) =
+ struct
+  type status = S.status
+  type obj = string * Obj.t
+
+  let require1 = ref (fun _ -> assert false (* unknown data*))
+  let already_registered = ref []
+
+  let register tag require =
+   assert (not (List.mem tag !already_registered));
+   already_registered := tag :: !already_registered;
+   let old_require1 = !require1 in
+   require1 :=
+     (fun (tag',data) as x ->
+      if tag=tag' then
+       require (Obj.magic data) ~refresh_uri_in_universe ~refresh_uri_in_term 
+      else
+       old_require1 x);
+   (fun x -> tag,Obj.repr x)
+
+  let serialize = serialize
+
+  let require ~baseuri status =
+   includes := baseuri::!includes;
+   let dump = require0 ~baseuri in
+    List.fold_right !require1 dump status
+end
+
+let decompile ~baseuri =
+ let baseuris = get_deps baseuri in
+ List.iter (fun baseuri ->
+  remove_deps baseuri;
+  HExtlib.safe_remove (path_of_baseuri baseuri);
+  let basepath = path_of_baseuri ~no_suffix:true baseuri in
+  try
+   let od = Unix.opendir basepath in
+   let rec aux names =
+    try
+     let name = Unix.readdir od in
+      if name <> "." && name <> ".." then aux (name::names) else aux names
+    with
+     End_of_file -> names in
+   let names = List.map (fun name -> basepath ^ "/" ^ name) (aux []) in
+    Unix.closedir od;
+    List.iter Unix.unlink names;
+    HExtlib.rmdir_descend basepath;
+    set_global_aliases
+     (List.filter
+      (fun (_,_,NReference.Ref (nuri,_)) ->
+        Filename.dirname (NUri.string_of_uri nuri) <> NUri.string_of_uri baseuri
+      ) (get_global_aliases ()))
+  with
+   Unix.Unix_error _ -> () (* raised by Unix.opendir, we hope :-) *)
+ ) baseuris
+;;
+
+LibraryClean.set_decompile_cb
+ (fun ~baseuri -> decompile ~baseuri:(NUri.uri_of_string baseuri));;
+
+let fetch_obj uri =
+ let obj = require0 ~baseuri:uri in
+  refresh_uri_in_obj obj
+;;
 
 let resolve name =
  try
   HExtlib.filter_map
-   (fun (name',nref) -> if name'=name then Some nref else None) !aliases
+   (fun (_,name',nref) -> if name'=name then Some nref else None)
+   (!local_aliases @ get_global_aliases ())
  with
-  Not_found -> raise (ObjectNotFound (lazy name))
+  Not_found -> raise (NCicEnvironment.ObjectNotFound (lazy name))
 ;;
 
-let add_obj u obj =
- storage := (u,obj)::!storage;
+let aliases_of uri =
+  HExtlib.filter_map
+   (fun (uri',_,nref) ->
+     if NUri.eq uri' uri then Some nref else None) !local_aliases
+;;
+
+let add_obj status ((u,_,_,_,_) as obj) =
+ NCicEnvironment.check_and_add_obj obj;
+ storage := (`Obj (u,obj))::!storage;
   let _,height,_,_,obj = obj in
   let references =
    match obj with
       NCic.Constant (_,name,None,_,_) ->
-       [name,NReference.reference_of_spec u NReference.Decl]
+       [u,name,NReference.reference_of_spec u NReference.Decl]
     | NCic.Constant (_,name,Some _,_,_) ->
-       [name,NReference.reference_of_spec u (NReference.Def height)]
+       [u,name,NReference.reference_of_spec u (NReference.Def height)]
     | NCic.Fixpoint (is_ind,fl,_) ->
        HExtlib.list_mapi
         (fun (_,name,recno,_,_) i ->
           if is_ind then
-           name,NReference.reference_of_spec u (NReference.Fix(i,recno,height))
+           u,name,NReference.reference_of_spec u(NReference.Fix(i,recno,height))
           else
-           name,NReference.reference_of_spec u (NReference.CoFix i)) fl
+           u,name,NReference.reference_of_spec u (NReference.CoFix i)) fl
     | NCic.Inductive (inductive,leftno,il,_) ->
        List.flatten
         (HExtlib.list_mapi
          (fun (_,iname,_,cl) i ->
            HExtlib.list_mapi
             (fun (_,cname,_) j->
-              cname,NReference.reference_of_spec u (NReference.Con (i,j,leftno))
+              u,cname,
+               NReference.reference_of_spec u (NReference.Con (i,j+1,leftno))
             ) cl @
-           [iname,
+           [u,iname,
              NReference.reference_of_spec u
               (NReference.Ind (inductive,i,leftno))]
          ) il)
   in
-   aliases := references @ !aliases
+  local_aliases := references @ !local_aliases;
+  status#set_timestamp (!storage,!local_aliases,!cache,!includes)
 ;;
 
-let cache = NUri.UriHash.create 313;;
+let add_constraint status u1 u2 = 
+  NCicEnvironment.add_lt_constraint u1 u2;
+  storage := (`Constr (u1,u2)) :: !storage;
+  status#set_timestamp (!storage,!local_aliases,!cache,!includes)
+;;
 
 let get_obj u =
- try List.assq u !storage
+ try 
+  List.assq u 
+   (HExtlib.filter_map 
+    (function `Obj (u,o) -> Some (u,o) | _ -> None )
+    !storage)
  with Not_found ->
-  try NUri.UriHash.find cache u
-  with Not_found ->
-    (* in the final implementation should get it from disk *)
+  try fetch_obj u
+  with Sys_error _ ->
+   try NUri.UriMap.find u !cache
+   with Not_found ->
     let ouri = NCic2OCic.ouri_of_nuri u in
     try
       let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph ouri in
       let l = OCic2NCic.convert_obj ouri o in
-      List.iter (fun (u,_,_,_,_ as o) -> 
-  (*       prerr_endline ("+"^NUri.string_of_uri u);  *)
-        NUri.UriHash.add cache u o) l;
+      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 () = NUri.UriHash.clear cache;;
+let clear_cache () = cache := NUri.UriMap.empty;;
+
+NCicEnvironment.set_get_obj get_obj;;
+NCicPp.set_get_obj get_obj;;