X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.ml;h=81f633bb6c850362623c0b617ff3ccc41e86b52f;hb=dff76b5e1557ff32872f4e48854daaa6c42e5ad2;hp=7ba5ab15219d435aa3be7011fd3086c0086f15ff;hpb=a059534681dde44cf2b39d8663cc98a59c3a9e0a;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 7ba5ab152..81f633bb6 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -765,9 +765,9 @@ let rec typeof ~subst ~metasenv context term =
       in
       if List.length pl <> constructorsno then
        raise (TypeCheckerFailure (lazy ("Wrong number of cases in a match")));
-      let j,branches_ok =
+      let j,branches_ok,p_ty, exp_p_ty =
         List.fold_left
-          (fun (j,b) p ->
+          (fun (j,b,old_p_ty,old_exp_p_ty) p ->
             if b then
               let cons = 
                 let cons = Ref.Ref (dummy_depth, uri, Ref.Con (tyno, j)) in
@@ -777,20 +777,24 @@ let rec typeof ~subst ~metasenv context term =
               let ty_p = typeof_aux context p in
               let ty_cons = typeof_aux context cons in
               let ty_branch = 
-                type_of_branch ~subst context leftno outtype cons ty_cons 0 in
-              j+1, R.are_convertible ~subst ~metasenv context ty_p ty_branch 
+                type_of_branch ~subst context leftno outtype cons ty_cons 0 
+              in
+              j+1, R.are_convertible ~subst ~metasenv context ty_p ty_branch,
+              ty_p, ty_branch
             else
-              j,false
-          ) (1,true) pl
-         in
-          if not branches_ok then
-           raise
-            (TypeCheckerFailure 
-              (lazy (Printf.sprintf "Branch for constructor %s has wrong type"
-              (NCicPp.ppterm (C.Const 
-                (Ref.Ref (dummy_depth, uri, Ref.Con (tyno, j)))))))); 
-          let res = outtype::arguments@[term] in
-          R.head_beta_reduce (C.Appl res)
+              j,false,old_p_ty,old_exp_p_ty
+          ) (1,true,C.Sort C.Prop,C.Sort C.Prop) pl
+      in
+      if not branches_ok then
+        raise
+         (TypeCheckerFailure 
+          (lazy (Printf.sprintf ("Branch for constructor %s :=\n%s\n"^^
+          "has type %s\nnot convertible with %s") (NCicPp.ppterm (C.Const 
+          (Ref.Ref (dummy_depth, uri, Ref.Con (tyno, j)))))
+          (NCicPp.ppterm ~context (List.nth pl (j-1)))
+          (NCicPp.ppterm ~context p_ty) (NCicPp.ppterm ~context exp_p_ty)))); 
+      let res = outtype::arguments@[term] in
+      R.head_beta_reduce (C.Appl res)
     | C.Match _ -> assert false
 
   and type_of_branch ~subst context leftno outty cons tycons liftno = 
@@ -953,7 +957,7 @@ let rec typeof ~subst ~metasenv context term =
  in 
    typeof_aux context term
 
-and check_mutual_inductive_defs _ = assert false
+and check_mutual_inductive_defs _ = ()
 
 and eat_lambdas ~subst context n te =
   match (n, R.whd ~subst context te) with
@@ -1150,7 +1154,7 @@ and type_of_constant ((Ref.Ref (_,uri,_)) as ref) =
       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 in 
+      let _,_,arity = List.nth cl (j-1) in 
       arity
   | (_,_,_,_,C.Fixpoint (_,fl,_)), Ref.Ref (_,_,(Ref.Fix (i,_)|Ref.CoFix i)) ->
       let _,_,_,arity,_ = List.nth fl i in
@@ -1170,7 +1174,7 @@ and check_obj_well_typed (uri,height,metasenv,subst,kind) =
         "the type of the body is not the one expected:\n%s\nvs\n%s"
         (NCicPp.ppterm ty_te) (NCicPp.ppterm ty))))
    | C.Constant (_,_,None,ty,_) -> ignore (typeof ~subst ~metasenv [] ty)
-   | C.Inductive _ as obj -> check_mutual_inductive_defs uri obj
+   | C.Inductive _ as obj -> check_mutual_inductive_defs obj
    | C.Fixpoint (inductive,fl,_) ->
       let types,kl,len =
         List.fold_left
@@ -1180,6 +1184,7 @@ and check_obj_well_typed (uri,height,metasenv,subst,kind) =
          ) ([],[],0) fl
       in
         List.iter (fun (_,name,x,ty,bo) ->
+         let bo = debruijn uri len bo in
          let ty_bo = typeof ~subst ~metasenv types bo in
          if not (R.are_convertible ~subst ~metasenv types ty_bo (S.lift len ty))
          then raise (TypeCheckerFailure (lazy ("(Co)Fix: ill-typed bodies")))