Swapped arguments in error message.

[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 125b66ed35cbd73a945a20a99f4d9d90df1dd8ac..dfb014c20d8ada6c609823153632d701b299cee2 100644 (file)
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -557,9 +557,12 @@ let eat_prods ~subst ~metasenv context he ty_he args_with_ty =
             raise 
               (TypeCheckerFailure 
                 (lazy (Printf.sprintf
-                  ("Appl: wrong parameter-type, expected\n%s\nfound\n%s")
-                  (NCicPp.ppterm ~subst ~metasenv ~context s)
-                  (NCicPp.ppterm ~subst ~metasenv ~context ty_arg))))
+                  ("Appl: wrong application of %s: the parameter %s has type"^^
+                   "\n%s\nbut is should have type \n%s\n")
+                  (NCicPp.ppterm ~subst ~metasenv ~context he)
+                  (NCicPp.ppterm ~subst ~metasenv ~context arg)
+                  (NCicPp.ppterm ~subst ~metasenv ~context ty_arg)
+                  (NCicPp.ppterm ~subst ~metasenv ~context s))))
        | _ ->
           raise 
             (TypeCheckerFailure
@@ -678,11 +681,11 @@ 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"))
@@ -719,9 +722,8 @@ let rec typeof ~subst ~metasenv context term =
         if parameters = [] then C.Const r
         else C.Appl ((C.Const r)::parameters) in
       let type_of_sort_of_ind_ty = typeof_aux context sort_of_ind_type in
-      if not (check_allowed_sort_elimination ~subst ~metasenv r context
-          sort_of_ind_type type_of_sort_of_ind_ty outsort)
-      then raise (TypeCheckerFailure (lazy ("Sort elimination not allowed")));
+      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
@@ -904,27 +906,41 @@ let rec typeof ~subst ~metasenv context term =
     let arity2 = R.whd ~subst context arity2 in
       match arity1,arity2 with
        | C.Prod (name,so1,de1), C.Prod (_,so2,de2) ->
-          R.are_convertible ~subst ~metasenv context so1 so2 &&
-           aux ((name, C.Decl so1)::context)
-            (mkapp (S.lift 1 ind) (C.Rel 1)) de1 de2
+          if not (R.are_convertible ~subst ~metasenv context so1 so2) then
+           raise (TypeCheckerFailure (lazy (Printf.sprintf
+            "In outtype: expected %s, found %s"
+            (NCicPp.ppterm ~subst ~metasenv ~context so1)
+            (NCicPp.ppterm ~subst ~metasenv ~context so2)
+            )));
+          aux ((name, C.Decl so1)::context)
+           (mkapp (S.lift 1 ind) (C.Rel 1)) de1 de2
        | C.Sort _, C.Prod (name,so,ta) ->
-        (R.are_convertible ~subst ~metasenv context so ind &&
-          match arity1,ta with
-          | (C.Sort (C.CProp | C.Type _), C.Sort _)
-          | (C.Sort C.Prop, C.Sort C.Prop) -> true
-          | (C.Sort C.Prop, C.Sort (C.CProp | C.Type _)) ->
-              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
-              let cl_len = List.length cl in
-               (* is it a singleton or empty non recursive and non informative
-                  definition? *)
-               cl_len = 0 ||
-                (itl_len = 1 && cl_len = 1 &&
-                 is_non_informative [name,C.Decl ty] leftno
-                  (let _,_,x = List.nth cl 0 in x))
-          | _,_ -> false)
-       | _,_ -> false
+          if not (R.are_convertible ~subst ~metasenv context so ind) then
+           raise (TypeCheckerFailure (lazy (Printf.sprintf
+            "In outtype: expected %s, found %s"
+            (NCicPp.ppterm ~subst ~metasenv ~context ind)
+            (NCicPp.ppterm ~subst ~metasenv ~context so)
+            )));
+          (match arity1,ta with
+            | (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 _)) ->
+                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
+                let cl_len = List.length cl in
+                 (* is it a singleton or empty non recursive and non informative
+                    definition? *)
+                 if not
+                  (cl_len = 0 ||
+                   (itl_len = 1 && cl_len = 1 &&
+                    is_non_informative [name,C.Decl ty] leftno
+                     (let _,_,x = List.nth cl 0 in x)))
+                 then
+                  raise (TypeCheckerFailure (lazy
+                   ("Sort elimination not allowed")));
+          | _,_ -> ())
+       | _,_ -> ()
    in
     aux 
 
@@ -1051,7 +1067,7 @@ and guarded_by_destructors ~subst ~metasenv context recfuns t =
        ) fl true
 *)
 
-and guarded_by_constructors ~subst _ _ _ _ _ _ _ = assert false
+and guarded_by_constructors ~subst ~metasenv _ _ _ _ _ _ _ = true
 
 and recursive_args ~subst ~metasenv context n nn te =
   match R.whd context te with