feat!(argus-parser): complete parser

This changes the API for `ExprBuilder`, but that is OK.

argus-core/src/expr.rs

@@ -119,7 +119,7 @@ pub enum ExprRef<'a> {
 }
 
 /// An expression (either [`BoolExpr`] or [`NumExpr`])
-#[derive(Clone, Debug, derive_more::From)]
+#[derive(Clone, Debug, derive_more::From, derive_more::TryInto)]
 pub enum Expr {
     /// A reference to a [`BoolExpr`]
     Bool(BoolExpr),
@@ -146,220 +146,284 @@ impl ExprBuilder {
     }
 
     /// Declare a constant boolean expression
-    pub fn bool_const(&self, value: bool) -> Box<BoolExpr> {
+    pub fn bool_const(&self, value: bool) -> BoolExpr {
-        Box::new(BoolLit(value).into())
+        BoolLit(value).into()
     }
 
     /// Declare a constant integer expression
-    pub fn int_const(&self, value: i64) -> Box<NumExpr> {
+    pub fn int_const(&self, value: i64) -> NumExpr {
-        Box::new(IntLit(value).into())
+        IntLit(value).into()
     }
 
     /// Declare a constant unsigned integer expression
-    pub fn uint_const(&self, value: u64) -> Box<NumExpr> {
+    pub fn uint_const(&self, value: u64) -> NumExpr {
-        Box::new(UIntLit(value).into())
+        UIntLit(value).into()
     }
 
     /// Declare a constant floating point expression
-    pub fn float_const(&self, value: f64) -> Box<NumExpr> {
+    pub fn float_const(&self, value: f64) -> NumExpr {
-        Box::new(FloatLit(value).into())
+        FloatLit(value).into()
     }
 
     /// Declare a boolean variable
-    pub fn bool_var(&mut self, name: String) -> ArgusResult<Box<BoolExpr>> {
+    pub fn bool_var(&mut self, name: String) -> ArgusResult<BoolExpr> {
         if self.declarations.insert(name.clone()) {
-            Ok(Box::new((BoolVar { name }).into()))
+            Ok((BoolVar { name }).into())
         } else {
             Err(Error::IdentifierRedeclaration)
         }
     }
 
     /// Declare a integer variable
-    pub fn int_var(&mut self, name: String) -> ArgusResult<Box<NumExpr>> {
+    pub fn int_var(&mut self, name: String) -> ArgusResult<NumExpr> {
         if self.declarations.insert(name.clone()) {
-            Ok(Box::new((IntVar { name }).into()))
+            Ok((IntVar { name }).into())
         } else {
             Err(Error::IdentifierRedeclaration)
         }
     }
 
     /// Declare a unsigned integer variable
-    pub fn uint_var(&mut self, name: String) -> ArgusResult<Box<NumExpr>> {
+    pub fn uint_var(&mut self, name: String) -> ArgusResult<NumExpr> {
         if self.declarations.insert(name.clone()) {
-            Ok(Box::new((UIntVar { name }).into()))
+            Ok((UIntVar { name }).into())
         } else {
             Err(Error::IdentifierRedeclaration)
         }
     }
 
     /// Declare a floating point variable
-    pub fn float_var(&mut self, name: String) -> ArgusResult<Box<NumExpr>> {
+    pub fn float_var(&mut self, name: String) -> ArgusResult<NumExpr> {
         if self.declarations.insert(name.clone()) {
-            Ok(Box::new((FloatVar { name }).into()))
+            Ok((FloatVar { name }).into())
         } else {
             Err(Error::IdentifierRedeclaration)
         }
     }
 
     /// Create a [`NumExpr::Neg`] expression
-    pub fn make_neg(&self, arg: Box<NumExpr>) -> Box<NumExpr> {
+    pub fn make_neg(&self, arg: Box<NumExpr>) -> NumExpr {
-        Box::new((Neg { arg }).into())
+        (Neg { arg }).into()
     }
 
     /// Create a [`NumExpr::Add`] expression
-    pub fn make_add<I>(&self, args: I) -> ArgusResult<Box<NumExpr>>
+    pub fn make_add<I>(&self, args: I) -> ArgusResult<NumExpr>
     where
         I: IntoIterator<Item = NumExpr>,
     {
-        let args: Vec<_> = args.into_iter().collect();
+        let mut new_args = Vec::<NumExpr>::new();
-        if args.len() < 2 {
+        for arg in args.into_iter() {
+            // Flatten the args if there is an Add
+            if let NumExpr::Add(Add { args }) = arg {
+                new_args.extend(args.into_iter());
+            } else {
+                new_args.push(arg);
+            }
+        }
+        if new_args.len() < 2 {
             Err(Error::IncompleteArgs)
         } else {
-            Ok(Box::new((Add { args }).into()))
+            Ok((Add { args: new_args }).into())
         }
     }
 
     /// Create a [`NumExpr::Mul`] expression
-    pub fn make_mul<I>(&self, args: I) -> ArgusResult<Box<NumExpr>>
+    pub fn make_mul<I>(&self, args: I) -> ArgusResult<NumExpr>
     where
         I: IntoIterator<Item = NumExpr>,
     {
-        let args: Vec<_> = args.into_iter().collect();
+        let mut new_args = Vec::<NumExpr>::new();
-        if args.len() < 2 {
+        for arg in args.into_iter() {
+            // Flatten the args if there is a Mul
+            if let NumExpr::Mul(Mul { args }) = arg {
+                new_args.extend(args.into_iter());
+            } else {
+                new_args.push(arg);
+            }
+        }
+        if new_args.len() < 2 {
             Err(Error::IncompleteArgs)
         } else {
-            Ok(Box::new((Mul { args }).into()))
+            Ok((Mul { args: new_args }).into())
         }
     }
 
+    /// Create a [`NumExpr::Sub`] expression
+    pub fn make_sub(&self, lhs: Box<NumExpr>, rhs: Box<NumExpr>) -> NumExpr {
+        (Sub { lhs, rhs }).into()
+    }
+
     /// Create a [`NumExpr::Div`] expression
-    pub fn make_div(&self, dividend: Box<NumExpr>, divisor: Box<NumExpr>) -> Box<NumExpr> {
+    pub fn make_div(&self, dividend: Box<NumExpr>, divisor: Box<NumExpr>) -> NumExpr {
-        Box::new((Div { dividend, divisor }).into())
+        (Div { dividend, divisor }).into()
     }
 
     /// Create a [`BoolExpr::Cmp`] expression
-    pub fn make_cmp(&self, op: Ordering, lhs: Box<NumExpr>, rhs: Box<NumExpr>) -> Box<BoolExpr> {
+    pub fn make_cmp(&self, op: Ordering, lhs: Box<NumExpr>, rhs: Box<NumExpr>) -> BoolExpr {
-        Box::new((Cmp { op, lhs, rhs }).into())
+        (Cmp { op, lhs, rhs }).into()
     }
 
     /// Create a "less than" ([`BoolExpr::Cmp`]) expression
-    pub fn make_lt(&self, lhs: Box<NumExpr>, rhs: Box<NumExpr>) -> Box<BoolExpr> {
+    pub fn make_lt(&self, lhs: Box<NumExpr>, rhs: Box<NumExpr>) -> BoolExpr {
         self.make_cmp(Ordering::Less { strict: true }, lhs, rhs)
     }
 
     /// Create a "less than or equal" ([`BoolExpr::Cmp`]) expression
-    pub fn make_le(&self, lhs: Box<NumExpr>, rhs: Box<NumExpr>) -> Box<BoolExpr> {
+    pub fn make_le(&self, lhs: Box<NumExpr>, rhs: Box<NumExpr>) -> BoolExpr {
         self.make_cmp(Ordering::Less { strict: false }, lhs, rhs)
     }
 
     /// Create a "greater than" ([`BoolExpr::Cmp`]) expression
-    pub fn make_gt(&self, lhs: Box<NumExpr>, rhs: Box<NumExpr>) -> Box<BoolExpr> {
+    pub fn make_gt(&self, lhs: Box<NumExpr>, rhs: Box<NumExpr>) -> BoolExpr {
         self.make_cmp(Ordering::Greater { strict: true }, lhs, rhs)
     }
 
     /// Create a "greater than or equal" ([`BoolExpr::Cmp`]) expression
-    pub fn make_ge(&self, lhs: Box<NumExpr>, rhs: Box<NumExpr>) -> Box<BoolExpr> {
+    pub fn make_ge(&self, lhs: Box<NumExpr>, rhs: Box<NumExpr>) -> BoolExpr {
         self.make_cmp(Ordering::Greater { strict: false }, lhs, rhs)
     }
 
     /// Create a "equals" ([`BoolExpr::Cmp`]) expression
-    pub fn make_eq(&self, lhs: Box<NumExpr>, rhs: Box<NumExpr>) -> Box<BoolExpr> {
+    pub fn make_eq(&self, lhs: Box<NumExpr>, rhs: Box<NumExpr>) -> BoolExpr {
         self.make_cmp(Ordering::Eq, lhs, rhs)
     }
 
     /// Create a "not equals" ([`BoolExpr::Cmp`]) expression
-    pub fn make_neq(&self, lhs: Box<NumExpr>, rhs: Box<NumExpr>) -> Box<BoolExpr> {
+    pub fn make_neq(&self, lhs: Box<NumExpr>, rhs: Box<NumExpr>) -> BoolExpr {
         self.make_cmp(Ordering::NotEq, lhs, rhs)
     }
 
     /// Create a [`BoolExpr::Not`] expression.
-    pub fn make_not(&self, arg: Box<BoolExpr>) -> Box<BoolExpr> {
+    pub fn make_not(&self, arg: Box<BoolExpr>) -> BoolExpr {
-        Box::new((Not { arg }).into())
+        (Not { arg }).into()
     }
 
     /// Create a [`BoolExpr::Or`] expression.
-    pub fn make_or<I>(&self, args: I) -> ArgusResult<Box<BoolExpr>>
+    pub fn make_or<I>(&self, args: I) -> ArgusResult<BoolExpr>
     where
         I: IntoIterator<Item = BoolExpr>,
     {
-        let args: Vec<_> = args.into_iter().collect();
+        let mut new_args = Vec::<BoolExpr>::new();
-        if args.len() < 2 {
+        for arg in args.into_iter() {
+            // Flatten the args if there is an Or
+            if let BoolExpr::Or(Or { args }) = arg {
+                new_args.extend(args.into_iter());
+            } else {
+                new_args.push(arg);
+            }
+        }
+        if new_args.len() < 2 {
             Err(Error::IncompleteArgs)
         } else {
-            Ok(Box::new((Or { args }).into()))
+            Ok((Or { args: new_args }).into())
         }
     }
 
     /// Create a [`BoolExpr::And`] expression.
-    pub fn make_and<I>(&self, args: I) -> ArgusResult<Box<BoolExpr>>
+    pub fn make_and<I>(&self, args: I) -> ArgusResult<BoolExpr>
     where
         I: IntoIterator<Item = BoolExpr>,
     {
-        let args: Vec<_> = args.into_iter().collect();
+        let mut new_args = Vec::<BoolExpr>::new();
-        if args.len() < 2 {
+        for arg in args.into_iter() {
+            // Flatten the args if there is an And
+            if let BoolExpr::And(And { args }) = arg {
+                new_args.extend(args.into_iter());
+            } else {
+                new_args.push(arg);
+            }
+        }
+        if new_args.len() < 2 {
             Err(Error::IncompleteArgs)
         } else {
-            Ok(Box::new((And { args }).into()))
+            Ok((And { args: new_args }).into())
         }
     }
 
+    /// Create an expression equivalent to `lhs -> rhs`.
+    ///
+    /// This essentially breaks down the expression as `~lhs | rhs`.
+    #[allow(clippy::boxed_local)]
+    pub fn make_implies(&self, lhs: Box<BoolExpr>, rhs: Box<BoolExpr>) -> ArgusResult<BoolExpr> {
+        let np = self.make_not(lhs);
+        self.make_or([np, *rhs])
+    }
+
+    /// Create an expression equivalent to `lhs <-> rhs`.
+    ///
+    /// This essentially breaks down the expression as `(lhs & rhs) | (~lhs & ~rhs)`.
+    pub fn make_equiv(&self, lhs: Box<BoolExpr>, rhs: Box<BoolExpr>) -> ArgusResult<BoolExpr> {
+        let np = self.make_not(lhs.clone());
+        let nq = self.make_not(rhs.clone());
+
+        let npnq = self.make_and([np, nq])?;
+        let pq = self.make_and([*lhs, *rhs])?;
+
+        self.make_or([pq, npnq])
+    }
+
+    /// Create an expression equivalent to `lhs ^ rhs`.
+    ///
+    /// This essentially breaks down the expression as `~(lhs <-> rhs)`.
+    pub fn make_xor(&self, lhs: Box<BoolExpr>, rhs: Box<BoolExpr>) -> ArgusResult<BoolExpr> {
+        Ok(self.make_not(Box::new(self.make_equiv(lhs, rhs)?)))
+    }
+
     /// Create a [`BoolExpr::Next`] expression.
-    pub fn make_next(&self, arg: Box<BoolExpr>) -> Box<BoolExpr> {
+    pub fn make_next(&self, arg: Box<BoolExpr>) -> BoolExpr {
-        Box::new((Next { arg }).into())
+        (Next { arg }).into()
     }
 
     /// Create a [`BoolExpr::Oracle`] expression.
-    pub fn make_oracle(&self, steps: usize, arg: Box<BoolExpr>) -> Box<BoolExpr> {
+    pub fn make_oracle(&self, steps: usize, arg: Box<BoolExpr>) -> BoolExpr {
-        Box::new((Oracle { steps, arg }).into())
+        if steps == 1 {
+            self.make_next(arg)
+        } else {
+            (Oracle { steps, arg }).into()
+        }
     }
 
     /// Create a [`BoolExpr::Always`] expression.
-    pub fn make_always(&self, arg: Box<BoolExpr>) -> Box<BoolExpr> {
+    pub fn make_always(&self, arg: Box<BoolExpr>) -> BoolExpr {
-        Box::new(
         (Always {
             arg,
             interval: (..).into(),
         })
-            .into(),
+        .into()
-        )
     }
 
     /// Create a [`BoolExpr::Always`] expression with an interval.
-    pub fn make_timed_always(&self, interval: Interval, arg: Box<BoolExpr>) -> Box<BoolExpr> {
+    pub fn make_timed_always(&self, interval: Interval, arg: Box<BoolExpr>) -> BoolExpr {
-        Box::new((Always { arg, interval }).into())
+        (Always { arg, interval }).into()
     }
 
     /// Create a [`BoolExpr::Eventually`] expression.
-    pub fn make_eventually(&self, arg: Box<BoolExpr>) -> Box<BoolExpr> {
+    pub fn make_eventually(&self, arg: Box<BoolExpr>) -> BoolExpr {
-        Box::new(
         (Eventually {
             arg,
             interval: (..).into(),
         })
-            .into(),
+        .into()
-        )
     }
 
     /// Create a [`BoolExpr::Eventually`] expression with an interval.
-    pub fn make_timed_eventually(&self, interval: Interval, arg: Box<BoolExpr>) -> Box<BoolExpr> {
+    pub fn make_timed_eventually(&self, interval: Interval, arg: Box<BoolExpr>) -> BoolExpr {
-        Box::new((Eventually { arg, interval }).into())
+        (Eventually { arg, interval }).into()
     }
 
     /// Create a [`BoolExpr::Until`] expression.
-    pub fn make_until(&self, lhs: Box<BoolExpr>, rhs: Box<BoolExpr>) -> Box<BoolExpr> {
+    pub fn make_until(&self, lhs: Box<BoolExpr>, rhs: Box<BoolExpr>) -> BoolExpr {
-        Box::new(
         (Until {
             lhs,
             rhs,
             interval: (..).into(),
         })
-            .into(),
+        .into()
-        )
     }
 
     /// Create a [`BoolExpr::Until`] expression with an interval.
-    pub fn make_timed_until(&self, interval: Interval, lhs: Box<BoolExpr>, rhs: Box<BoolExpr>) -> Box<BoolExpr> {
+    pub fn make_timed_until(&self, interval: Interval, lhs: Box<BoolExpr>, rhs: Box<BoolExpr>) -> BoolExpr {
-        Box::new((Until { lhs, rhs, interval }).into())
+        BoolExpr::from(Until { lhs, rhs, interval })
     }
 }
 

argus-core/src/expr/iter.rs

@@ -53,13 +53,13 @@ mod tests {
     fn simple_iter() {
         let mut ctx = ExprBuilder::new();
 
-        let x = ctx.float_var("x".to_owned()).unwrap();
+        let x = Box::new(ctx.float_var("x".to_owned()).unwrap());
-        let y = ctx.float_var("y".to_owned()).unwrap();
+        let y = Box::new(ctx.float_var("y".to_owned()).unwrap());
-        let lit = ctx.float_const(2.0);
+        let lit = Box::new(ctx.float_const(2.0));
 
-        let pred1 = ctx.make_le(x.clone(), lit.clone());
+        let pred1 = Box::new(ctx.make_le(x.clone(), lit.clone()));
-        let pred2 = ctx.make_gt(y.clone(), lit.clone());
+        let pred2 = Box::new(ctx.make_gt(y.clone(), lit.clone()));
-        let spec = ctx.make_or([*pred1.clone(), *pred2.clone()]).unwrap();
+        let spec = Box::new(ctx.make_or([*pred1.clone(), *pred2.clone()]).unwrap());
 
         drop(ctx);
 

argus-parser/Cargo.toml

@@ -7,6 +7,10 @@ edition = "2021"
 name = "dump_parse_tree"
 required-features = ["reporting"]
 
+[[example]]
+name = "dump_expr"
+required-features = ["reporting"]
+
 [dependencies]
 argus-core = { version = "0.1.0", path = "../argus-core" }
 ariadne = { version = "0.3.0", optional = true }

argus-parser/examples/dump_expr.rs

@@ -0,0 +1,31 @@
+use std::env;
+
+use argus_parser::parse_str;
+use ariadne::{sources, Color, Label, Report, ReportKind};
+
+fn main() {
+    let src = env::args().nth(1).expect("Expected expression");
+
+    match parse_str(&src) {
+        Ok(expr) => println!("{:#?}", expr),
+        Err(errs) => {
+            errs.into_iter().for_each(|e| {
+                Report::build(ReportKind::Error, src.clone(), e.span().start)
+                    .with_message(e.to_string())
+                    .with_label(
+                        Label::new((src.clone(), e.span().into_range()))
+                            .with_message(e.reason().to_string())
+                            .with_color(Color::Red),
+                    )
+                    .with_labels(e.contexts().map(|(label, span)| {
+                        Label::new((src.clone(), span.into_range()))
+                            .with_message(format!("while parsing this {}", label))
+                            .with_color(Color::Yellow)
+                    }))
+                    .finish()
+                    .print(sources([(src.clone(), src.clone())]))
+                    .unwrap()
+            });
+        }
+    }
+}

argus-parser/src/lib.rs

@@ -1,7 +1,305 @@
 //! # Argus logic syntax
 
+use std::time::Duration;
+
+use argus_core::ExprBuilder;
 mod lexer;
 mod parser;
 
+use chumsky::prelude::Rich;
 pub use lexer::{lexer, Error as LexError, Span, Token};
 pub use parser::{parser, Expr, Interval};
+
+pub fn parse_str(src: &str) -> Result<argus_core::Expr, Vec<Rich<'_, String>>> {
+    use chumsky::prelude::{Input, Parser};
+
+    let (tokens, lex_errors) = lexer().parse(src.clone()).into_output_errors();
+
+    let (parsed, parse_errors) = if let Some(tokens) = &tokens {
+        parser()
+            .parse(tokens.as_slice().spanned((src.len()..src.len()).into()))
+            .into_output_errors()
+    } else {
+        (None, Vec::new())
+    };
+
+    let (expr, expr_errors) = if let Some((ast, span)) = parsed {
+        let mut expr_builder = ExprBuilder::new();
+        let result = ast_to_expr(&ast, span, &mut expr_builder);
+        match result {
+            Ok(expr) => (Some(expr), vec![]),
+            Err(err) => (None, vec![err]),
+        }
+    } else {
+        (None, vec![])
+    };
+
+    let errors: Vec<_> = lex_errors
+        .into_iter()
+        .map(|e| e.map_token(|c| c.to_string()))
+        .chain(parse_errors.into_iter().map(|e| e.map_token(|tok| tok.to_string())))
+        .chain(expr_errors.into_iter().map(|e| e.map_token(|tok| tok.to_string())))
+        .map(|e| e.into_owned())
+        .collect();
+    if !errors.is_empty() {
+        Err(errors)
+    } else {
+        expr.ok_or(errors)
+    }
+}
+
+fn interval_convert(interval: &Interval<'_>) -> argus_core::Interval {
+    use core::ops::Bound;
+    let a = if let Some(a) = &interval.a {
+        match &a.0 {
+            Expr::UInt(value) => Bound::Included(Duration::from_secs(*value)),
+            Expr::Float(value) => Bound::Included(Duration::from_secs_f64(*value)),
+            _ => unreachable!("must be valid numeric literal."),
+        }
+    } else {
+        Bound::Unbounded
+    };
+    let b = if let Some(b) = &interval.b {
+        match &b.0 {
+            Expr::UInt(value) => Bound::Included(Duration::from_secs(*value)),
+            Expr::Float(value) => Bound::Included(Duration::from_secs_f64(*value)),
+            _ => unreachable!("must be valid numeric literal."),
+        }
+    } else {
+        Bound::Unbounded
+    };
+    argus_core::Interval::new(a, b)
+}
+
+/// Convert a parsed [`Expr`] into an [Argus `Expr`](argus_core::Expr)
+fn ast_to_expr<'tokens, 'src: 'tokens>(
+    ast: &Expr<'src>,
+    span: lexer::Span,
+    ctx: &mut ExprBuilder,
+) -> Result<argus_core::Expr, Rich<'tokens, Token<'src>, lexer::Span>> {
+    match ast {
+        Expr::Error => unreachable!("Errors should have been caught by parser"),
+        Expr::Bool(value) => Ok(ctx.bool_const(*value).into()),
+        Expr::Int(value) => Ok(ctx.int_const(*value).into()),
+        Expr::UInt(value) => Ok(ctx.uint_const(*value).into()),
+        Expr::Float(value) => Ok(ctx.float_const(*value).into()),
+        Expr::Var { name, kind } => match kind {
+            parser::Type::Unknown => Err(Rich::custom(span, "All variables must have defined type by now.")),
+            parser::Type::Bool => ctx
+                .bool_var(name.to_string())
+                .map(|var| var.into())
+                .map_err(|err| Rich::custom(span, err.to_string())),
+            parser::Type::UInt => ctx
+                .uint_var(name.to_string())
+                .map(|var| var.into())
+                .map_err(|err| Rich::custom(span, err.to_string())),
+            parser::Type::Int => ctx
+                .int_var(name.to_string())
+                .map(|var| var.into())
+                .map_err(|err| Rich::custom(span, err.to_string())),
+            parser::Type::Float => ctx
+                .float_var(name.to_string())
+                .map(|var| var.into())
+                .map_err(|err| Rich::custom(span, err.to_string())),
+        },
+        Expr::Unary { op, interval, arg } => {
+            let arg = ast_to_expr(&arg.0, arg.1, ctx)?;
+            let interval = interval.as_ref().map(|(i, span)| (interval_convert(i), span));
+            match op {
+                parser::UnaryOps::Neg => {
+                    assert!(interval.is_none());
+                    let argus_core::Expr::Num(arg) = arg else {
+                        unreachable!("- must have numeric expression argument");
+                    };
+                    Ok(ctx.make_neg(Box::new(arg)).into())
+                }
+                parser::UnaryOps::Not => {
+                    assert!(interval.is_none());
+                    let argus_core::Expr::Bool(arg) = arg else {
+                        unreachable!("`Not` must have boolean expression argument");
+                    };
+                    Ok(ctx.make_not(Box::new(arg)).into())
+                }
+                parser::UnaryOps::Next => {
+                    use core::ops::Bound;
+                    let argus_core::Expr::Bool(arg) = arg else {
+                        unreachable!("`Next` must have boolean expression argument");
+                    };
+                    match interval {
+                        Some((interval, ispan)) => {
+                            let steps: usize = match (interval.start, interval.end) {
+                                (Bound::Included(start), Bound::Included(end)) => (end - start).as_secs() as usize,
+                                _ => {
+                                    return Err(Rich::custom(
+                                        *ispan,
+                                        "Oracle operation (X[..]) cannot have unbounded intervals",
+                                    ))
+                                }
+                            };
+                            Ok(ctx.make_oracle(steps, Box::new(arg)).into())
+                        }
+                        None => Ok(ctx.make_next(Box::new(arg)).into()),
+                    }
+                }
+                parser::UnaryOps::Always => {
+                    let argus_core::Expr::Bool(arg) = arg else {
+                        unreachable!("`Always` must have boolean expression argument");
+                    };
+                    match interval {
+                        Some((interval, _)) => Ok(ctx.make_timed_always(interval, Box::new(arg)).into()),
+                        None => Ok(ctx.make_always(Box::new(arg)).into()),
+                    }
+                }
+                parser::UnaryOps::Eventually => {
+                    let argus_core::Expr::Bool(arg) = arg else {
+                        unreachable!("`Eventually` must have boolean expression argument");
+                    };
+                    match interval {
+                        Some((interval, _)) => Ok(ctx.make_timed_eventually(interval, Box::new(arg)).into()),
+                        None => Ok(ctx.make_eventually(Box::new(arg)).into()),
+                    }
+                }
+            }
+        }
+        Expr::Binary {
+            op,
+            interval,
+            args: (lhs, rhs),
+        } => {
+            let lhs = ast_to_expr(&lhs.0, lhs.1, ctx)?;
+            let rhs = ast_to_expr(&rhs.0, rhs.1, ctx)?;
+            let interval = interval.as_ref().map(|(i, span)| (interval_convert(i), span));
+
+            match op {
+                parser::BinaryOps::Add => {
+                    assert!(interval.is_none());
+                    let (argus_core::Expr::Num(lhs), argus_core::Expr::Num(rhs)) = (lhs, rhs) else {
+                        unreachable!("`Add` must have numeric expression arguments");
+                    };
+                    ctx.make_add([lhs, rhs])
+                        .map(|ex| ex.into())
+                        .map_err(|err| Rich::custom(span, err.to_string()))
+                }
+                parser::BinaryOps::Sub => {
+                    assert!(interval.is_none());
+                    let (argus_core::Expr::Num(lhs), argus_core::Expr::Num(rhs)) = (lhs, rhs) else {
+                        unreachable!("`Sub` must have numeric expression arguments");
+                    };
+                    Ok(ctx.make_sub(Box::new(lhs), Box::new(rhs)).into())
+                }
+                parser::BinaryOps::Mul => {
+                    assert!(interval.is_none());
+                    let (argus_core::Expr::Num(lhs), argus_core::Expr::Num(rhs)) = (lhs, rhs) else {
+                        unreachable!("`Mul` must have numeric expression arguments");
+                    };
+                    ctx.make_mul([lhs, rhs])
+                        .map(|ex| ex.into())
+                        .map_err(|err| Rich::custom(span, err.to_string()))
+                }
+                parser::BinaryOps::Div => {
+                    assert!(interval.is_none());
+                    let (argus_core::Expr::Num(lhs), argus_core::Expr::Num(rhs)) = (lhs, rhs) else {
+                        unreachable!("`Div` must have numeric expression arguments");
+                    };
+                    Ok(ctx.make_div(Box::new(lhs), Box::new(rhs)).into())
+                }
+                parser::BinaryOps::Lt => {
+                    assert!(interval.is_none());
+                    let (argus_core::Expr::Num(lhs), argus_core::Expr::Num(rhs)) = (lhs, rhs) else {
+                        unreachable!("Relational operation must have numeric expression arguments");
+                    };
+                    Ok(ctx.make_lt(Box::new(lhs), Box::new(rhs)).into())
+                }
+                parser::BinaryOps::Le => {
+                    assert!(interval.is_none());
+                    let (argus_core::Expr::Num(lhs), argus_core::Expr::Num(rhs)) = (lhs, rhs) else {
+                        unreachable!("Relational operation must have numeric expression arguments");
+                    };
+                    Ok(ctx.make_le(Box::new(lhs), Box::new(rhs)).into())
+                }
+                parser::BinaryOps::Gt => {
+                    assert!(interval.is_none());
+                    let (argus_core::Expr::Num(lhs), argus_core::Expr::Num(rhs)) = (lhs, rhs) else {
+                        unreachable!("Relational operation must have numeric expression arguments");
+                    };
+                    Ok(ctx.make_gt(Box::new(lhs), Box::new(rhs)).into())
+                }
+                parser::BinaryOps::Ge => {
+                    assert!(interval.is_none());
+                    let (argus_core::Expr::Num(lhs), argus_core::Expr::Num(rhs)) = (lhs, rhs) else {
+                        unreachable!("Relational operation must have numeric expression arguments");
+                    };
+                    Ok(ctx.make_ge(Box::new(lhs), Box::new(rhs)).into())
+                }
+                parser::BinaryOps::Eq => {
+                    assert!(interval.is_none());
+                    let (argus_core::Expr::Num(lhs), argus_core::Expr::Num(rhs)) = (lhs, rhs) else {
+                        unreachable!("Relational operation must have numeric expression arguments");
+                    };
+                    Ok(ctx.make_eq(Box::new(lhs), Box::new(rhs)).into())
+                }
+                parser::BinaryOps::Neq => {
+                    assert!(interval.is_none());
+                    let (argus_core::Expr::Num(lhs), argus_core::Expr::Num(rhs)) = (lhs, rhs) else {
+                        unreachable!("Relational operation must have numeric expression arguments");
+                    };
+                    Ok(ctx.make_neq(Box::new(lhs), Box::new(rhs)).into())
+                }
+                parser::BinaryOps::And => {
+                    assert!(interval.is_none());
+                    let (argus_core::Expr::Bool(lhs), argus_core::Expr::Bool(rhs)) = (lhs, rhs) else {
+                        unreachable!("`And` must have boolean expression arguments");
+                    };
+                    ctx.make_and([lhs, rhs])
+                        .map(|ex| ex.into())
+                        .map_err(|err| Rich::custom(span, err.to_string()))
+                }
+                parser::BinaryOps::Or => {
+                    assert!(interval.is_none());
+                    let (argus_core::Expr::Bool(lhs), argus_core::Expr::Bool(rhs)) = (lhs, rhs) else {
+                        unreachable!("`Or` must have boolean expression arguments");
+                    };
+                    ctx.make_or([lhs, rhs])
+                        .map(|ex| ex.into())
+                        .map_err(|err| Rich::custom(span, err.to_string()))
+                }
+                parser::BinaryOps::Implies => {
+                    assert!(interval.is_none());
+                    let (argus_core::Expr::Bool(lhs), argus_core::Expr::Bool(rhs)) = (lhs, rhs) else {
+                        unreachable!("`Implies` must have boolean expression arguments");
+                    };
+                    ctx.make_implies(Box::new(lhs), Box::new(rhs))
+                        .map(|ex| ex.into())
+                        .map_err(|err| Rich::custom(span, err.to_string()))
+                }
+                parser::BinaryOps::Equiv => {
+                    assert!(interval.is_none());
+                    let (argus_core::Expr::Bool(lhs), argus_core::Expr::Bool(rhs)) = (lhs, rhs) else {
+                        unreachable!("`Equiv` must have boolean expression arguments");
+                    };
+                    ctx.make_equiv(Box::new(lhs), Box::new(rhs))
+                        .map(|ex| ex.into())
+                        .map_err(|err| Rich::custom(span, err.to_string()))
+                }
+                parser::BinaryOps::Xor => {
+                    assert!(interval.is_none());
+                    let (argus_core::Expr::Bool(lhs), argus_core::Expr::Bool(rhs)) = (lhs, rhs) else {
+                        unreachable!("`Xor` must have boolean expression arguments");
+                    };
+                    ctx.make_xor(Box::new(lhs), Box::new(rhs))
+                        .map(|ex| ex.into())
+                        .map_err(|err| Rich::custom(span, err.to_string()))
+                }
+                parser::BinaryOps::Until => {
+                    let (argus_core::Expr::Bool(lhs), argus_core::Expr::Bool(rhs)) = (lhs, rhs) else {
+                        unreachable!("`Until` must have boolean expression arguments");
+                    };
+                    match interval {
+                        Some((interval, _)) => Ok(ctx.make_timed_until(interval, Box::new(lhs), Box::new(rhs)).into()),
+                        None => Ok(ctx.make_until(Box::new(lhs), Box::new(rhs)).into()),
+                    }
+                }
+            }
+        }
+    }
+}

argus-parser/src/parser.rs

@@ -37,8 +37,8 @@ impl Type {
 
 #[derive(Debug, Clone, PartialEq)]
 pub struct Interval<'src> {
-    a: Box<Spanned<Expr<'src>>>,
+    pub a: Option<Box<Spanned<Expr<'src>>>>,
-    b: Box<Spanned<Expr<'src>>>,
+    pub b: Option<Box<Spanned<Expr<'src>>>>,
 }
 
 #[derive(Debug, Clone, Copy, PartialEq, Eq)]
@@ -134,38 +134,40 @@ impl<'src> Expr<'src> {
     }
 
     /// Make untyped (`Type::Unknown`) expressions into the given type.
-    /// Returns a boolean flag to denote successful transformation or not.
+    fn make_typed(mut self, ty: Type) -> Self {
-    fn make_typed(&mut self, ty: Type) -> bool {
+        if let Expr::Var { name: _, kind } = &mut self {
-        match self {
-            Expr::Var { name: _, kind } => {
             *kind = ty;
-                true
-            }
-            _ => false,
         }
+        self
     }
 
-    fn unary_op(op: UnaryOps, arg: Box<Spanned<Self>>, interval: Option<Spanned<Interval<'src>>>) -> Self {
+    fn unary_op(op: UnaryOps, arg: Spanned<Self>, interval: Option<Spanned<Interval<'src>>>) -> Self {
-        let mut arg = arg;
+        let arg = Box::new((arg.0.make_typed(op.default_type()), arg.1));
-        (*arg).0.make_typed(op.default_type());
         Self::Unary { op, interval, arg }
     }
 
     fn binary_op(
         op: BinaryOps,
-        args: (Box<Spanned<Self>>, Box<Spanned<Self>>),
+        args: (Spanned<Self>, Spanned<Self>),
         interval: Option<Spanned<Interval<'src>>>,
     ) -> Self {
-        let mut args = args;
+        let (lhs, lspan) = args.0;
-
+        let (rhs, rspan) = args.1;
-        let lhs = &mut (*args.0).0;
-        let rhs = &mut (*args.1).0;
 
         let common_type = lhs.get_type().get_common_cast(rhs.get_type());
-        lhs.make_typed(common_type);
+        let common_type = if Type::Unknown == common_type {
-        rhs.make_typed(common_type);
+            op.default_type()
+        } else {
+            common_type
+        };
+        let lhs = Box::new((lhs.make_typed(common_type), lspan));
+        let rhs = Box::new((rhs.make_typed(common_type), rspan));
 
-        Self::Binary { op, interval, args }
+        Self::Binary {
+            op,
+            interval,
+            args: (lhs, rhs),
+        }
     }
 }
 
@@ -179,7 +181,7 @@ pub type Error<'tokens, 'src> = extra::Err<Rich<'tokens, Token<'src>, Span>>;
 // to understand.
 type ParserInput<'tokens, 'src> = SpannedInput<Token<'src>, Span, &'tokens [(Token<'src>, Span)]>;
 
-pub fn num_expr_parser<'tokens, 'src: 'tokens>(
+fn num_expr_parser<'tokens, 'src: 'tokens>(
 ) -> impl Parser<'tokens, ParserInput<'tokens, 'src>, Spanned<Expr<'src>>, Error<'tokens, 'src>> + Clone {
     recursive(|num_expr| {
         let var = select! { Token::Ident(name) => Expr::Var{ name, kind: Type::default()} }.labelled("variable");
@@ -210,7 +212,7 @@ pub fn num_expr_parser<'tokens, 'src: 'tokens>(
             .repeated()
             .foldr(num_atom, |op, rhs| {
                 let span = op.1.start..rhs.1.end;
-                (Expr::unary_op(op.0, Box::new(rhs), None), span.into())
+                (Expr::unary_op(op.0, rhs, None), span.into())
             });
 
         // Product ops (multiply and divide) have equal precedence
@@ -223,7 +225,7 @@ pub fn num_expr_parser<'tokens, 'src: 'tokens>(
                 .clone()
                 .foldl(op.then(neg_op).repeated(), |a, (op, b)| {
                     let span = a.1.start..b.1.end;
-                    (Expr::binary_op(op, (Box::new(a), Box::new(b)), None), span.into())
+                    (Expr::binary_op(op, (a, b), None), span.into())
                 })
                 .boxed()
         };
@@ -238,7 +240,7 @@ pub fn num_expr_parser<'tokens, 'src: 'tokens>(
                 .clone()
                 .foldl(op.then(product_op).repeated(), |a, (op, b)| {
                     let span = a.1.start..b.1.end;
-                    (Expr::binary_op(op, (Box::new(a), Box::new(b)), None), span.into())
+                    (Expr::binary_op(op, (a, b), None), span.into())
                 })
                 .boxed()
         };
@@ -251,7 +253,6 @@ pub fn parser<'tokens, 'src: 'tokens>(
 ) -> impl Parser<'tokens, ParserInput<'tokens, 'src>, Spanned<Expr<'src>>, Error<'tokens, 'src>> + Clone {
     let interval = {
         let num_literal = select! {
-            Token::Int(val) => Expr::Int(val),
             Token::UInt(val) => Expr::UInt(val),
             Token::Float(val) => Expr::Float(val),
         }
@@ -259,17 +260,17 @@ pub fn parser<'tokens, 'src: 'tokens>(
         let sep = just(Token::Comma).or(just(Token::DotDot));
 
         num_literal
+            .or_not()
             .then_ignore(sep)
-            .then(num_literal)
+            .then(num_literal.or_not())
             .delimited_by(just(Token::LBracket), just(Token::RBracket))
-            .map(|(a, b)| {
+            .map_with_span(|(a, b), span| {
-                let span = a.1.start..b.1.end;
                 (
                     Interval {
-                        a: Box::new(a),
+                        a: a.map(Box::new),
-                        b: Box::new(b),
+                        b: b.map(Box::new),
                     },
-                    span.into(),
+                    span,
                 )
             })
             .boxed()
@@ -300,7 +301,7 @@ pub fn parser<'tokens, 'src: 'tokens>(
                 .then(op.then(num_expr))
                 .map(|(a, (op, b))| {
                     let span = a.1.start..b.1.end;
-                    (Expr::binary_op(op, (Box::new(a), Box::new(b)), None), span.into())
+                    (Expr::binary_op(op, (a, b), None), span.into())
                 })
                 .boxed()
         }
@@ -324,7 +325,7 @@ pub fn parser<'tokens, 'src: 'tokens>(
             .repeated()
             .foldr(atom, |op, rhs| {
                 let span = op.1.start..rhs.1.end;
-                (Expr::unary_op(op.0, Box::new(rhs), None), span.into())
+                (Expr::unary_op(op.0, rhs, None), span.into())
             })
             .boxed();
 
@@ -339,7 +340,7 @@ pub fn parser<'tokens, 'src: 'tokens>(
                 .repeated()
                 .foldr(not_op, |(op, interval), rhs| {
                     let span = op.1.start..rhs.1.end;
-                    (Expr::unary_op(op.0, Box::new(rhs), interval), span.into())
+                    (Expr::unary_op(op.0, rhs, interval), span.into())
                 })
                 .boxed()
         };
@@ -351,10 +352,7 @@ pub fn parser<'tokens, 'src: 'tokens>(
             .foldr(unary_temporal_op, |(lhs, (op, interval)), rhs| {
                 let span = lhs.1.start..rhs.1.end;
                 assert_eq!(op, BinaryOps::Until);
-                (
+                (Expr::binary_op(op, (lhs, rhs), interval), span.into())
-                    Expr::binary_op(op, (Box::new(lhs), Box::new(rhs)), interval),
-                    span.into(),
-                )
             })
             .boxed();
 
@@ -364,7 +362,7 @@ pub fn parser<'tokens, 'src: 'tokens>(
                 .clone()
                 .foldl(op.then(binary_temporal_op).repeated(), |a, (op, b)| {
                     let span = a.1.start..b.1.end;
-                    (Expr::binary_op(op, (Box::new(a), Box::new(b)), None), span.into())
+                    (Expr::binary_op(op, (a, b), None), span.into())
                 })
                 .boxed()
         };
@@ -375,7 +373,7 @@ pub fn parser<'tokens, 'src: 'tokens>(
                 .clone()
                 .foldl(op.then(and_op).repeated(), |a, (op, b)| {
                     let span = a.1.start..b.1.end;
-                    (Expr::binary_op(op, (Box::new(a), Box::new(b)), None), span.into())
+                    (Expr::binary_op(op, (a, b), None), span.into())
                 })
                 .boxed()
         };
@@ -386,7 +384,7 @@ pub fn parser<'tokens, 'src: 'tokens>(
                 .clone()
                 .foldl(op.then(or_op).repeated(), |a, (op, b)| {
                     let span = a.1.start..b.1.end;
-                    (Expr::binary_op(op, (Box::new(a), Box::new(b)), None), span.into())
+                    (Expr::binary_op(op, (a, b), None), span.into())
                 })
                 .boxed()
         };
@@ -399,11 +397,14 @@ pub fn parser<'tokens, 'src: 'tokens>(
                 .clone()
                 .foldl(op.then(xor_op).repeated(), |a, (op, b)| {
                     let span = a.1.start..b.1.end;
-                    (Expr::binary_op(op, (Box::new(a), Box::new(b)), None), span.into())
+                    (Expr::binary_op(op, (a, b), None), span.into())
                 })
                 .boxed()
         };
 
-        implies_equiv_op.labelled("boolean expression").as_context()
+        implies_equiv_op
+            .map(|(expr, span)| (expr.make_typed(Type::Bool), span))
+            .labelled("boolean expression")
+            .as_context()
     })
 }

argus-parser/src/util.rs

@@ -0,0 +1 @@
+

argus-semantics/src/semantics/boolean.rs

@@ -374,8 +374,8 @@ mod tests {
     fn less_than() {
         let mut ctx = ExprBuilder::new();
 
-        let a = ctx.float_var("a".to_owned()).unwrap();
+        let a = Box::new(ctx.float_var("a".to_owned()).unwrap());
-        let spec = ctx.make_lt(a, ctx.float_const(0.0));
+        let spec = ctx.make_lt(a, Box::new(ctx.float_const(0.0)));
 
         let signals = HashMap::from_iter(vec![(
             "a".to_owned(),
@@ -405,8 +405,8 @@ mod tests {
     fn eventually_unbounded() {
         let mut ctx = ExprBuilder::new();
 
-        let a = ctx.float_var("a".to_owned()).unwrap();
+        let a = Box::new(ctx.float_var("a".to_owned()).unwrap());
-        let cmp = ctx.make_ge(a, ctx.float_const(0.0));
+        let cmp = Box::new(ctx.make_ge(a, Box::new(ctx.float_const(0.0))));
         let spec = ctx.make_eventually(cmp);
 
         {

argus-semantics/src/semantics/quantitative.rs

@@ -474,8 +474,8 @@ mod tests {
     fn addition() {
         let mut ctx = ExprBuilder::new();
 
-        let a = ctx.float_var("a".to_owned()).unwrap();
+        let a = Box::new(ctx.float_var("a".to_owned()).unwrap());
-        let b = ctx.float_var("b".to_owned()).unwrap();
+        let b = Box::new(ctx.float_var("b".to_owned()).unwrap());
         let spec = ctx.make_add([*a, *b]).unwrap();
 
         {
@@ -552,8 +552,8 @@ mod tests {
     fn less_than() {
         let mut ctx = ExprBuilder::new();
 
-        let a = ctx.float_var("a".to_owned()).unwrap();
+        let a = Box::new(ctx.float_var("a".to_owned()).unwrap());
-        let spec = ctx.make_lt(a, ctx.float_const(0.0));
+        let spec = Box::new(ctx.make_lt(a, Box::new(ctx.float_const(0.0))));
 
         let signals = HashMap::from_iter(vec![(
             "a".to_owned(),
@@ -583,8 +583,8 @@ mod tests {
     fn eventually_unbounded() {
         let mut ctx = ExprBuilder::new();
 
-        let a = ctx.float_var("a".to_owned()).unwrap();
+        let a = Box::new(ctx.float_var("a".to_owned()).unwrap());
-        let cmp = ctx.make_ge(a, ctx.float_const(0.0));
+        let cmp = Box::new(ctx.make_ge(a, Box::new(ctx.float_const(0.0))));
         let spec = ctx.make_eventually(cmp);
 
         {
@@ -618,10 +618,10 @@ mod tests {
     fn unbounded_until() {
         let mut ctx = ExprBuilder::new();
 
-        let a = ctx.int_var("a".to_owned()).unwrap();
+        let a = Box::new(ctx.int_var("a".to_owned()).unwrap());
-        let b = ctx.int_var("b".to_owned()).unwrap();
+        let b = Box::new(ctx.int_var("b".to_owned()).unwrap());
-        let lhs = ctx.make_gt(a, ctx.int_const(0));
+        let lhs = Box::new(ctx.make_gt(a, Box::new(ctx.int_const(0))));
-        let rhs = ctx.make_gt(b, ctx.int_const(0));
+        let rhs = Box::new(ctx.make_gt(b, Box::new(ctx.int_const(0))));
         let spec = ctx.make_until(lhs, rhs);
 
         {