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 = 1;;
  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  NUri.uri list;;
  65
  66 let time0 = [],[],NUri.UriMap.empty,[];;
  67 let storage = ref [];;
  68 let local_aliases = ref [];;
  69 let cache = ref NUri.UriMap.empty;;
  70 let includes = ref [];;
  71
  72 let load_db,set_global_aliases,get_global_aliases,add_deps,get_deps =
  73  let global_aliases = ref [] in
  74  let includes_map = ref NUri.UriMap.empty in
  75  let store_db () =
  76   let ch = open_out (db_path ()) in
  77   Marshal.to_channel ch (magic,(!global_aliases,!includes_map)) [];
  78   close_out ch in
  79  let load_db () =
  80   try
  81    let ga,im = require_path (db_path ()) in
  82    let ga =
  83     List.map
  84      (fun (uri,name,NReference.Ref (uri2,spec)) ->
  85        refresh_uri uri,name,NReference.reference_of_spec (refresh_uri uri2) spec
  86      ) ga in
  87    let im =
  88     NUri.UriMap.fold
  89      (fun u l im -> NUri.UriMap.add (refresh_uri u) (List.map refresh_uri l) im
  90      ) im NUri.UriMap.empty
  91    in
  92     global_aliases := ga;
  93     includes_map := im
  94   with
  95    Sys_error _ -> () in
  96  let get_deps u =
  97   let get_deps_one_step u =
  98     try NUri.UriMap.find u !includes_map with Not_found -> [] in
  99   let rec aux res =
 100    function
 101       [] -> res
 102     | he::tl ->
 103        if List.mem he res then
 104         aux res tl
 105        else
 106         aux (he::res) (get_deps_one_step he @ tl)
 107   in
 108    aux [] [u]
 109  in
 110   load_db,
 111   (fun ga -> global_aliases := ga; store_db ()),
 112   (fun () -> !global_aliases),
 113   (fun u l ->
 114     includes_map := NUri.UriMap.add u (l @ get_deps u) !includes_map;
 115     store_db ()),
 116   get_deps
 117 ;;
 118
 119 let init = load_db;;
 120
 121 class status =
 122  object
 123   val timestamp = (time0 : timestamp)
 124   method timestamp = timestamp
 125   method set_timestamp v = {< timestamp = v >}
 126   method set_library_status
 127    : 'status. < timestamp : timestamp; .. > as 'status -> 'self
 128    = fun o -> {< timestamp = o#timestamp >}
 129  end
 130
 131 let time_travel status =
 132  let sto,ali,cac,inc = status#timestamp in
 133   storage := sto; local_aliases := ali; cache := cac; includes := inc
 134 ;;
 135
 136 let serialize ~baseuri dump =
 137  let ch = open_out (path_of_baseuri baseuri) in
 138  Marshal.to_channel ch (magic,dump) [];
 139  close_out ch;
 140  List.iter
 141   (fun (uri,obj) ->
 142     let ch = open_out (path_of_baseuri uri) in
 143     Marshal.to_channel ch (magic,obj) [];
 144     close_out ch
 145   ) !storage;
 146  set_global_aliases (!local_aliases @ get_global_aliases ());
 147  List.iter (fun u -> add_deps u [baseuri]) !includes;
 148  time_travel (new status)
 149 ;;
 150
 151 module type Serializer =
 152  sig
 153   type status
 154   type obj
 155   val register:
 156    string ->
 157     ('a -> refresh_uri_in_term:(NCic.term -> NCic.term) -> status -> status) ->
 158     ('a -> obj)
 159   val serialize: baseuri:NUri.uri -> obj list -> unit
 160   val require: baseuri:NUri.uri -> status -> status
 161  end
 162
 163 module Serializer(S: sig type status end) =
 164  struct
 165   type status = S.status
 166   type obj = string * Obj.t
 167
 168   let require1 = ref (fun _ -> assert false (* unknown data*))
 169   let already_registered = ref []
 170
 171   let register tag require =
 172    assert (not (List.mem tag !already_registered));
 173    already_registered := tag :: !already_registered;
 174    require1 :=
 175     (fun (tag',data) as x ->
 176      if tag=tag' then
 177       require (Obj.magic data) ~refresh_uri_in_term
 178      else
 179       !require1 x);
 180    (fun x -> tag,Obj.repr x)
 181
 182   let serialize = serialize
 183
 184   let require ~baseuri status =
 185    includes := baseuri::!includes;
 186    let dump = require0 ~baseuri in
 187     List.fold_right !require1 dump status
 188 end
 189
 190 let decompile ~baseuri =
 191  let baseuris = get_deps baseuri in
 192  List.iter (fun baseuri ->
 193   HExtlib.safe_remove (path_of_baseuri baseuri);
 194   let basepath = path_of_baseuri ~no_suffix:true baseuri in
 195   try
 196    let od = Unix.opendir basepath in
 197    let rec aux names =
 198     try
 199      let name = Unix.readdir od in
 200       if name <> "." && name <> ".." then aux (name::names) else aux names
 201     with
 202      End_of_file -> names in
 203    let names = List.map (fun name -> basepath ^ "/" ^ name) (aux []) in
 204     Unix.closedir od;
 205     List.iter Unix.unlink names;
 206     HExtlib.rmdir_descend basepath;
 207     set_global_aliases
 208      (List.filter
 209       (fun (_,_,NReference.Ref (nuri,_)) ->
 210         Filename.dirname (NUri.string_of_uri nuri) <> NUri.string_of_uri baseuri
 211       ) (get_global_aliases ()))
 212   with
 213    Unix.Unix_error _ -> (* raised by Unix.opendir, we hope :-) *)
 214     assert (List.length baseuris = 1)
 215  ) baseuris
 216 ;;
 217
 218 LibraryClean.set_decompile_cb
 219  (fun ~baseuri -> decompile ~baseuri:(NUri.uri_of_string baseuri));;
 220
 221 let fetch_obj uri =
 222  let obj = require0 ~baseuri:uri in
 223   refresh_uri_in_obj obj
 224 ;;
 225
 226 let resolve name =
 227  try
 228   HExtlib.filter_map
 229    (fun (_,name',nref) -> if name'=name then Some nref else None)
 230    (!local_aliases @ get_global_aliases ())
 231  with
 232   Not_found -> raise (NCicEnvironment.ObjectNotFound (lazy name))
 233 ;;
 234
 235 let aliases_of uri =
 236  try
 237   HExtlib.filter_map
 238    (fun (uri',_,nref) ->
 239      if NUri.eq uri' uri then Some nref else None) !local_aliases
 240  with
 241   Not_found -> raise (NCicEnvironment.ObjectNotFound (lazy (NUri.string_of_uri uri)))
 242 ;;
 243
 244 let add_obj status u obj =
 245  storage := (u,obj)::!storage;
 246   let _,height,_,_,obj = obj in
 247   let references =
 248    match obj with
 249       NCic.Constant (_,name,None,_,_) ->
 250        [u,name,NReference.reference_of_spec u NReference.Decl]
 251     | NCic.Constant (_,name,Some _,_,_) ->
 252        [u,name,NReference.reference_of_spec u (NReference.Def height)]
 253     | NCic.Fixpoint (is_ind,fl,_) ->
 254        HExtlib.list_mapi
 255         (fun (_,name,recno,_,_) i ->
 256           if is_ind then
 257            u,name,NReference.reference_of_spec u(NReference.Fix(i,recno,height))
 258           else
 259            u,name,NReference.reference_of_spec u (NReference.CoFix i)) fl
 260     | NCic.Inductive (inductive,leftno,il,_) ->
 261        List.flatten
 262         (HExtlib.list_mapi
 263          (fun (_,iname,_,cl) i ->
 264            HExtlib.list_mapi
 265             (fun (_,cname,_) j->
 266               u,cname,
 267                NReference.reference_of_spec u (NReference.Con (i,j+1,leftno))
 268             ) cl @
 269            [u,iname,
 270              NReference.reference_of_spec u
 271               (NReference.Ind (inductive,i,leftno))]
 272          ) il)
 273   in
 274   local_aliases := references @ !local_aliases;
 275   status#set_timestamp (!storage,!local_aliases,!cache,!includes)
 276 ;;
 277
 278 let get_obj u =
 279  try List.assq u !storage
 280  with Not_found ->
 281   try fetch_obj u
 282   with Sys_error _ ->
 283    try NUri.UriMap.find u !cache
 284    with Not_found ->
 285     let ouri = NCic2OCic.ouri_of_nuri u in
 286     try
 287       let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph ouri in
 288       let l = OCic2NCic.convert_obj ouri o in
 289       List.iter (fun (u,_,_,_,_ as o) -> cache:= NUri.UriMap.add u o !cache) l;
 290       HExtlib.list_last l
 291     with CicEnvironment.Object_not_found u ->
 292       raise (NCicEnvironment.ObjectNotFound
 293                (lazy (NUri.string_of_uri (OCic2NCic.nuri_of_ouri u))))
 294 ;;
 295
 296 let clear_cache () = cache := NUri.UriMap.empty;;
 297
 298 NCicEnvironment.set_get_obj get_obj;;
 299 NCicPp.set_get_obj get_obj;;