X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicTypeChecker.ml;h=63366b4b9997f5897027117458c17a98a7627f05;hb=09aa799947c84148221af82e94e911adea8fd1e6;hp=c86a27ad04e89c3424ebff3b5c7ed8f8cd6be9e6;hpb=c748674f4d7e3dc104d3edb0c31bc3c006a455f9;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index c86a27ad0..63366b4b9 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -285,12 +285,6 @@ and strictly_positive n nn te =
             i &&
              weakly_positive (n+1) (nn+1) uri x
           ) cl' true
-   | C.MutInd (uri,_,i) ->
-      (match CicEnvironment.get_obj uri with
-          C.InductiveDefinition (tl,_,_) ->
-           List.length tl = 1
-        | _ -> raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
-      )
    | t -> does_not_occur n nn t
 
 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
@@ -433,8 +427,8 @@ and recursive_args n nn te =
    | C.Cast _ (*CSC ??? *) -> raise (Impossible 3) (* due to type-checking *)
    | C.Prod (_,so,de) ->
       (not (does_not_occur n nn so))::(recursive_args (n+1) (nn + 1) de)
-   | C.Lambda _ -> raise (Impossible 4) (* due to type-checking *)
-   | C.LetIn _ -> raise NotImplemented
+   | C.Lambda _
+   | C.LetIn _ -> raise (Impossible 4) (* due to type-checking *)
    | C.Appl _ -> []
    | C.Const _
    | C.Abst _ -> raise (Impossible 5)
@@ -459,16 +453,26 @@ and get_new_safes p c rl safes n nn x =
          if b then 1::safes' else safes'
         in
          get_new_safes ta2 ta1 tl safes'' (n+1) (nn+1) (x+1)
-   | (C.MutInd _, e, []) -> (e,safes,n,nn,x)
+   | (C.Prod _, (C.MutConstruct _ as e), _)
+   | (C.Prod _, (C.Rel _ as e), _)
+   | (C.MutInd _, e, [])
    | (C.Appl _, e, []) -> (e,safes,n,nn,x)
-   | (_,_,_) -> raise (Impossible 7)
+   | (_,_,_) ->
+      (* CSC: If the next exception is raised, it just means that   *)
+      (* CSC: the proof-assistant allows to use very strange things *)
+      (* CSC: as a branch of a case whose type is a Prod. In        *)
+      (* CSC: particular, this means that a new (C.Prod, x,_) case  *)
+      (* CSC: must be considered in this match. (e.g. x = MutCase)  *)
+      raise (Impossible 7)
 
-and eat_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 -> eat_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 +532,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, eat_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 +564,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, eat_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 +671,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, eat_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 +708,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, eat_prods paramsno ty, r)) cl
+                  List.map (fun (id,ty,r) -> (id, snd (split_prods paramsno ty), r)) cl
                  in
                   (isinductive,paramsno,cl')
              | _ ->
@@ -773,95 +777,163 @@ and guarded_by_destructors n nn kl x safes =
              bo
          ) fl true
 
-(*CSC h = 0 significa non ancora protetto *)
-and guarded_by_constructors n nn h =
+(* the boolean h means already protected *)
+(* args is the list of arguments the type of the constructor that may be *)
+(* found in head position must be applied to.                            *)
+(*CSC: coInductiveTypeURI non cambia mai di ricorsione in ricorsione *)
+and guarded_by_constructors n nn h te args coInductiveTypeURI =
  let module C = Cic in
-  function
-     C.Rel m when m > n && m <= nn -> h = 1
+  (*CSC: There is a lot of code replication between the cases X and    *)
+  (*CSC: (C.Appl X tl). Maybe it will be better to define a function   *)
+  (*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *)
+  match CicReduction.whd te with
+     C.Rel m when m > n && m <= nn -> h
    | C.Rel _
-   | C.Var _ 
+   | C.Var _  -> true
    | C.Meta _
    | C.Sort _
