diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-03-25 23:45:00 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-03-25 23:45:04 +0000 |
| commit | 714eefa9224786617aa7f81b6805b4a88e6744d8 (patch) | |
| tree | c7511e8d28ed97fab22dfcf6e0ef172e02441226 /src/verilog/PrettyPrint.ml | |
| parent | b21ac469facf8d9f9a20d86b306eecd0a70d8749 (diff) | |
| download | vericert-kvx-714eefa9224786617aa7f81b6805b4a88e6744d8.tar.gz vericert-kvx-714eefa9224786617aa7f81b6805b4a88e6744d8.zip | |
Update printing
Diffstat (limited to 'src/verilog/PrettyPrint.ml')
| -rw-r--r-- | src/verilog/PrettyPrint.ml | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/src/verilog/PrettyPrint.ml b/src/verilog/PrettyPrint.ml index 9b7750d..cb72226 100644 --- a/src/verilog/PrettyPrint.ml +++ b/src/verilog/PrettyPrint.ml @@ -16,7 +16,13 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -open Extraction.VerilogAST +open VerilogAST +open Registers +open Datatypes + +open Compcert.Camlcoq + +open Printf let concat = String.concat "" @@ -43,9 +49,11 @@ let pprint_binop = function | Or -> " | " | Xor -> " ^ " +let register (a : positive) : int = P.to_int a + let rec pprint_expr = function | Lit l -> pprint_value l - | Var s -> List.to_seq s |> String.of_seq + | Var s -> sprintf "reg_%d" (register s) | Neg e -> concat ["(-"; pprint_expr e; ")"] | BinOp (op, a, b) -> concat ["("; pprint_expr a; pprint_binop op; pprint_expr b; ")"] | Ternary (c, t, f) -> concat ["("; pprint_expr c; " ? "; pprint_expr t; " : "; pprint_expr f; ")"] |