From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 4 Apr 2008 10:04:06 +0000 (+0000)
Subject: returns_a_counductive implemented
X-Git-Tag: make_still_working~5458
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a2b79ad8b6fdbe07ea9d92102b0764ac4004a6db;p=helm.git

returns_a_counductive implemented
---

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 920a2078e..5e4000740 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -517,40 +517,6 @@ and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI =
              args coInductiveTypeURI
          ) fl true
 
- and returns_a_coinductive ~subst context ty =
-  let module C = Cic in
-   match CicReduction.whd ~subst context ty with
-      C.MutInd (uri,i,_) ->
-       (*CSC: definire una funzioncina per questo codice sempre replicato *)
-        let obj,_ =
-          try
-            CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
-          with Not_found -> assert false
-        in
-        (match obj with
-           C.InductiveDefinition (itl,_,_,_) ->
-            let (_,is_inductive,_,_) = List.nth itl i in
-             if is_inductive then None else (Some uri)
-         | _ ->
-            raise (TypeCheckerFailure
-              (lazy ("Unknown mutual inductive definition:" ^
-              UriManager.string_of_uri uri)))
-        )
-    | C.Appl ((C.MutInd (uri,i,_))::_) ->
-       (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
-         match o with
-           C.InductiveDefinition (itl,_,_,_) ->
-            let (_,is_inductive,_,_) = List.nth itl i in
-             if is_inductive then None else (Some uri)
-         | _ ->
-            raise (TypeCheckerFailure
-              (lazy ("Unknown mutual inductive definition:" ^
-              UriManager.string_of_uri uri)))
-        )
-    | C.Prod (n,so,de) ->
-       returns_a_coinductive ~subst ((Some (n,C.Decl so))::context) de
-    | _ -> None
-
  in
   type_of_aux ~logger context t ugraph
 
@@ -1148,7 +1114,15 @@ and is_really_smaller ~subst (context, recfuns, x, safes as k) te =
            pl cl
     | _ -> List.for_all (is_really_smaller ~subst k) pl)
 
-and returns_a_coinductive ~subst _ _ = assert false
+and returns_a_coinductive ~subst context ty =
+  match R.whd ~subst context ty with
+  | C.Const (Ref.Ref (_,uri,Ref.Ind _) as ref) 
+  | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind _) as ref)::_) ->
+     let isinductive, _, _, _, _ = E.get_checked_indtys ref in
+     if isinductive then None else (Some uri)
+  | C.Prod (n,so,de) ->
+     returns_a_coinductive ~subst ((n,C.Decl so)::context) de
+  | _ -> None
 
 and type_of_constant ref = assert false (* USARE typecheck_obj0 *)
 (* ALIAS typecheck *)