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     (* FIXED: should be ok even if not touched *)
 145       (* used to hash cons uris on restore to grant URI structure unicity *)
 146     let restore_uris =
 147       let module C = Cic in
 148       let recons uri =
 149         UriManager.uri_of_string (UriManager.string_of_uri uri)
 150       in
 151       let rec restore_in_term =
 152         function
 153          | (C.Rel _) as t -> t
 154          | C.Var (uri,exp_named_subst) ->
 155             let uri' = recons uri in
 156             let exp_named_subst' =
 157              List.map
 158               (function (uri,t) ->(recons uri,restore_in_term t))
 159                exp_named_subst
 160             in
 161              C.Var (uri',exp_named_subst')
 162          | C.Meta (i,l) ->
 163             let l' =
 164              List.map
 165               (function
 166                   None -> None
 167                 | Some t -> Some (restore_in_term t)
 168               ) l
 169             in
 170              C.Meta(i,l')
 171          | C.Sort (C.Type u) ->
 172              CicUniv.assert_univ u;
 173              C.Sort (C.Type (CicUniv.recons_univ u))
 174          | C.Sort _ as t -> t
 175          | C.Implicit _ as t -> t
 176          | C.Cast (te,ty) -> C.Cast (restore_in_term te, restore_in_term ty)
 177          | C.Prod (n,s,t) -> C.Prod (n, restore_in_term s, restore_in_term t)
 178          | C.Lambda (n,s,t) -> C.Lambda (n, restore_in_term s, restore_in_term t)
 179          | C.LetIn (n,s,t) -> C.LetIn (n, restore_in_term s, restore_in_term t)
 180          | C.Appl l -> C.Appl (List.map restore_in_term l)
 181          | C.Const (uri,exp_named_subst) ->
 182             let uri' = recons uri in
 183             let exp_named_subst' =
 184              List.map
 185               (function (uri,t) -> (recons uri,restore_in_term t)) exp_named_subst
 186             in
 187              C.Const (uri',exp_named_subst')
 188          | C.MutInd (uri,tyno,exp_named_subst) ->
 189             let uri' = recons uri in
 190             let exp_named_subst' =
 191              List.map
 192               (function (uri,t) -> (recons uri,restore_in_term t)) exp_named_subst
 193             in
 194              C.MutInd (uri',tyno,exp_named_subst')
 195          | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
 196             let uri' = recons uri in
 197             let exp_named_subst' =
 198              List.map
 199               (function (uri,t) -> (recons uri,restore_in_term t)) exp_named_subst
 200             in
 201              C.MutConstruct (uri',tyno,consno,exp_named_subst')
 202          | C.MutCase (uri,i,outty,t,pl) ->
 203             C.MutCase (recons uri, i, restore_in_term outty, restore_in_term t,
 204              List.map restore_in_term pl)
 205          | C.Fix (i, fl) ->
 206             let len = List.length fl in
 207             let liftedfl =
 208              List.map
 209               (fun (name, i, ty, bo) ->
 210                 (name, i, restore_in_term ty, restore_in_term bo))
 211                fl
 212             in
 213              C.Fix (i, liftedfl)
 214          | C.CoFix (i, fl) ->
 215             let len = List.length fl in
 216             let liftedfl =
 217              List.map
 218               (fun (name, ty, bo) -> (name, restore_in_term ty, restore_in_term bo))
 219                fl
 220             in
 221              C.CoFix (i, liftedfl)
 222       in
 223       function
 224          C.Constant (name,bo,ty,params,attrs) ->
 225            let bo' =
 226              match bo with
 227                None -> None
 228              | Some bo -> Some (restore_in_term bo)
 229            in
 230            let ty' = restore_in_term ty in
 231            let params' = List.map recons params in
 232            C.Constant (name, bo', ty', params',attrs)
 233        | C.CurrentProof (name,conjs,bo,ty,params,attrs) ->
 234            let conjs' =
 235              List.map
 236                (function (i,hyps,ty) ->
 237                  (i,
 238                  List.map (function
 239                      None -> None
 240                    | Some (name,C.Decl t) ->
 241                        Some (name,C.Decl (restore_in_term t))
 242                    | Some (name,C.Def (bo,ty)) ->
 243                        let ty' =
 244                          match ty with
 245                            None -> None
 246                          | Some ty'' -> Some (restore_in_term ty'')
 247                        in
 248                        Some (name,C.Def (restore_in_term bo, ty'))) hyps,
 249                  restore_in_term ty))
 250                conjs
 251            in
 252            let bo' = restore_in_term bo in
 253            let ty' = restore_in_term ty in
 254            let params' = List.map recons params in
 255            C.CurrentProof (name, conjs', bo', ty', params',attrs)
 256        | C.Variable (name,bo,ty,params,attrs) ->
 257            let bo' =
 258              match bo with
 259                None -> None
 260              | Some bo -> Some (restore_in_term bo)
 261            in
 262            let ty' = restore_in_term ty in
 263            let params' = List.map recons params in
 264            C.Variable (name, bo', ty', params',attrs)
 265        | C.InductiveDefinition (tl,params,paramsno,attrs) ->
 266            let params' = List.map recons params in
 267            let tl' =
 268              List.map (function (name, inductive, ty, constructors) ->
 269                name,
 270                inductive,
 271                restore_in_term ty,
 272                (List.map
 273                  (function (name, ty) -> name, restore_in_term ty)
 274                  constructors))
 275                tl
 276            in
 277            C.InductiveDefinition (tl', params', paramsno, attrs)
 278     ;;
 279
 280     let empty () =
 281       HT.clear cacheOfCookedObjects;
 282       unchecked_list := [] ;
 283       frozen_list := []
 284     ;;
 285
 286     (* FIX: universe stuff?? *)
 287     let dump_to_channel ?(callback = ignore) oc =
 288      HT.iter (fun uri _ -> callback (UriManager.string_of_uri uri))
 289        cacheOfCookedObjects;
 290      Marshal.to_channel oc cacheOfCookedObjects []
 291     ;;
 292
 293     (* FIX: universes stuff?? *)
 294     let restore_from_channel ?(callback = ignore) ic =
 295       let restored = Marshal.from_channel ic in
 296       (* FIXME: should this empty clean the frozen and unchecked?
 297        * if not, the only-one-empty-end-not-3 patch is wrong
 298        *)
 299       empty ();
 300       HT.iter
 301        (fun k (v,u,l) ->
 302          callback (UriManager.string_of_uri k);
 303          let reconsed_entry =
 304            restore_uris v,CicUniv.recons_graph u,List.map CicUniv.recons_univ l
 305          in
 306          HT.add cacheOfCookedObjects
 307            (UriManager.uri_of_string (UriManager.string_of_uri k))
 308            reconsed_entry)
 309        restored
 310     ;;
 311
 312
 313     let is_in_frozen uri =
 314       List.mem_assoc uri !frozen_list
 315     ;;
 316
 317     let is_in_unchecked uri =
 318       List.mem_assoc uri !unchecked_list
 319     ;;
 320
 321     let is_in_cooked uri =
 322       HT.mem cacheOfCookedObjects uri
 323     ;;
 324
 325
 326     (*******************************************************************
 327       TASSI: invariant
 328       we need, in the universe generation phase, to traverse objects
 329       that are not yet committed, so we search them in the frozen list.
 330       Only uncommitted objects without a universe file (see the assertion)
 331       can be searched with method
 332     *******************************************************************)
 333
 334     let find_or_add_to_unchecked uri ~get_object_to_add =
 335      try
 336        let o,g_and_l = List.assq uri !unchecked_list in
 337          match g_and_l with
 338              (* FIXME: we accept both cases, as at the end of this function
 339                * maybe the None universe outside the cache module should be
 340                * avoided elsewhere.
 341                *
 342                * another thing that should be removed if univ generation phase
 343                * and lib exportation are unified.
 344                *)
 345            | None -> o,CicUniv.empty_ugraph,[]
 346            | Some (g,l) -> o,g,l
 347      with
 348          Not_found ->
 349            if List.mem_assq uri !frozen_list then
 350              (* CIRCULAR DEPENDENCY DETECTED, print the error and raise *)
 351              begin
 352                print_endline "\nCircularDependency!\nfrozen list: \n";
 353                List.iter (
 354                  fun (u,(_,o)) ->
 355                    let su = UriManager.string_of_uri u in
 356                    let univ = if o = None then "NO_UNIV" else "" in
 357                    print_endline (su^" "^univ))
 358                  !frozen_list;
 359                raise (CircularDependency (lazy (UriManager.string_of_uri uri)))
 360              end
 361            else
 362              if HT.mem cacheOfCookedObjects uri then
 363                (* DOUBLE COOK DETECTED, raise the exception *)
 364                raise (AlreadyCooked (UriManager.string_of_uri uri))
 365              else
 366                (* OK, it is not already frozen nor cooked *)
 367                let obj,ugraph_and_univlist = get_object_to_add uri in
 368                let ugraph_real, univlist_real =
 369                  match ugraph_and_univlist with
 370                      (* FIXME: not sure it is OK*)
 371                      None -> CicUniv.empty_ugraph, []
 372                    | Some ((g,l) as g_and_l) -> g_and_l
 373                in
 374                unchecked_list :=
 375                  (uri,(obj,ugraph_and_univlist))::!unchecked_list ;
 376                obj, ugraph_real, univlist_real
 377     ;;
 378
 379     let unchecked_to_frozen uri =
 380       try
 381         let obj,ugraph_and_univlist = List.assq uri !unchecked_list in
 382         unchecked_list := List.remove_assq uri !unchecked_list ;
 383         frozen_list := (uri,(obj,ugraph_and_univlist))::!frozen_list
 384       with
 385         Not_found -> raise (CouldNotFreeze (UriManager.string_of_uri uri))
 386     ;;
 387
 388
 389    (************************************************************
 390      TASSI: invariant
 391      only object with a valid universe graph can be committed
 392
 393      this should disappear if the universe generation phase and the
 394      library exportation are unified.
 395    *************************************************************)
 396    let frozen_to_cooked ~uri =
 397     try
 398       let obj,ugraph_and_univlist = List.assq uri !frozen_list in
 399         match ugraph_and_univlist with
 400         | None -> assert false (* only NON dummy universes can be committed *)
 401         | Some (g,l) ->
 402            CicUniv.assert_univs_have_uri g l;
 403            frozen_list := List.remove_assq uri !frozen_list ;
 404            HT.add cacheOfCookedObjects uri (obj,g,l)
 405     with
 406         Not_found -> raise (CouldNotUnfreeze (UriManager.string_of_uri uri))
 407    ;;
 408
 409    let can_be_cooked uri =
 410      try
 411        let obj,ugraph_and_univlist = List.assq uri !frozen_list in
 412          (* FIXME: another thing to remove if univ generation phase and lib
 413           * exportation are unified.
 414           *)
 415          match ugraph_and_univlist with
 416              None -> false
 417            | Some _ -> true
 418      with
 419          Not_found -> false
 420    ;;
 421
 422    (* this function injects a real universe graph in a (uri, (obj, None))
 423     * element of the frozen list.
 424     *
 425     * FIXME: another thing to remove if univ generation phase and lib
 426     * exportation are unified.
 427     *)
 428    let hack_univ uri (real_ugraph, real_univlist)  =
 429      try
 430        let o,ugraph_and_univlist = List.assq uri !frozen_list in
 431          match ugraph_and_univlist with
 432              None ->
 433                frozen_list := List.remove_assoc uri !frozen_list;
 434                frozen_list :=
 435                  (uri,(o,Some (real_ugraph, real_univlist)))::!frozen_list;
 436            | Some g ->
 437                debug_print (lazy (
 438                  "You are probably hacking an object already hacked or an"^
 439                  " object that has the universe file but is not"^
 440                  " yet committed."));
 441                assert false
 442      with
 443          Not_found ->
 444            debug_print (lazy (
 445              "You are hacking an object that is not in the"^
 446              " frozen_list, this means you are probably generating an"^
 447              " universe file for an object that already"^
 448              " as an universe file"));
 449            assert false
 450    ;;
 451
 452    let find_cooked ~key:uri = HT.find cacheOfCookedObjects uri ;;
 453
 454    let add_cooked ~key:uri (obj,ugraph,univlist) =
 455      HT.add cacheOfCookedObjects uri (obj,ugraph,univlist)
 456    ;;
 457
 458    (* invariant
 459     *
 460     * an object can be romeved from the cache only if we are not typechecking
 461     * something. this means check and frozen must be empty.
 462     *)
 463    let remove uri =
 464      if !frozen_list <> [] then
 465        failwith "CicEnvironment.remove while type checking"
 466      else
 467       begin
 468        HT.remove cacheOfCookedObjects uri;
 469        unchecked_list :=
 470         List.filter (fun (uri',_) -> not (UriManager.eq uri uri')) !unchecked_list
 471       end
 472    ;;
 473
 474    let  list_all_cooked_uris () =
 475      HT.fold (fun u _ l -> u::l) cacheOfCookedObjects []
 476    ;;
 477
 478   end
 479 ;;
 480
 481 (* ************************************************************************
 482                         HERE ENDS THE CACHE MODULE
 483  * ************************************************************************ *)
 484
 485 (* exported cache functions *)
 486 let dump_to_channel = Cache.dump_to_channel;;
 487 let restore_from_channel = Cache.restore_from_channel;;
 488 let empty = Cache.empty;;
 489
 490 let total_parsing_time = ref 0.0
 491
 492 let get_object_to_add uri =
 493  try
 494   let filename = Http_getter.getxml' uri in
 495   let bodyfilename =
 496     match UriManager.bodyuri_of_uri uri with
 497        None -> None
 498     |  Some bodyuri ->
 499         if Http_getter.exists' bodyuri then
 500           Some (Http_getter.getxml' bodyuri)
 501         else
 502           None
 503   in
 504   let obj =
 505     try
 506       let time = Unix.gettimeofday() in
 507       let rc = CicParser.obj_of_xml uri filename bodyfilename in
 508       total_parsing_time :=
 509         !total_parsing_time +. ((Unix.gettimeofday()) -. time );
 510       rc
 511     with exn ->
 512       (match exn with
 513       | CicParser.Getter_failure ("key_not_found", uri) ->
 514           raise (Object_not_found (UriManager.uri_of_string uri))
 515       | _ -> raise exn)
 516   in
 517   let ugraph_and_univlist,filename_univ =
 518     try
 519       let filename_univ =
 520         let univ_uri = UriManager.univgraphuri_of_uri uri in
 521         Http_getter.getxml' univ_uri
 522       in
 523         Some (CicUniv.ugraph_and_univlist_of_xml filename_univ),
 524         Some filename_univ
 525     with
 526     | Http_getter_types.Key_not_found _
 527     | Http_getter_types.Unresolvable_URI _ ->
 528       debug_print (lazy (
 529         "WE HAVE NO UNIVERSE FILE FOR " ^ (UriManager.string_of_uri uri)));
 530       (* WE SHOULD FAIL (or return None, None *)
 531       Some (CicUniv.empty_ugraph, []), None
 532   in
 533   obj, ugraph_and_univlist
 534  with Http_getter_types.Key_not_found _ -> raise (Object_not_found uri)
 535 ;;
 536
 537 (* this is the function to fetch the object in the unchecked list and
 538  * nothing more (except returning it)
 539  *)
 540 let find_or_add_to_unchecked uri =
 541  Cache.find_or_add_to_unchecked uri ~get_object_to_add
 542
 543 (* set_type_checking_info uri                                   *)
 544 (* must be called once the type-checking of uri is finished     *)
 545 (* The object whose uri is uri is unfreezed                     *)
 546 (*                                                              *)
 547 (* the replacement ugraph must be the one returned by the       *)
 548 (* typechecker, restricted with the CicUnivUtils.clean_and_fill *)
 549 let set_type_checking_info ?(replace_ugraph_and_univlist=None) uri =
 550 (*
 551   if not (Cache.can_be_cooked uri) && replace_ugraph <> None then begin
 552     debug_print (lazy (
 553       "?replace_ugraph must be None if you are not committing an "^
 554       "object that has a universe graph associated "^
 555       "(can happen only in the fase of universes graphs generation)."));
 556     assert false
 557   else
 558 *)
 559   match Cache.can_be_cooked uri, replace_ugraph_and_univlist with
 560   | true, Some _
 561   | false, None ->
 562       debug_print (lazy (
 563         "?replace_ugraph must be (Some ugraph) when committing an object that "^
 564         "has no associated universe graph. If this is in make_univ phase you "^
 565         "should drop this exception and let univ_make commit thi object with "^
 566         "proper arguments"));
 567       assert false
 568   | _ ->
 569       (match replace_ugraph_and_univlist with
 570       | None -> ()
 571       | Some g_and_l -> Cache.hack_univ uri g_and_l);
 572       Cache.frozen_to_cooked uri
 573 ;;
 574
 575 (* fetch, unfreeze and commit an uri to the cacheOfCookedObjects and
 576  * return the object,ugraph
 577  *)
 578 let add_trusted_uri_to_cache uri =
 579   let o,u,_ = find_or_add_to_unchecked uri in
 580   Cache.unchecked_to_frozen uri;
 581   set_type_checking_info uri;
 582   try
 583     Cache.find_cooked uri
 584   with Not_found -> assert false
 585 ;;
 586
 587 (* get the uri, if we trust it will be added to the cacheOfCookedObjects *)
 588 let get_cooked_obj_with_univlist ?(trust=true) base_univ uri =
 589   try
 590     (* the object should be in the cacheOfCookedObjects *)
 591     let o,u,l = Cache.find_cooked uri in
 592       o,(CicUniv.merge_ugraphs base_univ u),l
 593   with Not_found ->
 594     (* this should be an error case, but if we trust the uri... *)
 595     if trust && trust_obj uri then
 596       (* trusting means that we will fetch cook it on the fly *)
 597       let o,u,l = add_trusted_uri_to_cache uri in
 598         o,(CicUniv.merge_ugraphs base_univ u),l
 599     else
 600       (* we don't trust the uri, so we fail *)
 601       begin
 602         debug_print (lazy ("CACHE MISS: " ^ (UriManager.string_of_uri uri)));
 603         raise Not_found
 604       end
 605
 606 let get_cooked_obj ?trust base_univ uri =
 607   let o,g,_ = get_cooked_obj_with_univlist ?trust base_univ uri in
 608   o,g
 609
 610 (* This has not the old semantic :( but is what the name suggests
 611  *
 612  *   let is_type_checked ?(trust=true) uri =
 613  *     try
 614  *       let _ = Cache.find_cooked uri in
 615  *         true
 616  *     with
 617  *       Not_found ->
 618  *         trust && trust_obj uri
 619  *   ;;
 620  *
 621  * as the get_cooked_obj but returns a type_checked_obj
 622  *
 623  *)
 624 let is_type_checked ?(trust=true) base_univ uri =
 625   try
 626     let o,u,_ = Cache.find_cooked uri in
 627       CheckedObj (o,(CicUniv.merge_ugraphs base_univ u))
 628   with Not_found ->
 629     (* this should return UncheckedObj *)
 630     if trust && trust_obj uri then
 631       (* trusting means that we will fetch cook it on the fly *)
 632       let o,u,_ = add_trusted_uri_to_cache uri in
 633         CheckedObj ( o, CicUniv.merge_ugraphs u base_univ )
 634     else
 635       let o,u,_ = find_or_add_to_unchecked uri in
 636       Cache.unchecked_to_frozen uri;
 637         UncheckedObj o
 638 ;;
 639
 640 (* as the get cooked, but if not present the object is only fetched,
 641  * not unfreezed and committed
 642  *)
 643 let get_obj base_univ uri =
 644   try
 645     (* the object should be in the cacheOfCookedObjects *)
 646     let o,u,_ = Cache.find_cooked uri in
 647       o,(CicUniv.merge_ugraphs base_univ u)
 648   with Not_found ->
 649     (* this should be an error case, but if we trust the uri... *)
 650       let o,u,_ = find_or_add_to_unchecked uri in
 651         o,(CicUniv.merge_ugraphs base_univ u)
 652 ;;
 653
 654 let in_cache uri =
 655   Cache.is_in_cooked uri || Cache.is_in_frozen uri || Cache.is_in_unchecked uri
 656
 657 let add_type_checked_obj uri (obj,ugraph,univlist) =
 658  Cache.add_cooked ~key:uri (obj,ugraph,univlist)
 659
 660 let in_library uri = in_cache uri || Http_getter.exists' uri
 661
 662 let remove_obj = Cache.remove
 663
 664 let list_uri () =
 665   Cache.list_all_cooked_uris ()
 666 ;;
 667
 668 let list_obj () =
 669   try
 670     List.map (fun u ->
 671       let o,ug = get_obj CicUniv.empty_ugraph u in
 672         (u,o,ug))
 673     (list_uri ())
 674   with
 675     Not_found ->
 676       debug_print (lazy "Who has removed the uri in the meanwhile?");
 677       raise Not_found
 678 ;;