feat!(core): Use new AST structure

Derive Expr methods using a derive proc-macro. These macros are present in
the `argus-derive` crate, but the traits are defined in `argus-core`

argus-core/src/expr/bool_expr.rs

@@ -0,0 +1,294 @@
+//! Boolean expression types
+
+use std::ops::{Bound, RangeBounds};
+use std::time::Duration;
+
+use super::{BoolExpr, Expr, NumExpr};
+
+/// Types of comparison operations
+#[derive(Clone, Copy, Debug, PartialEq)]
+pub enum Ordering {
+    /// Equality check for two expressions
+    Eq,
+    /// Non-equality check for two expressions
+    NotEq,
+    /// Less than check
+    Less {
+        /// Denotes `lhs < rhs` if `strict`, and `lhs <= rhs` otherwise.
+        strict: bool,
+    },
+    /// Greater than check
+    Greater {
+        /// Denotes `lhs > rhs` if `strict`, and `lhs >= rhs` otherwise.
+        strict: bool,
+    },
+}
+
+impl Ordering {
+    /// Check if `Ordering::Eq`
+    pub fn equal() -> Self {
+        Self::Eq
+    }
+
+    /// Check if `Ordering::NotEq`
+    pub fn not_equal() -> Self {
+        Self::NotEq
+    }
+
+    /// Check if `Ordering::Less { strict: true }`
+    pub fn less_than() -> Self {
+        Self::Less { strict: true }
+    }
+
+    /// Check if `Ordering::Less { strict: false }`
+    pub fn less_than_eq() -> Self {
+        Self::Less { strict: false }
+    }
+
+    /// Check if `Ordering::Greater { strict: true }`
+    pub fn greater_than() -> Self {
+        Self::Greater { strict: true }
+    }
+
+    /// Check if `Ordering::Less { strict: false }`
+    pub fn greater_than_eq() -> Self {
+        Self::Greater { strict: false }
+    }
+}
+
+/// A time interval for a temporal expression.
+#[derive(Copy, Clone, Debug, PartialEq, Eq, derive_more::Into)]
+#[into(owned, ref, ref_mut)]
+pub struct Interval {
+    /// Start of the interval
+    pub start: Bound<Duration>,
+    /// End of the interval
+    pub end: Bound<Duration>,
+}
+
+impl Interval {
+    /// Create a new interval
+    ///
+    /// # Note
+    ///
+    /// Argus doesn't permit `Interval`s with [`Bound::Excluded(_)`] values (as these
+    /// can't be monitored reliably) and thus converts all such bounds to an
+    /// [`Bound::Included(_)`]. Moreover, if the `start` bound is [`Bound::Unbounded`],
+    /// it will get transformed to [`Bound::Included(Duration::ZERO)`].
+    pub fn new(start: Bound<Duration>, end: Bound<Duration>) -> Self {
+        use Bound::*;
+        let start = match start {
+            a @ Included(_) => a,
+            Excluded(b) => Included(b),
+            Unbounded => Included(Duration::ZERO),
+        };
+
+        let end = match end {
+            Excluded(b) => Included(b),
+            bound => bound,
+        };
+
+        Self { start, end }
+    }
+
+    /// Check if the interval is empty
+    #[inline]
+    pub fn is_empty(&self) -> bool {
+        use Bound::*;
+        match (&self.start, &self.end) {
+            (Included(a), Included(b)) => a > b,
+            (Included(a), Excluded(b)) | (Excluded(a), Included(b)) | (Excluded(a), Excluded(b)) => a >= b,
+            (Unbounded, Excluded(b)) => b == &Duration::ZERO,
+            _ => false,
+        }
+    }
+
+    /// Check if the interval is a singleton
+    ///
+    /// This implies that only 1 timepoint is valid within this interval.
+    #[inline]
+    pub fn is_singleton(&self) -> bool {
+        use Bound::*;
+        match (&self.start, &self.end) {
+            (Included(a), Included(b)) => a == b,
+            (Unbounded, Included(b)) => b == &Duration::ZERO,
+            _ => false,
+        }
+    }
+
+    /// Check if the interval covers `[0, ..)`.
+    #[inline]
+    pub fn is_untimed(&self) -> bool {
+        use Bound::*;
+        match (self.start, self.end) {
+            (Unbounded, Unbounded) | (Included(Duration::ZERO), Unbounded) => true,
+            (Included(_), Included(_)) | (Included(_), Unbounded) => false,
+            (Excluded(_), _) | (_, Excluded(_)) | (Unbounded, _) => {
+                unreachable!("looks like someone didn't use Interval::new")
+            }
+        }
+    }
+}
+
+impl<T> From<T> for Interval
+where
+    T: RangeBounds<Duration>,
+{
+    fn from(value: T) -> Self {
+        Self::new(value.start_bound().cloned(), value.end_bound().cloned())
+    }
+}
+
+// TODO(anand): Can I implement this within argus_derive?
+macro_rules! impl_bool_expr {
+    ($ty:ty$(, $($arg:ident),* )? ) => {
+        impl Expr for $ty {
+            fn is_numeric(&self) -> bool {
+                false
+            }
+
+            fn is_boolean(&self) -> bool {
+                true
+            }
+
+            fn args(&self) -> Vec<super::ExprRef<'_>> {
+                vec![$($( self.$arg.as_ref().into(), )* )*]
+            }
+        }
+    };
+    ($ty:ty, [$args:ident]) => {
+        impl Expr for $ty {
+            fn is_numeric(&self) -> bool {
+                false
+            }
+
+            fn is_boolean(&self) -> bool {
+                true
+            }
+
+            fn args(&self) -> Vec<super::ExprRef<'_>> {
+                self.$args.iter().map(|arg| arg.into()).collect()
+            }
+        }
+    };
+}
+
+/// A `bool` literal
+#[derive(Clone, Debug, PartialEq, argus_derive::BoolExpr)]
+pub struct BoolLit(pub bool);
+
+impl_bool_expr!(BoolLit);
+
+/// A `bool` variable
+#[derive(Clone, Debug, PartialEq, argus_derive::BoolExpr)]
+pub struct BoolVar {
+    /// Variable name
+    pub name: String,
+}
+
+impl_bool_expr!(BoolVar);
+
+/// A comparison expression
+#[derive(Clone, Debug, PartialEq, argus_derive::BoolExpr)]
+pub struct Cmp {
+    /// The type of comparison
+    pub op: Ordering,
+    /// The LHS for the comparison
+    pub lhs: Box<NumExpr>,
+    /// The RHS for the comparison
+    pub rhs: Box<NumExpr>,
+}
+
+impl_bool_expr!(Cmp, lhs, rhs);
+
+/// Logical negation of an expression
+#[derive(Clone, Debug, PartialEq, argus_derive::BoolExpr)]
+pub struct Not {
+    /// Expression to be negated
+    pub arg: Box<BoolExpr>,
+}
+
+impl_bool_expr!(Not, arg);
+
+/// Logical conjunction of a list of expressions
+#[derive(Clone, Debug, PartialEq, argus_derive::BoolExpr)]
+pub struct And {
+    /// Expressions to be "and"-ed
+    pub args: Vec<BoolExpr>,
+}
+
+impl_bool_expr!(And, [args]);
+
+/// Logical disjunction of a list of expressions
+#[derive(Clone, Debug, PartialEq, argus_derive::BoolExpr)]
+pub struct Or {
+    /// Expressions to be "or"-ed
+    pub args: Vec<BoolExpr>,
+}
+
+impl_bool_expr!(Or, [args]);
+
+/// A temporal next expression
+///
+/// Checks if the next time point in a signal is `true` or not.
+#[derive(Clone, Debug, PartialEq, argus_derive::BoolExpr)]
+pub struct Next {
+    /// Argument for `Next`
+    pub arg: Box<BoolExpr>,
+}
+impl_bool_expr!(Next, arg);
+
+/// Temporal "oracle" expression
+///
+/// This is equivalent to `steps` number of nested [`Next`](BoolExpr::Next)
+/// expressions.
+#[derive(Clone, Debug, PartialEq, argus_derive::BoolExpr)]
+pub struct Oracle {
+    /// Number of steps to look ahead
+    pub steps: usize,
+    /// Argument for `Oracle`
+    pub arg: Box<BoolExpr>,
+}
+impl_bool_expr!(Oracle, arg);
+
+/// A temporal always expression
+///
+/// - If the `interval` is `(Unbounded, Unbounded)` or equivalent to `(0, Unbounded)`:
+///   checks if the signal is `true` for all points in a signal.
+/// - Otherwise: checks if the signal is `true` for all points within the `interval`.
+#[derive(Clone, Debug, PartialEq, argus_derive::BoolExpr)]
+pub struct Always {
+    /// Argument for `Always`
+    pub arg: Box<BoolExpr>,
+    /// Interval for the expression
+    pub interval: Interval,
+}
+impl_bool_expr!(Always, arg);
+
+/// A temporal eventually expression
+///
+/// - If the `interval` is `(Unbounded, Unbounded)` or equivalent to `(0, Unbounded)`:
+///   checks if the signal is `true` for some point in a signal.
+/// - Otherwise: checks if the signal is `true` for some point within the `interval`.
+#[derive(Clone, Debug, PartialEq, argus_derive::BoolExpr)]
+pub struct Eventually {
+    /// Argument for `Eventually`
+    pub arg: Box<BoolExpr>,
+    /// Interval for the expression
+    pub interval: Interval,
+}
+impl_bool_expr!(Eventually, arg);
+
+/// A temporal until expression
+///
+/// Checks if the `lhs` is always `true` for a signal until `rhs` becomes `true`.
+#[derive(Clone, Debug, PartialEq, argus_derive::BoolExpr)]
+pub struct Until {
+    /// LHS to `lhs Until rhs`
+    pub lhs: Box<BoolExpr>,
+    /// RHS to `lhs Until rhs`
+    pub rhs: Box<BoolExpr>,
+    /// Interval for the expression
+    pub interval: Interval,
+}
+impl_bool_expr!(Until, lhs, rhs);