-   | C.Implicit -> true (*CSC: ma alcuni sono impossibili!!!! vedi Prod *)
-   | C.Cast (te,ty) ->
-      guarded_by_constructors n nn h te &&
-       guarded_by_constructors n nn h ty
-   | C.Prod (_,so,de) ->
+   | C.Implicit
+   | C.Cast _
+   | C.Prod _
+   | C.LetIn _ ->
       raise (Impossible 17) (* the term has just been type-checked *)
    | C.Lambda (_,so,de) ->
       does_not_occur n nn so &&
-       guarded_by_constructors (n + 1) (nn + 1) h de
-   | C.LetIn (_,so,de) ->
-      does_not_occur n nn so &&
-       guarded_by_constructors (n + 1) (nn + 1) h de
+       guarded_by_constructors (n + 1) (nn + 1) h de args coInductiveTypeURI
    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
-      h = 1 &&
+      h &&
        List.fold_right (fun x i -> i && does_not_occur n nn x) tl true
    | C.Appl ((C.MutConstruct (uri,cookingsno,i,j))::tl) ->
-      let (is_coinductive, rl) =
+      let consty =
        match CicEnvironment.get_cooked_obj uri cookingsno with
           C.InductiveDefinition (itl,_,_) ->
-           let (_,is_inductive,_,cl) = List.nth itl i in
-            let (_,cons,rrec_args) = List.nth cl (j - 1) in
-             (match !rrec_args with
-                 None -> raise (Impossible 18)
-               | Some rec_args -> (not is_inductive, rec_args)
-             )
+           let (_,_,_,cl) = List.nth itl i in
+            let (_,cons,_) = List.nth cl (j - 1) in cons
         | _ ->
          raise (WrongUriToMutualInductiveDefinitions
           (UriManager.string_of_uri uri))
       in
