X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_library%2FnCicLibrary.ml;h=ae6666be581fbae322e84226e43708be8cbc54b9;hb=4556677f40e6b979d9bdaa4475bb1ca6701264f8;hp=d4ea77a317ba7be499218c693ed028c62bd8dfae;hpb=aab0401db0bedd941da96a32acd600af3fbe42e7;p=helm.git

diff --git a/matita/components/ng_library/nCicLibrary.ml b/matita/components/ng_library/nCicLibrary.ml
index d4ea77a31..ae6666be5 100644
--- a/matita/components/ng_library/nCicLibrary.ml
+++ b/matita/components/ng_library/nCicLibrary.ml
@@ -22,13 +22,15 @@ let refresh_uri_in_universe =
  List.map (fun (x,u) -> x, refresh_uri u)
 ;;
 
+let refresh_uri_in_reference (NReference.Ref (uri,spec)) =
+ NReference.reference_of_spec (refresh_uri uri) spec
+
 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.Const ref -> NCic.Const (refresh_uri_in_reference ref)
   | 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
@@ -46,7 +48,7 @@ let refresh_uri_in_obj (uri,height,metasenv,subst,obj_kind) =
   NCicUntrusted.map_obj_kind refresh_uri_in_term obj_kind
 ;;
 
-let path_of_baseuri ?(no_suffix=false) baseuri =
+let ng_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
@@ -68,13 +70,10 @@ let require_path path =
    dump
 ;;
 
-let require0 ~baseuri =
-  require_path (path_of_baseuri baseuri)
-;;
+let require0 ~baseuri = require_path (ng_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 *
@@ -89,6 +88,8 @@ let local_aliases = ref [];;
 let cache = ref NUri.UriMap.empty;;
 let includes = ref [];;
 
+let get_already_included () = !includes;;
+
 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
@@ -146,19 +147,11 @@ let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps,remove_deps=
 
 let init = load_db;;
 
-class type g_status =
- object
-  method timestamp: timestamp
- end
-
 class status =
- object(self)
+ 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 -> self#set_timestamp o#timestamp
  end
 
 let time_travel status =
@@ -170,14 +163,14 @@ let time_travel status =
    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) [];
+let serialize ~baseuri ~dependencies dump =
+ let ch = open_out (ng_path_of_baseuri baseuri) in
+ Marshal.to_channel ch (magic,(dependencies,dump)) [];
  close_out ch;
  List.iter
   (function 
    | `Obj (uri,obj) ->
-       let ch = open_out (path_of_baseuri uri) in
+       let ch = open_out (ng_path_of_baseuri uri) in
        Marshal.to_channel ch (magic,obj) [];
        close_out ch
    | `Constr _ -> ()
@@ -190,7 +183,7 @@ let serialize ~baseuri dump =
 type obj = string * Obj.t
 
 class dumpable_status =
- object(self)
+ object
   val dump = ([] : obj list)
   method dump = dump
   method set_dump v = {< dump = v >}
@@ -204,12 +197,14 @@ module type SerializerType =
    'a ->
     refresh_uri_in_universe:(NCic.universe -> NCic.universe) ->
     refresh_uri_in_term:(NCic.term -> NCic.term) ->
+    refresh_uri_in_reference:(NReference.reference -> NReference.reference) ->
      dumpable_status -> dumpable_status
 
   val register: < run: 'a.  string -> 'a register_type -> ('a -> obj) >
-  val serialize: baseuri:NUri.uri -> obj list -> unit
+  val serialize: baseuri:NUri.uri -> dependencies:string list -> obj list -> unit
    (* the obj is the "include" command to be added to the dump list *)
   val require: baseuri:NUri.uri -> dumpable_status -> dumpable_status * obj
+  val dependencies_of: baseuri:NUri.uri -> string list
  end
 
 module Serializer(D: sig type dumpable_status end) =
@@ -219,6 +214,7 @@ module Serializer(D: sig type dumpable_status end) =
    'a ->
     refresh_uri_in_universe:(NCic.universe -> NCic.universe) ->
     refresh_uri_in_term:(NCic.term -> NCic.term) ->
+    refresh_uri_in_reference:(NReference.reference -> NReference.reference) ->
      dumpable_status -> dumpable_status
 
   let require1 = ref (fun _ -> assert false) (* unknown data*)
@@ -235,6 +231,7 @@ module Serializer(D: sig type dumpable_status end) =
       (fun ((tag',data) as x) ->
         if tag=tag' then
          require (Obj.magic data) ~refresh_uri_in_universe ~refresh_uri_in_term
+          ~refresh_uri_in_reference
         else
          old_require1 x);
      (fun x -> tag,Obj.repr x)
@@ -245,14 +242,17 @@ module Serializer(D: sig type dumpable_status end) =
   let require2 ~baseuri status =
    try
     includes := baseuri::!includes;
-    let dump = require0 ~baseuri in
+    let _dependencies,dump = require0 ~baseuri in
      List.fold_right !require1 dump status
    with
     Sys_error _ ->
-     raise (IncludedFileNotCompiled(path_of_baseuri baseuri,NUri.string_of_uri baseuri))
+     raise (IncludedFileNotCompiled(ng_path_of_baseuri baseuri,NUri.string_of_uri baseuri))
+
+  let dependencies_of ~baseuri = fst (require0 ~baseuri)
 
   let record_include =
-   let aux baseuri ~refresh_uri_in_universe ~refresh_uri_in_term =
+   let aux baseuri ~refresh_uri_in_universe ~refresh_uri_in_term
+   ~refresh_uri_in_reference =
      (* memorizzo baseuri in una tabella; *)
      require2 ~baseuri
    in
@@ -268,8 +268,8 @@ 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
+  HExtlib.safe_remove (ng_path_of_baseuri baseuri);
+  let basepath = ng_path_of_baseuri ~no_suffix:true baseuri in
   try
    let od = Unix.opendir basepath in
    let rec aux names =