Support for copy-avoiding functions on pure values, at the cost of readability.
authorwenzelm
Thu Jul 16 16:24:49 2009 +0200 (2009-07-16)
changeset 320157101feb5247e
parent 32014 857367925493
child 32016 597b3b69b8d8
Support for copy-avoiding functions on pure values, at the cost of readability.
src/Pure/General/same.ML
src/Pure/IsaMakefile
src/Pure/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/General/same.ML	Thu Jul 16 16:24:49 2009 +0200
     1.3 @@ -0,0 +1,36 @@
     1.4 +(*  Title:      Pure/General/same.ML
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Support for copy-avoiding functions on pure values, at the cost of
     1.8 +readability.
     1.9 +*)
    1.10 +
    1.11 +signature SAME =
    1.12 +sig
    1.13 +  exception SAME
    1.14 +  type ('a, 'b) function = 'a -> 'b  (*exception SAME*)
    1.15 +  type 'a operation = ('a, 'a) function  (*exception SAME*)
    1.16 +  val commit: 'a operation -> 'a -> 'a
    1.17 +  val function: ('a -> 'b option) -> ('a, 'b) function
    1.18 +  val capture: ('a, 'b) function -> 'a -> 'b option
    1.19 +end;
    1.20 +
    1.21 +structure Same: SAME =
    1.22 +struct
    1.23 +
    1.24 +exception SAME;
    1.25 +
    1.26 +type ('a, 'b) function = 'a -> 'b;
    1.27 +type 'a operation = ('a, 'a) function;
    1.28 +
    1.29 +fun commit f x = f x handle SAME => x;
    1.30 +
    1.31 +fun capture f x = SOME (f x) handle SAME => NONE;
    1.32 +
    1.33 +fun function f x =
    1.34 +  (case f x of
    1.35 +    NONE => raise SAME
    1.36 +  | SOME y => y);
    1.37 +
    1.38 +
    1.39 +end;
     2.1 --- a/src/Pure/IsaMakefile	Thu Jul 16 00:24:11 2009 +0200
     2.2 +++ b/src/Pure/IsaMakefile	Thu Jul 16 16:24:49 2009 +0200
     2.3 @@ -52,12 +52,12 @@
     2.4    General/long_name.ML General/markup.ML General/name_space.ML		\
     2.5    General/ord_list.ML General/output.ML General/path.ML			\
     2.6    General/position.ML General/pretty.ML General/print_mode.ML		\
     2.7 -  General/properties.ML General/queue.ML General/scan.ML		\
     2.8 -  General/secure.ML General/seq.ML General/source.ML General/stack.ML	\
     2.9 -  General/symbol.ML General/symbol_pos.ML General/table.ML		\
    2.10 -  General/url.ML General/xml.ML General/yxml.ML Isar/args.ML		\
    2.11 -  Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML	\
    2.12 -  Isar/class_target.ML Isar/code.ML Isar/constdefs.ML			\
    2.13 +  General/properties.ML General/queue.ML General/same.ML		\
    2.14 +  General/scan.ML General/secure.ML General/seq.ML General/source.ML	\
    2.15 +  General/stack.ML General/symbol.ML General/symbol_pos.ML		\
    2.16 +  General/table.ML General/url.ML General/xml.ML General/yxml.ML	\
    2.17 +  Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML	\
    2.18 +  Isar/class.ML Isar/class_target.ML Isar/code.ML Isar/constdefs.ML	\
    2.19    Isar/context_rules.ML Isar/element.ML Isar/expression.ML		\
    2.20    Isar/isar_cmd.ML Isar/isar_document.ML Isar/isar_syn.ML		\
    2.21    Isar/local_defs.ML Isar/local_syntax.ML Isar/local_theory.ML		\
     3.1 --- a/src/Pure/ROOT.ML	Thu Jul 16 00:24:11 2009 +0200
     3.2 +++ b/src/Pure/ROOT.ML	Thu Jul 16 16:24:49 2009 +0200
     3.3 @@ -33,11 +33,12 @@
     3.4  use "ML/ml_lex.ML";
     3.5  use "ML/ml_parse.ML";
     3.6  use "General/secure.ML";
     3.7 -(*----- basic ML bootstrap finished -----*)
     3.8 +(*^^^^^ end of basic ML bootstrap ^^^^^*)
     3.9  use "General/integer.ML";
    3.10  use "General/stack.ML";
    3.11  use "General/queue.ML";
    3.12  use "General/heap.ML";
    3.13 +use "General/same.ML";
    3.14  use "General/ord_list.ML";
    3.15  use "General/balanced_tree.ML";
    3.16  use "General/graph.ML";