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 | |
parent | 9ef4601b795c121622dcc47dfbe947dc378e15bc (diff) | |
download | vericert-kvx-48e49a65d66b104c54679ab7ad8854b75931d744.tar.gz vericert-kvx-48e49a65d66b104c54679ab7ad8854b75931d744.zip |
Added value_to_nat
-rw-r--r-- | Makefile | 6 | ||||
-rw-r--r-- | src/CoqUp/Helper.v | 13 | ||||
-rw-r--r-- | src/CoqUp/Verilog.v | 30 |
3 files changed, 31 insertions, 18 deletions
@@ -1,14 +1,14 @@ IGNORE:= -LIBVS:=$(wildcard CoqUp/Lib/*.v) +LIBVS:=$(wildcard src/CoqUp/Lib/*.v) LIBVS:=$(filter-out $(IGNORE:%=%.v),$(LIBVS)) -VS:=$(wildcard CoqUp/*.v) +VS:=$(wildcard src/CoqUp/*.v) VS:=$(filter-out $(LIBVS) $(IGNORE:%=%.v),$(VS)) .PHONY: coq clean -ARGS := -R CoqUp CoqUp +ARGS := -R src/CoqUp CoqUp coq: Makefile.coq $(MAKE) -f Makefile.coq 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 |