From c9d7e13cbe125a708ce4d4afd9473bae80cc09fc Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sun, 22 Mar 2020 20:34:43 +0000
Subject: Add compcert library to coquplib

---
 src/common/Coquplib.v    |  4 ++++
 src/verilog/VerilogAST.v | 17 +++++++++--------
 2 files changed, 13 insertions(+), 8 deletions(-)

(limited to 'src')

diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v
index b801756..310efa5 100644
--- a/src/common/Coquplib.v
+++ b/src/common/Coquplib.v
@@ -23,6 +23,10 @@ From Coq Require Export
      List
      Bool.
 
+(* Depend on CompCert for the basic library, as they declare and prove some
+   useful theorems. *)
+From compcert.lib Require Export Coqlib.
+
 Ltac unfold_rec c := unfold c; fold c.
 
 Ltac solve_by_inverts n :=
diff --git a/src/verilog/VerilogAST.v b/src/verilog/VerilogAST.v
index 8bb8ba8..88c8ac4 100644
--- a/src/verilog/VerilogAST.v
+++ b/src/verilog/VerilogAST.v
@@ -16,14 +16,15 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From Coq Require Import Lists.List Strings.String.
 From Coq Require Import
 Structures.OrderedTypeEx
 FSets.FMapList
 Program.Basics
 PeanoNat.
 
-From coqup.common Require Import Helper Tactics Show.
+From compcert.backend Require Registers.
+
+From coqup.common Require Import Helper Coquplib Show.
 
 Import ListNotations.
 
@@ -47,7 +48,7 @@ Definition cons_value (a b : value) : value :=
 
 Fixpoint nat_to_value' (sz n : nat) : value :=
   match sz with
-  | 0 => VArray []
+  | 0%nat => VArray []
   | S sz' =>
     if Nat.even n then
       cons_value (VBool false) (nat_to_value' sz' (Nat.div n 2))
@@ -76,7 +77,7 @@ Inductive binop : Type :=
 
 Inductive expr : Type :=
 | Lit (n : value)
-| Var (s : string)
+| Var (s : Registers.reg)
 | Neg (a : expr)
 | BinOp (op : binop) (a1 a2 : expr)
 | Ternary (c t f : expr).
@@ -91,11 +92,11 @@ Inductive stmnt : Type :=
 
 Inductive verilog : Type := Verilog (s : list stmnt).
 
-Definition verilog_example := Verilog [Block [Nonblocking (Var "hello") (BinOp Plus (Lit (nat_to_value 40)) (Lit (nat_to_value 20))); Cond (BinOp LE (Lit (nat_to_value 2)) (Lit (nat_to_value 3))) (Blocking (Var "Another") (BinOp Times (Lit (nat_to_value 20)) (Lit (nat_to_value 500)))) Skip]; Block []].
+Definition verilog_example := Verilog [Block [Nonblocking (Var  2%positive) (BinOp Plus (Lit (nat_to_value 40)) (Lit (nat_to_value 20))); Cond (BinOp LE (Lit (nat_to_value 2)) (Lit (nat_to_value 3))) (Blocking (Var 2%positive) (BinOp Times (Lit (nat_to_value 20)) (Lit (nat_to_value 500)))) Skip]; Block []].
 
 Coercion VBool : bool >-> value.
 Coercion Lit : value >-> expr.
-Coercion Var : string >-> expr.
+Coercion Var : Registers.reg >-> expr.
 
 Definition value_is_bool (v : value) : bool :=
   match v with
@@ -175,7 +176,7 @@ Proof.
 Qed.
 
 Lemma check_5_is_101 :
-  value_to_nat (VArray [VBool true; VBool false; VBool true]) = Some 5.
+  value_to_nat (VArray [VBool true; VBool false; VBool true]) = Some 5%nat.
 Proof. reflexivity. Qed.
 
 Lemma cons_value_flat :
@@ -213,7 +214,7 @@ Qed.
 
 Lemma nat_to_value_idempotent :
   forall (sz n : nat),
-    sz > 0 -> (value_to_nat' sz (nat_to_value' sz n)) = Some n.
+    (sz > 0)%nat -> (value_to_nat' sz (nat_to_value' sz n)) = Some n.
 Proof.
   induction sz; intros.
   - inversion H.
-- 
cgit