Update printing

4 files changed, 56 insertions, 38 deletions

diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v
index 310efa5..c633874 100644
--- a/src/common/Coquplib.v
+++ b/src/common/Coquplib.v
@@ -38,3 +38,7 @@ Ltac solve_by_inverts n :=
   end.
 
 Ltac solve_by_invert := solve_by_inverts 1.
+
+(* Definition const (A B : Type) (a : A) (b : B) : A := a.
+
+Definition compose (A B C : Type) (f : B -> C) (g : A -> B) (x : A) : C := f (g x). *)
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
index 1fc6932..202a8b7 100644
--- a/src/verilog/HTL.v
+++ b/src/verilog/HTL.v
@@ -1,7 +1,7 @@
 From coqup.common Require Import Coquplib.
 
-From compcert Require Op Maps.
-From compcert Require AST Memory Registers.
+From compcert Require Import Maps.
+From compcert Require Op AST Memory Registers.
 
 Definition node := positive.
 
@@ -10,46 +10,51 @@ Definition reg := Registers.reg.
 Definition ident := AST.ident.
 
 Inductive instruction : Type :=
-| Vnop : node -> instruction
-| Vnonblock : Op.operation -> list reg -> reg -> node -> instruction
-| Vload : AST.memory_chunk -> Op.addressing -> list reg -> reg -> node -> instruction
-| Vstore : AST.memory_chunk -> Op.addressing -> list reg -> reg -> node -> instruction
-| Vinst : AST.signature -> ident -> list reg -> reg -> node -> instruction
-| Vtailinst : AST.signature -> ident -> list reg -> instruction
-| Vcond : Op.condition -> list reg -> node -> node -> instruction
-| Vjumptable : reg -> list node -> instruction
-| Vfinish : option reg -> instruction.
+| Hnop : node -> instruction
+| Hnonblock : Op.operation -> list reg -> reg -> node -> instruction
+  (** [Hnonblock op args res next] Defines a nonblocking assignment to a
+      register, using the operation defined in Op.v. *)
+| Hload : AST.memory_chunk -> Op.addressing -> list reg -> reg -> node -> instruction
+| Hstore : AST.memory_chunk -> Op.addressing -> list reg -> reg -> node -> instruction
+| Hinst : AST.signature -> ident -> reg -> node -> instruction
+  (** [Hinst sig fun args rst strt end res next] Defines the start of a
+      module instantiation, meaning the function will run until the result is
+      returned. *)
+| Htailcall : AST.signature -> ident -> list reg -> instruction
+| Hcond : Op.condition -> list reg -> node -> node -> instruction
+| Hjumptable : reg -> list node -> instruction
+| Hfinish : option reg -> instruction.
 
 Record inst : Type :=
   mkinst {
-inst_start : reg;
-inst_finish : reg;
-inst_result : reg;
-inst_args : list reg
-}.
+    inst_moddecl : ident;
+    inst_args : list reg
+  }.
 
-Definition code : Type := Maps.PTree.t instruction.
+Definition code : Type := PTree.t instruction.
 
-Definition instantiations : Type := Maps.PTree.t inst.
+Definition instances : Type := PTree.t inst.
+
+Definition empty_instances : instances := PTree.empty inst.
 
 (** Function declaration for VTL also contain a construction which describes the
     functions that are called in the current function. This information is used
     to print out *)
 Record module : Type :=
   mkmodule {
-      mod_sig : AST.signature;
-      mod_params : list reg;
-      mod_stacksize : Z;
-      mod_code : code;
-      mod_insts : inst;
-      mod_entrypoint : node
-    }.
+    mod_sig : AST.signature;
+    mod_params : list reg;
+    mod_stacksize : Z;
+    mod_code : code;
+    mod_insts : instances;
+    mod_entrypoint : node
+  }.
 
-Definition moddef := AST.fundef module.
+Definition moddecl := AST.fundef module.
 
-Definition design := AST.program moddef unit.
+Definition design := AST.program moddecl unit.
 
-Definition modsig (md : moddef) :=
+Definition modsig (md : moddecl) :=
   match md with
   | AST.Internal m => mod_sig m
   | AST.External ef => AST.ef_sig ef
@@ -62,12 +67,13 @@ Section TRANSF.
 
   Variable transf : node -> instruction -> instruction.
 
-  Definition transf_function (f : function) : function :=
-    mkfunction
-      f.(fn_sig)
-      f.(fn_params)
-      f.(fn_stacksize)
-      (Maps.PTree.map transf f.(fn_code))
-      f.(fn_entrypoint).
+  Definition transf_function (m : module) : module :=
+    mkmodule
+      m.(mod_sig)
+      m.(mod_params)
+      m.(mod_stacksize)
+      (PTree.map transf m.(mod_code))
+      m.(mod_insts)
+      m.(mod_entrypoint).
 
 End TRANSF.
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; ")"]
diff --git a/src/verilog/PrettyPrint.mli b/src/verilog/PrettyPrint.mli
index a8b6e01..b6478fd 100644
--- a/src/verilog/PrettyPrint.mli
+++ b/src/verilog/PrettyPrint.mli
@@ -16,4 +16,4 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-val prettyprint : Extraction.VerilogAST.verilog -> string
+val prettyprint : VerilogAST.verilog -> string