# Theory Separation_Logic_Imperative_HOL.Array_Blit

```section ‹Bit Block Transfer and Other Array Optimizations›
theory Array_Blit
imports
"../Sep_Main"
"HOL-Library.Code_Target_Numeral"
begin

subsection "Definition"

(* TODO/FIXME: Does not work with same arrays and overlapping ranges.
Currently, the generated code will throw an exception if the arrays are the same.

If only used with blit_rule, separation logic guarantees that arrays will be disjoint.
*)
primrec blit :: "_ array ⇒ nat ⇒ _ array ⇒ nat ⇒ nat ⇒ unit Heap" where
"blit _ _ _ _ 0 = return ()"
| "blit src si dst di (Suc l) = do {
x ← Array.nth src si;
Array.upd di x dst;
blit src (si+1) dst (di+1) l
}"

lemma blit_rule[sep_heap_rules]:
assumes LEN: "si+len ≤ length lsrc" "di+len ≤ length ldst"
shows
"< src ↦⇩a lsrc
* dst ↦⇩a ldst >
blit src si dst di len
<λ_. src ↦⇩a lsrc
* dst ↦⇩a (take di ldst @ take len (drop si lsrc) @ drop (di+len) ldst)
>"
using LEN
proof (induction len arbitrary: si di ldst)
case 0 thus ?case by sep_auto
next
case (Suc len)
note [sep_heap_rules] = Suc.IH

have [simp]: "⋀x. lsrc ! si # take len (drop (Suc si) lsrc) @ x
= take (Suc len) (drop si lsrc) @ x"
apply simp

from Suc.prems show ?case
by (sep_auto simp: take_update_last drop_upd_irrelevant)
qed

definition nth_oo where "nth_oo v a i ≡ do {
l←Array.len a;
if i<l then
Array.nth a i
else
return v
}"

definition upd_oo where "upd_oo f i x a ≡ do {
l←Array.len a;
if i<l then
Array.upd i x a
else
f
}"

ML_val Array.update

subsection "Code Generator Setup"
code_printing code_module "array_blit" ⇀ (SML)
‹
fun array_blit src si dst di len = (
src=dst andalso raise Fail ("array_blit: Same arrays");
ArraySlice.copy {
di = IntInf.toInt di,
src = ArraySlice.slice (src,IntInf.toInt si,SOME (IntInf.toInt len)),
dst = dst})

fun array_nth_oo v a i () = Array.sub(a,IntInf.toInt i) handle Subscript => v | Overflow => v
fun array_upd_oo f i x a () =
(Array.update(a,IntInf.toInt i,x); a) handle Subscript => f () | Overflow => f ()

›

definition blit' where
[code del]: "blit' src si dst di len
= blit src (nat_of_integer si) dst (nat_of_integer di)
(nat_of_integer len)"

lemma [code]:
"blit src si dst di len
= blit' src (integer_of_nat si) dst (integer_of_nat di)
(integer_of_nat len)" by (simp add: blit'_def)

(* TODO: Export to other languages: OCaml, Haskell *)
code_printing constant blit' ⇀
(SML) "(fn/ ()/ => /array'_blit _ _ _ _ _)"
and (Scala) "{ ('_: Unit)/=>/
def safecopy(src: Array['_], srci: Int, dst: Array['_], dsti: Int, len: Int) = {
if (src eq dst)
sys.error(\"array'_blit: Same arrays\")
else
System.arraycopy(src, srci, dst, dsti, len)
}
safecopy(_.array,_.toInt,_.array,_.toInt,_.toInt)
}"

definition [code del]: "nth_oo' v a == nth_oo v a o nat_of_integer"
definition [code del]: "upd_oo' f == upd_oo f o nat_of_integer"

lemma [code]:
"nth_oo v a == nth_oo' v a o integer_of_nat"
"upd_oo f == upd_oo' f o integer_of_nat"
by (simp_all add: nth_oo'_def upd_oo'_def o_def)

text ‹Fallbacks›
lemmas [code] = nth_oo'_def[unfolded nth_oo_def[abs_def]]
lemmas [code] = upd_oo'_def[unfolded upd_oo_def[abs_def]]

code_printing constant nth_oo' ⇀ (SML) "array'_nth'_oo _ _ _"
| constant upd_oo' ⇀ (SML) "array'_upd'_oo _ _ _ _"

subsection ‹Derived Functions›
definition "array_shrink a s ≡ do {
― ‹Avoiding the need for default value›
l←Array.len a;
if l=s then
return a
else if l=0 then
Array.of_list []
else do {
x←Array.nth a 0;
a'←Array.new s x;
blit a 0 a' 0 s;
return a'
}
}"

lemma array_shrink_rule[sep_heap_rules]:
assumes "s≤length la"
shows "< a↦⇩ala > array_shrink a s <λa'. a'↦⇩atake s la >⇩t"
using assms unfolding array_shrink_def
by sep_auto

definition "array_grow a s x ≡ do {
l←Array.len a;
if l=s then
return a
else do {
a'←Array.new s x;
blit a 0 a' 0 l;
return a'
}
}"

lemma array_grow_rule[sep_heap_rules]:
assumes "s≥length la"
shows "
< a↦⇩ala >
array_grow a s x
<λa'. a'↦⇩a (la @ replicate (s-length la) x)>⇩t"
using assms
unfolding array_grow_def
by sep_auto

export_code array_grow checking SML Scala

(* TODO: Are there system-calls for array-copy? *)
definition "array_copy a ≡ do {
l←Array.len a;
if l=0 then
Array.of_list []
else do {
s ← Array.nth a 0;
a'←Array.new l s;
blit a 0 a' 0 l;
return a'
}
}"

lemma array_copy_rule[sep_heap_rules]:
"
< a↦⇩al>
array_copy a
<λa'. a↦⇩al * a'↦⇩a l>"
unfolding array_copy_def
by sep_auto

export_code array_copy checking SML Scala

end
```