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