...

[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 65e87e55d0c43fd912d53c41a5fb19fd8139ed6a..bd660903cc86fa682b74fbff028694f46c2e2e0f 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -124,7 +124,7 @@ let sort_of_prod ~metasenv ~subst context (name,s) (t1, t2) =
    let t2 = R.whd ~subst ((name,C.Decl s)::context) t2 in
    match t1, t2 with
    | C.Sort s1, C.Sort C.Prop -> t2
-   | C.Sort (C.Type u1), C.Sort (C.Type u2) -> C.Sort (C.Type (max u1 u2)) 
+   | C.Sort (C.Type u1), C.Sort (C.Type u2) -> C.Sort (C.Type (u1@u2)) 
    | C.Sort _,C.Sort (C.Type _) -> t2
    | C.Sort (C.Type _) , C.Sort C.CProp -> t1
    | C.Sort _, C.Sort C.CProp
@@ -712,12 +712,37 @@ and check_mutual_inductive_defs uri ~metasenv ~subst is_ind leftno tyl =
   ignore
    (List.fold_right
     (fun (_,_,ty,cl) i ->
-       let _,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) -> 
-(*CSC: assicurarmi che i sx siano esattamente gli stessi! *)
            let te = debruijn uri len [] te in
            let context,te = split_prods ~subst tys leftno te 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_left2
+              (fun context item1 item2 ->
+                let convertible =
+                 match item1,item2 with
+                   (n1,C.Decl ty1),(n2,C.Decl ty2) ->
+                     n1 = n2 && R.are_convertible ~subst context ty1 ty2
+                 | (n1,C.Def (bo1,ty1)),(n2,C.Def (bo2,ty2)) ->
+                     n1 = n2
+                     && R.are_convertible ~subst context ty1 ty2
+                     && R.are_convertible ~subst context bo1 bo2
+                 | _,_ -> false
+                in
+                 if not convertible then
+                  raise (TypeCheckerFailure (lazy
+                   ("Mismatch between the left parameters of the constructor " ^
+                    "and those of its inductive type")))
+                 else
+                  item1::context
+              ) [] 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
                (C.Sort (C.Type u1) as s1), (C.Sort (C.Type u2) as s2) ->
@@ -985,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"))
 ;;