X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicTypeChecker.ml;h=9de1f0f5c27203258e4512d6bab0a5e9b8f7598d;hb=ccb09743430d585f773eb83ad9a18d1dbdda07ed;hp=3d0f13e2b582440fcc99af9ef83b78411d06acb0;hpb=97b4064d9c578ba0e944282d5b465419488dbd33;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 3d0f13e2b..9de1f0f5c 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -558,11 +558,11 @@ let eat_prods ~subst ~metasenv context he ty_he args_with_ty =
               (TypeCheckerFailure 
                 (lazy (Printf.sprintf
                   ("Appl: wrong application of %s: the parameter %s has type"^^
-                   "\n%s\nbut is should have type \n%s\n")
+                   "\n%s\nbut it should have type \n%s\n")
                   (NCicPp.ppterm ~subst ~metasenv ~context he)
                   (NCicPp.ppterm ~subst ~metasenv ~context arg)
-                  (NCicPp.ppterm ~subst ~metasenv ~context s)
-                  (NCicPp.ppterm ~subst ~metasenv ~context ty_arg))))
+                  (NCicPp.ppterm ~subst ~metasenv ~context ty_arg)
+                  (NCicPp.ppterm ~subst ~metasenv ~context s))))
        | _ ->
           raise 
             (TypeCheckerFailure
@@ -681,17 +681,20 @@ let rec typeof ~subst ~metasenv context term =
        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 ("HEAD: " ^ NCicPp.ppterm ~subst ~metasenv ~context ty_he);
        prerr_endline ("TARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm
-       ~context) (List.map snd args_with_ty)));
+       ~subst ~metasenv ~context) (List.map snd args_with_ty)));
        prerr_endline ("ARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm
-       ~context) (List.map fst args_with_ty)));
+       ~subst ~metasenv ~context) (List.map fst args_with_ty)));
 *)
        eat_prods ~subst ~metasenv context he ty_he args_with_ty
    | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
    | C.Match (Ref.Ref (_,_,Ref.Ind tyno) as r,outtype,term,pl) ->
       let outsort = typeof_aux context outtype in
-      let leftno = E.get_indty_leftno r in
+      let inductive,leftno,itl,_,_ = E.get_checked_indtys r in
+      let constructorsno =
+        let _,_,_,cl = List.nth itl tyno in List.length cl
+      in
       let parameters, arguments =
         let ty = R.whd ~subst context (typeof_aux context term) in
         let r',tl =
@@ -725,12 +728,6 @@ let rec typeof ~subst ~metasenv context term =
       check_allowed_sort_elimination ~subst ~metasenv r context
        sort_of_ind_type type_of_sort_of_ind_ty outsort;
       (* let's check if the type of branches are right *)
-      let leftno,constructorsno =
-        let inductive,leftno,itl,_,i = E.get_checked_indtys r in
-        let _,name,ty,cl = List.nth itl i in
-        let cl_len = List.length cl in
-        leftno, cl_len
-      in
       if List.length pl <> constructorsno then
        raise (TypeCheckerFailure (lazy ("Wrong number of cases in a match")));
       let j,branches_ok,p_ty, exp_p_ty =
@@ -925,6 +922,8 @@ let rec typeof ~subst ~metasenv context term =
             | (C.Sort (C.CProp | C.Type _), C.Sort _)
             | (C.Sort C.Prop, C.Sort C.Prop) -> ()
             | (C.Sort C.Prop, C.Sort (C.CProp | C.Type _)) ->
+        (* TODO: we should pass all these parameters since we
+         * have them already *)
                 let inductive,leftno,itl,_,i = E.get_checked_indtys r in
                 let itl_len = List.length itl in
                 let _,name,ty,cl = List.nth itl i in
@@ -952,7 +951,7 @@ and check_mutual_inductive_defs uri ~metasenv ~subst is_ind leftno tyl =
   List.iter (fun (_,_,x,_) -> ignore (typeof ~subst ~metasenv [] x)) tyl;
   (* let's check if the types of the inductive constructors are well formed. *)
   let len = List.length tyl in
-  let tys = List.map (fun (_,n,ty,_) -> (n,(C.Decl ty))) tyl in
+  let tys = List.rev (List.map (fun (_,n,ty,_) -> (n,(C.Decl ty))) tyl) in
   ignore
    (List.fold_right
     (fun (_,_,_,cl) i ->
@@ -1168,8 +1167,6 @@ and type_of_constant ((Ref.Ref (_,uri,_)) as ref) =
        check_obj_well_typed uobj;
        E.add_obj uobj;
        !logger (`Type_checking_completed uri);
-       if not (fst (E.get_obj uri)) then
-         raise (AssertFailure (lazy "environment error"));
        uobj
   in
   match cobj, ref with