-       is_coinductive &&
-       List.fold_right
-        (fun (x,r) i ->
-          i &&
-           if r then
-            guarded_by_constructors n nn 1 x
-           else
-            does_not_occur n nn x
-        ) (List.combine tl rl) true
+       let rec analyse_branch ty te =
+        match CicReduction.whd ty with
+           C.Meta _ -> raise (Impossible 34)
+         | C.Rel _
+         | C.Var _
+         | C.Sort _ ->
+            does_not_occur n nn te
+         | C.Implicit
+         | C.Cast _ -> raise (Impossible 24) (* due to type-checking *)
+         | C.Prod (_,_,de) ->
+            analyse_branch de te
+         | C.Lambda _
+         | C.LetIn _ -> raise (Impossible 25) (* due to type-checking *)
+         | C.Appl ((C.MutInd (uri,_,_))::tl) as ty
+            when uri == coInductiveTypeURI -> 
+             guarded_by_constructors n nn true te [] coInductiveTypeURI
+         | C.Appl ((C.MutInd (uri,_,_))::tl) as ty -> 
+            guarded_by_constructors n nn true te tl coInductiveTypeURI
+         | C.Appl _ ->
+            does_not_occur n nn te
+         | C.Const _
+         | C.Abst _ -> raise (Impossible 26)
+         | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
+            guarded_by_constructors n nn true te [] coInductiveTypeURI
+         | C.MutInd _ ->
+            does_not_occur n nn te
+         | C.MutConstruct _ -> raise (Impossible 27)
+         (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
+         (*CSC: in head position.                                       *)
+         | C.MutCase _
+         | C.Fix _
+         | C.CoFix _ -> raise (Impossible 28) (* due to type-checking *)
+       in
+       let rec analyse_instantiated_type ty l =
+        match CicReduction.whd ty with
+           C.Rel _
+         | C.Var _
+         | C.Meta _
+         | C.Sort _
+         | C.Implicit
+         | C.Cast _ -> raise (Impossible 29) (* due to type-checking *)
+         | C.Prod (_,so,de) ->
+            begin
+             match l with
+                [] -> true
+              | he::tl ->
+                 analyse_branch so he &&
+                  analyse_instantiated_type de tl
+            end
+         | C.Lambda _
+         | C.LetIn _ -> raise (Impossible 30) (* due to type-checking *)
+         | C.Appl _ -> 
+            List.fold_left (fun i x -> i && does_not_occur n nn x) true l
+         | C.Const _
+         | C.Abst _ -> raise (Impossible 31)
+         | C.MutInd _ ->
+            List.fold_left (fun i x -> i && does_not_occur n nn x) true l
+         | C.MutConstruct _ -> raise (Impossible 32)
+         (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
+         (*CSC: in head position.                                       *)
+         | C.MutCase _
+         | C.Fix _
+         | C.CoFix _ -> raise (Impossible 33) (* due to type-checking *)
+       in
+        let rec instantiate_type args consty =
+         function
+            [] -> true
+          | tlhe::tltl as l ->
+             let consty' = CicReduction.whd consty in
+              match args with 
+                 he::tl ->
+                  begin
+                   match consty' with
+                      C.Prod (_,_,de) ->
+                       let instantiated_de = CicSubstitution.subst he de in
+                        (*CSC: siamo sicuri che non sia troppo forte? *)
+                        does_not_occur n nn tlhe &
+                         instantiate_type tl instantiated_de tltl
+                    | _ ->
+                      (*CSC:We do not consider backbones with a MutCase, a    *)
+                      (*CSC:FixPoint, a CoFixPoint and so on in head position.*)
+                      raise (Impossible 23)
+                  end
+               | [] -> analyse_instantiated_type consty' l
+                  (* These are all the other cases *)
+       in
+        instantiate_type args consty tl
+   | C.Appl ((C.CoFix (_,fl))::tl) ->
+      List.fold_left (fun i x -> i && does_not_occur n nn x) true tl &&
+       let len = List.length fl in
+        let n_plus_len = n + len
+        and nn_plus_len = nn + len in
+         List.fold_right
+          (fun (_,ty,bo) i ->
+            i && does_not_occur n_plus_len nn_plus_len ty &&
+             guarded_by_constructors n_plus_len nn_plus_len h bo args
+              coInductiveTypeURI
+          ) fl true
+   | C.Appl ((C.MutCase (_,_,_,out,te,pl))::tl) ->
+       List.fold_left (fun i x -> i && does_not_occur n nn x) true tl &&
+        does_not_occur n nn out &&
+         does_not_occur n nn te &&
+          List.fold_right
+           (fun x i ->
+             i &&
+             guarded_by_constructors n nn h x args coInductiveTypeURI
+           ) pl true
    | C.Appl l ->
       List.fold_right (fun x i -> i && does_not_occur n nn x) l true
-   | C.Const _
+   | C.Const _ -> true
    | C.Abst _
-   | C.MutInd _ 
-   | C.MutConstruct _ -> true (*CSC: ma alcuni sono impossibili!!!! vedi Prod *)
+   | C.MutInd _ -> assert false
+   | C.MutConstruct _ -> true
    | C.MutCase (_,_,_,out,te,pl) ->
-      let rec returns_a_coinductive =
-       function
-          (*CSC: per le regole di tipaggio, la chiamata ricorsiva verra' *)
-          (*CSC: effettata solo una volta, per mangiarsi l'astrazione    *)
-          (*CSC: non dummy                                               *)
-          C.Lambda (_,_,de) -> returns_a_coinductive de
-        | C.MutInd (uri,_,i) ->
-           (*CSC: definire una funzioncina per questo codice sempre replicato *)
-           (match CicEnvironment.get_obj uri with
-               C.InductiveDefinition (itl,_,_) ->
-                let (_,is_inductive,_,_) = List.nth itl i in
-                 not is_inductive
-             | _ ->
-               raise (WrongUriToMutualInductiveDefinitions
-                (UriManager.string_of_uri uri))
-            )
-        (*CSC: bug nella prossima riga (manca la whd) *)
-        | C.Appl ((C.MutInd (uri,_,i))::_) ->
-           (match CicEnvironment.get_obj uri with
-               C.InductiveDefinition (itl,_,_) ->
-                let (_,is_inductive,_,_) = List.nth itl i in
-                 not is_inductive
-             | _ ->
-               raise (WrongUriToMutualInductiveDefinitions
-                (UriManager.string_of_uri uri))
-            )
-        | _ -> false
-      in
        does_not_occur n nn out &&
         does_not_occur n nn te &&
-        if returns_a_coinductive out then
          List.fold_right
-          (fun x i -> i && guarded_by_constructors n nn h x) pl true
-        else
-         List.fold_right (fun x i -> i && does_not_occur n nn x) pl true
+          (fun x i ->
+            i &&
+             guarded_by_constructors n nn h x args coInductiveTypeURI
+          ) pl true
    | C.Fix (_,fl) ->
       let len = List.length fl in
        let n_plus_len = n + len
@@ -878,7 +950,8 @@ and guarded_by_constructors n nn h =
         List.fold_right
          (fun (_,ty,bo) i ->
            i && does_not_occur n_plus_len nn_plus_len ty &&
-            does_not_occur n_plus_len nn_plus_len bo
+            guarded_by_constructors n_plus_len nn_plus_len h bo args
+             coInductiveTypeURI
          ) fl true
 
 and check_allowed_sort_elimination uri i need_dummy ind arity1 arity2 =
@@ -903,19 +976,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
-             (* is a small inductive type? *)
-             (*CSC: ottimizzare calcolando staticamente *)
-             let rec is_small =
-              function
-                 C.Prod (_,so,de) ->
-                  let s = type_of so in
-                   (s = C.Sort C.Prop || s = C.Sort C.Set) &&
-                   is_small de
-               | _ -> true (*CSC: we trust the type-checker *)
-             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))
        )
@@ -947,18 +1010,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
-                   (* is a small inductive type? *)
-                   let rec is_small =
-                    function
-                       C.Prod (_,so,de) ->
-                        let s = type_of so in
-                         (s = C.Sort C.Prop || s = C.Sort C.Set) &&
-                         is_small de
-                     | _ -> true (*CSC: we trust the type-checker *)
-                   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))
@@ -992,14 +1047,22 @@ and type_of_branch argsno need_dummy outtype term constype =
   | _ -> raise (Impossible 20)
        
  
