diff options
| author | Robert Norton | 2018-03-14 16:05:37 +0000 |
|---|---|---|
| committer | Robert Norton | 2018-03-14 18:04:09 +0000 |
| commit | 26c7468c15c15424535afebc12e995a3a746476f (patch) | |
| tree | eef4818c21d114150e781056fccd0a0017c33e39 /mips/prelude.sail | |
| parent | 4c3579a6e4bd10e05f381235e4827b945553d0c1 (diff) | |
rename EXTS and EXTZ to sign_extend and zero_extend because it is more obviosu and to more closely match existing cheri pseudocode.
Diffstat (limited to 'mips/prelude.sail')
| -rw-r--r-- | mips/prelude.sail | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/mips/prelude.sail b/mips/prelude.sail index 272b6e04..63fed9c4 100644 --- a/mips/prelude.sail +++ b/mips/prelude.sail @@ -311,14 +311,14 @@ union exception = { Error_internal_error : unit } -val "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) -val "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) +val _sign_extend = "sign_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) +val _zero_extend = "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) -val EXTS : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m) -val EXTZ : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m) +val sign_extend : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m) +val zero_extend : forall 'n 'm , 'm >= 'n . bits('n) -> bits('m) -function EXTS v = sign_extend(v, sizeof('m)) -function EXTZ v = zero_extend(v, sizeof('m)) +function sign_extend v = _sign_extend(v, sizeof('m)) +function zero_extend v = _zero_extend(v, sizeof('m)) val zeros : forall 'n, 'n >= 0 . unit -> bits('n) function zeros() = replicate_bits (0b0,'n) |