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