diff options
| author | Brian Campbell | 2018-04-20 10:55:56 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-04-20 10:56:28 +0100 |
| commit | 83b7f7065c638ed3b0e0c40a5c4b64257bae4975 (patch) | |
| tree | 1770aeda7c9f19ece0edd52625284f443485741c /src/gen_lib/sail_operators_mwords.lem | |
| parent | cf3283f176797f9209e3a8b1d5cc76e38f67d471 (diff) | |
Have sign_extend in common Sail Lem library, use it and zero_extend in
mono rewrites
Diffstat (limited to 'src/gen_lib/sail_operators_mwords.lem')
| -rw-r--r-- | src/gen_lib/sail_operators_mwords.lem | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem index 55e6ff51..8bcc0319 100644 --- a/src/gen_lib/sail_operators_mwords.lem +++ b/src/gen_lib/sail_operators_mwords.lem @@ -73,6 +73,9 @@ let exts_vec _ w = Machine_word.signExtend w val zero_extend : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b let zero_extend w _ = Machine_word.zeroExtend w +val sign_extend : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b +let sign_extend w _ = Machine_word.signExtend w + val vector_truncate : forall 'a 'b. Size 'a, Size 'b => mword 'a -> integer -> mword 'b let vector_truncate w _ = Machine_word.zeroExtend w |