X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_proof_checking%2FcicEnvironment.mli;h=3e5c2bf77c161b071c77f80366047b076f8422e1;hb=ac7687ce66526f905874ed99a845223c853c558a;hp=c3ffd6fe452706bd1a7d0d0a687ec201b0245da7;hpb=5a92117eeff70048d29e91ba24e113155d956e1b;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli
index c3ffd6fe4..3e5c2bf77 100644
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.mli
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli
@@ -30,10 +30,13 @@
 (*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
 (*                                 24/01/2000                                 *)
 (*                                                                            *)
-(* This module implements a trival cache system (an hash-table) for cic       *)(* objects. Uses the getter (getter.ml) and the parser (cicParser.ml)         *)(*                                                                            *)
+(* This module implements a trival cache system (an hash-table) for cic       *)
+(* objects. Uses the getter (getter.ml) and the parser (cicParser.ml)         *)
+(*                                                                            *)
 (******************************************************************************)
 
 exception CircularDependency of string;;
+exception Term_not_found of UriManager.uri;;
 
 (* get_obj uri                                                                *)
 (* returns the cic object whose uri is uri. If the term is not just in cache, *)
@@ -41,22 +44,6 @@ exception CircularDependency of string;;
 (* the result of Getter.get uri                                               *)
 val get_obj : UriManager.uri -> Cic.obj
 
-(* get_annobj uri                                                             *)
-(* returns the cic object whose uri is uri either in annotated and in         *)
-(* deannotated form. It returns also the map from ids to annotation targets.  *)
-(* The term is put in cache if it's not there yet.                            *)
-(* The functions raise CircularDependency if asked to retrieve a Frozen object*)
-val get_annobj :
- UriManager.uri -> Cic.annobj * (Cic.id, Cic.anntarget) Hashtbl.t * Cic.obj
-
-(* DANGEROUS!!!                                *)
-(* USEFUL ONLY DURING THE FIXING OF THE FILES  *)
-(* change_obj uri (Some newobj)                *)
-(*  maps uri to newobj in cache.               *)
-(* change_obj uri None                         *)
-(*  maps uri to a freeze dummy-object.         *)
-val change_obj : UriManager.uri -> Cic.obj option -> unit
-
 type type_checked_obj =
    CheckedObj of Cic.obj    (* cooked obj *)
  | UncheckedObj of Cic.obj  (* uncooked obj *)
@@ -67,7 +54,7 @@ type type_checked_obj =
 (* otherwise it returns (false,object) and freeze the object for    *)
 (* type-checking                                                    *)
 (* set_type_checking_info must be called to unfreeze the object     *)
-val is_type_checked : UriManager.uri -> int -> type_checked_obj
+val is_type_checked : ?trust:bool -> UriManager.uri -> type_checked_obj
 
 (* set_type_checking_info uri                                         *)
 (* must be called once the type-checking of uri is finished           *)
@@ -75,9 +62,36 @@ val is_type_checked : UriManager.uri -> int -> type_checked_obj
 (* again in the future (is_type_checked will return true)             *)
 val set_type_checking_info : UriManager.uri -> unit
 
-(* get_cooked_obj uri cookingsno *)
-val get_cooked_obj : UriManager.uri -> int -> Cic.obj
+(* We need this in the Qed. *)
+val add_type_checked_term : UriManager.uri -> Cic.obj -> unit
+
+  (** remove a type checked term
+  * @raise Term_not_found when given term is not in the environment
+  * @raise Failure when remove_term is invoked while type checking *)
+val remove_term: UriManager.uri -> unit
+
+(* get_cooked_obj ~trust uri                                        *)
+(* returns the object if it is already type-checked or if it can be *)
+(* trusted (if [trust] = true and the trusting function accepts it) *)
+(* Otherwise it raises Not_found                                    *)
+val get_cooked_obj : ?trust:bool -> UriManager.uri -> Cic.obj
+
+(* FUNCTIONS USED ONLY IN THE TOPLEVEL/PROOF-ENGINE *)
+
+exception OnlyPutOfInductiveDefinitionsIsAllowed
+
+(* put_inductive_definition uri obj                                      *)
+(* put [obj] (that must be an InductiveDefinition and show URI is [uri]) *)
+(* in the environment.                                                   *)
+(* WARNING: VERY UNSAFE.                                                 *)
+(* This function should be called only on a well-typed definition.       *)
+val put_inductive_definition : UriManager.uri -> Cic.obj -> unit
+
+(* (de)serialization *)
+val dump_to_channel : ?callback:(string -> unit) -> out_channel -> unit
+val restore_from_channel : ?callback:(string -> unit) -> in_channel -> unit
+val empty : unit -> unit
 
-(* set_cooking_function cooking_function *)
-val set_cooking_function :
- (Cic.obj -> UriManager.uri -> (int * Cic.obj) list) -> unit
+(* for filtering in tacticChaser *)
+(* NEW *)
+val in_cache : UriManager.uri -> bool