X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicTypeChecker.ml;h=1db82a99fb48eeddcf63adb96c4a31575e2ca5e6;hb=358cefe50cccd4cb7d8e2a9cecb7efcb5780b8a3;hp=6789c4dff8213acdf53d18aef9b286c0bd46744f;hpb=53ee2f5095adadffcafb40e436d23dc330d3bd87;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 6789c4dff..1db82a99f 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -64,7 +64,9 @@ let debrujin_constructor uri number_of_types = List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst in C.Var (uri,exp_named_subst') - | C.Meta _ -> assert false + | C.Meta (i,l) -> + let l' = List.map (function None -> None | Some t -> Some (aux k t)) l in + C.Meta (i,l) | C.Sort _ | C.Implicit _ as t -> t | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) @@ -2031,13 +2033,67 @@ in debug_print "FINE TYPE_OF_AUX'" ; flush stderr ; res *) ;; -let typecheck uri ugraph = +let typecheck_obj0 ~logger uri ugraph = + let module C = Cic in + function + C.Constant (_,Some te,ty,_,_) -> + let _,ugraph = type_of ~logger ty ugraph in + let ty_te,ugraph = type_of ~logger te ugraph in + let b,ugraph = (CicReduction.are_convertible [] ty_te ty ugraph) in + if not b then + raise (TypeCheckerFailure + ("the type of the body is not the one expected")) + else + ugraph + | C.Constant (_,None,ty,_,_) -> + (* only to check that ty is well-typed *) + let _,ugraph = type_of ~logger ty ugraph in + ugraph + | C.CurrentProof (_,conjs,te,ty,_,_) -> + let _,ugraph = + List.fold_left + (fun (metasenv,ugraph) ((_,context,ty) as conj) -> + let _,ugraph = + type_of_aux' ~logger metasenv context ty ugraph + in + metasenv @ [conj],ugraph + ) ([],ugraph) conjs + in + let _,ugraph = type_of_aux' ~logger conjs [] ty ugraph in + let type_of_te,ugraph = + type_of_aux' ~logger conjs [] te ugraph + in + let b,ugraph = CicReduction.are_convertible [] type_of_te ty ugraph in + if not b then + raise (TypeCheckerFailure (sprintf + "the current proof is not well typed because the type %s of the body is not convertible to the declared type %s" + (CicPp.ppterm type_of_te) (CicPp.ppterm ty))) + else + ugraph + | C.Variable (_,bo,ty,_,_) -> + (* only to check that ty is well-typed *) + let _,ugraph = type_of ~logger ty ugraph in + (match bo with + None -> ugraph + | Some bo -> + let ty_bo,ugraph = type_of ~logger bo ugraph in + let b,ugraph = CicReduction.are_convertible [] ty_bo ty ugraph in + if not b then + raise (TypeCheckerFailure + ("the body is not the one expected")) + else + ugraph + ) + | (C.InductiveDefinition _ as obj) -> + check_mutual_inductive_defs ~logger uri obj ugraph + +let typecheck uri = let module C = Cic in let module R = CicReduction in let module U = UriManager in let logger = new CicLogger.logger in (* ??? match CicEnvironment.is_type_checked ~trust:true uri with ???? *) - match CicEnvironment.is_type_checked ~trust:false ugraph uri with + match CicEnvironment.is_type_checked ~trust:false CicUniv.empty_ugraph uri with CicEnvironment.CheckedObj (cobj,ugraph') -> (* debug_print ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri);*) cobj,ugraph' @@ -2045,60 +2101,7 @@ let typecheck uri ugraph = (* let's typecheck the uncooked object *) logger#log (`Start_type_checking uri) ; (* debug_print ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri); *) - let ugraph1 = - (match uobj with - C.Constant (_,Some te,ty,_,_) -> - let _,ugraph1 = type_of ~logger ty ugraph in - let ty_te,ugraph2 = type_of ~logger te ugraph1 in - let b,ugraph3 = (R.are_convertible [] ty_te ty ugraph2) in - if not b then - raise (TypeCheckerFailure - ("Unknown constant:" ^ U.string_of_uri uri)) - else - ugraph3 - | C.Constant (_,None,ty,_,_) -> - (* only to check that ty is well-typed *) - let _,ugraph1 = type_of ~logger ty ugraph in - ugraph1 - | C.CurrentProof (_,conjs,te,ty,_,_) -> - let _,ugraph1 = - List.fold_left - (fun (metasenv,ugraph) ((_,context,ty) as conj) -> - let _,ugraph1 = - type_of_aux' ~logger metasenv context ty ugraph - in - metasenv @ [conj],ugraph1 - ) ([],ugraph) conjs - in - let _,ugraph2 = type_of_aux' ~logger conjs [] ty ugraph1 in - let type_of_te,ugraph3 = - type_of_aux' ~logger conjs [] te ugraph2 - in - let b,ugraph4 = R.are_convertible [] type_of_te ty ugraph3 in - if not b then - raise (TypeCheckerFailure (sprintf - "the current proof %s is not well typed because the type %s of the body is not convertible to the declared type %s" - (U.string_of_uri uri) (CicPp.ppterm type_of_te) - (CicPp.ppterm ty))) - else - ugraph4 - | C.Variable (_,bo,ty,_,_) -> - (* only to check that ty is well-typed *) - let _,ugraph1 = type_of ~logger ty ugraph in - (match bo with - None -> ugraph1 - | Some bo -> - let ty_bo,ugraph2 = type_of ~logger bo ugraph1 in - let b,ugraph3 = R.are_convertible [] ty_bo ty ugraph2 in - if not b then - raise (TypeCheckerFailure - ("Unknown variable:" ^ U.string_of_uri uri)) - else - ugraph3 - ) - | C.InductiveDefinition _ -> - check_mutual_inductive_defs ~logger uri uobj ugraph - ) in + let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph uobj in try CicEnvironment.set_type_checking_info uri; logger#log (`Type_checking_completed uri); @@ -2114,16 +2117,20 @@ let typecheck uri ugraph = *) Invalid_argument s -> (*debug_print s;*) - uobj,ugraph1 + uobj,ugraph ;; +let typecheck_obj ~logger uri obj = + let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph obj in + let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in + CicEnvironment.add_type_checked_obj uri (obj,ugraph) + (** wrappers which instantiate fresh loggers *) let type_of_aux' ?(subst = []) metasenv context t ugraph = let logger = new CicLogger.logger in type_of_aux' ~logger ~subst metasenv context t ugraph -let typecheck_mutual_inductive_defs uri (itl, uris, indparamsno) = - let logger = new CicLogger.logger in - typecheck_mutual_inductive_defs ~logger uri (itl, uris, indparamsno) - +let typecheck_obj uri obj = + let logger = new CicLogger.logger in + typecheck_obj ~logger uri obj