diff options
| author | Thomas Bauereiss | 2017-10-31 16:17:45 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2017-10-31 16:17:45 +0000 |
| commit | fe486c7b4126131920157c9348478fe6b40d3636 (patch) | |
| tree | 1866f3e7a7c6259745214dcb94040b23a7031a6e /src/pretty_print_lem.ml | |
| parent | a88e0182b05acf417b262173a2b83ecd9a35c93a (diff) | |
Pretty-print Sail assertions in Lem
Map to calls to monadic function assert_exp that throws an exception if the
assertion is false
Diffstat (limited to 'src/pretty_print_lem.ml')
| -rw-r--r-- | src/pretty_print_lem.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 7d0d3459..67febd0a 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -1029,10 +1029,8 @@ let doc_exp_lem, doc_let_lem = if aexp_needed then parens (align epp) else align epp | E_exit e -> liftR (separate space [string "exit"; expY e;]) | E_assert (e1,e2) -> - (* FIXME needs pretty-printing of E_constraint; ignore for now *) - string "()" - (* let epp = separate space [string "assert'"; expY e1; expY e2] in - if aexp_needed then parens (align epp) else align epp *) + let epp = liftR (separate space [string "assert_exp"; expY e1; expY e2]) in + if aexp_needed then parens (align epp) else align epp | E_app_infix (e1,id,e2) -> (* TODO: Should have been removed by the new type checker; check with Alasdair *) raise (Reporting_basic.err_unreachable l |