adding order on modes
authorbulwahn
Mon Sep 13 16:44:18 2010 +0200 (2010-09-13)
changeset 393112bd067f80b92
parent 39310 17ef4415b17c
child 39312 968c33be5c96
adding order on modes
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Sep 13 16:44:17 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Mon Sep 13 16:44:18 2010 +0200
     1.3 @@ -15,6 +15,7 @@
     1.4    (* mode *)
     1.5    datatype mode = Bool | Input | Output | Pair of mode * mode | Fun of mode * mode
     1.6    val eq_mode : mode * mode -> bool
     1.7 +  val mode_ord: mode * mode -> order
     1.8    val list_fun_mode : mode list -> mode
     1.9    val strip_fun_mode : mode -> mode list
    1.10    val dest_fun_mode : mode -> mode list
    1.11 @@ -187,6 +188,14 @@
    1.12    | eq_mode (Bool, Bool) = true
    1.13    | eq_mode _ = false
    1.14  
    1.15 +fun mode_ord (Input, Output) = LESS
    1.16 +  | mode_ord (Output, Input) = GREATER
    1.17 +  | mode_ord (Input, Input) = EQUAL
    1.18 +  | mode_ord (Output, Output) = EQUAL
    1.19 +  | mode_ord (Bool, Bool) = EQUAL
    1.20 +  | mode_ord (Pair (m1, m2), Pair (m3, m4)) = prod_ord mode_ord mode_ord ((m1, m2), (m3, m4))
    1.21 +  | mode_ord (Fun (m1, m2), Fun (m3, m4)) = prod_ord mode_ord mode_ord ((m1, m2), (m3, m4))
    1.22 + 
    1.23  fun list_fun_mode [] = Bool
    1.24    | list_fun_mode (m :: ms) = Fun (m, list_fun_mode ms)
    1.25