Currently the semantics of bitvector operations is defined by the widths of the arguments, this works fine on a fully typed AST, but means a type inference algorithm for bincaml needs to be able to handle width-dependent ad-hoc polymorphic bitvector operations.
The only complex cases are
extend 32 (expr) : bitvec ((32 + width_of expr))
concat e1 e2 : bitvec (width_of e1 + width_of e2)
extract hi lo e1 ==> lo <= hi <= width_of e1
- An approach like Ocaml's weak type variables is appropriate here; we generalise the type of each bitvector operation, hope that there is enough annotation to infer a concrete type and emit a type error when there is not.
- We additionally emit dependent type constraints, or apply a heuristic deduction system to further propagate types in specific cases.
- They could be solved completely using simplex.
Currently the semantics of bitvector operations is defined by the widths of the arguments, this works fine on a fully typed AST, but means a type inference algorithm for bincaml needs to be able to handle width-dependent ad-hoc polymorphic bitvector operations.
The only complex cases are
extend 32 (expr) : bitvec ((32 + width_of expr))
concat e1 e2 : bitvec (width_of e1 + width_of e2)
extract hi lo e1 ==> lo <= hi <= width_of e1