diff options
| author | Alasdair Armstrong | 2018-11-13 18:54:35 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-11-13 21:50:28 +0000 |
| commit | 60bcce4648ed029ca3c19c023f5ca525b43eced4 (patch) | |
| tree | 999353452b0d0bcb14e19a6123f4b4c73478679c | |
| parent | 7a0fba122b781a41de080e365c6d360f41117698 (diff) | |
Make pretty printer stricter with brace placement
Also add a special case for shift-left when we are shifting 8 by a two
bit opcode, or 32 by a one bit opcode.
| -rw-r--r-- | lib/arith.sail | 20 | ||||
| -rw-r--r-- | src/pretty_print_sail.ml | 5 |
2 files changed, 22 insertions, 3 deletions
diff --git a/lib/arith.sail b/lib/arith.sail index 61a1ff76..e61ec473 100644 --- a/lib/arith.sail +++ b/lib/arith.sail @@ -50,7 +50,25 @@ val "prerr_int" : (string, int) -> unit // ***** Integer shifts ***** -val shl_int = "shl_int" : (int, int) -> int +/*! +A common idiom in asl is to take two bits of an opcode and convert in into a variable like +``` +let elsize = shl_int(8, UInt(size)) +``` +THIS ensures that in this case the typechecker knows that the end result will be a value in the set `{8, 16, 32, 64}` +*/ +val _shl8 = "shl_int" : + forall 'n, 0 <= 'n <= 3. (int(8), int('n)) -> int('m) with 'm in {8, 16, 32, 64} + +/*! +Similarly, we can shift 32 by either 0 or 1 to get a value in `{32, 64}` +*/ +val _shl32 = "shl_int" : + forall 'n, 'n in {0, 1}. (int(32), int('n)) -> int('m) with 'm in {32, 64} + +val _shl_int = "shl_int" : (int, int) -> int + +overload shl_int = {_shl8, _shl32, _shl_int} val shr_int = "shr_int" : (int, int) -> int diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml index d71b32b2..93693339 100644 --- a/src/pretty_print_sail.ml +++ b/src/pretty_print_sail.ml @@ -119,7 +119,7 @@ let doc_nc = match nc_aux with | NC_true -> string "true" | NC_false -> string "false" - | NC_equal (n1, n2) -> nc_op "=" n1 n2 + | NC_equal (n1, n2) -> nc_op "==" n1 n2 | NC_not_equal (n1, n2) -> nc_op "!=" n1 n2 | NC_bounded_ge (n1, n2) -> nc_op ">=" n1 n2 | NC_bounded_le (n1, n2) -> nc_op "<=" n1 n2 @@ -318,7 +318,8 @@ let fixities = let rec doc_exp (E_aux (e_aux, _) as exp) = match e_aux with | E_block [] -> string "()" - | E_block exps -> surround 2 0 lbrace (doc_block exps) rbrace + | E_block exps -> + group (lbrace ^^ nest 4 (hardline ^^ doc_block exps) ^^ hardline ^^ rbrace) | E_nondet exps -> assert false (* This is mostly for the -convert option *) | E_app_infix (x, id, y) when Id.compare (mk_id "quot") id == 0 -> |