src/Pure/General/same.ML
author wenzelm
Thu Jul 16 16:24:49 2009 +0200 (2009-07-16 ago)
changeset 32015 7101feb5247e
child 32017 e91a3acf8383
permissions -rw-r--r--
Support for copy-avoiding functions on pure values, at the cost of readability.
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@32015
    13
  val commit: 'a operation -> 'a -> 'a
wenzelm@32015
    14
  val function: ('a -> 'b option) -> ('a, 'b) function
wenzelm@32015
    15
  val capture: ('a, 'b) function -> 'a -> 'b option
wenzelm@32015
    16
end;
wenzelm@32015
    17
wenzelm@32015
    18
structure Same: SAME =
wenzelm@32015
    19
struct
wenzelm@32015
    20
wenzelm@32015
    21
exception SAME;
wenzelm@32015
    22
wenzelm@32015
    23
type ('a, 'b) function = 'a -> 'b;
wenzelm@32015
    24
type 'a operation = ('a, 'a) function;
wenzelm@32015
    25
wenzelm@32015
    26
fun commit f x = f x handle SAME => x;
wenzelm@32015
    27
wenzelm@32015
    28
fun capture f x = SOME (f x) handle SAME => NONE;
wenzelm@32015
    29
wenzelm@32015
    30
fun function f x =
wenzelm@32015
    31
  (case f x of
wenzelm@32015
    32
    NONE => raise SAME
wenzelm@32015
    33
  | SOME y => y);
wenzelm@32015
    34
wenzelm@32015
    35
wenzelm@32015
    36
end;