X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicTypeChecker.ml;h=ee76389069b7456a89904c81e1728430476d7d91;hb=cb27dc85331027e290e3c4afc7ddef2e869cdfac;hp=cab4640c89ecb8d7e73cdd3c61d3fbe3af597375;hpb=218c0062f93dd3221b0266cfbc26fd9cf787ad18;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index cab4640c8..ee7638906 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -36,13 +36,13 @@ let debug t context = let rec debug_aux t i = let module C = Cic in let module U = UriManager in - CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i + CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i in if !fdebug = 0 then raise (TypeCheckerFailure (List.fold_right debug_aux (t::context) "")) ;; -let debug_print = prerr_endline ;; +let debug_print = fun _ -> () ;; let rec split l n = match (l,n) with @@ -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) @@ -136,7 +138,7 @@ let rec type_of_constant ~logger uri ugraph = let ugraph_dust = (match uobj with - C.Constant (_,Some te,ty,_) -> + C.Constant (_,Some te,ty,_,_) -> let _,ugraph = type_of ~logger ty ugraph in let type_of_te,ugraph' = type_of ~logger te ugraph in let b',ugraph'' = (R.are_convertible [] type_of_te ty ugraph') in @@ -147,11 +149,11 @@ let rec type_of_constant ~logger uri ugraph = (CicPp.ppterm ty))) else ugraph' - | C.Constant (_,None,ty,_) -> + | 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,_) -> + | C.CurrentProof (_,conjs,te,ty,_,_) -> let _,ugraph1 = List.fold_left (fun (metasenv,ugraph) ((_,context,ty) as conj) -> @@ -184,12 +186,12 @@ let rec type_of_constant ~logger uri ugraph = CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph' | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError with Invalid_argument s -> - (*prerr_endline s;*) + (*debug_print (lazy s);*) uobj,ugraph_dust in match cobj,ugraph with - (C.Constant (_,_,ty,_)),g -> ty,g - | (C.CurrentProof (_,_,_,ty,_)),g -> ty,g + (C.Constant (_,_,ty,_,_)),g -> ty,g + | (C.CurrentProof (_,_,_,ty,_,_)),g -> ty,g | _ -> raise (TypeCheckerFailure ("Unknown constant:" ^ U.string_of_uri uri)) @@ -199,8 +201,8 @@ and type_of_variable ~logger uri ugraph = let module U = UriManager in (* 0 because a variable is never cooked => no partial cooking at one level *) match CicEnvironment.is_type_checked ~trust:true ugraph uri with - CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_)),ugraph') -> ty,ugraph' - | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_)) -> + CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') -> ty,ugraph' + | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_,_)) -> logger#log (`Start_type_checking uri) ; (* only to check that ty is well-typed *) let _,ugraph1 = type_of ~logger ty ugraph in @@ -220,12 +222,12 @@ and type_of_variable ~logger uri ugraph = CicEnvironment.set_type_checking_info uri ; logger#log (`Type_checking_completed uri) ; match CicEnvironment.is_type_checked ~trust:false ugraph uri with - CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_)),ugraph') -> + CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') -> ty,ugraph' | CicEnvironment.CheckedObj _ | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError with Invalid_argument s -> - (*prerr_endline s;*) + (*debug_print (lazy s);*) ty,ugraph2) | _ -> raise (TypeCheckerFailure ("Unknown variable:" ^ U.string_of_uri uri)) @@ -406,7 +408,7 @@ and strictly_positive context n nn te = let (ok,paramsno,ity,cl,name) = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with - C.InductiveDefinition (tl,_,paramsno) -> + C.InductiveDefinition (tl,_,paramsno,_) -> let (name,_,ity,cl) = List.nth tl i in (List.length tl = 1, paramsno, ity, cl, name) | _ -> @@ -545,7 +547,7 @@ and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph = (* inductive block definition. *) and check_mutual_inductive_defs uri obj ugraph = match obj with - Cic.InductiveDefinition (itl, params, indparamsno) -> + Cic.InductiveDefinition (itl, params, indparamsno, _) -> typecheck_mutual_inductive_defs uri (itl,params,indparamsno) ugraph | _ -> raise (TypeCheckerFailure ( @@ -574,11 +576,11 @@ and type_of_mutual_inductive_defs ~logger uri i ugraph = ) with Invalid_argument s -> - (*prerr_endline s;*) + (*debug_print (lazy s);*) uobj,ugraph1_dust in match cobj with - C.InductiveDefinition (dl,_,_) -> + C.InductiveDefinition (dl,_,_,_) -> let (_,_,arity,_) = List.nth dl i in arity,ugraph1 | _ -> @@ -609,11 +611,11 @@ and type_of_mutual_inductive_constr ~logger uri i j ugraph = raise CicEnvironmentError) with Invalid_argument s -> - (*prerr_endline s;*) + (*debug_print (lazy s);*) uobj,ugraph1_dust in match cobj with - C.InductiveDefinition (dl,_,_) -> + C.InductiveDefinition (dl,_,_,_) -> let (_,_,_,cl) = List.nth dl i in let (_,ty) = List.nth cl (j-1) in ty,ugraph1 @@ -742,7 +744,7 @@ and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te = let (tys,len,isinductive,paramsno,cl) = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with - C.InductiveDefinition (tl,_,paramsno) -> + C.InductiveDefinition (tl,_,paramsno,_) -> let tys = List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl @@ -765,6 +767,13 @@ and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te = i && check_is_really_smaller_arg ~subst context n nn kl x safes p) pl true else + let pl_and_cl = + try + List.combine pl cl + with + Invalid_argument _ -> + raise (TypeCheckerFailure "not enough patterns") + in List.fold_right (fun (p,(_,c)) i -> let rl' = @@ -776,12 +785,12 @@ and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te = in i && check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e - ) (List.combine pl cl) true + ) pl_and_cl true | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x -> let (tys,len,isinductive,paramsno,cl) = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with - C.InductiveDefinition (tl,_,paramsno) -> + C.InductiveDefinition (tl,_,paramsno,_) -> let (_,isinductive,_,cl) = List.nth tl i in let tys = List.map (fun (n,_,ty,_) -> @@ -804,6 +813,13 @@ and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te = i && check_is_really_smaller_arg ~subst context n nn kl x safes p) pl true else + let pl_and_cl = + try + List.combine pl cl + with + Invalid_argument _ -> + raise (TypeCheckerFailure "not enough patterns") + in (*CSC: supponiamo come prima che nessun controllo sia necessario*) (*CSC: sugli argomenti di una applicazione *) List.fold_right @@ -817,7 +833,7 @@ and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te = in i && check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e - ) (List.combine pl cl) true + ) pl_and_cl true | _ -> List.fold_right (fun p i -> @@ -903,12 +919,12 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes = (fun (_,t) i -> i && guarded_by_destructors context n nn kl x safes t) exp_named_subst true | C.MutCase (uri,i,outtype,term,pl) -> - (match term with + (match CicReduction.whd context term with C.Rel m when List.mem m safes || m = x -> let (tys,len,isinductive,paramsno,cl) = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with - C.InductiveDefinition (tl,_,paramsno) -> + C.InductiveDefinition (tl,_,paramsno,_) -> let len = List.length tl in let (_,isinductive,_,cl) = List.nth tl i in let tys = @@ -938,6 +954,13 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes = i && guarded_by_destructors context n nn kl x safes p) pl true else + let pl_and_cl = + try + List.combine pl cl + with + Invalid_argument _ -> + raise (TypeCheckerFailure "not enough patterns") + in guarded_by_destructors context n nn kl x safes outtype && (*CSC: manca ??? il controllo sul tipo di term? *) List.fold_right @@ -948,12 +971,12 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes = in i && guarded_by_destructors context' n' nn' kl x' safes' e - ) (List.combine pl cl) true + ) pl_and_cl true | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x -> let (tys,len,isinductive,paramsno,cl) = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with - C.InductiveDefinition (tl,_,paramsno) -> + C.InductiveDefinition (tl,_,paramsno,_) -> let (_,isinductive,_,cl) = List.nth tl i in let tys = List.map @@ -979,6 +1002,13 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes = i && guarded_by_destructors context n nn kl x safes p) pl true else + let pl_and_cl = + try + List.combine pl cl + with + Invalid_argument _ -> + raise (TypeCheckerFailure "not enough patterns") + in guarded_by_destructors context n nn kl x safes outtype && (*CSC: manca ??? il controllo sul tipo di term? *) List.fold_right @@ -996,7 +1026,7 @@ and guarded_by_destructors ?(subst = []) context n nn kl x safes = in i && guarded_by_destructors context' n' nn' kl x' safes' e - ) (List.combine pl cl) true + ) pl_and_cl true | _ -> guarded_by_destructors context n nn kl x safes outtype && guarded_by_destructors context n nn kl x safes term && @@ -1068,7 +1098,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = with Not_found -> assert false in match obj with - C.InductiveDefinition (itl,_,_) -> + C.InductiveDefinition (itl,_,_,_) -> let (_,_,_,cl) = List.nth itl i in let (_,cons) = List.nth cl (j - 1) in CicSubstitution.subst_vars exp_named_subst cons @@ -1253,7 +1283,7 @@ and check_allowed_sort_elimination ~logger context uri i need_dummy ind (*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *) (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with - C.InductiveDefinition (itl,_,_) -> + C.InductiveDefinition (itl,_,_,_) -> let (_,_,_,cl) = List.nth itl i in (* is a singleton definition or the empty proposition? *) (List.length cl = 1 || List.length cl = 0) , ugraph @@ -1273,7 +1303,7 @@ and check_allowed_sort_elimination ~logger context uri i need_dummy ind when need_dummy -> (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with - C.InductiveDefinition (itl,_,paramsno) -> + C.InductiveDefinition (itl,_,paramsno,_) -> let tys = List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in @@ -1297,21 +1327,19 @@ and check_allowed_sort_elimination ~logger context uri i need_dummy ind false,ugraph1 else (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with - C.Sort C.Prop -> true,ugraph1 - | (C.Sort C.Set | C.Sort C.CProp) -> - (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with - C.InductiveDefinition (itl,_,_) -> - let (_,_,_,cl) = List.nth itl i in - (* is a singleton definition? *) - List.length cl = 1,ugraph1 - | _ -> - raise (TypeCheckerFailure - ("Unknown mutual inductive definition:" ^ - UriManager.string_of_uri uri)) - ) - | _ -> false,ugraph1 - ) + C.Sort C.Prop -> true,ugraph1 + | (C.Sort C.Set | C.Sort C.CProp | C.Sort (C.Type _)) -> + (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + match o with + C.InductiveDefinition (itl,_,_,_) -> + let (_,_,_,cl) = List.nth itl i in + (* is a singleton definition or the empty proposition? *) + (List.length cl = 1 || List.length cl = 0),ugraph1 + | _ -> + raise (TypeCheckerFailure + ("Unknown mutual inductive definition:" ^ + UriManager.string_of_uri uri))) + | _ -> false,ugraph1) | ((C.Sort C.Set, C.Prod (name,so,ta)) | (C.Sort C.CProp, C.Prod (name,so,ta))) when not need_dummy -> @@ -1327,7 +1355,7 @@ and check_allowed_sort_elimination ~logger context uri i need_dummy ind (* TASSI: da verificare *) (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with - C.InductiveDefinition (itl,_,paramsno) -> + C.InductiveDefinition (itl,_,paramsno,_) -> let (_,_,_,cl) = List.nth itl i in let tys = List.map @@ -1395,12 +1423,12 @@ and check_metasenv_consistency ~logger ?(subst=[]) metasenv context function [] -> [] | (Some (n,C.Decl t))::tl -> - (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl) + (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl) | (Some (n,C.Def (t,None)))::tl -> - (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl) + (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl) | None::tl -> None::(aux (i+1) tl) | (Some (n,C.Def (t,Some ty)))::tl -> - (Some (n,C.Def ((S.lift_meta l (S.lift i t)),Some (S.lift_meta l (S.lift i ty)))))::(aux (i+1) tl) + (Some (n,C.Def ((S.subst_meta l (S.lift i t)),Some (S.subst_meta l (S.lift i ty)))))::(aux (i+1) tl) in aux 1 canonical_context in @@ -1457,7 +1485,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = Some (_,C.Decl t) -> S.lift n t,ugraph | Some (_,C.Def (_,Some ty)) -> S.lift n ty,ugraph | Some (_,C.Def (bo,None)) -> - debug_print "##### CASO DA INVESTIGARE E CAPIRE" ; + debug_print (lazy "##### CASO DA INVESTIGARE E CAPIRE") ; type_of_aux ~logger context (S.lift n bo) ugraph | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis") @@ -1482,15 +1510,15 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = ~subst metasenv context canonical_context l ugraph in (* assuming subst is well typed !!!!! *) - ((CicSubstitution.lift_meta l ty), ugraph1) - (* type_of_aux context (CicSubstitution.lift_meta l term) *) + ((CicSubstitution.subst_meta l ty), ugraph1) + (* type_of_aux context (CicSubstitution.subst_meta l term) *) with CicUtil.Subst_not_found _ -> let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in let ugraph1 = check_metasenv_consistency ~logger ~subst metasenv context canonical_context l ugraph in - ((CicSubstitution.lift_meta l ty),ugraph1)) + ((CicSubstitution.subst_meta l ty),ugraph1)) (* TASSI: CONSTRAINTS *) | C.Sort (C.Type t) -> let t' = CicUniv.fresh() in @@ -1680,8 +1708,8 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = else raise (TypeCheckerFailure (sprintf - ("Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}") - (CicPp.ppterm typ) (U.string_of_uri uri) i)) + ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}") + (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i)) | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' -> if U.eq uri uri' && i = i' then @@ -1691,8 +1719,8 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = else raise (TypeCheckerFailure (sprintf - "Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}" - (CicPp.ppterm typ') (U.string_of_uri uri) i)) + ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}") + (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i)) | _ -> raise (TypeCheckerFailure @@ -1727,7 +1755,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = with Not_found -> assert false in match obj with - C.InductiveDefinition (_,_,parsno) -> parsno + C.InductiveDefinition (_,_,parsno,_) -> parsno | _ -> raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^ @@ -1755,9 +1783,9 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = ~subst ~metasenv context ty_p ty_branch ugraph3 in if not b1 then - debug_print + debug_print (lazy ("#### " ^ CicPp.ppterm ty_p ^ - " <==> " ^ CicPp.ppterm ty_branch); + " <==> " ^ CicPp.ppterm ty_branch)); (j + 1,b1,ugraph4) else (j,false,ugraph) @@ -1766,12 +1794,14 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = if not branches_ok then raise (TypeCheckerFailure "Case analysys: wrong branch type"); - if not need_dummy then - (C.Appl ((outtype::arguments)@[term])),ugraph5 - else if arguments = [] then - outtype,ugraph5 - else - (C.Appl (outtype::arguments)),ugraph5 + let arguments' = + if not need_dummy then outtype::arguments@[term] + else outtype::arguments in + let outtype = + if need_dummy && arguments = [] then outtype + else CicReduction.head_beta_reduce (C.Appl arguments') + in + outtype,ugraph5 | C.Fix (i,fl) -> let types_times_kl,ugraph1 = (* WAS: list rev list map *) @@ -1966,7 +1996,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = with Not_found -> assert false in (match obj with - C.InductiveDefinition (itl,_,_) -> + C.InductiveDefinition (itl,_,_,_) -> let (_,is_inductive,_,_) = List.nth itl i in if is_inductive then None else (Some uri) | _ -> @@ -1977,7 +2007,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = | C.Appl ((C.MutInd (uri,i,_))::_) -> (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in match o with - C.InductiveDefinition (itl,_,_) -> + C.InductiveDefinition (itl,_,_,_) -> let (_,is_inductive,_,_) = List.nth itl i in if is_inductive then None else (Some uri) | _ -> @@ -1991,12 +2021,12 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph = in (*CSC -debug_print ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t) ; flush stderr ; +debug_print (lazy ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t)) ; flush stderr ; let res = *) type_of_aux ~logger context t ugraph (* -in debug_print "FINE TYPE_OF_AUX" ; flush stderr ; res +in debug_print (lazy "FINE TYPE_OF_AUX") ; flush stderr ; res *) (* is a small constructor? *) @@ -2020,83 +2050,84 @@ and is_small ~logger context paramsno c ugraph = and type_of ~logger t ugraph = (*CSC -debug_print ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t) ; flush stderr ; +debug_print (lazy ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t)) ; flush stderr ; let res = *) type_of_aux' ~logger [] [] t ugraph (*CSC -in debug_print "FINE TYPE_OF_AUX'" ; flush stderr ; res +in debug_print (lazy "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') -> - (* prerr_endline ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri);*) + (* debug_print (lazy ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri));*) cobj,ugraph' | CicEnvironment.UncheckedObj uobj -> (* let's typecheck the uncooked object *) logger#log (`Start_type_checking uri) ; - (* prerr_endline ("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 + (* debug_print (lazy ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri)); *) + let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph uobj in try CicEnvironment.set_type_checking_info uri; logger#log (`Type_checking_completed uri); @@ -2111,17 +2142,22 @@ let typecheck uri ugraph = object. *) Invalid_argument s -> - (*prerr_endline s;*) - uobj,ugraph1 + (*debug_print (lazy s);*) + uobj,ugraph ;; +let typecheck_obj ~logger uri obj = + let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph obj in + let ugraph, univlist = CicUnivUtils.clean_and_fill uri obj ugraph in + CicEnvironment.add_type_checked_obj uri (obj,ugraph,univlist) + (** wrappers which instantiate fresh loggers *) -let type_of_aux' ?(subst = []) metasenv context t = +let type_of_aux' ?(subst = []) metasenv context t ugraph = let logger = new CicLogger.logger in - type_of_aux' ~logger ~subst metasenv context t + 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