src/HOL/Library/Ref.thy
author haftmann
Mon Jul 07 08:47:17 2008 +0200 (2008-07-07)
changeset 27487 c8a6ce181805
parent 26752 6b276119139b
child 27695 033732c90ebd
permissions -rw-r--r--
absolute imports of HOL/*.thy theories
haftmann@26170
     1
(*  Title:      HOL/Library/Ref.thy
haftmann@26170
     2
    ID:         $Id$
haftmann@26170
     3
    Author:     John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
haftmann@26170
     4
*)
haftmann@26170
     5
haftmann@26170
     6
header {* Monadic references *}
haftmann@26170
     7
haftmann@26170
     8
theory Ref
haftmann@26170
     9
imports Heap_Monad
haftmann@26170
    10
begin
haftmann@26170
    11
haftmann@26170
    12
text {*
haftmann@26170
    13
  Imperative reference operations; modeled after their ML counterparts.
haftmann@26170
    14
  See http://caml.inria.fr/pub/docs/manual-caml-light/node14.15.html
haftmann@26170
    15
  and http://www.smlnj.org/doc/Conversion/top-level-comparison.html
haftmann@26170
    16
*}
haftmann@26170
    17
haftmann@26170
    18
subsection {* Primitives *}
haftmann@26170
    19
haftmann@26170
    20
definition
haftmann@26170
    21
  new :: "'a\<Colon>heap \<Rightarrow> 'a ref Heap" where
haftmann@26170
    22
  [code del]: "new v = Heap_Monad.heap (Heap.ref v)"
haftmann@26170
    23
haftmann@26170
    24
definition
haftmann@26170
    25
  lookup :: "'a\<Colon>heap ref \<Rightarrow> 'a Heap" ("!_" 61) where
haftmann@26170
    26
  [code del]: "lookup r = Heap_Monad.heap (\<lambda>h. (get_ref r h, h))"
haftmann@26170
    27
haftmann@26170
    28
definition
haftmann@26170
    29
  update :: "'a ref \<Rightarrow> ('a\<Colon>heap) \<Rightarrow> unit Heap" ("_ := _" 62) where
haftmann@26170
    30
  [code del]: "update r e = Heap_Monad.heap (\<lambda>h. ((), set_ref r e h))"
haftmann@26170
    31
haftmann@26182
    32
haftmann@26170
    33
subsection {* Derivates *}
haftmann@26170
    34
haftmann@26170
    35
definition
haftmann@26170
    36
  change :: "('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a ref \<Rightarrow> 'a Heap"
haftmann@26170
    37
where
haftmann@26170
    38
  "change f r = (do x \<leftarrow> ! r;
haftmann@26170
    39
                    let y = f x;
haftmann@26170
    40
                    r := y;
haftmann@26170
    41
                    return y
haftmann@26170
    42
                 done)"
haftmann@26170
    43
haftmann@26170
    44
hide (open) const new lookup update change
haftmann@26170
    45
haftmann@26182
    46
haftmann@26170
    47
subsection {* Properties *}
haftmann@26170
    48
haftmann@26170
    49
lemma lookup_chain:
haftmann@26170
    50
  "(!r \<guillemotright> f) = f"
haftmann@26170
    51
  by (cases f)
haftmann@26170
    52
    (auto simp add: Let_def bindM_def lookup_def expand_fun_eq)
haftmann@26170
    53
haftmann@26170
    54
lemma update_change [code func]:
haftmann@26170
    55
  "r := e = Ref.change (\<lambda>_. e) r \<guillemotright> return ()"
haftmann@26170
    56
  by (auto simp add: monad_simp change_def lookup_chain)
haftmann@26170
    57
haftmann@26182
    58
haftmann@26182
    59
subsection {* Code generator setup *}
haftmann@26182
    60
haftmann@26182
    61
subsubsection {* SML *}
haftmann@26182
    62
haftmann@26182
    63
code_type ref (SML "_/ ref")
haftmann@26182
    64
code_const Ref (SML "raise/ (Fail/ \"bare Ref\")")
haftmann@26752
    65
code_const Ref.new (SML "(fn/ ()/ =>/ ref/ _)")
haftmann@26752
    66
code_const Ref.lookup (SML "(fn/ ()/ =>/ !/ _)")
haftmann@26752
    67
code_const Ref.update (SML "(fn/ ()/ =>/ _/ :=/ _)")
haftmann@26182
    68
haftmann@26182
    69
code_reserved SML ref
haftmann@26182
    70
haftmann@26182
    71
haftmann@26182
    72
subsubsection {* OCaml *}
haftmann@26182
    73
haftmann@26182
    74
code_type ref (OCaml "_/ ref")
haftmann@26752
    75
code_const Ref (OCaml "failwith/ \"bare Ref\")")
haftmann@26752
    76
code_const Ref.new (OCaml "(fn/ ()/ =>/ ref/ _)")
haftmann@26752
    77
code_const Ref.lookup (OCaml "(fn/ ()/ =>/ !/ _)")
haftmann@26752
    78
code_const Ref.update (OCaml "(fn/ ()/ =>/ _/ :=/ _)")
haftmann@26182
    79
haftmann@26182
    80
code_reserved OCaml ref
haftmann@26182
    81
haftmann@26182
    82
haftmann@26182
    83
subsubsection {* Haskell *}
haftmann@26182
    84
haftmann@26182
    85
code_type ref (Haskell "STRef '_s _")
haftmann@26182
    86
code_const Ref (Haskell "error/ \"bare Ref\"")
haftmann@26182
    87
code_const Ref.new (Haskell "newSTRef")
haftmann@26182
    88
code_const Ref.lookup (Haskell "readSTRef")
haftmann@26182
    89
code_const Ref.update (Haskell "writeSTRef")
haftmann@26182
    90
haftmann@26170
    91
end