rems-project/sail

Clarify bidirectional mapping clause restrictions

ThinkOpenly opened this issue · 0 comments

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
}