Fix Verilog printing

2 files changed, 35 insertions, 33 deletions

diff --git a/src/verilog/PrintVerilog.ml b/src/verilog/PrintVerilog.ml
index cb72226..016a626 100644
--- a/src/verilog/PrintVerilog.ml
+++ b/src/verilog/PrintVerilog.ml
@@ -16,11 +16,10 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-open VerilogAST
-open Registers
+open Verilog
 open Datatypes
 
-open Compcert.Camlcoq
+open Camlcoq
 
 open Printf
 
@@ -30,45 +29,48 @@ let indent i = String.make (2 * i) ' '
 
 let fold_map f s = List.map f s |> concat
 
-let rec pprint_value = function
-  | VBool l -> if l then "1" else "0"
-  (* Assume that array is flat if it's a literal, should probably be changed to a nat or int *)
-  | VArray a -> concat [List.length a |> string_of_int; "'b"; fold_map pprint_value a]
+let pstr pp = fprintf pp "%s"
 
 let pprint_binop = function
-  | Plus -> " + "
-  | Minus -> " - "
-  | Times -> " * "
-  | Divide -> " / "
-  | LT -> " < "
-  | GT -> " > "
-  | LE -> " <= "
-  | GE -> " >= "
-  | Eq -> " == "
-  | And -> " & "
-  | Or -> " | "
-  | Xor -> " ^ "
+  | Vadd -> " + "
+  | Vsub -> " - "
+  | Vmul -> " * "
+  | Vdiv -> " / "
+  | Vmod -> " % "
+  | Vlt -> " < "
+  | Vgt -> " > "
+  | Vle -> " <= "
+  | Vge -> " >= "
+  | Veq -> " == "
+  | Vne -> " != "
+  | Vand -> " & "
+  | Vor -> " | "
+  | Vxor -> " ^ "
+  | Vshl -> " << "
+  | Vshr -> " >> "
 
-let register (a : positive) : int = P.to_int a
+let register a = P.to_int a
+
+let literal l = sprintf "%d'd%d" (Nat.to_int l.vsize) (Z.to_int (valueToZ l))
 
 let rec pprint_expr = function
-  | Lit l -> pprint_value l
-  | 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; ")"]
+  | Vlit l -> literal l
+  | Vvar s -> sprintf "reg_%d" (register s)
+  | Vunop e -> concat ["(~"; pprint_expr e; ")"]
+  | Vbinop (op, a, b) -> concat ["("; pprint_expr a; pprint_binop op; pprint_expr b; ")"]
+  | Vternary (c, t, f) -> concat ["("; pprint_expr c; " ? "; pprint_expr t; " : "; pprint_expr f; ")"]
 
 let rec pprint_stmnt i =
   let pprint_case (e, s) = concat [indent (i + 1); pprint_expr e; ":\n"; pprint_stmnt (i + 2) s]
   in function
-  | Skip -> concat [indent i; ";\n"]
-  | Block s -> concat [indent i; "begin\n"; fold_map (pprint_stmnt (i+1)) s; indent i; "end\n"]
-  | Cond (e, st, sf) -> concat [indent i; "if ("; pprint_expr e; ")\n";
+  | Vskip -> concat [indent i; ";\n"]
+  | Vseq s -> concat [indent i; "begin\n"; fold_map (pprint_stmnt (i+1)) s; indent i; "end\n"]
+  | Vcond (e, st, sf) -> concat [indent i; "if ("; pprint_expr e; ")\n";
                                 pprint_stmnt (i + 1) st; indent i; "else\n";
                                 pprint_stmnt (i + 1) sf]
-  | Case (e, es) -> concat [indent i; "case ("; pprint_expr e; ")\n";
+  | Vcase (e, es) -> concat [indent i; "case ("; pprint_expr e; ")\n";
                             fold_map pprint_case es; indent i; "endcase\n"]
-  | Blocking (a, b) -> concat [indent i; pprint_expr a; " = "; pprint_expr b; ";\n"]
-  | Nonblocking (a, b) -> concat [indent i; pprint_expr a; " <= "; pprint_expr b; ";\n"]
+  | Vblock (a, b) -> concat [indent i; pprint_expr a; " = "; pprint_expr b; ";\n"]
+  | Vnonblock (a, b) -> concat [indent i; pprint_expr a; " <= "; pprint_expr b; ";\n"]
 
-let prettyprint = fold_map (pprint_stmnt 0)
+let print_program pp v = pstr pp (fold_map (pprint_stmnt 0) v)
diff --git a/src/verilog/PrintVerilog.mli b/src/verilog/PrintVerilog.mli
index b6478fd..4197d4a 100644
--- a/src/verilog/PrintVerilog.mli
+++ b/src/verilog/PrintVerilog.mli
@@ -16,4 +16,4 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-val prettyprint : VerilogAST.verilog -> string
+val print_program : out_channel -> Verilog.verilog -> unit