Add pretty printing for Verilog integrated with CompCert

21 files changed, 336 insertions, 332 deletions

diff --git a/Makefile b/Makefile
index eff7f35..415f6ee 100644
--- a/Makefile
+++ b/Makefile
@@ -3,7 +3,7 @@ COMPCERTRECDIRS=lib common $(ARCHDIRS) backend cfrontend driver flocq exportclig
 
 COMPCERTCOQINCLUDES=$(foreach d, $(RECDIRS), -R lib/CompCert/$(d) compcert.$(d))
 
-COQINCLUDES=-R src/CoqUp CoqUp $(COMPCERTCOQINCLUDES)
+COQINCLUDES=-R src/Common CoqUp.Common -R src/Verilog CoqUp.Verilog -R src/Driver CoqUp.Driver -R src/Extraction CoqUp.Extraction $(COMPCERTCOQINCLUDES)
 
 COQEXEC=$(COQBIN)coqtop $(COQINCLUDES) -batch -load-vernac-source
 COQMAKE="$(COQBIN)coq_makefile"
@@ -24,17 +24,17 @@ install:
 coq: Makefile.coq
 	$(MAKE) -f Makefile.coq
 
-extraction: extraction/STAMP
+extraction: src/Extraction/STAMP
 
-compile: extraction/STAMP
+compile: src/Extraction/STAMP
 	@echo "OCaml bin/coqup"
 	@mkdir -p bin
-	@dune build extraction/main.exe
-	@cp _build/default/extraction/main.exe bin/coqup
+	@dune build src/Extraction/Driver.exe
+	@cp _build/default/src/Extraction/Driver.exe bin/coqup
 
-extraction/STAMP:
-	@echo "COQEXEC ./extraction/Extraction.v"
-	@$(COQEXEC) ./extraction/Extraction.v
+src/Extraction/STAMP:
+	@echo "COQEXEC ./src/Extraction/Extraction.v"
+	@$(COQEXEC) ./src/Extraction/Extraction.v
 	@touch $@
 
 Makefile.coq:
diff --git a/_CoqProject b/_CoqProject
index 3d5dae3..54ff493 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,2 +1,16 @@
--R src/CoqUp CoqUp -R lib/CompCert/lib compcert.lib -R lib/CompCert/common compcert.common -R lib/CompCert/x86 compcert.x86 -R lib/CompCert/backend compcert.backend -R lib/CompCert/cfrontend compcert.cfrontend -R lib/CompCert/driver compcert.driver -R lib/CompCert/flocq compcert.flocq -R lib/CompCert/exportclight compcert.exportclight -R lib/CompCert/cparser compcert.cparser -R lib/CompCert/MenhirLib compcert.MenhirLib
+-R src/Common CoqUp.Common
+-R src/Verilog CoqUp.Verilog
+-R src/Driver CoqUp.Driver
+-R src/Extraction CoqUp.Extraction
+
+-R lib/CompCert/lib compcert.lib
+-R lib/CompCert/common compcert.common
+-R lib/CompCert/x86 compcert.x86
+-R lib/CompCert/backend compcert.backend
+-R lib/CompCert/cfrontend compcert.cfrontend
+-R lib/CompCert/driver compcert.driver
+-R lib/CompCert/flocq compcert.flocq
+-R lib/CompCert/exportclight compcert.exportclight
+-R lib/CompCert/cparser compcert.cparser
+-R lib/CompCert/MenhirLib compcert.MenhirLib
 -R lib/CompCert/x86_64 compcert.x86_64
