diff options
| author | Thomas Bauereiss | 2017-06-21 11:10:55 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2017-06-21 11:10:55 +0100 |
| commit | 649d5fd1e9ab474e73c16389335b02de77dd3700 (patch) | |
| tree | 1a55ff47d3d71154cc648ea58b8e2d2aeaebdafd /src/pretty_print_ocaml.ml | |
| parent | 606fdd6a90f551a54033f9a69ef1cd28b3b6455e (diff) | |
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
Diffstat (limited to 'src/pretty_print_ocaml.ml')
| -rw-r--r-- | src/pretty_print_ocaml.ml | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/src/pretty_print_ocaml.ml b/src/pretty_print_ocaml.ml index 3772f549..adca6b12 100644 --- a/src/pretty_print_ocaml.ml +++ b/src/pretty_print_ocaml.ml @@ -338,10 +338,7 @@ let doc_exp_ocaml, doc_let_ocaml = | Typ_var (Kid_aux (Var "length",_)) -> parens ((string "set_start_to_length") ^//^ exp e) | _ -> - parens (doc_op colon (group (exp e)) (doc_typ_ocaml typ))) - - -) + parens (doc_op colon (group (exp e)) (doc_typ_ocaml typ)))) | E_tuple exps -> parens (separate_map comma exp exps) | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> @@ -753,4 +750,3 @@ let pp_defs_ocaml f d top_line opens = print f (string "(*" ^^ (string top_line) ^^ string "*)" ^/^ (separate_map hardline (fun lib -> (string "open") ^^ space ^^ (string lib)) opens) ^/^ (doc_defs_ocaml d)) - |