X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_library%2FnCicLibrary.ml;h=a7e35f42796500ab47b434d2b7980b09a90bf04f;hb=41b61472d2c475e0f69e3dfc85539da3ad2bac1e;hp=92c57b12391f960ec09f6693c3d364ef5b50e83c;hpb=2914bfbeac3c2e0f53ba8c612cd11b3b2afbabce;p=helm.git

diff --git a/matitaB/components/ng_library/nCicLibrary.ml b/matitaB/components/ng_library/nCicLibrary.ml
index 92c57b123..a7e35f427 100644
--- a/matitaB/components/ng_library/nCicLibrary.ml
+++ b/matitaB/components/ng_library/nCicLibrary.ml
@@ -16,6 +16,8 @@ exception IncludedFileNotCompiled of string * string
 
 let magic = 2;;
 
+let prerr_endline _ = ()
+
 let refresh_uri uri = NUri.uri_of_string (NUri.string_of_uri uri);;
 
 let refresh_uri_in_universe =
@@ -51,9 +53,13 @@ let refresh_uri_in_obj status (uri,height,metasenv,subst,obj_kind) =
   NCicUntrusted.map_obj_kind (refresh_uri_in_term status) obj_kind
 ;;
 
-let ng_path_of_baseuri ?(no_suffix=false) baseuri =
+let ng_path_of_baseuri ?(no_suffix=false) user baseuri =
  let uri = NUri.string_of_uri baseuri in
  let path = String.sub uri 4 (String.length uri - 4) in
+ let path = match user with
+ | Some u -> "/" ^ u ^ path
+ | _ -> prerr_endline "WARNING: ng_path_of_baseuri called without a uid"; path
+ in
  let path = Helm_registry.get "matita.basedir" ^ path in
  let dirname = Filename.dirname path in
   HExtlib.mkdir dirname;
@@ -73,9 +79,14 @@ let require_path path =
    dump
 ;;
 
-let require0 ~baseuri = require_path (ng_path_of_baseuri baseuri)
+let require0 user ~baseuri = require_path (ng_path_of_baseuri user baseuri)
 
