src/Pure/General/basics.ML
changeset 21394 9f20604d2b5e
child 22935 c6689e15bc98
equal deleted inserted replaced
21393:c648e24fd7ee 21394:9f20604d2b5e
       
     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 dest: 'a list -> 'a * 'a list
       
    43   val append: 'a list -> 'a list -> 'a list
       
    44   val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
       
    45   val fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
       
    46   val fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
       
    47   val unfold: int -> ('b -> 'a * 'b) -> 'b -> 'a list * 'b
       
    48   val unfold_rev: int -> ('b -> 'a * 'b) -> 'b -> 'a list * 'b
       
    49 end;
       
    50 
       
    51 structure Basics: BASICS =
       
    52 struct
       
    53 
       
    54 (* functions *)
       
    55 
       
    56 (*application and structured results*)
       
    57 fun x |> f = f x;
       
    58 fun (x, y) |-> f = f x y;
       
    59 fun (x, y) |>> f = (f x, y);
       
    60 fun (x, y) ||> f = (x, f y);
       
    61 fun (x, y) ||>> f = let val (z, y') = f y in ((x, z), y') end;
       
    62 
       
    63 (*composition and structured results*)
       
    64 fun (f #> g) x   = x |> f |> g;
       
    65 fun (f #-> g) x  = x |> f |-> g;
       
    66 fun (f #>> g) x  = x |> f |>> g;
       
    67 fun (f ##> g) x  = x |> f ||> g;
       
    68 fun (f ##>> g) x = x |> f ||>> g;
       
    69 
       
    70 (*result views*)
       
    71 fun `f = fn x => (f x, x);
       
    72 fun tap f = fn x => (f x; x);
       
    73 
       
    74 
       
    75 (* options *)
       
    76 
       
    77 fun is_some (SOME _) = true
       
    78   | is_some NONE = false;
       
    79 
       
    80 fun is_none (SOME _) = false
       
    81   | is_none NONE = true;
       
    82 
       
    83 fun the (SOME x) = x
       
    84   | the NONE = raise Option;
       
    85 
       
    86 fun these (SOME x) = x
       
    87   | these _ = [];
       
    88 
       
    89 fun the_list (SOME x) = [x]
       
    90   | the_list _ = []
       
    91 
       
    92 fun the_default x (SOME y) = y
       
    93   | the_default x _ = x;
       
    94 
       
    95 fun perhaps f x = the_default x (f x);
       
    96 
       
    97 
       
    98 (* partiality *)
       
    99 
       
   100 exception Interrupt = Interrupt;   (*signals intruding execution :-[*)
       
   101 
       
   102 fun try f x = SOME (f x)
       
   103   handle Interrupt => raise Interrupt | _ => NONE;
       
   104 
       
   105 fun can f x = is_some (try f x);
       
   106 
       
   107 
       
   108 (* lists *)
       
   109 
       
   110 fun cons x xs = x :: xs;
       
   111 
       
   112 fun dest (x :: xs) = (x, xs)
       
   113   | dest [] = raise Empty;
       
   114 
       
   115 fun append xs ys = xs @ ys;
       
   116 
       
   117 
       
   118 (* fold *)
       
   119 
       
   120 fun fold f =
       
   121   let
       
   122     fun fld [] y = y
       
   123       | fld (x :: xs) y = fld xs (f x y);
       
   124   in fld end;
       
   125 
       
   126 fun fold_rev f =
       
   127   let
       
   128     fun fld [] y = y
       
   129       | fld (x :: xs) y = f x (fld xs y);
       
   130   in fld end;
       
   131 
       
   132 fun fold_map f =
       
   133   let
       
   134     fun fld [] y = ([], y)
       
   135       | fld (x :: xs) y =
       
   136           let
       
   137             val (x', y') = f x y;
       
   138             val (xs', y'') = fld xs y';
       
   139           in (x' :: xs', y'') end;
       
   140   in fld end;
       
   141 
       
   142 
       
   143 (* unfold -- with optional limit *)
       
   144 
       
   145 fun unfold lim f =
       
   146   let
       
   147     fun unfld 0 ys x = (ys, x)
       
   148       | unfld n ys x =
       
   149           (case try f x of
       
   150             NONE => (ys, x)
       
   151           | SOME (y, x') => unfld (n - 1) (y :: ys) x');
       
   152   in unfld lim [] end;
       
   153 
       
   154 fun unfold_rev lim f =
       
   155   let
       
   156     fun unfld 0 x = ([], x)
       
   157       | unfld n x =
       
   158           (case try f x of
       
   159             NONE => ([], x)
       
   160           | SOME (y, x') => unfld (n - 1) x' |>> cons y);
       
   161   in unfld lim end;
       
   162 
       
   163 end;
       
   164 
       
   165 open Basics;