From d9b592b89bd2c47622aa9dbcd0843936322322e3 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Mon, 25 Mar 2019 18:54:42 +0000
Subject: Lem: Work around if-cascade indentation problem

Copied from Coq backend.
---
 src/pretty_print_lem.ml | 4 ++++
 1 file changed, 4 insertions(+)

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
-- 
cgit v1.2.3