Skip to content

Commit ae87072

Browse files
lsarra-axlsarra-ax
committed
render statements
1 parent 9cc2aad commit ae87072

File tree

1 file changed

+224
-75
lines changed

1 file changed

+224
-75
lines changed

‎src/axiomatic/pic_helpers.py‎

Lines changed: 224 additions & 75 deletions
Original file line numberDiff line numberDiff line change
@@ -230,9 +230,11 @@ def print_statements(
230230
statements: StatementDictionary,
231231
validation: Optional[StatementValidationDictionary] = None,
232232
only_formalized: bool = False,
233+
pprint=True,
233234
):
234235
"""
235236
Print a list of statements in nice readable format.
237+
pprint enabled HTML rendering in Jupyter notebooks.
236238
"""
237239

238240
validation = StatementValidationDictionary(
@@ -255,88 +257,235 @@ def print_statements(
255257
if len(validation.unformalizable_statements or []) != len(statements.unformalizable_statements or []):
256258
raise ValueError("Number of unformalizable statements and validations do not match.")
257259

258-
print("-----------------------------------\n")
259-
for cost_stmt, cost_val in zip(statements.cost_functions or [], validation.cost_functions or []):
260-
if (cost_stmt.formalization is None or cost_stmt.formalization.mapping is None) and only_formalized:
261-
continue
262-
print("Type:", cost_stmt.type)
263-
print("Statement:", cost_stmt.text)
264-
print("Formalization:", end=" ")
265-
if cost_stmt.formalization is None:
266-
print("UNFORMALIZED")
267-
else:
268-
code = cost_stmt.formalization.code
269-
if cost_stmt.formalization.mapping is not None:
270-
for var_name, computation in cost_stmt.formalization.mapping.items():
271-
if computation is not None:
272-
args_str = ", ".join(
273-
[
260+
if pprint:
261+
# NOTE: the pprint code has been generated by Chattie by conversion from the HTML code below
262+
html_parts = []
263+
264+
# Start of HTML document
265+
html_parts.append("""
266+
<!DOCTYPE html>
267+
<html lang="en">
268+
<head>
269+
<meta charset="UTF-8">
270+
<meta name="viewport" content="width=device-width, initial-scale=1.0">
271+
<title>Validation Report</title>
272+
<style>
273+
body { font-family: Arial, sans-serif; padding: 20px; background-color: #f9f9f9; }
274+
.block { background-color: #fff; border: 1px solid #ddd; padding: 15px; margin-bottom: 20px; border-radius: 5px; }
275+
.block h2 { margin-top: 0; font-size: 1.2em; color: #333; }
276+
.block p { margin: 5px 0; color: #555; }
277+
.label { font-weight: bold; }
278+
.block code {
279+
background-color: #f4f4f4;
280+
border: 1px solid #ddd;
281+
padding: 2px 4px;
282+
border-radius: 3px;
283+
font-family: Consolas, "Courier New", monospace;
284+
font-size: 0.9em;
285+
color: #c7254e;
286+
background-color: #f9f2f4;
287+
}
288+
</style>
289+
</head>
290+
<body>
291+
<h1> Extracted statements </h1>
292+
""")
293+
294+
# Cost Functions Rendering
295+
for cost_stmt, cost_val in zip(statements.cost_functions or [], validation.cost_functions or []):
296+
if (cost_stmt.formalization is None or cost_stmt.formalization.mapping is None) and only_formalized:
297+
continue
298+
299+
html_parts.append('<div class="block">')
300+
html_parts.append(f"<h2>{cost_stmt.type}</h2>")
301+
html_parts.append(f'<p><span class="label">Statement:</span> {cost_stmt.text}</p>')
302+
html_parts.append('<p><span class="label">Formalization:</span> ')
303+
if cost_stmt.formalization is None:
304+
html_parts.append("UNFORMALIZED")
305+
else:
306+
code = cost_stmt.formalization.code
307+
if cost_stmt.formalization.mapping is not None:
308+
for var_name, computation in cost_stmt.formalization.mapping.items():
309+
if computation is not None:
310+
args_str = ", ".join(
274311
f"{argname}=" + (f"'{argvalue}'" if isinstance(argvalue, str) else str(argvalue))
275312
for argname, argvalue in computation.arguments.items()
276-
]
277-
)
278-
code = code.replace(var_name, f"{computation.name}({args_str})")
279-
print(code)
280-
val = cost_stmt.validation or cost_val
281-
if val.satisfiable is not None and val.message is not None:
282-
print(f"Satisfiable: {val.satisfiable}")
283-
print(val.message)
284-
print("\n-----------------------------------\n")
285-
for param_stmt, param_val in zip(statements.parameter_constraints or [], validation.parameter_constraints or []):
286-
if (param_stmt.formalization is None or param_stmt.formalization.mapping is None) and only_formalized:
287-
continue
288-
print("Type:", param_stmt.type)
289-
print("Statement:", param_stmt.text)
290-
print("Formalization:", end=" ")
291-
if param_stmt.formalization is None:
292-
print("UNFORMALIZED")
293-
else:
294-
code = param_stmt.formalization.code
295-
if param_stmt.formalization.mapping is not None:
296-
for var_name, computation in param_stmt.formalization.mapping.items():
297-
if computation is not None:
298-
args_str = ", ".join(
299-
[
313+
)
314+
code = code.replace(var_name, f"{computation.name}({args_str})")
315+
html_parts.append(f"<code>{code}</code>")
316+
html_parts.append("</p>")
317+
val = cost_stmt.validation or cost_val
318+
if val.satisfiable is not None and val.message is not None:
319+
html_parts.append(f'<p><span class="label">Satisfiable:</span> {val.satisfiable}</p>')
320+
html_parts.append(f"<p>{val.message}</p>")
321+
html_parts.append("</div>")
322+
323+
# Parameter Constraints Rendering
324+
for param_stmt, param_val in zip(
325+
statements.parameter_constraints or [], validation.parameter_constraints or []
326+
):
327+
if (param_stmt.formalization is None or param_stmt.formalization.mapping is None) and only_formalized:
328+
continue
329+
330+
html_parts.append('<div class="block">')
331+
html_parts.append(f"<h2>{param_stmt.type}</h2>")
332+
html_parts.append(f'<p><span class="label">Statement:</span> {param_stmt.text}</p>')
333+
html_parts.append('<p><span class="label">Formalization:</span> ')
334+
if param_stmt.formalization is None:
335+
html_parts.append("UNFORMALIZED")
336+
else:
337+
code = param_stmt.formalization.code
338+
if param_stmt.formalization.mapping is not None:
339+
for var_name, computation in param_stmt.formalization.mapping.items():
340+
if computation is not None:
341+
args_str = ", ".join(
300342
f"{argname}=" + (f"'{argvalue}'" if isinstance(argvalue, str) else str(argvalue))
301343
for argname, argvalue in computation.arguments.items()
302-
]
303-
)
304-
code = code.replace(var_name, f"{computation.name}({args_str})")
305-
print(code)
306-
val = param_stmt.validation or param_val
307-
if val.satisfiable is not None and val.message is not None and val.holds is not None:
308-
print(f"Satisfiable: {val.satisfiable}")
309-
print(f"Holds: {val.holds} ({val.message})")
310-
print("\n-----------------------------------\n")
311-
for struct_stmt, struct_val in zip(statements.structure_constraints or [], validation.structure_constraints or []):
312-
if struct_stmt.formalization is None and only_formalized:
313-
continue
314-
print("Type:", struct_stmt.type)
315-
print("Statement:", struct_stmt.text)
316-
print("Formalization:", end=" ")
317-
if struct_stmt.formalization is None:
318-
print("UNFORMALIZED")
319-
else:
320-
func_constr = struct_stmt.formalization
321-
args_str = ", ".join(
322-
[
344+
)
345+
code = code.replace(var_name, f"{computation.name}({args_str})")
346+
html_parts.append(f"<code>{code}</code>")
347+
html_parts.append("</p>")
348+
val = param_stmt.validation or param_val
349+
if val.satisfiable is not None and val.message is not None and val.holds is not None:
350+
html_parts.append(f'<p><span class="label">Satisfiable:</span> {val.satisfiable}</p>')
351+
html_parts.append(f'<p><span class="label">Holds:</span> {val.holds} ({val.message})</p>')
352+
html_parts.append("</div>")
353+
354+
# Structure Constraints Rendering
355+
for struct_stmt, struct_val in zip(
356+
statements.structure_constraints or [], validation.structure_constraints or []
357+
):
358+
if struct_stmt.formalization is None and only_formalized:
359+
continue
360+
361+
html_parts.append('<div class="block">')
362+
html_parts.append(f"<h2>Type: {struct_stmt.type}</h2>")
363+
html_parts.append(f'<p><span class="label">Statement:</span> {struct_stmt.text}</p>')
364+
html_parts.append('<p><span class="label">Formalization:</span> ')
365+
if struct_stmt.formalization is None:
366+
html_parts.append("UNFORMALIZED")
367+
else:
368+
func_constr = struct_stmt.formalization
369+
args_str = ", ".join(
323370
f"{argname}=" + (f"'{argvalue}'" if isinstance(argvalue, str) else str(argvalue))
324371
for argname, argvalue in func_constr.arguments.items()
325-
]
326-
)
327-
func_str = f"{func_constr.function_name}({args_str}) == {func_constr.expected_result}"
328-
print(func_str)
329-
val = struct_stmt.validation or struct_val
330-
if val.satisfiable is not None and val.holds is not None:
331-
print(f"Satisfiable: {val.satisfiable}")
332-
print(f"Holds: {val.holds}")
333-
print("\n-----------------------------------\n")
334-
if not only_formalized:
335-
for unf_stmt in statements.unformalizable_statements or []:
336-
print("Type:", unf_stmt.type)
337-
print("Statement:", unf_stmt.text)
338-
print("Formalization: UNFORMALIZABLE")
372+
)
373+
func_str = f"{func_constr.function_name}({args_str}) == {func_constr.expected_result}"
374+
html_parts.append(f"<code>{func_str}</code>")
375+
html_parts.append("</p>")
376+
val = struct_stmt.validation or struct_val
377+
if val.satisfiable is not None and val.holds is not None:
378+
html_parts.append(f'<p><span class="label">Satisfiable:</span> {val.satisfiable}</p>')
379+
html_parts.append(f'<p><span class="label">Holds:</span> {val.holds}</p>')
380+
html_parts.append("</div>")
381+
382+
# Unformalizable Statements Rendering (if applicable)
383+
if not only_formalized:
384+
for unf_stmt in statements.unformalizable_statements or []:
385+
html_parts.append('<div class="block">')
386+
html_parts.append(f"<h2>Type: {unf_stmt.type}</h2>")
387+
html_parts.append(f'<p><span class="label">Statement:</span> {unf_stmt.text}</p>')
388+
html_parts.append('<p><span class="label">Formalization:</span> UNFORMALIZABLE</p>')
389+
html_parts.append("</div>")
390+
391+
# End of HTML document
392+
html_parts.append("""</body></html>""")
393+
394+
# Combine all parts into the final HTML string
395+
final_html = "\n".join(html_parts)
396+
397+
# Display the HTML string
398+
from IPython.display import display, HTML # type: ignore
399+
400+
display(HTML(final_html))
401+
402+
else:
403+
print("-----------------------------------\n")
404+
for cost_stmt, cost_val in zip(statements.cost_functions or [], validation.cost_functions or []):
405+
if (cost_stmt.formalization is None or cost_stmt.formalization.mapping is None) and only_formalized:
406+
continue
407+
print("Type:", cost_stmt.type)
408+
print("Statement:", cost_stmt.text)
409+
print("Formalization:", end=" ")
410+
if cost_stmt.formalization is None:
411+
print("UNFORMALIZED")
412+
else:
413+
code = cost_stmt.formalization.code
414+
if cost_stmt.formalization.mapping is not None:
415+
for var_name, computation in cost_stmt.formalization.mapping.items():
416+
if computation is not None:
417+
args_str = ", ".join(
418+
[
419+
f"{argname}=" + (f"'{argvalue}'" if isinstance(argvalue, str) else str(argvalue))
420+
for argname, argvalue in computation.arguments.items()
421+
]
422+
)
423+
code = code.replace(var_name, f"{computation.name}({args_str})")
424+
print(code)
425+
val = cost_stmt.validation or cost_val
426+
if val.satisfiable is not None and val.message is not None:
427+
print(f"Satisfiable: {val.satisfiable}")
428+
print(val.message)
429+
print("\n-----------------------------------\n")
430+
for param_stmt, param_val in zip(
431+
statements.parameter_constraints or [], validation.parameter_constraints or []
432+
):
433+
if (param_stmt.formalization is None or param_stmt.formalization.mapping is None) and only_formalized:
434+
continue
435+
print("Type:", param_stmt.type)
436+
print("Statement:", param_stmt.text)
437+
print("Formalization:", end=" ")
438+
if param_stmt.formalization is None:
439+
print("UNFORMALIZED")
440+
else:
441+
code = param_stmt.formalization.code
442+
if param_stmt.formalization.mapping is not None:
443+
for var_name, computation in param_stmt.formalization.mapping.items():
444+
if computation is not None:
445+
args_str = ", ".join(
446+
[
447+
f"{argname}=" + (f"'{argvalue}'" if isinstance(argvalue, str) else str(argvalue))
448+
for argname, argvalue in computation.arguments.items()
449+
]
450+
)
451+
code = code.replace(var_name, f"{computation.name}({args_str})")
452+
print(code)
453+
val = param_stmt.validation or param_val
454+
if val.satisfiable is not None and val.message is not None and val.holds is not None:
455+
print(f"Satisfiable: {val.satisfiable}")
456+
print(f"Holds: {val.holds} ({val.message})")
457+
print("\n-----------------------------------\n")
458+
for struct_stmt, struct_val in zip(
459+
statements.structure_constraints or [], validation.structure_constraints or []
460+
):
461+
if struct_stmt.formalization is None and only_formalized:
462+
continue
463+
print("Type:", struct_stmt.type)
464+
print("Statement:", struct_stmt.text)
465+
print("Formalization:", end=" ")
466+
if struct_stmt.formalization is None:
467+
print("UNFORMALIZED")
468+
else:
469+
func_constr = struct_stmt.formalization
470+
args_str = ", ".join(
471+
[
472+
f"{argname}=" + (f"'{argvalue}'" if isinstance(argvalue, str) else str(argvalue))
473+
for argname, argvalue in func_constr.arguments.items()
474+
]
475+
)
476+
func_str = f"{func_constr.function_name}({args_str}) == {func_constr.expected_result}"
477+
print(func_str)
478+
val = struct_stmt.validation or struct_val
479+
if val.satisfiable is not None and val.holds is not None:
480+
print(f"Satisfiable: {val.satisfiable}")
481+
print(f"Holds: {val.holds}")
339482
print("\n-----------------------------------\n")
483+
if not only_formalized:
484+
for unf_stmt in statements.unformalizable_statements or []:
485+
print("Type:", unf_stmt.type)
486+
print("Statement:", unf_stmt.text)
487+
print("Formalization: UNFORMALIZABLE")
488+
print("\n-----------------------------------\n")
340489

341490

342491
def _str_units_to_float(str_units: str) -> float:

0 commit comments

Comments
 (0)