From bba3b7f83610c3babb797e8ce1e844a560303295 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 18 May 2008 17:49:57 +0000 Subject: [PATCH] New missing check implemented: the left parameters of each constructor and inductive types should be convertible and should have the very same name. --- .../components/ng_kernel/nCicTypeChecker.ml | 25 +++++++++++++++++-- 1 file changed, 23 insertions(+), 2 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index bccf753f2..21da67bb8 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -712,12 +712,33 @@ and check_mutual_inductive_defs uri ~metasenv ~subst is_ind leftno tyl = ignore (List.fold_right (fun (_,_,ty,cl) i -> - let _,ty_sort = split_prods ~subst [] ~-1 ty in + let sx_context_ty,ty_sort = split_prods ~subst [] ~-1 ty in List.iter (fun (_,name,te) -> -(*CSC: assicurarmi che i sx siano esattamente gli stessi! *) let te = debruijn uri len [] te in let context,te = split_prods ~subst tys leftno te in + let sx_context_te,_ = HExtlib.split_nth leftno context in + (try + ignore (List.fold_right2 + (fun item1 item2 context -> + let convertible = + match item1,item2 with + (n1,C.Decl ty1),(n2,C.Decl ty2) -> + n1 = n2 && R.are_convertible ~subst context ty1 ty2 + | (n1,C.Def (bo1,ty1)),(n2,C.Def (bo2,ty2)) -> + n1 = n2 + && R.are_convertible ~subst context ty1 ty2 + && R.are_convertible ~subst context bo1 bo2 + | _,_ -> false + in + if not convertible then + raise (TypeCheckerFailure (lazy + ("Mismatch between the left parameters of the constructor " ^ + "and those of its inductive type"))) + else + item1::context + ) sx_context_ty sx_context_te []) + with Invalid_argument _ -> assert false); let con_sort = typeof ~subst ~metasenv context te in (match R.whd ~subst context con_sort, R.whd ~subst [] ty_sort with (C.Sort (C.Type u1) as s1), (C.Sort (C.Type u2) as s2) -> -- 2.39.2