--- a/src/HOL/Imperative_HOL/Ref.thy Thu Jul 29 12:07:09 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy Thu Jul 29 15:07:52 2010 +0200
@@ -263,22 +263,32 @@
subsection {* Code generator setup *}
+text {* Intermediate operation avoids invariance problem in @{text Scala} (similiar to value restriction) *}
+
+definition ref' where
+ [code del]: "ref' = ref"
+
+lemma [code]:
+ "ref x = ref' x"
+ by (simp add: ref'_def)
+
+
text {* SML *}
code_type ref (SML "_/ Unsynchronized.ref")
code_const Ref (SML "raise/ (Fail/ \"bare Ref\")")
-code_const ref (SML "(fn/ ()/ =>/ Unsynchronized.ref/ _)")
+code_const ref' (SML "(fn/ ()/ =>/ Unsynchronized.ref/ _)")
code_const Ref.lookup (SML "(fn/ ()/ =>/ !/ _)")
code_const Ref.update (SML "(fn/ ()/ =>/ _/ :=/ _)")
-code_reserved SML ref
+code_reserved SML Unsynchronized
text {* OCaml *}
code_type ref (OCaml "_/ ref")
code_const Ref (OCaml "failwith/ \"bare Ref\"")
-code_const ref (OCaml "(fun/ ()/ ->/ ref/ _)")
+code_const ref' (OCaml "(fun/ ()/ ->/ ref/ _)")
code_const Ref.lookup (OCaml "(fun/ ()/ ->/ !/ _)")
code_const Ref.update (OCaml "(fun/ ()/ ->/ _/ :=/ _)")
@@ -289,7 +299,7 @@
code_type ref (Haskell "Heap.STRef/ Heap.RealWorld/ _")
code_const Ref (Haskell "error/ \"bare Ref\"")
-code_const ref (Haskell "Heap.newSTRef")
+code_const ref' (Haskell "Heap.newSTRef")
code_const Ref.lookup (Haskell "Heap.readSTRef")
code_const Ref.update (Haskell "Heap.writeSTRef")
@@ -298,7 +308,7 @@
code_type ref (Scala "!Ref[_]")
code_const Ref (Scala "!error(\"bare Ref\")")
-code_const ref (Scala "('_: Unit)/ =>/ Ref((_))")
+code_const ref' (Scala "('_: Unit)/ =>/ Ref((_))")
code_const Ref.lookup (Scala "('_: Unit)/ =>/ Ref.lookup((_))")
code_const Ref.update (Scala "('_: Unit)/ =>/ Ref.update((_), (_))")
--- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Thu Jul 29 12:07:09 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy Thu Jul 29 15:07:52 2010 +0200
@@ -110,7 +110,7 @@
subarray_def sublist'_all rev.simps[where j=0] elim!: crel_elims)
(drule sym[of "List.length (Array.get h a)"], simp)
-definition "example = (Array.of_list [1::nat, 2, 3, 4, 5, 6, 7, 8, 9, 10] \<guillemotright>= (\<lambda>a. rev a 0 9))"
+definition "example = (Array.make 10 id \<guillemotright>= (\<lambda>a. rev a 0 9))"
export_code example checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? Scala_imp?
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Thu Jul 29 12:07:09 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Thu Jul 29 15:07:52 2010 +0200
@@ -1014,6 +1014,6 @@
ML {* @{code test_2} () *}
ML {* @{code test_3} () *}
-export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? (*Scala_imp?*)
+export_code test_1 test_2 test_3 checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? Scala_imp?
end
--- a/src/Tools/Code/code_ml.ML Thu Jul 29 12:07:09 2010 +0200
+++ b/src/Tools/Code/code_ml.ML Thu Jul 29 15:07:52 2010 +0200
@@ -987,7 +987,8 @@
)))
#> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
#> fold (Code_Target.add_reserved target_SML)
- ["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*), "IntInf"]
+ ["ref" (*rebinding is illegal*), "o" (*dictionary projections use it already*),
+ "Fail", "div", "mod" (*standard infixes*), "IntInf"]
#> fold (Code_Target.add_reserved target_OCaml) [
"and", "as", "assert", "begin", "class",
"constraint", "do", "done", "downto", "else", "end", "exception",