--- a/NEWS Tue Nov 20 22:53:59 2012 +0100
+++ b/NEWS Wed Nov 21 09:07:41 2012 +0100
@@ -212,6 +212,8 @@
from sorted associative lists. Merging two trees with rbt_union may
return a structurally different tree than before. MINOR INCOMPATIBILITY.
+* Library/IArray.thy: immutable arrays with code generation.
+
* Simproc "finite_Collect" rewrites set comprehensions into pointfree
expressions.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/IArray.thy Wed Nov 21 09:07:41 2012 +0100
@@ -0,0 +1,53 @@
+header "Immutable Arrays with Code Generation"
+
+theory IArray
+imports "~~/src/HOL/Library/Efficient_Nat"
+begin
+
+text{* Immutable arrays are lists wrapped up in an additional constructor.
+There are no update operations. Hence code generation can safely implement
+this type by efficient target language arrays. Currently only SML is
+provided. Should be extended to other target languages and more operations.
+
+Note that arrays cannot be printed directly but only by turning them into
+lists first. Arrays could be converted back into lists for printing if they
+were wrapped up in an additional constructor. *}
+
+datatype 'a iarray = IArray "'a list"
+
+fun of_fun :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a iarray" where
+"of_fun f n = IArray (map f [0..<n])"
+hide_const (open) of_fun
+
+fun length :: "'a iarray \<Rightarrow> nat" where
+"length (IArray xs) = List.length xs"
+hide_const (open) length
+
+fun sub :: "'a iarray \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
+"(IArray as) !! n = as!n"
+hide_const (open) sub
+
+fun list_of :: "'a iarray \<Rightarrow> 'a list" where
+"list_of (IArray xs) = xs"
+hide_const (open) list_of
+
+
+subsection "Code Generation"
+
+code_type iarray
+ (SML "_ Vector.vector")
+
+code_const IArray
+ (SML "Vector.fromList")
+code_const IArray.sub
+ (SML "Vector.sub(_,_)")
+code_const IArray.length
+ (SML "Vector.length")
+code_const IArray.of_fun
+ (SML "!(fn f => fn n => Vector.tabulate(n,f))")
+
+lemma list_of_code[code]:
+ "IArray.list_of A = map (%n. A!!n) [0..< IArray.length A]"
+by (cases A) (simp add: map_nth)
+
+end
--- a/src/HOL/ROOT Tue Nov 20 22:53:59 2012 +0100
+++ b/src/HOL/ROOT Wed Nov 21 09:07:41 2012 +0100
@@ -49,6 +49,7 @@
(* Code_Prolog FIXME cf. 76965c356d2a *)
Code_Real_Approx_By_Float
Code_Target_Numeral
+ IArray
Refute
theories [condition = ISABELLE_FULL_TEST]
Sum_of_Squares_Remote
@@ -484,6 +485,7 @@
FinFunPred
Set_Comprehension_Pointfree_Tests
Parallel_Example
+ IArray_Examples
theories SVC_Oracle
theories [condition = SVC_HOME]
svc_test
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/IArray_Examples.thy Wed Nov 21 09:07:41 2012 +0100
@@ -0,0 +1,26 @@
+theory IArray_Examples
+imports "~~/src/HOL/Library/IArray"
+begin
+
+lemma "IArray [True,False] !! 1 = False"
+by eval
+
+lemma "IArray.length (IArray [[],[]]) = 2"
+by eval
+
+lemma "IArray.list_of (IArray [1,3::int]) = [1,3]"
+by eval
+
+lemma "IArray.list_of (IArray.of_fun (%n. n*n) 5) = [0,1,4,9,16]"
+by eval
+
+fun sum2 :: "'a::monoid_add iarray \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
+"sum2 A n s = (if n=0 then s else sum2 A (n - 1) (s + A!!(n - 1)))"
+
+definition sum :: "'a::monoid_add iarray \<Rightarrow> 'a" where
+"sum A = sum2 A (IArray.length A) 0"
+
+lemma "sum (IArray [1,2,3,4,5,6,7,8,9::int]) = 45"
+by eval
+
+end