some debug printings

[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 7ba5ab15219d435aa3be7011fd3086c0086f15ff..ceb14d17c4145cd432ee4fc3290bb06c8fb1b082 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -608,6 +608,11 @@ let eat_prods ~subst ~metasenv context ty_he args_with_ty =
   | (arg, ty_arg)::tl ->
       (match R.whd ~subst context ty_he with 
       | C.Prod (n,s,t) ->
+(*
+          prerr_endline (NCicPp.ppterm ~context s ^ " - Vs - " ^ NCicPp.ppterm
+          ~context ty_arg);
+          prerr_endline (NCicPp.ppterm ~context (S.subst ~avoid_beta_redexes:true arg t));
+*)
           if R.are_convertible ~subst ~metasenv context ty_arg s then
             aux (S.subst ~avoid_beta_redexes:true arg t) tl
           else
@@ -667,7 +672,9 @@ let does_not_occur ~subst context n nn t =
 exception NotGuarded;;
 
 let rec typeof ~subst ~metasenv context term =
-  let rec typeof_aux context = function
+  let rec typeof_aux context = 
+    fun t -> (*prerr_endline (NCicPp.ppterm ~context t); *)
+    match t with
     | C.Rel n ->
        (try
          match List.nth context (n - 1) with
@@ -720,6 +727,13 @@ let rec typeof ~subst ~metasenv context term =
     | C.Appl (he::(_::_ as args)) ->
        let ty_he = typeof_aux context he in
        let args_with_ty = List.map (fun t -> t, typeof_aux context t) args in
+(*
+       prerr_endline ("HEAD: " ^ NCicPp.ppterm ~context ty_he);
+       prerr_endline ("TARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm
+       ~context) (List.map snd args_with_ty)));
+       prerr_endline ("ARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm
+       ~context) (List.map fst args_with_ty)));
+*)
        eat_prods ~subst ~metasenv context ty_he args_with_ty
    | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
    | C.Match (Ref.Ref (dummy_depth,uri,Ref.Ind tyno) as r,outtype,term,pl) ->
@@ -765,9 +779,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 +791,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 +971,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 +1168,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
@@ -1163,14 +1181,17 @@ and check_obj_well_typed (uri,height,metasenv,subst,kind) =
  assert (metasenv = [] && subst = []);
  match kind with
    | C.Constant (_,_,Some te,ty,_) ->
+      prerr_endline ("TY: " ^ NCicPp.ppterm ty);
+      prerr_endline ("BO: " ^ NCicPp.ppterm te);
       let _ = typeof ~subst ~metasenv [] ty in
       let ty_te = typeof ~subst ~metasenv [] te in
+      prerr_endline "XXXX";
       if not (R.are_convertible ~subst ~metasenv [] ty_te ty) then
        raise (TypeCheckerFailure (lazy (Printf.sprintf
         "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 +1201,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")))