Clarify bidirectional mapping clause restrictions
ThinkOpenly opened this issue · 0 comments
ThinkOpenly commented
Section "Mappings" says:
Sometimes, because the subset of Sail allowed in bidirectional mapping clauses is quite restrictive, it can be useful to specify the forwards and backwards part of a mapping separately
It would be helpful to specify the restrictions more precisely.
For example, apparently, mappings are OK, but function calls are not:
default Order dec
$include <vector.sail>
function rb5 () : unit -> bits(5) = 0b00000
function x() : unit -> bits(16) = rb5() @ 0b00000000000
enum word_width = { BYTE, HALF, WORD, DOUBLE }
enum bzenum = { BZ5, BZ12, BZ16 }
mapping bz5 : bzenum <-> bits(5) = { BZ5 <-> 0b00000 }
mapping size_bits : word_width <-> bits(5) = {
BYTE <-> rb5(),
Type error:
| ^---^
| rb5 is not a union constructor or mapping in mapping-pattern rb5(())
forwards HALF => rb5(),
backwards rb5() => HALF,
Type error:
| ^---^
| rb5 is not a union constructor or mapping in pattern rb5(())
WORD <-> bz5(BZ5),
DOUBLE <-> 0b0 @ 0b0 @ 0b011
}