diff options
author | Brian Campbell <Brian.Campbell@ed.ac.uk> | 2022-11-14 17:18:35 +0000 |
---|---|---|
committer | Philipp Tomsich <philipp.tomsich@vrull.eu> | 2023-05-31 00:27:23 -0700 |
commit | 566c58eb5a8aa26c2feb8529f2402b5b796ac552 (patch) | |
tree | bd4455bdd9f1f2e3abbf9c44022db3367fd0dbba | |
parent | 3fca4c87b98ebac2c1ecb174e22b4f57c3b1d4ee (diff) | |
download | sail-riscv-566c58eb5a8aa26c2feb8529f2402b5b796ac552.zip sail-riscv-566c58eb5a8aa26c2feb8529f2402b5b796ac552.tar.gz sail-riscv-566c58eb5a8aa26c2feb8529f2402b5b796ac552.tar.bz2 |
Coq updates for Sail 0.15
-rw-r--r-- | handwritten_support/mem_metadata.v | 2 | ||||
-rw-r--r-- | handwritten_support/riscv_extras.v | 14 |
2 files changed, 1 insertions, 15 deletions
diff --git a/handwritten_support/mem_metadata.v b/handwritten_support/mem_metadata.v index dfdbec2..d173848 100644 --- a/handwritten_support/mem_metadata.v +++ b/handwritten_support/mem_metadata.v @@ -73,6 +73,6 @@ Open Scope Z. Definition write_ram {rv e a} wk (addr : mword a) size (v : mword (8 * size)) (meta : unit) : monad rv bool e := write_mem wk a addr size v. -Definition read_ram {rv e a} rk (addr : mword a) size (read_tag : bool) `{ArithFact (size >=? 0)} : monad rv (mword (8 * size) * unit) e := +Definition read_ram {rv e a} rk (addr : mword a) size (read_tag : bool) : monad rv (mword (8 * size) * unit) e := read_mem rk a addr size >>= fun data => returnm (data, tt). diff --git a/handwritten_support/riscv_extras.v b/handwritten_support/riscv_extras.v index ca1c555..e0b685f 100644 --- a/handwritten_support/riscv_extras.v +++ b/handwritten_support/riscv_extras.v @@ -149,20 +149,6 @@ match vs with | (h::_) => returnm h | _ => Fail "empty list in internal_pick" end. -Definition undefined_string {rv e} (_:unit) : monad rv string e := returnm ""%string. -Definition undefined_unit {rv e} (_:unit) : monad rv unit e := returnm tt. -Definition undefined_int {rv e} (_:unit) : monad rv Z e := returnm (0:ii). -(*val undefined_vector : forall 'rv 'a 'e. integer -> 'a -> monad 'rv (list 'a) 'e*) -Definition undefined_vector {rv a e} len (u : a) `{ArithFact (len >=? 0)} : monad rv (vec a len) e := returnm (vec_init u len). -(*val undefined_bitvector : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e*) -Definition undefined_bitvector {rv e} len `{ArithFact (len >=? 0)} : monad rv (mword len) e := returnm (mword_of_int 0). -(*val undefined_bits : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e*) -Definition undefined_bits {rv e} := @undefined_bitvector rv e. -Definition undefined_bit {rv e} (_:unit) : monad rv bitU e := returnm BU. -(*Definition undefined_real {rv e} (_:unit) : monad rv real e := returnm (realFromFrac 0 1).*) -Definition undefined_range {rv e} i j `{ArithFact (i <=? j)} : monad rv {z : Z & ArithFact (i <=? z <=? j)} e := returnm (build_ex i). -Definition undefined_atom {rv e} i : monad rv Z e := returnm i. -Definition undefined_nat {rv e} (_:unit) : monad rv Z e := returnm (0:ii). Definition skip {rv e} (_:unit) : monad rv unit e := returnm tt. |