# HG changeset patch
# User haftmann
# Date 1280399325 -7200
# Node ID 00042fd999a80838a453cab389dbd4a51fd8bc04
# Parent  a9b52497661caf90455271655a7b4995e690235d
intermediate operation avoids invariance problem in Scala

diff -r a9b52497661c -r 00042fd999a8 src/HOL/Imperative_HOL/Ref.thy
--- a/src/HOL/Imperative_HOL/Ref.thy	Thu Jul 29 09:57:10 2010 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy	Thu Jul 29 12:28:45 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((_), (_))")
 
diff -r a9b52497661c -r 00042fd999a8 src/HOL/Imperative_HOL/ex/Linked_Lists.thy
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Thu Jul 29 09:57:10 2010 +0200
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Thu Jul 29 12:28:45 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