The definition of small inductive types has been relaxed: a constructor

is now considered small when its type without the parameters was small
with the previous definition. This is consistent with Coq's behaviour.

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 77a1251605f2915e0fa6c8a9cc349d5feec86461..895d157dfe9e26b3ad53ded633035a88b16fcd8b 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -463,12 +463,14 @@ and get_new_safes p c rl safes n nn x =
    | (C.Appl _, e, []) -> (e,safes,n,nn,x)
    | (_,_,_) -> raise (Impossible 7)
 
-and drop_prods n te =
+and split_prods n te =
  let module C = Cic in
  let module R = CicReduction in
   match (n, R.whd te) with
-     (0, _) -> te
-   | (n, C.Prod (_,_,ta)) when n > 0 -> drop_prods (n - 1) ta
+     (0, _) -> [],te
+   | (n, C.Prod (_,so,ta)) when n > 0 ->
+      let (l1,l2) = split_prods (n - 1) ta in
+       (so::l1,l2)
    | (_, _) -> raise (Impossible 8)
 
 and eat_lambdas n te =
@@ -528,7 +530,7 @@ and check_is_really_smaller_arg n nn kl x safes te =
                C.InductiveDefinition (tl,_,paramsno) ->
                 let (_,isinductive,_,cl) = List.nth tl i in
                  let cl' =
-                  List.map (fun (id,ty,r) -> (id, drop_prods paramsno ty, r)) cl
+                  List.map (fun (id,ty,r) -> (id, snd (split_prods paramsno ty), r)) cl
                  in
                   (isinductive,paramsno,cl')
              | _ ->
@@ -560,7 +562,7 @@ and check_is_really_smaller_arg n nn kl x safes te =
                C.InductiveDefinition (tl,_,paramsno) ->
                 let (_,isinductive,_,cl) = List.nth tl i in
                  let cl' =
-                  List.map (fun (id,ty,r) -> (id, drop_prods paramsno ty, r)) cl
+                  List.map (fun (id,ty,r) -> (id, snd (split_prods paramsno ty), r)) cl
                  in
                   (isinductive,paramsno,cl')
              | _ ->
@@ -667,7 +669,7 @@ and guarded_by_destructors n nn kl x safes =
                C.InductiveDefinition (tl,_,paramsno) ->
                 let (_,isinductive,_,cl) = List.nth tl i in
                  let cl' =
-                  List.map (fun (id,ty,r) -> (id, drop_prods paramsno ty, r)) cl
+                  List.map (fun (id,ty,r) -> (id, snd (split_prods paramsno ty), r)) cl
                  in
                   (isinductive,paramsno,cl')
              | _ ->
@@ -704,7 +706,7 @@ and guarded_by_destructors n nn kl x safes =
                C.InductiveDefinition (tl,_,paramsno) ->
                 let (_,isinductive,_,cl) = List.nth tl i in
                  let cl' =
-                  List.map (fun (id,ty,r) -> (id, drop_prods paramsno ty, r)) cl
+                  List.map (fun (id,ty,r) -> (id, snd (split_prods paramsno ty), r)) cl
                  in
                   (isinductive,paramsno,cl')
              | _ ->
@@ -903,9 +905,9 @@ and check_allowed_sort_elimination uri i need_dummy ind arity1 arity2 =
    | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true
    | (C.Sort C.Set, C.Sort C.Type) when need_dummy ->
        (match CicEnvironment.get_obj uri with
-           C.InductiveDefinition (itl,_,_) ->
+           C.InductiveDefinition (itl,_,paramsno) ->
             let (_,_,_,cl) = List.nth itl i in
-             List.fold_right (fun (_,x,_) i -> i && is_small x) cl true
+             List.fold_right (fun (_,x,_) i -> i && is_small paramsno x) cl true
          | _ ->
            raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
        )
@@ -937,9 +939,10 @@ and check_allowed_sort_elimination uri i need_dummy ind arity1 arity2 =
           | C.Sort C.Set  -> true
           | C.Sort C.Type ->
              (match CicEnvironment.get_obj uri with
-                 C.InductiveDefinition (itl,_,_) ->
+                 C.InductiveDefinition (itl,_,paramsno) ->
                   let (_,_,_,cl) = List.nth itl i in
-                   List.fold_right (fun (_,x,_) i -> i && is_small x) cl true
+                   List.fold_right
+                    (fun (_,x,_) i -> i && is_small paramsno x) cl true
                | _ ->
                  raise (WrongUriToMutualInductiveDefinitions
                   (U.string_of_uri uri))
@@ -1211,7 +1214,7 @@ and type_of_aux' env t =
 
 (* is a small constructor? *)
 (*CSC: ottimizzare calcolando staticamente *)
-and is_small c =
+and is_small paramsno c =
  let rec is_small_aux env c =
   let module C = Cic in
    match CicReduction.whd c with
@@ -1221,7 +1224,8 @@ and is_small c =
         is_small_aux (so::env) de
     | _ -> true (*CSC: we trust the type-checker *)
  in
-  is_small_aux [] c
+  let (sx,dx) = split_prods paramsno c in
+   is_small_aux sx dx
 
 and type_of t =
  type_of_aux' [] t