# HG changeset patch
# User bulwahn
# Date 1284389058 -7200
# Node ID 2bd067f80b92f1850e15512e2658b14581bd2897
# Parent  17ef4415b17c74bbdae3ca7319027e75a171d73e
adding order on modes

diff -r 17ef4415b17c -r 2bd067f80b92 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Sep 13 16:44:17 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Sep 13 16:44:18 2010 +0200
@@ -15,6 +15,7 @@
   (* mode *)
   datatype mode = Bool | Input | Output | Pair of mode * mode | Fun of mode * mode
   val eq_mode : mode * mode -> bool
+  val mode_ord: mode * mode -> order
   val list_fun_mode : mode list -> mode
   val strip_fun_mode : mode -> mode list
   val dest_fun_mode : mode -> mode list
@@ -187,6 +188,14 @@
   | eq_mode (Bool, Bool) = true
   | eq_mode _ = false
 
+fun mode_ord (Input, Output) = LESS
+  | mode_ord (Output, Input) = GREATER
+  | mode_ord (Input, Input) = EQUAL
+  | mode_ord (Output, Output) = EQUAL
+  | mode_ord (Bool, Bool) = EQUAL
+  | mode_ord (Pair (m1, m2), Pair (m3, m4)) = prod_ord mode_ord mode_ord ((m1, m2), (m3, m4))
+  | mode_ord (Fun (m1, m2), Fun (m3, m4)) = prod_ord mode_ord mode_ord ((m1, m2), (m3, m4))
+ 
 fun list_fun_mode [] = Bool
   | list_fun_mode (m :: ms) = Fun (m, list_fun_mode ms)