1use intent_parser::ast;
6
7use crate::format_type;
8
9pub fn format(file: &ast::File) -> String {
11 let mut out = String::new();
12 out.push_str(&format!("module {}\n", file.module.name));
13
14 if let Some(doc) = &file.doc {
15 out.push('\n');
16 for line in &doc.lines {
17 out.push_str(&format!("--- {}\n", line.trim()));
18 }
19 }
20
21 for use_decl in &file.imports {
22 out.push('\n');
23 if let Some(item) = &use_decl.item {
24 out.push_str(&format!("use {}.{}\n", use_decl.module_name, item));
25 } else {
26 out.push_str(&format!("use {}\n", use_decl.module_name));
27 }
28 }
29
30 for item in &file.items {
31 out.push('\n');
32 match item {
33 ast::TopLevelItem::Entity(e) => fmt_entity(&mut out, e),
34 ast::TopLevelItem::Action(a) => fmt_action(&mut out, a),
35 ast::TopLevelItem::Invariant(i) => fmt_invariant(&mut out, i),
36 ast::TopLevelItem::EdgeCases(ec) => fmt_edge_cases(&mut out, ec),
37 ast::TopLevelItem::Test(_) => {} }
39 }
40
41 out
42}
43
44fn fmt_doc(out: &mut String, doc: &Option<ast::DocBlock>) {
45 if let Some(doc) = doc {
46 for line in &doc.lines {
47 out.push_str(&format!(" --- {}\n", line.trim()));
48 }
49 out.push('\n');
50 }
51}
52
53fn fmt_entity(out: &mut String, entity: &ast::EntityDecl) {
54 out.push_str(&format!("entity {} {{\n", entity.name));
55 fmt_doc(out, &entity.doc);
56 for field in &entity.fields {
57 out.push_str(&format!(" {}: {}\n", field.name, format_type(&field.ty)));
58 }
59 out.push_str("}\n");
60}
61
62fn fmt_action(out: &mut String, action: &ast::ActionDecl) {
63 out.push_str(&format!("action {} {{\n", action.name));
64 fmt_doc(out, &action.doc);
65
66 for param in &action.params {
67 out.push_str(&format!(" {}: {}\n", param.name, format_type(¶m.ty)));
68 }
69
70 if let Some(req) = &action.requires {
71 out.push_str("\n requires {\n");
72 for cond in &req.conditions {
73 out.push_str(&format!(" {}\n", fmt_expr(cond)));
74 }
75 out.push_str(" }\n");
76 }
77
78 if let Some(ens) = &action.ensures {
79 out.push_str("\n ensures {\n");
80 for item in &ens.items {
81 match item {
82 ast::EnsuresItem::Expr(expr) => {
83 out.push_str(&format!(" {}\n", fmt_expr(expr)));
84 }
85 ast::EnsuresItem::When(w) => {
86 out.push_str(&format!(
87 " when {} => {}\n",
88 fmt_expr(&w.condition),
89 fmt_expr(&w.consequence)
90 ));
91 }
92 }
93 }
94 out.push_str(" }\n");
95 }
96
97 if let Some(props) = &action.properties {
98 out.push_str("\n properties {\n");
99 for entry in &props.entries {
100 out.push_str(&format!(
101 " {}: {}\n",
102 entry.key,
103 fmt_prop_value(&entry.value)
104 ));
105 }
106 out.push_str(" }\n");
107 }
108
109 out.push_str("}\n");
110}
111
112fn fmt_invariant(out: &mut String, inv: &ast::InvariantDecl) {
113 out.push_str(&format!("invariant {} {{\n", inv.name));
114 fmt_doc(out, &inv.doc);
115 out.push_str(&format!(" {}\n", fmt_expr(&inv.body)));
116 out.push_str("}\n");
117}
118
119fn fmt_edge_cases(out: &mut String, ec: &ast::EdgeCasesDecl) {
120 out.push_str("edge_cases {\n");
121 for rule in &ec.rules {
122 out.push_str(&format!(
123 " when {} => {}({})\n",
124 fmt_expr(&rule.condition),
125 rule.action.name,
126 fmt_call_args(&rule.action.args),
127 ));
128 }
129 out.push_str("}\n");
130}
131
132fn fmt_expr(expr: &ast::Expr) -> String {
133 match &expr.kind {
134 ast::ExprKind::Implies(l, r) => format!("{} => {}", fmt_expr(l), fmt_expr(r)),
135 ast::ExprKind::Or(l, r) => format!("{} || {}", fmt_expr(l), fmt_expr(r)),
136 ast::ExprKind::And(l, r) => format!("{} && {}", fmt_expr(l), fmt_expr(r)),
137 ast::ExprKind::Not(e) => format!("!{}", fmt_expr(e)),
138 ast::ExprKind::Compare { left, op, right } => {
139 let op_str = match op {
140 ast::CmpOp::Eq => "==",
141 ast::CmpOp::Ne => "!=",
142 ast::CmpOp::Lt => "<",
143 ast::CmpOp::Gt => ">",
144 ast::CmpOp::Le => "<=",
145 ast::CmpOp::Ge => ">=",
146 };
147 format!("{} {} {}", fmt_expr(left), op_str, fmt_expr(right))
148 }
149 ast::ExprKind::Arithmetic { left, op, right } => {
150 let op_str = match op {
151 ast::ArithOp::Add => "+",
152 ast::ArithOp::Sub => "-",
153 };
154 format!("{} {} {}", fmt_expr(left), op_str, fmt_expr(right))
155 }
156 ast::ExprKind::Old(e) => format!("old({})", fmt_expr(e)),
157 ast::ExprKind::Quantifier {
158 kind,
159 binding,
160 ty,
161 body,
162 } => {
163 let kw = match kind {
164 ast::QuantifierKind::Forall => "forall",
165 ast::QuantifierKind::Exists => "exists",
166 };
167 format!("{} {}: {} => {}", kw, binding, ty, fmt_expr(body))
168 }
169 ast::ExprKind::Call { name, args } => {
170 format!("{}({})", name, fmt_call_args(args))
171 }
172 ast::ExprKind::FieldAccess { root, fields } => {
173 format!("{}.{}", fmt_expr(root), fields.join("."))
174 }
175 ast::ExprKind::List(items) => {
176 let inner: Vec<_> = items.iter().map(fmt_expr).collect();
177 format!("[{}]", inner.join(", "))
178 }
179 ast::ExprKind::Ident(name) => name.clone(),
180 ast::ExprKind::Literal(lit) => fmt_literal(lit),
181 }
182}
183
184fn fmt_literal(lit: &ast::Literal) -> String {
185 match lit {
186 ast::Literal::Null => "null".to_string(),
187 ast::Literal::Bool(b) => b.to_string(),
188 ast::Literal::Int(n) => n.to_string(),
189 ast::Literal::Decimal(s) => s.clone(),
190 ast::Literal::String(s) => format!("\"{}\"", s),
191 }
192}
193
194fn fmt_call_args(args: &[ast::CallArg]) -> String {
195 args.iter()
196 .map(|a| match a {
197 ast::CallArg::Named { key, value, .. } => {
198 format!("{}: {}", key, fmt_expr(value))
199 }
200 ast::CallArg::Positional(e) => fmt_expr(e),
201 })
202 .collect::<Vec<_>>()
203 .join(", ")
204}
205
206fn fmt_prop_value(val: &ast::PropValue) -> String {
207 match val {
208 ast::PropValue::Literal(lit) => fmt_literal(lit),
209 ast::PropValue::Ident(s) => s.clone(),
210 ast::PropValue::List(items) => {
211 let inner: Vec<_> = items.iter().map(fmt_prop_value).collect();
212 format!("[{}]", inner.join(", "))
213 }
214 ast::PropValue::Object(fields) => {
215 let inner: Vec<_> = fields
216 .iter()
217 .map(|(k, v)| format!("{}: {}", k, fmt_prop_value(v)))
218 .collect();
219 format!("{{ {} }}", inner.join(", "))
220 }
221 }
222}