From 3ec1830d5251709ed6c4899c74903498a6cd2744 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 4 Apr 2008 13:10:22 +0000 Subject: [PATCH] type_of_constant was retunrning the type of the wrong constructor (-1 missing) fixpoints were not properly debruijnated before being checked better error message for match branches --- .../components/ng_kernel/nCicTypeChecker.ml | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index e0f6bbaed..81f633bb6 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -777,7 +777,8 @@ let rec typeof ~subst ~metasenv context term = let ty_p = typeof_aux context p in let ty_cons = typeof_aux context cons in let ty_branch = - type_of_branch ~subst context leftno outtype cons ty_cons 0 in + type_of_branch ~subst context leftno outtype cons ty_cons 0 + in j+1, R.are_convertible ~subst ~metasenv context ty_p ty_branch, ty_p, ty_branch else @@ -787,9 +788,10 @@ let rec typeof ~subst ~metasenv context term = if not branches_ok then raise (TypeCheckerFailure - (lazy (Printf.sprintf "Branch for constructor %s has type %s != %s" - (NCicPp.ppterm (C.Const - (Ref.Ref (dummy_depth, uri, Ref.Con (tyno, j))))) + (lazy (Printf.sprintf ("Branch for constructor %s :=\n%s\n"^^ + "has type %s\nnot convertible with %s") (NCicPp.ppterm (C.Const + (Ref.Ref (dummy_depth, uri, Ref.Con (tyno, j))))) + (NCicPp.ppterm ~context (List.nth pl (j-1))) (NCicPp.ppterm ~context p_ty) (NCicPp.ppterm ~context exp_p_ty)))); let res = outtype::arguments@[term] in R.head_beta_reduce (C.Appl res) @@ -1152,7 +1154,7 @@ and type_of_constant ((Ref.Ref (_,uri,_)) as ref) = let _,_,arity,_ = List.nth tl i in arity | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,_,Ref.Con (i,j)) -> let _,_,_,cl = List.nth tl i in - let _,_,arity = List.nth cl j in + let _,_,arity = List.nth cl (j-1) in arity | (_,_,_,_,C.Fixpoint (_,fl,_)), Ref.Ref (_,_,(Ref.Fix (i,_)|Ref.CoFix i)) -> let _,_,_,arity,_ = List.nth fl i in @@ -1182,6 +1184,7 @@ and check_obj_well_typed (uri,height,metasenv,subst,kind) = ) ([],[],0) fl in List.iter (fun (_,name,x,ty,bo) -> + let bo = debruijn uri len bo in let ty_bo = typeof ~subst ~metasenv types bo in if not (R.are_convertible ~subst ~metasenv types ty_bo (S.lift len ty)) then raise (TypeCheckerFailure (lazy ("(Co)Fix: ill-typed bodies"))) -- 2.39.2