removed rev_append;
authorwenzelm
Tue May 17 10:08:24 2005 +0200 (2005-05-17)
changeset 15970b8855873d234
parent 15969 201f6738480f
child 15971 c0c4088edccf
removed rev_append;
tuned presentation of datatype option: removed apsome, export the and if_none;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Tue May 17 10:08:24 2005 +0200
     1.2 +++ b/src/Pure/library.ML	Tue May 17 10:08:24 2005 +0200
     1.3 @@ -35,13 +35,16 @@
     1.4    type stamp
     1.5    val stamp: unit -> stamp
     1.6  
     1.7 -  (*options*)
     1.8 -  val is_none: 'a option -> bool
     1.9 -
    1.10    (*old options -- invalidated*)
    1.11    datatype invalid = None of invalid
    1.12    exception OPTION of invalid
    1.13  
    1.14 +  (*options*)
    1.15 +  val the: 'a option -> 'a
    1.16 +  val if_none: 'a option -> 'a -> 'a
    1.17 +  val is_some: 'a option -> bool
    1.18 +  val is_none: 'a option -> bool
    1.19 +
    1.20    exception ERROR
    1.21    val try: ('a -> 'b) -> 'a -> 'b option
    1.22    val can: ('a -> 'b) -> 'a -> bool
    1.23 @@ -262,13 +265,6 @@
    1.24  signature LIBRARY =
    1.25  sig
    1.26    include BASIC_LIBRARY
    1.27 -
    1.28 -  val the: 'a option -> 'a
    1.29 -  val if_none: 'a option -> 'a -> 'a
    1.30 -  val is_some: 'a option -> bool
    1.31 -  val apsome: ('a -> 'b) -> 'a option -> 'b option
    1.32 -
    1.33 -  val rev_append: 'a list -> 'a list -> 'a list
    1.34    val foldl: ('a * 'b -> 'a) -> 'a * 'b list -> 'a
    1.35    val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b
    1.36    val take: int * 'a list -> 'a list
    1.37 @@ -325,16 +321,22 @@
    1.38  
    1.39  (** options **)
    1.40  
    1.41 -val the = valOf;
    1.42 -fun if_none opt a = getOpt (opt, a);
    1.43 -val is_some = isSome;
    1.44 -fun is_none opt = not (isSome opt);
    1.45 -val apsome = Option.map;
    1.46 -
    1.47  (*invalidate former constructors to prevent accidental use as match-all patterns!*)
    1.48  datatype invalid = None of invalid;
    1.49  exception OPTION of invalid;
    1.50  
    1.51 +val the = Option.valOf;
    1.52 +
    1.53 +(*strict!*)
    1.54 +fun if_none NONE y = y
    1.55 +  | if_none (SOME x) _ = x;
    1.56 +
    1.57 +fun is_some (SOME _) = true
    1.58 +  | is_some NONE = false;
    1.59 +
    1.60 +fun is_none (SOME _) = false
    1.61 +  | is_none NONE = true;
    1.62 +
    1.63  
    1.64  (* exception handling *)
    1.65  
    1.66 @@ -446,8 +448,6 @@
    1.67  
    1.68  fun append xs ys = xs @ ys;
    1.69  
    1.70 -fun rev_append xs ys = List.revAppend (xs, ys);
    1.71 -
    1.72  fun apply [] x = x
    1.73    | apply (f :: fs) x = apply fs (f x);
    1.74