-
Notifications
You must be signed in to change notification settings - Fork 2
Description
An unpacking is the binary representation of an integer. Currently we use Vector Bool for that. However the current evaluator doesn't attempt to track the bidwidth of a variable by analysing constraints of the v < c form and so the evaluator and the compiler do not always agree on what the bitwidth of a variable is and sometimes compilation succeeds while evaluation doesn't (but not vice versa). There's a number of ways to approach this problem:
- add a separate type of unpackings instead of using
Vector Booland implementv[i]as "return thei-th bit of thevvariable, unless the variable doesn't have enough bits, in which case return0" - add a
lookupDef : Integer -> a -> Vector a -> aprimitive, which returns a default value if there aren't enough elements in a vector - add the
Maybetype and add the usuallookup : a -> Vector a -> Maybe aprimitive - add the
length : Vector a -> Integerprimitive and define 2 or 3 in terms of it - track bitwidth info in the evaluator like in the compiler
It should be sufficient to implement 5 for current purposes. I kind of like 1, but I don't think it makes much sense from the compilation point of view where you just can't ask for the value of a bit if that bit is outside of the specified bitwidth and we're going to make such specifications mandatory. 3 is too heavyweight of a feature, so out of scope currently. 2 or/and 4 seem useful on their own.
If I don't change my mind about something, then I'll implement 1 at some point.