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