From 61370f56adef637d71b1709b53140ba8785b3b53 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 18 Nov 2004 16:47:28 +0000 Subject: [PATCH] use stateful logger so that the ProofChecker daemon is able to properly indent proof checking messages --- .../cic_proof_checking/cicTypeChecker.ml | 188 ++++++++++-------- 1 file changed, 101 insertions(+), 87 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index 414d0b976..5d3d40a10 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -118,7 +118,7 @@ let debrujin_constructor uri number_of_types = exception CicEnvironmentError;; -let rec type_of_constant uri = +let rec type_of_constant ~logger uri = let module C = Cic in let module R = CicReduction in let module U = UriManager in @@ -126,13 +126,13 @@ let rec type_of_constant uri = match CicEnvironment.is_type_checked ~trust:true uri with CicEnvironment.CheckedObj cobj -> cobj | CicEnvironment.UncheckedObj uobj -> - CicLogger.log (`Start_type_checking uri) ; + logger#log (`Start_type_checking uri) ; CicUniv.directly_to_env_begin (); (* let's typecheck the uncooked obj *) (match uobj with C.Constant (_,Some te,ty,_) -> - let _ = type_of ty in - let type_of_te = type_of te in + let _ = type_of ~logger ty in + let type_of_te = type_of ~logger te in if not (R.are_convertible [] type_of_te ty) then raise (TypeCheckerFailure (sprintf "the constant %s is not well typed because the type %s of the body is not convertible to the declared type %s" @@ -145,12 +145,12 @@ let rec type_of_constant uri = let _ = List.fold_left (fun metasenv ((_,context,ty) as conj) -> - ignore (type_of_aux' metasenv context ty) ; + ignore (type_of_aux' ~logger metasenv context ty) ; metasenv @ [conj] ) [] conjs in - let _ = type_of_aux' conjs [] ty in - let type_of_te = type_of_aux' conjs [] te in + let _ = type_of_aux' ~logger conjs [] ty in + let type_of_te = type_of_aux' ~logger conjs [] te in if not (R.are_convertible [] type_of_te ty) 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" @@ -162,7 +162,7 @@ let rec type_of_constant uri = ); CicEnvironment.set_type_checking_info uri ; CicUniv.directly_to_env_end (); - CicLogger.log (`Type_checking_completed uri) ; + logger#log (`Type_checking_completed uri) ; match CicEnvironment.is_type_checked ~trust:false uri with CicEnvironment.CheckedObj cobj -> cobj | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError @@ -173,7 +173,7 @@ let rec type_of_constant uri = | _ -> raise (TypeCheckerFailure ("Unknown constant:" ^ U.string_of_uri uri)) -and type_of_variable uri = +and type_of_variable ~logger uri = let module C = Cic in let module R = CicReduction in let module U = UriManager in @@ -181,20 +181,20 @@ and type_of_variable uri = match CicEnvironment.is_type_checked ~trust:true uri with CicEnvironment.CheckedObj (C.Variable (_,_,ty,_)) -> ty | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_)) -> - CicLogger.log (`Start_type_checking uri) ; + logger#log (`Start_type_checking uri) ; CicUniv.directly_to_env_begin (); (* only to check that ty is well-typed *) let _ = type_of ty in (match bo with None -> () | Some bo -> - if not (R.are_convertible [] (type_of bo) ty) then + if not (R.are_convertible [] (type_of ~logger bo) ty) then raise (TypeCheckerFailure ("Unknown variable:" ^ U.string_of_uri uri)) ) ; CicEnvironment.set_type_checking_info uri ; CicUniv.directly_to_env_end (); - CicLogger.log (`Type_checking_completed uri) ; + logger#log (`Type_checking_completed uri) ; ty | _ -> raise (TypeCheckerFailure ("Unknown variable:" ^ U.string_of_uri uri)) @@ -462,11 +462,11 @@ and are_all_occurrences_positive context uri indparamsno i n nn te = (* Main function to checks the correctness of a mutual *) (* inductive block definition. This is the function *) (* exported to the proof-engine. *) -and typecheck_mutual_inductive_defs uri (itl,_,indparamsno) = +and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) = let module U = UriManager in (* let's check if the arity of the inductive types are well *) (* formed *) - List.iter (fun (_,_,x,_) -> let _ = type_of x in ()) itl ; + List.iter (fun (_,_,x,_) -> let _ = type_of ~logger x in ()) itl ; (* let's check if the types of the inductive constructors *) (* are well formed. *) @@ -513,7 +513,7 @@ and check_mutual_inductive_defs uri = raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri)) -and type_of_mutual_inductive_defs uri i = +and type_of_mutual_inductive_defs ~logger uri i = let module C = Cic in let module R = CicReduction in let module U = UriManager in @@ -521,12 +521,12 @@ and type_of_mutual_inductive_defs uri i = match CicEnvironment.is_type_checked ~trust:true uri with CicEnvironment.CheckedObj cobj -> cobj | CicEnvironment.UncheckedObj uobj -> - CicLogger.log (`Start_type_checking uri) ; + logger#log (`Start_type_checking uri) ; CicUniv.directly_to_env_begin (); - check_mutual_inductive_defs uri uobj ; + check_mutual_inductive_defs ~logger uri uobj ; CicEnvironment.set_type_checking_info uri ; CicUniv.directly_to_env_end (); - CicLogger.log (`Type_checking_completed uri) ; + logger#log (`Type_checking_completed uri) ; (match CicEnvironment.is_type_checked ~trust:false uri with CicEnvironment.CheckedObj cobj -> cobj | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError @@ -540,7 +540,7 @@ and type_of_mutual_inductive_defs uri i = raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^ U.string_of_uri uri)) -and type_of_mutual_inductive_constr uri i j = +and type_of_mutual_inductive_constr ~logger uri i j = let module C = Cic in let module R = CicReduction in let module U = UriManager in @@ -548,12 +548,12 @@ and type_of_mutual_inductive_constr uri i j = match CicEnvironment.is_type_checked ~trust:true uri with CicEnvironment.CheckedObj cobj -> cobj | CicEnvironment.UncheckedObj uobj -> - CicLogger.log (`Start_type_checking uri) ; + logger#log (`Start_type_checking uri) ; (*CicUniv.directly_to_env_begin ();*) - check_mutual_inductive_defs uri uobj ; + check_mutual_inductive_defs ~logger uri uobj ; CicEnvironment.set_type_checking_info uri ; (*CicUniv.directly_to_env_end ();*) - CicLogger.log (`Type_checking_completed uri) ; + logger#log (`Type_checking_completed uri) ; (match CicEnvironment.is_type_checked ~trust:false uri with CicEnvironment.CheckedObj cobj -> cobj | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError @@ -1171,13 +1171,13 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI = args coInductiveTypeURI ) fl true -and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 = +and check_allowed_sort_elimination ~logger context uri i need_dummy ind arity1 arity2 = let module C = Cic in let module U = UriManager in match (CicReduction.whd context arity1, CicReduction.whd context arity2) with (C.Prod (_,so1,de1), C.Prod (_,so2,de2)) when CicReduction.are_convertible context so1 so2 -> - check_allowed_sort_elimination context uri i need_dummy + check_allowed_sort_elimination ~logger context uri i need_dummy (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2 | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true | (C.Sort C.Prop, C.Sort C.Set) @@ -1210,7 +1210,7 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 = in let (_,_,_,cl) = List.nth itl i in List.fold_right - (fun (_,x) i -> i && is_small tys paramsno x) cl true + (fun (_,x) i -> i && is_small ~logger tys paramsno x) cl true | _ -> raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri)) @@ -1255,7 +1255,7 @@ and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 = (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in List.fold_right - (fun (_,x) i -> i && is_small tys paramsno x) cl true + (fun (_,x) i -> i && is_small ~logger tys paramsno x) cl true | _ -> raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^ @@ -1299,7 +1299,9 @@ and type_of_branch context argsno need_dummy outtype term constype = metavariable is consitent - up to relocation via the relocation list l - with the actual context *) -and check_metasenv_consistency ?(subst=[]) metasenv context canonical_context l = +and check_metasenv_consistency ~logger ?(subst=[]) metasenv context + canonical_context l += let module C = Cic in let module R = CicReduction in let module S = CicSubstitution in @@ -1327,7 +1329,7 @@ and check_metasenv_consistency ?(subst=[]) metasenv context canonical_context l "Not well typed metavariable local context: expected a term convertible with %s, found %s" (CicPp.ppterm ct) (CicPp.ppterm t))) | Some t,Some (_,C.Decl ct) -> - let type_t = type_of_aux' ~subst metasenv context t in + let type_t = type_of_aux' ~logger ~subst metasenv context t in if not (R.are_convertible ~subst ~metasenv context type_t ct) then (* debug *) raise (TypeCheckerFailure (sprintf @@ -1339,8 +1341,8 @@ and check_metasenv_consistency ?(subst=[]) metasenv context canonical_context l ) l lifted_canonical_context (* type_of_aux' is just another name (with a different scope) for type_of_aux *) -and type_of_aux' ?(subst = []) metasenv context t = - let rec type_of_aux context = +and type_of_aux' ~logger ?(subst = []) metasenv context t = + let rec type_of_aux ~logger context = let module C = Cic in let module R = CicReduction in let module S = CicSubstitution in @@ -1353,7 +1355,7 @@ and type_of_aux' ?(subst = []) metasenv context t = | Some (_,C.Def (_,Some ty)) -> S.lift n ty | Some (_,C.Def (bo,None)) -> debug_print "##### CASO DA INVESTIGARE E CAPIRE" ; - type_of_aux context (S.lift n bo) + type_of_aux ~logger context (S.lift n bo) | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis") with _ -> @@ -1361,23 +1363,23 @@ and type_of_aux' ?(subst = []) metasenv context t = ) | C.Var (uri,exp_named_subst) -> incr fdebug ; - check_exp_named_subst ~subst context exp_named_subst ; + check_exp_named_subst ~logger ~subst context exp_named_subst ; let ty = - CicSubstitution.subst_vars exp_named_subst (type_of_variable uri) + CicSubstitution.subst_vars exp_named_subst (type_of_variable ~logger uri) in decr fdebug ; ty | C.Meta (n,l) -> (try let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in - check_metasenv_consistency + check_metasenv_consistency ~logger ~subst metasenv context canonical_context l; (* assuming subst is well typed !!!!! *) CicSubstitution.lift_meta l ty (* type_of_aux context (CicSubstitution.lift_meta l term) *) with CicUtil.Subst_not_found _ -> let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in - check_metasenv_consistency + check_metasenv_consistency ~logger ~subst metasenv context canonical_context l; CicSubstitution.lift_meta l ty) (* TASSI: CONSTRAINTS *) @@ -1391,19 +1393,19 @@ and type_of_aux' ?(subst = []) metasenv context t = | C.Sort s -> C.Sort (C.Type (CicUniv.fresh ())) | C.Implicit _ -> raise (AssertFailure "21") | C.Cast (te,ty) as t -> - let _ = type_of_aux context ty in - if R.are_convertible ~subst ~metasenv context (type_of_aux context te) ty then + let _ = type_of_aux ~logger context ty in + if R.are_convertible ~subst ~metasenv context (type_of_aux ~logger context te) ty then ty else raise (TypeCheckerFailure (sprintf "Invalid cast %s" (CicPp.ppterm t))) | C.Prod (name,s,t) -> - let sort1 = type_of_aux context s - and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in + let sort1 = type_of_aux ~logger context s + and sort2 = type_of_aux ~logger ((Some (name,(C.Decl s)))::context) t in let res = sort_of_prod ~subst context (name,s) (sort1,sort2) in res | C.Lambda (n,s,t) -> - let sort1 = type_of_aux context s in + let sort1 = type_of_aux ~logger context s in (match R.whd ~subst context sort1 with C.Meta _ | C.Sort _ -> () @@ -1414,11 +1416,11 @@ and type_of_aux' ?(subst = []) metasenv context t = type; instead it is a term of type %s" (CicPp.ppterm s) (CicPp.ppterm sort1))) ) ; - let type2 = type_of_aux ((Some (n,(C.Decl s)))::context) t in + let type2 = type_of_aux ~logger ((Some (n,(C.Decl s)))::context) t in C.Prod (n,s,type2) | C.LetIn (n,s,t) -> (* only to check if s is well-typed *) - let ty = type_of_aux context s in + let ty = type_of_aux ~logger context s in (* The type of a LetIn is a LetIn. Extremely slow since the computed LetIn is later reduced and maybe also re-checked. (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)) @@ -1432,38 +1434,38 @@ and type_of_aux' ?(subst = []) metasenv context t = (* One-step LetIn reduction. Even faster than the previous solution. Moreover the inferred type is closer to the expected one. *) (CicSubstitution.subst s - (type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t)) + (type_of_aux ~logger ((Some (n,(C.Def (s,Some ty))))::context) t)) | C.Appl (he::tl) when List.length tl > 0 -> - let hetype = type_of_aux context he in - let tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in + let hetype = type_of_aux ~logger context he in + let tlbody_and_type = List.map (fun x -> (x, type_of_aux ~logger context x)) tl in eat_prods ~subst context hetype tlbody_and_type | C.Appl _ -> raise (AssertFailure "Appl: no arguments") | C.Const (uri,exp_named_subst) -> incr fdebug ; - check_exp_named_subst ~subst context exp_named_subst ; + check_exp_named_subst ~logger ~subst context exp_named_subst ; let cty = - CicSubstitution.subst_vars exp_named_subst (type_of_constant uri) + CicSubstitution.subst_vars exp_named_subst (type_of_constant ~logger uri) in decr fdebug ; cty | C.MutInd (uri,i,exp_named_subst) -> incr fdebug ; - check_exp_named_subst ~subst context exp_named_subst ; + check_exp_named_subst ~logger ~subst context exp_named_subst ; let cty = CicSubstitution.subst_vars exp_named_subst - (type_of_mutual_inductive_defs uri i) + (type_of_mutual_inductive_defs ~logger uri i) in decr fdebug ; cty | C.MutConstruct (uri,i,j,exp_named_subst) -> - check_exp_named_subst ~subst context exp_named_subst ; + check_exp_named_subst ~logger ~subst context exp_named_subst ; let cty = CicSubstitution.subst_vars exp_named_subst - (type_of_mutual_inductive_constr uri i j) + (type_of_mutual_inductive_constr ~logger uri i j) in cty | C.MutCase (uri,i,outtype,term,pl) -> - let outsort = type_of_aux context outtype in + let outsort = type_of_aux ~logger context outtype in let (need_dummy, k) = let rec guess_args context t = let outtype = CicReduction.whd ~subst context t in @@ -1494,7 +1496,7 @@ and type_of_aux' ?(subst = []) metasenv context t = let (b, k) = guess_args context outsort in if not b then (b, k - 1) else (b, k) in let (parameters, arguments, exp_named_subst) = - match R.whd ~subst context (type_of_aux context term) with + match R.whd ~subst context (type_of_aux ~logger context term) with C.MutInd (uri',i',exp_named_subst) as typ -> if U.eq uri uri' && i = i' then ([],[],exp_named_subst) else raise @@ -1528,8 +1530,8 @@ and type_of_aux' ?(subst = []) metasenv context t = else C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters) in if not - (check_allowed_sort_elimination context uri i need_dummy - sort_of_ind_type (type_of_aux context sort_of_ind_type) outsort) + (check_allowed_sort_elimination ~logger context uri i need_dummy + sort_of_ind_type (type_of_aux ~logger context sort_of_ind_type) outsort) then raise (TypeCheckerFailure ("Case analasys: sort elimination not allowed")); @@ -1555,11 +1557,11 @@ and type_of_aux' ?(subst = []) metasenv context t = let res = b && R.are_convertible - ~subst ~metasenv context (type_of_aux context p) + ~subst ~metasenv context (type_of_aux ~logger context p) (type_of_branch context parsno need_dummy outtype cons - (type_of_aux context cons)) in + (type_of_aux ~logger context cons)) in if not res then - debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^ " <==> " ^ CicPp.ppterm (type_of_branch context parsno need_dummy outtype cons (type_of_aux context cons))) ; res + debug_print ("#### " ^ CicPp.ppterm (type_of_aux ~logger context p) ^ " <==> " ^ CicPp.ppterm (type_of_branch context parsno need_dummy outtype cons (type_of_aux ~logger context cons))) ; res ) ) (1,true) pl in @@ -1577,7 +1579,7 @@ and type_of_aux' ?(subst = []) metasenv context t = List.rev (List.map (fun (n,k,ty,_) -> - let _ = type_of_aux context ty in + let _ = type_of_aux ~logger context ty in (Some (C.Name n,(C.Decl ty)),k)) fl) in let (types,kl) = List.split types_times_kl in @@ -1586,7 +1588,7 @@ and type_of_aux' ?(subst = []) metasenv context t = (fun (name,x,ty,bo) -> if (R.are_convertible - ~subst ~metasenv (types@context) (type_of_aux (types@context) bo) + ~subst ~metasenv (types@context) (type_of_aux ~logger (types@context) bo) (CicSubstitution.lift len ty)) then begin @@ -1611,7 +1613,7 @@ and type_of_aux' ?(subst = []) metasenv context t = List.rev (List.map (fun (n,ty,_) -> - let _ = type_of_aux context ty in Some (C.Name n,(C.Decl ty))) fl) + let _ = type_of_aux ~logger context ty in Some (C.Name n,(C.Decl ty))) fl) in let len = List.length types in List.iter @@ -1619,7 +1621,7 @@ and type_of_aux' ?(subst = []) metasenv context t = if (R.are_convertible ~subst ~metasenv (types @ context) - (type_of_aux (types @ context) bo) (CicSubstitution.lift len ty)) + (type_of_aux ~logger (types @ context) bo) (CicSubstitution.lift len ty)) then begin (* let's control that the returned type is coinductive *) @@ -1645,17 +1647,17 @@ and type_of_aux' ?(subst = []) metasenv context t = let (_,ty,_) = List.nth fl i in ty - and check_exp_named_subst ?(subst = []) context = - let rec check_exp_named_subst_aux esubsts = + and check_exp_named_subst ~logger ?(subst = []) context = + let rec check_exp_named_subst_aux ~logger esubsts = function [] -> () | ((uri,t) as item)::tl -> let typeofvar = - CicSubstitution.subst_vars esubsts (type_of_variable uri) in - let typeoft = type_of_aux context t in + CicSubstitution.subst_vars esubsts (type_of_variable ~logger uri) in + let typeoft = type_of_aux ~logger context t in if CicReduction.are_convertible ~subst ~metasenv context typeoft typeofvar then - check_exp_named_subst_aux (esubsts@[item]) tl + check_exp_named_subst_aux ~logger (esubsts@[item]) tl else begin CicReduction.fdebug := 0 ; @@ -1665,7 +1667,7 @@ and type_of_aux' ?(subst = []) metasenv context t = raise (TypeCheckerFailure "Wrong Explicit Named Substitution") end in - check_exp_named_subst_aux [] + check_exp_named_subst_aux ~logger [] and sort_of_prod ?(subst = []) context (name,s) (t1, t2) = let module C = Cic in @@ -1753,33 +1755,33 @@ and type_of_aux' ?(subst = []) metasenv context t = debug_print ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t) ; flush stderr ; let res = *) - type_of_aux context t + type_of_aux ~logger context t (* in debug_print "FINE TYPE_OF_AUX" ; flush stderr ; res *) (* is a small constructor? *) (*CSC: ottimizzare calcolando staticamente *) -and is_small context paramsno c = - let rec is_small_aux context c = +and is_small ~logger context paramsno c = + let rec is_small_aux ~logger context c = let module C = Cic in match CicReduction.whd context c with C.Prod (n,so,de) -> (*CSC: [] is an empty metasenv. Is it correct? *) - let s = type_of_aux' [] context so in + let s = type_of_aux' ~logger [] context so in (s = C.Sort C.Prop || s = C.Sort C.Set || s = C.Sort C.CProp) && - is_small_aux ((Some (n,(C.Decl so)))::context) de + is_small_aux ~logger ((Some (n,(C.Decl so)))::context) de | _ -> true (*CSC: we trust the type-checker *) in let (context',dx) = split_prods context paramsno c in - is_small_aux context' dx + is_small_aux ~logger context' dx -and type_of t = +and type_of ~logger t = (*CSC debug_print ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t) ; flush stderr ; let res = *) - type_of_aux' [] [] t + type_of_aux' ~logger [] [] t (*CSC in debug_print "FINE TYPE_OF_AUX'" ; flush stderr ; res *) @@ -1790,32 +1792,33 @@ 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:false uri with*) match CicEnvironment.is_type_checked ~trust:true uri with CicEnvironment.CheckedObj cobj -> cobj | CicEnvironment.UncheckedObj uobj -> (* let's typecheck the uncooked object *) - CicLogger.log (`Start_type_checking uri) ; + logger#log (`Start_type_checking uri) ; CicUniv.directly_to_env_begin (); (match uobj with C.Constant (_,Some te,ty,_) -> - let _ = type_of ty in - if not (R.are_convertible [] (type_of te ) ty) then + let _ = type_of ~logger ty in + if not (R.are_convertible [] (type_of ~logger te ) ty) then raise (TypeCheckerFailure ("Unknown constant:" ^ U.string_of_uri uri)) | C.Constant (_,None,ty,_) -> (* only to check that ty is well-typed *) - let _ = type_of ty in () + let _ = type_of ~logger ty in () | C.CurrentProof (_,conjs,te,ty,_) -> let _ = List.fold_left (fun metasenv ((_,context,ty) as conj) -> - ignore (type_of_aux' metasenv context ty) ; + ignore (type_of_aux' ~logger metasenv context ty) ; metasenv @ [conj] ) [] conjs in - let _ = type_of_aux' conjs [] ty in - let type_of_te = type_of_aux' conjs [] te in + let _ = type_of_aux' ~logger conjs [] ty in + let type_of_te = type_of_aux' ~logger conjs [] te in if not (R.are_convertible [] type_of_te ty) then raise (TypeCheckerFailure (sprintf @@ -1824,19 +1827,30 @@ let typecheck uri = (CicPp.ppterm ty))) | C.Variable (_,bo,ty,_) -> (* only to check that ty is well-typed *) - let _ = type_of ty in + let _ = type_of ~logger ty in (match bo with None -> () | Some bo -> - if not (R.are_convertible [] (type_of bo) ty) then + if not (R.are_convertible [] (type_of ~logger bo) ty) then raise (TypeCheckerFailure ("Unknown variable:" ^ U.string_of_uri uri)) ) | C.InductiveDefinition _ -> - check_mutual_inductive_defs uri uobj + check_mutual_inductive_defs ~logger uri uobj ) ; CicEnvironment.set_type_checking_info uri ; CicUniv.directly_to_env_end (); - CicLogger.log (`Type_checking_completed uri); + logger#log (`Type_checking_completed uri); uobj ;; + +(** wrappers which instantiate fresh loggers *) + +let type_of_aux' ?(subst = []) metasenv context t = + let logger = new CicLogger.logger in + type_of_aux' ~logger metasenv context t + +let typecheck_mutual_inductive_defs uri (itl, uris, indparamsno) = + let logger = new CicLogger.logger in + typecheck_mutual_inductive_defs ~logger uri (itl, uris, indparamsno) + -- 2.39.2