1#[derive(Debug, Clone, PartialEq, Eq)]
3pub struct Span {
4 pub start: usize,
5 pub end: usize,
6}
7
8impl Span {
9 pub fn new(start: usize, end: usize) -> Self {
10 Self { start, end }
11 }
12
13 pub fn merge(&self, other: &Span) -> Span {
14 Span {
15 start: self.start.min(other.start),
16 end: self.end.max(other.end),
17 }
18 }
19}
20
21#[derive(Debug, Clone)]
23pub struct Spanned<T> {
24 pub node: T,
25 pub span: Span,
26}
27
28impl<T> Spanned<T> {
29 pub fn new(node: T, span: Span) -> Self {
30 Self { node, span }
31 }
32}
33
34#[derive(Debug, Clone)]
37pub struct Program {
38 pub declarations: Vec<Spanned<Declaration>>,
39}
40
41#[derive(Debug, Clone)]
42pub enum Declaration {
43 Import(ImportDecl),
44 Type(TypeDecl),
45 Enum(EnumDecl),
46 Function(FunctionDecl),
47 Intent(IntentDecl),
48 Safety(SafetyDecl),
49 Theorem(TheoremDecl),
50 Axiom(AxiomDecl),
51 Goal(GoalDecl),
53 Coverage(CoverageDecl),
55}
56
57#[derive(Debug, Clone)]
60pub enum ImportPath {
61 Plugin(Vec<String>),
63 File(String),
65}
66
67#[derive(Debug, Clone)]
68pub struct ImportDecl {
69 pub path: ImportPath,
70 pub alias: Option<String>,
71}
72
73#[derive(Debug, Clone)]
74pub struct TypeDecl {
75 pub name: String,
76 pub type_params: Vec<String>,
77 pub fields: Vec<Field>,
78}
79
80#[derive(Debug, Clone)]
81pub struct Field {
82 pub name: String,
83 pub ty: TypeExpr,
84}
85
86#[derive(Debug, Clone)]
87pub struct EnumDecl {
88 pub name: String,
89 pub variants: Vec<String>,
90}
91
92#[derive(Debug, Clone)]
93pub struct FunctionDecl {
94 pub name: String,
95 pub params: Vec<Param>,
96 pub return_type: TypeExpr,
97 pub body: Spanned<Expr>,
98}
99
100#[derive(Debug, Clone)]
101pub struct Param {
102 pub name: String,
103 pub ty: TypeExpr,
104}
105
106#[derive(Debug, Clone)]
107pub struct IntentDecl {
108 pub name: String,
109 pub annotations: Vec<Annotation>,
110 pub params: Vec<Param>,
111 pub clauses: Vec<Spanned<Clause>>,
112}
113
114#[derive(Debug, Clone)]
115pub enum Clause {
116 Require(Spanned<Expr>),
117 Ensure(Spanned<Expr>),
118 Invariant(Spanned<Expr>),
119}
120
121#[derive(Debug, Clone)]
122pub struct SafetyDecl {
123 pub name: String,
124 pub params: Vec<Param>,
125 pub invariants: Vec<Spanned<Expr>>,
126}
127
128#[derive(Debug, Clone)]
129pub struct TheoremDecl {
130 pub name: String,
131 pub body: Spanned<Expr>,
132}
133
134#[derive(Debug, Clone)]
135pub struct AxiomDecl {
136 pub name: String,
137 pub body: Spanned<Expr>,
138}
139
140#[derive(Debug, Clone)]
141pub struct GoalDecl {
142 pub name: String,
144 pub rationale: Option<String>,
145 pub stakeholder: Vec<String>,
147 pub measure: Option<String>,
148 pub realized_by: Vec<String>,
150}
151
152#[derive(Debug, Clone)]
153pub struct CoverageDecl {
154 pub name: String,
156 pub dimensions: Vec<CoverageDim>,
158}
159
160#[derive(Debug, Clone)]
161pub struct CoverageDim {
162 pub name: String,
163 pub values: Vec<Spanned<Expr>>,
164}
165
166#[derive(Debug, Clone)]
167pub struct Annotation {
168 pub name: String,
169 pub args: Vec<AnnotationArg>,
170}
171
172#[derive(Debug, Clone)]
173pub enum AnnotationArg {
174 Positional(Spanned<Expr>),
175 Named(String, Spanned<Expr>),
176}
177
178#[derive(Debug, Clone, PartialEq, Eq)]
181pub enum TypeExpr {
182 Named(String),
183 Qualified(String, String),
185 Generic(String, Vec<TypeExpr>),
186}
187
188impl std::fmt::Display for TypeExpr {
189 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
190 match self {
191 TypeExpr::Named(n) => write!(f, "{n}"),
192 TypeExpr::Qualified(module, name) => write!(f, "{module}.{name}"),
193 TypeExpr::Generic(n, args) => {
194 write!(f, "{n}<")?;
195 for (i, a) in args.iter().enumerate() {
196 if i > 0 {
197 write!(f, ", ")?;
198 }
199 write!(f, "{a}")?;
200 }
201 write!(f, ">")
202 }
203 }
204 }
205}
206
207#[derive(Debug, Clone)]
210pub enum Expr {
211 IntLit(i64),
212 BoolLit(bool),
213 StringLit(String),
214
215 Ident(String),
216
217 Prime(Box<Spanned<Expr>>),
219
220 FieldAccess(Box<Spanned<Expr>>, String),
222
223 Index(Box<Spanned<Expr>>, Box<Spanned<Expr>>),
225
226 BinOp(Box<Spanned<Expr>>, BinOp, Box<Spanned<Expr>>),
227 UnaryOp(UnaryOp, Box<Spanned<Expr>>),
228
229 IfThenElse(Box<Spanned<Expr>>, Box<Spanned<Expr>>, Box<Spanned<Expr>>),
231
232 Forall(Vec<TypedVar>, Box<Spanned<Expr>>),
234 Exists(Vec<TypedVar>, Box<Spanned<Expr>>),
236
237 Call(String, Vec<Spanned<Expr>>),
239
240 Paren(Box<Spanned<Expr>>),
241}
242
243#[derive(Debug, Clone)]
244pub struct TypedVar {
245 pub name: String,
246 pub ty: TypeExpr,
247}
248
249#[derive(Debug, Clone, Copy, PartialEq, Eq)]
250pub enum BinOp {
251 Add,
252 Sub,
253 Mul,
254 Div,
255 Mod,
256 Eq,
257 Neq,
258 Lt,
259 Le,
260 Gt,
261 Ge,
262 And,
263 Or,
264 Implies,
265}
266
267impl std::fmt::Display for BinOp {
268 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
269 match self {
270 BinOp::Add => write!(f, "+"),
271 BinOp::Sub => write!(f, "-"),
272 BinOp::Mul => write!(f, "*"),
273 BinOp::Div => write!(f, "/"),
274 BinOp::Mod => write!(f, "%"),
275 BinOp::Eq => write!(f, "=="),
276 BinOp::Neq => write!(f, "!="),
277 BinOp::Lt => write!(f, "<"),
278 BinOp::Le => write!(f, "<="),
279 BinOp::Gt => write!(f, ">"),
280 BinOp::Ge => write!(f, ">="),
281 BinOp::And => write!(f, "&&"),
282 BinOp::Or => write!(f, "||"),
283 BinOp::Implies => write!(f, "==>"),
284 }
285 }
286}
287
288#[derive(Debug, Clone, Copy, PartialEq, Eq)]
289pub enum UnaryOp {
290 Not,
291 Neg,
292}