Added value_to_nat

2 files changed, 28 insertions, 15 deletions

diff --git a/src/CoqUp/Helper.v b/src/CoqUp/Helper.v
index fef7b9e..f57a16f 100644
--- a/src/CoqUp/Helper.v
+++ b/src/CoqUp/Helper.v
@@ -1,10 +1,15 @@
-Module OptionHelpers.
+Module Option.
 
-Definition opt_default {T : Type} (x : T) (u : option T) : T :=
+Definition default {T : Type} (x : T) (u : option T) : T :=
   match u with
   | Some y => y
   | None => x
   end.
 
-End OptionHelpers.
-Export OptionHelpers.
+Definition map {S : Type} {T : Type} (f : S -> T) (u : option S) : option T :=
+  match u with
+  | Some y => Some (f y)
+  | None => None
+  end.
+
+End Option.
diff --git a/src/CoqUp/Verilog.v b/src/CoqUp/Verilog.v
index 7d3c524..1fe1239 100644
--- a/src/CoqUp/Verilog.v
+++ b/src/CoqUp/Verilog.v
@@ -2,8 +2,8 @@ From Coq Require Import Lists.List Strings.String.
 From Coq Require Import
      Structures.OrderedTypeEx
      FSets.FMapList
-     Program.Basics.
-
+     Program.Basics
+     PeanoNat.
 From CoqUp Require Import Helper.
 
 Import ListNotations.
@@ -72,6 +72,7 @@ Module Verilog.
   Coercion VBool : bool >-> value.
   Coercion Lit : value >-> expr.
   Coercion Var : string >-> expr.
+  Coercion VArray : list >-> value.
 
   Definition value_is_bool (v : value) : bool :=
     match v with
@@ -127,17 +128,24 @@ Module Verilog.
       apply H. assumption.
   Qed.
 
-  Fixpoint value_to_nat (v : value) : option nat :=
+  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 b => Some 0
-    | VArray [] => None
-    | VArray (a :: l) =>
-      match a with
-      | VBool b => None
-      | VArray _ => None
-      end
+    | VBool _ => 0
+    | VArray l => Datatypes.length l
     end.
 
+  Definition value_to_nat (v : value) : option nat :=
+    value_to_nat' (value_length v) v.
+
   Module VerilogNotation.
 
     Declare Scope verilog_scope.
@@ -170,7 +178,7 @@ Module Verilog.
   Module VerilogEval.
 
     Definition state_find (k : string) (s : state) : value :=
-      opt_default (VBool false) (Map.find k (fst s)).
+      Option.default (VBool false) (Map.find k (fst s)).
 
     Definition eval_binop (op : binop) (a1 a2 : value) : value :=
       match op with