Demote compare #1267
Demote compare #1267
Conversation
These allow users to test equalites between type variables and branch on the results. This could nearly be accomplished by instead demoting the value of the numeric expressions to integers and comparing them as integers. However, this required `fin` constraints on the expressions, which is sometimes undesirable. We also implement the `coerceSize` operation discussed in issue #704. We may decide to make this a primitive at a later time.
| * 'True' when 'm <= n' and 'False' otherwise. | ||
| */ | ||
| primitive compareLeq : { m : #, n : # } Bit | ||
|
|
||
| /** |
There was a problem hiding this comment.
In the interest of keeping the number of primitives down, I wonder if it might be better to add a single demoteNumeric primitve? Perhaps something like this:
demoteNumeric : { m : # } => (Bool,Integer)
The first component indicates if the number is infinite, so finite numbers would be of the form (false,n) and infinity would be (true,0). I guess it would be prettier to expose InfNat, but I am not sure it is worth the extra work.
There was a problem hiding this comment.
I was envisioning a demoteConstraint that takes logic about inf into account.
There was a problem hiding this comment.
Also, I was able to get isPrefix to work, so perhaps we only need a narrow solution for cases like coerceSize?
isPrefix : {m, n, a} (fin n, Eq a) => [m]a -> [n]a -> Bit
isPrefix xs x =
if `(min n m) < `n then False
else and [ xi == xsi | xi <- x | xsi <- xs ]
There was a problem hiding this comment.
Oh, that trick with min is interesting. We can probably reduce everything we want to do down to just the compareEq primitive with clever uses of min and max. Or, Iavor's idea would also work.
There was a problem hiding this comment.
Hm, demoteConstraint as a primitive seems tricky, as it is not clear what would be its type. I think for now we should go with a simpler solution, and the "proper" fix would be to add a GADT style language construct for examining numeric types.
Add primitives for computing value-level results from comparing number types.