src/Pure/General/basics.ML
author wenzelm
Thu Jul 19 23:18:48 2007 +0200 (2007-07-19)
changeset 23863 8f3099589cfa
parent 23559 0de527730294
child 28443 de653f1ad78b
permissions -rw-r--r--
tuned signature;
     1 (*  Title:      Pure/General/basics.ML
     2     ID:         $Id$
     3     Author:     Florian Haftmann and Makarius, TU Muenchen
     4 
     5 Fundamental concepts.
     6 *)
     7 
     8 infix 1 |> |-> |>> ||> ||>>
     9 infix 1 #> #-> #>> ##> ##>>
    10 
    11 signature BASICS =
    12 sig
    13   (*functions*)
    14   val |> : 'a * ('a -> 'b) -> 'b
    15   val |-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b
    16   val |>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c
    17   val ||> : ('c * 'a) * ('a -> 'b) -> 'c * 'b
    18   val ||>> : ('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b
    19   val #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c
    20   val #-> : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd
    21   val #>> : ('a -> 'c * 'b) * ('c -> 'd) -> 'a -> 'd * 'b
    22   val ##> : ('a -> 'c * 'b) * ('b -> 'd) -> 'a -> 'c * 'd
    23   val ##>> : ('a -> 'c * 'b) * ('b -> 'e * 'd) -> 'a -> ('c * 'e) * 'd
    24   val ` : ('b -> 'a) -> 'b -> 'a * 'b
    25   val tap: ('b -> 'a) -> 'b -> 'b
    26 
    27   (*options*)
    28   val is_some: 'a option -> bool
    29   val is_none: 'a option -> bool
    30   val the: 'a option -> 'a
    31   val these: 'a list option -> 'a list
    32   val the_list: 'a option -> 'a list
    33   val the_default: 'a -> 'a option -> 'a
    34   val perhaps: ('a -> 'a option) -> 'a -> 'a
    35 
    36   (*partiality*)
    37   val try: ('a -> 'b) -> 'a -> 'b option
    38   val can: ('a -> 'b) -> 'a -> bool
    39 
    40   (*lists*)
    41   val cons: 'a -> 'a list -> 'a list
    42   val append: 'a list -> 'a list -> 'a list
    43   val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
    44   val fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
    45   val fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
    46 end;
    47 
    48 structure Basics: BASICS =
    49 struct
    50 
    51 (* functions *)
    52 
    53 (*application and structured results*)
    54 fun x |> f = f x;
    55 fun (x, y) |-> f = f x y;
    56 fun (x, y) |>> f = (f x, y);
    57 fun (x, y) ||> f = (x, f y);
    58 fun (x, y) ||>> f = let val (z, y') = f y in ((x, z), y') end;
    59 
    60 (*composition and structured results*)
    61 fun (f #> g) x   = x |> f |> g;
    62 fun (f #-> g) x  = x |> f |-> g;
    63 fun (f #>> g) x  = x |> f |>> g;
    64 fun (f ##> g) x  = x |> f ||> g;
    65 fun (f ##>> g) x = x |> f ||>> g;
    66 
    67 (*result views*)
    68 fun `f = fn x => (f x, x);
    69 fun tap f = fn x => (f x; x);
    70 
    71 
    72 (* options *)
    73 
    74 fun is_some (SOME _) = true
    75   | is_some NONE = false;
    76 
    77 fun is_none (SOME _) = false
    78   | is_none NONE = true;
    79 
    80 fun the (SOME x) = x
    81   | the NONE = raise Option;
    82 
    83 fun these (SOME x) = x
    84   | these NONE = [];
    85 
    86 fun the_list (SOME x) = [x]
    87   | the_list NONE = []
    88 
    89 fun the_default x (SOME y) = y
    90   | the_default x NONE = x;
    91 
    92 fun perhaps f x = the_default x (f x);
    93 
    94 
    95 (* partiality *)
    96 
    97 fun try f x = SOME (f x)
    98   handle Interrupt => raise Interrupt | _ => NONE;
    99 
   100 fun can f x = is_some (try f x);
   101 
   102 
   103 (* lists *)
   104 
   105 fun cons x xs = x :: xs;
   106 
   107 fun append xs ys = xs @ ys;
   108 
   109 fun fold _ [] y = y
   110   | fold f (x :: xs) y = fold f xs (f x y);
   111 
   112 fun fold_rev _ [] y = y
   113   | fold_rev f (x :: xs) y = f x (fold_rev f xs y);
   114 
   115 fun fold_map _ [] y = ([], y)
   116   | fold_map f (x :: xs) y =
   117       let
   118         val (x', y') = f x y;
   119         val (xs', y'') = fold_map f xs y';
   120       in (x' :: xs', y'') end;
   121 
   122 end;
   123 
   124 open Basics;