Email Gateway (Aug 19 2022 at 14:18): Email Gateway (Aug 19 2022 at 14:18):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
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?
Email Gateway (Aug 19 2022 at 14:21):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
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.
Last updated: Apr 26 2024 at 01:06 UTC