From 90a9ceff7dc614e7be0b600fc6c820abd980595a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 8 Apr 2008 17:22:19 +0000 Subject: [PATCH] Improved error messages in place of "sort elimination not allowed". --- .../components/ng_kernel/nCicTypeChecker.ml | 59 +++++++++++-------- 1 file changed, 36 insertions(+), 23 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 125b66ed3..f1a99408a 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -719,9 +719,8 @@ let rec typeof ~subst ~metasenv context term = if parameters = [] then C.Const r else C.Appl ((C.Const r)::parameters) in let type_of_sort_of_ind_ty = typeof_aux context sort_of_ind_type in - if not (check_allowed_sort_elimination ~subst ~metasenv r context - sort_of_ind_type type_of_sort_of_ind_ty outsort) - then raise (TypeCheckerFailure (lazy ("Sort elimination not allowed"))); + check_allowed_sort_elimination ~subst ~metasenv r context + sort_of_ind_type type_of_sort_of_ind_ty outsort; (* let's check if the type of branches are right *) let leftno,constructorsno = let inductive,leftno,itl,_,i = E.get_checked_indtys r in @@ -904,27 +903,41 @@ let rec typeof ~subst ~metasenv context term = let arity2 = R.whd ~subst context arity2 in match arity1,arity2 with | C.Prod (name,so1,de1), C.Prod (_,so2,de2) -> - R.are_convertible ~subst ~metasenv context so1 so2 && - aux ((name, C.Decl so1)::context) - (mkapp (S.lift 1 ind) (C.Rel 1)) de1 de2 + if not (R.are_convertible ~subst ~metasenv context so1 so2) then + raise (TypeCheckerFailure (lazy (Printf.sprintf + "In outtype: expected %s, found %s" + (NCicPp.ppterm ~subst ~metasenv ~context so1) + (NCicPp.ppterm ~subst ~metasenv ~context so2) + ))); + aux ((name, C.Decl so1)::context) + (mkapp (S.lift 1 ind) (C.Rel 1)) de1 de2 | C.Sort _, C.Prod (name,so,ta) -> - (R.are_convertible ~subst ~metasenv context so ind && - match arity1,ta with - | (C.Sort (C.CProp | C.Type _), C.Sort _) - | (C.Sort C.Prop, C.Sort C.Prop) -> true - | (C.Sort C.Prop, C.Sort (C.CProp | C.Type _)) -> - let inductive,leftno,itl,_,i = E.get_checked_indtys r in - let itl_len = List.length itl in - let _,name,ty,cl = List.nth itl i in - let cl_len = List.length cl in - (* is it a singleton or empty non recursive and non informative - definition? *) - cl_len = 0 || - (itl_len = 1 && cl_len = 1 && - is_non_informative [name,C.Decl ty] leftno - (let _,_,x = List.nth cl 0 in x)) - | _,_ -> false) - | _,_ -> false + if not (R.are_convertible ~subst ~metasenv context so ind) then + raise (TypeCheckerFailure (lazy (Printf.sprintf + "In outtype: expected %s, found %s" + (NCicPp.ppterm ~subst ~metasenv ~context ind) + (NCicPp.ppterm ~subst ~metasenv ~context so) + ))); + (match arity1,ta with + | (C.Sort (C.CProp | C.Type _), C.Sort _) + | (C.Sort C.Prop, C.Sort C.Prop) -> () + | (C.Sort C.Prop, C.Sort (C.CProp | C.Type _)) -> + let inductive,leftno,itl,_,i = E.get_checked_indtys r in + let itl_len = List.length itl in + let _,name,ty,cl = List.nth itl i in + let cl_len = List.length cl in + (* is it a singleton or empty non recursive and non informative + definition? *) + if not + (cl_len = 0 || + (itl_len = 1 && cl_len = 1 && + is_non_informative [name,C.Decl ty] leftno + (let _,_,x = List.nth cl 0 in x))) + then + raise (TypeCheckerFailure (lazy + ("Sort elimination not allowed"))); + | _,_ -> ()) + | _,_ -> () in aux -- 2.39.2