# HG changeset patch
# User haftmann
# Date 1279286902 -7200
# Node ID b70d7a3479642e3a01143468b6907538ee5a0f0a
# Parent  f26becedaeb10e066bf18c853cd79de01cc6df2f
first roughly working version of Imperative HOL for Scala

diff -r f26becedaeb1 -r b70d7a347964 src/HOL/Imperative_HOL/Array.thy
--- a/src/HOL/Imperative_HOL/Array.thy	Fri Jul 16 14:11:08 2010 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy	Fri Jul 16 15:28:22 2010 +0200
@@ -345,7 +345,7 @@
   "new n x = make n (\<lambda>_. x)"
   by (rule Heap_eqI) (simp add: map_replicate_trivial execute_simps)
 
-lemma array_of_list_make:
+lemma array_of_list_make [code]:
   "of_list xs = make (List.length xs) (\<lambda>n. xs ! n)"
   by (rule Heap_eqI) (simp add: map_nth execute_simps)
 
@@ -482,11 +482,10 @@
 
 text {* Scala *}
 
-code_type array (Scala "!Array[_]")
+code_type array (Scala "!collection.mutable.ArraySeq[_]")
 code_const Array (Scala "!error(\"bare Array\")")
-code_const Array.new' (Scala "('_: Unit)/ => / Array.fill((_))((_))")
-code_const Array.of_list (Scala "('_: Unit)/ =>/ _.toArray")
-code_const Array.make' (Scala "('_: Unit)/ =>/ Array.tabulate((_),/ (_))")
+code_const Array.new' (Scala "('_: Unit)/ => / collection.mutable.ArraySeq.fill((_))((_))")
+code_const Array.make' (Scala "('_: Unit)/ =>/ collection.mutable.ArraySeq.tabulate((_))((_))")
 code_const Array.len' (Scala "('_: Unit)/ =>/ _.length")
 code_const Array.nth' (Scala "('_: Unit)/ =>/ _((_))")
 code_const Array.upd' (Scala "('_: Unit)/ =>/ _.update((_),/ (_))")
diff -r f26becedaeb1 -r b70d7a347964 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 16 14:11:08 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Jul 16 15:28:22 2010 +0200
@@ -489,7 +489,7 @@
 code_type Heap (Scala "Unit/ =>/ _")
 code_const bind (Scala "!Heap.bind((_), (_))")
 code_const return (Scala "('_: Unit)/ =>/ _")
-code_const Heap_Monad.raise' (Scala "!error(_)")
+code_const Heap_Monad.raise' (Scala "!error((_))")
 
 
 subsubsection {* Target variants with less units *}
diff -r f26becedaeb1 -r b70d7a347964 src/HOL/Imperative_HOL/Imperative_HOL_ex.thy
--- a/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Fri Jul 16 14:11:08 2010 +0200
+++ b/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Fri Jul 16 15:28:22 2010 +0200
@@ -14,6 +14,6 @@
   Array.upd, Array.map_entry, Array.swap, Array.freeze,
   ref, Ref.lookup, Ref.update, Ref.change)"
 
-export_code everything checking SML SML_imp OCaml? OCaml_imp? Haskell?
+export_code everything checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala?
 
 end
diff -r f26becedaeb1 -r b70d7a347964 src/HOL/Imperative_HOL/Ref.thy
--- a/src/HOL/Imperative_HOL/Ref.thy	Fri Jul 16 14:11:08 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy	Fri Jul 16 15:28:22 2010 +0200
@@ -303,3 +303,4 @@
 code_const Ref.update (Scala "('_: Unit)/ =>/ Heap.update((_), (_))")
 
 end
+
diff -r f26becedaeb1 -r b70d7a347964 src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Fri Jul 16 14:11:08 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Fri Jul 16 15:28:22 2010 +0200
@@ -655,6 +655,6 @@
 
 ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *}
 
-export_code qsort checking SML SML_imp OCaml? OCaml_imp? Haskell?
+export_code qsort checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala?
 
-end
\ No newline at end of file
+end
diff -r f26becedaeb1 -r b70d7a347964 src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Fri Jul 16 14:11:08 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Fri Jul 16 15:28:22 2010 +0200
@@ -110,6 +110,6 @@
       subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elims)
   (drule sym[of "List.length (Array.get h a)"], simp)
 
-export_code rev checking SML SML_imp OCaml? OCaml_imp? Haskell?
+export_code rev checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala?
 
 end