diff options
| author | Thomas Bauereiss | 2019-03-25 18:54:42 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2019-03-26 16:13:02 +0000 |
| commit | d9b592b89bd2c47622aa9dbcd0843936322322e3 (patch) | |
| tree | f6c9637c99be7a8bd69a63413e11e04c58935e20 /src/pretty_print_lem.ml | |
| parent | a0aae7194dddab24d0c198d46b0e22fef04c2026 (diff) | |
Lem: Work around if-cascade indentation problem
Copied from Coq backend.
Diffstat (limited to 'src/pretty_print_lem.ml')
| -rw-r--r-- | src/pretty_print_lem.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 933925da..20c9a69f 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -975,6 +975,10 @@ let doc_exp_lem, doc_let_lem = | E_aux (E_if (c', t', e'), _) | E_aux (E_cast (_, E_aux (E_if (c', t', e'), _)), _) -> if_exp ctxt true c' t' e' + (* Special case to prevent current arm decoder becoming a staircase *) + (* TODO: replace with smarter pretty printing *) + | E_aux (E_internal_plet (pat,exp1,E_aux (E_cast (typ, (E_aux (E_if (_, _, _), _) as exp2)),_)),ann) when Typ.compare typ unit_typ == 0 -> + string "else" ^/^ top_exp ctxt false (E_aux (E_internal_plet (pat,exp1,exp2),ann)) | _ -> prefix 2 1 (string "else") (top_exp ctxt false e) in (prefix 2 1 |