Skip to content

Commit

Permalink
add support for lnot on ints and uints
Browse files Browse the repository at this point in the history
  • Loading branch information
enjhnsn2 committed Dec 7, 2023
1 parent 2aecd0d commit 8e58d17
Showing 1 changed file with 16 additions and 1 deletion.
17 changes: 16 additions & 1 deletion crates/flux-refineck/src/sigs/default.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ use flux_middle::{
rty::{BaseTy, BinOp, Expr, INT_TYS, UINT_TYS},
rustc::mir,
};
use itertools::iproduct;
use itertools::{chain, iproduct};

use super::{Sig, SigTable};
use crate::{
Expand All @@ -30,6 +30,7 @@ pub(super) static UN_OPS: LazyLock<SigTable<mir::UnOp, 1>> = LazyLock::new(|| {

table.extend(mk_neg());
table.extend([mk_not()]);
table.extend(mk_lnot());

table
});
Expand Down Expand Up @@ -166,3 +167,17 @@ pub(crate) fn mk_not() -> (mir::UnOp, Sig<1>) {
define_btys! { let bool = BaseTy::Bool; }
(mir::UnOp::Not, s!(fn(a: bool) -> bool[a.not()]))
}

pub(crate) fn mk_lnot() -> impl IntoIterator<Item = (mir::UnOp, Sig<1>)> {
let int_lnots = INT_TYS.map(|int_ty| {
define_btys! { let Int = BaseTy::Int(int_ty); };
(mir::UnOp::Not, s!(fn(a: Int) -> Int[E::tt()]))
});

let uint_lnots = UINT_TYS.map(|uint_ty| {
define_btys! { let Uint = BaseTy::Uint(uint_ty); };
(mir::UnOp::Not, s!(fn(a: Uint) -> Uint[E::tt()]))
});

chain!(int_lnots, uint_lnots)
}

0 comments on commit 8e58d17

Please sign in to comment.