1use intent_parser::ast;
4
5use crate::format_type;
6
7pub fn render(file: &ast::File) -> String {
9 let mut body = String::new();
10 body.push_str(&format!("<h1>{}</h1>\n", esc(&file.module.name)));
11
12 if let Some(doc) = &file.doc {
13 body.push_str("<p class=\"doc\">");
14 body.push_str(&esc(&doc.lines.join(" ")));
15 body.push_str("</p>\n");
16 }
17
18 if !file.imports.is_empty() {
19 body.push_str("<section class=\"imports\">\n<h2>Imports</h2>\n<ul>\n");
20 for use_decl in &file.imports {
21 if let Some(item) = &use_decl.item {
22 body.push_str(&format!(
23 "<li><code>{}.{}</code></li>\n",
24 esc(&use_decl.module_name),
25 esc(item)
26 ));
27 } else {
28 body.push_str(&format!(
29 "<li><code>{}</code></li>\n",
30 esc(&use_decl.module_name)
31 ));
32 }
33 }
34 body.push_str("</ul>\n</section>\n");
35 }
36
37 for item in &file.items {
38 match item {
39 ast::TopLevelItem::Entity(e) => render_entity(&mut body, e),
40 ast::TopLevelItem::Action(a) => render_action(&mut body, a),
41 ast::TopLevelItem::Invariant(i) => render_invariant(&mut body, i),
42 ast::TopLevelItem::EdgeCases(ec) => render_edge_cases(&mut body, ec),
43 }
44 }
45
46 format!(
47 "<!DOCTYPE html>\n<html lang=\"en\">\n<head>\n<meta charset=\"utf-8\">\n\
48 <title>{title}</title>\n<style>\n{css}\n</style>\n</head>\n\
49 <body>\n{body}</body>\n</html>\n",
50 title = esc(&file.module.name),
51 css = CSS,
52 body = body,
53 )
54}
55
56fn render_entity(out: &mut String, entity: &ast::EntityDecl) {
57 out.push_str(&format!(
58 "<section class=\"entity\">\n<h2>Entity: {}</h2>\n",
59 esc(&entity.name)
60 ));
61 render_doc(out, &entity.doc);
62 if !entity.fields.is_empty() {
63 out.push_str("<table>\n<thead><tr><th>Field</th><th>Type</th></tr></thead>\n<tbody>\n");
64 for field in &entity.fields {
65 out.push_str(&format!(
66 "<tr><td><code>{}</code></td><td><code>{}</code></td></tr>\n",
67 esc(&field.name),
68 esc(&format_type(&field.ty))
69 ));
70 }
71 out.push_str("</tbody>\n</table>\n");
72 }
73 out.push_str("</section>\n");
74}
75
76fn render_action(out: &mut String, action: &ast::ActionDecl) {
77 out.push_str(&format!(
78 "<section class=\"action\">\n<h2>Action: {}</h2>\n",
79 esc(&action.name)
80 ));
81 render_doc(out, &action.doc);
82 if !action.params.is_empty() {
83 out.push_str("<h3>Parameters</h3>\n<ul>\n");
84 for p in &action.params {
85 out.push_str(&format!(
86 "<li><code>{}</code>: <code>{}</code></li>\n",
87 esc(&p.name),
88 esc(&format_type(&p.ty))
89 ));
90 }
91 out.push_str("</ul>\n");
92 }
93 if let Some(req) = &action.requires {
94 out.push_str("<h3>Requires</h3>\n<ul class=\"constraints\">\n");
95 for cond in &req.conditions {
96 out.push_str(&format!(
97 "<li><code>{}</code></li>\n",
98 esc(&format_expr(cond))
99 ));
100 }
101 out.push_str("</ul>\n");
102 }
103 if let Some(ens) = &action.ensures {
104 out.push_str("<h3>Ensures</h3>\n<ul class=\"constraints\">\n");
105 for item in &ens.items {
106 match item {
107 ast::EnsuresItem::Expr(e) => {
108 out.push_str(&format!("<li><code>{}</code></li>\n", esc(&format_expr(e))));
109 }
110 ast::EnsuresItem::When(w) => {
111 out.push_str(&format!(
112 "<li>when <code>{}</code> ⇒ <code>{}</code></li>\n",
113 esc(&format_expr(&w.condition)),
114 esc(&format_expr(&w.consequence))
115 ));
116 }
117 }
118 }
119 out.push_str("</ul>\n");
120 }
121 if let Some(props) = &action.properties {
122 out.push_str("<h3>Properties</h3>\n<table>\n<thead><tr><th>Key</th><th>Value</th></tr></thead>\n<tbody>\n");
123 for entry in &props.entries {
124 out.push_str(&format!(
125 "<tr><td><code>{}</code></td><td><code>{}</code></td></tr>\n",
126 esc(&entry.key),
127 esc(&format_prop_value(&entry.value))
128 ));
129 }
130 out.push_str("</tbody>\n</table>\n");
131 }
132 out.push_str("</section>\n");
133}
134
135fn render_invariant(out: &mut String, inv: &ast::InvariantDecl) {
136 out.push_str(&format!(
137 "<section class=\"invariant\">\n<h2>Invariant: {}</h2>\n",
138 esc(&inv.name)
139 ));
140 render_doc(out, &inv.doc);
141 out.push_str(&format!(
142 "<pre><code>{}</code></pre>\n",
143 esc(&format_expr(&inv.body))
144 ));
145 out.push_str("</section>\n");
146}
147
148fn render_edge_cases(out: &mut String, ec: &ast::EdgeCasesDecl) {
149 out.push_str("<section class=\"edge-cases\">\n<h2>Edge Cases</h2>\n<ul>\n");
150 for rule in &ec.rules {
151 out.push_str(&format!(
152 "<li>when <code>{}</code> ⇒ <code>{}({})</code></li>\n",
153 esc(&format_expr(&rule.condition)),
154 esc(&rule.action.name),
155 esc(&format_call_args(&rule.action.args))
156 ));
157 }
158 out.push_str("</ul>\n</section>\n");
159}
160
161fn render_doc(out: &mut String, doc: &Option<ast::DocBlock>) {
162 if let Some(d) = doc {
163 out.push_str("<p class=\"doc\">");
164 out.push_str(&esc(&d.lines.join(" ")));
165 out.push_str("</p>\n");
166 }
167}
168
169fn format_expr(expr: &ast::Expr) -> String {
172 match &expr.kind {
173 ast::ExprKind::Implies(l, r) => format!("{} => {}", format_expr(l), format_expr(r)),
174 ast::ExprKind::Or(l, r) => format!("{} || {}", format_expr(l), format_expr(r)),
175 ast::ExprKind::And(l, r) => format!("{} && {}", format_expr(l), format_expr(r)),
176 ast::ExprKind::Not(e) => format!("!{}", format_expr(e)),
177 ast::ExprKind::Compare { left, op, right } => {
178 let op_str = match op {
179 ast::CmpOp::Eq => "==",
180 ast::CmpOp::Ne => "!=",
181 ast::CmpOp::Lt => "<",
182 ast::CmpOp::Gt => ">",
183 ast::CmpOp::Le => "<=",
184 ast::CmpOp::Ge => ">=",
185 };
186 format!("{} {} {}", format_expr(left), op_str, format_expr(right))
187 }
188 ast::ExprKind::Arithmetic { left, op, right } => {
189 let op_str = match op {
190 ast::ArithOp::Add => "+",
191 ast::ArithOp::Sub => "-",
192 };
193 format!("{} {} {}", format_expr(left), op_str, format_expr(right))
194 }
195 ast::ExprKind::Old(e) => format!("old({})", format_expr(e)),
196 ast::ExprKind::Quantifier {
197 kind,
198 binding,
199 ty,
200 body,
201 } => {
202 let kw = match kind {
203 ast::QuantifierKind::Forall => "forall",
204 ast::QuantifierKind::Exists => "exists",
205 };
206 format!("{} {}: {} => {}", kw, binding, ty, format_expr(body))
207 }
208 ast::ExprKind::Call { name, args } => {
209 format!("{}({})", name, format_call_args(args))
210 }
211 ast::ExprKind::FieldAccess { root, fields } => {
212 format!("{}.{}", format_expr(root), fields.join("."))
213 }
214 ast::ExprKind::List(items) => {
215 let inner: Vec<_> = items.iter().map(format_expr).collect();
216 format!("[{}]", inner.join(", "))
217 }
218 ast::ExprKind::Ident(name) => name.clone(),
219 ast::ExprKind::Literal(lit) => format_literal(lit),
220 }
221}
222
223fn format_literal(lit: &ast::Literal) -> String {
224 match lit {
225 ast::Literal::Null => "null".to_string(),
226 ast::Literal::Bool(b) => b.to_string(),
227 ast::Literal::Int(n) => n.to_string(),
228 ast::Literal::Decimal(s) => s.clone(),
229 ast::Literal::String(s) => format!("\"{}\"", s),
230 }
231}
232
233fn format_call_args(args: &[ast::CallArg]) -> String {
234 args.iter()
235 .map(|a| match a {
236 ast::CallArg::Named { key, value, .. } => {
237 format!("{}: {}", key, format_expr(value))
238 }
239 ast::CallArg::Positional(e) => format_expr(e),
240 })
241 .collect::<Vec<_>>()
242 .join(", ")
243}
244
245fn format_prop_value(val: &ast::PropValue) -> String {
246 match val {
247 ast::PropValue::Literal(lit) => format_literal(lit),
248 ast::PropValue::Ident(name) => name.clone(),
249 ast::PropValue::List(items) => {
250 let inner: Vec<String> = items.iter().map(format_prop_value).collect();
251 format!("[{}]", inner.join(", "))
252 }
253 ast::PropValue::Object(fields) => {
254 let inner: Vec<String> = fields
255 .iter()
256 .map(|(k, v)| format!("{}: {}", k, format_prop_value(v)))
257 .collect();
258 format!("{{{}}}", inner.join(", "))
259 }
260 }
261}
262
263fn esc(s: &str) -> String {
266 s.replace('&', "&")
267 .replace('<', "<")
268 .replace('>', ">")
269 .replace('"', """)
270}
271
272const CSS: &str = "\
273body { font-family: system-ui, -apple-system, sans-serif; max-width: 48rem; margin: 2rem auto; padding: 0 1rem; color: #1a1a1a; line-height: 1.6; }
274h1 { border-bottom: 2px solid #333; padding-bottom: 0.3rem; }
275h2 { margin-top: 2rem; color: #2c5282; }
276h3 { color: #555; }
277.doc { color: #555; font-style: italic; }
278table { border-collapse: collapse; width: 100%; margin: 0.5rem 0; }
279th, td { border: 1px solid #ddd; padding: 0.4rem 0.8rem; text-align: left; }
280th { background: #f7f7f7; }
281code { background: #f5f5f5; padding: 0.1rem 0.3rem; border-radius: 3px; font-size: 0.9em; }
282pre { background: #f5f5f5; padding: 1rem; border-radius: 4px; overflow-x: auto; }
283pre code { background: none; padding: 0; }
284ul.constraints { list-style: none; padding-left: 1rem; }
285ul.constraints li::before { content: '\\2713 '; color: #38a169; }
286section { margin-bottom: 1.5rem; }
287.entity { border-left: 3px solid #3182ce; padding-left: 1rem; }
288.action { border-left: 3px solid #d69e2e; padding-left: 1rem; }
289.invariant { border-left: 3px solid #38a169; padding-left: 1rem; }
290.edge-cases { border-left: 3px solid #e53e3e; padding-left: 1rem; }";