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