mstlo_macros/
lib.rs

1//! Procedural macro for STL (Signal Temporal Logic) formula definitions.
2//!
3//! This crate provides the `stl!` macro for defining STL formulas with a DSL syntax.
4
5use proc_macro::TokenStream;
6use proc_macro2::TokenStream as TokenStream2;
7use quote::quote;
8use syn::parse::{Parse, ParseStream};
9use syn::{Expr, Ident, LitBool, LitInt, Result, Token, bracketed, parenthesized};
10
11/// Convenience macro to construct a `::mstlo::Step`.
12///
13/// # Syntax
14///
15/// ```ignore
16/// step!("x", 5.5, 10ms);
17/// step!("x", 5.5, 1s);
18/// step!("x", 5.5, std::time::Duration::from_millis(10));
19/// ```
20///
21/// Supported integer duration suffixes are: `ns`, `us`, `ms`, and `s`.
22#[proc_macro]
23pub fn step(input: TokenStream) -> TokenStream {
24    let parsed = syn::parse_macro_input!(input as StepMacroInput);
25
26    let signal = parsed.signal;
27    let value = parsed.value;
28
29    let ts_tokens = match parsed.timestamp {
30        StepTimestamp::Suffixed(lit) => match duration_expr_from_lit(&lit) {
31            Ok(tokens) => tokens,
32            Err(err) => return err.to_compile_error().into(),
33        },
34        StepTimestamp::Expr(expr) => quote! { #expr },
35    };
36
37    quote! {
38        ::mstlo::Step::new(#signal, #value, #ts_tokens)
39    }
40    .into()
41}
42
43struct StepMacroInput {
44    signal: Expr,
45    value: Expr,
46    timestamp: StepTimestamp,
47}
48
49enum StepTimestamp {
50    Suffixed(LitInt),
51    Expr(Expr),
52}
53
54impl Parse for StepMacroInput {
55    fn parse(input: ParseStream) -> Result<Self> {
56        let signal = input.parse::<Expr>()?;
57        input.parse::<Token![,]>()?;
58        let value = input.parse::<Expr>()?;
59        input.parse::<Token![,]>()?;
60
61        let timestamp = if input.peek(LitInt) {
62            StepTimestamp::Suffixed(input.parse::<LitInt>()?)
63        } else {
64            StepTimestamp::Expr(input.parse::<Expr>()?)
65        };
66
67        if !input.is_empty() {
68            return Err(input.error("unexpected tokens after timestamp argument"));
69        }
70
71        Ok(Self {
72            signal,
73            value,
74            timestamp,
75        })
76    }
77}
78
79fn duration_expr_from_lit(lit: &LitInt) -> Result<TokenStream2> {
80    let value = lit.base10_parse::<u64>()?;
81    let suffix = lit.suffix();
82
83    match suffix {
84        "ns" => Ok(quote! { ::std::time::Duration::from_nanos(#value) }),
85        "us" => Ok(quote! { ::std::time::Duration::from_micros(#value) }),
86        "ms" => Ok(quote! { ::std::time::Duration::from_millis(#value) }),
87        "s" => Ok(quote! { ::std::time::Duration::from_secs(#value) }),
88        _ => Err(syn::Error::new(
89            lit.span(),
90            "unsupported duration suffix; use one of: ns, us, ms, s",
91        )),
92    }
93}
94
95/// The main entry point for the `stl!` procedural macro.
96///
97/// # Syntax
98///
99/// ## Atomics
100/// - `true` - Always true
101/// - `false` - Always false
102///
103/// ## Predicates
104/// - `signal > value` - Signal greater than value
105/// - `signal < value` - Signal less than value
106/// - `signal >= value` - Signal greater than or equal to value (sugar for `!(signal < value)`)
107/// - `signal <= value` - Signal less than or equal to value (sugar for `!(signal > value)`)
108/// - `signal == value` - Signal equal to value (sugar for `(signal >= value) && (signal <= value)`)
109///
110/// ## Variable Predicates
111/// Use `$variable` syntax to reference runtime variables that can be updated at runtime:
112/// - `signal > $threshold` - Signal greater than runtime variable `threshold`
113/// - `signal < $limit` - Signal less than runtime variable `limit`
114/// - `signal >= $min` - Signal greater than or equal to runtime variable `min`
115/// - `signal <= $max` - Signal less than or equal to runtime variable `max`
116/// - `signal == $target` - Signal equal to runtime variable `target`
117///
118/// ## Unary Operators
119/// - `!(sub)` or `not(sub)` - Negation
120/// - `G[start, end](sub)` or `globally[start, end](sub)` - Globally
121/// - `F[start, end](sub)` or `eventually[start, end](sub)` - Eventually
122///
123/// ## Binary Operators (parentheses optional for simple operands)
124/// - `left && right` or `left and right` - Conjunction
125/// - `left || right` or `left or right` - Disjunction  
126/// - `left -> right` or `left implies right` - Implication
127/// - `left U[start, end] right` or `left until[start, end] right` - Until
128///
129/// ## Operator Precedence
130/// Operators have the following precedence (from lowest to highest):
131/// - `Implication (->, implies)` : Lowest (1, right-associative)
132/// - `Or (||, or)`               : (2)
133/// - `And (&&, and)`             : (3)
134/// - `Until (U, until)`          : (4)
135/// - `Unary (F, G) and Atoms`               : Highest (5)
136///
137/// # Examples
138///
139/// ```ignore
140/// // With parentheses
141/// let formula = stl!(G[0, 5]((signal > 5) and ((x > 0) U[0, 2] (true))));
142/// // Without parentheses using operator precedence
143/// let formula = stl!(x > 0 && y < 10);
144/// let formula = stl!(G[0, 5](x > 0 && y < 10));
145/// // With runtime variables
146/// let formula = stl!(G[0, 5](signal > $threshold));
147/// let formula = stl!(x > 5 && y < $limit);
148/// ```
149#[proc_macro]
150pub fn stl(input: TokenStream) -> TokenStream {
151    let input2 = TokenStream2::from(input);
152
153    match parse_stl_formula(input2) {
154        Ok(output) => output.into(),
155        Err(err) => err.to_compile_error().into(),
156    }
157}
158
159fn parse_stl_formula(input: TokenStream2) -> Result<TokenStream2> {
160    // since the Parse trait is implemented for StlFormula, we can use syn to parse it
161    let formula: StlFormula = syn::parse2(input)?;
162    Ok(formula.to_token_stream())
163}
164
165/// Represents a predicate value - either a constant expression or a variable reference
166enum PredicateValue {
167    /// A constant expression (e.g., `5`, `threshold`, `(x + 1)`)
168    Const(Expr),
169    /// A variable reference using $ syntax (e.g., `$threshold`)
170    Var(Ident),
171}
172
173/// Represents a parsed STL formula.
174enum StlFormula {
175    True,
176    False,
177    GreaterThan(Ident, Expr),
178    LessThan(Ident, Expr),
179    /// Variable-based greater-than: signal > $variable
180    GreaterThanVar(Ident, Ident),
181    /// Variable-based less-than: signal < $variable
182    LessThanVar(Ident, Ident),
183    Not(Box<StlFormula>),
184    And(Box<StlFormula>, Box<StlFormula>),
185    Or(Box<StlFormula>, Box<StlFormula>),
186    Implies(Box<StlFormula>, Box<StlFormula>),
187    Globally(Expr, Expr, Box<StlFormula>),
188    Eventually(Expr, Expr, Box<StlFormula>),
189    Until(Expr, Expr, Box<StlFormula>, Box<StlFormula>),
190    /// Interpolation: an arbitrary expression that evaluates to FormulaDefinition
191    Interpolated(Expr),
192}
193
194impl StlFormula {
195    fn to_token_stream(&self) -> TokenStream2 {
196        match self {
197            StlFormula::True => quote! {
198                ::mstlo::FormulaDefinition::True
199            },
200            StlFormula::False => quote! {
201                ::mstlo::FormulaDefinition::False
202            },
203            StlFormula::GreaterThan(signal, val) => {
204                let signal_str = signal.to_string();
205                quote! {
206                    ::mstlo::FormulaDefinition::GreaterThan(#signal_str, #val as f64)
207                }
208            }
209            StlFormula::LessThan(signal, val) => {
210                let signal_str = signal.to_string();
211                quote! {
212                    ::mstlo::FormulaDefinition::LessThan(#signal_str, #val as f64)
213                }
214            }
215            StlFormula::GreaterThanVar(signal, var) => {
216                let signal_str = signal.to_string();
217                let var_str = var.to_string();
218                quote! {
219                    ::mstlo::FormulaDefinition::GreaterThanVar(#signal_str, #var_str)
220                }
221            }
222            StlFormula::LessThanVar(signal, var) => {
223                let signal_str = signal.to_string();
224                let var_str = var.to_string();
225                quote! {
226                    ::mstlo::FormulaDefinition::LessThanVar(#signal_str, #var_str)
227                }
228            }
229            StlFormula::Not(sub) => {
230                let sub_tokens = sub.to_token_stream();
231                quote! {
232                    ::mstlo::FormulaDefinition::Not(
233                        Box::new(#sub_tokens)
234                    )
235                }
236            }
237            StlFormula::And(left, right) => {
238                let left_tokens = left.to_token_stream();
239                let right_tokens = right.to_token_stream();
240                quote! {
241                    ::mstlo::FormulaDefinition::And(
242                        Box::new(#left_tokens),
243                        Box::new(#right_tokens)
244                    )
245                }
246            }
247            StlFormula::Or(left, right) => {
248                let left_tokens = left.to_token_stream();
249                let right_tokens = right.to_token_stream();
250                quote! {
251                    ::mstlo::FormulaDefinition::Or(
252                        Box::new(#left_tokens),
253                        Box::new(#right_tokens)
254                    )
255                }
256            }
257            StlFormula::Implies(left, right) => {
258                let left_tokens = left.to_token_stream();
259                let right_tokens = right.to_token_stream();
260                quote! {
261                    ::mstlo::FormulaDefinition::Implies(
262                        Box::new(#left_tokens),
263                        Box::new(#right_tokens)
264                    )
265                }
266            }
267            StlFormula::Globally(start, end, sub) => {
268                let sub_tokens = sub.to_token_stream();
269                quote! {
270                    ::mstlo::FormulaDefinition::Globally(
271                        ::mstlo::TimeInterval {
272                            start: ::std::time::Duration::from_secs(#start as u64),
273                            end: ::std::time::Duration::from_secs(#end as u64),
274                        },
275                        Box::new(#sub_tokens)
276                    )
277                }
278            }
279            StlFormula::Eventually(start, end, sub) => {
280                let sub_tokens = sub.to_token_stream();
281                quote! {
282                    ::mstlo::FormulaDefinition::Eventually(
283                        ::mstlo::TimeInterval {
284                            start: ::std::time::Duration::from_secs(#start as u64),
285                            end: ::std::time::Duration::from_secs(#end as u64),
286                        },
287                        Box::new(#sub_tokens)
288                    )
289                }
290            }
291            StlFormula::Until(start, end, left, right) => {
292                let left_tokens = left.to_token_stream();
293                let right_tokens = right.to_token_stream();
294                quote! {
295                    ::mstlo::FormulaDefinition::Until(
296                        ::mstlo::TimeInterval {
297                            start: ::std::time::Duration::from_secs(#start as u64),
298                            end: ::std::time::Duration::from_secs(#end as u64),
299                        },
300                        Box::new(#left_tokens),
301                        Box::new(#right_tokens)
302                    )
303                }
304            }
305            StlFormula::Interpolated(expr) => {
306                quote! { #expr }
307            }
308        }
309    }
310}
311
312impl Parse for StlFormula {
313    fn parse(input: ParseStream) -> Result<Self> {
314        parse_expr(input, 0) // Start parsing with minimum precedence 0
315    }
316}
317
318/// Operator precedence levels (higher = binds tighter)
319/// Implication (->, implies) : 1 (lowest, right-associative)
320/// Or (||, or)               : 2
321/// And (&&, and)             : 3
322/// Until (U, until)          : 4
323/// Unary/Atoms               : 5 (highest)
324fn get_binary_op_precedence(input: ParseStream) -> Option<u8> {
325    if input.peek(Token![->]) {
326        return Some(1);
327    }
328    if input.peek(Token![||]) {
329        return Some(2);
330    }
331    if input.peek(Token![&&]) {
332        return Some(3);
333    }
334    if input.peek(Ident) {
335        let fork = input.fork();
336        if let Ok(ident) = fork.parse::<Ident>() {
337            match ident.to_string().as_str() {
338                "implies" => return Some(1),
339                "or" => return Some(2),
340                "and" => return Some(3),
341                "U" | "until" => return Some(4),
342                _ => {}
343            }
344        }
345    }
346    None
347}
348
349/// Parse an expression with precedence climbing (Pratt parser)
350fn parse_expr(input: ParseStream, min_prec: u8) -> Result<StlFormula> {
351    let mut left = parse_primary(input)?;
352
353    while let Some(prec) = get_binary_op_precedence(input) {
354        if prec < min_prec {
355            break;
356        }
357
358        left = parse_binary_op(input, left, prec)?;
359    }
360
361    Ok(left)
362}
363
364/// Parse a binary operator and its right operand
365fn parse_binary_op(input: ParseStream, left: StlFormula, prec: u8) -> Result<StlFormula> {
366    // Parse the operator
367    if input.peek(Token![&&]) {
368        let op_token = input.parse::<Token![&&]>()?;
369        if input.is_empty() {
370            return Err(syn::Error::new(
371                op_token.spans[0],
372                "missing right operand after '&&'\n  help: conjunction requires a formula on both sides, e.g., `x > 0 && y < 10`",
373            ));
374        }
375        let right = parse_expr(input, prec + 1)?;
376        return Ok(StlFormula::And(Box::new(left), Box::new(right)));
377    }
378
379    if input.peek(Token![||]) {
380        let op_token = input.parse::<Token![||]>()?;
381        if input.is_empty() {
382            return Err(syn::Error::new(
383                op_token.spans[0],
384                "missing right operand after '||'\n  help: disjunction requires a formula on both sides, e.g., `x > 0 || y < 10`",
385            ));
386        }
387        let right = parse_expr(input, prec + 1)?;
388        return Ok(StlFormula::Or(Box::new(left), Box::new(right)));
389    }
390
391    if input.peek(Token![->]) {
392        let op_token = input.parse::<Token![->]>()?;
393        if input.is_empty() {
394            return Err(syn::Error::new(
395                op_token.spans[0],
396                "missing right operand after '->'\n  help: implication requires a formula on both sides, e.g., `x > 0 -> y < 10`",
397            ));
398        }
399        // Implication is right-associative, so use same precedence
400        let right = parse_expr(input, prec)?;
401        return Ok(StlFormula::Implies(Box::new(left), Box::new(right)));
402    }
403
404    if input.peek(Ident) {
405        let fork = input.fork();
406        let ident: Ident = fork.parse()?;
407        let ident_str = ident.to_string();
408
409        match ident_str.as_str() {
410            "and" => {
411                let op_ident = input.parse::<Ident>()?;
412                if input.is_empty() {
413                    return Err(syn::Error::new(
414                        op_ident.span(),
415                        "missing right operand after 'and'\n  help: conjunction requires a formula on both sides, e.g., `(x > 0) and (y < 10)`",
416                    ));
417                }
418                let right = parse_expr(input, prec + 1)?;
419                return Ok(StlFormula::And(Box::new(left), Box::new(right)));
420            }
421            "or" => {
422                let op_ident = input.parse::<Ident>()?;
423                if input.is_empty() {
424                    return Err(syn::Error::new(
425                        op_ident.span(),
426                        "missing right operand after 'or'\n  help: disjunction requires a formula on both sides, e.g., `(x > 0) or (y < 10)`",
427                    ));
428                }
429                let right = parse_expr(input, prec + 1)?;
430                return Ok(StlFormula::Or(Box::new(left), Box::new(right)));
431            }
432            "implies" => {
433                let op_ident = input.parse::<Ident>()?;
434                if input.is_empty() {
435                    return Err(syn::Error::new(
436                        op_ident.span(),
437                        "missing right operand after 'implies'\n  help: implication requires a formula on both sides, e.g., `(x > 0) implies (y < 10)`",
438                    ));
439                }
440                // Right-associative
441                let right = parse_expr(input, prec)?;
442                return Ok(StlFormula::Implies(Box::new(left), Box::new(right)));
443            }
444            "U" | "until" => {
445                let op_ident = input.parse::<Ident>()?;
446
447                if !input.peek(syn::token::Bracket) {
448                    return Err(syn::Error::new(
449                        op_ident.span(),
450                        format!(
451                            "missing time interval after '{}'\n  \
452                            help: the '{}' operator requires a time interval, e.g., `left {}[0, 10] right`",
453                            ident_str, ident_str, ident_str
454                        ),
455                    ));
456                }
457
458                let (start, end) = parse_time_interval(input)?;
459
460                if input.is_empty() {
461                    return Err(syn::Error::new(
462                        op_ident.span(),
463                        format!(
464                            "missing right operand after '{}[_, _]'\n  \
465                            help: until requires a formula on both sides, e.g., `(x > 0) {}[0, 10] (y < 10)`",
466                            ident_str, ident_str
467                        ),
468                    ));
469                }
470
471                let right = parse_expr(input, prec + 1)?;
472                return Ok(StlFormula::Until(
473                    start,
474                    end,
475                    Box::new(left),
476                    Box::new(right),
477                ));
478            }
479            _ => {}
480        }
481    }
482
483    Err(syn::Error::new(
484        input.span(),
485        "expected binary operator (&&, ||, ->, and, or, implies, U[_, _], until[_, _])",
486    ))
487}
488
489/// Parse a primary expression (atoms, unary operators, parenthesized expressions)
490fn parse_primary(input: ParseStream) -> Result<StlFormula> {
491    // Check for Rust boolean literals first
492    if input.peek(LitBool) {
493        let lit: LitBool = input.parse()?;
494        return if lit.value {
495            Ok(StlFormula::True)
496        } else {
497            Ok(StlFormula::False)
498        };
499    }
500
501    // Check for negation: !
502    if input.peek(Token![!]) {
503        return parse_not(input);
504    }
505
506    // Check for keyword operators and predicates
507    if input.peek(Ident) {
508        let fork = input.fork();
509        let ident: Ident = fork.parse()?;
510        let ident_str = ident.to_string();
511
512        match ident_str.as_str() {
513            "not" => return parse_not_keyword(input),
514            "G" | "globally" => return parse_globally(input),
515            "F" | "eventually" => return parse_eventually(input),
516            _ => {
517                // Try to parse as a predicate
518                if let Ok(predicate) = try_parse_predicate(input) {
519                    return Ok(predicate);
520                }
521            }
522        }
523    }
524
525    // Check for parenthesized expression
526    if input.peek(syn::token::Paren) {
527        let content;
528        parenthesized!(content in input);
529        let inner = parse_expr(&content, 0)?;
530
531        if !content.is_empty() {
532            return Err(content.error("unexpected tokens inside parentheses"));
533        }
534
535        return Ok(inner);
536    }
537
538    // Fallback: parse as an arbitrary expression (interpolation)
539    let expr: Expr = input.parse()?;
540    Ok(StlFormula::Interpolated(expr))
541}
542
543/// Parse negation: !(sub) or !sub for simple atoms
544fn parse_not(input: ParseStream) -> Result<StlFormula> {
545    let not_token = input.parse::<Token![!]>()?;
546
547    if input.is_empty() {
548        return Err(syn::Error::new(
549            not_token.span,
550            "missing operand after '!'\n  \
551            help: negation requires a subformula, e.g., `!(x > 5)` or `!true`",
552        ));
553    }
554
555    // Allow both !(sub) with parentheses and !sub without for simple expressions
556    if input.peek(syn::token::Paren) {
557        let content;
558        parenthesized!(content in input);
559
560        if content.is_empty() {
561            return Err(content.error(
562                "empty subformula in negation\n  \
563                help: negation requires a subformula, e.g., `!(x > 5)`",
564            ));
565        }
566
567        let sub = parse_expr(&content, 0)?;
568
569        if !content.is_empty() {
570            return Err(content.error(
571                "unexpected tokens after negation subformula\n  \
572                help: if you want to negate a complex formula, wrap it in parentheses: `!(a && b)`",
573            ));
574        }
575
576        Ok(StlFormula::Not(Box::new(sub)))
577    } else {
578        // Parse the next primary expression
579        let sub = parse_primary(input)?;
580        Ok(StlFormula::Not(Box::new(sub)))
581    }
582}
583
584/// Parse negation keyword: not(sub) or not sub
585fn parse_not_keyword(input: ParseStream) -> Result<StlFormula> {
586    let ident: Ident = input.parse()?;
587    if ident != "not" {
588        return Err(syn::Error::new(ident.span(), "expected 'not'"));
589    }
590
591    if input.is_empty() {
592        return Err(syn::Error::new(
593            ident.span(),
594            "missing operand after 'not'\n  \
595            help: negation requires a subformula, e.g., `not(x > 5)` or `not true`",
596        ));
597    }
598
599    // Allow both not(sub) with parentheses and not sub without
600    if input.peek(syn::token::Paren) {
601        let content;
602        parenthesized!(content in input);
603
604        if content.is_empty() {
605            return Err(content.error(
606                "empty subformula in negation\n  \
607                help: negation requires a subformula, e.g., `not(x > 5)`",
608            ));
609        }
610
611        let sub = parse_expr(&content, 0)?;
612
613        if !content.is_empty() {
614            return Err(content.error(
615                "unexpected tokens after negation subformula\n  \
616                help: if you want to negate a complex formula, wrap it in parentheses: `not(a and b)`"
617            ));
618        }
619
620        Ok(StlFormula::Not(Box::new(sub)))
621    } else {
622        let sub = parse_primary(input)?;
623        Ok(StlFormula::Not(Box::new(sub)))
624    }
625}
626
627/// Parse time interval: [start, end]
628fn parse_time_interval(input: ParseStream) -> Result<(Expr, Expr)> {
629    let content;
630    bracketed!(content in input);
631
632    if content.is_empty() {
633        return Err(content.error(
634            "empty time interval\n  \
635            help: time intervals require two values [start, end], e.g., [0, 10]",
636        ));
637    }
638
639    let start: Expr = content.parse().map_err(|_| {
640        syn::Error::new(
641            content.span(),
642            "invalid start value in time interval\n  \
643            help: expected a numeric expression for the interval start, e.g., [0, 10]",
644        )
645    })?;
646
647    if !content.peek(Token![,]) {
648        return Err(syn::Error::new(
649            content.span(),
650            "missing comma in time interval\n  \
651            help: time intervals must have two comma-separated values [start, end], e.g., [0, 10]",
652        ));
653    }
654    content.parse::<Token![,]>()?;
655
656    if content.is_empty() {
657        return Err(content.error(
658            "missing end value in time interval\n  \
659            help: time intervals require two values [start, end], e.g., [0, 10]",
660        ));
661    }
662
663    let end: Expr = content.parse().map_err(|_| {
664        syn::Error::new(
665            content.span(),
666            "invalid end value in time interval\n  \
667            help: expected a numeric expression for the interval end, e.g., [0, 10]",
668        )
669    })?;
670
671    if !content.is_empty() {
672        return Err(content.error(
673            "too many values in time interval\n  \
674            help: time intervals take exactly two values [start, end], e.g., [0, 10]",
675        ));
676    }
677
678    Ok((start, end))
679}
680
681/// Parse globally: G[start, end]\(sub\) or G[start, end] sub
682fn parse_globally(input: ParseStream) -> Result<StlFormula> {
683    let ident: Ident = input.parse()?;
684    let ident_str = ident.to_string();
685
686    if ident_str != "G" && ident_str != "globally" {
687        return Err(syn::Error::new(
688            ident.span(),
689            format!("expected 'G' or 'globally', found '{}'", ident_str),
690        ));
691    }
692
693    if !input.peek(syn::token::Bracket) {
694        return Err(syn::Error::new(
695            ident.span(),
696            format!(
697                "missing time interval after '{}'\n  \
698                help: the globally operator requires a time interval, e.g., `{}[0, 10](x > 5)`\n  \
699                note: '{}' means \"always\" within the given time window",
700                ident_str, ident_str, ident_str
701            ),
702        ));
703    }
704
705    let (start, end) = parse_time_interval(input)?;
706
707    // Allow both G[a,b](sub) with parentheses and G[a,b] sub without
708    let sub = if input.peek(syn::token::Paren) {
709        let content;
710        parenthesized!(content in input);
711
712        if content.is_empty() {
713            return Err(content.error(
714                "empty subformula in globally operator\n  \
715                help: globally requires a subformula, e.g., `G[0, 10](x > 5)`",
716            ));
717        }
718
719        let sub = parse_expr(&content, 0)?;
720
721        if !content.is_empty() {
722            return Err(content.error(
723                "unexpected tokens after globally subformula\n  \
724                help: if you want to combine formulas, use binary operators outside the parentheses"
725            ));
726        }
727        sub
728    } else if input.is_empty() {
729        return Err(syn::Error::new(
730            ident.span(),
731            format!(
732                "missing subformula after '{}[_, _]'\n  \
733                help: globally requires a subformula, e.g., `{}[0, 10](x > 5)` or `{}[0, 10] x > 5`",
734                ident_str, ident_str, ident_str
735            ),
736        ));
737    } else {
738        parse_primary(input)?
739    };
740
741    Ok(StlFormula::Globally(start, end, Box::new(sub)))
742}
743
744/// Parse eventually: F[start, end]\(sub\) or F[start, end] sub  
745fn parse_eventually(input: ParseStream) -> Result<StlFormula> {
746    let ident: Ident = input.parse()?;
747    let ident_str = ident.to_string();
748
749    if ident_str != "F" && ident_str != "eventually" {
750        return Err(syn::Error::new(
751            ident.span(),
752            format!("expected 'F' or 'eventually', found '{}'", ident_str),
753        ));
754    }
755
756    if !input.peek(syn::token::Bracket) {
757        return Err(syn::Error::new(
758            ident.span(),
759            format!(
760                "missing time interval after '{}'\n  \
761                help: the eventually operator requires a time interval, e.g., `{}[0, 10](x > 5)`\n  \
762                note: '{}' means \"at some point\" within the given time window",
763                ident_str, ident_str, ident_str
764            ),
765        ));
766    }
767
768    let (start, end) = parse_time_interval(input)?;
769
770    // Allow both F[a,b](sub) with parentheses and F[a,b] sub without
771    let sub = if input.peek(syn::token::Paren) {
772        let content;
773        parenthesized!(content in input);
774
775        if content.is_empty() {
776            return Err(content.error(
777                "empty subformula in eventually operator\n  \
778                help: eventually requires a subformula, e.g., `F[0, 10](x > 5)`",
779            ));
780        }
781
782        let sub = parse_expr(&content, 0)?;
783
784        if !content.is_empty() {
785            return Err(content.error(
786                "unexpected tokens after eventually subformula\n  \
787                help: if you want to combine formulas, use binary operators outside the parentheses"
788            ));
789        }
790        sub
791    } else if input.is_empty() {
792        return Err(syn::Error::new(
793            ident.span(),
794            format!(
795                "missing subformula after '{}[_, _]'\n  \
796                help: eventually requires a subformula, e.g., `{}[0, 10](x > 5)` or `{}[0, 10] x > 5`",
797                ident_str, ident_str, ident_str
798            ),
799        ));
800    } else {
801        parse_primary(input)?
802    };
803
804    Ok(StlFormula::Eventually(start, end, Box::new(sub)))
805}
806
807/// Try to parse a predicate: signal > val, signal < val, signal >= val, signal <= val, signal == val
808fn try_parse_predicate(input: ParseStream) -> Result<StlFormula> {
809    let fork = input.fork();
810
811    // Must start with an identifier (signal name)
812    if !fork.peek(Ident) {
813        return Err(syn::Error::new(input.span(), "expected signal identifier"));
814    }
815
816    let signal: Ident = fork.parse()?;
817    let signal_str = signal.to_string();
818
819    // Check it's not a keyword
820    if matches!(
821        signal_str.as_str(),
822        "true"
823            | "false"
824            | "not"
825            | "and"
826            | "or"
827            | "implies"
828            | "G"
829            | "F"
830            | "U"
831            | "globally"
832            | "eventually"
833            | "until"
834    ) {
835        return Err(syn::Error::new(
836            signal.span(),
837            format!(
838                "'{}' is a reserved keyword and cannot be used as a signal name\n  \
839                help: use a different identifier for your signal",
840                signal_str
841            ),
842        ));
843    }
844
845    // Parse comparison operator
846    if fork.peek(Token![>]) && !fork.peek(Token![>=]) {
847        fork.parse::<Token![>]>()?;
848        let val = parse_predicate_value(&fork).map_err(|_| {
849            syn::Error::new(
850                fork.span(),
851                format!(
852                    "invalid value after '>' in predicate\n  \
853                    help: expected a numeric value, e.g., `{} > 5` or `{} > $threshold`",
854                    signal_str, signal_str
855                ),
856            )
857        })?;
858
859        // Commit the parse
860        input.parse::<Ident>()?;
861        input.parse::<Token![>]>()?;
862        let _: PredicateValue = parse_predicate_value(input)?;
863
864        return match val {
865            PredicateValue::Const(expr) => Ok(StlFormula::GreaterThan(signal, expr)),
866            PredicateValue::Var(var_ident) => Ok(StlFormula::GreaterThanVar(signal, var_ident)),
867        };
868    }
869
870    if fork.peek(Token![<]) && !fork.peek(Token![<=]) {
871        fork.parse::<Token![<]>()?;
872        let val = parse_predicate_value(&fork).map_err(|_| {
873            syn::Error::new(
874                fork.span(),
875                format!(
876                    "invalid value after '<' in predicate\n  \
877                    help: expected a numeric value, e.g., `{} < 5` or `{} < $threshold`",
878                    signal_str, signal_str
879                ),
880            )
881        })?;
882
883        // Commit the parse
884        input.parse::<Ident>()?;
885        input.parse::<Token![<]>()?;
886        let _: PredicateValue = parse_predicate_value(input)?;
887
888        return match val {
889            PredicateValue::Const(expr) => Ok(StlFormula::LessThan(signal, expr)),
890            PredicateValue::Var(var_ident) => Ok(StlFormula::LessThanVar(signal, var_ident)),
891        };
892    }
893
894    if fork.peek(Token![>=]) {
895        fork.parse::<Token![>=]>()?;
896        let val = parse_predicate_value(&fork).map_err(|_| {
897            syn::Error::new(
898                fork.span(),
899                format!(
900                    "invalid value after '>=' in predicate\n  \
901                    help: expected a numeric value, e.g., `{} >= 5` or `{} >= $threshold`",
902                    signal_str, signal_str
903                ),
904            )
905        })?;
906
907        // Commit the parse
908        input.parse::<Ident>()?;
909        input.parse::<Token![>=]>()?;
910        let _: PredicateValue = parse_predicate_value(input)?;
911
912        // >= is sugar for !(signal < val)
913        return match val {
914            PredicateValue::Const(expr) => Ok(StlFormula::Not(Box::new(StlFormula::LessThan(
915                signal, expr,
916            )))),
917            PredicateValue::Var(var_ident) => Ok(StlFormula::Not(Box::new(
918                StlFormula::LessThanVar(signal, var_ident),
919            ))),
920        };
921    }
922
923    if fork.peek(Token![<=]) {
924        fork.parse::<Token![<=]>()?;
925        let val = parse_predicate_value(&fork).map_err(|_| {
926            syn::Error::new(
927                fork.span(),
928                format!(
929                    "invalid value after '<=' in predicate\n  \
930                    help: expected a numeric value, e.g., `{} <= 5` or `{} <= $threshold`",
931                    signal_str, signal_str
932                ),
933            )
934        })?;
935
936        // Commit the parse
937        input.parse::<Ident>()?;
938        input.parse::<Token![<=]>()?;
939        let _: PredicateValue = parse_predicate_value(input)?;
940
941        // <= is sugar for !(signal > val)
942        return match val {
943            PredicateValue::Const(expr) => Ok(StlFormula::Not(Box::new(StlFormula::GreaterThan(
944                signal, expr,
945            )))),
946            PredicateValue::Var(var_ident) => Ok(StlFormula::Not(Box::new(
947                StlFormula::GreaterThanVar(signal, var_ident),
948            ))),
949        };
950    }
951
952    if fork.peek(Token![==]) {
953        fork.parse::<Token![==]>()?;
954        let val = parse_predicate_value(&fork).map_err(|_| {
955            syn::Error::new(
956                fork.span(),
957                format!(
958                    "invalid value after '==' in predicate\n  \
959                    help: expected a numeric value, e.g., `{} == 5` or `{} == $threshold`",
960                    signal_str, signal_str
961                ),
962            )
963        })?;
964
965        // Commit the parse
966        input.parse::<Ident>()?;
967        input.parse::<Token![==]>()?;
968        let _: PredicateValue = parse_predicate_value(input)?;
969
970        // == is sugar for (signal >= val) && (signal <= val)
971        // Which is: !(signal < val) && !(signal > val)
972        return match val {
973            PredicateValue::Const(expr) => {
974                let gte =
975                    StlFormula::Not(Box::new(StlFormula::LessThan(signal.clone(), expr.clone())));
976                let lte = StlFormula::Not(Box::new(StlFormula::GreaterThan(signal, expr)));
977                Ok(StlFormula::And(Box::new(gte), Box::new(lte)))
978            }
979            PredicateValue::Var(var_ident) => {
980                let gte = StlFormula::Not(Box::new(StlFormula::LessThanVar(
981                    signal.clone(),
982                    var_ident.clone(),
983                )));
984                let lte = StlFormula::Not(Box::new(StlFormula::GreaterThanVar(signal, var_ident)));
985                Ok(StlFormula::And(Box::new(gte), Box::new(lte)))
986            }
987        };
988    }
989
990    Err(syn::Error::new(
991        signal.span(),
992        format!(
993            "expected comparison operator after signal '{}'\n  \
994            help: predicates require a comparison: `{} > value`, `{} < value`, `{} >= value`, `{} <= value`, or `{} == value`",
995            signal_str, signal_str, signal_str, signal_str, signal_str, signal_str
996        ),
997    ))
998}
999
1000/// Parse a predicate value - stops at binary operators to avoid consuming them
1001/// Returns either a constant expression or a variable reference ($var)
1002fn parse_predicate_value(input: ParseStream) -> Result<PredicateValue> {
1003    // We need to parse a numeric literal or expression, but stop before binary STL operators
1004    // Use syn's expression parsing but be careful with what we consume
1005
1006    // Check for variable reference with $ prefix: $threshold
1007    if input.peek(Token![$]) {
1008        input.parse::<Token![$]>()?;
1009        if !input.peek(Ident) {
1010            return Err(syn::Error::new(
1011                input.span(),
1012                "expected identifier after '$'\n  \
1013                help: variable references should be written as `$variable_name`, e.g., `x > $threshold`",
1014            ));
1015        }
1016        let var_ident: Ident = input.parse()?;
1017        return Ok(PredicateValue::Var(var_ident));
1018    }
1019
1020    // Check for negative numbers: -5, -3.14, etc.
1021    if input.peek(Token![-]) {
1022        let neg: Token![-] = input.parse()?;
1023        if input.peek(syn::LitInt) {
1024            let lit: syn::LitInt = input.parse()?;
1025            return Ok(PredicateValue::Const(
1026                syn::parse_quote_spanned!(neg.span=> -#lit),
1027            ));
1028        }
1029        if input.peek(syn::LitFloat) {
1030            let lit: syn::LitFloat = input.parse()?;
1031            return Ok(PredicateValue::Const(
1032                syn::parse_quote_spanned!(neg.span=> -#lit),
1033            ));
1034        }
1035        // Parenthesized negative expression
1036        if input.peek(syn::token::Paren) {
1037            let content;
1038            parenthesized!(content in input);
1039            let inner: Expr = content.parse()?;
1040            return Ok(PredicateValue::Const(
1041                syn::parse_quote_spanned!(neg.span=> -(#inner)),
1042            ));
1043        }
1044        return Err(syn::Error::new(
1045            neg.span,
1046            "invalid negative value\n  \
1047            help: expected a number after '-', e.g., `-5`, `-3.14`, or `-(expr)`",
1048        ));
1049    }
1050
1051    // Simple literals
1052    if input.peek(syn::LitInt) {
1053        let lit: syn::LitInt = input.parse()?;
1054        return Ok(PredicateValue::Const(Expr::Lit(syn::ExprLit {
1055            attrs: vec![],
1056            lit: syn::Lit::Int(lit),
1057        })));
1058    }
1059
1060    if input.peek(syn::LitFloat) {
1061        let lit: syn::LitFloat = input.parse()?;
1062        return Ok(PredicateValue::Const(Expr::Lit(syn::ExprLit {
1063            attrs: vec![],
1064            lit: syn::Lit::Float(lit),
1065        })));
1066    }
1067
1068    // Parenthesized expression for the value
1069    if input.peek(syn::token::Paren) {
1070        let content;
1071        parenthesized!(content in input);
1072        if content.is_empty() {
1073            return Err(content.error(
1074                "empty parentheses in value position\n  \
1075                help: expected an expression inside parentheses, e.g., `(x + 1)`",
1076            ));
1077        }
1078        let inner: Expr = content.parse()?;
1079        return Ok(PredicateValue::Const(syn::parse_quote!((#inner))));
1080    }
1081
1082    // Variable reference (identifier)
1083    if input.peek(Ident) {
1084        let ident: Ident = input.parse()?;
1085        let ident_str = ident.to_string();
1086
1087        // Check if this looks like an STL keyword used in value position
1088        if matches!(
1089            ident_str.as_str(),
1090            "and"
1091                | "or"
1092                | "implies"
1093                | "not"
1094                | "G"
1095                | "F"
1096                | "U"
1097                | "globally"
1098                | "eventually"
1099                | "until"
1100        ) {
1101            return Err(syn::Error::new(
1102                ident.span(),
1103                format!(
1104                    "'{}' is an STL keyword and cannot be used as a value\n  \
1105                    help: did you forget the comparison value? e.g., `signal > 5 {} ...`",
1106                    ident_str, ident_str
1107                ),
1108            ));
1109        }
1110
1111        return Ok(PredicateValue::Const(Expr::Path(syn::ExprPath {
1112            attrs: vec![],
1113            qself: None,
1114            path: ident.into(),
1115        })));
1116    }
1117
1118    Err(syn::Error::new(
1119        input.span(),
1120        "expected a value (number, variable, $var reference, or parenthesized expression)\n  \
1121        help: valid values include: `5`, `3.14`, `-10`, `threshold`, `$threshold`, `(x + 1)`",
1122    ))
1123}
mstlo_macros/lib.rs

mstlo_macros/
lib.rs
