GaloisInc / daedalus

The Daedalus data description language
BSD 3-Clause "New" or "Revised" License
65 stars 11 forks source link

Support explicit type on bitdata #315

Open jtdaugherty opened 1 year ago

jtdaugherty commented 1 year ago

bitdata declarations with alternatives currently need to annotate at least one alternative with a type to indicate the width of all of the possible alternatives, e.g.,

bitdata Foo where
  X = 0x01: uint 8
  Y = 0x02: uint 8

This is repetitive and leads to redundant type annotations that Daedalus checks anyway, so if one alternative has a different width, you get an error like

  Mismatched constructor widths
    • constructor X has width 2
    • constructor Y has width 8

This ticket proposes that we instead allow the bitdata head itself to be annotated with a type that is then assigned to all of the alternatives, which then no longer need to be annotated explicitly. @yav and I discussed two possible syntax options:

bitdata Foo as uint 8 where
  ...

bitdata Foo: uint 8 where
  ...