Add some proofs about values

1 files changed, 181 insertions, 94 deletions

diff --git a/src/CoqUp/Verilog.v b/src/CoqUp/Verilog.v
index 52bf798..1ec95c1 100644
--- a/src/CoqUp/Verilog.v
+++ b/src/CoqUp/Verilog.v
@@ -1,105 +1,192 @@
 From Coq Require Import Lists.List Strings.String.
 From Coq Require Import
      Structures.OrderedTypeEx
-     FSets.FMapList.
-
-From bbv Require Word.
+     FSets.FMapList
+     Program.Basics.
 
 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.
+Module Verilog.
+
+  Module Map := FMapList.Make String_as_OT.
+
+  Inductive value : Type :=
+  | VBool (b : bool)
+  | VArray (l : list value).
+
+  Definition cons_value (a b : value) : value :=
+    match a, b with
+    | VBool _, VArray b' => VArray (a :: b')
+    | VArray a', VBool _ => VArray (List.concat [a'; [b]])
+    | VArray a', VArray b' => VArray (List.concat [a'; b'])
+    | _, _ => VArray [a; b]
+    end.
+
+  (** * Conversion to and from value *)
+
+  Fixpoint nat_to_value (sz n : nat) : value :=
+    match sz with
+    | 0 => VArray []
+    | S sz' =>
+      match Nat.modulo n 2 with
+      | 0 => cons_value (VBool false) (nat_to_value sz' (Nat.div n 2))
+      | S _ => cons_value (VBool true) (nat_to_value sz' (Nat.div n 2))
+      end
+    end.
+
+  Coercion VBool : bool >-> value.
+
+  Definition value_is_bool (v : value) : bool :=
+    match v with
+    | VBool _ => true
+    | VArray _ => false
+    end.
+
+  Definition value_is_array : value -> bool := compose negb value_is_bool.
+
+  Definition flat_value (v : value) : bool :=
+    match v with
+    | VBool _ => true
+    | VArray l => forallb value_is_bool l
+    end.
+
+  Inductive value_is_boolP : value -> Prop :=
+  | ValIsBool : forall b : bool, value_is_boolP (VBool b).
+
+  Inductive value_is_arrayP : value -> Prop :=
+  | ValIsArray : forall v : list value, value_is_arrayP (VArray v).
+
+  Inductive flat_valueP : value -> Prop :=
+  | FLV0 : forall b : value, value_is_boolP b -> flat_valueP b
+  | FLVA : forall l : list value,
+      Forall (value_is_boolP) l -> flat_valueP (VArray l).
+
+  Lemma value_is_bool_equiv :
+    forall v, value_is_boolP v <-> value_is_bool v = true.
+  Proof.
+    split; intros.
+    - inversion H. trivial.
+    - destruct v. constructor. unfold value_is_bool in H. discriminate.
+  Qed.
+
+  Lemma value_is_array_equiv :
+    forall v, value_is_arrayP v <-> value_is_array v = true.
+  Proof.
+    split; intros.
+    - inversion H. trivial.
+    - destruct v; try constructor. unfold value_is_array in H.
+      unfold compose, value_is_bool, negb in H. discriminate.
+  Qed.
+
+  Lemma flat_value_equiv :
+    forall v, flat_valueP v <-> flat_value v = true.
+  Proof.
+    split; intros.
+    - unfold flat_value. inversion H. subst.
+      destruct v.
+      + trivial.
+      + inversion H0.
+      + subst. rewrite Forall_forall in H0. rewrite forallb_forall.
+        intros. apply value_is_bool_equiv. apply H0. assumption.
+    - unfold flat_value in H. destruct v.
+      + repeat constructor.
+      + constructor. apply value_is_bool_equiv. rewrite forallb_forall in H. 
+
+  Fixpoint value_to_nat (v : value) : option nat :=
+    match v with
+    | VBool b => 0
+    | VArray (l :: ls) =>
+
+  Definition state : Type := Map.t value * Map.t value.
+
+  Inductive binop : Type :=
+  | Plus
+  | Minus
+  | Times
+  | Divide
+  | LT
+  | GT
+  | LE
+  | GE
+  | Eq
+  | And
+  | Or
+  | Xor.
+
+  Inductive expr : Type :=
+  | Lit (n : value)
+  | 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 VBool : bool >-> value.
+  Coercion Lit : value >-> 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) : value :=
+      opt_default (VBool false) (Map.find k (fst s)).
+
+    Definition eval_binop (op : binop) (a1 a2 : value) : value :=
+      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.