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