Added boolean "is_inductive" to NReference.Ind

[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 25042b4cdf8b1d6aee7f82145cee50ac4d29a9ca..7e0f483d301adf6773d5bc4e9822a291caa40113 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -111,7 +111,7 @@ let debruijn ?(cb=fun _ _ -> ()) uri number_of_types context =
        if l1 == l then t else C.Meta (i,(s,C.Ctx l1))
     | C.Meta _ -> t
     | C.Const (Ref.Ref (_,uri1,(Ref.Fix (no,_) | Ref.CoFix no))) 
-    | C.Const (Ref.Ref (_,uri1,Ref.Ind no)) when NUri.eq uri uri1 ->
+    | C.Const (Ref.Ref (_,uri1,Ref.Ind (_,no))) when NUri.eq uri uri1 ->
        C.Rel (k + number_of_types - no)
     | t -> U.map (fun _ k -> k+1) k aux t
   in
@@ -190,8 +190,8 @@ let rec instantiate_parameters params c =
 
 let specialize_inductive_type_constrs ~subst context ty_term =
   match R.whd ~subst context ty_term with
-  | C.Const (Ref.Ref (_,uri,Ref.Ind i) as ref)  
-  | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind i) as ref) :: _ ) as ty ->
+  | C.Const (Ref.Ref (_,uri,Ref.Ind (_,i)) as ref)  
+  | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind (_,i)) as ref) :: _ ) as ty ->
       let args = match ty with C.Appl (_::tl) -> tl | _ -> [] in
       let is_ind, leftno, itl, attrs, i = E.get_checked_indtys ref in
       let left_args,_ = HExtlib.split_nth leftno args in
@@ -249,8 +249,8 @@ let rec weakly_positive ~subst context n nn uri te =
   let dummy = C.Sort (C.Type ~-1) in
   (*CSC: mettere in cicSubstitution *)
   let rec subst_inductive_type_with_dummy _ = function
-    | C.Const (Ref.Ref (_,uri',Ref.Ind 0)) when NUri.eq uri' uri -> dummy
-    | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind 0)))::tl) 
+    | C.Const (Ref.Ref (_,uri',Ref.Ind (true,0))) when NUri.eq uri' uri -> dummy
+    | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind (true,0))))::tl) 
         when NUri.eq uri' uri -> dummy
     | t -> U.map (fun _ x->x) () subst_inductive_type_with_dummy t
   in
@@ -282,7 +282,7 @@ and strictly_positive ~subst context n nn te =
        strictly_positive ~subst ((name,C.Decl so)::context) (n+1) (nn+1) ta
    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
       List.for_all (does_not_occur ~subst context n nn) tl
-   | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind i) as r)::tl) -> 
+   | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind (_,i)) as r)::tl) -> 
       let _,paramsno,tyl,_,i = E.get_checked_indtys r in
       let _,name,ity,cl = List.nth tyl i in
       let ok = List.length tyl = 1 in
@@ -416,7 +416,7 @@ let rec typeof ~subst ~metasenv context term =
 *)
        eat_prods ~subst ~metasenv context he ty_he args_with_ty
    | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
-   | C.Match (Ref.Ref (_,_,Ref.Ind tyno) as r,outtype,term,pl) ->
+   | C.Match (Ref.Ref (_,_,Ref.Ind (_,tyno)) as r,outtype,term,pl) ->
       let outsort = typeof_aux context outtype in
       let inductive,leftno,itl,_,_ = E.get_checked_indtys r in
       let constructorsno =
@@ -805,13 +805,9 @@ and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t =
          ) bos
       in
        List.iter (fun (bo,k) -> aux k bo) bos_and_ks
-  | C.Match (Ref.Ref (_,uri,_) as ref,outtype,term,pl) as t ->
+  | C.Match (Ref.Ref (_,uri,Ref.Ind (true,_)),outtype,term,pl) as t ->
      (match R.whd ~subst context term with
      | C.Rel m | C.Appl (C.Rel m :: _ ) as t when is_safe m recfuns || m = x ->
-        (* TODO: add CoInd to references so that this call is useless *)
-        let isinductive, _, _, _, _ = E.get_checked_indtys ref in
-        if not isinductive then recursor aux k t
-        else
          let ty = typeof ~subst ~metasenv context term in
          let dc_ctx, dcl, start, stop = 
            specialize_and_abstract_constrs ~subst r_uri r_len context ty in
@@ -953,17 +949,17 @@ and is_really_smaller
 
 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, _, itl, _, _ = E.get_checked_indtys ref in
-     if isinductive then None else (Some (uri,List.length itl))
+  | C.Const (Ref.Ref (_,uri,Ref.Ind (false,_)) as ref) 
+  | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind (false,_)) as ref)::_) ->
+     let _, _, itl, _, _ = E.get_checked_indtys ref in
+     Some (uri,List.length itl)
   | C.Prod (n,so,de) ->
      returns_a_coinductive ~subst ((n,C.Decl so)::context) de
   | _ -> None
 
 and type_of_constant ((Ref.Ref (_,uri,_)) as ref) = 
   match E.get_checked_obj uri, ref with
-  | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,_,Ref.Ind i)  ->
+  | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,_,Ref.Ind (_,i))  ->
       let _,_,arity,_ = List.nth tl i in arity
   | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,_,Ref.Con (i,j))  ->
       let _,_,_,cl = List.nth tl i in