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)    (* cooked obj *)
  57  | UncheckedObj of Cic.obj   (* uncooked obj to proof-check *)
  58 ;;
  59
  60 exception AlreadyCooked of string;;
  61 exception CircularDependency of string Lazy.t;;
  62 exception CouldNotFreeze of string;;
  63 exception CouldNotUnfreeze of string;;
  64 exception Object_not_found of UriManager.uri;;
  65
  66
  67 (* ************************************************************************** *
  68                          HERE STARTS THE CACHE MODULE
  69  * ************************************************************************** *)
  70
  71 (* I think this should be the right place to implement mecanisms and
  72  * invasriants
  73  *)
  74
  75 (* Cache that uses == instead of = for testing equality *)
  76 (* Invariant: an object is always in at most one of the *)
  77 (* following states: unchecked, frozen and cooked.      *)
  78 module Cache :
  79   sig
  80    val find_or_add_to_unchecked :
  81      UriManager.uri ->
  82      get_object_to_add:
  83        (UriManager.uri ->
  84          Cic.obj * (CicUniv.universe_graph * CicUniv.universe list) option) ->
  85      Cic.obj * CicUniv.universe_graph * CicUniv.universe list
  86    val can_be_cooked:
  87      UriManager.uri -> bool
  88    val unchecked_to_frozen :
  89      UriManager.uri -> unit
  90    val frozen_to_cooked :
  91      uri:UriManager.uri -> unit
  92    val hack_univ:
  93      UriManager.uri -> CicUniv.universe_graph * CicUniv.universe list -> unit
  94    val find_cooked :
  95      key:UriManager.uri ->
  96        Cic.obj * CicUniv.universe_graph * CicUniv.universe list
  97    val add_cooked :
  98      key:UriManager.uri ->
  99      (Cic.obj * CicUniv.universe_graph * CicUniv.universe list) -> unit
 100    val remove: UriManager.uri -> unit
 101    val dump_to_channel : ?callback:(string -> unit) -> out_channel -> unit
 102    val restore_from_channel : ?callback:(string -> unit) -> in_channel -> unit
 103    val empty : unit -> unit
 104    val is_in_frozen: UriManager.uri -> bool
 105    val is_in_unchecked: UriManager.uri -> bool
 106    val is_in_cooked: UriManager.uri -> bool
 107    val list_all_cooked_uris: unit -> UriManager.uri list
 108   end
 109 =
 110   struct
 111    (*************************************************************************
 112      TASSI: invariant
 113      The cacheOfCookedObjects will contain only objects with a valid universe
 114      graph. valid means that not None (used if there is no universe file
 115      in the universe generation phase).
 116    **************************************************************************)
 117
 118     (* DATA: the data structure that implements the CACHE *)
 119     module HashedType =
 120     struct
 121      type t = UriManager.uri
 122      let equal = UriManager.eq
 123      let hash = Hashtbl.hash
 124     end
 125     ;;
 126
 127     module HT = Hashtbl.Make(HashedType);;
 128
 129     let cacheOfCookedObjects = HT.create 1009;;
 130
 131     (* DATA: The parking lists
 132      * the lists elements are (uri * (obj * universe_graph option))
 133      * ( u, ( o, None )) means that the object has no universes file, this
 134      *  should happen only in the universe generation phase.
 135      *  FIXME: if the universe generation is integrated in the library
 136      *  exportation phase, the 'option' MUST be removed.
 137      * ( u, ( o, Some g)) means that the object has a universes file,
 138      *  the usual case.
 139      *)
 140
 141     (* frozen is used to detect circular dependency. *)
 142     let frozen_list = ref [];;
 143     (* unchecked is used to store objects just fetched, nothing more. *)
 144     let unchecked_list = ref [];;
 145
 146     let empty () =
 147       HT.clear cacheOfCookedObjects;
 148       unchecked_list := [] ;
 149       frozen_list := []
 150     ;;
 151
 152     (* FIX: universe stuff?? *)
 153     let dump_to_channel ?(callback = ignore) oc =
 154      HT.iter (fun uri _ -> callback (UriManager.string_of_uri uri))
 155        cacheOfCookedObjects;
 156      Marshal.to_channel oc cacheOfCookedObjects []
 157     ;;
 158
 159     (* FIX: universes stuff?? *)
 160     let restore_from_channel ?(callback = ignore) ic =
 161       let restored = Marshal.from_channel ic in
 162       (* FIXME: should this empty clean the frozen and unchecked?
 163        * if not, the only-one-empty-end-not-3 patch is wrong
 164        *)
 165       empty ();
 166       HT.iter
 167        (fun k (v,u,l) ->
 168          callback (UriManager.string_of_uri k);
 169          let reconsed_entry =
 170            CicUtil.rehash_obj v,
 171            CicUniv.recons_graph u,
 172            List.map CicUniv.recons_univ l
 173          in
 174          HT.add cacheOfCookedObjects
 175            (UriManager.uri_of_string (UriManager.string_of_uri k))
 176            reconsed_entry)
 177        restored
 178     ;;
 179
 180
 181     let is_in_frozen uri =
 182       List.mem_assoc uri !frozen_list
 183     ;;
 184
 185     let is_in_unchecked uri =
 186       List.mem_assoc uri !unchecked_list
 187     ;;
 188
 189     let is_in_cooked uri =
 190       HT.mem cacheOfCookedObjects uri
 191     ;;
 192
 193
 194     (*******************************************************************
 195       TASSI: invariant
 196       we need, in the universe generation phase, to traverse objects
 197       that are not yet committed, so we search them in the frozen list.
 198       Only uncommitted objects without a universe file (see the assertion)
 199       can be searched with method
 200     *******************************************************************)
 201
 202     let find_or_add_to_unchecked uri ~get_object_to_add =
 203      try
 204        let o,g_and_l = List.assq uri !unchecked_list in
 205          match g_and_l with
 206              (* FIXME: we accept both cases, as at the end of this function
 207                * maybe the None universe outside the cache module should be
 208                * avoided elsewhere.
 209                *
 210                * another thing that should be removed if univ generation phase
 211                * and lib exportation are unified.
 212                *)
 213            | None -> o,CicUniv.empty_ugraph,[]
 214            | Some (g,l) -> o,g,l
 215      with
 216          Not_found ->
 217            if List.mem_assq uri !frozen_list then
 218              (* CIRCULAR DEPENDENCY DETECTED, print the error and raise *)
 219              begin
 220 (*
 221                prerr_endline "\nCircularDependency!\nfrozen list: \n";
 222                List.iter (
 223                  fun (u,(_,o)) ->
 224                    let su = UriManager.string_of_uri u in
 225                    let univ = if o = None then "NO_UNIV" else "" in
 226                    prerr_endline (su^" "^univ))
 227                  !frozen_list;
 228 *)
 229                raise (CircularDependency (lazy (UriManager.string_of_uri uri)))
 230              end
 231            else
 232              if HT.mem cacheOfCookedObjects uri then
 233                (* DOUBLE COOK DETECTED, raise the exception *)
 234                raise (AlreadyCooked (UriManager.string_of_uri uri))
 235              else
 236                (* OK, it is not already frozen nor cooked *)
 237                let obj,ugraph_and_univlist = get_object_to_add uri in
 238                let ugraph_real, univlist_real =
 239                  match ugraph_and_univlist with
 240                      (* FIXME: not sure it is OK*)
 241                      None -> CicUniv.empty_ugraph, []
 242                    | Some ((g,l) as g_and_l) -> g_and_l
 243                in
 244                unchecked_list :=
 245                  (uri,(obj,ugraph_and_univlist))::!unchecked_list ;
 246                obj, ugraph_real, univlist_real
 247     ;;
 248
 249     let unchecked_to_frozen uri =
 250       try
 251         let obj,ugraph_and_univlist = List.assq uri !unchecked_list in
 252         unchecked_list := List.remove_assq uri !unchecked_list ;
 253         frozen_list := (uri,(obj,ugraph_and_univlist))::!frozen_list
 254       with
 255         Not_found -> raise (CouldNotFreeze (UriManager.string_of_uri uri))
 256     ;;
 257
 258
 259    (************************************************************
 260      TASSI: invariant
 261      only object with a valid universe graph can be committed
 262
 263      this should disappear if the universe generation phase and the
 264      library exportation are unified.
 265    *************************************************************)
 266    let frozen_to_cooked ~uri =
 267     try
 268       let obj,ugraph_and_univlist = List.assq uri !frozen_list in
 269         match ugraph_and_univlist with
 270         | None -> assert false (* only NON dummy universes can be committed *)
 271         | Some (g,l) ->
 272            CicUniv.assert_univs_have_uri g l;
 273            frozen_list := List.remove_assq uri !frozen_list ;
 274            HT.add cacheOfCookedObjects uri (obj,g,l)
 275     with
 276         Not_found -> raise (CouldNotUnfreeze (UriManager.string_of_uri uri))
 277    ;;
 278
 279    let can_be_cooked uri =
 280      try
 281        let obj,ugraph_and_univlist = List.assq uri !frozen_list in
 282          (* FIXME: another thing to remove if univ generation phase and lib
 283           * exportation are unified.
 284           *)
 285          match ugraph_and_univlist with
 286              None -> false
 287            | Some _ -> true
 288      with
 289          Not_found -> false
 290    ;;
 291
 292    (* this function injects a real universe graph in a (uri, (obj, None))
 293     * element of the frozen list.
 294     *
 295     * FIXME: another thing to remove if univ generation phase and lib
 296     * exportation are unified.
 297     *)
 298    let hack_univ uri (real_ugraph, real_univlist)  =
 299      try
 300        let o,ugraph_and_univlist = List.assq uri !frozen_list in
 301          match ugraph_and_univlist with
 302              None ->
 303                frozen_list := List.remove_assoc uri !frozen_list;
 304                frozen_list :=
 305                  (uri,(o,Some (real_ugraph, real_univlist)))::!frozen_list;
 306            | Some g ->
 307                debug_print (lazy (
 308                  "You are probably hacking an object already hacked or an"^
 309                  " object that has the universe file but is not"^
 310                  " yet committed."));
 311                assert false
 312      with
 313          Not_found ->
 314            debug_print (lazy (
 315              "You are hacking an object that is not in the"^
 316              " frozen_list, this means you are probably generating an"^
 317              " universe file for an object that already"^
 318              " as an universe file"));
 319            assert false
 320    ;;
 321
 322    let find_cooked ~key:uri = HT.find cacheOfCookedObjects uri ;;
 323
 324    let add_cooked ~key:uri (obj,ugraph,univlist) =
 325      HT.add cacheOfCookedObjects uri (obj,ugraph,univlist)
 326    ;;
 327
 328    (* invariant
 329     *
 330     * an object can be romeved from the cache only if we are not typechecking
 331     * something. this means check and frozen must be empty.
 332     *)
 333    let remove uri =
 334      if !frozen_list <> [] then
 335        failwith "CicEnvironment.remove while type checking"
 336      else
 337       begin
 338        HT.remove cacheOfCookedObjects uri;
 339        unchecked_list :=
 340         List.filter (fun (uri',_) -> not (UriManager.eq uri uri')) !unchecked_list
 341       end
 342    ;;
 343
 344    let  list_all_cooked_uris () =
 345      HT.fold (fun u _ l -> u::l) cacheOfCookedObjects []
 346    ;;
 347
 348   end
 349 ;;
 350
 351 (* ************************************************************************
 352                         HERE ENDS THE CACHE MODULE
 353  * ************************************************************************ *)
 354
 355 (* exported cache functions *)
 356 let dump_to_channel = Cache.dump_to_channel;;
 357 let restore_from_channel = Cache.restore_from_channel;;
 358 let empty = Cache.empty;;
 359
 360 let total_parsing_time = ref 0.0
 361
 362 let get_object_to_add uri =
 363  try
 364   let filename = Http_getter.getxml' uri in
 365   let bodyfilename =
 366     match UriManager.bodyuri_of_uri uri with
 367        None -> None
 368     |  Some bodyuri ->
 369         if Http_getter.exists' ~local:false bodyuri then
 370           Some (Http_getter.getxml' bodyuri)
 371         else
 372           None
 373   in
 374   let obj =
 375     try
 376       let time = Unix.gettimeofday() in
 377       let rc = CicParser.obj_of_xml uri filename bodyfilename in
 378       total_parsing_time :=
 379         !total_parsing_time +. ((Unix.gettimeofday()) -. time );
 380       rc
 381     with exn ->
 382       (match exn with
 383       | CicParser.Getter_failure ("key_not_found", uri) ->
 384           raise (Object_not_found (UriManager.uri_of_string uri))
 385       | _ -> raise exn)
 386   in
 387   let ugraph_and_univlist,filename_univ =
 388     try
 389       let filename_univ =
 390         let univ_uri = UriManager.univgraphuri_of_uri uri in
 391         Http_getter.getxml' univ_uri
 392       in
 393         Some (CicUniv.ugraph_and_univlist_of_xml filename_univ),
 394         Some filename_univ
 395     with
 396     | Http_getter_types.Key_not_found _
 397     | Http_getter_types.Unresolvable_URI _ ->
 398       debug_print (lazy (
 399         "WE HAVE NO UNIVERSE FILE FOR " ^ (UriManager.string_of_uri uri)));
 400       (* WE SHOULD FAIL (or return None, None *)
 401       Some (CicUniv.empty_ugraph, []), None
 402   in
 403   obj, ugraph_and_univlist
 404  with Http_getter_types.Key_not_found _ -> raise (Object_not_found uri)
 405 ;;
 406
 407 (* this is the function to fetch the object in the unchecked list and
 408  * nothing more (except returning it)
 409  *)
 410 let find_or_add_to_unchecked uri =
 411  Cache.find_or_add_to_unchecked uri ~get_object_to_add
 412
 413 (* set_type_checking_info uri                                   *)
 414 (* must be called once the type-checking of uri is finished     *)
 415 (* The object whose uri is uri is unfreezed                     *)
 416 (*                                                              *)
 417 (* the replacement ugraph must be the one returned by the       *)
 418 (* typechecker, restricted with the CicUnivUtils.clean_and_fill *)
 419 let set_type_checking_info ?(replace_ugraph_and_univlist=None) uri =
 420 (*
 421   if not (Cache.can_be_cooked uri) && replace_ugraph <> None then begin
 422     debug_print (lazy (
 423       "?replace_ugraph must be None if you are not committing an "^
 424       "object that has a universe graph associated "^
 425       "(can happen only in the fase of universes graphs generation)."));
 426     assert false
 427   else
 428 *)
 429   match Cache.can_be_cooked uri, replace_ugraph_and_univlist with
 430   | true, Some _
 431   | false, None ->
 432       debug_print (lazy (
 433         "?replace_ugraph must be (Some ugraph) when committing an object that "^
 434         "has no associated universe graph. If this is in make_univ phase you "^
 435         "should drop this exception and let univ_make commit thi object with "^
 436         "proper arguments"));
 437       assert false
 438   | _ ->
 439       (match replace_ugraph_and_univlist with
 440       | None -> ()
 441       | Some g_and_l -> Cache.hack_univ uri g_and_l);
 442       Cache.frozen_to_cooked uri
 443 ;;
 444
 445 (* fetch, unfreeze and commit an uri to the cacheOfCookedObjects and
 446  * return the object,ugraph
 447  *)
 448 let add_trusted_uri_to_cache uri =
 449   let _ = find_or_add_to_unchecked uri in
 450   Cache.unchecked_to_frozen uri;
 451   set_type_checking_info uri;
 452   try
 453     Cache.find_cooked uri
 454   with Not_found -> assert false
 455 ;;
 456
 457 (* get the uri, if we trust it will be added to the cacheOfCookedObjects *)
 458 let get_cooked_obj_with_univlist ?(trust=true) base_ugraph uri =
 459   try
 460     (* the object should be in the cacheOfCookedObjects *)
 461     let o,u,l = Cache.find_cooked uri in
 462       o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*))),l
 463   with Not_found ->
 464     (* this should be an error case, but if we trust the uri... *)
 465     if trust && trust_obj uri then
 466       (* trusting means that we will fetch cook it on the fly *)
 467       let o,u,l = add_trusted_uri_to_cache uri in
 468         o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*))),l
 469     else
 470       (* we don't trust the uri, so we fail *)
 471       begin
 472         debug_print (lazy ("CACHE MISS: " ^ (UriManager.string_of_uri uri)));
 473         raise Not_found
 474       end
 475
 476 let get_cooked_obj ?trust base_ugraph uri =
 477   let o,g,_ = get_cooked_obj_with_univlist ?trust base_ugraph uri in
 478   o,g
 479
 480 (* This has not the old semantic :( but is what the name suggests
 481  *
 482  *   let is_type_checked ?(trust=true) uri =
 483  *     try
 484  *       let _ = Cache.find_cooked uri in
 485  *         true
 486  *     with
 487  *       Not_found ->
 488  *         trust && trust_obj uri
 489  *   ;;
 490  *
 491  * as the get_cooked_obj but returns a type_checked_obj
 492  *
 493  *)
 494 let is_type_checked ?(trust=true) base_ugraph uri =
 495   try
 496     let o,u,l = Cache.find_cooked uri in
 497       CheckedObj (o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*))))
 498   with Not_found ->
 499     (* this should return UncheckedObj *)
 500     if trust && trust_obj uri then
 501       (* trusting means that we will fetch cook it on the fly *)
 502       let o,u,l = add_trusted_uri_to_cache uri in
 503         CheckedObj ( o, CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*)))
 504     else
 505       let o,u,_ = find_or_add_to_unchecked uri in
 506       Cache.unchecked_to_frozen uri;
 507         UncheckedObj o
 508 ;;
 509
 510 (* as the get cooked, but if not present the object is only fetched,
 511  * not unfreezed and committed
 512  *)
 513 let get_obj base_ugraph uri =
 514   try
 515     (* the object should be in the cacheOfCookedObjects *)
 516     let o,u,l = Cache.find_cooked uri in
 517       o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*)))
 518   with Not_found ->
 519     (* this should be an error case, but if we trust the uri... *)
 520       let o,u,l = find_or_add_to_unchecked uri in
 521         o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*)))
 522 ;;
 523
 524 let in_cache uri =
 525   Cache.is_in_cooked uri || Cache.is_in_frozen uri || Cache.is_in_unchecked uri
 526
 527 let add_type_checked_obj uri (obj,ugraph,univlist) =
 528  Cache.add_cooked ~key:uri (obj,ugraph,univlist)
 529
 530 let in_library uri = in_cache uri || Http_getter.exists' ~local:false uri
 531
 532 let remove_obj = Cache.remove
 533
 534 let list_uri () =
 535   Cache.list_all_cooked_uris ()
 536 ;;
 537
 538 let list_obj () =
 539   try
 540     List.map (fun u ->
 541       let o,ug = get_obj CicUniv.empty_ugraph u in
 542         (u,o,ug))
 543     (list_uri ())
 544   with
 545     Not_found ->
 546       debug_print (lazy "Who has removed the uri in the meanwhile?");
 547       raise Not_found
 548 ;;