scarf_syntax/behavioral_statements/
assertion_statements.rs1use 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>, )>,
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>, pub Metadata<'a>, pub Expression<'a>,
54 pub Metadata<'a>, pub ActionBlock<'a>,
56);
57
58#[derive(Clone, Debug, PartialEq)]
59pub struct SimpleImmediateAssumeStatement<'a>(
60 pub Metadata<'a>, pub Metadata<'a>, pub Expression<'a>,
63 pub Metadata<'a>, pub ActionBlock<'a>,
65);
66
67#[derive(Clone, Debug, PartialEq)]
68pub struct SimpleImmediateCoverStatement<'a>(
69 pub Metadata<'a>, pub Metadata<'a>, pub Expression<'a>,
72 pub Metadata<'a>, pub StatementOrNull<'a>,
74);
75
76#[derive(Clone, Debug, PartialEq)]
77pub enum DeferredImmediateAssertStatement<'a> {
78 Now(
79 Box<(
80 Metadata<'a>, Metadata<'a>, Metadata<'a>, Metadata<'a>, Expression<'a>,
85 Metadata<'a>, ActionBlock<'a>,
87 )>,
88 ),
89 Final(
90 Box<(
91 Metadata<'a>, Metadata<'a>, Metadata<'a>, Expression<'a>,
95 Metadata<'a>, ActionBlock<'a>,
97 )>,
98 ),
99}
100
101#[derive(Clone, Debug, PartialEq)]
102pub enum DeferredImmediateAssumeStatement<'a> {
103 Now(
104 Box<(
105 Metadata<'a>, Metadata<'a>, Metadata<'a>, Metadata<'a>, Expression<'a>,
110 Metadata<'a>, ActionBlock<'a>,
112 )>,
113 ),
114 Final(
115 Box<(
116 Metadata<'a>, Metadata<'a>, Metadata<'a>, Expression<'a>,
120 Metadata<'a>, ActionBlock<'a>,
122 )>,
123 ),
124}
125
126#[derive(Clone, Debug, PartialEq)]
127pub enum DeferredImmediateCoverStatement<'a> {
128 Now(
129 Box<(
130 Metadata<'a>, Metadata<'a>, Metadata<'a>, Metadata<'a>, Expression<'a>,
135 Metadata<'a>, StatementOrNull<'a>,
137 )>,
138 ),
139 Final(
140 Box<(
141 Metadata<'a>, Metadata<'a>, Metadata<'a>, Expression<'a>,
145 Metadata<'a>, StatementOrNull<'a>,
147 )>,
148 ),
149}