-let db_path () = Helm_registry.get "matita.basedir" ^ "/ng_db.ng";;
+let db_path user =
+ let midpath = match user with
+  | None -> ""
+  | Some u -> "/" ^ u
+ in
+ Helm_registry.get "matita.basedir" ^ midpath ^ "/ng_db.ng";;
 
 type timestamp =
  [ `Obj of NUri.uri * NCic.obj 
@@ -84,20 +95,36 @@ type timestamp =
 ;;
 
 let time0 = [],[];;
-let storage = ref [];;
-let local_aliases = ref [];;
+
+let global_aliases_db = ref [];;
+let rev_includes_map_db = ref [];;
+
+let global_aliases u = 
+  try List.assoc u !global_aliases_db
+  with Not_found -> 
+   let db = ref [] in
+   global_aliases_db := (u,db)::!global_aliases_db;
+   db
+;;
+
+let rev_includes_map u = 
+  try List.assoc u !rev_includes_map_db
+  with Not_found -> 
+   let db = ref NUri.UriMap.empty in
+   rev_includes_map_db := (u,db)::!rev_includes_map_db;
+   db
+;;
 
 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)) [];
+ let store_db user =
+  let ch = open_out (db_path user) in
+  Marshal.to_channel ch (magic,(!(global_aliases user),!(rev_includes_map user))) [];
   close_out ch in
- let load_db () =
+ let load_db user =
   HExtlib.mkdir (Helm_registry.get "matita.basedir");
+  if user <> None then HExtlib.mkdir ((Helm_registry.get "matita.basedir") ^ "/" ^ HExtlib.unopt user);
   try
-   let ga,im = require_path (db_path ()) in
+   let ga,im = require_path (db_path user) in
    let ga =
     List.map
      (fun (uri,name,NReference.Ref (uri2,spec)) ->
@@ -108,13 +135,13 @@ let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps=
      (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
+    global_aliases user := ga;
+    rev_includes_map user := im
   with
    Sys_error _ -> () in
- let get_deps u =
+ let get_deps user u =
   let get_deps_one_step u =
-    try NUri.UriMap.find u !rev_includes_map with Not_found -> [] in
+    try NUri.UriMap.find u !(rev_includes_map user) with Not_found -> [] in
   let rec aux res =
    function
       [] -> res
@@ -125,42 +152,79 @@ let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps=
         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 :=
+ let remove_deps user u =
+  rev_includes_map user := NUri.UriMap.remove u !(rev_includes_map user);
+  rev_includes_map user :=
    NUri.UriMap.map
-    (fun l -> List.filter (fun uri -> not (NUri.eq u uri)) l) !rev_includes_map;
-  store_db ()
+    (fun l -> List.filter (fun uri -> not (NUri.eq u uri)) l) !(rev_includes_map user);
+  store_db user
  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 ()),
+  (fun user ga -> global_aliases user := ga; store_db user),
+  (fun user -> !(global_aliases user)),
+  (fun user u l ->
+    rev_includes_map user := NUri.UriMap.add u (l @ get_deps user u) !(rev_includes_map user);
+    store_db user),
   get_deps,
   remove_deps
 ;;
 
 let init = load_db;;
 
-class virtual status =
+type db = {
+  storage : 
+    [ `Obj of NUri.uri * NCic.obj 
+    | `Constr of NCic.universe * NCic.universe] list ref;
+  local_aliases : 
+    (NUri.uri * string * NReference.reference) list ref
+}
+
+class type g_status =
+  object
+    inherit NCicEnvironment.g_status
+    method lib_db : db
+  end
+
+class virtual status uid =
  object
-  inherit NCic.status
+  inherit NCicEnvironment.status uid
+
+  val lib_db = {
+    storage = ref [];
+    local_aliases = ref []
+  }
+  method lib_db = lib_db
+
   val timestamp = (time0 : timestamp)
   method timestamp = timestamp
+
+  method print_timestamp () = 
+    prerr_endline ("length(lib_db.storage) = " ^
+                   string_of_int (List.length !(lib_db.storage)));
+    prerr_endline ("length(timestamp.storage) = " ^
+                   string_of_int (List.length (fst timestamp)));
   method set_timestamp v = {< timestamp = v >}
+  method set_lib_db v = {< lib_db = v >}
+  method set_lib_status : 's.#g_status as 's -> 'self
+   = fun o -> {< lib_db = o#lib_db >}#set_env_status o
  end
 
-let time_travel0 (sto,ali) =
- let diff_len = List.length !storage - List.length sto in
- let to_be_deleted,_ = HExtlib.split_nth diff_len !storage in
+let reset_timestamp st =
+  st#lib_db.storage := [];
+  st#lib_db.local_aliases := []
+;;
+
+let time_travel0 st (sto,ali) =
+ prerr_endline ("length of lib_db.storage = " ^ (string_of_int (List.length !(st#lib_db.storage))));
+ prerr_endline ("length of sto = " ^ (string_of_int (List.length sto)));
+ let diff_len = List.length !(st#lib_db.storage) - List.length sto in
+ let to_be_deleted,_ = HExtlib.split_nth diff_len !(st#lib_db.storage) in
   if List.length to_be_deleted > 0 then
-   List.iter NCicEnvironment.invalidate_item to_be_deleted;
-  storage := sto; local_aliases := ali
+   List.iter (NCicEnvironment.invalidate_item st) to_be_deleted;
+  st#lib_db.storage := sto; st#lib_db.local_aliases := ali
 ;;
 
-let time_travel status = time_travel0 status#timestamp;;
+let time_travel status = time_travel0 status status#timestamp;;
 
 type obj = string * Obj.t
 (* includes are transitively closed; dependencies are only immediate *)
@@ -172,8 +236,12 @@ class type g_dumpable_status =
   method dump: dump
  end
 
-class dumpable_status =
+(* uid = None --> single user mode *)
+class dumpable_status uid =
  object
+  inherit NCicPp.status uid
+  inherit status uid
+
   val db = { objs = []; includes = []; dependencies = [] }
   method dump = db
   method set_dump v = {< db = v >}
@@ -197,7 +265,7 @@ module type SerializerType =
   type 'a register_type =
    'a ->
     refresh_uri_in_universe:(NCic.universe -> NCic.universe) ->
-    refresh_uri_in_term:(NCic.status -> NCic.term -> NCic.term) ->
+    refresh_uri_in_term:(NCicEnvironment.status -> NCic.term -> NCic.term) ->
     refresh_uri_in_reference:(NReference.reference -> NReference.reference) ->
     alias_only:bool ->
      dumpable_status -> dumpable_status
@@ -207,16 +275,18 @@ module type SerializerType =
   val require:
    baseuri:NUri.uri -> fname:string -> alias_only:bool ->
     dumpable_status -> dumpable_status
-  val dependencies_of: baseuri:NUri.uri -> string list
+  val dependencies_of: string option -> baseuri:NUri.uri -> string list
  end
 
-module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status  val set: dumpable_s -> dumpable_status -> dumpable_s end) =
+module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status
+  val set: dumpable_s -> dumpable_status -> dumpable_s val user : dumpable_s ->
+  string option end) =
  struct
   type dumpable_status = D.dumpable_s
   type 'a register_type =
    'a ->
     refresh_uri_in_universe:(NCic.universe -> NCic.universe) ->
-    refresh_uri_in_term:(NCic.status -> NCic.term -> NCic.term) ->
+    refresh_uri_in_term:(NCicEnvironment.status -> NCic.term -> NCic.term) ->
     refresh_uri_in_reference:(NReference.reference -> NReference.reference) ->
     alias_only:bool ->
      dumpable_status -> dumpable_status
@@ -245,21 +315,23 @@ module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status
    end
 
   let serialize ~baseuri status =
-   let status = D.get status in
-   let ch = open_out (ng_path_of_baseuri baseuri) in
-   Marshal.to_channel ch (magic,(status#dump.dependencies,status#dump.objs)) [];
+   let ch = open_out (ng_path_of_baseuri (D.get status)#user baseuri) in
+   Marshal.to_channel ch (magic,((D.get status)#dump.dependencies,(D.get status)#dump.objs)) [];
    close_out ch;
+   let deps = String.concat ", " ((D.get status)#dump.dependencies) in 
+   prerr_endline ("dumping dependencies:\n" ^ deps ^ "\nend of deps");
    List.iter
     (function 
      | `Obj (uri,obj) ->
-         let ch = open_out (ng_path_of_baseuri uri) in
+         let ch = open_out (ng_path_of_baseuri (D.get status)#user 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]) status#dump.includes;
-   time_travel0 time0
+    ) !((D.get status)#lib_db.storage);
+   let user = D.user status in
+   set_global_aliases user (!((D.get status)#lib_db.local_aliases) @ get_global_aliases user);
+   List.iter (fun u -> add_deps (D.user status) u [baseuri]) (D.get status)#dump.includes;
+   reset_timestamp (D.get status)
 
   let require2 ~baseuri ~alias_only status =
    try
@@ -269,13 +341,13 @@ module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status
       (s#set_dump
         {s#dump with
         includes = baseuri::List.filter ((<>) baseuri) s#dump.includes}) in
-    let _dependencies,dump = require0 ~baseuri in
+    let _dependencies,dump = require0 (D.get status)#user ~baseuri in
      List.fold_right (!require1 ~alias_only) dump status
    with
     Sys_error _ ->
-     raise (IncludedFileNotCompiled(ng_path_of_baseuri baseuri,NUri.string_of_uri baseuri))
+     raise (IncludedFileNotCompiled(ng_path_of_baseuri (D.get status)#user baseuri,NUri.string_of_uri baseuri))
 
-  let dependencies_of ~baseuri = fst (require0 ~baseuri)
+  let dependencies_of user ~baseuri = fst (require0 user ~baseuri)
 
   let record_include =
    let aux (baseuri,fname) ~refresh_uri_in_universe:_ ~refresh_uri_in_term:_
@@ -311,29 +383,31 @@ module Serializer(D: sig type dumpable_s val get: dumpable_s -> dumpable_status
          objs = record_include (baseuri,fname)::s#dump.objs })
 end
 
-let fetch_obj status uri =
- let obj = require0 ~baseuri:uri in
+let fetch_obj user status uri =
+ let obj = require0 user ~baseuri:uri in
   refresh_uri_in_obj status obj
 ;;
 
-let resolve name =
+let resolve st name =
  try
   HExtlib.filter_map
    (fun (_,name',nref) -> if name'=name then Some nref else None)
-   (!local_aliases @ get_global_aliases ())
+   (!(st#lib_db.local_aliases) @ get_global_aliases st#user)
  with
-  Not_found -> raise (NCicEnvironment.ObjectNotFound (lazy name))
+  Not_found -> 
+   (prerr_endline ("can't resolve object " ^ name);
+    raise (NCicEnvironment.ObjectNotFound (lazy name)))
 ;;
 
-let aliases_of uri =
+let aliases_of st uri =
   HExtlib.filter_map
    (fun (uri',_,nref) ->
-     if NUri.eq uri' uri then Some nref else None) !local_aliases
+     if NUri.eq uri' uri then Some nref else None) !(st#lib_db.local_aliases)
 ;;
 
 let add_obj status ((u,_,_,_,_) as obj) =
  NCicEnvironment.check_and_add_obj status obj;
- storage := (`Obj (u,obj))::!storage;
+ status#lib_db.storage := (`Obj (u,obj))::!(status#lib_db.storage);
   let _,height,_,_,obj = obj in
   let references =
    match obj with
@@ -362,33 +436,36 @@ let add_obj status ((u,_,_,_,_) as obj) =
               (NReference.Ind (inductive,i,leftno))]
          ) il)
   in
-  local_aliases := references @ !local_aliases;
-  status#set_timestamp (!storage,!local_aliases)
+  status#lib_db.local_aliases := references @ !(status#lib_db.local_aliases);
+  status#set_timestamp (!(status#lib_db.storage),!(status#lib_db.local_aliases))
 ;;
 
 let add_constraint status u1 u2 = 
   if
    List.exists
     (function `Constr (u1',u2') when u1=u1' && u2=u2' -> true | _ -> false)
-    !storage
+    !(status#lib_db.storage)
   then
    (*CSC: raise an exception here! *)
    (prerr_endline "CANNOT ADD A CONSTRAINT TWICE"; assert false);
-  NCicEnvironment.add_lt_constraint u1 u2;
-  storage := (`Constr (u1,u2)) :: !storage;
-  status#set_timestamp (!storage,!local_aliases)
+  NCicEnvironment.add_lt_constraint status u1 u2;
+  status#lib_db.storage := (`Constr (u1,u2)) :: !(status#lib_db.storage);
+  status#set_timestamp (!(status#lib_db.storage),!(status#lib_db.local_aliases))
 ;;
 
 let get_obj status u =
+(*
  try 
   List.assq u 
    (HExtlib.filter_map 
     (function `Obj (u,o) -> Some (u,o) | _ -> None )
-    !storage)
- with Not_found ->
-  try fetch_obj status u
+    !(status#lib_db.storage))
+ with Not_found ->*)
+  try fetch_obj (status#user) status u
   with Sys_error _ ->
-   raise (NCicEnvironment.ObjectNotFound (lazy (NUri.string_of_uri u)))
+   (prerr_endline ("can't fetch object " ^ NUri.string_of_uri u);
+   raise (NCicEnvironment.ObjectNotFound (lazy (NUri.string_of_uri u))))
 ;;
 
-NCicEnvironment.set_get_obj get_obj;;
+NCicEnvironment.set_get_obj 
+  (get_obj :> NCicEnvironment.status -> NUri.uri -> NCic.obj);;