rems-project / sail

Sail architecture definition language
Other
563 stars 92 forks source link

Use type alias in constraints? #558

Closed Timmmm closed 1 month ago

Timmmm commented 1 month ago

I have this code which works now:

type level_range('v), 'v in {32, 39, 48, 57} =
  range(0, (if 'v == 32 then 1 else (if 'v == 39 then 2 else (if 'v == 48 then 3 else 4))))

struct PTW_Output('v : Int), 'v in {32, 39, 48, 57} = {
  level   : level_range('v),
}

But as you can imagine I am writing {32, 39, 48, 57} in a lot of places! Is there any way to make an alias for it? Something like this:

type svmodes = {32, 39, 48, 57}

type level_range('v), 'v in svmodes =
  range(0, (if 'v == 32 then 1 else (if 'v == 39 then 2 else (if 'v == 48 then 3 else 4))))

struct PTW_Output('v : Int), 'v in svmodes = {
  level   : level_range('v),
}

or even

type svlevels = {32, 39, 48, 57}

type level_range('v : svlevels) =
  range(0, (if 'v == 32 then 1 else (if 'v == 39 then 2 else (if 'v == 48 then 3 else 4))))

struct PTW_Output('v : svlevels) = {
  level   : level_range('v),
}

Neither of those work now. I guess because svlevels would have to be a Kind, but it's only a type? Maybe there's a way to automatically promote constrained integer types to an Int kind plus constraints?

Don't worry if it's a pain. I think we can live with lots of {32, 39, 48, 57} if necessary.

Alasdair commented 1 month ago

You could do:

type svmode('v) -> Bool = 'v in {32, 39, 48, 57}

type level_range('v), svmode('v) =
  range(0, (if 'v == 32 then 1 else (if 'v == 39 then 2 else (if 'v == 48 then 3 else 4))))

struct PTW_Output('v : Int), svmode('v) = {
  level   : level_range('v),
}

The issue here the grammar is pretty restrictive - a constraint can be <numeric_expression> in <set_literal>. You can then make a synonym for the whole constraint, but the set literal cannot be behind a synonym.

Timmmm commented 1 month ago

Ah that's still pretty good, thanks!