helm/software/components/cic_proof_checking/cicEnvironment.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (*****************************************************************************)
  27 (*                                                                           *)
  28 (*                              PROJECT HELM                                 *)
  29 (*                                                                           *)
  30 (*               Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
  31 (*                                24/01/2000                                 *)
  32 (*                                                                           *)
  33 (* This module implements a trival cache system (an hash-table) for cic      *)
  34 (* objects. Uses the getter (getter.ml) and the parser (cicParser.ml)        *)
  35 (*                                                                           *)
  36 (*****************************************************************************)
  37
  38 (* $Id$ *)
  39
  40 (* ************************************************************************** *
  41                  CicEnvironment SETTINGS (trust and clean_tmp)
  42  * ************************************************************************** *)
  43
  44 let debug = false;;
  45 let cleanup_tmp = true;;
  46 let trust = ref  (fun _ -> true);;
  47 let set_trust f = trust := f
  48 let trust_obj uri = !trust uri
  49 let debug_print = if debug then fun x -> prerr_endline (Lazy.force x) else ignore
  50
  51 (* ************************************************************************** *
  52                                    TYPES
  53  * ************************************************************************** *)
  54
  55 type type_checked_obj =
  56  | CheckedObj of (Cic.obj * CicUniv.universe_graph)
  57  | UncheckedObj of Cic.obj * (CicUniv.universe_graph * CicUniv.universe list) option
  58
  59 exception AlreadyCooked of string;;
  60 exception CircularDependency of string Lazy.t;;
  61 exception CouldNotFreeze of string;;
  62 exception CouldNotUnfreeze of string;;
  63 exception Object_not_found of UriManager.uri;;
  64
  65
  66 (* ************************************************************************** *
  67                          HERE STARTS THE CACHE MODULE
  68  * ************************************************************************** *)
  69
  70 (* I think this should be the right place to implement mecanisms and
  71  * invasriants
  72  *)
  73
  74 (* Cache that uses == instead of = for testing equality *)
  75 (* Invariant: an object is always in at most one of the *)
  76 (* following states: unchecked, frozen and cooked.      *)
  77 module Cache :
  78   sig
  79    val find_or_add_to_unchecked :
  80      UriManager.uri ->
  81      get_object_to_add:
  82        (UriManager.uri ->
  83          Cic.obj * (CicUniv.universe_graph * CicUniv.universe list) option) ->
  84      Cic.obj * (CicUniv.universe_graph * CicUniv.universe list) option
  85    val can_be_cooked:
  86      UriManager.uri -> bool
  87    val unchecked_to_frozen :
  88      UriManager.uri -> unit
  89    val frozen_to_cooked :
  90      uri:UriManager.uri ->
  91      Cic.obj -> CicUniv.universe_graph -> CicUniv.universe list -> unit
  92    val find_cooked :
  93      key:UriManager.uri ->
  94        Cic.obj * CicUniv.universe_graph * CicUniv.universe list
  95    val add_cooked :
  96      key:UriManager.uri ->
  97      (Cic.obj * CicUniv.universe_graph * CicUniv.universe list) -> unit
  98    val remove: UriManager.uri -> unit
  99    val dump_to_channel : ?callback:(string -> unit) -> out_channel -> unit
 100    val restore_from_channel : ?callback:(string -> unit) -> in_channel -> unit
 101    val empty : unit -> unit
 102    val is_in_frozen: UriManager.uri -> bool
 103    val is_in_unchecked: UriManager.uri -> bool
 104    val is_in_cooked: UriManager.uri -> bool
 105    val list_all_cooked_uris: unit -> UriManager.uri list
 106    val invalidate: unit -> unit
 107   end
 108 =
 109   struct
 110    (*************************************************************************
 111      TASSI: invariant
 112      The cacheOfCookedObjects will contain only objects with a valid universe
 113      graph. valid means that not None (used if there is no universe file
 114      in the universe generation phase).
 115    **************************************************************************)
 116
 117     (* DATA: the data structure that implements the CACHE *)
 118     module HashedType =
 119     struct
 120      type t = UriManager.uri
 121      let equal = UriManager.eq
 122      let hash = Hashtbl.hash
 123     end
 124     ;;
 125
 126     module HT = Hashtbl.Make(HashedType);;
 127
 128     let cacheOfCookedObjects = HT.create 1009;;
 129
 130     (* DATA: The parking lists
 131      * the lists elements are (uri * (obj * universe_graph option))
 132      * ( u, ( o, None )) means that the object has no universes file, this
 133      *  should happen only in the universe generation phase.
 134      *  FIXME: if the universe generation is integrated in the library
 135      *  exportation phase, the 'option' MUST be removed.
 136      * ( u, ( o, Some g)) means that the object has a universes file,
 137      *  the usual case.
 138      *)
 139
 140     (* frozen is used to detect circular dependency. *)
 141     let frozen_list = ref [];;
 142     (* unchecked is used to store objects just fetched, nothing more. *)
 143     let unchecked_list = ref [];;
 144
 145     let invalidate _ =
 146       let l = HT.fold (fun k (o,g,gl) acc -> (k,(o,Some (g,gl)))::acc) cacheOfCookedObjects [] in
 147       unchecked_list :=
 148         HExtlib.list_uniq ~eq:(fun (x,_) (y,_) -> UriManager.eq x y)
 149         (List.sort (fun (x,_) (y,_) -> UriManager.compare x y) (l @ !unchecked_list));
 150       frozen_list := [];
 151       HT.clear cacheOfCookedObjects;
 152     ;;
 153
 154     let empty () =
 155       HT.clear cacheOfCookedObjects;
 156       unchecked_list := [] ;
 157       frozen_list := []
 158     ;;
 159
 160     (* FIX: universe stuff?? *)
 161     let dump_to_channel ?(callback = ignore) oc =
 162      HT.iter (fun uri _ -> callback (UriManager.string_of_uri uri))
 163        cacheOfCookedObjects;
 164      Marshal.to_channel oc cacheOfCookedObjects []
 165     ;;
 166
 167     (* FIX: universes stuff?? *)
 168     let restore_from_channel ?(callback = ignore) ic =
 169       let restored = Marshal.from_channel ic in
 170       (* FIXME: should this empty clean the frozen and unchecked?
 171        * if not, the only-one-empty-end-not-3 patch is wrong
 172        *)
 173       empty ();
 174       HT.iter
 175        (fun k (v,u,l) ->
 176          callback (UriManager.string_of_uri k);
 177          let reconsed_entry =
 178            CicUtil.rehash_obj v,
 179            CicUniv.recons_graph u,
 180            List.map CicUniv.recons_univ l
 181          in
 182          HT.add cacheOfCookedObjects
 183            (UriManager.uri_of_string (UriManager.string_of_uri k))
 184            reconsed_entry)
 185        restored
 186     ;;
 187
 188
 189     let is_in_frozen uri =
 190       List.mem_assoc uri !frozen_list
 191     ;;
 192
 193     let is_in_unchecked uri =
 194       List.mem_assoc uri !unchecked_list
 195     ;;
 196
 197     let is_in_cooked uri =
 198       HT.mem cacheOfCookedObjects uri
 199     ;;
 200
 201
 202     (*******************************************************************
 203       TASSI: invariant
 204       we need, in the universe generation phase, to traverse objects
 205       that are not yet committed, so we search them in the frozen list.
 206       Only uncommitted objects without a universe file (see the assertion)
 207       can be searched with method
 208     *******************************************************************)
 209
 210     let find_or_add_to_unchecked uri ~get_object_to_add =
 211      try
 212        List.assq uri !unchecked_list
 213      with
 214          Not_found ->
 215            if List.mem_assq uri !frozen_list then
 216              (* CIRCULAR DEPENDENCY DETECTED, print the error and raise *)
 217              begin
 218 (*
 219                prerr_endline "\nCircularDependency!\nfrozen list: \n";
 220                List.iter (
 221                  fun (u,(_,o)) ->
 222                    let su = UriManager.string_of_uri u in
 223                    let univ = if o = None then "NO_UNIV" else "" in
 224                    prerr_endline (su^" "^univ))
 225                  !frozen_list;
 226 *)
 227                raise (CircularDependency (lazy (UriManager.string_of_uri uri)))
 228              end
 229            else
 230              if HT.mem cacheOfCookedObjects uri then
 231                (* DOUBLE COOK DETECTED, raise the exception *)
 232                raise (AlreadyCooked (UriManager.string_of_uri uri))
 233              else
 234                (* OK, it is not already frozen nor cooked *)
 235                let obj,ugraph_and_univlist = get_object_to_add uri in
 236                unchecked_list := (uri,(obj,ugraph_and_univlist))::!unchecked_list;
 237                obj, ugraph_and_univlist
 238     ;;
 239
 240     let unchecked_to_frozen uri =
 241       try
 242         let obj,ugraph_and_univlist = List.assq uri !unchecked_list in
 243         unchecked_list := List.remove_assq uri !unchecked_list ;
 244         frozen_list := (uri,(obj,ugraph_and_univlist))::!frozen_list
 245       with
 246         Not_found -> raise (CouldNotFreeze (UriManager.string_of_uri uri))
 247     ;;
 248
 249    let frozen_to_cooked ~uri o ug ul =
 250      CicUniv.assert_univs_have_uri ug ul;
 251      frozen_list := List.remove_assq uri !frozen_list ;
 252      HT.add cacheOfCookedObjects uri (o,ug,ul)
 253    ;;
 254
 255    let can_be_cooked uri = List.mem_assq uri !frozen_list;;
 256
 257    let find_cooked ~key:uri = HT.find cacheOfCookedObjects uri ;;
 258
 259    let add_cooked ~key:uri (obj,ugraph,univlist) =
 260      HT.add cacheOfCookedObjects uri (obj,ugraph,univlist)
 261    ;;
 262
 263    (* invariant
 264     *
 265     * an object can be romeved from the cache only if we are not typechecking
 266     * something. this means check and frozen must be empty.
 267     *)
 268    let remove uri =
 269      if !frozen_list <> [] then
 270        failwith "CicEnvironment.remove while type checking"
 271      else
 272       begin
 273        HT.remove cacheOfCookedObjects uri;
 274        unchecked_list :=
 275         List.filter (fun (uri',_) -> not (UriManager.eq uri uri')) !unchecked_list
 276       end
 277    ;;
 278
 279    let  list_all_cooked_uris () =
 280      HT.fold (fun u _ l -> u::l) cacheOfCookedObjects []
 281    ;;
 282
 283   end
 284 ;;
 285
 286 (* ************************************************************************
 287                         HERE ENDS THE CACHE MODULE
 288  * ************************************************************************ *)
 289
 290 (* exported cache functions *)
 291 let dump_to_channel = Cache.dump_to_channel;;
 292 let restore_from_channel = Cache.restore_from_channel;;
 293 let empty = Cache.empty;;
 294
 295 let total_parsing_time = ref 0.0
 296
 297 let get_object_to_add uri =
 298  try
 299   let filename = Http_getter.getxml' uri in
 300   let bodyfilename =
 301     match UriManager.bodyuri_of_uri uri with
 302        None -> None
 303     |  Some bodyuri ->
 304         if Http_getter.exists' ~local:false bodyuri then
 305           Some (Http_getter.getxml' bodyuri)
 306         else
 307           None
 308   in
 309   let obj =
 310     try
 311       let time = Unix.gettimeofday() in
 312       let rc = CicParser.obj_of_xml uri filename bodyfilename in
 313       total_parsing_time :=
 314         !total_parsing_time +. ((Unix.gettimeofday()) -. time );
 315       rc
 316     with exn ->
 317       (match exn with
 318       | CicParser.Getter_failure ("key_not_found", uri) ->
 319           raise (Object_not_found (UriManager.uri_of_string uri))
 320       | _ -> raise exn)
 321   in
 322   let ugraph_and_univlist,filename_univ =
 323     try
 324       let filename_univ =
 325         let univ_uri = UriManager.univgraphuri_of_uri uri in
 326         Http_getter.getxml' univ_uri
 327       in
 328         Some (CicUniv.ugraph_and_univlist_of_xml filename_univ),
 329         Some filename_univ
 330     with
 331     | Http_getter_types.Key_not_found _
 332     | Http_getter_types.Unresolvable_URI _ ->
 333       debug_print (lazy (
 334         "WE HAVE NO UNIVERSE FILE FOR " ^ (UriManager.string_of_uri uri)));
 335       None, None
 336   in
 337   obj, ugraph_and_univlist
 338  with Http_getter_types.Key_not_found _ -> raise (Object_not_found uri)
 339 ;;
 340
 341 (* this is the function to fetch the object in the unchecked list and
 342  * nothing more (except returning it)
 343  *)
 344 let find_or_add_to_unchecked uri =
 345  Cache.find_or_add_to_unchecked uri ~get_object_to_add
 346
 347 (* set_type_checking_info uri                                   *)
 348 (* must be called once the type-checking of uri is finished     *)
 349 (* The object whose uri is uri is unfreezed                     *)
 350 (*                                                              *)
 351 (* the replacement ugraph must be the one returned by the       *)
 352 (* typechecker, restricted with the CicUnivUtils.clean_and_fill *)
 353 let set_type_checking_info uri (o,ug,ul) =
 354   if not (Cache.can_be_cooked uri) then assert false
 355   else
 356     Cache.frozen_to_cooked ~uri o ug ul
 357 ;;
 358
 359 (* fetch, unfreeze and commit an uri to the cacheOfCookedObjects and
 360  * return the object,ugraph
 361  *)
 362 let add_trusted_uri_to_cache uri =
 363   let o,u_and_ul = find_or_add_to_unchecked uri in
 364   Cache.unchecked_to_frozen uri;
 365   let u,ul =
 366     match u_and_ul with
 367     (* for backward compat with Coq *)
 368     | None -> CicUniv.empty_ugraph, []
 369     | Some (ug,ul) -> ug, ul
 370   in
 371   set_type_checking_info uri (o,u,ul);
 372   try Cache.find_cooked uri
 373   with Not_found -> assert false
 374 ;;
 375
 376 (* get the uri, if we trust it will be added to the cacheOfCookedObjects *)
 377 let get_cooked_obj_with_univlist ?(trust=true) base_ugraph uri =
 378   try
 379     (* the object should be in the cacheOfCookedObjects *)
 380     let o,u,l = Cache.find_cooked uri in
 381       o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*))),l
 382   with Not_found ->
 383     (* this should be an error case, but if we trust the uri... *)
 384     if trust && trust_obj uri then
 385       (* trusting means that we will fetch cook it on the fly *)
 386       let o,u,l = add_trusted_uri_to_cache uri in
 387         o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*))),l
 388     else
 389       (* we don't trust the uri, so we fail *)
 390       begin
 391         debug_print (lazy ("CACHE MISS: " ^ (UriManager.string_of_uri uri)));
 392         raise Not_found
 393       end
 394
 395 let get_cooked_obj ?trust base_ugraph uri =
 396   let o,g,_ = get_cooked_obj_with_univlist ?trust base_ugraph uri in
 397   o,g
 398
 399 let is_type_checked ?(trust=true) base_ugraph uri =
 400   try
 401     let o,u,l = Cache.find_cooked uri in
 402       CheckedObj (o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*))))
 403   with Not_found ->
 404     (* this should return UncheckedObj *)
 405     if trust && trust_obj uri then
 406       (* trusting means that we will fetch cook it on the fly *)
 407       let o,u,l = add_trusted_uri_to_cache uri in
 408         CheckedObj ( o, CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*)))
 409     else
 410       let o,u_and_ul = find_or_add_to_unchecked uri in
 411       Cache.unchecked_to_frozen uri;
 412       UncheckedObj (o,u_and_ul)
 413 ;;
 414
 415 (* as the get cooked, but if not present the object is only fetched,
 416  * not unfreezed and committed
 417  *)
 418 let get_obj base_ugraph uri =
 419   try
 420     (* the object should be in the cacheOfCookedObjects *)
 421     let o,u,_ = Cache.find_cooked uri in
 422     o,CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri)
 423   with Not_found ->
 424     (* this should be an error case, but if we trust the uri... *)
 425       let o,u_and_l = find_or_add_to_unchecked uri in
 426       match u_and_l with
 427       | None -> o, base_ugraph
 428       | Some (ug,_) -> o,CicUniv.merge_ugraphs ~base_ugraph ~increment:(ug,uri)
 429 ;;
 430
 431 let in_cache uri =
 432   Cache.is_in_cooked uri || Cache.is_in_frozen uri || Cache.is_in_unchecked uri
 433
 434 let add_type_checked_obj uri (obj,ugraph,univlist) =
 435  Cache.add_cooked ~key:uri (obj,ugraph,univlist)
 436
 437 let in_library uri = in_cache uri || Http_getter.exists' ~local:false uri
 438
 439 let remove_obj = Cache.remove
 440
 441 let list_uri () =
 442   Cache.list_all_cooked_uris ()
 443 ;;
 444
 445 let list_obj () =
 446   try
 447     List.map (fun u ->
 448       let o,ug = get_obj CicUniv.empty_ugraph u in
 449         (u,o,ug))
 450     (list_uri ())
 451   with
 452     Not_found ->
 453       debug_print (lazy "Who has removed the uri in the meanwhile?");
 454       raise Not_found
 455 ;;
 456
 457 let invalidate _ =
 458    Cache.invalidate ()
 459 ;;