From 8e58d17e8d23592ed4d0ac4bcde98668b1bcec2b Mon Sep 17 00:00:00 2001 From: Evan Johnson Date: Thu, 7 Dec 2023 15:13:04 -0800 Subject: [PATCH] add support for lnot on ints and uints --- crates/flux-refineck/src/sigs/default.rs | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/crates/flux-refineck/src/sigs/default.rs b/crates/flux-refineck/src/sigs/default.rs index aaac77c63f..ffa18995b1 100644 --- a/crates/flux-refineck/src/sigs/default.rs +++ b/crates/flux-refineck/src/sigs/default.rs @@ -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::{ @@ -30,6 +30,7 @@ pub(super) static UN_OPS: LazyLock> = LazyLock::new(|| { table.extend(mk_neg()); table.extend([mk_not()]); + table.extend(mk_lnot()); table }); @@ -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)> { + 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) +}