src/Pure/General/same.ML
author wenzelm
Fri Nov 25 18:37:14 2011 +0100 (2011-11-25 ago)
changeset 45633 2cb7e34f6096
parent 32025 e8fbfa84c23f
permissions -rw-r--r--
retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
     1 (*  Title:      Pure/General/same.ML
     2     Author:     Makarius
     3 
     4 Support for copy-avoiding functions on pure values, at the cost of
     5 readability.
     6 *)
     7 
     8 signature SAME =
     9 sig
    10   exception SAME
    11   type ('a, 'b) function = 'a -> 'b  (*exception SAME*)
    12   type 'a operation = ('a, 'a) function  (*exception SAME*)
    13   val same: ('a, 'b) function
    14   val commit: 'a operation -> 'a -> 'a
    15   val function: ('a -> 'b option) -> ('a, 'b) function
    16   val capture: ('a, 'b) function -> 'a -> 'b option
    17   val map: 'a operation -> 'a list operation
    18   val map_option: ('a, 'b) function -> ('a option, 'b option) function
    19 end;
    20 
    21 structure Same: SAME =
    22 struct
    23 
    24 exception SAME;
    25 
    26 type ('a, 'b) function = 'a -> 'b;
    27 type 'a operation = ('a, 'a) function;
    28 
    29 fun same _ = raise SAME;
    30 fun commit f x = f x handle SAME => x;
    31 
    32 fun capture f x = SOME (f x) handle SAME => NONE;
    33 
    34 fun function f x =
    35   (case f x of
    36     NONE => raise SAME
    37   | SOME y => y);
    38 
    39 fun map f [] = raise SAME
    40   | map f (x :: xs) = (f x :: commit (map f) xs handle SAME => x :: map f xs);
    41 
    42 fun map_option f NONE = raise SAME
    43   | map_option f (SOME x) = SOME (f x);
    44 
    45 end;