-and type_of t =
+(* type_of_aux' is just another name (with a different scope) for type_of_aux *)
+and type_of_aux' env t =
  let rec type_of_aux env =
   let module C = Cic in
   let module R = CicReduction in
   let module S = CicSubstitution in
   let module U = UriManager in
    function
-      C.Rel n -> S.lift n (List.nth env (n - 1))
+      C.Rel n ->
+       let t =
+        try
+         List.nth env (n - 1)
+        with
+         _ -> raise (NotWellTyped "Not a close term")
+       in
+        S.lift n t
     | C.Var uri ->
       incr fdebug ;
       let ty = type_of_variable uri in
@@ -1024,15 +1087,12 @@ and type_of t =
          let _ = sort_of_prod (sort1,sort2) in
           C.Prod (n,s,type2)
    | C.LetIn (n,s,t) ->
-       let type1 = type_of_aux env s in
-       let type2 = type_of_aux (type1::env) t in
-        type2
+       let t' = CicSubstitution.subst s t in
+        type_of_aux env t'
    | C.Appl (he::tl) when List.length tl > 0 ->
       let hetype = type_of_aux env he
       and tlbody_and_type = List.map (fun x -> (x, type_of_aux env x)) tl in
-       (try
-        eat_prods hetype tlbody_and_type
-       with _ -> debug (C.Appl (he::tl)) env ; C.Implicit)
+       eat_prods hetype tlbody_and_type
    | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
    | C.Const (uri,cookingsno) ->
       incr fdebug ;
@@ -1053,7 +1113,7 @@ and type_of t =
       let outsort = type_of_aux env outtype in
       let (need_dummy, k) =
        let rec guess_args t =
-        match decast t with
+        match CicReduction.whd t with
            C.Sort _ -> (true, 0)
          | C.Prod (_, s, t) ->
             let (b, n) = guess_args t in
@@ -1172,9 +1232,14 @@ and type_of t =
             (CicSubstitution.lift len ty))
            then
             begin
