X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicEnvironment.mli;h=55566a614493de9ae8b872a0a9347d2cf6a37073;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=3e5c2bf77c161b071c77f80366047b076f8422e1;hpb=f945768c2bdd355b394f1c4606727283504fbb54;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli index 3e5c2bf77..55566a614 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.mli +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli @@ -23,75 +23,114 @@ * 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) *) -(* *) -(******************************************************************************) - -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 +(****************************************************************************) +(* *) +(* 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 Lazy.t;; +exception Object_not_found of UriManager.uri;; + +(* as the get cooked, but if not present the object is only fetched, + * not unfreezed and committed + *) +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 : ?trust:bool -> UriManager.uri -> 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 *) +(* WARNING: THIS FUNCTION MUST BE CALLED ONLY BY CicTypeChecker *) +val set_type_checking_info : + ?replace_ugraph_and_univlist: + ((CicUniv.universe_graph * CicUniv.universe list) option) -> + UriManager.uri -> unit -(* We need this in the Qed. *) -val add_type_checked_term : UriManager.uri -> Cic.obj -> unit +(* this function is called by CicTypeChecker.typecheck_obj to add to the *) +(* environment a new well typed object that is not yet in the library *) +(* WARNING: THIS FUNCTION MUST BE CALLED ONLY BY CicTypeChecker *) +val add_type_checked_obj : + UriManager.uri -> + (Cic.obj * CicUniv.universe_graph * CicUniv.universe list) -> unit - (** remove a type checked term - * @raise Term_not_found when given term is not in the environment + (** remove a type checked object + * @raise Object_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 +val remove_obj: 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 *) +val get_cooked_obj : + ?trust:bool -> CicUniv.universe_graph -> UriManager.uri -> + Cic.obj * CicUniv.universe_graph -exception OnlyPutOfInductiveDefinitionsIsAllowed +(* get_cooked_obj_with_univlist ~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_with_univlist : + ?trust:bool -> CicUniv.universe_graph -> UriManager.uri -> + Cic.obj * CicUniv.universe_graph * CicUniv.universe list -(* 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 +(* FUNCTIONS USED ONLY IN THE TOPLEVEL/PROOF-ENGINE *) (* (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 -(* for filtering in tacticChaser *) -(* NEW *) +(** 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 + + (** @return true for objects available in the library *) +val in_library: UriManager.uri -> bool + + (** total parsing time, only to benchmark the parser *) +val total_parsing_time: float ref + +(* EOF *)