1.1 --- a/src/HOL/Library/Array.thy	Thu Feb 28 15:55:33 2008 +0100
     1.2 +++ b/src/HOL/Library/Array.thy	Thu Feb 28 16:50:52 2008 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Monadic arrays *}
     1.5  
     1.6  theory Array
     1.7 -imports Heap_Monad
     1.8 +imports Heap_Monad Code_Index
     1.9  begin
    1.10  
    1.11  subsection {* Primitives *}
    1.12 @@ -99,21 +99,6 @@
    1.13  hide (open) const new map -- {* avoid clashed with some popular names *}
    1.14  
    1.15  
    1.16 -subsection {* Converting arrays to lists *}
    1.17 -
    1.18 -primrec list_of_aux :: "nat \<Rightarrow> ('a\<Colon>heap) array \<Rightarrow> 'a list \<Rightarrow> 'a list Heap" where
    1.19 -  "list_of_aux 0 a xs = return xs"
    1.20 -  | "list_of_aux (Suc n) a xs = (do
    1.21 -        x \<leftarrow> Array.nth a n;
    1.22 -        list_of_aux n a (x#xs)
    1.23 -     done)"
    1.24 -
    1.25 -definition list_of :: "('a\<Colon>heap) array \<Rightarrow> 'a list Heap" where
    1.26 -  "list_of a = (do n \<leftarrow> Array.length a;
    1.27 -                   list_of_aux n a []
    1.28 -                done)"
    1.29 -
    1.30 -
    1.31  subsection {* Properties *}
    1.32  
    1.33  lemma array_make [code func]:
    1.34 @@ -127,4 +112,93 @@
    1.35    "of_list xs = make (List.length xs) (\<lambda>n. xs ! n)"
    1.36    unfolding make_def map_nth ..
    1.37  
    1.38 +
    1.39 +subsection {* Code generator setup *}
    1.40 +
    1.41 +subsubsection {* Logical intermediate layer *}
    1.42 +
    1.43 +definition new' where
    1.44 +  [code del]: "new' = Array.new o nat_of_index"
    1.45 +hide (open) const new'
    1.46 +lemma [code func]:
    1.47 +  "Array.new = Array.new' o index_of_nat"
    1.48 +  by (simp add: new'_def o_def)
    1.49 +
    1.50 +definition of_list' where
    1.51 +  [code del]: "of_list' i xs = Array.of_list (take (nat_of_index i) xs)"
    1.52 +hide (open) const of_list'
    1.53 +lemma [code func]:
    1.54 +  "Array.of_list xs = Array.of_list' (index_of_nat (List.length xs)) xs"
    1.55 +  by (simp add: of_list'_def)
    1.56 +
    1.57 +definition make' where
    1.58 +  [code del]: "make' i f = Array.make (nat_of_index i) (f o index_of_nat)"
    1.59 +hide (open) const make'
    1.60 +lemma [code func]:
    1.61 +  "Array.make n f = Array.make' (index_of_nat n) (f o nat_of_index)"
    1.62 +  by (simp add: make'_def o_def)
    1.63 +
    1.64 +definition length' where
    1.65 +  [code del]: "length' = Array.length \<guillemotright>== liftM index_of_nat"
    1.66 +hide (open) const length'
    1.67 +lemma [code func]:
    1.68 +  "Array.length = Array.length' \<guillemotright>== liftM nat_of_index"
    1.69 +  by (simp add: length'_def monad_simp',
    1.70 +    simp add: liftM_def comp_def monad_simp,
    1.71 +    simp add: monad_simp')
    1.72 +
    1.73 +definition nth' where
    1.74 +  [code del]: "nth' a = Array.nth a o nat_of_index"
    1.75 +hide (open) const nth'
    1.76 +lemma [code func]:
    1.77 +  "Array.nth a n = Array.nth' a (index_of_nat n)"
    1.78 +  by (simp add: nth'_def)
    1.79 +
    1.80 +definition upd' where
    1.81 +  [code del]: "upd' a i x = Array.upd (nat_of_index i) x a \<guillemotright> return ()"
    1.82 +hide (open) const upd'
    1.83 +lemma [code func]:
    1.84 +  "Array.upd i x a = Array.upd' a (index_of_nat i) x \<guillemotright> return a"
    1.85 +  by (simp add: upd'_def monad_simp upd_return)
    1.86 +
    1.87 +
    1.88 +subsubsection {* SML *}
    1.89 +
    1.90 +code_type array (SML "_/ array")
    1.91 +code_const Array (SML "raise/ (Fail/ \"bare Array\")")
    1.92 +code_const Array.new' (SML "Array.array ((_), (_))")
    1.93 +code_const Array.of_list (SML "Array.fromList")
    1.94 +code_const Array.make' (SML "Array.tabulate ((_), (_))")
    1.95 +code_const Array.length' (SML "Array.length")
    1.96 +code_const Array.nth' (SML "Array.sub ((_), (_))")
    1.97 +code_const Array.upd' (SML "Array.update ((_), (_), (_))")
    1.98 +
    1.99 +code_reserved SML Array
   1.100 +
   1.101 +
   1.102 +subsubsection {* OCaml *}
   1.103 +
   1.104 +code_type array (OCaml "_/ array")
   1.105 +code_const Array (OCaml "failwith/ \"bare Array\"")
   1.106 +code_const Array.new' (OCaml "Array.make")
   1.107 +code_const Array.of_list (OCaml "Array.of_list")
   1.108 +code_const Array.make' (OCaml "Array.init")
   1.109 +code_const Array.length' (OCaml "Array.length")
   1.110 +code_const Array.nth' (OCaml "Array.get")
   1.111 +code_const Array.upd' (OCaml "Array.set")
   1.112 +
   1.113 +code_reserved OCaml Array
   1.114 +
   1.115 +
   1.116 +subsubsection {* Haskell *}
   1.117 +
   1.118 +code_type array (Haskell "STArray '_s _")
   1.119 +code_const Array (Haskell "error/ \"bare Array\"")
   1.120 +code_const Array.new' (Haskell "newArray/ (0,/ _)")
   1.121 +code_const Array.of_list' (Haskell "newListArray/ (0,/ _)")
   1.122 +code_const Array.length' (Haskell "length")
   1.123 +code_const Array.nth' (Haskell "readArray")
   1.124 +code_const Array.upd' (Haskell "writeArray")
   1.125 +
   1.126 +
   1.127  end

     2.1 --- a/src/HOL/Library/Heap_Monad.thy	Thu Feb 28 15:55:33 2008 +0100
     2.2 +++ b/src/HOL/Library/Heap_Monad.thy	Thu Feb 28 16:50:52 2008 +0100
     2.3 @@ -274,4 +274,101 @@
     2.4  
     2.5  hide (open) const heap execute
     2.6  
     2.7 +
     2.8 +subsection {* Code generator setup *}
     2.9 +
    2.10 +subsubsection {* Logical intermediate layer *}
    2.11 +
    2.12 +definition
    2.13 +  Fail :: "message_string \<Rightarrow> exception"
    2.14 +where
    2.15 +  [code func del]: "Fail s = Exn"
    2.16 +
    2.17 +definition
    2.18 +  raise_exc :: "exception \<Rightarrow> 'a Heap"
    2.19 +where
    2.20 +  [code func del]: "raise_exc e = raise []"
    2.21 +
    2.22 +lemma raise_raise_exc [code func, code inline]:
    2.23 +  "raise s = raise_exc (Fail (STR s))"
    2.24 +  unfolding Fail_def raise_exc_def raise_def ..
    2.25 +
    2.26 +hide (open) const Fail raise_exc
    2.27 +
    2.28 +
    2.29 +subsubsection {* SML *}
    2.30 +
    2.31 +code_type Heap (SML "_")
    2.32 +code_const Heap (SML "raise/ (Fail/ \"bare Heap\")")
    2.33 +code_monad run "op \<guillemotright>=" SML
    2.34 +code_const run (SML "_")
    2.35 +code_const return (SML "_")
    2.36 +code_const "Heap_Monad.Fail" (SML "Fail")
    2.37 +code_const "Heap_Monad.raise_exc" (SML "raise")
    2.38 +
    2.39 +
    2.40 +subsubsection {* OCaml *}
    2.41 +
    2.42 +code_type Heap (OCaml "_")
    2.43 +code_const Heap (OCaml "failwith/ \"bare Heap\"")
    2.44 +code_monad run "op \<guillemotright>=" OCaml
    2.45 +code_const run (OCaml "_")
    2.46 +code_const return (OCaml "_")
    2.47 +code_const "Heap_Monad.Fail" (OCaml "Failure")
    2.48 +code_const "Heap_Monad.raise_exc" (OCaml "raise")
    2.49 +
    2.50 +code_reserved OCaml Failure raise
    2.51 +
    2.52 +
    2.53 +subsubsection {* Haskell *}
    2.54 +
    2.55 +text {* Adaption layer *}
    2.56 +
    2.57 +code_include Haskell "STMonad"
    2.58 +{*import qualified Control.Monad;
    2.59 +import qualified Control.Monad.ST;
    2.60 +import qualified Data.STRef;
    2.61 +import qualified Data.Array.ST;
    2.62 +
    2.63 +type ST s a = Control.Monad.ST.ST s a;
    2.64 +type STRef s a = Data.STRef.STRef s a;
    2.65 +type STArray s a = Data.Array.ST.STArray s Integer a;
    2.66 +
    2.67 +runST :: (forall s. ST s a) -> a;
    2.68 +runST s = Control.Monad.ST.runST s;
    2.69 +
    2.70 +newSTRef = Data.STRef.newSTRef;
    2.71 +readSTRef = Data.STRef.readSTRef;
    2.72 +writeSTRef = Data.STRef.writeSTRef;
    2.73 +
    2.74 +newArray :: (Integer, Integer) -> a -> ST s (STArray s a);
    2.75 +newArray = Data.Array.ST.newArray;
    2.76 +
    2.77 +newListArray :: (Integer, Integer) -> [a] -> ST s (STArray s a);
    2.78 +newListArray = Data.Array.ST.newListArray;
    2.79 +
    2.80 +length :: STArray s a -> ST s Integer;
    2.81 +length a = Control.Monad.liftM snd (Data.Array.ST.getBounds a);
    2.82 +
    2.83 +readArray :: STArray s a -> Integer -> ST s a;
    2.84 +readArray = Data.Array.ST.readArray;
    2.85 +
    2.86 +writeArray :: STArray s a -> Integer -> a -> ST s ();
    2.87 +writeArray = Data.Array.ST.writeArray;*}
    2.88 +
    2.89 +code_reserved Haskell ST STRef Array
    2.90 +  runST
    2.91 +  newSTRef reasSTRef writeSTRef
    2.92 +  newArray newListArray bounds readArray writeArray
    2.93 +
    2.94 +text {* Monad *}
    2.95 +
    2.96 +code_type Heap (Haskell "ST '_s _")
    2.97 +code_const Heap (Haskell "error \"bare Heap\")")
    2.98 +code_const evaluate (Haskell "runST")
    2.99 +code_monad run bindM Haskell
   2.100 +code_const return (Haskell "return")
   2.101 +code_const "Heap_Monad.Fail" (Haskell "_")
   2.102 +code_const "Heap_Monad.raise_exc" (Haskell "error")
   2.103 +
   2.104  end

     3.1 --- a/src/HOL/Library/Ref.thy	Thu Feb 28 15:55:33 2008 +0100
     3.2 +++ b/src/HOL/Library/Ref.thy	Thu Feb 28 16:50:52 2008 +0100
     3.3 @@ -29,6 +29,7 @@
     3.4    update :: "'a ref \<Rightarrow> ('a\<Colon>heap) \<Rightarrow> unit Heap" ("_ := _" 62) where
     3.5    [code del]: "update r e = Heap_Monad.heap (\<lambda>h. ((), set_ref r e h))"
     3.6  
     3.7 +
     3.8  subsection {* Derivates *}
     3.9  
    3.10  definition
    3.11 @@ -42,6 +43,7 @@
    3.12  
    3.13  hide (open) const new lookup update change
    3.14  
    3.15 +
    3.16  subsection {* Properties *}
    3.17  
    3.18  lemma lookup_chain:
    3.19 @@ -53,4 +55,37 @@
    3.20    "r := e = Ref.change (\<lambda>_. e) r \<guillemotright> return ()"
    3.21    by (auto simp add: monad_simp change_def lookup_chain)
    3.22  
    3.23 +
    3.24 +subsection {* Code generator setup *}
    3.25 +
    3.26 +subsubsection {* SML *}
    3.27 +
    3.28 +code_type ref (SML "_/ ref")
    3.29 +code_const Ref (SML "raise/ (Fail/ \"bare Ref\")")
    3.30 +code_const Ref.new (SML "ref")
    3.31 +code_const Ref.lookup (SML "'!")
    3.32 +code_const Ref.update (SML infixl 3 ":=")
    3.33 +
    3.34 +code_reserved SML ref
    3.35 +
    3.36 +
    3.37 +subsubsection {* OCaml *}
    3.38 +
    3.39 +code_type ref (OCaml "_/ ref")
    3.40 +code_const Ref (OCaml "failwith/ \"bare Ref\"")
    3.41 +code_const Ref.new (OCaml "ref")
    3.42 +code_const Ref.lookup (OCaml "'!")
    3.43 +code_const Ref.update (OCaml infixr 1 ":=")
    3.44 +
    3.45 +code_reserved OCaml ref
    3.46 +
    3.47 +
    3.48 +subsubsection {* Haskell *}
    3.49 +
    3.50 +code_type ref (Haskell "STRef '_s _")
    3.51 +code_const Ref (Haskell "error/ \"bare Ref\"")
    3.52 +code_const Ref.new (Haskell "newSTRef")
    3.53 +code_const Ref.lookup (Haskell "readSTRef")
    3.54 +code_const Ref.update (Haskell "writeSTRef")
    3.55 +
    3.56  end
    3.57 \ No newline at end of file