From f951f6a1c14f33b624789bcf60e80d8307b461d3 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen 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