From 83e716e65a3d497387e6bf8f33de29fff3bd269d Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Thu, 19 Mar 2020 15:09:59 +0000
Subject: Update names of directories

---
 _CoqProject               | 10 +++++-----
 shell.nix                 |  8 +++++++-
 src/SMTrans/SMTrans.v     | 18 ------------------
 src/Verilog/VerilogAST.v  |  6 +++---
 src/translation/SMTrans.v | 37 +++++++++++++++++++++++++++++++++++++
 5 files changed, 52 insertions(+), 27 deletions(-)
 delete mode 100644 src/SMTrans/SMTrans.v
 create mode 100644 src/translation/SMTrans.v

diff --git a/_CoqProject b/_CoqProject
index 2ac5d91..5fac407 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,8 +1,8 @@
--R src/Common CoqUp.Common
--R src/Verilog CoqUp.Verilog
--R src/Driver CoqUp.Driver
--R src/Extraction CoqUp.Extraction
--R src/SMTrans CoqUp.SMTrans
+-R src/common coqup.common
+-R src/verilog coqup.verilog
+-R src/driver coqup.driver
+-R src/extraction coqup.extraction
+-R src/translation coqup.translation
 
 -R lib/CompCert/lib compcert.lib
 -R lib/CompCert/common compcert.common
diff --git a/shell.nix b/shell.nix
index 84ead99..42cbd1d 100644
--- a/shell.nix
+++ b/shell.nix
@@ -1 +1,7 @@
-import ./.
+with import <nixpkgs> {};
+mkShell {
+  buildInputs = [
+    coq_8_10 ocamlPackages.menhir dune ocaml
+    ocamlPackages.findlib
+  ];
+}
diff --git a/src/SMTrans/SMTrans.v b/src/SMTrans/SMTrans.v
deleted file mode 100644
index f651544..0000000
--- a/src/SMTrans/SMTrans.v
+++ /dev/null
@@ -1,18 +0,0 @@
-(* 
- * CoqUp: Verified high-level synthesis.
- * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
- *
- * This program is free software: you can redistribute it and/or modify
- * it under the terms of the GNU General Public License as published by
- * the Free Software Foundation, either version 3 of the License, or
- * (at your option) any later version.
- *
- * This program is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with this program.  If not, see <https://www.gnu.org/licenses/>.
- *)
-
diff --git a/src/Verilog/VerilogAST.v b/src/Verilog/VerilogAST.v
index 5886652..8bb8ba8 100644
--- a/src/Verilog/VerilogAST.v
+++ b/src/Verilog/VerilogAST.v
@@ -22,7 +22,8 @@ Structures.OrderedTypeEx
 FSets.FMapList
 Program.Basics
 PeanoNat.
-From CoqUp.Common Require Import Helper Tactics Show.
+
+From coqup.common Require Import Helper Tactics Show.
 
 Import ListNotations.
 
@@ -32,8 +33,7 @@ Inductive value : Type :=
 | VBool (b : bool)
 | VArray (l : list value).
 
-Inductive literal : Type :=
-| LitArray (l : list bool).
+Inductive literal : Type := LitArray (l : list bool).
 
 Definition cons_value (a b : value) : value :=
   match a, b with
diff --git a/src/translation/SMTrans.v b/src/translation/SMTrans.v
new file mode 100644
index 0000000..33a65d5
--- /dev/null
+++ b/src/translation/SMTrans.v
@@ -0,0 +1,37 @@
+(* 
+ * CoqUp: Verified high-level synthesis.
+ * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com>
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ *)
+
+From compcert.backend Require RTL.
+
+From coqup.verilog Require VerilogAST.
+
+Definition translation (rtl : RTL.code) : Verilog.verilog :=
+  match rtl with
+  | RTL.Inop ->
+    (** Nop instruction should just become a Skip in Verilog, which is just a semicolon *)
+  | RTL.op ->
+    (** Perform an arithmetic operation over registers. This will just become one binary operation in
+        Verilog. This will contain a list of registers, so these will just become a chain of binary
+        operations in Verilog. *)
+  | RTL.Iload ->
+    (** Load from memory, which will maybe become a load from RAM, however, I'm not sure yet how memory
+        will be implemented or how it will be formalised. *)
+  | RTL.Istore ->
+    (** How memory will be laid out will also affect how stores are handled. For now hopefully these can
+        be ignored, and hopefull they are not used that often when they are not required in C. *)
+  | RTL.Icall -> 
-- 
cgit