added member, option_ord;
authorwenzelm
Mon Jun 20 22:14:06 2005 +0200 (2005-06-20)
changeset 16492fbfd15412f05
parent 16491 7310d0a36599
child 16493 d0f6c33b2300
added member, option_ord;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Mon Jun 20 22:14:05 2005 +0200
     1.2 +++ b/src/Pure/library.ML	Mon Jun 20 22:14:06 2005 +0200
     1.3 @@ -166,7 +166,7 @@
     1.4    val replicate_string: int -> string -> string
     1.5    val translate_string: (string -> string) -> string -> string
     1.6  
     1.7 -  (*lists as sets*)
     1.8 +  (*lists as sets -- see also Pure/General/ord_list.ML*)
     1.9    val mem: ''a * ''a list -> bool
    1.10    val mem_int: int * int list -> bool
    1.11    val mem_string: string * string list -> bool
    1.12 @@ -175,6 +175,7 @@
    1.13    val ins_int: int * int list -> int list
    1.14    val ins_string: string * string list -> string list
    1.15    val gen_ins: ('a * 'a -> bool) -> 'a * 'a list -> 'a list
    1.16 +  val member: ('b * 'a -> bool) -> 'a list -> 'b -> bool
    1.17    val insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list
    1.18    val remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list
    1.19    val union: ''a list * ''a list -> ''a list
    1.20 @@ -231,6 +232,7 @@
    1.21    val make_ord: ('a * 'a -> bool) -> 'a * 'a -> order
    1.22    val int_ord: int * int -> order
    1.23    val string_ord: string * string -> order
    1.24 +  val option_ord: ('a * 'b -> order) -> 'a option * 'b option -> order
    1.25    val prod_ord: ('a * 'b -> order) -> ('c * 'd -> order) -> ('a * 'c) * ('b * 'd) -> order
    1.26    val dict_ord: ('a * 'b -> order) -> 'a list * 'b list -> order
    1.27    val list_ord: ('a * 'b -> order) -> 'a list * 'b list -> order
    1.28 @@ -817,7 +819,7 @@
    1.29  
    1.30  
    1.31  
    1.32 -(** lists as sets **)
    1.33 +(** lists as sets -- see also Pure/General/ord_list.ML **)
    1.34  
    1.35  (*membership in a list*)
    1.36  fun x mem [] = false
    1.37 @@ -835,7 +837,8 @@
    1.38  fun gen_mem eq (x, []) = false
    1.39    | gen_mem eq (x, y :: ys) = eq (x, y) orelse gen_mem eq (x, ys);
    1.40  
    1.41 -(*insert and remove*)
    1.42 +(*member, insert, and remove -- with canonical argument order*)
    1.43 +fun member eq xs x = gen_mem eq (x, xs);
    1.44  fun insert eq x xs = if gen_mem eq (x, xs) then xs else x :: xs;
    1.45  fun remove eq x xs = if gen_mem eq (x, xs) then filter_out (fn y => eq (x, y)) xs else xs;
    1.46  
    1.47 @@ -1085,6 +1088,11 @@
    1.48  val int_ord = Int.compare;
    1.49  val string_ord = String.compare;
    1.50  
    1.51 +fun option_ord ord (SOME x, SOME y) = ord (x, y)
    1.52 +  | option_ord _ (NONE, NONE) = EQUAL
    1.53 +  | option_ord _ (NONE, SOME _) = LESS
    1.54 +  | option_ord _ (SOME _, NONE) = GREATER;
    1.55 +
    1.56  (*lexicographic product*)
    1.57  fun prod_ord a_ord b_ord ((x, y), (x', y')) =
    1.58    (case a_ord (x, x') of EQUAL => b_ord (y, y') | ord => ord);