X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicEnvironment.mli;h=5c10c81a37ea150f77be59597f6762de3363ea0c;hb=de36c6322dde3866f3da822f1795cc518233c79f;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..5c10c81a3 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.mli +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli @@ -23,61 +23,108 @@ * 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 Object_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_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 +(* as the get cooked, but if not present the object is only fetched, + * not unfreezed and committed + * @raise Object_not_found + *) +val get_obj : + CicUniv.universe_graph -> UriManager.uri -> + 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 *) -(*CSC commento falso ed obsoleto *) -(* returns (true,object) if the object has been type-checked *) -(* 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 +(* + * I think this should be the real semantic: + * + * val is_type_checked: + * ?trust:bool -> UriManager.uri -> bool + * + * but the old semantic is similar to get_cooked_obj, but + * returns an unchecked object intead of a Not_found + *) +val is_type_checked : + ?trust:bool -> CicUniv.universe_graph -> UriManager.uri -> + 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 * CicUniv.universe_graph) -> 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 -> CicUniv.universe_graph -> UriManager.uri -> + 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 + + (** @return true for objects currently cooked/frozend/unchecked, false + * otherwise (i.e. objects already parsed from XML) *) +val in_cache : UriManager.uri -> bool + +(* to debug the matitac batch compiler *) +val list_obj: unit -> (UriManager.uri * Cic.obj * CicUniv.universe_graph) list +val list_uri: unit -> UriManager.uri list -(* get_cooked_obj uri cookingsno *) -val get_cooked_obj : UriManager.uri -> int -> Cic.obj + (** @return true for objects available in the library *) +val in_library: UriManager.uri -> bool -(* set_cooking_function cooking_function *) -val set_cooking_function : - (Cic.obj -> UriManager.uri -> (int * Cic.obj) list) -> unit +(* EOF *)