helm/software/components/ng_kernel/nCicLibrary.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 (* $Id$ *)
  13
  14 exception LibraryOutOfSync of string Lazy.t
  15
  16 let magic = 0;;
  17
  18 let refresh_uri uri = NUri.uri_of_string (NUri.string_of_uri uri);;
  19
  20 let rec refresh_uri_in_term =
  21  function
  22     NCic.Const (NReference.Ref (u,spec)) ->
  23      NCic.Const (NReference.reference_of_spec (refresh_uri u) spec)
  24   | t -> NCicUtils.map (fun _ _ -> ()) () (fun _ -> refresh_uri_in_term) t
  25 ;;
  26
  27 let refresh_uri_in_obj (uri,height,metasenv,subst,obj_kind) =
  28  assert (metasenv = []);
  29  assert (subst = []);
  30  uri,height,metasenv,subst,
  31   NCicUntrusted.map_obj_kind refresh_uri_in_term obj_kind
  32 ;;
  33
  34 let path_of_baseuri ?(no_suffix=false) baseuri =
  35  let uri = NUri.string_of_uri baseuri in
  36  let path = String.sub uri 4 (String.length uri - 4) in
  37  let path = Helm_registry.get "matita.basedir" ^ path in
  38  let dirname = Filename.dirname path in
  39   HExtlib.mkdir dirname;
  40   if no_suffix then
  41    path
  42   else
  43    path ^ ".ng"
  44 ;;
  45
  46 let require_path path =
  47  let ch = open_in path in
  48  let mmagic,dump = Marshal.from_channel ch in
  49   close_in ch;
  50   if mmagic <> magic then
  51    raise (LibraryOutOfSync (lazy "The library is out of sync with the implementation. Please recompile the library."))
  52   else
  53    dump
  54 ;;
  55
  56 let require0 ~baseuri = require_path (path_of_baseuri baseuri);;
  57
  58 let db_path () = Helm_registry.get "matita.basedir" ^ "/ng_db.ng";;
  59
  60 type timestamp =
  61  (NUri.uri * NCic.obj) list *
  62  (NUri.uri * string * NReference.reference) list *
  63  NCic.obj NUri.UriMap.t;;
  64
  65 let time0 = [],[],NUri.UriMap.empty;;
  66 let storage = ref [];;
  67 let local_aliases = ref [];;
  68
  69 let set_global_aliases,get_global_aliases =
  70  let global_aliases = ref [] in
  71   let store_db () =
  72    let ch = open_out (db_path ()) in
  73    Marshal.to_channel ch (magic,!global_aliases) [];
  74    close_out ch;
  75   in
  76   (fun ga -> global_aliases := ga; store_db ()),
  77   (fun () -> !global_aliases)
  78 ;;
  79
  80 let init () =
  81  try
  82   let global_aliases = require_path (db_path ()) in
  83   let global_aliases =
  84    List.map
  85     (fun (uri,name,NReference.Ref (uri2,spec)) ->
  86       refresh_uri uri,name,NReference.reference_of_spec (refresh_uri uri2) spec
  87     ) global_aliases
  88   in
  89    set_global_aliases global_aliases
  90  with
  91   Sys_error _ -> ()
  92 ;;
  93
  94 let cache = ref NUri.UriMap.empty;;
  95
  96 class status =
  97  object
  98   val timestamp = (time0 : timestamp)
  99   method timestamp = timestamp
 100   method set_timestamp v = {< timestamp = v >}
 101   method set_library_status
 102    : 'status. < timestamp : timestamp; .. > as 'status -> 'self
 103    = fun o -> {< timestamp = o#timestamp >}
 104  end
 105
 106 let time_travel status =
 107  let sto,ali,cac = status#timestamp in
 108   storage := sto; local_aliases := ali; cache := cac
 109 ;;
 110
 111 let serialize ~baseuri dump =
 112  let ch = open_out (path_of_baseuri baseuri) in
 113  Marshal.to_channel ch (magic,dump) [];
 114  close_out ch;
 115  List.iter
 116   (fun (uri,obj) ->
 117     let ch = open_out (path_of_baseuri uri) in
 118     Marshal.to_channel ch (magic,obj) [];
 119     close_out ch
 120   ) !storage;
 121  set_global_aliases (!local_aliases @ get_global_aliases ());
 122  time_travel (new status)
 123 ;;
 124
 125 module type Serializer =
 126  sig
 127   type status
 128   type obj
 129   val register:
 130    string ->
 131     ('a -> refresh_uri_in_term:(NCic.term -> NCic.term) -> status -> status) ->
 132     ('a -> obj)
 133   val serialize: baseuri:NUri.uri -> obj list -> unit
 134   val require: baseuri:NUri.uri -> status -> status
 135  end
 136
 137 module Serializer(S: sig type status end) =
 138  struct
 139   type status = S.status
 140   type obj = string * Obj.t
 141
 142   let require1 = ref (fun _ -> assert false (* unknown data*))
 143   let already_registered = ref []
 144
 145   let register tag require =
 146    assert (not (List.mem tag !already_registered));
 147    already_registered := tag :: !already_registered;
 148    require1 :=
 149     (fun (tag',data) as x ->
 150      if tag=tag' then
 151       require (Obj.magic data) ~refresh_uri_in_term
 152      else
 153       !require1 x);
 154    (fun x -> tag,Obj.repr x)
 155
 156   let serialize = serialize
 157
 158   let require ~baseuri status =
 159    let dump = require0 ~baseuri in
 160     List.fold_right !require1 dump status
 161 end
 162
 163 let decompile ~baseuri =
 164  HExtlib.safe_remove (path_of_baseuri baseuri);
 165  let basepath = path_of_baseuri ~no_suffix:true baseuri in
 166  try
 167   let od = Unix.opendir basepath in
 168   let rec aux names =
 169    try
 170     let name = Unix.readdir od in
 171      if name <> "." && name <> ".." then aux (name::names) else aux names
 172    with
 173     End_of_file -> names in
 174   let names = List.map (fun name -> basepath ^ "/" ^ name) (aux []) in
 175    Unix.closedir od;
 176    List.iter Unix.unlink names;
 177    HExtlib.rmdir_descend basepath;
 178    set_global_aliases
 179     (List.filter
 180      (fun (_,_,NReference.Ref (nuri,_)) ->
 181        Filename.dirname (NUri.string_of_uri nuri) <> NUri.string_of_uri baseuri
 182      ) (get_global_aliases ()))
 183  with
 184   Unix.Unix_error _ -> () (* raised by Unix.opendir, we hope :-) *)
 185 ;;
 186
 187 LibraryClean.set_decompile_cb
 188  (fun ~baseuri -> decompile ~baseuri:(NUri.uri_of_string baseuri));;
 189
 190 let fetch_obj uri =
 191  let obj = require0 ~baseuri:uri in
 192   refresh_uri_in_obj obj
 193 ;;
 194
 195 let resolve name =
 196  try
 197   HExtlib.filter_map
 198    (fun (_,name',nref) -> if name'=name then Some nref else None)
 199    (!local_aliases @ get_global_aliases ())
 200  with
 201   Not_found -> raise (NCicEnvironment.ObjectNotFound (lazy name))
 202 ;;
 203
 204 let aliases_of uri =
 205  try
 206   HExtlib.filter_map
 207    (fun (uri',_,nref) ->
 208      if NUri.eq uri' uri then Some nref else None) !local_aliases
 209  with
 210   Not_found -> raise (NCicEnvironment.ObjectNotFound (lazy (NUri.string_of_uri uri)))
 211 ;;
 212
 213 let add_obj status u obj =
 214  storage := (u,obj)::!storage;
 215   let _,height,_,_,obj = obj in
 216   let references =
 217    match obj with
 218       NCic.Constant (_,name,None,_,_) ->
 219        [u,name,NReference.reference_of_spec u NReference.Decl]
 220     | NCic.Constant (_,name,Some _,_,_) ->
 221        [u,name,NReference.reference_of_spec u (NReference.Def height)]
 222     | NCic.Fixpoint (is_ind,fl,_) ->
 223        HExtlib.list_mapi
 224         (fun (_,name,recno,_,_) i ->
 225           if is_ind then
 226            u,name,NReference.reference_of_spec u(NReference.Fix(i,recno,height))
 227           else
 228            u,name,NReference.reference_of_spec u (NReference.CoFix i)) fl
 229     | NCic.Inductive (inductive,leftno,il,_) ->
 230        List.flatten
 231         (HExtlib.list_mapi
 232          (fun (_,iname,_,cl) i ->
 233            HExtlib.list_mapi
 234             (fun (_,cname,_) j->
 235               u,cname,
 236                NReference.reference_of_spec u (NReference.Con (i,j+1,leftno))
 237             ) cl @
 238            [u,iname,
 239              NReference.reference_of_spec u
 240               (NReference.Ind (inductive,i,leftno))]
 241          ) il)
 242   in
 243   local_aliases := references @ !local_aliases;
 244   status#set_timestamp (!storage,!local_aliases,!cache)
 245 ;;
 246
 247 let get_obj u =
 248  try List.assq u !storage
 249  with Not_found ->
 250   try fetch_obj u
 251   with Sys_error _ ->
 252    try NUri.UriMap.find u !cache
 253    with Not_found ->
 254     let ouri = NCic2OCic.ouri_of_nuri u in
 255     try
 256       let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph ouri in
 257       let l = OCic2NCic.convert_obj ouri o in
 258       List.iter (fun (u,_,_,_,_ as o) -> cache:= NUri.UriMap.add u o !cache) l;
 259       HExtlib.list_last l
 260     with CicEnvironment.Object_not_found u ->
 261       raise (NCicEnvironment.ObjectNotFound
 262                (lazy (NUri.string_of_uri (OCic2NCic.nuri_of_ouri u))))
 263 ;;
 264
 265 let clear_cache () = cache := NUri.UriMap.empty;;
 266
 267 NCicEnvironment.set_get_obj get_obj;;
 268 NCicPp.set_get_obj get_obj;;