[isabelle] I need a fixed mutable array
I did a few searches to find whether there are mutable arrays in
Isabelle. It appears there's not, though I found a little info:
I need to simulate the RAM of a cpu, and this is what I've done with a
record and list:
record 'a marray = MList :: "'a list"
definition "array_size_512 = ( (| MList = replicate 0x100 (0::nat) |),
fun array_write :: "('a marray * nat) => nat => 'a => ('a marray * nat)
"array_write (an_array, a_size) index data = (
if (index >= a_size) then None
else Some (an_array(| MList := (MList an_array)[index := data] |),
value "array_write array_size_512 3 1234"
value "array_write array_size_512 0x100 1234"
I'm wondering if there's a better way to do that. Better efficiency
would be good, but efficiency in Isabelle is not of utmost concern,
since it will hopefully represent what will be done in assembly language.
I'm just getting started, but a partial record for a Intel 64-bit cpu
might be something like this, where "Mem" is the fixed mutable array to
record cpu64 =
Ax :: nat
Bx :: nat
Mem :: "nat list"
definition cpu_mem256 :: "cpu64 * nat" where
( (| Ax = 0, Bx = 0, Mem = (replicate 0x100 (0::nat)) |), 0x100::nat )"
fun mem_write :: "(cpu64 * nat) => nat => nat => (cpu64 * nat) option" where
"mem_write (cpu, memsize) addr data = (
if (addr >= memsize) then None
else Some (cpu(| Mem := (Mem cpu)[addr := data] |), memsize)
This is the beginning of an attempt to tie into the SIMD instruction
sets of the AMD and Intel microprocessors. The SIMD instructions use
128-bit and 256-bit registers to do multiple operations at the same
time. I include a lot of links below.
AMD (See AMD64 Arch Programmer's Manuals under the manual heading)
PRO ASSEMBLY LANGUAGE (chapter 17)
This archive was generated by a fusion of
Pipermail (Mailman edition) and