diff options
| author | Robert Norton <rmn30@cam.ac.uk> | 2019-06-14 16:40:49 +0100 |
|---|---|---|
| committer | Robert Norton <rmn30@cam.ac.uk> | 2019-06-14 16:40:49 +0100 |
| commit | 36f5da6a169afaba86d2c7191df477ae1837d5d1 (patch) | |
| tree | b66141d2dd7a059727cc465a040174f8ea63a0f0 /model/prelude.sail | |
| parent | 69b805540e868a7d097a28d6a7e84bcc30d628bc (diff) | |
| download | sail-riscv-36f5da6a169afaba86d2c7191df477ae1837d5d1.zip sail-riscv-36f5da6a169afaba86d2c7191df477ae1837d5d1.tar.gz sail-riscv-36f5da6a169afaba86d2c7191df477ae1837d5d1.tar.bz2 | |
Use sail's built-in ones functions for compatibility with smt backend.
Diffstat (limited to 'model/prelude.sail')
| -rw-r--r-- | model/prelude.sail | 14 |
1 files changed, 4 insertions, 10 deletions
diff --git a/model/prelude.sail b/model/prelude.sail index 31d5668..51ed984 100644 --- a/model/prelude.sail +++ b/model/prelude.sail @@ -111,13 +111,10 @@ val zeros_implicit : forall 'n, 'n >= 0 . unit -> bits('n) function zeros_implicit () = sail_zeros('n) overload zeros = {zeros_implicit, sail_zeros} -val ones_n : forall 'n, 'n >= 0 . int('n) -> bits('n) -function ones_n n = replicate_bits (0b1, n) - val ones_implicit : forall 'n, 'n >= 0 . unit -> bits('n) -function ones_implicit () = ones_n ('n) +function ones_implicit () = sail_ones ('n) -overload ones = {ones_implicit, ones_n} +overload ones = {ones_implicit, sail_ones} $else val EXTS : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m) @@ -130,13 +127,10 @@ val zeros_implicit : forall 'n, 'n >= 0 . implicit('n) -> bits('n) function zeros_implicit (n) = sail_zeros(n) overload zeros = {zeros_implicit, sail_zeros} -val ones_n : forall 'n, 'n >= 0 . int('n) -> bits('n) -function ones_n n = replicate_bits (0b1, n) - val ones_implicit : forall 'n, 'n >= 0 . implicit('n) -> bits('n) -function ones_implicit (n) = ones_n (n) +function ones_implicit (n) = sail_ones (n) -overload ones = {ones_implicit, ones_n} +overload ones = {ones_implicit, sail_ones} $endif |