# HG changeset patch
# User bulwahn
# Date 1285246215 -7200
# Node ID 2e06dad03dd32ecaa38210ebcd3071e759df955e
# Parent  2a35950ec49523890f33320eb15170b31cee9bad
adding check if user-given modes match type of predicates; removed useless function expand_tuples_elim

diff -r 2a35950ec495 -r 2e06dad03dd3 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Sep 23 14:50:14 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Sep 23 14:50:15 2010 +0200
@@ -427,6 +427,26 @@
       | NONE => ())
   | NONE => ()) preds
 
+fun check_matches_type ctxt predname T ms =
+  let
+    fun check (m as Fun (m1, m2)) (Type("fun", [T1,T2])) = check m1 T1 andalso check m2 T2
+      | check m (Type("fun", _)) = false
+      | check (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) =
+          check m1 T1 andalso check m2 T2 
+      | check Input T = true
+      | check Output T = true
+      | check Bool @{typ bool} = true
+      | check _ _ = false
+    val _ = map
+      (fn mode =>
+        if (forall (uncurry check) (strip_fun_mode mode ~~ binder_types T)) then ()
+        else error (string_of_mode mode ^ " is not a valid mode for " ^ Syntax.string_of_typ ctxt T
+        ^ " at predicate " ^ predname)) ms
+  in
+    ms
+  end
+
+
 (* importing introduction rules *)
 
 fun unify_consts thy cs intr_ts =
@@ -633,8 +653,6 @@
     Thm.equal_elim eq elimrule |> singleton (Variable.export ctxt' ctxt)
   end;
 
-fun expand_tuples_elim th = th
-
 val no_compilation = ([], ([], []))
 
 fun fetch_pred_data ctxt name =
@@ -2679,7 +2697,7 @@
     val all_modes = 
       map (fn (s, T) =>
         (s, case proposed_modes options s of
-            SOME ms => ms
+            SOME ms => check_matches_type ctxt s T ms
           | NONE => generate_modes s T)) preds
     val params =
       case intrs of