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                prerr_endline "\nCircularDependency!\nfrozen list: \n";
 221                List.iter (
 222                  fun (u,(_,o)) ->
 223                    let su = UriManager.string_of_uri u in
 224                    let univ = if o = None then "NO_UNIV" else "" in
 225                    print_endline (su^" "^univ))
 226                  !frozen_list;
 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                let ugraph_real, univlist_real =
 237                  match ugraph_and_univlist with
 238                      (* FIXME: not sure it is OK*)
 239                      None -> CicUniv.empty_ugraph, []
 240                    | Some ((g,l) as g_and_l) -> g_and_l
 241                in
 242                unchecked_list :=
 243                  (uri,(obj,ugraph_and_univlist))::!unchecked_list ;
 244                obj, ugraph_real, univlist_real
 245     ;;
 246
 247     let unchecked_to_frozen uri =
 248       try
 249         let obj,ugraph_and_univlist = List.assq uri !unchecked_list in
 250         unchecked_list := List.remove_assq uri !unchecked_list ;
 251         frozen_list := (uri,(obj,ugraph_and_univlist))::!frozen_list
 252       with
 253         Not_found -> raise (CouldNotFreeze (UriManager.string_of_uri uri))
 254     ;;
 255
 256
 257    (************************************************************
 258      TASSI: invariant
 259      only object with a valid universe graph can be committed
 260
 261      this should disappear if the universe generation phase and the
 262      library exportation are unified.
 263    *************************************************************)
 264    let frozen_to_cooked ~uri =
 265     try
 266       let obj,ugraph_and_univlist = List.assq uri !frozen_list in
 267         match ugraph_and_univlist with
 268         | None -> assert false (* only NON dummy universes can be committed *)
 269         | Some (g,l) ->
 270            CicUniv.assert_univs_have_uri g l;
 271            frozen_list := List.remove_assq uri !frozen_list ;
 272            HT.add cacheOfCookedObjects uri (obj,g,l)
 273     with
 274         Not_found -> raise (CouldNotUnfreeze (UriManager.string_of_uri uri))
 275    ;;
 276
 277    let can_be_cooked uri =
 278      try
 279        let obj,ugraph_and_univlist = List.assq uri !frozen_list in
 280          (* FIXME: another thing to remove if univ generation phase and lib
 281           * exportation are unified.
 282           *)
 283          match ugraph_and_univlist with
 284              None -> false
 285            | Some _ -> true
 286      with
 287          Not_found -> false
 288    ;;
 289
 290    (* this function injects a real universe graph in a (uri, (obj, None))
 291     * element of the frozen list.
 292     *
 293     * FIXME: another thing to remove if univ generation phase and lib
 294     * exportation are unified.
 295     *)
 296    let hack_univ uri (real_ugraph, real_univlist)  =
 297      try
 298        let o,ugraph_and_univlist = List.assq uri !frozen_list in
 299          match ugraph_and_univlist with
 300              None ->
 301                frozen_list := List.remove_assoc uri !frozen_list;
 302                frozen_list :=
 303                  (uri,(o,Some (real_ugraph, real_univlist)))::!frozen_list;
 304            | Some g ->
 305                debug_print (lazy (
 306                  "You are probably hacking an object already hacked or an"^
 307                  " object that has the universe file but is not"^
 308                  " yet committed."));
 309                assert false
 310      with
 311          Not_found ->
 312            debug_print (lazy (
 313              "You are hacking an object that is not in the"^
 314              " frozen_list, this means you are probably generating an"^
 315              " universe file for an object that already"^
 316              " as an universe file"));
 317            assert false
 318    ;;
 319
 320    let find_cooked ~key:uri = HT.find cacheOfCookedObjects uri ;;
 321
 322    let add_cooked ~key:uri (obj,ugraph,univlist) =
 323      HT.add cacheOfCookedObjects uri (obj,ugraph,univlist)
 324    ;;
 325
 326    (* invariant
 327     *
 328     * an object can be romeved from the cache only if we are not typechecking
 329     * something. this means check and frozen must be empty.
 330     *)
 331    let remove uri =
 332      if !frozen_list <> [] then
 333        failwith "CicEnvironment.remove while type checking"
 334      else
 335       begin
 336        HT.remove cacheOfCookedObjects uri;
 337        unchecked_list :=
 338         List.filter (fun (uri',_) -> not (UriManager.eq uri uri')) !unchecked_list
 339       end
 340    ;;
 341
 342    let  list_all_cooked_uris () =
 343      HT.fold (fun u _ l -> u::l) cacheOfCookedObjects []
 344    ;;
 345
 346   end
 347 ;;
 348
 349 (* ************************************************************************
 350                         HERE ENDS THE CACHE MODULE
 351  * ************************************************************************ *)
 352
 353 (* exported cache functions *)
 354 let dump_to_channel = Cache.dump_to_channel;;
 355 let restore_from_channel = Cache.restore_from_channel;;
 356 let empty = Cache.empty;;
 357
 358 let total_parsing_time = ref 0.0
 359
 360 let get_object_to_add uri =
 361  try
 362   let filename = Http_getter.getxml' uri in
 363   let bodyfilename =
 364     match UriManager.bodyuri_of_uri uri with
 365        None -> None
 366     |  Some bodyuri ->
 367         if Http_getter.exists' bodyuri then
 368           Some (Http_getter.getxml' bodyuri)
 369         else
 370           None
 371   in
 372   let obj =
 373     try
 374       let time = Unix.gettimeofday() in
 375       let rc = CicParser.obj_of_xml uri filename bodyfilename in
 376       total_parsing_time :=
 377         !total_parsing_time +. ((Unix.gettimeofday()) -. time );
 378       rc
 379     with exn ->
 380       (match exn with
 381       | CicParser.Getter_failure ("key_not_found", uri) ->
 382           raise (Object_not_found (UriManager.uri_of_string uri))
 383       | _ -> raise exn)
 384   in
 385   let ugraph_and_univlist,filename_univ =
 386     try
 387       let filename_univ =
 388         let univ_uri = UriManager.univgraphuri_of_uri uri in
 389         Http_getter.getxml' univ_uri
 390       in
 391         Some (CicUniv.ugraph_and_univlist_of_xml filename_univ),
 392         Some filename_univ
 393     with
 394     | Http_getter_types.Key_not_found _
 395     | Http_getter_types.Unresolvable_URI _ ->
 396       debug_print (lazy (
 397         "WE HAVE NO UNIVERSE FILE FOR " ^ (UriManager.string_of_uri uri)));
 398       (* WE SHOULD FAIL (or return None, None *)
 399       Some (CicUniv.empty_ugraph, []), None
 400   in
 401   obj, ugraph_and_univlist
 402  with Http_getter_types.Key_not_found _ -> raise (Object_not_found uri)
 403 ;;
 404
 405 (* this is the function to fetch the object in the unchecked list and
 406  * nothing more (except returning it)
 407  *)
 408 let find_or_add_to_unchecked uri =
 409  Cache.find_or_add_to_unchecked uri ~get_object_to_add
 410
 411 (* set_type_checking_info uri                                   *)
 412 (* must be called once the type-checking of uri is finished     *)
 413 (* The object whose uri is uri is unfreezed                     *)
 414 (*                                                              *)
 415 (* the replacement ugraph must be the one returned by the       *)
 416 (* typechecker, restricted with the CicUnivUtils.clean_and_fill *)
 417 let set_type_checking_info ?(replace_ugraph_and_univlist=None) uri =
 418 (*
 419   if not (Cache.can_be_cooked uri) && replace_ugraph <> None then begin
 420     debug_print (lazy (
 421       "?replace_ugraph must be None if you are not committing an "^
 422       "object that has a universe graph associated "^
 423       "(can happen only in the fase of universes graphs generation)."));
 424     assert false
 425   else
 426 *)
 427   match Cache.can_be_cooked uri, replace_ugraph_and_univlist with
 428   | true, Some _
 429   | false, None ->
 430       debug_print (lazy (
 431         "?replace_ugraph must be (Some ugraph) when committing an object that "^
 432         "has no associated universe graph. If this is in make_univ phase you "^
 433         "should drop this exception and let univ_make commit thi object with "^
 434         "proper arguments"));
 435       assert false
 436   | _ ->
 437       (match replace_ugraph_and_univlist with
 438       | None -> ()
 439       | Some g_and_l -> Cache.hack_univ uri g_and_l);
 440       Cache.frozen_to_cooked uri
 441 ;;
 442
 443 (* fetch, unfreeze and commit an uri to the cacheOfCookedObjects and
 444  * return the object,ugraph
 445  *)
 446 let add_trusted_uri_to_cache uri =
 447   let _ = find_or_add_to_unchecked uri in
 448   Cache.unchecked_to_frozen uri;
 449   set_type_checking_info uri;
 450   try
 451     Cache.find_cooked uri
 452   with Not_found -> assert false
 453 ;;
 454
 455 (* get the uri, if we trust it will be added to the cacheOfCookedObjects *)
 456 let get_cooked_obj_with_univlist ?(trust=true) base_ugraph uri =
 457   try
 458     (* the object should be in the cacheOfCookedObjects *)
 459     let o,u,l = Cache.find_cooked uri in
 460       o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri)),l
 461   with Not_found ->
 462     (* this should be an error case, but if we trust the uri... *)
 463     if trust && trust_obj uri then
 464       (* trusting means that we will fetch cook it on the fly *)
 465       let o,u,l = add_trusted_uri_to_cache uri in
 466         o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri)),l
 467     else
 468       (* we don't trust the uri, so we fail *)
 469       begin
 470         debug_print (lazy ("CACHE MISS: " ^ (UriManager.string_of_uri uri)));
 471         raise Not_found
 472       end
 473
 474 let get_cooked_obj ?trust base_ugraph uri =
 475   let o,g,_ = get_cooked_obj_with_univlist ?trust base_ugraph uri in
 476   o,g
 477
 478 (* This has not the old semantic :( but is what the name suggests
 479  *
 480  *   let is_type_checked ?(trust=true) uri =
 481  *     try
 482  *       let _ = Cache.find_cooked uri in
 483  *         true
 484  *     with
 485  *       Not_found ->
 486  *         trust && trust_obj uri
 487  *   ;;
 488  *
 489  * as the get_cooked_obj but returns a type_checked_obj
 490  *
 491  *)
 492 let is_type_checked ?(trust=true) base_ugraph uri =
 493   try
 494     let o,u,_ = Cache.find_cooked uri in
 495       CheckedObj (o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri)))
 496   with Not_found ->
 497     (* this should return UncheckedObj *)
 498     if trust && trust_obj uri then
 499       (* trusting means that we will fetch cook it on the fly *)
 500       let o,u,_ = add_trusted_uri_to_cache uri in
 501         CheckedObj ( o, CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri))
 502     else
 503       let o,u,_ = find_or_add_to_unchecked uri in
 504       Cache.unchecked_to_frozen uri;
 505         UncheckedObj o
 506 ;;
 507
 508 (* as the get cooked, but if not present the object is only fetched,
 509  * not unfreezed and committed
 510  *)
 511 let get_obj base_ugraph uri =
 512   try
 513     (* the object should be in the cacheOfCookedObjects *)
 514     let o,u,_ = Cache.find_cooked uri in
 515       o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri))
 516   with Not_found ->
 517     (* this should be an error case, but if we trust the uri... *)
 518       let o,u,_ = find_or_add_to_unchecked uri in
 519         o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri))
 520 ;;
 521
 522 let in_cache uri =
 523   Cache.is_in_cooked uri || Cache.is_in_frozen uri || Cache.is_in_unchecked uri
 524
 525 let add_type_checked_obj uri (obj,ugraph,univlist) =
 526  Cache.add_cooked ~key:uri (obj,ugraph,univlist)
 527
 528 let in_library uri = in_cache uri || Http_getter.exists' uri
 529
 530 let remove_obj = Cache.remove
 531
 532 let list_uri () =
 533   Cache.list_all_cooked_uris ()
 534 ;;
 535
 536 let list_obj () =
 537   try
 538     List.map (fun u ->
 539       let o,ug = get_obj CicUniv.empty_ugraph u in
 540         (u,o,ug))
 541     (list_uri ())
 542   with
 543     Not_found ->
 544       debug_print (lazy "Who has removed the uri in the meanwhile?");
 545       raise Not_found
 546 ;;