--- 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