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