From 1bd58ea9bfc5b8fc2534ba6698fb6afd9c4c9404 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 3 Dec 2002 14:50:31 +0000 Subject: [PATCH] put_inductive_definition implemented and exposed. It is a very UNSAFE solution to the problem of computing inner-types of non-debrujined mutual inductive types (whose constructors referes to the not-yet-defined inductive type block): you can use this function to add the block to the environment; then you compute the inner-types; and finally you save the object and register it to the getter. --- helm/ocaml/cic_proof_checking/cicEnvironment.ml | 10 ++++++++++ helm/ocaml/cic_proof_checking/cicEnvironment.mli | 13 ++++++++++++- 2 files changed, 22 insertions(+), 1 deletion(-) diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml index e9050cd8c..823aa3a40 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml @@ -61,6 +61,7 @@ module Cache : val frozen_to_cooked : uri:UriManager.uri -> unit val find_cooked : key:UriManager.uri -> Cic.obj + val add_cooked : key:UriManager.uri -> Cic.obj -> unit end = struct @@ -130,6 +131,7 @@ module Cache : Not_found -> raise (CouldNotUnfreeze (UriManager.string_of_uri uri)) ;; let find_cooked ~key:uri = CacheOfCookedObjects.find uri;; + let add_cooked ~key:uri obj = CacheOfCookedObjects.add uri obj;; end ;; @@ -225,3 +227,11 @@ let get_obj uri = Not_found -> find_or_add_unchecked_to_cache uri ;; + +exception OnlyPutOfInductiveDefinitionsIsAllowed + +let put_inductive_definition uri obj = + match obj with + Cic.InductiveDefinition _ -> Cache.add_cooked uri obj + | _ -> raise OnlyPutOfInductiveDefinitionsIsAllowed +;; diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli index fbc53955b..e93db9582 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.mli +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli @@ -61,8 +61,19 @@ val is_type_checked : ?trust:bool -> UriManager.uri -> type_checked_obj (* again in the future (is_type_checked will return true) *) val set_type_checking_info : UriManager.uri -> unit -(* get_cooked_obj ~trust uri *) +(* 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 *) + +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 -> unit -- 2.39.2