-             (* let's control the guarded by constructors conditions C{f,M} *)
-             if not (guarded_by_constructors 0 len 0 bo) then
-              raise (NotWellTyped "CoFix: not guarded by constructors")
+             (* let's control that the returned type is coinductive *)
+             match returns_a_coinductive ty with
+                None ->
+                 raise(NotWellTyped "CoFix: does not return a coinductive type")
+              | Some uri ->
+                 (*let's control the guarded by constructors conditions C{f,M}*)
+                 if not (guarded_by_constructors 0 len false bo [] uri) then
+                  raise (NotWellTyped "CoFix: not guarded by constructors")
             end
            else
             raise (NotWellTyped "CoFix: ill-typed bodies")
@@ -1183,25 +1248,19 @@ and type_of t =
         let (_,ty,_) = List.nth fl i in
          ty
 
- (* CSC: wrong name and position: decast really does Cast-LetIn reduction *)
- and decast =
-  let module C = Cic in
-   function
-      C.Cast (t,_) -> decast t
-    | C.LetIn (_,s,t) -> decast (CicSubstitution.subst s t)
-    | t -> t
-
  and sort_of_prod (t1, t2) =
   let module C = Cic in
-   match (decast t1, decast t2) with
+   let t1' = CicReduction.whd t1 in
+   let t2' = CicReduction.whd t2 in
+   match (t1', t2') with
       (C.Sort s1, C.Sort s2)
         when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *)
          C.Sort s2
     | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
     | (_,_) ->
       raise
-       (NotWellTyped ("Prod: sort1= " ^ CicPp.ppterm t1 ^ " ;
-         sort2= " ^ CicPp.ppterm t2))
+       (NotWellTyped
+        ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= " ^ CicPp.ppterm t2'))
 
  and eat_prods hetype =
   (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
@@ -1213,19 +1272,64 @@ and type_of t =
         Cic.Prod (n,s,t) ->
          if CicReduction.are_convertible s hety then
           (CicReduction.fdebug := -1 ;
-          eat_prods (CicSubstitution.subst hete t) tl
+           eat_prods (CicSubstitution.subst hete t) tl
           )
          else
-          (
-          CicReduction.fdebug := 0 ;
-          let _ = CicReduction.are_convertible s hety in
-          debug hete [hety ; s] ;
-          raise (NotWellTyped "Appl: wrong parameter-type")
-)
+          begin
+           CicReduction.fdebug := 0 ;
+           ignore (CicReduction.are_convertible s hety) ;
+           fdebug := 0 ;
+           debug s [hety] ;
+           raise (NotWellTyped "Appl: wrong parameter-type")
+          end
       | _ -> raise (NotWellTyped "Appl: wrong Prod-type")
     )
+
+ and returns_a_coinductive ty =
+  let module C = Cic in
+   match CicReduction.whd ty with
+      C.MutInd (uri,cookingsno,i) ->
+       (*CSC: definire una funzioncina per questo codice sempre replicato *)
+       (match CicEnvironment.get_cooked_obj uri cookingsno with
+           C.InductiveDefinition (itl,_,_) ->
+            let (_,is_inductive,_,cl) = List.nth itl i in
+             if is_inductive then None else (Some uri)
+         | _ ->
+           raise (WrongUriToMutualInductiveDefinitions
+            (UriManager.string_of_uri uri))
+        )
+    | C.Appl ((C.MutInd (uri,_,i))::_) ->
+       (match CicEnvironment.get_obj uri with
+           C.InductiveDefinition (itl,_,_) ->
+            let (_,is_inductive,_,_) = List.nth itl i in
+             if is_inductive then None else (Some uri)
+         | _ ->
+           raise (WrongUriToMutualInductiveDefinitions
+            (UriManager.string_of_uri uri))
+        )
+    | C.Prod (_,_,de) -> returns_a_coinductive de
+    | _ -> None
+
  in
-  type_of_aux [] t
+  type_of_aux env t
+
+(* is a small constructor? *)
+(*CSC: ottimizzare calcolando staticamente *)
+and is_small paramsno c =
+ let rec is_small_aux env c =
+  let module C = Cic in
+   match CicReduction.whd c with
+      C.Prod (_,so,de) ->
+       let s = type_of_aux' env so in
+        (s = C.Sort C.Prop || s = C.Sort C.Set) &&
+        is_small_aux (so::env) de
+    | _ -> true (*CSC: we trust the type-checker *)
+ in
+  let (sx,dx) = split_prods paramsno c in
+   is_small_aux (List.rev sx) dx
+
+and type_of t =
+ type_of_aux' [] t
 ;;
 
 let typecheck uri =