repaired some implementations of imperative operations
authorhaftmann
Wed Jul 14 17:15:58 2010 +0200 (2010-07-14)
changeset 37831fa3a2e35c4f1
parent 37830 01d308b00bcf
child 37832 f8fcfc678280
repaired some implementations of imperative operations
src/HOL/Imperative_HOL/Array.thy
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Imperative_HOL/Imperative_HOL_ex.thy
     1.1 --- a/src/HOL/Imperative_HOL/Array.thy	Wed Jul 14 16:45:30 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Wed Jul 14 17:15:58 2010 +0200
     1.3 @@ -363,13 +363,6 @@
     1.4    "Array.new = new' o Code_Numeral.of_nat"
     1.5    by (simp add: new'_def o_def)
     1.6  
     1.7 -definition of_list' where
     1.8 -  [code del]: "of_list' i xs = Array.of_list (take (Code_Numeral.nat_of i) xs)"
     1.9 -
    1.10 -lemma [code]:
    1.11 -  "Array.of_list xs = of_list' (Code_Numeral.of_nat (List.length xs)) xs"
    1.12 -  by (simp add: of_list'_def)
    1.13 -
    1.14  definition make' where
    1.15    [code del]: "make' i f = Array.make (Code_Numeral.nat_of i) (f o Code_Numeral.of_nat)"
    1.16  
    1.17 @@ -443,7 +436,7 @@
    1.18      }) h" by (simp add: execute_simps)
    1.19  qed
    1.20  
    1.21 -hide_const (open) new' of_list' make' len' nth' upd'
    1.22 +hide_const (open) new' make' len' nth' upd'
    1.23  
    1.24  
    1.25  text {* SML *}
    1.26 @@ -451,7 +444,7 @@
    1.27  code_type array (SML "_/ array")
    1.28  code_const Array (SML "raise/ (Fail/ \"bare Array\")")
    1.29  code_const Array.new' (SML "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))")
    1.30 -code_const Array.of_list' (SML "((_); fn/ ()/ =>/ Array.fromList/ _)")
    1.31 +code_const Array.of_list (SML "(fn/ ()/ =>/ Array.fromList/ _)")
    1.32  code_const Array.make' (SML "(fn/ ()/ =>/ Array.tabulate/ ((_),/ (_)))")
    1.33  code_const Array.len' (SML "(fn/ ()/ =>/ Array.length/ _)")
    1.34  code_const Array.nth' (SML "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))")
    1.35 @@ -465,7 +458,9 @@
    1.36  code_type array (OCaml "_/ array")
    1.37  code_const Array (OCaml "failwith/ \"bare Array\"")
    1.38  code_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ (Big'_int.int'_of'_big'_int/ _)/ _)")
    1.39 -code_const Array.of_list' (OCaml "((_); fun/ ()/ ->/ Array.of'_list/ _)")
    1.40 +code_const Array.of_list (OCaml "(fun/ ()/ ->/ Array.of'_list/ _)")
    1.41 +code_const Array.make' (OCaml "(fun/ ()/ ->/ Array.init/ (Big'_int.int'_of'_big'_int/ _)/
    1.42 +  (fun k'_ ->/ _/ (Big'_int.big'_int'_of'_int/ k'_)))")
    1.43  code_const Array.len' (OCaml "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))")
    1.44  code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ (Big'_int.int'_of'_big'_int/ _))")
    1.45  code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ (Big'_int.int'_of'_big'_int/ _)/ _)")
    1.46 @@ -477,8 +472,9 @@
    1.47  
    1.48  code_type array (Haskell "Heap.STArray/ Heap.RealWorld/ _")
    1.49  code_const Array (Haskell "error/ \"bare Array\"")
    1.50 -code_const Array.new' (Haskell "Heap.newArray/ (0,/ _)")
    1.51 -code_const Array.of_list' (Haskell "Heap.newListArray/ (0,/ _)")
    1.52 +code_const Array.new' (Haskell "Heap.newArray")
    1.53 +code_const Array.of_list (Haskell "Heap.newListArray")
    1.54 +code_const Array.make' (Haskell "Heap.newFunArray")
    1.55  code_const Array.len' (Haskell "Heap.lengthArray")
    1.56  code_const Array.nth' (Haskell "Heap.readArray")
    1.57  code_const Array.upd' (Haskell "Heap.writeArray")
     2.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Jul 14 16:45:30 2010 +0200
     2.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Wed Jul 14 17:15:58 2010 +0200
     2.3 @@ -508,11 +508,14 @@
     2.4  readSTRef = Data.STRef.readSTRef;
     2.5  writeSTRef = Data.STRef.writeSTRef;
     2.6  
     2.7 -newArray :: (Int, Int) -> a -> ST s (STArray s a);
     2.8 -newArray = Data.Array.ST.newArray;
     2.9 +newArray :: Int -> a -> ST s (STArray s a);
    2.10 +newArray k = Data.Array.ST.newArray (0, k);
    2.11  
    2.12 -newListArray :: (Int, Int) -> [a] -> ST s (STArray s a);
    2.13 -newListArray = Data.Array.ST.newListArray;
    2.14 +newListArray :: [a] -> ST s (STArray s a);
    2.15 +newListArray xs = Data.Array.ST.newListArray (0, length xs) xs;
    2.16 +
    2.17 +newFunArray :: Int -> (Int -> a) -> ST s (STArray s a);
    2.18 +newFunArray k f = Data.Array.ST.newListArray (0, k) (map f [0..k-1]);
    2.19  
    2.20  lengthArray :: STArray s a -> ST s Int;
    2.21  lengthArray a = Control.Monad.liftM snd (Data.Array.ST.getBounds a);
    2.22 @@ -534,4 +537,6 @@
    2.23  
    2.24  hide_const (open) Heap heap guard raise' fold_map
    2.25  
    2.26 +export_code return in Haskell file "/tmp/"
    2.27 +
    2.28  end
     3.1 --- a/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Wed Jul 14 16:45:30 2010 +0200
     3.2 +++ b/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Wed Jul 14 17:15:58 2010 +0200
     3.3 @@ -10,9 +10,9 @@
     3.4    "ex/Imperative_Quicksort" "ex/Imperative_Reverse" "ex/Linked_Lists" "ex/SatChecker"
     3.5  begin
     3.6  
     3.7 -definition "everything = (Array.new, Array.of_list, (*Array.make,*) Array.len, Array.nth,
     3.8 +definition "everything = (Array.new, Array.of_list, Array.make, Array.len, Array.nth,
     3.9    Array.upd, Array.map_entry, Array.swap, Array.freeze,
    3.10 -  ref, Ref.lookup, Ref.update(*, Ref.change*))"
    3.11 +  ref, Ref.lookup, Ref.update, Ref.change)"
    3.12  
    3.13  export_code everything checking SML SML_imp OCaml? OCaml_imp? Haskell?
    3.14