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 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> ⇒ <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> ⇒ <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
150fn 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
240fn esc(s: &str) -> String {
243 s.replace('&', "&")
244 .replace('<', "<")
245 .replace('>', ">")
246 .replace('"', """)
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; }";