Add some thms about v2w + some syntax upgrades

[ordinarymath]

[ordinarymath]

I don't know whether this theorem is good considering the v2n uses + while this one uses ||

[mn200]

The particularly simple theorems look like good candidates for simp.

[ordinarymath]

The issue is the conflicting rewrites between

(v2w [] = 0w) /\
  (v2w (x :: xs) = (if x then ((1w << (LENGTH xs)) || v2w xs) else v2w xs))

And

Theorem v2n:
  v2n [] = 0 /\
  v2n (b::bs) = if b then 2 ** LENGTH bs + v2n bs else v2n bs
Proof

It can be fairly easy to end up needing to prove that the shift equals the addition. Which form should stuff be normalized to.

[ordinarymath]

Note the main motivation of this pr was stuff like v2w (x:xs) not being simplified

[ordinarymath]

The theorem i was attempting to prove was

Definition bits_to_word_def:
  (bits_to_word [] = 0w) /\
  (bits_to_word (T::xs) = (bits_to_word xs << 1 || 1w)) /\
  (bits_to_word (F::xs) = (bits_to_word xs << 1))
End

https://github.com/CakeML/cakeml/blob/901170b785fb177d23b8f92318e9252266eed3ac/compiler/backend/word_to_stackScript.sml#L201 is equal to the v2w reversed.

[mn200]

Strictly, v2w and v2n don't conflict: they have different types and don't refer to each other. If the issue is how to deal with or on words and its connection to addition, that should be addressed in theorems relevant to that situation. I think that using operations appropriate to the types (+ for :num, the shift and logical-or for the :'a word) is entirely reasonable.

The connection between the two constants is presumably expressed with a theorem like

  v2w v = n2w (v2n v)

Given our (generally very strong) preference for n2w forms, you could conceivably make the simp rule be the above.

[ordinarymath]

I would agree that having v2w v = n2w (v2n v) might be a better situation. A normalized word is actually going to end up being n2w n anyway where n is some constant.

[mn200]

Are you planning to finalise this (make it not a draft)?

[ordinarymath]

I don't think I have time to figure out the simp rules so leaving it as just theorems added.

[mn200]

Thanks!