From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 18 May 2008 17:49:57 +0000 (+0000)
Subject: New missing check implemented: the left parameters of each constructor and
X-Git-Tag: make_still_working~5167
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bba3b7f83610c3babb797e8ce1e844a560303295;p=helm.git

New missing check implemented: the left parameters of each constructor and
inductive types should be convertible and should have the very same name.
---

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) ->