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 Bool and implement v[i] as "return the i-th bit of the v variable, unless the variable doesn't have enough bits, in which case return 0"
- add a
lookupDef : Integer -> a -> Vector a -> a primitive, which returns a default value if there aren't enough elements in a vector
- add the
Maybe type and add the usual lookup : a -> Vector a -> Maybe a primitive
- add the
length : Vector a -> Integer primitive 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.
An unpacking is the binary representation of an integer. Currently we use
Vector Boolfor that. However the current evaluator doesn't attempt to track the bidwidth of a variable by analysing constraints of thev < cform 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:Vector Booland implementv[i]as "return thei-th bit of thevvariable, unless the variable doesn't have enough bits, in which case return0"lookupDef : Integer -> a -> Vector a -> aprimitive, which returns a default value if there aren't enough elements in a vectorMaybetype and add the usuallookup : a -> Vector a -> Maybe aprimitivelength : Vector a -> Integerprimitive and define 2 or 3 in terms of itIt 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.