Re: [isabelle] Arity limitations of type classes? [SOLVED]


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).


Rafal Kolanski.

Brian Huffman wrote:

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.

- Brian

Quoting Rafal Kolanski <rafalk at>:


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.


Rafal Kolanski.

Brian Huffman wrote:
[An ingenious idea]

theory WordsARM imports WordMain begin

class word_len_1 = len +
  assumes word_len_1: "len_of TYPE('a) = 1"

class word_len_1_2 = len +
  assumes word_len_1_2: "len_of TYPE('a) = 1 \<or> len_of TYPE('a) = 2"

class word_len_1_2_4 = len + 
  assumes word_len_1_2_4: "len_of TYPE('a) = 1 \<or> len_of TYPE('a) = 2 \<or> len_of TYPE('a) = 4"

class word_len_2_4_8 = len + 
  assumes word_len_2_4_8: "len_of TYPE('a) = 2 \<or> len_of TYPE('a) = 4 \<or> len_of TYPE('a) = 8"

class word_len_4_8_16 = len + 
  assumes word_len_4_8_16: "len_of TYPE('a) = 4 \<or> len_of TYPE('a) = 8 \<or> len_of TYPE('a) = 16"

class word_len_8_16_32 = len + 
  assumes word_len_8_16_32: "len_of TYPE('a) = 8 \<or> len_of TYPE('a) = 16 \<or> len_of TYPE('a) = 32"

instance num1 :: word_len_1
  by (intro_classes, simp)

instance num1 :: word_len_1_2
  by (intro_classes, simp)

instance num1 :: word_len_1_2_4
  by (intro_classes, simp)

instance bit0 :: (word_len_1) word_len_1_2
  by (intro_classes, simp add: word_len_1)

instance bit0 :: (word_len_1_2) word_len_1_2_4
  by (intro_classes, insert word_len_1_2, simp)

instance bit0 :: (word_len_1_2_4) word_len_2_4_8
  by (intro_classes, insert word_len_1_2_4, simp)

instance bit0 :: (word_len_2_4_8) word_len_4_8_16
  by (intro_classes, insert word_len_2_4_8, simp)

instance bit0 :: (word_len_4_8_16) word_len_8_16_32
  by (intro_classes, insert word_len_4_8_16, simp)


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