Bug fixed: when computing the left arguments, I was not doing the right thing.

New check implemented: references should cache data correctly.

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 21da67bb820d7963ce325d6fe1bd46d77988dc47..bd660903cc86fa682b74fbff028694f46c2e2e0f 100644 (file)
--- 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"))
 ;;