Pretty-print bitvector expressions

- Add case distinctions between bitvector types and vectors of other element
  types (e.g. registers) and use the corresponding operations (i.e. "bvslice",
"bvaccess", etc for the former, and "slice", "access", etc for the latter) when
pretty-printing expressions
- Add type annotations to expressions when the type includes bitvectors with
  concretely known length
- Update state.lem to use bitvectors (in the interface, at least; internally,
  bitvectors are still stored as bit lists for now, since that makes it easier
to support storing different registers with different lengths)

This has been tested with the CHERI-MIPS model with some success, but some
things are still missing:
- Bitvector patterns are not handled yet
- Some bitvector length monomorphisation is needed in a few places of the model
- Some type annotations are missing, because the (old) Sail type checker does
  not infer bitvector lengths in some instances where one would hope it to do
that; this should be checked with the new type checker

1 files changed, 2 insertions, 2 deletions

diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 426b0811..70850dc1 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -71,12 +71,12 @@ let read_reg_range reg i j =
   read_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger j))
 let read_reg_bit reg i =
   read_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger i)) >>= fun v ->
-  return (extract_only_bit v)
+  return (extract_only_element v)
 let read_reg_field reg regfield =
   read_reg_aux (external_reg_field_whole reg regfield)
 let read_reg_bitfield reg regfield =
   read_reg_aux (external_reg_field_whole reg regfield) >>= fun v ->
-  return (extract_only_bit v)
+  return (extract_only_element v)
 
 val write_reg_aux : reg_name -> vector bitU -> M unit
 let write_reg_aux reg_name v =