From d02944ff5704c332f9f5303095dfd2ec7bd421a6 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Wed, 22 Jan 2020 18:30:28 +0000
Subject: Move into src directory

---
 CoqUp/CoqUp.v       |   4 --
 CoqUp/Helper.v      |  10 -----
 CoqUp/Verilog.v     | 105 ----------------------------------------------------
 src/CoqUp/CoqUp.v   |   4 ++
 src/CoqUp/Helper.v  |  10 +++++
 src/CoqUp/Verilog.v | 105 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 6 files changed, 119 insertions(+), 119 deletions(-)
 delete mode 100644 CoqUp/CoqUp.v
 delete mode 100644 CoqUp/Helper.v
 delete mode 100644 CoqUp/Verilog.v
 create mode 100644 src/CoqUp/CoqUp.v
 create mode 100644 src/CoqUp/Helper.v
 create mode 100644 src/CoqUp/Verilog.v

diff --git a/CoqUp/CoqUp.v b/CoqUp/CoqUp.v
deleted file mode 100644
index 02d71ee..0000000
--- a/CoqUp/CoqUp.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Set Implicit Arguments.
-
-Require Import Bool List String.
-
diff --git a/CoqUp/Helper.v b/CoqUp/Helper.v
deleted file mode 100644
index fef7b9e..0000000
--- a/CoqUp/Helper.v
+++ /dev/null
@@ -1,10 +0,0 @@
-Module OptionHelpers.
-
-Definition opt_default {T : Type} (x : T) (u : option T) : T :=
-  match u with
-  | Some y => y
-  | None => x
-  end.
-
-End OptionHelpers.
-Export OptionHelpers.
diff --git a/CoqUp/Verilog.v b/CoqUp/Verilog.v
deleted file mode 100644
index 52bf798..0000000
--- a/CoqUp/Verilog.v
+++ /dev/null
@@ -1,105 +0,0 @@
-From Coq Require Import Lists.List Strings.String.
-From Coq Require Import
-     Structures.OrderedTypeEx
-     FSets.FMapList.
-
-From bbv Require Word.
-
-From CoqUp Require Import Helper.
-
-Module Verilog.
-
-Import ListNotations.
-
-Module Map := FMapList.Make String_as_OT.
-
-Definition state : Type := Map.t nat * Map.t nat.
-
-Inductive binop : Type :=
-| Plus
-| Minus
-| Times
-| Divide
-| LT
-| GT
-| LE
-| GE
-| Eq
-| And
-| Or
-| Xor.
-
-Inductive expr : Type :=
-| Lit (n : nat)
-| Var (s : string)
-| Neg (a : expr)
-| BinOp (op : binop) (a1 a2 : expr)
-| Ternary (c t f : expr).
-
-Inductive stmnt : Type :=
-| Skip
-| Block (s : list stmnt)
-| Cond (c : expr) (st sf : stmnt)
-| Case (c : expr) (b : list (expr * stmnt))
-| Blocking (a b : expr)
-| Nonblocking (a b : expr).
-
-Inductive verilog : Type := Verilog (s : list stmnt).
-
-Coercion Lit : nat >-> expr.
-Coercion Var : string >-> expr.
-
-Module VerilogNotation.
-
-Declare Scope verilog_scope.
-Bind Scope verilog_scope with expr.
-Bind Scope verilog_scope with stmnt.
-Bind Scope verilog_scope with verilog.
-Delimit Scope verilog_scope with verilog.
-
-Notation "x + y" := (BinOp Plus x y) (at level 50, left associativity) : verilog_scope.
-Notation "x - y" := (BinOp Minus x y) (at level 50, left associativity) : verilog_scope.
-Notation "x * y" := (BinOp Times x y) (at level 40, left associativity) : verilog_scope.
-Notation "x / y" := (BinOp Divide x y) (at level 40, left associativity) : verilog_scope.
-Notation "x < y" := (BinOp LT x y) (at level 70, no associativity) : verilog_scope.
-Notation "x <= y" := (BinOp LE x y) (at level 70, no associativity) : verilog_scope.
-Notation "x > y" := (BinOp GT x y) (at level 70, no associativity) : verilog_scope.
-Notation "x >= y" := (BinOp GE x y) (at level 70, no associativity) : verilog_scope.
-Notation "x == y" := (BinOp Eq x y) (at level 70, no associativity) : verilog_scope.
-Notation "x & y" := (BinOp And x y) (at level 40, left associativity) : verilog_scope.
-Notation "x | y" := (BinOp Eq x y) (at level 40, left associativity) : verilog_scope.
-Notation "x ^ y" := (BinOp Eq x y) (at level 30, right associativity) : verilog_scope.
-Notation "~ y" := (Neg y) (at level 75, right associativity) : verilog_scope.
-Notation "c ? t : f" := (Ternary c t f) (at level 20, right associativity) : verilog_scope.
-
-Notation "a '<=!' b" := (Nonblocking a b) (at level 80, no associativity) : verilog_scope.
-Notation "a '=!' b" := (Blocking a b) (at level 80, no associativity) : verilog_scope.
-Notation "'IF' c 'THEN' a 'ELSE' b 'FI'" := (Cond c a b) (at level 80, right associativity) : verilog_scope.
-
-End VerilogNotation.
-
-Module VerilogEval.
-
-Definition state_find (k : string) (s : state) : nat :=
-  opt_default 0 (Map.find k (fst s)).
-
-Definition eval_binop (op : binop) (a1 a2 : nat) : nat :=
-  match op with
-  | Plus => a1 + a2
-  | Minus => a1 - a2
-  | Times => a1 * a2
-  end.
-
-Fixpoint eval_expr (s : state) (e : expr) : nat :=
-  match e with
-  | Lit n => n
-  | Var v => state_find v s
-  | Neg a => 0 - (eval_expr s a)
-  | BinOp op a1 a2 => eval_binop op a1 a2
-  | Ternary c t f => if eval_expr s c then eval_expr s t else eval_expr s f
-  end.
-
-End VerilogEval.
-
-End Verilog.
-Export Verilog.
diff --git a/src/CoqUp/CoqUp.v b/src/CoqUp/CoqUp.v
new file mode 100644
index 0000000..02d71ee
--- /dev/null
+++ b/src/CoqUp/CoqUp.v
@@ -0,0 +1,4 @@
+Set Implicit Arguments.
+
+Require Import Bool List String.
+
diff --git a/src/CoqUp/Helper.v b/src/CoqUp/Helper.v
new file mode 100644
index 0000000..fef7b9e
--- /dev/null
+++ b/src/CoqUp/Helper.v
@@ -0,0 +1,10 @@
+Module OptionHelpers.
+
+Definition opt_default {T : Type} (x : T) (u : option T) : T :=
+  match u with
+  | Some y => y
+  | None => x
+  end.
+
+End OptionHelpers.
+Export OptionHelpers.
diff --git a/src/CoqUp/Verilog.v b/src/CoqUp/Verilog.v
new file mode 100644
index 0000000..52bf798
--- /dev/null
+++ b/src/CoqUp/Verilog.v
@@ -0,0 +1,105 @@
+From Coq Require Import Lists.List Strings.String.
+From Coq Require Import
+     Structures.OrderedTypeEx
+     FSets.FMapList.
+
+From bbv Require Word.
+
+From CoqUp Require Import Helper.
+
+Module Verilog.
+
+Import ListNotations.
+
+Module Map := FMapList.Make String_as_OT.
+
+Definition state : Type := Map.t nat * Map.t nat.
+
+Inductive binop : Type :=
+| Plus
+| Minus
+| Times
+| Divide
+| LT
+| GT
+| LE
+| GE
+| Eq
+| And
+| Or
+| Xor.
+
+Inductive expr : Type :=
+| Lit (n : nat)
+| Var (s : string)
+| Neg (a : expr)
+| BinOp (op : binop) (a1 a2 : expr)
+| Ternary (c t f : expr).
+
+Inductive stmnt : Type :=
+| Skip
+| Block (s : list stmnt)
+| Cond (c : expr) (st sf : stmnt)
+| Case (c : expr) (b : list (expr * stmnt))
+| Blocking (a b : expr)
+| Nonblocking (a b : expr).
+
+Inductive verilog : Type := Verilog (s : list stmnt).
+
+Coercion Lit : nat >-> expr.
+Coercion Var : string >-> expr.
+
+Module VerilogNotation.
+
+Declare Scope verilog_scope.
+Bind Scope verilog_scope with expr.
+Bind Scope verilog_scope with stmnt.
+Bind Scope verilog_scope with verilog.
+Delimit Scope verilog_scope with verilog.
+
+Notation "x + y" := (BinOp Plus x y) (at level 50, left associativity) : verilog_scope.
+Notation "x - y" := (BinOp Minus x y) (at level 50, left associativity) : verilog_scope.
+Notation "x * y" := (BinOp Times x y) (at level 40, left associativity) : verilog_scope.
+Notation "x / y" := (BinOp Divide x y) (at level 40, left associativity) : verilog_scope.
+Notation "x < y" := (BinOp LT x y) (at level 70, no associativity) : verilog_scope.
+Notation "x <= y" := (BinOp LE x y) (at level 70, no associativity) : verilog_scope.
+Notation "x > y" := (BinOp GT x y) (at level 70, no associativity) : verilog_scope.
+Notation "x >= y" := (BinOp GE x y) (at level 70, no associativity) : verilog_scope.
+Notation "x == y" := (BinOp Eq x y) (at level 70, no associativity) : verilog_scope.
+Notation "x & y" := (BinOp And x y) (at level 40, left associativity) : verilog_scope.
+Notation "x | y" := (BinOp Eq x y) (at level 40, left associativity) : verilog_scope.
+Notation "x ^ y" := (BinOp Eq x y) (at level 30, right associativity) : verilog_scope.
+Notation "~ y" := (Neg y) (at level 75, right associativity) : verilog_scope.
+Notation "c ? t : f" := (Ternary c t f) (at level 20, right associativity) : verilog_scope.
+
+Notation "a '<=!' b" := (Nonblocking a b) (at level 80, no associativity) : verilog_scope.
+Notation "a '=!' b" := (Blocking a b) (at level 80, no associativity) : verilog_scope.
+Notation "'IF' c 'THEN' a 'ELSE' b 'FI'" := (Cond c a b) (at level 80, right associativity) : verilog_scope.
+
+End VerilogNotation.
+
+Module VerilogEval.
+
+Definition state_find (k : string) (s : state) : nat :=
+  opt_default 0 (Map.find k (fst s)).
+
+Definition eval_binop (op : binop) (a1 a2 : nat) : nat :=
+  match op with
+  | Plus => a1 + a2
+  | Minus => a1 - a2
+  | Times => a1 * a2
+  end.
+
+Fixpoint eval_expr (s : state) (e : expr) : nat :=
+  match e with
+  | Lit n => n
+  | Var v => state_find v s
+  | Neg a => 0 - (eval_expr s a)
+  | BinOp op a1 a2 => eval_binop op a1 a2
+  | Ternary c t f => if eval_expr s c then eval_expr s t else eval_expr s f
+  end.
+
+End VerilogEval.
+
+End Verilog.
+Export Verilog.
-- 
cgit