diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-01-24 12:43:52 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-01-24 12:43:52 +0000 |
commit | 48e49a65d66b104c54679ab7ad8854b75931d744 (patch) | |
tree | 9c1d5810d121eadf21717983ad38789ab6df799d /src/CoqUp | |
parent | 9ef4601b795c121622dcc47dfbe947dc378e15bc (diff) | |
download | vericert-48e49a65d66b104c54679ab7ad8854b75931d744.tar.gz vericert-48e49a65d66b104c54679ab7ad8854b75931d744.zip |
Added value_to_nat
Diffstat (limited to 'src/CoqUp')
-rw-r--r-- | src/CoqUp/Helper.v | 13 | ||||
-rw-r--r-- | src/CoqUp/Verilog.v | 30 |
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 |