Allow global type variables

Wanted to know yesterday if possible to parameterise specification by 32/64 bits in context of RISCV - i.e. can we do something like

let size = 32
type xlen = bits(size)

This patch tweaks the typechecker slightly to allow type variables to be introduced by global let bindings in the same way they can be introduced by local let bindings (techically this was always allowed, but some bugs prevented it from really working), so

let 'size : atom(32) = 32

means we have a global type variable 'size, with a global constraint 'size  = 32

We can go further though...

let 'size : {|32, 64|} = 32

means we have a global type variable 'size with a constraint 'size = 32 | 'size = 64, in this case the specification will only typecheck if the specification is correct for BOTH 'size = 32 and 'size = 64. This also creates a global binding size (note no tick) with value 32 and type atom('size), one can also do

let _ as 'size : {|32, 64|} = 32

which won't create the binding, only the type variable.

These global type variables are bound to not be very well understood by certain parts of sail, so typical here be dragons warning etc.

0 files changed, 0 insertions, 0 deletions