From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 3 Dec 2002 14:50:31 +0000 (+0000)
Subject: put_inductive_definition implemented and exposed.
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1bd58ea9bfc5b8fc2534ba6698fb6afd9c4c9404;p=helm.git

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.
---

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