a first sketch for Imperative HOL witht Scala
authorhaftmann
Fri Jul 16 13:58:29 2010 +0200 (2010-07-16)
changeset 3784227e7047d9ae6
parent 37838 28848d338261
child 37843 336dae59af03
a first sketch for Imperative HOL witht Scala
src/HOL/Imperative_HOL/Array.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Imperative_HOL/Ref.thy
     1.1 --- a/src/HOL/Imperative_HOL/Array.thy	Fri Jul 16 10:23:21 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Fri Jul 16 13:58:29 2010 +0200
     1.3 @@ -479,4 +479,19 @@
     1.4  code_const Array.nth' (Haskell "Heap.readArray")
     1.5  code_const Array.upd' (Haskell "Heap.writeArray")
     1.6  
     1.7 +
     1.8 +text {* Scala *}
     1.9 +
    1.10 +code_type array (Scala "!Array[_]")
    1.11 +code_const Array (Scala "!error(\"bare Array\")")
    1.12 +code_const Array.new' (Scala "('_: Unit)/ => / Array.fill((_))((_))")
    1.13 +code_const Array.of_list (Scala "('_: Unit)/ =>/ _.toArray")
    1.14 +code_const Array.make' (Scala "('_: Unit)/ =>/ Array.tabulate((_),/ (_))")
    1.15 +code_const Array.len' (Scala "('_: Unit)/ =>/ _.length")
    1.16 +code_const Array.nth' (Scala "('_: Unit)/ =>/ _((_))")
    1.17 +code_const Array.upd' (Scala "('_: Unit)/ =>/ _.update((_),/ (_))")
    1.18 +code_const Array.freeze (Scala "('_: Unit)/ =>/ _.toList")
    1.19 +
    1.20 +code_reserved Scala Array
    1.21 +
    1.22  end
     2.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 16 10:23:21 2010 +0200
     2.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 16 13:58:29 2010 +0200
     2.3 @@ -469,14 +469,26 @@
     2.4  
     2.5  subsubsection {* Scala *}
     2.6  
     2.7 -code_include Haskell "Heap"
     2.8 -{*def bind[A, B](f: Unit => A, g: A => Unit => B, u: Unit): B = g (f ()) ()*}
     2.9 +code_include Scala "Heap"
    2.10 +{*def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) ()
    2.11 +
    2.12 +class Ref[A](x: A) {
    2.13 +  var value = x
    2.14 +}
    2.15 +
    2.16 +object Ref {
    2.17 +  def apply[A](x: A): Ref[A] = new Ref[A](x)
    2.18 +}
    2.19 +
    2.20 +def lookup[A](r: Ref[A]): A = r.value
    2.21 +
    2.22 +def update[A](r: Ref[A], x: A): Unit = { r.value = x }*}
    2.23  
    2.24  code_reserved Scala Heap
    2.25  
    2.26  code_type Heap (Scala "Unit/ =>/ _")
    2.27 -code_const bind (Scala "Heap.bind")
    2.28 -code_const return (Scala "!(()/ =>/ _)")
    2.29 +code_const bind (Scala "!Heap.bind((_), (_))")
    2.30 +code_const return (Scala "('_: Unit)/ =>/ _")
    2.31  code_const Heap_Monad.raise' (Scala "!error(_)")
    2.32  
    2.33  
     3.1 --- a/src/HOL/Imperative_HOL/Ref.thy	Fri Jul 16 10:23:21 2010 +0200
     3.2 +++ b/src/HOL/Imperative_HOL/Ref.thy	Fri Jul 16 13:58:29 2010 +0200
     3.3 @@ -293,4 +293,13 @@
     3.4  code_const Ref.lookup (Haskell "Heap.readSTRef")
     3.5  code_const Ref.update (Haskell "Heap.writeSTRef")
     3.6  
     3.7 +
     3.8 +text {* Scala *}
     3.9 +
    3.10 +code_type ref (Scala "!Heap.Ref[_]")
    3.11 +code_const Ref (Scala "!error(\"bare Ref\")")
    3.12 +code_const ref (Scala "('_: Unit)/ =>/ Heap.Ref((_))")
    3.13 +code_const Ref.lookup (Scala "('_: Unit)/ =>/ Heap.lookup((_))")
    3.14 +code_const Ref.update (Scala "('_: Unit)/ =>/ Heap.update((_), (_))")
    3.15 +
    3.16  end