X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicEnvironment.mli;h=55566a614493de9ae8b872a0a9347d2cf6a37073;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=c3ca6ef952f191c6c1c4fb9783b43557733ed143;hpb=31851952e1cc2db59168c5fd6f6093d9bc37ea86;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli index c3ca6ef95..55566a614 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.mli +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli @@ -23,47 +23,45 @@ * 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 *) -(* *) -(* ~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. *) +(****************************************************************************) +(* *) +(* 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 : - ?not_jet_cooked:bool -> UriManager.uri -> CicUniv.universe_graph -> - Cic.obj * CicUniv.universe_graph + CicUniv.universe_graph -> UriManager.uri -> + Cic.obj * CicUniv.universe_graph type type_checked_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 *) +(* + * 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 -> UriManager.uri -> CicUniv.universe_graph -> type_checked_obj + ?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 *) @@ -77,37 +75,41 @@ val is_type_checked : (* 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:(CicUniv.universe_graph option) -> UriManager.uri -> unit + ?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 * CicUniv.universe_graph) -> 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 -> - CicUniv.universe_graph -> Cic.obj * CicUniv.universe_graph - -(* FUNCTIONS USED ONLY IN THE TOPLEVEL/PROOF-ENGINE *) + ?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 * CicUniv.universe_graph) -> unit +(* FUNCTIONS USED ONLY IN THE TOPLEVEL/PROOF-ENGINE *) (* (de)serialization *) val dump_to_channel : ?callback:(string -> unit) -> out_channel -> unit @@ -117,6 +119,18 @@ 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 *) + (** @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 *)