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