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=b7b4a51797c5e9ad34d50c9e7da003521e1f289a;hpb=1a685a8dd6747753020b8af3648441a6d7bdf36a;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli index b7b4a5179..c3ca6ef95 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.mli +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli @@ -23,29 +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 *) @@ -54,16 +62,27 @@ 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 : ?trust:bool -> UriManager.uri -> 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 (* We need this in the Qed. *) -val add_type_checked_term : UriManager.uri -> Cic.obj -> unit +val add_type_checked_term : + UriManager.uri -> (Cic.obj * CicUniv.universe_graph) -> unit (** remove a type checked term * @raise Term_not_found when given term is not in the environment @@ -74,7 +93,9 @@ val remove_term: UriManager.uri -> unit (* 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 +val get_cooked_obj : + ?trust:bool -> UriManager.uri -> + CicUniv.universe_graph -> Cic.obj * CicUniv.universe_graph (* FUNCTIONS USED ONLY IN THE TOPLEVEL/PROOF-ENGINE *) @@ -85,7 +106,8 @@ exception OnlyPutOfInductiveDefinitionsIsAllowed (* 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 +val put_inductive_definition : + UriManager.uri -> (Cic.obj * CicUniv.universe_graph) -> unit (* (de)serialization *) val dump_to_channel : ?callback:(string -> unit) -> out_channel -> unit