diff options
| author | Christopher Pulte | 2016-09-26 16:00:29 +0100 |
|---|---|---|
| committer | Christopher Pulte | 2016-09-26 16:00:29 +0100 |
| commit | 764ce21594d77d188e477db8306b3e649075cf0a (patch) | |
| tree | 1217307e318fb2d816ef0e68568ead281221f1e9 | |
| parent | c81529cf5b92fd7c87879ebbb7208dd24c408a09 (diff) | |
minor changes
| -rw-r--r-- | src/gen_lib/sail_values.lem | 1 | ||||
| -rw-r--r-- | src/pretty_print.ml | 19 |
2 files changed, 7 insertions, 13 deletions
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem index 31ebbd1a..6de5b853 100644 --- a/src/gen_lib/sail_values.lem +++ b/src/gen_lib/sail_values.lem @@ -533,4 +533,3 @@ let rec foreach_dec (i,stop,by) vars body = else vars - diff --git a/src/pretty_print.ml b/src/pretty_print.ml index f48ea55c..7f9866f4 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -2176,9 +2176,9 @@ let doc_lit_lem in_pat (L_aux(lit,l)) a = | L_true -> "I" | L_num i -> let ipp = string_of_int i in - if in_pat then "("^ipp^" : n)" - else if i < 0 then "((0"^ipp^") : i)" - else "("^ipp^" : i)" + if in_pat then "("^ipp^":n)" + else if i < 0 then "((0"^ipp^"):i)" + else "("^ipp^":i)" | L_hex n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0x" ^ n) ^ ")" (*shouldn't happen*)*) | L_bin n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0b" ^ n) ^ ")" (*shouldn't happen*)*) | L_undef -> @@ -2391,15 +2391,10 @@ let doc_exp_lem, doc_let_lem = | _ -> string n) | Base(_,Constructor _,_,_,_,_) -> doc_id_lem_ctor f | _ -> doc_id_lem f in - let epp = - align - (call ^//^ - (match args with - | [a] -> expY a - | args -> (parens (align (separate_map (comma ^^ break 1) expY args))) - ) - ) - in + let argpp = match args with + | [a] -> expY a + | args -> parens (align (separate_map (comma ^^ break 0) expY args)) in + let epp = align (call ^//^ argpp) in if aexp_needed then parens (align epp) else epp ) ) |