X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicEnvironment.mli;h=c3ca6ef952f191c6c1c4fb9783b43557733ed143;hb=31851952e1cc2db59168c5fd6f6093d9bc37ea86;hp=b781a5c42fc4dfa6b53e6e955f9f98bfe6577ce4;hpb=ae326f646ef4c01b43d6da04201b427d1e175400;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli index b781a5c42..c3ca6ef95 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.mli +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli @@ -23,26 +23,37 @@ * http://cs.unibo.it/helm/. *) -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 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) *)(* *) -(******************************************************************************) +(*****************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 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) *) +(* *) +(*****************************************************************************) 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, *) -(* then it is parsed via CicParser.term_of_xml from the file whose name is *) -(* the result of Getter.get uri *) -val get_obj : UriManager.uri -> Cic.obj +(* get_obj uri *) +(* returns the cic object whose uri is uri. If the term is not just in cache,*) +(* then it is parsed via CicParser.term_of_xml from the file whose name is *) +(* the result of Getter.get uri *) +(* *) +(* ~not_jet_cooked returns the object even if it is not in the *) +(* CacheOfCookedObjects searching it in the frozen list. *) +(* This is necessary in cicUnivUtils.ml since (in the univ_maker phase *) +(* it has to traverse object before they are committed. *) +(* see the .ml file for some reassuring invariants on this. *) +val get_obj : + ?not_jet_cooked:bool -> UriManager.uri -> CicUniv.universe_graph -> + Cic.obj * CicUniv.universe_graph type type_checked_obj = - CheckedObj of Cic.obj (* cooked obj *) + CheckedObj of (Cic.obj * CicUniv.universe_graph) (* cooked obj *) | UncheckedObj of Cic.obj (* uncooked obj *) (* is_type_checked uri cookingsno *) @@ -51,17 +62,61 @@ 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 -> CicUniv.universe_graph -> type_checked_obj (* set_type_checking_info uri *) (* must be called once the type-checking of uri is finished *) (* The object whose uri is uri is unfreezed and won't be type-checked *) (* again in the future (is_type_checked will return true) *) -val set_type_checking_info : UriManager.uri -> unit +(* *) +(* Since the universes are not exported directly, but generated *) +(* typecheking the library, we can't find them in the library as we *) +(* do for the types. This means that when we commit uris during *) +(* univ generation we can't associate the uri with the universe graph *) +(* we find in the library, we have to calculate it and then inject it *) +(* in the cacke. This is an orrible backdoor used by univ_maker. *) +(* see the .ml file for some reassuring invariants *) +val set_type_checking_info : + ?replace_ugraph:(CicUniv.universe_graph option) -> 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 * CicUniv.universe_graph) -> unit -(* set_cooking_function cooking_function *) -val set_cooking_function : - (Cic.obj -> UriManager.uri -> (int * Cic.obj) list) -> 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 -> + CicUniv.universe_graph -> Cic.obj * CicUniv.universe_graph + +(* 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 * CicUniv.universe_graph) -> 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 trust function. Per default this function is set to (fun _ -> true) *) +val set_trust: (UriManager.uri -> bool) -> unit + +(* for filtering in tacticChaser *) +(* NEW *) +val in_cache : UriManager.uri -> bool