diff options
| author | Shaked Flur | 2015-05-19 16:31:17 +0100 |
|---|---|---|
| committer | Shaked Flur | 2015-05-19 16:31:17 +0100 |
| commit | 65954b92b20ad295b98ea12a8da87e0b3a0b5f54 (patch) | |
| tree | aab7c1fefdf28dd8697e48516a12a92b468accd2 /src/lem_interp/pretty_interp.ml | |
| parent | a7de95f222940cbc3f341cb281932d55248325d3 (diff) | |
| parent | 2667b17d8bd508b49674928b7440d779f66431cc (diff) | |
Merge branch 'master' of bitbucket.org:Peter_Sewell/l2
Diffstat (limited to 'src/lem_interp/pretty_interp.ml')
| -rw-r--r-- | src/lem_interp/pretty_interp.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml index 76f216ee..76e696f9 100644 --- a/src/lem_interp/pretty_interp.ml +++ b/src/lem_interp/pretty_interp.ml @@ -364,13 +364,13 @@ let doc_exp, doc_let = let default_print _ = brackets (separate_map comma (exp env add_red) exps) in (match exps with | [] -> default_print () - | E_aux(e,_)::es -> - (match e with - | E_lit (L_aux(L_one, _)) | E_lit (L_aux(L_zero, _)) -> - utf8string - ("0b" ^ - (List.fold_right (fun (E_aux(E_lit(L_aux(l, _)),_)) rst -> match l with | L_one -> "1"^rst | L_zero -> "0"^rst) exps "")) - | _ -> default_print ())) + | es -> + if (List.for_all (fun e -> match e with (E_aux(E_lit(L_aux((L_one | L_zero),_)),_)) -> true | _ -> false) es) + then + utf8string + ("0b" ^ + (List.fold_right (fun (E_aux(E_lit(L_aux(l, _)),_)) rst -> match l with | L_one -> "1"^rst | L_zero -> "0"^rst | L_undef -> "u"^rst) exps "")) + else default_print ()) | E_vector_indexed (iexps, (Def_val_aux(default,_))) -> let default_string = (match default with |