From f951f6a1c14f33b624789bcf60e80d8307b461d3 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 5 Sep 2005 12:42:57 +0000
Subject: [PATCH] Critical bug fixed: the get_cooked_obj was called on an
 object that was not in cache. The bug did not manifest when the environment
 was trusted.

---
 helm/matita/matita.txt                  |   4 +-
 helm/ocaml/cic_unification/cicRefine.ml | 107 +++++++++++-------------
 2 files changed, 52 insertions(+), 59 deletions(-)

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index 0d3fa1aec..a3d87835a 100644
--- a/helm/matita/matita.txt
+++ b/helm/matita/matita.txt
@@ -1,7 +1,5 @@
 TODO
   NUCLEO
-  - CRITICO: quando l'environment non e' trusted non compila la library di
-    matita!!!
   - PREOCCUPANTE: per 
     inductive i : Prop := K : True (*-> i*) -> i.
     noi generiamo i_rec e i_rect con e senza il commento qui sopra; Coq NON
@@ -112,6 +110,8 @@ TODO
     i demoni scopiazzano venti righe per via del getter embedded :-(
 
 DONE
+- CRITICO: quando l'environment non e' trusted non compila la library di
+  matita!!! -> Gares, CSC
 - bug di unsharing -> CSC
 - CRITICO (trovato anche da Ferruccio): typechecking di
   cic:/Coq/ring/Quote/index_eq_prop.con
diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 5c031f473..148450f5d 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -47,76 +47,68 @@ let rec split l n =
 ;;
 
 let rec type_of_constant uri ugraph =
-  let module C = Cic in
-  let module R = CicReduction in
-  let module U = UriManager in
-    (*
-      let obj =
-      try
-      CicEnvironment.get_cooked_obj uri
-      with Not_found -> assert false
-      in
-    *)
-  let obj,u= CicEnvironment.get_obj ugraph uri in
-    match obj with
-	C.Constant (_,_,ty,_,_) -> ty,u
-      | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
-      | _ ->
-	  raise
-	    (RefineFailure ("Unknown constant definition " ^  U.string_of_uri uri))
+ let module C = Cic in
+ let module R = CicReduction in
+ let module U = UriManager in
+  let _ = CicTypeChecker.typecheck uri in
+  let obj,u =
+   try
+    CicEnvironment.get_cooked_obj ugraph uri
+   with Not_found -> assert false
+  in
+   match obj with
+      C.Constant (_,_,ty,_,_) -> ty,u
+    | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
+    | _ ->
+       raise
+        (RefineFailure ("Unknown constant definition " ^  U.string_of_uri uri))
 
 and type_of_variable uri ugraph =
   let module C = Cic in
   let module R = CicReduction in
   let module U = UriManager in
-    (*
-      let obj =
-      try
-      CicEnvironment.get_cooked_obj uri
-      with Not_found -> assert false
-      in
-    *)
-  let obj,u = CicEnvironment.get_obj ugraph uri in
-    match obj with
-	C.Variable (_,_,ty,_,_) -> ty,u
-      |  _ ->
-	   raise
-	    (RefineFailure
-               ("Unknown variable definition " ^ UriManager.string_of_uri uri))
+  let _ = CicTypeChecker.typecheck uri in
+  let obj,u =
+   try
+    CicEnvironment.get_cooked_obj ugraph uri
+    with Not_found -> assert false
+  in
+   match obj with
+      C.Variable (_,_,ty,_,_) -> ty,u
+    | _ ->
+        raise
+         (RefineFailure
+          ("Unknown variable definition " ^ UriManager.string_of_uri uri))
 
 and type_of_mutual_inductive_defs uri i ugraph =
   let module C = Cic in
   let module R = CicReduction in
   let module U = UriManager in
-    (*
-      let obj =
-      try
-      CicEnvironment.get_cooked_obj uri
-      with Not_found -> assert false
-      in
-    *)
-  let obj,u = CicEnvironment.get_obj ugraph uri in
-    match obj with
-	C.InductiveDefinition (dl,_,_,_) ->
-	  let (_,_,arity,_) = List.nth dl i in
-	    arity,u
-      | _ ->
-	  raise
-	    (RefineFailure
-               ("Unknown mutual inductive definition " ^ U.string_of_uri uri))
+  let _ = CicTypeChecker.typecheck uri in
+  let obj,u =
+   try
+    CicEnvironment.get_cooked_obj ugraph uri
+   with Not_found -> assert false
+  in
+   match obj with
+      C.InductiveDefinition (dl,_,_,_) ->
+        let (_,_,arity,_) = List.nth dl i in
+	 arity,u
+    | _ ->
+       raise
+        (RefineFailure
+         ("Unknown mutual inductive definition " ^ U.string_of_uri uri))
 
 and type_of_mutual_inductive_constr uri i j ugraph =
   let module C = Cic in
   let module R = CicReduction in
   let module U = UriManager in
-    (*
-      let obj =
-      try
-      CicEnvironment.get_cooked_obj uri
-      with Not_found -> assert false
-      in
-    *)
-  let obj,u = CicEnvironment.get_obj ugraph uri in
+  let _ = CicTypeChecker.typecheck uri in
+   let obj,u =
+    try
+     CicEnvironment.get_cooked_obj ugraph uri
+    with Not_found -> assert false
+   in
     match obj with
 	C.InductiveDefinition (dl,_,_,_) ->
 	  let (_,_,_,cl) = List.nth dl i in
@@ -342,7 +334,8 @@ and type_of_aux' metasenv context t ugraph =
 	    (* first, get the inductive type (and noparams) 
              * in the environment  *)
 	    let (_,b,arity,constructors), expl_params, no_left_params,ugraph =
-	      let obj,u = CicEnvironment.get_obj ugraph uri in
+              let _ = CicTypeChecker.typecheck uri in
+	      let obj,u = CicEnvironment.get_cooked_obj ugraph uri in
               match obj with
 		  C.InductiveDefinition (l,expl_params,parsno,_) -> 
 		    List.nth l i , expl_params, parsno, u
@@ -437,7 +430,7 @@ and type_of_aux' metasenv context t ugraph =
                (let candidate,ugraph5,metasenv,subst = 
                  let exp_name_subst, metasenv = 
                     let o,_ = 
-                      CicEnvironment.get_obj CicUniv.empty_ugraph uri 
+                      CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri 
                     in
                     let uris = CicUtil.params_of_obj o in
                     List.fold_right (
-- 
2.39.2