From 5fceb6772ae35c4d3847aa07ee414b79224f1fb3 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Mon, 23 Mar 2020 20:44:12 +0000
Subject: Rename to HTL

---
 src/verilog/HTL.v | 73 +++++++++++++++++++++++++++++++++++++++++++++++++++++++
 src/verilog/VTL.v | 63 -----------------------------------------------
 2 files changed, 73 insertions(+), 63 deletions(-)
 create mode 100644 src/verilog/HTL.v
 delete mode 100644 src/verilog/VTL.v

diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v
new file mode 100644
index 0000000..1fc6932
--- /dev/null
+++ b/src/verilog/HTL.v
@@ -0,0 +1,73 @@
+From coqup.common Require Import Coquplib.
+
+From compcert Require Op Maps.
+From compcert Require AST Memory Registers.
+
+Definition node := positive.
+
+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.
+
+Record inst : Type :=
+  mkinst {
+inst_start : reg;
+inst_finish : reg;
+inst_result : reg;
+inst_args : list reg
+}.
+
+Definition code : Type := Maps.PTree.t instruction.
+
+Definition instantiations : Type := Maps.PTree.t 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
+    }.
+
+Definition moddef := AST.fundef module.
+
+Definition design := AST.program moddef unit.
+
+Definition modsig (md : moddef) :=
+  match md with
+  | AST.Internal m => mod_sig m
+  | AST.External ef => AST.ef_sig ef
+  end.
+
+(** Describes the transformation of VTL instruction by instruction. This applies
+    the transformation to each instruction in the function and returns the new
+    function with the modified instructions. *)
+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).
+
+End TRANSF.
diff --git a/src/verilog/VTL.v b/src/verilog/VTL.v
deleted file mode 100644
index 7273f96..0000000
--- a/src/verilog/VTL.v
+++ /dev/null
@@ -1,63 +0,0 @@
-From coqup.common Require Import Coquplib.
-
-From compcert Require Op Maps.
-From compcert Require AST Memory Registers.
-
-Definition node := positive.
-
-Definition reg := Registers.reg.
-
-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 -> reg + AST.ident -> list reg -> reg -> node -> instruction
-| Vtailinst : AST.signature -> reg + AST.ident -> list reg -> instruction
-| Vcond : Op.condition -> list reg -> node -> node -> instruction
-| Vjumptable : reg -> list node -> instruction
-| Vfinish : option reg -> instruction.
-
-Definition code : Type := Maps.PTree.t instruction.
-
-(** 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 function : Type :=
-  mkfunction {
-      fn_sig : AST.signature;
-      fn_params : list reg;
-      fn_stacksize : Z;
-      fn_code : code;
-      fn_entrypoint : node;
-      fn_calledfuns : list AST.ident
-    }.
-
-Definition fundef := AST.fundef function.
-
-Definition design := AST.program fundef unit.
-
-Definition funsig (fd : fundef) :=
-  match fd with
-  | AST.Internal f => fn_sig f
-  | AST.External ef => AST.ef_sig ef
-  end.
-
-(** Describes the transformation of VTL instruction by instruction. This applies
-    the transformation to each instruction in the function and returns the new
-    function with the modified instructions. *)
-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)
-      f.(fn_calledfuns).
-
-End TRANSF.
-
-- 
cgit