# HG changeset patch
# User haftmann
# Date 1531939880 7200
# Node ID 65ad2bfc19d284ab5cf229fdc5f70ce44991dab5
# Parent 297ca38c7da5977e0307e64eb10776222f6a3639
restructured for future incorporation of Haskell
diff r 297ca38c7da5 r 65ad2bfc19d2 src/HOL/Library/IArray.thy
 a/src/HOL/Library/IArray.thy Wed Jul 18 20:51:19 2018 +0200
+++ b/src/HOL/Library/IArray.thy Wed Jul 18 20:51:20 2018 +0200
@@ 1,17 +1,19 @@
+(* Title: HOL/Library/IArray.thy
+ Author: Tobias Nipkow, TU Muenchen
+*)
+
section \Immutable Arrays with Code Generation\
theory IArray
imports Main
begin
text\Immutable arrays are lists wrapped up in an additional constructor.
+subsection \Fundamental operations\
+
+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.\
+provided. Could be extended to other target languages and more operations.\
context
begin
@@ 47,15 +49,7 @@
end
subsection \Code Generation\

code_reserved SML Vector

code_printing
 type_constructor iarray \ (SML) "_ Vector.vector"
 constant IArray \ (SML) "Vector.fromList"
 constant IArray.all \ (SML) "Vector.all"
 constant IArray.exists \ (SML) "Vector.exists"
+subsection \Generic code equations\
lemma [code]:
"size (as :: 'a iarray) = Suc (length (IArray.list_of as))"
@@ 89,56 +83,6 @@
"HOL.equal as bs \ HOL.equal (IArray.list_of as) (IArray.list_of bs)"
by (cases as, cases bs) (simp add: equal)
context
begin

qualified primrec tabulate :: "integer \ (integer \ 'a) \ 'a iarray" where
 "tabulate (n, f) = IArray (map (f \ integer_of_nat) [0.. nat_of_integer)"
 by simp

code_printing
 constant IArray.tabulate \ (SML) "Vector.tabulate"

context
begin

qualified primrec sub' :: "'a iarray \ integer \ 'a" where
 [code del]: "sub' (as, n) = IArray.list_of as ! nat_of_integer n"

end

lemma [code]:
 "IArray.sub' (IArray as, n) = as ! nat_of_integer n"
 by simp

lemma [code]:
 "as !! n = IArray.sub' (as, integer_of_nat n)"
 by simp

code_printing
 constant IArray.sub' \ (SML) "Vector.sub"

context
begin

qualified definition length' :: "'a iarray \ integer" where
 [code del, simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))"

end

lemma [code]:
 "IArray.length' (IArray as) = integer_of_nat (List.length as)"
 by simp

lemma [code]:
 "IArray.length as = nat_of_integer (IArray.length' as)"
 by simp

context term_syntax
begin
@@ 149,7 +93,59 @@
end
code_printing
 constant IArray.length' \ (SML) "Vector.length"
+
+subsection \Auxiliary operations for code generation\
+
+context
+begin
+
+qualified primrec tabulate :: "integer \ (integer \ 'a) \ 'a iarray" where
+ "tabulate (n, f) = IArray (map (f \ integer_of_nat) [0.. nat_of_integer)"
+ by simp
+
+qualified primrec sub' :: "'a iarray \ integer \ 'a" where
+ "sub' (as, n) = IArray.list_of as ! nat_of_integer n"
+
+lemma [code]:
+ "IArray.sub' (IArray as, n) = as ! nat_of_integer n"
+ by simp
+
+lemma [code]:
+ "as !! n = IArray.sub' (as, integer_of_nat n)"
+ by simp
+
+qualified definition length' :: "'a iarray \ integer" where
+ [simp]: "length' as = integer_of_nat (List.length (IArray.list_of as))"
+
+lemma [code]:
+ "IArray.length' (IArray as) = integer_of_nat (List.length as)"
+ by simp
+
+lemma [code]:
+ "IArray.length as = nat_of_integer (IArray.length' as)"
+ by simp
end
+
+
+subsection \Code Generation for SML\
+
+text \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.\
+
+code_reserved SML Vector
+
+code_printing
+ type_constructor iarray \ (SML) "_ Vector.vector"
+ constant IArray \ (SML) "Vector.fromList"
+ constant IArray.all \ (SML) "Vector.all"
+ constant IArray.exists \ (SML) "Vector.exists"
+ constant IArray.tabulate \ (SML) "Vector.tabulate"
+ constant IArray.sub' \ (SML) "Vector.sub"
+ constant IArray.length' \ (SML) "Vector.length"
+
+end