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.

diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt
index 0d3fa1aec319fe77d0a7dc36d8853606719a2c3d..a3d87835ad04ef286b35a13233a8fb0ede2d3fca 100644 (file)
--- 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 5c031f4733b6806f2da7c1b9ef683d8d589112ec..148450f5d17f1375b275186f3c08d807d0780a6b 100644 (file)
--- 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 (