diff options
| author | Brian Campbell | 2019-02-14 11:31:35 +0000 |
|---|---|---|
| committer | Brian Campbell | 2019-02-14 11:31:35 +0000 |
| commit | b8fa1b62c114e030f2dcdc58d7df01ae2308b6d4 (patch) | |
| tree | d80b75470d63d97167989491f807824b53e984b8 /src | |
| parent | 33c27c9a4e30f6b3532aeeed0d72b0331c943d8b (diff) | |
Coq: special case printing of bind-if-then-else trees for decoding
Reduces the current arm model output from 268MB to 15MB.
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_coq.ml | 4 |
1 files changed, 4 insertions, 0 deletions
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 |