Skip to main content

scarf_syntax/behavioral_statements/
assertion_statements.rs

1// =======================================================================
2// assertion_statements.rs
3// =======================================================================
4//! CST Nodes from 1800-2023 A.6.10
5use crate::*;
6
7#[derive(Clone, Debug, PartialEq)]
8pub enum AssertionItem<'a> {
9    Concurrent(Box<ConcurrentAssertionItem<'a>>),
10    DeferredImmediate(Box<DeferredImmediateAssertionItem<'a>>),
11}
12
13#[derive(Clone, Debug, PartialEq)]
14pub struct DeferredImmediateAssertionItem<'a>(
15    pub  Option<(
16        BlockIdentifier<'a>,
17        Metadata<'a>, // ;
18    )>,
19    pub DeferredImmediateAssertionStatement<'a>,
20);
21
22#[derive(Clone, Debug, PartialEq)]
23pub enum ProceduralAssertionStatement<'a> {
24    Concurrent(Box<ConcurrentAssertionStatement<'a>>),
25    Immediate(Box<ImmediateAssertionStatement<'a>>),
26    Checker(Box<CheckerInstantiation<'a>>),
27}
28
29#[derive(Clone, Debug, PartialEq)]
30pub enum ImmediateAssertionStatement<'a> {
31    Simple(Box<SimpleImmediateAssertionStatement<'a>>),
32    Deferred(Box<DeferredImmediateAssertionStatement<'a>>),
33}
34
35#[derive(Clone, Debug, PartialEq)]
36pub enum SimpleImmediateAssertionStatement<'a> {
37    Assert(Box<SimpleImmediateAssertStatement<'a>>),
38    Assume(Box<SimpleImmediateAssumeStatement<'a>>),
39    Cover(Box<SimpleImmediateCoverStatement<'a>>),
40}
41
42#[derive(Clone, Debug, PartialEq)]
43pub enum DeferredImmediateAssertionStatement<'a> {
44    Assert(Box<DeferredImmediateAssertStatement<'a>>),
45    Assume(Box<DeferredImmediateAssumeStatement<'a>>),
46    Cover(Box<DeferredImmediateCoverStatement<'a>>),
47}
48
49#[derive(Clone, Debug, PartialEq)]
50pub struct SimpleImmediateAssertStatement<'a>(
51    pub Metadata<'a>, // assert
52    pub Metadata<'a>, // (
53    pub Expression<'a>,
54    pub Metadata<'a>, // )
55    pub ActionBlock<'a>,
56);
57
58#[derive(Clone, Debug, PartialEq)]
59pub struct SimpleImmediateAssumeStatement<'a>(
60    pub Metadata<'a>, // assume
61    pub Metadata<'a>, // (
62    pub Expression<'a>,
63    pub Metadata<'a>, // )
64    pub ActionBlock<'a>,
65);
66
67#[derive(Clone, Debug, PartialEq)]
68pub struct SimpleImmediateCoverStatement<'a>(
69    pub Metadata<'a>, // cover
70    pub Metadata<'a>, // (
71    pub Expression<'a>,
72    pub Metadata<'a>, // )
73    pub StatementOrNull<'a>,
74);
75
76#[derive(Clone, Debug, PartialEq)]
77pub enum DeferredImmediateAssertStatement<'a> {
78    Now(
79        Box<(
80            Metadata<'a>, // assert
81            Metadata<'a>, // #
82            Metadata<'a>, // 0
83            Metadata<'a>, // (
84            Expression<'a>,
85            Metadata<'a>, // )
86            ActionBlock<'a>,
87        )>,
88    ),
89    Final(
90        Box<(
91            Metadata<'a>, // assert
92            Metadata<'a>, // final
93            Metadata<'a>, // (
94            Expression<'a>,
95            Metadata<'a>, // )
96            ActionBlock<'a>,
97        )>,
98    ),
99}
100
101#[derive(Clone, Debug, PartialEq)]
102pub enum DeferredImmediateAssumeStatement<'a> {
103    Now(
104        Box<(
105            Metadata<'a>, // assume
106            Metadata<'a>, // #
107            Metadata<'a>, // 0
108            Metadata<'a>, // (
109            Expression<'a>,
110            Metadata<'a>, // )
111            ActionBlock<'a>,
112        )>,
113    ),
114    Final(
115        Box<(
116            Metadata<'a>, // assume
117            Metadata<'a>, // final
118            Metadata<'a>, // (
119            Expression<'a>,
120            Metadata<'a>, // )
121            ActionBlock<'a>,
122        )>,
123    ),
124}
125
126#[derive(Clone, Debug, PartialEq)]
127pub enum DeferredImmediateCoverStatement<'a> {
128    Now(
129        Box<(
130            Metadata<'a>, // cover
131            Metadata<'a>, // #
132            Metadata<'a>, // 0
133            Metadata<'a>, // (
134            Expression<'a>,
135            Metadata<'a>, // )
136            StatementOrNull<'a>,
137        )>,
138    ),
139    Final(
140        Box<(
141            Metadata<'a>, // cover
142            Metadata<'a>, // final
143            Metadata<'a>, // (
144            Expression<'a>,
145            Metadata<'a>, // )
146            StatementOrNull<'a>,
147        )>,
148    ),
149}