From b8fa1b62c114e030f2dcdc58d7df01ae2308b6d4 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 14 Feb 2019 11:31:35 +0000
Subject: Coq: special case printing of bind-if-then-else trees for decoding
 Reduces the current arm model output from 268MB to 15MB.

---
 src/pretty_print_coq.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 4596f23f..27484560 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1775,6 +1775,10 @@ let doc_exp, doc_let =
       | 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