From 6b1ac4f9ec36e07ac0e69e6cb6d8530af18d3832 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 18 May 2008 20:51:15 +0000
Subject: [PATCH] Bug fixed: when computing the left arguments, I was not doing
 the right thing.

New check implemented: references should cache data correctly.
---
 .../components/ng_kernel/nCicTypeChecker.ml   | 31 ++++++++++++++-----
 1 file changed, 23 insertions(+), 8 deletions(-)

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 21da67bb8..bd660903c 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -712,15 +712,19 @@ and check_mutual_inductive_defs uri ~metasenv ~subst is_ind leftno tyl =
   ignore
    (List.fold_right
     (fun (_,_,ty,cl) i ->
-       let sx_context_ty,ty_sort = split_prods ~subst [] ~-1 ty in
+       let context,ty_sort = split_prods ~subst [] ~-1 ty in
+       let sx_context_ty_rev,_ = HExtlib.split_nth leftno (List.rev context) in
        List.iter
          (fun (_,name,te) -> 
            let te = debruijn uri len [] te in
            let context,te = split_prods ~subst tys leftno te in
-           let sx_context_te,_ = HExtlib.split_nth leftno context in
+           let _,chopped_context_rev =
+            HExtlib.split_nth (List.length tys) (List.rev context) in
+           let sx_context_te_rev,_ =
+            HExtlib.split_nth leftno chopped_context_rev in
            (try
-             ignore (List.fold_right2
-              (fun item1 item2 context ->
+             ignore (List.fold_left2
+              (fun context item1 item2 ->
                 let convertible =
                  match item1,item2 with
                    (n1,C.Decl ty1),(n2,C.Decl ty2) ->
@@ -737,7 +741,7 @@ and check_mutual_inductive_defs uri ~metasenv ~subst is_ind leftno tyl =
                     "and those of its inductive type")))
                  else
                   item1::context
-              ) sx_context_ty sx_context_te [])
+              ) [] sx_context_ty_rev sx_context_te_rev)
             with Invalid_argument _ -> assert false);
            let con_sort = typeof ~subst ~metasenv context te in
            (match R.whd ~subst context con_sort, R.whd ~subst [] ty_sort with
@@ -1006,17 +1010,28 @@ and returns_a_coinductive ~subst context ty =
   | _ -> None
 
 and type_of_constant ((Ref.Ref (uri,_)) as ref) = 
+ let error () =
+  raise (TypeCheckerFailure (lazy "Inconsistent cached infos in reference"))
+ in
   match E.get_checked_obj uri, ref with
-  | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,Ref.Ind (_,i))  ->
+  | (_,_,_,_,C.Inductive (isind1,_,tl,_)), Ref.Ref (_,Ref.Ind (isind2,i))  ->
+      if isind1 <> isind2 then error ();
       let _,_,arity,_ = List.nth tl i in arity
   | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,Ref.Con (i,j))  ->
       let _,_,_,cl = List.nth tl i in 
       let _,_,arity = List.nth cl (j-1) in 
       arity
-  | (_,_,_,_,C.Fixpoint (_,fl,_)), Ref.Ref (_,(Ref.Fix (i,_,_)|Ref.CoFix i)) ->
+  | (_,_,_,_,C.Fixpoint (_,fl,_)), Ref.Ref (_,Ref.CoFix i) ->
       let _,_,_,arity,_ = List.nth fl i in
       arity
-  | (_,_,_,_,C.Constant (_,_,_,ty,_)), Ref.Ref (_,(Ref.Def _|Ref.Decl)) -> ty
+  | (_,h1,_,_,C.Fixpoint (_,fl,_)), Ref.Ref (_,Ref.Fix (i,recno2,h2)) ->
+      let _,_,recno1,arity,_ = List.nth fl i in
+      if h1 <> h2 || recno1 <> recno2 then error ();
+      arity
+  | (_,_,_,_,C.Constant (_,_,_,ty,_)), Ref.Ref (_,Ref.Decl) -> ty
+  | (_,h1,_,_,C.Constant (_,_,_,ty,_)), Ref.Ref (_,Ref.Def h2) ->
+     if h1 <> h2 then error ();
+     ty
   | _ -> raise (AssertFailure (lazy "type_of_constant: environment/reference"))
 ;;
 
-- 
2.39.2