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.
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!