src/HOL/Imperative_HOL/Heap_Monad.thy
changeset 37842 27e7047d9ae6
parent 37838 28848d338261
child 37845 b70d7a347964
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 16 10:23:21 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 16 13:58:29 2010 +0200
     1.3 @@ -469,14 +469,26 @@
     1.4  
     1.5  subsubsection {* Scala *}
     1.6  
     1.7 -code_include Haskell "Heap"
     1.8 -{*def bind[A, B](f: Unit => A, g: A => Unit => B, u: Unit): B = g (f ()) ()*}
     1.9 +code_include Scala "Heap"
    1.10 +{*def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) ()
    1.11 +
    1.12 +class Ref[A](x: A) {
    1.13 +  var value = x
    1.14 +}
    1.15 +
    1.16 +object Ref {
    1.17 +  def apply[A](x: A): Ref[A] = new Ref[A](x)
    1.18 +}
    1.19 +
    1.20 +def lookup[A](r: Ref[A]): A = r.value
    1.21 +
    1.22 +def update[A](r: Ref[A], x: A): Unit = { r.value = x }*}
    1.23  
    1.24  code_reserved Scala Heap
    1.25  
    1.26  code_type Heap (Scala "Unit/ =>/ _")
    1.27 -code_const bind (Scala "Heap.bind")
    1.28 -code_const return (Scala "!(()/ =>/ _)")
    1.29 +code_const bind (Scala "!Heap.bind((_), (_))")
    1.30 +code_const return (Scala "('_: Unit)/ =>/ _")
    1.31  code_const Heap_Monad.raise' (Scala "!error(_)")
    1.32  
    1.33