src/HOL/Imperative_HOL/Heap_Monad.thy
changeset 38968 e55deaa22fff
parent 38773 f9837065b5e8
child 39021 139aada5caf8
     1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Sep 01 09:03:34 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Sep 01 11:09:50 2010 +0200
     1.3 @@ -477,9 +477,9 @@
     1.4  subsubsection {* Scala *}
     1.5  
     1.6  code_include Scala "Heap"
     1.7 -{*import collection.mutable.ArraySeq
     1.8 -
     1.9 -def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) ()
    1.10 +{*object Heap {
    1.11 +  def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) ()
    1.12 +}
    1.13  
    1.14  class Ref[A](x: A) {
    1.15    var value = x
    1.16 @@ -495,21 +495,23 @@
    1.17  }
    1.18  
    1.19  object Array {
    1.20 -  def alloc[A](n: Natural.Nat)(x: A): ArraySeq[A] =
    1.21 +  import collection.mutable.ArraySeq
    1.22 +  def alloc[A](n: Natural)(x: A): ArraySeq[A] =
    1.23      ArraySeq.fill(n.as_Int)(x)
    1.24 -  def make[A](n: Natural.Nat)(f: Natural.Nat => A): ArraySeq[A] =
    1.25 -    ArraySeq.tabulate(n.as_Int)((k: Int) => f(Natural.Nat(k)))
    1.26 -  def len[A](a: ArraySeq[A]): Natural.Nat =
    1.27 -    Natural.Nat(a.length)
    1.28 -  def nth[A](a: ArraySeq[A], n: Natural.Nat): A =
    1.29 +  def make[A](n: Natural)(f: Natural => A): ArraySeq[A] =
    1.30 +    ArraySeq.tabulate(n.as_Int)((k: Int) => f(Natural(k)))
    1.31 +  def len[A](a: ArraySeq[A]): Natural =
    1.32 +    Natural(a.length)
    1.33 +  def nth[A](a: ArraySeq[A], n: Natural): A =
    1.34      a(n.as_Int)
    1.35 -  def upd[A](a: ArraySeq[A], n: Natural.Nat, x: A): Unit =
    1.36 +  def upd[A](a: ArraySeq[A], n: Natural, x: A): Unit =
    1.37      a.update(n.as_Int, x)
    1.38    def freeze[A](a: ArraySeq[A]): List[A] =
    1.39      a.toList
    1.40 -}*}
    1.41 +}
    1.42 +*}
    1.43  
    1.44 -code_reserved Scala bind Ref Array
    1.45 +code_reserved Scala Heap Ref Array
    1.46  
    1.47  code_type Heap (Scala "Unit/ =>/ _")
    1.48  code_const bind (Scala "Heap.bind")