argus-core/src/expr/bool_ops.rs

@@ -1,71 +0,0 @@
-use std::ops::{BitAnd, BitOr, Not};
-
-use super::{internal_macros, BoolExpr};
-
-impl Not for BoolExpr {
-    type Output = BoolExpr;
-
-    fn not(self) -> Self::Output {
-        BoolExpr::Not { arg: Box::new(self) }
-    }
-}
-
-impl Not for Box<BoolExpr> {
-    type Output = BoolExpr;
-
-    fn not(self) -> Self::Output {
-        BoolExpr::Not { arg: self }
-    }
-}
-
-impl BitOr for BoolExpr {
-    type Output = BoolExpr;
-
-    #[inline]
-    fn bitor(self, rhs: Self) -> Self::Output {
-        use BoolExpr::*;
-
-        match (self, rhs) {
-            (Or { args: mut left }, Or { args: mut right }) => {
-                left.append(&mut right);
-                Or { args: left }
-            }
-            (Or { mut args }, other) | (other, Or { mut args }) => {
-                args.push(other);
-                Or { args }
-            }
-            (left, right) => {
-                let args = vec![left, right];
-                Or { args }
-            }
-        }
-    }
-}
-
-internal_macros::forward_box_binop! {impl BitOr, bitor for BoolExpr, BoolExpr }
-
-impl BitAnd for BoolExpr {
-    type Output = BoolExpr;
-
-    #[inline]
-    fn bitand(self, rhs: Self) -> Self::Output {
-        use BoolExpr::*;
-
-        match (self, rhs) {
-            (And { args: mut left }, And { args: mut right }) => {
-                left.append(&mut right);
-                And { args: left }
-            }
-            (And { mut args }, other) | (other, And { mut args }) => {
-                args.push(other);
-                And { args }
-            }
-            (left, right) => {
-                let args = vec![left, right];
-                And { args }
-            }
-        }
-    }
-}
-
-internal_macros::forward_box_binop! {impl BitAnd, bitand for BoolExpr, BoolExpr }

