# HG changeset patch # User haftmann # Date 1280408872 -7200 # Node ID aaeb6f0b1b1d923e77d078088b02dea706809970 # Parent 81ead4aaba2d3876309803086737e39584b093a0# Parent 5beae0d6b7bc150236949f03ef102119780c8063 merged diff -r 81ead4aaba2d -r aaeb6f0b1b1d src/HOL/Imperative_HOL/Ref.thy --- 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((_), (_))") diff -r 81ead4aaba2d -r aaeb6f0b1b1d src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy --- 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] \= (\a. rev a 0 9))" +definition "example = (Array.make 10 id \= (\a. rev a 0 9))" export_code example checking SML SML_imp OCaml? OCaml_imp? Haskell? Scala? Scala_imp? diff -r 81ead4aaba2d -r aaeb6f0b1b1d src/HOL/Imperative_HOL/ex/Linked_Lists.thy --- 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 diff -r 81ead4aaba2d -r aaeb6f0b1b1d src/Tools/Code/code_ml.ML --- 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",