Re: [isabelle] Working with SML's Word8Array and al
I answer my own question in case some ones else have the same question.
At least `'a array Heap` from `Imperative_HOL` make use of SML's
`Array.array` and this theory seems generic and lightweight enough.
Remains an issue with efficient representation of naturals and integers
(one obviously must be aware of bounds). There use to be an
`Efficient_nat` theory, which is not there any more. According to
https://isabelle.in.tum.de/dist/Isabelle2013-2/NEWS , it was replaced by
`Code_Target_Int`, `Code_Binary_Nat`, `Code_Target_Nat` and
Le Sat, 12 Apr 2014 23:44:40 +0200, Yannick Duchêne (Hibou57)
<yannick_duchene at yahoo.fr> a écrit:
I hope I'm not wrong with this question, but searching the web on the
topic, gave no answer (unless I missed something).
What's the most recommended way to generated SML programs using
Word8Array, Word8ArraySlice, Word8Vector and Word8VectorSlice?
Of course, I guess destructive updates may be an issue… I still feel the
question is worth to be asked, in case it has an answer.
Are there some known papers and/or theories on the topic?
“Syntactic sugar causes cancer of the semi-colons.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and