diff --git a/extraction/Extraction.v b/extraction/Extraction.v
deleted file mode 100644
index 4c5f034..0000000
--- a/extraction/Extraction.v
+++ /dev/null
@@ -1,4 +0,0 @@
-From CoqUp Require Import Verilog.
-
-Cd "extraction".
-Separate Extraction Verilog.nat_to_value Verilog.value_to_nat.
diff --git a/extraction/driver.ml b/extraction/driver.ml
deleted file mode 100644
index eb14d45..0000000
--- a/extraction/driver.ml
+++ /dev/null
@@ -1,73 +0,0 @@
-open Compcert
-
-let parse_c_file sourcename ifile =
-  (* Simplification options *)
-  let simplifs =
-    "b" (* blocks: mandatory *)
-    ^ (if false then "s" else "")
-    ^ (if false then "f" else "")
-    ^ (if false then "p" else "")
-  in
-  (* Parsing and production of a simplified C AST *)
-  let ast = Parse.preprocessed_file simplifs sourcename ifile in
-  (* Conversion to Csyntax *)
-  let csyntax = Timing.time "CompCert C generation" C2C.convertProgram ast in
-  (* Save CompCert C AST if requested *)
-  PrintCsyntax.print_if csyntax;
-  csyntax
-
-let compile_c_file sourcename ifile ofile =
-  (* Parse the ast *)
-  let csyntax = parse_c_file sourcename ifile in
-  (* Convert to Asm *)
-  let rtl =
-    match Compiler.apply_partial
-            (CoqUp.transf_frontend csyntax) with
-    | Errors.OK rtl ->
-       rtl
-    | Errors.Error msg ->
-       let loc = file_loc sourcename in
-       fatal_error loc "%a"  print_error msg in
-  (* Print Asm in text form *)
-  let oc = open_out ofile in
-  PrintAsm.print_program oc asm;
-  close_out oc
-
-let compile_i_file sourcename preproname =
-  if !option_interp then begin
-      Machine.config := Machine.compcert_interpreter !Machine.config;
-      let csyntax = parse_c_file sourcename preproname in
-      Interp.execute csyntax;
-      ""
-    end else if !option_S then begin
-      compile_c_file sourcename preproname
-        (output_filename ~final:true sourcename ".c" ".s");
-      ""
-    end else begin
-      let asmname =
-        if !option_dasm
-        then output_filename sourcename ".c" ".s"
-        else tmp_file ".s" in
-      compile_c_file sourcename preproname asmname;
-      let objname = object_filename sourcename ".c" in
-      assemble asmname objname;
-      objname
-    end
-
-(* Processing of a .c file *)
-
-let process_c_file sourcename =
-  ensure_inputfile_exists sourcename;
-  if !option_E then begin
-      preprocess sourcename (output_filename_default "-");
-      ""
-    end else begin
-      let preproname = if !option_dprepro then
-                         output_filename sourcename ".c" ".i"
-                       else
-                         tmp_file ".i" in
-      preprocess sourcename preproname;
-      compile_i_file sourcename preproname
-    end
-
-let _ = print_endline "Hello world"
diff --git a/extraction/dune b/extraction/dune
deleted file mode 100644
index 12a6b8d..0000000
--- a/extraction/dune
+++ /dev/null
@@ -1,8 +0,0 @@
-(executables
- (flags (:standard -warn-error -A))
- (names driver)
- (libraries compcert))
-
-(install
- (section bin)
- (files (driver.exe as coqup)))
diff --git a/src/CoqUp/Helper.v b/src/Common/Helper.v
index 292d011..292d011 100644
--- a/src/CoqUp/Helper.v
+++ b/src/Common/Helper.v
diff --git a/src/CoqUp/Show.v b/src/Common/Show.v
index 83ec5bc..83ec5bc 100644
--- a/src/CoqUp/Show.v
+++ b/src/Common/Show.v
diff --git a/src/CoqUp/Tactics.v b/src/Common/Tactics.v
index 5978d49..5978d49 100644
--- a/src/CoqUp/Tactics.v
+++ b/src/Common/Tactics.v
diff --git a/src/Common/dune b/src/Common/dune
new file mode 100644
index 0000000..de481e2
--- /dev/null
+++ b/src/Common/dune
@@ -0,0 +1,3 @@
+(library
+ (name Common)
+ (public_name coqup.common))
diff --git a/src/CoqUp/CoqUp.v b/src/CoqUp/CoqUp.v
deleted file mode 100644
index 02d71ee..0000000
--- a/src/CoqUp/CoqUp.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Set Implicit Arguments.
-
-Require Import Bool List String.
-
diff --git a/src/CoqUp/Verilog.v b/src/CoqUp/Verilog.v
deleted file mode 100644
index 314c95e..0000000
--- a/src/CoqUp/Verilog.v
+++ /dev/null
@@ -1,234 +0,0 @@
-From Coq Require Import Lists.List Strings.String.
-From Coq Require Import
-Structures.OrderedTypeEx
-FSets.FMapList
-Program.Basics
-PeanoNat.
-From CoqUp Require Import Helper Tactics Show.
-
-Import ListNotations.
-
-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' =>
-      if Nat.even n then
-        cons_value (VBool false) (nat_to_value' sz' (Nat.div n 2))
-      else
-        cons_value (VBool true) (nat_to_value' sz' (Nat.div n 2))
-    end.
-
-  Definition nat_to_value (n : nat) : value :=
-    nat_to_value' ((Nat.log2 n) + 1) n.
-
-  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.
-
-  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 : bool, flat_valueP (VBool 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. trivial.
-      + rewrite Forall_forall in H0. rewrite forallb_forall. intros. subst.
-        apply value_is_bool_equiv. apply H0. assumption.
-    - destruct v. constructor. constructor. unfold flat_value in H.
-      rewrite Forall_forall. rewrite forallb_forall in H. intros. apply value_is_bool_equiv.
-      apply H. assumption.
-  Qed.
-
-  Fixpoint value_to_nat' (i : nat) (v : value) : option nat :=
-    match i, v with
-    | _, VBool b => Some (Nat.b2n b)
-    | _, VArray [VBool b] => Some (Nat.b2n b)
-    | S i', VArray ((VBool b) :: l) =>
-      Option.map (compose (Nat.add (Nat.b2n b)) (Mult.tail_mult 2)) (value_to_nat' i' (VArray l))
-    | _, _ => None
-    end.
-
-  Definition value_length (v : value) : nat :=
-    match v with
-    | VBool _ => 1
-    | VArray l => Datatypes.length l
-    end.
-
-  Definition value_to_nat (v : value) : option nat :=
-    value_to_nat' (value_length v) v.
-
-  Lemma empty_is_flat : flat_valueP (VArray []).
-  Proof.
-    constructor. apply Forall_forall. intros. inversion H.
-  Qed.
-
-  Lemma check_5_is_101 :
-    value_to_nat (VArray [VBool true; VBool false; VBool true]) = Some 5.
-  Proof. reflexivity. Qed.
-
-  Lemma cons_value_flat :
-    forall (b : bool) (v : value),
-      flat_valueP v -> flat_valueP (cons_value (VBool b) v).
-  Proof.
-    intros. unfold cons_value. destruct v.
-    - constructor. apply Forall_forall. intros.
-      inversion H0; subst. constructor.
-      inversion H1; subst. constructor.
-      inversion H2.
-    - intros. inversion H. inversion H1; subst; constructor.
-      + apply Forall_forall. intros.
-        inversion H0; subst. constructor.
-        inversion H2.
-      + repeat constructor. assumption. assumption.
-  Qed.
-
-  Lemma nat_to_value'_is_flat :
-    forall (sz n : nat),
-      flat_valueP (nat_to_value' sz n).
-  Proof.
-    induction sz; intros.
-    - subst. apply empty_is_flat.
-    - unfold_rec nat_to_value'.
-      destruct (Nat.even n); apply cons_value_flat; apply IHsz.
-  Qed.
-
-  Lemma nat_to_value_is_flat :
-    forall (sz n : nat),
-      flat_valueP (nat_to_value n).
-  Proof.
-    intros. unfold nat_to_value. apply nat_to_value'_is_flat.
-  Qed.
-
-  Lemma nat_to_value_idempotent :
-    forall (sz n : nat),
-      sz > 0 -> (value_to_nat' sz (nat_to_value' sz n)) = Some n.
-  Proof.
-    induction sz; intros.
-    - inversion H.
-    - unfold_rec value_to_nat'.
-      assert (flat_valueP (nat_to_value' (S sz) n)).
-      { apply nat_to_value'_is_flat. }
-      destruct (nat_to_value' (S sz) n) eqn:?.
-  Admitted.
-
-  Module VerilogEval.
-
-    Definition app (f : nat -> nat -> nat) (a : value) (b : value) : option value :=
-      Option.map nat_to_value (Option.liftA2 f (value_to_nat a) (value_to_nat b)).
-
-    Definition state_find (k : string) (s : state) : option value :=
-      Map.find k (fst s).
-
-    Definition eval_binop (op : binop) (a1 a2 : value) : option value :=
-      match op with
-      | Plus => app Nat.add a1 a2
-      | Minus => app Nat.sub a1 a2
-      | Times => app Mult.tail_mult a1 a2
-      | Divide => app Nat.div a1 a2
-      | _ => Some a1
-      end.
-
-(*    Fixpoint eval_expr (s : state) (e : expr) : option value :=
-      match e with
-      | Lit n => Some 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/CompCert.v b/src/Driver/CompCert.v
index c984690..c984690 100644
--- a/src/CoqUp/CompCert.v
+++ b/src/Driver/CompCert.v
diff --git a/src/Driver/Driver.ml b/src/Driver/Driver.ml
new file mode 100644
index 0000000..47125fa
--- /dev/null
+++ b/src/Driver/Driver.ml
@@ -0,0 +1,4 @@
+open Verilog
+open Extraction
+
+let _ = print_string (PrettyPrint.prettyprint VerilogAST.verilog_example)
diff --git a/src/Driver/dune b/src/Driver/dune
new file mode 100644
index 0000000..e295a76
--- /dev/null
+++ b/src/Driver/dune
@@ -0,0 +1,7 @@
+(executables
+ (names Driver)
+ (libraries compcert coqup.verilog coqup.extraction))
+
+(install
+ (section bin)
+ (files (Driver.exe as coqup)))
diff --git a/src/Extraction/Extraction.v b/src/Extraction/Extraction.v
new file mode 100644
index 0000000..c4248cb
--- /dev/null
+++ b/src/Extraction/Extraction.v
@@ -0,0 +1,8 @@
+Require CoqUp.Verilog.VerilogAST.
+
+Require Import ExtrOcamlBasic.
+Require Import ExtrOcamlString.
+
+Cd "src/Extraction".
+Separate Extraction
+         VerilogAST.nat_to_value VerilogAST.value_to_nat VerilogAST.verilog VerilogAST.verilog_example.
diff --git a/src/Extraction/dune b/src/Extraction/dune
new file mode 100644
index 0000000..731701a
--- /dev/null
+++ b/src/Extraction/dune
@@ -0,0 +1,4 @@
+(library
+ (name Extraction)
+ (public_name coqup.extraction)
+ (flags (:standard -warn-error -A)))
diff --git a/src/Verilog/PrettyPrint.ml b/src/Verilog/PrettyPrint.ml
new file mode 100644
index 0000000..786d962
--- /dev/null
+++ b/src/Verilog/PrettyPrint.ml
@@ -0,0 +1,48 @@
+open Extraction.VerilogAST
+
+let concat = String.concat ""
+
+let indent i = String.make (2 * i) ' '
+
+let fold_map f s = List.map f s |> concat
+
+let rec pprint_value = function
+  | VBool l -> if l then "1" else "0"
+  (* Assume that array is flat if it's a literal, should probably be changed to a nat or int *)
+  | VArray a -> concat [List.length a |> string_of_int; "'b"; fold_map pprint_value a]
+
+let pprint_binop = function
+  | Plus -> " + "
+  | Minus -> " - "
+  | Times -> " * "
+  | Divide -> " / "
+  | LT -> " < "
+  | GT -> " > "
+  | LE -> " <= "
+  | GE -> " >= "
+  | Eq -> " == "
+  | And -> " & "
+  | Or -> " | "
+  | Xor -> "^"
+
+let rec pprint_expr = function
+  | Lit l -> pprint_value l
+  | Var s -> List.to_seq s |> String.of_seq
+  | Neg e -> concat ["(-"; pprint_expr e; ")"]
+  | BinOp (op, a, b) -> concat ["("; pprint_expr a; pprint_binop op; pprint_expr b; ")"]
+  | Ternary (c, t, f) -> concat ["("; pprint_expr c; " ? "; pprint_expr t; " : "; pprint_expr f; ")"]
+
+let rec pprint_stmnt i =
+  let pprint_case (e, s) = concat [indent (i + 1); pprint_expr e; ":\n"; pprint_stmnt (i+2) s]
+  in function
+  | Skip -> concat [indent i; ";\n"]
+  | Block s -> concat [indent i; "begin\n"; fold_map (pprint_stmnt (i+1)) s; indent i; "end\n"]
+  | Cond (e, st, sf) -> concat [indent i; "if ("; pprint_expr e; ")\n";
+                                pprint_stmnt (i + 1) st; indent i; "else\n";
+                                pprint_stmnt (i + 1) sf]
+  | Case (e, es) -> concat [indent i; "case ("; pprint_expr e; ")\n";
+                            fold_map pprint_case es; indent i; "endcase"]
+  | Blocking (a, b) -> concat [indent i; pprint_expr a; " = "; pprint_expr b; ";\n"]
+  | Nonblocking (a, b) -> concat [indent i; pprint_expr a; " <= "; pprint_expr b; ";\n"]
+
+let prettyprint = fold_map (pprint_stmnt 0)
diff --git a/src/Verilog/PrettyPrint.mli b/src/Verilog/PrettyPrint.mli
new file mode 100644
index 0000000..843feec
--- /dev/null
+++ b/src/Verilog/PrettyPrint.mli
@@ -0,0 +1 @@
+val prettyprint : Extraction.VerilogAST.verilog -> string
diff --git a/src/Verilog/VerilogAST.v b/src/Verilog/VerilogAST.v
new file mode 100644
index 0000000..0c2b38b
--- /dev/null
+++ b/src/Verilog/VerilogAST.v
@@ -0,0 +1,231 @@
+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.
+
+Import ListNotations.
+
+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' =>
+    if Nat.even n then
+      cons_value (VBool false) (nat_to_value' sz' (Nat.div n 2))
+    else
+      cons_value (VBool true) (nat_to_value' sz' (Nat.div n 2))
+  end.
+
+Definition nat_to_value (n : nat) : value :=
+  nat_to_value' ((Nat.log2 n) + 1) n.
+
+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).
+
+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 []].
+
+Coercion VBool : bool >-> value.
+Coercion Lit : value >-> expr.
+Coercion Var : string >-> expr.
+
+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 : bool, flat_valueP (VBool 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. trivial.
+    + rewrite Forall_forall in H0. rewrite forallb_forall. intros. subst.
+      apply value_is_bool_equiv. apply H0. assumption.
+  - destruct v. constructor. constructor. unfold flat_value in H.
+    rewrite Forall_forall. rewrite forallb_forall in H. intros. apply value_is_bool_equiv.
+    apply H. assumption.
+Qed.
+
+Fixpoint value_to_nat' (i : nat) (v : value) : option nat :=
+  match i, v with
+  | _, VBool b => Some (Nat.b2n b)
+  | _, VArray [VBool b] => Some (Nat.b2n b)
+  | S i', VArray ((VBool b) :: l) =>
+    Option.map (compose (Nat.add (Nat.b2n b)) (Mult.tail_mult 2)) (value_to_nat' i' (VArray l))
+  | _, _ => None
+  end.
+
+Definition value_length (v : value) : nat :=
+  match v with
+  | VBool _ => 1
+  | VArray l => Datatypes.length l
+  end.
+
+Definition value_to_nat (v : value) : option nat :=
+  value_to_nat' (value_length v) v.
+
+Lemma empty_is_flat : flat_valueP (VArray []).
+Proof.
+  constructor. apply Forall_forall. intros. inversion H.
+Qed.
+
+Lemma check_5_is_101 :
+  value_to_nat (VArray [VBool true; VBool false; VBool true]) = Some 5.
+Proof. reflexivity. Qed.
+
+Lemma cons_value_flat :
+  forall (b : bool) (v : value),
+    flat_valueP v -> flat_valueP (cons_value (VBool b) v).
+Proof.
+  intros. unfold cons_value. destruct v.
+  - constructor. apply Forall_forall. intros.
+    inversion H0; subst. constructor.
+    inversion H1; subst. constructor.
+    inversion H2.
+  - intros. inversion H. inversion H1; subst; constructor.
+    + apply Forall_forall. intros.
+      inversion H0; subst. constructor.
+      inversion H2.
+    + repeat constructor. assumption. assumption.
+Qed.
+
+Lemma nat_to_value'_is_flat :
+  forall (sz n : nat),
+    flat_valueP (nat_to_value' sz n).
+Proof.
+  induction sz; intros.
+  - subst. apply empty_is_flat.
+  - unfold_rec nat_to_value'.
+    destruct (Nat.even n); apply cons_value_flat; apply IHsz.
+Qed.
+
+Lemma nat_to_value_is_flat :
+  forall (sz n : nat),
+    flat_valueP (nat_to_value n).
+Proof.
+  intros. unfold nat_to_value. apply nat_to_value'_is_flat.
+Qed.
+
+Lemma nat_to_value_idempotent :
+  forall (sz n : nat),
+    sz > 0 -> (value_to_nat' sz (nat_to_value' sz n)) = Some n.
+Proof.
+  induction sz; intros.
+  - inversion H.
+  - unfold_rec value_to_nat'.
+    assert (flat_valueP (nat_to_value' (S sz) n)).
+    { apply nat_to_value'_is_flat. }
+    destruct (nat_to_value' (S sz) n) eqn:?.
+Admitted.
+
+Module VerilogEval.
+
+  Definition app (f : nat -> nat -> nat) (a : value) (b : value) : option value :=
+    Option.map nat_to_value (Option.liftA2 f (value_to_nat a) (value_to_nat b)).
+
+  Definition state_find (k : string) (s : state) : option value :=
+    Map.find k (fst s).
+
+  Definition eval_binop (op : binop) (a1 a2 : value) : option value :=
+    match op with
+    | Plus => app Nat.add a1 a2
+    | Minus => app Nat.sub a1 a2
+    | Times => app Mult.tail_mult a1 a2
+    | Divide => app Nat.div a1 a2
+    | _ => Some a1
+    end.
+
+(*    Fixpoint eval_expr (s : state) (e : expr) : option value :=
+      match e with
+      | Lit n => Some 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.
diff --git a/src/Verilog/dune b/src/Verilog/dune
new file mode 100644
index 0000000..227d4a5
--- /dev/null
+++ b/src/Verilog/dune
@@ -0,0 +1,4 @@
+(library
+ (name Verilog)
+ (public_name coqup.verilog)
+ (libraries coqup.extraction))
diff --git a/src/dune b/src/dune
new file mode 100644
index 0000000..1c9fdde
--- /dev/null
+++ b/src/dune
@@ -0,0 +1,3 @@
+(library
+ (name CoqUp)
+ (public_name coqup))