added if_none, parents, commas, gen_duplicates, duplicates, assoc2;
authorwenzelm
Thu Feb 03 13:56:15 1994 +0100 (1994-02-03)
changeset 255ee132db91681
parent 254 b1fcd27fcac4
child 256 b401c3d06024
added if_none, parents, commas, gen_duplicates, duplicates, assoc2;
changed cat_lines: no final "\n";
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Thu Feb 03 13:55:42 1994 +0100
     1.2 +++ b/src/Pure/library.ML	Thu Feb 03 13:56:15 1994 +0100
     1.3 @@ -45,6 +45,9 @@
     1.4  fun the (Some x) = x
     1.5    | the None = raise OPTION "the";
     1.6  
     1.7 +fun if_none None y = y
     1.8 +  | if_none (Some x) _ = x;
     1.9 +
    1.10  fun is_some (Some _) = true
    1.11    | is_some None = false;
    1.12  
    1.13 @@ -256,7 +259,6 @@
    1.14  fun split_list (l: ('a * 'b) list) = (map #1 l, map #2 l);
    1.15  
    1.16  
    1.17 -
    1.18  (* prefixes, suffixes *)
    1.19  
    1.20  infix prefix;
    1.21 @@ -268,8 +270,8 @@
    1.22     where xi is the first element that does not satisfy the predicate*)
    1.23  fun take_prefix (pred : 'a -> bool)  (xs: 'a list) : 'a list * 'a list =
    1.24    let fun take (rxs, []) = (rev rxs, [])
    1.25 -        | take (rxs, x::xs) =
    1.26 -            if  pred x  then  take(x::rxs, xs)  else  (rev rxs, x::xs)
    1.27 +        | take (rxs, x :: xs) =
    1.28 +            if  pred x  then  take(x :: rxs, xs)  else  (rev rxs, x :: xs)
    1.29    in  take([], xs)  end;
    1.30  
    1.31  (* [x1, ..., xi, ..., xn]  --->  ([x1, ..., xi], [x(i+1), ..., xn])
    1.32 @@ -374,14 +376,19 @@
    1.33    in implode o (map lower) o explode end;
    1.34  
    1.35  
    1.36 +(*parentesize*)
    1.37 +fun parents lpar rpar str = lpar ^ str ^ rpar;
    1.38 +
    1.39  (*simple quoting (does not escape special chars)*)
    1.40 -fun quote s = "\"" ^ s ^ "\"";
    1.41 +val quote = parents "\"" "\"";
    1.42  
    1.43  (*space_implode "..." (explode "hello"); gives "h...e...l...l...o"*)
    1.44  fun space_implode a bs = implode (separate a bs);
    1.45  
    1.46 +val commas = space_implode ", ";
    1.47 +
    1.48  (*concatenate messages, one per line, into a string*)
    1.49 -val cat_lines = implode o (map (apr (op ^, "\n")));
    1.50 +val cat_lines = space_implode "\n";
    1.51  
    1.52  
    1.53  
    1.54 @@ -468,6 +475,24 @@
    1.55    | findrep (x :: xs) = if x mem xs then x :: xs else findrep xs;
    1.56  
    1.57  
    1.58 +(*returns a list containing all repeated elements exactly once; preserves
    1.59 +  order, takes first of equal elements*)
    1.60 +fun gen_duplicates eq lst =
    1.61 +  let
    1.62 +    val memb = gen_mem eq;
    1.63 +
    1.64 +    fun dups (rev_dups, []) = rev rev_dups
    1.65 +      | dups (rev_dups, x :: xs) =
    1.66 +          if memb (x, rev_dups) orelse not (memb (x, xs)) then
    1.67 +            dups (rev_dups, xs)
    1.68 +          else dups (x :: rev_dups, xs);
    1.69 +  in
    1.70 +    dups ([], lst)
    1.71 +  end;
    1.72 +
    1.73 +val duplicates = gen_duplicates (op =);
    1.74 +
    1.75 +
    1.76  
    1.77  (** association lists **)
    1.78  
    1.79 @@ -481,6 +506,12 @@
    1.80      None => []
    1.81    | Some ys => ys);
    1.82  
    1.83 +(*two-fold association list lookup*)
    1.84 +fun assoc2 (aal, (key1, key2)) =
    1.85 +  (case assoc (aal, key1) of
    1.86 +    Some al => assoc (al, key2)
    1.87 +  | None => None);
    1.88 +
    1.89  (*generalized association list lookup*)
    1.90  fun gen_assoc eq ([], key) = None
    1.91    | gen_assoc eq ((keyi, xi) :: pairs, key) =