src/Pure/library.ML
changeset 17153 d871853e13e0
parent 17141 4b0dc89de43b
child 17257 0ab67cb765da
     1.1 --- a/src/Pure/library.ML	Sun Aug 28 09:02:42 2005 +0200
     1.2 +++ b/src/Pure/library.ML	Sun Aug 28 09:18:22 2005 +0200
     1.3 @@ -48,6 +48,7 @@
     1.4  
     1.5    (*options*)
     1.6    val the: 'a option -> 'a
     1.7 +  val these: 'a list option -> 'a list
     1.8    val if_none: 'a option -> 'a -> 'a
     1.9    val is_some: 'a option -> bool
    1.10    val is_none: 'a option -> bool
    1.11 @@ -220,13 +221,12 @@
    1.12    val duplicates: ''a list -> ''a list
    1.13    val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool
    1.14  
    1.15 -  (*association lists*)
    1.16 +  (*association lists -- see also Pure/General/alist.ML*)
    1.17    val assoc: (''a * 'b) list * ''a -> 'b option
    1.18    val assoc_int: (int * 'a) list * int -> 'a option
    1.19    val assoc_string: (string * 'a) list * string -> 'a option
    1.20    val assoc_string_int: ((string * int) * 'a) list * (string * int) -> 'a option
    1.21    val assocs: (''a * 'b list) list -> ''a -> 'b list
    1.22 -  val assoc2: (''a * (''b * 'c) list) list * (''a * ''b) -> 'c option
    1.23    val gen_assoc: ('a * 'b -> bool) -> ('b * 'c) list * 'a -> 'c option
    1.24    val overwrite: (''a * 'b) list * (''a * 'b) -> (''a * 'b) list
    1.25    val gen_overwrite: ('a * 'a -> bool) -> ('a * 'b) list * ('a * 'b) -> ('a * 'b) list
    1.26 @@ -353,6 +353,8 @@
    1.27  exception OPTION of invalid;
    1.28  
    1.29  val the = Option.valOf;
    1.30 +fun these (SOME x) = x
    1.31 +  | these _ = []
    1.32  
    1.33  (*strict!*)
    1.34  fun if_none NONE y = y
    1.35 @@ -1045,16 +1047,7 @@
    1.36    | assoc_string_int ((keyi, xi) :: pairs, key) =
    1.37        if key = keyi then SOME xi else assoc_string_int (pairs, key);
    1.38  
    1.39 -fun assocs ps x =
    1.40 -  (case assoc (ps, x) of
    1.41 -    NONE => []
    1.42 -  | SOME ys => ys);
    1.43 -
    1.44 -(*two-fold association list lookup*)
    1.45 -fun assoc2 (aal, (key1, key2)) =
    1.46 -  (case assoc (aal, key1) of
    1.47 -    SOME al => assoc (al, key2)
    1.48 -  | NONE => NONE);
    1.49 +fun assocs z = curry (these o assoc) z
    1.50  
    1.51  (*generalized association list lookup*)
    1.52  fun gen_assoc eq ([], key) = NONE