From 7dbed3811e57479c78e4e82806d343d9285576c1 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 8 May 2020 23:34:36 +0100 Subject: Add lessdef for values --- src/verilog/Value.v | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/src/verilog/Value.v b/src/verilog/Value.v index a96d67c..cde98d4 100644 --- a/src/verilog/Value.v +++ b/src/verilog/Value.v @@ -19,8 +19,8 @@ (* begin hide *) From bbv Require Import Word. From bbv Require HexNotation WordScope. -From Coq Require Import ZArith.ZArith. -From compcert Require Import lib.Integers. +From Coq Require Import ZArith.ZArith FSets.FMapPositive. +From compcert Require Import lib.Integers common.Values. (* end hide *) (** * Value @@ -48,7 +48,7 @@ Definition wordToValue : forall sz : nat, word sz -> value := mkvalue. Definition valueToWord : forall v : value, word (vsize v) := vword. -Definition valueToNat (v : value) : nat := +Definition valueToNat (v :value) : nat := wordToNat (vword v). Definition natToValue sz (n : nat) : value := @@ -284,3 +284,10 @@ Module HexNotationValue. Notation "sz ''h' a" := (NToValue sz (hex a)) (at level 50). End HexNotationValue. + +Inductive val_value_lessdef: val -> value -> Prop := +| val_value_lessdef_int: + forall i v', + Integers.Int.unsigned i = valueToZ v' -> + val_value_lessdef (Vint i) v' +| lessdef_undef: forall v, val_value_lessdef Vundef v. -- cgit