You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I am trying to make a decode function dependently-typed as val decode : forall 'n, 'n <= 32. bits('n) -> option(ast) so that it could uniformly handle decoding variable-length instructions. But I am having trouble defining clauses of such a decode function with different size arguments in different clauses, e.g., I get a type error of the form:
14 |function clause decode 0xEA = Some(IMP_OP(0xEA,NOP))
| ^--^ checking function argument has type bitvector('n)
| Failed to prove constraint: 8 == 'n
Perhaps this is not allowed or I am making a mistake somewhere? I could always define different decode functions for each allowed instruction length and piece them all together at the end, but I was wondering if my approach above works.
Thanks in advance!
The text was updated successfully, but these errors were encountered:
Currently all the patterns in a function need to have the same width, so the way to go is indeed to have a scattered decode8, decode16, etc, and dispatch to them from a top-level decode function.
I am trying to make a
decode
function dependently-typed asval decode : forall 'n, 'n <= 32. bits('n) -> option(ast)
so that it could uniformly handle decoding variable-length instructions. But I am having trouble defining clauses of such adecode
function with different size arguments in different clauses, e.g., I get a type error of the form:Perhaps this is not allowed or I am making a mistake somewhere? I could always define different decode functions for each allowed instruction length and piece them all together at the end, but I was wondering if my approach above works.
Thanks in advance!
The text was updated successfully, but these errors were encountered: