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