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 `Code_Target_Numeral`.

Le Sat, 12 Apr 2014 23:44:40 +0200, Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr> a écrit:

Hi,

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.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.