# HG changeset patch
# User haftmann
# Date 1279120558 -7200
# Node ID fa3a2e35c4f11db1c2bff4c02180261ab5e61b1d
# Parent  01d308b00bcfe508ce65e49343f6e0cbdb13616b
repaired some implementations of imperative operations

diff -r 01d308b00bcf -r fa3a2e35c4f1 src/HOL/Imperative_HOL/Array.thy
--- a/src/HOL/Imperative_HOL/Array.thy	Wed Jul 14 16:45:30 2010 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy	Wed Jul 14 17:15:58 2010 +0200
@@ -363,13 +363,6 @@
   "Array.new = new' o Code_Numeral.of_nat"
   by (simp add: new'_def o_def)
 
-definition of_list' where
-  [code del]: "of_list' i xs = Array.of_list (take (Code_Numeral.nat_of i) xs)"
-
-lemma [code]:
-  "Array.of_list xs = of_list' (Code_Numeral.of_nat (List.length xs)) xs"
-  by (simp add: of_list'_def)
-
 definition make' where
   [code del]: "make' i f = Array.make (Code_Numeral.nat_of i) (f o Code_Numeral.of_nat)"
 
@@ -443,7 +436,7 @@
     }) h" by (simp add: execute_simps)
 qed
 
-hide_const (open) new' of_list' make' len' nth' upd'
+hide_const (open) new' make' len' nth' upd'
 
 
 text {* SML *}
@@ -451,7 +444,7 @@
 code_type array (SML "_/ array")
 code_const Array (SML "raise/ (Fail/ \"bare Array\")")
 code_const Array.new' (SML "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))")
-code_const Array.of_list' (SML "((_); fn/ ()/ =>/ Array.fromList/ _)")
+code_const Array.of_list (SML "(fn/ ()/ =>/ Array.fromList/ _)")
 code_const Array.make' (SML "(fn/ ()/ =>/ Array.tabulate/ ((_),/ (_)))")
 code_const Array.len' (SML "(fn/ ()/ =>/ Array.length/ _)")
 code_const Array.nth' (SML "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))")
@@ -465,7 +458,9 @@
 code_type array (OCaml "_/ array")
 code_const Array (OCaml "failwith/ \"bare Array\"")
 code_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ (Big'_int.int'_of'_big'_int/ _)/ _)")
-code_const Array.of_list' (OCaml "((_); fun/ ()/ ->/ Array.of'_list/ _)")
+code_const Array.of_list (OCaml "(fun/ ()/ ->/ Array.of'_list/ _)")
+code_const Array.make' (OCaml "(fun/ ()/ ->/ Array.init/ (Big'_int.int'_of'_big'_int/ _)/
+  (fun k'_ ->/ _/ (Big'_int.big'_int'_of'_int/ k'_)))")
 code_const Array.len' (OCaml "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))")
 code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ (Big'_int.int'_of'_big'_int/ _))")
 code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ (Big'_int.int'_of'_big'_int/ _)/ _)")
@@ -477,8 +472,9 @@
 
 code_type array (Haskell "Heap.STArray/ Heap.RealWorld/ _")
 code_const Array (Haskell "error/ \"bare Array\"")
-code_const Array.new' (Haskell "Heap.newArray/ (0,/ _)")
-code_const Array.of_list' (Haskell "Heap.newListArray/ (0,/ _)")
+code_const Array.new' (Haskell "Heap.newArray")
+code_const Array.of_list (Haskell "Heap.newListArray")
+code_const Array.make' (Haskell "Heap.newFunArray")
 code_const Array.len' (Haskell "Heap.lengthArray")
 code_const Array.nth' (Haskell "Heap.readArray")
 code_const Array.upd' (Haskell "Heap.writeArray")
diff -r 01d308b00bcf -r fa3a2e35c4f1 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Jul 14 16:45:30 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Jul 14 17:15:58 2010 +0200
@@ -508,11 +508,14 @@
 readSTRef = Data.STRef.readSTRef;
 writeSTRef = Data.STRef.writeSTRef;
 
-newArray :: (Int, Int) -> a -> ST s (STArray s a);
-newArray = Data.Array.ST.newArray;
+newArray :: Int -> a -> ST s (STArray s a);
+newArray k = Data.Array.ST.newArray (0, k);
 
-newListArray :: (Int, Int) -> [a] -> ST s (STArray s a);
-newListArray = Data.Array.ST.newListArray;
+newListArray :: [a] -> ST s (STArray s a);
+newListArray xs = Data.Array.ST.newListArray (0, length xs) xs;
+
+newFunArray :: Int -> (Int -> a) -> ST s (STArray s a);
+newFunArray k f = Data.Array.ST.newListArray (0, k) (map f [0..k-1]);
 
 lengthArray :: STArray s a -> ST s Int;
 lengthArray a = Control.Monad.liftM snd (Data.Array.ST.getBounds a);
@@ -534,4 +537,6 @@
 
 hide_const (open) Heap heap guard raise' fold_map
 
+export_code return in Haskell file "/tmp/"
+
 end
diff -r 01d308b00bcf -r fa3a2e35c4f1 src/HOL/Imperative_HOL/Imperative_HOL_ex.thy
--- a/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Wed Jul 14 16:45:30 2010 +0200
+++ b/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Wed Jul 14 17:15:58 2010 +0200
@@ -10,9 +10,9 @@
   "ex/Imperative_Quicksort" "ex/Imperative_Reverse" "ex/Linked_Lists" "ex/SatChecker"
 begin
 
-definition "everything = (Array.new, Array.of_list, (*Array.make,*) Array.len, Array.nth,
+definition "everything = (Array.new, Array.of_list, Array.make, Array.len, Array.nth,
   Array.upd, Array.map_entry, Array.swap, Array.freeze,
-  ref, Ref.lookup, Ref.update(*, Ref.change*))"
+  ref, Ref.lookup, Ref.update, Ref.change)"
 
 export_code everything checking SML SML_imp OCaml? OCaml_imp? Haskell?