feat(semantics): add boolean semantics

correct references
This commit is contained in:
Anand Balakrishnan 2023-04-16 18:42:56 -07:00
parent e22410eea8
commit bcddb7a1a2
No known key found for this signature in database
2 changed files with 70 additions and 112 deletions

View file

@ -10,11 +10,11 @@ where
Signal<i64>: TrySignalCast<Signal<T>>, Signal<i64>: TrySignalCast<Signal<T>>,
Signal<u64>: TrySignalCast<Signal<T>>, Signal<u64>: TrySignalCast<Signal<T>>,
Signal<f64>: TrySignalCast<Signal<T>>, Signal<f64>: TrySignalCast<Signal<T>>,
Signal<T>: std::ops::Neg<Output = Signal<T>>, for<'a> &'a Signal<T>: std::ops::Neg<Output = Signal<T>>,
Signal<T>: std::ops::Add<Signal<T>, Output = Signal<T>>, for<'a> &'a Signal<T>: std::ops::Add<&'a Signal<T>, Output = Signal<T>>,
Signal<T>: std::ops::Sub<Signal<T>, Output = Signal<T>>, for<'a> &'a Signal<T>: std::ops::Sub<&'a Signal<T>, Output = Signal<T>>,
Signal<T>: std::ops::Mul<Signal<T>, Output = Signal<T>>, for<'a> &'a Signal<T>: std::ops::Mul<&'a Signal<T>, Output = Signal<T>>,
Signal<T>: std::ops::Div<Signal<T>, Output = Signal<T>>, for<'a> &'a Signal<T>: std::ops::Div<&'a Signal<T>, Output = Signal<T>>,
Signal<T>: SignalAbs, Signal<T>: SignalAbs,
{ {
match root { match root {
@ -24,32 +24,32 @@ where
NumExpr::IntVar { name } => trace.get::<i64>(name.as_str()).unwrap().try_cast(), NumExpr::IntVar { name } => trace.get::<i64>(name.as_str()).unwrap().try_cast(),
NumExpr::UIntVar { name } => trace.get::<u64>(name.as_str()).unwrap().try_cast(), NumExpr::UIntVar { name } => trace.get::<u64>(name.as_str()).unwrap().try_cast(),
NumExpr::FloatVar { name } => trace.get::<f64>(name.as_str()).unwrap().try_cast(), NumExpr::FloatVar { name } => trace.get::<f64>(name.as_str()).unwrap().try_cast(),
NumExpr::Neg { arg } => eval_num_expr(arg, trace).map(|sig| -sig), NumExpr::Neg { arg } => eval_num_expr(arg, trace).map(|sig| -&sig),
NumExpr::Add { args } => { NumExpr::Add { args } => {
let mut ret: Signal<T> = Signal::constant(0i64).try_cast()?; let mut ret: Signal<T> = Signal::<T>::zero();
for arg in args.iter() { for arg in args.iter() {
let arg = eval_num_expr(arg, trace)?; let arg = eval_num_expr(arg, trace)?;
ret = ret + arg; ret = &ret + &arg;
} }
Ok(ret) Ok(ret)
} }
NumExpr::Sub { lhs, rhs } => { NumExpr::Sub { lhs, rhs } => {
let lhs = eval_num_expr(lhs, trace)?; let lhs = eval_num_expr(lhs, trace)?;
let rhs = eval_num_expr(rhs, trace)?; let rhs = eval_num_expr(rhs, trace)?;
Ok(lhs - rhs) Ok(&lhs - &rhs)
} }
NumExpr::Mul { args } => { NumExpr::Mul { args } => {
let mut ret: Signal<T> = Signal::constant(1i64).try_cast()?; let mut ret: Signal<T> = Signal::<T>::one();
for arg in args.iter() { for arg in args.iter() {
let arg = eval_num_expr(arg, trace)?; let arg = eval_num_expr(arg, trace)?;
ret = ret * arg; ret = &ret * &arg;
} }
Ok(ret) Ok(ret)
} }
NumExpr::Div { dividend, divisor } => { NumExpr::Div { dividend, divisor } => {
let dividend = eval_num_expr(dividend, trace)?; let dividend = eval_num_expr(dividend, trace)?;
let divisor = eval_num_expr(divisor, trace)?; let divisor = eval_num_expr(divisor, trace)?;
Ok(dividend / divisor) Ok(&dividend / &divisor)
} }
NumExpr::Abs { arg } => { NumExpr::Abs { arg } => {
let arg = eval_num_expr(arg, trace)?; let arg = eval_num_expr(arg, trace)?;

View file

@ -1,131 +1,89 @@
use argus_core::expr::BoolExpr;
use argus_core::prelude::*; use argus_core::prelude::*;
use argus_core::signals::SignalPartialOrd;
use crate::eval::NumExprEval; use crate::eval::eval_num_expr;
use crate::{Semantics, Trace}; use crate::{Semantics, Trace};
macro_rules! signal_cmp_op_impl {
($lhs:ident, $rhs:ident, $op:ident, [$( $type:ident ),*]) => {
paste::paste!{
{
use argus_core::signals::traits::SignalPartialOrd;
use argus_core::prelude::*;
use AnySignal::*;
match ($lhs, $rhs) {
(Bool(_), _) | (ConstBool(_), _) | (_, Bool(_)) | (_, ConstBool(_)) => panic!("cannot perform comparison operation ({}) for boolean arguments", stringify!($op)),
$(
([<$type >](lhs), [< $type >](rhs)) => lhs.$op(&rhs).map(AnySignal::from),
([<$type >](lhs), [< Const $type >](rhs)) => lhs.$op(&rhs).map(AnySignal::from),
([<Const $type >](lhs), [< $type >](rhs)) => lhs.$op(&rhs).map(AnySignal::from),
([<Const $type >](lhs), [< Const $type >](rhs)) => lhs.$op(&rhs).map(AnySignal::from),
)*
_ => panic!("mismatched argument types for comparison operation ({})", stringify!($op)),
}
}
}
};
($lhs:ident < $rhs:ident) => {
signal_cmp_op_impl!($lhs, $rhs, signal_lt, [Int, UInt, Float])
};
($lhs:ident <= $rhs:ident) => {
signal_cmp_op_impl!($lhs, $rhs, signal_le, [Int, UInt, Float])
};
($lhs:ident > $rhs:ident) => {
signal_cmp_op_impl!($lhs, $rhs, signal_gt, [Int, UInt, Float])
};
($lhs:ident >= $rhs:ident) => {
signal_cmp_op_impl!($lhs, $rhs, signal_ge, [Int, UInt, Float])
};
($lhs:ident == $rhs:ident) => {
signal_cmp_op_impl!($lhs, $rhs, signal_eq, [Int, UInt, Float])
};
($lhs:ident != $rhs:ident) => {
signal_cmp_op_impl!($lhs, $rhs, signal_ne, [Int, UInt, Float])
};
}
macro_rules! signal_bool_op_impl {
// Unary bool opeartions
(! $signal:ident) => {{
use argus_core::prelude::*;
use AnySignal::*;
match $signal {
Bool(sig) => AnySignal::from(!(&sig)),
ConstBool(sig) => AnySignal::from(!(&sig)),
_ => panic!("cannot perform unary operation (!) on numeric signals"),
}
}};
($lhs:ident $op:tt $rhs:ident) => {
paste::paste! {
{
use argus_core::prelude::*;
use AnySignal::*;
match ($lhs, $rhs) {
(Bool(lhs), Bool(rhs)) => AnySignal::from(&lhs $op &rhs),
(Bool(lhs), ConstBool(rhs)) => AnySignal::from(&lhs $op &rhs),
(ConstBool(lhs), Bool(rhs)) => AnySignal::from(&lhs $op &rhs),
(ConstBool(lhs), ConstBool(rhs)) => AnySignal::from(&lhs $op &rhs),
_ => panic!("mismatched argument types for {} operation", stringify!($op)),
}
}
}
};
}
/// Boolean semantics of Argus expressions /// Boolean semantics of Argus expressions
pub struct BooleanSemantics; pub struct BooleanSemantics;
impl Semantics for BooleanSemantics { impl Semantics for BooleanSemantics {
// TODO: figure out how to make Output concrete Signal<bool> or ConstantSignal<bool> type Output = Signal<bool>;
type Output = AnySignal;
type Context = (); type Context = ();
fn eval(expr: &BoolExpr, trace: &impl Trace, ctx: Self::Context) -> ArgusResult<Self::Output> { fn eval(expr: &BoolExpr, trace: &impl Trace, ctx: Self::Context) -> ArgusResult<Self::Output> {
match expr { match expr {
BoolExpr::BoolLit(val) => Ok(ConstantSignal::new(*val).into()), BoolExpr::BoolLit(val) => Ok(Signal::constant(*val)),
BoolExpr::BoolVar { name } => trace.get(name.as_str()).cloned().ok_or(ArgusError::SignalNotPresent), BoolExpr::BoolVar { name } => trace.get(name.as_str()).cloned().ok_or(ArgusError::SignalNotPresent),
BoolExpr::Cmp { op, lhs, rhs } => { BoolExpr::Cmp { op, lhs, rhs } => {
use argus_core::expr::Ordering::*; use argus_core::expr::Ordering::*;
let lhs = NumExprEval::eval(lhs, trace); let lhs = eval_num_expr::<f64>(lhs, trace)?;
let rhs = NumExprEval::eval(rhs, trace); let rhs = eval_num_expr::<f64>(rhs, trace)?;
let ret = match op { let ret = match op {
Eq => signal_cmp_op_impl!(lhs == rhs), Eq => lhs.signal_eq(&rhs),
NotEq => signal_cmp_op_impl!(lhs != rhs), NotEq => lhs.signal_ne(&rhs),
Less { strict } if *strict => signal_cmp_op_impl!(lhs < rhs), Less { strict } if *strict => lhs.signal_lt(&rhs),
Less { strict: _ } => signal_cmp_op_impl!(lhs <= rhs), Less { strict: _ } => lhs.signal_le(&rhs),
Greater { strict } if *strict => signal_cmp_op_impl!(lhs > rhs), Greater { strict } if *strict => lhs.signal_gt(&rhs),
Greater { strict: _ } => signal_cmp_op_impl!(lhs >= rhs), Greater { strict: _ } => lhs.signal_ge(&rhs),
}; };
ret.ok_or(ArgusError::InvalidOperation) ret.ok_or(ArgusError::InvalidOperation)
} }
BoolExpr::Not { arg } => { BoolExpr::Not { arg } => {
let arg = Self::eval(arg, trace, ctx)?; let arg = Self::eval(arg, trace, ctx)?;
Ok(signal_bool_op_impl!(!arg)) Ok(!&arg)
} }
BoolExpr::And { args } => { BoolExpr::And { args } => {
let args: ArgusResult<Vec<_>> = args.iter().map(|arg| Self::eval(arg, trace, ctx)).collect(); let mut ret = Signal::constant(true);
let ret = args? for arg in args.iter() {
.into_iter() let arg = Self::eval(arg, trace, ctx)?;
.fold(AnySignal::from(ConstantSignal::new(true)), |lhs, rhs| { ret = &ret & &arg;
signal_bool_op_impl!(lhs & rhs) }
});
Ok(ret) Ok(ret)
} }
BoolExpr::Or { args } => { BoolExpr::Or { args } => {
let args: ArgusResult<Vec<_>> = args.iter().map(|arg| Self::eval(arg, trace, ctx)).collect(); let mut ret = Signal::constant(false);
let ret = args? for arg in args.iter() {
.into_iter() let arg = Self::eval(arg, trace, ctx)?;
.fold(AnySignal::from(ConstantSignal::new(true)), |lhs, rhs| { ret = &ret | &arg;
signal_bool_op_impl!(lhs | rhs) }
});
Ok(ret) Ok(ret)
} }
BoolExpr::Next { arg: _ } => todo!(),
BoolExpr::Always { arg } => {
let mut arg = Self::eval(arg, trace, ctx)?;
match &mut arg {
// if signal is empty or constant, return the signal itself.
// This works because if a signal is True everythere, then it must
// "always be true".
Signal::Empty | Signal::Constant { value: _ } => (),
Signal::Sampled { values, time_points } => {
// Compute the & in a expanding window fashion from the back
for i in (0..(time_points.len() - 1)).rev() {
values[i] &= values[i + 1];
}
}
}
Ok(arg)
}
BoolExpr::Eventually { arg } => {
let mut arg = Self::eval(arg, trace, ctx)?;
match &mut arg {
// if signal is empty or constant, return the signal itself.
// This works because if a signal is True everywhere, then it must
// "eventually be true", and if it is False everywhere, then it will
// "never be true".
Signal::Empty | Signal::Constant { value: _ } => (),
Signal::Sampled { values, time_points } => {
// Compute the | in a expanding window fashion from the back
for i in (0..(time_points.len() - 1)).rev() {
values[i] |= values[i + 1];
}
}
}
Ok(arg)
}
BoolExpr::Until { lhs, rhs } => todo!(),
} }
} }
} }