argus-core/src/expr/internal_macros.rs

@@ -1,32 +0,0 @@
-macro_rules! forward_box_binop {
-    (impl $imp:ident, $method:ident for $t:ty, $u:ty) => {
-        impl $imp<$u> for Box<$t> {
-            type Output = <$t as $imp<$u>>::Output;
-
-            #[inline]
-            fn $method(self, other: $u) -> <$t as $imp<$u>>::Output {
-                $imp::$method(*self, other)
-            }
-        }
-
-        impl $imp<Box<$u>> for $t {
-            type Output = <$t as $imp<$u>>::Output;
-
-            #[inline]
-            fn $method(self, other: Box<$u>) -> <$t as $imp<$u>>::Output {
-                $imp::$method(self, *other)
-            }
-        }
-
-        impl $imp<Box<$u>> for Box<$t> {
-            type Output = <$t as $imp<$u>>::Output;
-
-            #[inline]
-            fn $method(self, other: Box<$u>) -> <$t as $imp<$u>>::Output {
-                $imp::$method(*self, *other)
-            }
-        }
-    };
-}
-
-pub(crate) use forward_box_binop;

argus-core/src/expr/iter.rs

@@ -47,7 +47,7 @@ impl<'a> Iterator for AstIter<'a> {
 mod tests {
     use itertools::Itertools;
 
-    use crate::expr::{Expr, ExprBuilder, ExprRef};
+    use crate::expr::{ExprBuilder, ExprRef};
 
     #[test]
     fn simple_iter() {

argus-core/src/expr/num_expr.rs

@@ -0,0 +1,128 @@
+//! Numeric expression types
+
+use super::{Expr, NumExpr};
+
+// TODO(anand): Can I implement this within argus_derive?
+macro_rules! impl_num_expr {
+    ($ty:ty$(, $($arg:ident),* )? ) => {
+        impl Expr for $ty {
+            fn is_numeric(&self) -> bool {
+                true
+            }
+
+            fn is_boolean(&self) -> bool {
+                false
+            }
+
+            fn args(&self) -> Vec<super::ExprRef<'_>> {
+                vec![$($( self.$arg.as_ref().into(), )* )*]
+            }
+        }
+    };
+    ($ty:ty, [$args:ident]) => {
+        impl Expr for $ty {
+            fn is_numeric(&self) -> bool {
+                false
+            }
+
+            fn is_boolean(&self) -> bool {
+                true
+            }
+
+            fn args(&self) -> Vec<super::ExprRef<'_>> {
+                self.$args.iter().map(|arg| arg.into()).collect()
+            }
+        }
+    };
+}
+
+/// A signed integer literal
+#[derive(Clone, Debug, PartialEq, argus_derive::NumExpr)]
+pub struct IntLit(pub i64);
+impl_num_expr!(IntLit);
+
+/// An unsigned integer literal
+#[derive(Clone, Debug, PartialEq, argus_derive::NumExpr)]
+pub struct UIntLit(pub u64);
+impl_num_expr!(UIntLit);
+
+/// A floating point literal
+#[derive(Clone, Debug, PartialEq, argus_derive::NumExpr)]
+pub struct FloatLit(pub f64);
+impl_num_expr!(FloatLit);
+
+/// A signed integer variable
+#[derive(Clone, Debug, PartialEq, argus_derive::NumExpr)]
+pub struct IntVar {
+    /// Name of the variable
+    pub name: String,
+}
+impl_num_expr!(IntVar);
+
+/// A unsigned integer variable
+#[derive(Clone, Debug, PartialEq, argus_derive::NumExpr)]
+pub struct UIntVar {
+    /// Name of the variable
+    pub name: String,
+}
+impl_num_expr!(UIntVar);
+
+/// A floating point number variable
+#[derive(Clone, Debug, PartialEq, argus_derive::NumExpr)]
+pub struct FloatVar {
+    /// Name of the variable
+    pub name: String,
+}
+impl_num_expr!(FloatVar);
+
+/// Numeric negation of a numeric expression
+#[derive(Clone, Debug, PartialEq, argus_derive::NumExpr)]
+pub struct Neg {
+    /// Numeric expression being negated
+    pub arg: Box<NumExpr>,
+}
+impl_num_expr!(Neg, arg);
+
+/// Arithmetic addition of a list of numeric expressions
+#[derive(Clone, Debug, PartialEq, argus_derive::NumExpr)]
+pub struct Add {
+    /// List of expressions being added
+    pub args: Vec<NumExpr>,
+}
+impl_num_expr!(Add, [args]);
+
+/// Subtraction of two numbers
+#[derive(Clone, Debug, PartialEq, argus_derive::NumExpr)]
+pub struct Sub {
+    /// LHS to the expression `lhs - rhs`
+    pub lhs: Box<NumExpr>,
+    /// RHS to the expression `lhs - rhs`
+    pub rhs: Box<NumExpr>,
+}
+impl_num_expr!(Sub, lhs, rhs);
+
+/// Arithmetic multiplication of a list of numeric expressions
+#[derive(Clone, Debug, PartialEq, argus_derive::NumExpr)]
+pub struct Mul {
+    /// List of expressions being multiplied
+    pub args: Vec<NumExpr>,
+}
+impl_num_expr!(Mul, [args]);
+
+/// Divide two expressions `dividend / divisor`
+#[derive(Clone, Debug, PartialEq, argus_derive::NumExpr)]
+pub struct Div {
+    /// The dividend
+    pub dividend: Box<NumExpr>,
+    /// The divisor
+    pub divisor: Box<NumExpr>,
+}
+impl_num_expr!(Div, dividend, divisor);
+
+/// The absolute value of an expression
+#[derive(Clone, Debug, PartialEq, argus_derive::NumExpr)]
+pub struct Abs {
+    /// Argument to `abs`
+    pub arg: Box<NumExpr>,
+}
+impl_num_expr!(Abs, arg);

argus-core/src/expr/num_ops.rs

@@ -1,146 +0,0 @@
-use std::ops::{Add, Div, Mul, Neg};
-
-use super::{internal_macros, BoolExpr, NumExpr};
-
-impl Neg for NumExpr {
-    type Output = NumExpr;
-
-    #[inline]
-    fn neg(self) -> Self::Output {
-        NumExpr::Neg { arg: Box::new(self) }
-    }
-}
-
-impl Neg for Box<NumExpr> {
-    type Output = NumExpr;
-
-    #[inline]
-    fn neg(self) -> Self::Output {
-        NumExpr::Neg { arg: self }
-    }
-}
-
-impl Add for NumExpr {
-    type Output = NumExpr;
-
-    #[inline]
-    fn add(self, rhs: Self) -> Self::Output {
-        use NumExpr::*;
-
-        match (self, rhs) {
-            (Add { args: mut left }, Add { args: mut right }) => {
-                left.append(&mut right);
-                Add { args: left }
-            }
-            (Add { mut args }, other) | (other, Add { mut args }) => {
-                args.push(other);
-                Add { args }
-            }
-            (left, right) => {
-                let args = vec![left, right];
-                Add { args }
-            }
-        }
-    }
-}
-
-internal_macros::forward_box_binop! {impl Add, add for NumExpr, NumExpr }
-
-impl Mul for NumExpr {
-    type Output = NumExpr;
-
-    #[inline]
-    fn mul(self, rhs: Self) -> Self::Output {
-        use NumExpr::*;
-
-        match (self, rhs) {
-            (Mul { args: mut left }, Mul { args: mut right }) => {
-                left.append(&mut right);
-                Mul { args: left }
-            }
-            (Mul { mut args }, other) | (other, Mul { mut args }) => {
-                args.push(other);
-                Mul { args }
-            }
-            (left, right) => {
-                let args = vec![left, right];
-                Mul { args }
-            }
-        }
-    }
-}
-
-internal_macros::forward_box_binop! {impl Mul, mul for NumExpr, NumExpr }
-
-impl Div for NumExpr {
-    type Output = NumExpr;
-
-    #[inline]
-    fn div(self, rhs: Self) -> Self::Output {
-        use NumExpr::*;
-        Div {
-            dividend: Box::new(self),
-            divisor: Box::new(rhs),
-        }
-    }
-}
-
-internal_macros::forward_box_binop! {impl Div, div for NumExpr, NumExpr }
-
-use super::Ordering;
-
-impl NumExpr {
-    /// Convenience method to create an `lhs < rhs` expression.
-    pub fn less_than(self, rhs: Self) -> BoolExpr {
-        BoolExpr::Cmp {
-            op: Ordering::Less { strict: true },
-            lhs: Box::new(self),
-            rhs: Box::new(rhs),
-        }
-    }
-
-    /// Convenience method to create an `lhs <= rhs` expression.
-    pub fn less_than_eq(self, rhs: Self) -> BoolExpr {
-        BoolExpr::Cmp {
-            op: Ordering::Less { strict: false },
-            lhs: Box::new(self),
-            rhs: Box::new(rhs),
-        }
-    }
-
-    /// Convenience method to create an `lhs > rhs` expression.
-    pub fn greater_than(self, rhs: Self) -> BoolExpr {
-        BoolExpr::Cmp {
-            op: Ordering::Greater { strict: true },
-            lhs: Box::new(self),
-            rhs: Box::new(rhs),
-        }
-    }
-
-    /// Convenience method to create an `lhs >= rhs` expression.
-    pub fn greater_than_eq(self, rhs: Self) -> BoolExpr {
-        BoolExpr::Cmp {
-            op: Ordering::Greater { strict: false },
-            lhs: Box::new(self),
-            rhs: Box::new(rhs),
-        }
-    }
-
-    /// Convenience method to create an `lhs == rhs` expression.
-    pub fn equal(self, rhs: Self) -> BoolExpr {
-        BoolExpr::Cmp {
-            op: Ordering::Eq,
-            lhs: Box::new(self),
-            rhs: Box::new(rhs),
-        }
-    }
-
-    /// Convenience method to create an `lhs != rhs` expression.
-    pub fn not_equal(self, rhs: Self) -> BoolExpr {
-        BoolExpr::Cmp {
-            op: Ordering::NotEq,
-            lhs: Box::new(self),
-            rhs: Box::new(rhs),
-        }
-    }
-}

argus-core/src/expr/traits.rs

@@ -1,9 +1,9 @@
-use std::any::Any;
+use enum_dispatch::enum_dispatch;
 
-use super::iter::AstIter;
-use super::ExprRef;
+use super::{BoolExpr, ExprRef, NumExpr};
 
 /// A trait representing expressions
+#[enum_dispatch]
 pub trait Expr {
     /// Check if the given expression is a numeric expression
     fn is_numeric(&self) -> bool;
@@ -14,48 +14,10 @@ pub trait Expr {
     /// If the expression doesn't contain arguments (i.e., it is a leaf expression) then
     /// the vector is empty.
     fn args(&self) -> Vec<ExprRef<'_>>;
-    /// Helper function for upcasting to [`std::any::Any`] and then downcasting to a
-    /// concrete [`BoolExpr`](crate::expr::BoolExpr) or
-    /// [`NumExpr`](crate::expr::NumExpr).
-    fn as_any(&self) -> &dyn Any;
-    /// An iterator over the AST starting from the current expression.
-    fn iter(&self) -> AstIter<'_>;
 }
 
-impl dyn Expr {
-    /// Convenience method to downcast an expression to a concrete expression node.
-    pub fn downcast_expr_ref<T>(&self) -> Option<&T>
-    where
-        T: Any,
-    {
-        self.as_any().downcast_ref::<T>()
-    }
-}
+/// Marker trait for numeric expressions
+pub trait IsNumExpr: Expr + Into<NumExpr> {}
 
-#[cfg(test)]
-mod tests {
-    use proptest::prelude::*;
-
-    use super::super::{arbitrary, BoolExpr, NumExpr};
-    use super::*;
-
-    proptest! {
-        #[test]
-        fn downcast_expr_bool(bool_expr in arbitrary::bool_expr()) {
-            let expr_ref = bool_expr.as_ref() as &dyn Expr;
-
-            let downcast_ref = expr_ref.downcast_expr_ref::<BoolExpr>().unwrap();
-            assert_eq!(downcast_ref, bool_expr.as_ref());
-        }
-    }
-
-    proptest! {
-        #[test]
-        fn downcast_expr_num(num_expr in arbitrary::num_expr()) {
-            let expr_ref = num_expr.as_ref() as &dyn Expr;
-
-            let downcast_ref = expr_ref.downcast_expr_ref::<NumExpr>().unwrap();
-            assert_eq!(downcast_ref, num_expr.as_ref());
-        }
-    }
-}
+/// Marker trait for Boolean expressions
+pub trait IsBoolExpr: Expr + Into<BoolExpr> {}