src/Pure/General/same.ML
author wenzelm
Thu Jul 16 22:54:39 2009 +0200 (2009-07-16 ago)
changeset 32025 e8fbfa84c23f
parent 32022 c2f4ee07647f
permissions -rw-r--r--
added same;
wenzelm@32015
     1
(*  Title:      Pure/General/same.ML
wenzelm@32015
     2
    Author:     Makarius
wenzelm@32015
     3
wenzelm@32015
     4
Support for copy-avoiding functions on pure values, at the cost of
wenzelm@32015
     5
readability.
wenzelm@32015
     6
*)
wenzelm@32015
     7
wenzelm@32015
     8
signature SAME =
wenzelm@32015
     9
sig
wenzelm@32015
    10
  exception SAME
wenzelm@32015
    11
  type ('a, 'b) function = 'a -> 'b  (*exception SAME*)
wenzelm@32015
    12
  type 'a operation = ('a, 'a) function  (*exception SAME*)
wenzelm@32025
    13
  val same: ('a, 'b) function
wenzelm@32015
    14
  val commit: 'a operation -> 'a -> 'a
wenzelm@32015
    15
  val function: ('a -> 'b option) -> ('a, 'b) function
wenzelm@32015
    16
  val capture: ('a, 'b) function -> 'a -> 'b option
wenzelm@32017
    17
  val map: 'a operation -> 'a list operation
wenzelm@32022
    18
  val map_option: ('a, 'b) function -> ('a option, 'b option) function
wenzelm@32015
    19
end;
wenzelm@32015
    20
wenzelm@32015
    21
structure Same: SAME =
wenzelm@32015
    22
struct
wenzelm@32015
    23
wenzelm@32015
    24
exception SAME;
wenzelm@32015
    25
wenzelm@32015
    26
type ('a, 'b) function = 'a -> 'b;
wenzelm@32015
    27
type 'a operation = ('a, 'a) function;
wenzelm@32015
    28
wenzelm@32025
    29
fun same _ = raise SAME;
wenzelm@32015
    30
fun commit f x = f x handle SAME => x;
wenzelm@32015
    31
wenzelm@32015
    32
fun capture f x = SOME (f x) handle SAME => NONE;
wenzelm@32015
    33
wenzelm@32015
    34
fun function f x =
wenzelm@32015
    35
  (case f x of
wenzelm@32015
    36
    NONE => raise SAME
wenzelm@32015
    37
  | SOME y => y);
wenzelm@32015
    38
wenzelm@32017
    39
fun map f [] = raise SAME
wenzelm@32017
    40
  | map f (x :: xs) = (f x :: commit (map f) xs handle SAME => x :: map f xs);
wenzelm@32015
    41
wenzelm@32022
    42
fun map_option f NONE = raise SAME
wenzelm@32022
    43
  | map_option f (SOME x) = SOME (f x);
wenzelm@32022
    44
wenzelm@32015
    45
end;