Skip to main content

intent_lang_syntax/
ast.rs

1/// Source span for error reporting.
2#[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/// A node wrapping a value with its source span.
22#[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// ── Program ──────────────────────────────────────────────────
35
36#[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 "name" { rationale: ...; stakeholder: ...; measure: ...; realized_by: [...] }`
52    Goal(GoalDecl),
53    /// `coverage "name" { dimensions: { d1: [...]; d2: [...] } }`
54    Coverage(CoverageDecl),
55}
56
57// ── Declarations ─────────────────────────────────────────────
58
59#[derive(Debug, Clone)]
60pub enum ImportPath {
61    /// Plugin import: `import smarthome` or `import finance.currency`
62    Plugin(Vec<String>),
63    /// File import: `import "./path/to/file.intent"`
64    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    /// Human-readable goal name (a string literal)
143    pub name: String,
144    pub rationale: Option<String>,
145    /// Free-form list of stakeholder labels (e.g., "compliance", "finance")
146    pub stakeholder: Vec<String>,
147    pub measure: Option<String>,
148    /// Identifier names of safety/intent declarations that realize this goal
149    pub realized_by: Vec<String>,
150}
151
152#[derive(Debug, Clone)]
153pub struct CoverageDecl {
154    /// Human-readable coverage scenario name (a string literal)
155    pub name: String,
156    /// Each dimension: (name, list of values as expressions — usually idents/lits)
157    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// ── Types ────────────────────────────────────────────────────
179
180#[derive(Debug, Clone, PartialEq, Eq)]
181pub enum TypeExpr {
182    Named(String),
183    /// `module.TypeName` — qualified type reference
184    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// ── Expressions ──────────────────────────────────────────────
208
209#[derive(Debug, Clone)]
210pub enum Expr {
211    IntLit(i64),
212    BoolLit(bool),
213    StringLit(String),
214
215    Ident(String),
216
217    /// `x'` or `after(x)` — post-execution value
218    Prime(Box<Spanned<Expr>>),
219
220    /// `expr.field`
221    FieldAccess(Box<Spanned<Expr>>, String),
222
223    /// `expr[index]`
224    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    /// `if cond then a else b`
230    IfThenElse(Box<Spanned<Expr>>, Box<Spanned<Expr>>, Box<Spanned<Expr>>),
231
232    /// `forall vars, body`
233    Forall(Vec<TypedVar>, Box<Spanned<Expr>>),
234    /// `exists vars, body`
235    Exists(Vec<TypedVar>, Box<Spanned<Expr>>),
236
237    /// `name(args)`
238    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}