X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicTypeChecker.ml;h=a494c4a690f519638efacbe63738446e9f100245;hb=95776c5fdf7a7609159450c8de92e71180cd90db;hp=57bc5e2ad3698be43ae6a93e77d45b0273d100bb;hpb=125a10b86b9caf857e49867e2c0d8b101e0b3752;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 57bc5e2ad..a494c4a69 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 *) @@ -1644,10 +1644,16 @@ let typecheck uri = (* only to check that ty is well-typed *) let _ = type_of ty in () | C.CurrentProof (_,conjs,te,ty,_) -> - (*CSC: bisogna controllare anche il metasenv!!! *) + let _ = + List.fold_left + (fun metasenv ((_,context,ty) as conj) -> + ignore (type_of_aux' metasenv context ty) ; + metasenv @ [conj] + ) [] conjs + in let _ = type_of_aux' conjs [] ty in - debug (type_of_aux' conjs [] te) [] ; - if not (R.are_convertible [] (type_of_aux' conjs [] te) ty) then + if not (R.are_convertible [] (type_of_aux' conjs [] te) ty) + then raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri))) | C.Variable (_,bo,ty,_) -> (* only to check that ty is well-typed *)