# HG changeset patch # User nipkow # Date 1353485261 -3600 # Node ID ca989d793b34f27dcb8b99525eaf1191c95e44bf # Parent 0226d408058b9668930cda11eb97cb04c850fa59 new theory of immutable arrays diff -r 0226d408058b -r ca989d793b34 NEWS --- 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. diff -r 0226d408058b -r ca989d793b34 src/HOL/Library/IArray.thy --- /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 \ 'a) \ nat \ 'a iarray" where +"of_fun f n = IArray (map f [0.. nat" where +"length (IArray xs) = List.length xs" +hide_const (open) length + +fun sub :: "'a iarray \ nat \ 'a" (infixl "!!" 100) where +"(IArray as) !! n = as!n" +hide_const (open) sub + +fun list_of :: "'a iarray \ '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 diff -r 0226d408058b -r ca989d793b34 src/HOL/ROOT --- 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 diff -r 0226d408058b -r ca989d793b34 src/HOL/ex/IArray_Examples.thy --- /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 \ nat \ 'a \ '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 \ '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