Skip to main content

intent_render/
html.rs

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