Email Gateway (Aug 18 2022 at 12:41): Email Gateway (Aug 18 2022 at 12:41):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Brian,
Thank you very much for the detailed explanations. All fixed now. I
guess I got too caught up in the simple joy of being able to finally
state the type class at all :)
I don't know if anyone's interested in this, but I'm attaching the fixed
version of "words for ARM (8,16,32)" in the interest of completeness
(after having checked that "8 word", "16 word" and "32 word" are indeed
instances).
Sincerely,
Rafal Kolanski.
Brian Huffman wrote:
WordsARM.thy
Email Gateway (Aug 18 2022 at 12:47):From: Brian Huffman <brianh@cs.pdx.edu>
Rafal,
Your WordsARM.thy file is still missing two important instance declarations:
instance num1 :: word_len_1_2 (* necessary for 16 :: word_len_8_16_32 *)
by (intro_classes, simp)
instance num1 :: word_len_1_2_4 (* necessary for 8 :: word_len_8_16_32 *)
by (intro_classes, simp)
To see why these are necessary, you can trace what the type checker
does when trying to prove, for example, that 16 :: word_len_8_16_32:
num1 bit0 bit0 bit0 bit0 :: word_len_8_16_32
num1 bit0 bit0 bit0 :: word_len_4_8_16
num1 bit0 bit0 :: word_len_2_4_8
num1 bit0 :: word_len_1_2_4
num1 :: word_len_1_2
Similarly, 8 :: word_len_8_16_32 reduces to num1 :: word_len_1_2_4.
Alternatively, you could prove the subclass relations word_len_1 <
word_len_1_2 < word_len_1_2_4, and the system would infer the missing
class instances for num1 automatically.
Quoting Rafal Kolanski <rafalk@cse.unsw.edu.au>:
Email Gateway (Aug 18 2022 at 12:48):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Using instantiation is indeed not necessary for classes without class
parameters.
Florian
signature.asc
Email Gateway (Aug 18 2022 at 12:48):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Brian,
Thank you very, very much. I've been bashing my head against this for a
while. As of now, thanks to you, I have a non-hacky class of words which
are actually storable in C on a 32-bit architecture.
Regarding Florian's comment on using new-style classes, I'm attaching
what I have (the word_len_8_16_32 class is the one I wanted). It doesn't
use axclasses, but does use instance instead of instantiation as the
proofs are relatively simple.
Sincerely,
Rafal Kolanski.
Brian Huffman wrote:
[An ingenious idea]
WordsARM.thy
Last updated: Nov 21 2024 at 12:39 UTC