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