From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 30 Jul 2008 15:08:17 +0000 (+0000)
Subject: fixed allowed sort elim
X-Git-Tag: make_still_working~4871
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=341a777b344e7adb1e989dda3fdd643a3d9fb5f5;p=helm.git

fixed allowed sort elim
---

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 8124afcc4..c68982ff7 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -320,7 +320,7 @@ and are_all_occurrences_positive ~subst context uri indparamsno i n nn te =
         raise (TypeCheckerFailure
          (lazy ("Non-positive occurence in mutual inductive definition(s) [3]"^
           NUri.string_of_uri uri)))
-  | C.Prod (name,source,dest) when
+   | C.Prod (name,source,dest) when
       does_not_occur ~subst ((name,C.Decl source)::context) 0 1 dest ->
       strictly_positive ~subst context n nn indparamsno uri source &&
        are_all_occurrences_positive ~subst 
@@ -632,15 +632,16 @@ let rec typeof ~subst ~metasenv context term =
          * have them already *)
                 let _,leftno,itl,_,i = E.get_checked_indtys r in
                 let itl_len = List.length itl in
-                let _,_,_,cl = List.nth itl i in
+                let _,itname,ittype,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? *)
+                 (* is it a singleton, non recursive and non informative
+                    definition or an empty one? *)
                  if not
                   (cl_len = 0 ||
                    (itl_len = 1 && cl_len = 1 &&
-                    is_non_informative leftno
-                     (let _,_,x = List.hd cl in x)))
+                    let _,_,constrty = List.hd cl in
+                      is_non_recursive_singleton r itname ittype constrty &&
+                      is_non_informative leftno constrty))
                  then
                   raise (TypeCheckerFailure (lazy
                    ("Sort elimination not allowed")));
@@ -685,6 +686,11 @@ and eat_prods ~subst ~metasenv context he ty_he args_with_ty =
   in
     aux ty_he args_with_ty
 
+and is_non_recursive_singleton (Ref.Ref (uri,_)) iname ity cty =
+     let ctx = [iname, C.Decl ity] in
+     let cty = debruijn uri 1 [] cty in
+     does_not_occur ~subst:[] ctx 0 1 cty
+
 and is_non_informative paramsno c =
  let rec aux context c =
    match R.whd context c with