--- a/src/HOL/Library/Array.thy Thu Feb 28 15:55:33 2008 +0100
+++ b/src/HOL/Library/Array.thy Thu Feb 28 16:50:52 2008 +0100
@@ -6,7 +6,7 @@
header {* Monadic arrays *}
theory Array
-imports Heap_Monad
+imports Heap_Monad Code_Index
begin
subsection {* Primitives *}
@@ -99,21 +99,6 @@
hide (open) const new map -- {* avoid clashed with some popular names *}
-subsection {* Converting arrays to lists *}
-
-primrec list_of_aux :: "nat \<Rightarrow> ('a\<Colon>heap) array \<Rightarrow> 'a list \<Rightarrow> 'a list Heap" where
- "list_of_aux 0 a xs = return xs"
- | "list_of_aux (Suc n) a xs = (do
- x \<leftarrow> Array.nth a n;
- list_of_aux n a (x#xs)
- done)"
-
-definition list_of :: "('a\<Colon>heap) array \<Rightarrow> 'a list Heap" where
- "list_of a = (do n \<leftarrow> Array.length a;
- list_of_aux n a []
- done)"
-
-
subsection {* Properties *}
lemma array_make [code func]:
@@ -127,4 +112,93 @@
"of_list xs = make (List.length xs) (\<lambda>n. xs ! n)"
unfolding make_def map_nth ..
+
+subsection {* Code generator setup *}
+
+subsubsection {* Logical intermediate layer *}
+
+definition new' where
+ [code del]: "new' = Array.new o nat_of_index"
+hide (open) const new'
+lemma [code func]:
+ "Array.new = Array.new' o index_of_nat"
+ by (simp add: new'_def o_def)
+
+definition of_list' where
+ [code del]: "of_list' i xs = Array.of_list (take (nat_of_index i) xs)"
+hide (open) const of_list'
+lemma [code func]:
+ "Array.of_list xs = Array.of_list' (index_of_nat (List.length xs)) xs"
+ by (simp add: of_list'_def)
+
+definition make' where
+ [code del]: "make' i f = Array.make (nat_of_index i) (f o index_of_nat)"
+hide (open) const make'
+lemma [code func]:
+ "Array.make n f = Array.make' (index_of_nat n) (f o nat_of_index)"
+ by (simp add: make'_def o_def)
+
+definition length' where
+ [code del]: "length' = Array.length \<guillemotright>== liftM index_of_nat"
+hide (open) const length'
+lemma [code func]:
+ "Array.length = Array.length' \<guillemotright>== liftM nat_of_index"
+ by (simp add: length'_def monad_simp',
+ simp add: liftM_def comp_def monad_simp,
+ simp add: monad_simp')
+
+definition nth' where
+ [code del]: "nth' a = Array.nth a o nat_of_index"
+hide (open) const nth'
+lemma [code func]:
+ "Array.nth a n = Array.nth' a (index_of_nat n)"
+ by (simp add: nth'_def)
+
+definition upd' where
+ [code del]: "upd' a i x = Array.upd (nat_of_index i) x a \<guillemotright> return ()"
+hide (open) const upd'
+lemma [code func]:
+ "Array.upd i x a = Array.upd' a (index_of_nat i) x \<guillemotright> return a"
+ by (simp add: upd'_def monad_simp upd_return)
+
+
+subsubsection {* SML *}
+
+code_type array (SML "_/ array")
+code_const Array (SML "raise/ (Fail/ \"bare Array\")")
+code_const Array.new' (SML "Array.array ((_), (_))")
+code_const Array.of_list (SML "Array.fromList")
+code_const Array.make' (SML "Array.tabulate ((_), (_))")
+code_const Array.length' (SML "Array.length")
+code_const Array.nth' (SML "Array.sub ((_), (_))")
+code_const Array.upd' (SML "Array.update ((_), (_), (_))")
+
+code_reserved SML Array
+
+
+subsubsection {* OCaml *}
+
+code_type array (OCaml "_/ array")
+code_const Array (OCaml "failwith/ \"bare Array\"")
+code_const Array.new' (OCaml "Array.make")
+code_const Array.of_list (OCaml "Array.of_list")
+code_const Array.make' (OCaml "Array.init")
+code_const Array.length' (OCaml "Array.length")
+code_const Array.nth' (OCaml "Array.get")
+code_const Array.upd' (OCaml "Array.set")
+
+code_reserved OCaml Array
+
+
+subsubsection {* Haskell *}
+
+code_type array (Haskell "STArray '_s _")
+code_const Array (Haskell "error/ \"bare Array\"")
+code_const Array.new' (Haskell "newArray/ (0,/ _)")
+code_const Array.of_list' (Haskell "newListArray/ (0,/ _)")
+code_const Array.length' (Haskell "length")
+code_const Array.nth' (Haskell "readArray")
+code_const Array.upd' (Haskell "writeArray")
+
+
end
--- a/src/HOL/Library/Heap_Monad.thy Thu Feb 28 15:55:33 2008 +0100
+++ b/src/HOL/Library/Heap_Monad.thy Thu Feb 28 16:50:52 2008 +0100
@@ -274,4 +274,101 @@
hide (open) const heap execute
+
+subsection {* Code generator setup *}
+
+subsubsection {* Logical intermediate layer *}
+
+definition
+ Fail :: "message_string \<Rightarrow> exception"
+where
+ [code func del]: "Fail s = Exn"
+
+definition
+ raise_exc :: "exception \<Rightarrow> 'a Heap"
+where
+ [code func del]: "raise_exc e = raise []"
+
+lemma raise_raise_exc [code func, code inline]:
+ "raise s = raise_exc (Fail (STR s))"
+ unfolding Fail_def raise_exc_def raise_def ..
+
+hide (open) const Fail raise_exc
+
+
+subsubsection {* SML *}
+
+code_type Heap (SML "_")
+code_const Heap (SML "raise/ (Fail/ \"bare Heap\")")
+code_monad run "op \<guillemotright>=" SML
+code_const run (SML "_")
+code_const return (SML "_")
+code_const "Heap_Monad.Fail" (SML "Fail")
+code_const "Heap_Monad.raise_exc" (SML "raise")
+
+
+subsubsection {* OCaml *}
+
+code_type Heap (OCaml "_")
+code_const Heap (OCaml "failwith/ \"bare Heap\"")
+code_monad run "op \<guillemotright>=" OCaml
+code_const run (OCaml "_")
+code_const return (OCaml "_")
+code_const "Heap_Monad.Fail" (OCaml "Failure")
+code_const "Heap_Monad.raise_exc" (OCaml "raise")
+
+code_reserved OCaml Failure raise
+
+
+subsubsection {* Haskell *}
+
+text {* Adaption layer *}
+
+code_include Haskell "STMonad"
+{*import qualified Control.Monad;
+import qualified Control.Monad.ST;
+import qualified Data.STRef;
+import qualified Data.Array.ST;
+
+type ST s a = Control.Monad.ST.ST s a;
+type STRef s a = Data.STRef.STRef s a;
+type STArray s a = Data.Array.ST.STArray s Integer a;
+
+runST :: (forall s. ST s a) -> a;
+runST s = Control.Monad.ST.runST s;
+
+newSTRef = Data.STRef.newSTRef;
+readSTRef = Data.STRef.readSTRef;
+writeSTRef = Data.STRef.writeSTRef;
+
+newArray :: (Integer, Integer) -> a -> ST s (STArray s a);
+newArray = Data.Array.ST.newArray;
+
+newListArray :: (Integer, Integer) -> [a] -> ST s (STArray s a);
+newListArray = Data.Array.ST.newListArray;
+
+length :: STArray s a -> ST s Integer;
+length a = Control.Monad.liftM snd (Data.Array.ST.getBounds a);
+
+readArray :: STArray s a -> Integer -> ST s a;
+readArray = Data.Array.ST.readArray;
+
+writeArray :: STArray s a -> Integer -> a -> ST s ();
+writeArray = Data.Array.ST.writeArray;*}
+
+code_reserved Haskell ST STRef Array
+ runST
+ newSTRef reasSTRef writeSTRef
+ newArray newListArray bounds readArray writeArray
+
+text {* Monad *}
+
+code_type Heap (Haskell "ST '_s _")
+code_const Heap (Haskell "error \"bare Heap\")")
+code_const evaluate (Haskell "runST")
+code_monad run bindM Haskell
+code_const return (Haskell "return")
+code_const "Heap_Monad.Fail" (Haskell "_")
+code_const "Heap_Monad.raise_exc" (Haskell "error")
+
end
--- a/src/HOL/Library/Ref.thy Thu Feb 28 15:55:33 2008 +0100
+++ b/src/HOL/Library/Ref.thy Thu Feb 28 16:50:52 2008 +0100
@@ -29,6 +29,7 @@
update :: "'a ref \<Rightarrow> ('a\<Colon>heap) \<Rightarrow> unit Heap" ("_ := _" 62) where
[code del]: "update r e = Heap_Monad.heap (\<lambda>h. ((), set_ref r e h))"
+
subsection {* Derivates *}
definition
@@ -42,6 +43,7 @@
hide (open) const new lookup update change
+
subsection {* Properties *}
lemma lookup_chain:
@@ -53,4 +55,37 @@
"r := e = Ref.change (\<lambda>_. e) r \<guillemotright> return ()"
by (auto simp add: monad_simp change_def lookup_chain)
+
+subsection {* Code generator setup *}
+
+subsubsection {* SML *}
+
+code_type ref (SML "_/ ref")
+code_const Ref (SML "raise/ (Fail/ \"bare Ref\")")
+code_const Ref.new (SML "ref")
+code_const Ref.lookup (SML "'!")
+code_const Ref.update (SML infixl 3 ":=")
+
+code_reserved SML ref
+
+
+subsubsection {* OCaml *}
+
+code_type ref (OCaml "_/ ref")
+code_const Ref (OCaml "failwith/ \"bare Ref\"")
+code_const Ref.new (OCaml "ref")
+code_const Ref.lookup (OCaml "'!")
+code_const Ref.update (OCaml infixr 1 ":=")
+
+code_reserved OCaml ref
+
+
+subsubsection {* Haskell *}
+
+code_type ref (Haskell "STRef '_s _")
+code_const Ref (Haskell "error/ \"bare Ref\"")
+code_const Ref.new (Haskell "newSTRef")
+code_const Ref.lookup (Haskell "readSTRef")
+code_const Ref.update (Haskell "writeSTRef")
+
end
\ No newline at end of file