Procedural: explicit flavour specification for constants is now working

[helm.git] / helm / software / components / ng_kernel / nCicTypeChecker.ml

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 8124afcc4ae9115f708800b1c68845597ce9ca8b..cf445a8f0fc28d0d562238ecc053fd719186527c 100644 (file)
--- 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,20 @@ 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
+     let len = List.length ctx in
+     let rec aux ctx n nn t =
+       match R.whd ctx t with
+       | C.Prod (name, src, tgt) ->
+            does_not_occur ~subst:[] ctx n nn src &&
+             aux ((name, C.Decl src) :: ctx) (n+1) (nn+1) tgt
+       | C.Rel k | C.Appl (C.Rel k :: _) when k = nn -> true
+       | _ -> assert false
+     in
+     aux ctx (len-1) len cty
+
 and is_non_informative paramsno c =
  let rec aux context c =
    match R.whd context c with