From 3158af584f7fdd261a39757d979bd4369197c2bb Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 30 Oct 2002 14:10:01 +0000 Subject: [PATCH] Better implementation of the trusting machinery: some CicEnvironment functions now have a trust optional attribute (that defaults to true). The TypeChecker uses the false value only when type-checking the topmost object. Every other operation of the kernel uses the true value (i.e. it trusts). Is this really a safe behaviour? Hmmmmm. We need a proof here. --- .../cic_proof_checking/cicEnvironment.ml | 38 +++++++++---------- .../cic_proof_checking/cicEnvironment.mli | 9 +++-- .../cic_proof_checking/cicReductionMachine.ml | 16 ++++---- .../cic_proof_checking/cicReductionNaif.ml | 4 +- .../cic_proof_checking/cicSubstitution.ml | 8 ++-- .../cic_proof_checking/cicTypeChecker.ml | 24 ++++++------ 6 files changed, 49 insertions(+), 50 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml index 329615bb3..e9050cd8c 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml @@ -37,9 +37,7 @@ let cleanup_tmp = true;; -let never_trust = function uri -> false;; -let always_trust = function uri -> true;; -let trust_obj = ref never_trust;; +let trust_obj = function uri -> true;; type type_checked_obj = CheckedObj of Cic.obj (* cooked obj *) @@ -169,7 +167,6 @@ let find_or_add_unchecked_to_cache uri = (* must be called once the type-checking of uri is finished *) (* The object whose uri is uri is unfreezed *) let set_type_checking_info uri = - trust_obj := never_trust ; Cache.frozen_to_cooked uri ;; @@ -179,43 +176,42 @@ let set_type_checking_info uri = (* otherwise it freezes the term for type-checking and returns it *) (* set_type_checking_info must be called to unfreeze the term *) -let is_type_checked uri = +let is_type_checked ?(trust=true) uri = try CheckedObj (Cache.find_cooked uri) with Not_found -> let obj = find_or_add_unchecked_to_cache uri in Cache.unchecked_to_frozen uri ; - if !trust_obj uri then + if trust && trust_obj uri then begin Logger.log (`Trusting uri) ; set_type_checking_info uri ; - trust_obj := always_trust ; CheckedObj (Cache.find_cooked uri) end else - begin - trust_obj := always_trust ; - UncheckedObj obj - end + UncheckedObj obj ;; -(* get_cooked_obj uri *) -(* returns the cooked cic object whose uri is uri. The term must be present *) -(* and cooked in cache *) -let get_cooked_obj 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 *) +let get_cooked_obj ?(trust=true) uri = try Cache.find_cooked uri with Not_found -> - if not (!trust_obj uri) then + if trust && trust_obj uri then begin - prerr_endline ("@@@ OOOOOOOPS: WE DO NOT TRUST " ^ UriManager.string_of_uri uri ^ " EVEN IF WE ARE REQUIRED TO DO THAT! THAT MAY MEAN LOOKING FOR TROUBLES ;-(") ; - raise Not_found + match is_type_checked uri with + CheckedObj obj -> obj + | _ -> assert false end else - match is_type_checked uri with - CheckedObj obj -> obj - | _ -> assert false + begin + prerr_endline ("@@@ OOOOOOOPS: get_cooked_obj(" ^ UriManager.string_of_uri uri ^ ") raises Not_found since the object is not type-checked nor trusted.") ; + raise Not_found + end ;; (* get_obj uri *) diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli index c54df77e2..fbc53955b 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.mli +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli @@ -53,7 +53,7 @@ type type_checked_obj = (* otherwise it returns (false,object) and freeze the object for *) (* type-checking *) (* set_type_checking_info must be called to unfreeze the object *) -val is_type_checked : UriManager.uri -> type_checked_obj +val is_type_checked : ?trust:bool -> UriManager.uri -> type_checked_obj (* set_type_checking_info uri *) (* must be called once the type-checking of uri is finished *) @@ -61,5 +61,8 @@ val is_type_checked : 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 uri *) -val get_cooked_obj : UriManager.uri -> Cic.obj +(* 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 diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml index e45702077..3b769b5bc 100644 --- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml +++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml @@ -82,7 +82,7 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) - CicSubstitution.lift m (List.assq uri ens) else let params = - (match CicEnvironment.get_cooked_obj uri with + (match CicEnvironment.get_obj uri with C.Constant _ -> raise ReferenceToConstant | C.Variable (_,_,_,params) -> params | C.CurrentProof _ -> raise ReferenceToCurrentProof @@ -111,7 +111,7 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) - | C.Appl l -> C.Appl (List.map (unwind_aux m) l) | C.Const (uri,exp_named_subst) -> let params = - (match CicEnvironment.get_cooked_obj uri with + (match CicEnvironment.get_obj uri with C.Constant (_,_,_,params) -> params | C.Variable _ -> raise ReferenceToVariable | C.CurrentProof (_,_,_,_,params) -> params @@ -124,7 +124,7 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) - C.Const (uri,exp_named_subst') | C.MutInd (uri,i,exp_named_subst) -> let params = - (match CicEnvironment.get_cooked_obj uri with + (match CicEnvironment.get_obj uri with C.Constant _ -> raise ReferenceToConstant | C.Variable _ -> raise ReferenceToVariable | C.CurrentProof _ -> raise ReferenceToCurrentProof @@ -137,7 +137,7 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) - C.MutInd (uri,i,exp_named_subst') | C.MutConstruct (uri,i,j,exp_named_subst) -> let params = - (match CicEnvironment.get_cooked_obj uri with + (match CicEnvironment.get_obj uri with C.Constant _ -> raise ReferenceToConstant | C.Variable _ -> raise ReferenceToVariable | C.CurrentProof _ -> raise ReferenceToCurrentProof @@ -259,7 +259,7 @@ let reduce context : config -> Cic.term = if List.exists (function (uri',_) -> UriManager.eq uri' uri) ens then reduce (0, [], [], List.assq uri ens, s) else - (match CicEnvironment.get_cooked_obj uri with + (match CicEnvironment.get_obj uri with C.Constant _ -> raise ReferenceToConstant | C.CurrentProof _ -> raise ReferenceToCurrentProof | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition @@ -319,7 +319,7 @@ let reduce context : config -> Cic.term = C.Appl (List.append (List.map (unwind k e ens) l) s) *) | (k, e, ens, (C.Const (uri,exp_named_subst) as t), s) -> - (match CicEnvironment.get_cooked_obj uri with + (match CicEnvironment.get_obj uri with C.Constant (_,Some body,_,_) -> let ens' = push_exp_named_subst k e ens exp_named_subst in (* constants are closed *) @@ -598,8 +598,8 @@ let are_convertible = else begin debug t1 [t2] "PREWHD"; - let t1' = whd context t1 - and t2' = whd context t2 in + let t1' = whd context t1 in + let t2' = whd context t2 in debug t1' [t2'] "POSTWHD"; aux2 t1' t2' end diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml index f7ddd1968..581c5918f 100644 --- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml +++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml @@ -57,7 +57,7 @@ let whd context = | None -> raise RelToHiddenHypothesis ) | C.Var (uri,exp_named_subst) as t -> - (match CicEnvironment.get_cooked_obj uri with + (match CicEnvironment.get_cooked_obj ~trust:false uri with C.Constant _ -> raise ReferenceToConstant | C.CurrentProof _ -> raise ReferenceToCurrentProof | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition @@ -80,7 +80,7 @@ let whd context = | C.Appl (he::tl) -> whdaux (tl@l) he | C.Appl [] -> raise (Impossible 1) | C.Const (uri,exp_named_subst) as t -> - (match CicEnvironment.get_cooked_obj uri with + (match CicEnvironment.get_cooked_obj ~trust:false uri with C.Constant (_,Some body,_,_) -> whdaux l (CicSubstitution.subst_vars exp_named_subst body) | C.Constant _ -> if l = [] then t else C.Appl (t::l) diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml index 002ea28df..4a938acb9 100644 --- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml +++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml @@ -202,7 +202,7 @@ prerr_endline ("@@@POSSIBLE BUG: SUBSTITUTION IS NOT SIMULTANEOUS") ; with Not_found -> let params = - (match CicEnvironment.get_cooked_obj uri with + (match CicEnvironment.get_cooked_obj ~trust:true uri with C.Constant _ -> raise ReferenceToConstant | C.Variable (_,_,_,params) -> params | C.CurrentProof _ -> raise ReferenceToCurrentProof @@ -250,7 +250,7 @@ prerr_endline "---- END\n\n " ; | C.Appl _ -> assert false | C.Const (uri,exp_named_subst') -> let params = - (match CicEnvironment.get_cooked_obj uri with + (match CicEnvironment.get_cooked_obj ~trust:true uri with C.Constant (_,_,_,params) -> params | C.Variable _ -> raise ReferenceToVariable | C.CurrentProof (_,_,_,_,params) -> params @@ -263,7 +263,7 @@ prerr_endline "---- END\n\n " ; C.Const (uri,exp_named_subst'') | C.MutInd (uri,typeno,exp_named_subst') -> let params = - (match CicEnvironment.get_cooked_obj uri with + (match CicEnvironment.get_cooked_obj ~trust:true uri with C.Constant _ -> raise ReferenceToConstant | C.Variable _ -> raise ReferenceToVariable | C.CurrentProof _ -> raise ReferenceToCurrentProof @@ -276,7 +276,7 @@ prerr_endline "---- END\n\n " ; C.MutInd (uri,typeno,exp_named_subst'') | C.MutConstruct (uri,typeno,consno,exp_named_subst') -> let params = - (match CicEnvironment.get_cooked_obj uri with + (match CicEnvironment.get_cooked_obj ~trust:true uri with C.Constant _ -> raise ReferenceToConstant | C.Variable _ -> raise ReferenceToVariable | C.CurrentProof _ -> raise ReferenceToCurrentProof diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 57bc5e2ad..7e96de2a4 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -124,7 +124,7 @@ let rec type_of_constant uri = let module R = CicReduction in let module U = UriManager in let cobj = - match CicEnvironment.is_type_checked uri with + match CicEnvironment.is_type_checked ~trust:true uri with CicEnvironment.CheckedObj cobj -> cobj | CicEnvironment.UncheckedObj uobj -> Logger.log (`Start_type_checking uri) ; @@ -153,7 +153,7 @@ let rec type_of_constant uri = ) ; CicEnvironment.set_type_checking_info uri ; Logger.log (`Type_checking_completed uri) ; - match CicEnvironment.is_type_checked uri with + match CicEnvironment.is_type_checked ~trust:false uri with CicEnvironment.CheckedObj cobj -> cobj | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError in @@ -167,7 +167,7 @@ and type_of_variable uri = let module R = CicReduction in let module U = UriManager in (* 0 because a variable is never cooked => no partial cooking at one level *) - match CicEnvironment.is_type_checked uri with + match CicEnvironment.is_type_checked ~trust:true uri with CicEnvironment.CheckedObj (C.Variable (_,_,ty,_)) -> ty | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_)) -> Logger.log (`Start_type_checking uri) ; @@ -477,14 +477,14 @@ and type_of_mutual_inductive_defs uri i = let module R = CicReduction in let module U = UriManager in let cobj = - match CicEnvironment.is_type_checked uri with + match CicEnvironment.is_type_checked ~trust:true uri with CicEnvironment.CheckedObj cobj -> cobj | CicEnvironment.UncheckedObj uobj -> Logger.log (`Start_type_checking uri) ; check_mutual_inductive_defs uri uobj ; CicEnvironment.set_type_checking_info uri ; Logger.log (`Type_checking_completed uri) ; - (match CicEnvironment.is_type_checked uri with + (match CicEnvironment.is_type_checked ~trust:false uri with CicEnvironment.CheckedObj cobj -> cobj | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError ) @@ -500,14 +500,14 @@ and type_of_mutual_inductive_constr uri i j = let module R = CicReduction in let module U = UriManager in let cobj = - match CicEnvironment.is_type_checked uri with + match CicEnvironment.is_type_checked ~trust:true uri with CicEnvironment.CheckedObj cobj -> cobj | CicEnvironment.UncheckedObj uobj -> Logger.log (`Start_type_checking uri) ; check_mutual_inductive_defs uri uobj ; CicEnvironment.set_type_checking_info uri ; Logger.log (`Type_checking_completed uri) ; - (match CicEnvironment.is_type_checked uri with + (match CicEnvironment.is_type_checked ~trust:false uri with CicEnvironment.CheckedObj cobj -> cobj | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError ) @@ -934,7 +934,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) -> let consty = - match CicEnvironment.get_cooked_obj uri with + match CicEnvironment.get_cooked_obj ~trust:false uri with C.InductiveDefinition (itl,_,_) -> let (_,_,_,cl) = List.nth itl i in let (_,cons) = List.nth cl (j - 1) in @@ -1393,7 +1393,7 @@ and type_of_aux' metasenv context t = (* let's check if the type of branches are right *) let parsno = - match CicEnvironment.get_cooked_obj uri with + match CicEnvironment.get_cooked_obj ~trust:false uri with C.InductiveDefinition (_,_,parsno) -> parsno | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) @@ -1504,7 +1504,7 @@ in if not res then prerr_endline ("#### " ^ CicPp.ppterm (type_of_aux context p) | ((uri,t) as subst)::tl -> let typeofvar = CicSubstitution.subst_vars substs (type_of_variable uri) in - (match CicEnvironment.get_cooked_obj uri with + (match CicEnvironment.get_cooked_obj ~trust:false uri with Cic.Variable (_,Some bo,_,_) -> raise (NotWellTyped @@ -1568,7 +1568,7 @@ in if not res then prerr_endline ("#### " ^ CicPp.ppterm (type_of_aux context p) match CicReduction.whd context ty with C.MutInd (uri,i,_) -> (*CSC: definire una funzioncina per questo codice sempre replicato *) - (match CicEnvironment.get_cooked_obj uri with + (match CicEnvironment.get_cooked_obj ~trust:false uri with C.InductiveDefinition (itl,_,_) -> let (_,is_inductive,_,_) = List.nth itl i in if is_inductive then None else (Some uri) @@ -1630,7 +1630,7 @@ let typecheck uri = let module C = Cic in let module R = CicReduction in let module U = UriManager in - match CicEnvironment.is_type_checked uri with + match CicEnvironment.is_type_checked ~trust:false uri with CicEnvironment.CheckedObj _ -> () | CicEnvironment.UncheckedObj uobj -> (* let's typecheck the uncooked object *) -- 2.39.2