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