Skip to content

Commit df22e17

Browse files
yavyav
committed
Improvements to pretty printing of terms.
* This changes the `atomic` boolean parameter to a `prec` integer parameter specifying the precedence of the surrounding context. * We also change how some things are printed: - a lot fewer parens, based on precedence - suffix of numeric literals is separated by `'` (see also #337) - pointers are printed in base 16 - use `NULL` instead of `null` to match CN's input notation - custom printing for negated comparisons `x != y` instead of `!(x == y)` - use `%` instead of `rem` - use `^` instead of `xor_uf` - use `&` instead of `bw_and_uf` - use `|` instead of `bw_or_uf` - use `<<` instead of `shift_left` - use `>>` instead of `shift_right` - use `{ ...s, x = e }` for updating things. This is borrowed from JavaScript but it makes the precedence story simpler. - use `&p->x` instead of `member_shift<T>(p,x)` - use `&p[x]` instead of `array_shift<T>(p,x)` - use `cons(x,xs)` instead of `x :: xs`
1 parent 09200e4 commit df22e17

4 files changed

Lines changed: 142 additions & 115 deletions

File tree

‎backend/cn/lib/indexTerms.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ let term_of_sterm : sterm -> typed = Terms.map_term SurfaceBaseTypes.to_basetype
2828

2929
let sterm_of_term : typed -> sterm = Terms.map_term SurfaceBaseTypes.of_basetype
3030

31-
let pp ?(atomic = false) = Terms.pp ~atomic
31+
let pp ?(prec = 0) = Terms.pp ~prec
3232

3333
let pp_with_typf f it = Pp.typ (pp it) (f (bt it))
3434

‎backend/cn/lib/resourceTypes.ml‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -71,6 +71,13 @@ let pp_predicate_type_aux (p : predicate_type) oargs =
7171

7272

7373
let pp_qpredicate_type_aux (p : qpredicate_type) oargs =
74+
(* XXX: this is `p + i * step` but that's "wrong" in a couple of ways:
75+
- we are not using the correct precedences for `p` and `step`
76+
- in C pointer arithmetic takes account of the types, but here
77+
we seem to be doing it at the byte level. Would `step` ever
78+
differ from the size of elements that `p` points to?
79+
- perhaps print as `&p[i]` or `&p[j + i]`
80+
*)
7481
let pointer = IT.pp p.pointer ^^^ plus ^^^ Sym.pp (fst p.q) ^^^ star ^^^ IT.pp p.step in
7582
let args = pointer :: List.map IT.pp p.iargs in
7683
!^"each"

‎backend/cn/lib/simplify.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -380,7 +380,7 @@ module IndexTerms = struct
380380
(match (op, IT.term a) with
381381
| Not, Const (Bool b) -> bool_ (not b) the_loc
382382
| Not, Unop (Not, x) -> x
383-
| Negate, Unop (Negate,x) -> x
383+
| Negate, Unop (Negate, x) -> x
384384
| Negate, Const (Z z) -> z_ (Z.neg z) the_loc
385385
| Negate, Const (Bits ((sign, width), z)) ->
386386
num_lit_ (Z.neg z) (BT.Bits (sign, width)) the_loc

‎backend/cn/lib/terms.ml‎

Lines changed: 133 additions & 113 deletions
Original file line numberDiff line numberDiff line change
@@ -148,13 +148,36 @@ let rec pp_pattern (Pat (pat_, _bt, _)) =
148148
args)
149149

150150

151+
(* Precedences:
152+
Reference: https://en.cppreference.com/w/c/language/operator_precedence
153+
The number we use are `16 - p` where `p` is the reference in the table.
154+
We do this so bigger numbers are higher precedence.
155+
156+
Highest
157+
158+
15: . [] -> selectors
159+
14: ! - ~ & cast unary
160+
13: * / %
161+
12: + -
162+
10: < <= > >=
163+
9: == !=
164+
8: &
165+
7: ^
166+
6: |
167+
5: &&
168+
4: ||
169+
3: ? : ternary
170+
171+
Lowest
172+
*)
173+
151174
let pp
152175
: 'bt 'a.
153-
?atomic:bool -> ?f:('bt term -> Pp.document -> Pp.document) -> 'bt term -> Pp.document
176+
?prec:int -> ?f:('bt term -> Pp.document -> Pp.document) -> 'bt term -> Pp.document
154177
=
155-
fun ?(atomic = false) ?(f = fun _ x -> x) ->
156-
let rec aux atomic (IT (it, _, _)) =
157-
let aux b x = f x (aux b x) in
178+
fun ?(prec = 0) ?(f = fun _ x -> x) ->
179+
let rec aux prec (IT (it, _, _)) =
180+
let aux prec x = f x (aux prec x) in
158181
(* Without the `lparen` inside `nest 2`, the printed `rparen` is indented by 2 (wrt to
159182
the lparen). I don't quite understand it, but it works. *)
160183
let parens pped =
@@ -163,7 +186,7 @@ let pp
163186
let braces pped =
164187
Pp.group ((nest 2 @@ lbrace ^^ break 0 ^^ pped) ^^ break 0 ^^ rbrace)
165188
in
166-
let mparens pped = if atomic then parens pped else Pp.group pped in
189+
let wrap_after tgt doc = if prec > tgt then parens doc else doc in
167190
let break_op x = break 1 ^^ x ^^ space in
168191
let alloc_id i = !^("@" ^ Z.to_string i) in
169192
match it with
@@ -173,7 +196,7 @@ let pp
173196
| Bits ((sign, n), v) ->
174197
let dec =
175198
!^(Z.to_string v)
176-
^^ (match sign with Unsigned -> !^"u" | Signed -> !^"i")
199+
^^ (match sign with Unsigned -> !^"'u" | Signed -> !^"'i")
177200
^^ !^(string_of_int n)
178201
in
179202
if Z.lt v (Z.of_int 16) then
@@ -185,89 +208,100 @@ let pp
185208
^^^ !^"*/"
186209
| Q q -> !^(Q.to_string q)
187210
| Pointer { alloc_id = id; addr } ->
188-
braces (alloc_id id ^^ Pp.semi ^^ Pp.space ^^ !^(Z.to_string addr))
211+
braces (alloc_id id ^^ Pp.semi ^^ Pp.space ^^ !^("0x" ^ Z.format "%x" addr))
189212
| Alloc_id i -> !^("@" ^ Z.to_string i)
190213
| Bool true -> !^"true"
191214
| Bool false -> !^"false"
192215
| Unit -> !^"void"
193216
| Default bt -> c_app !^"default" [ BaseTypes.pp bt ]
194-
| Null -> !^"null"
217+
| Null -> !^"NULL"
195218
| CType_const ct -> Pp.squotes (Sctypes.pp ct))
196219
| Sym sym -> Sym.pp sym
197220
| Unop (uop, it1) ->
221+
let prefix x op p = wrap_after x (!^op ^^ aux p it1) in
198222
(match uop with
199-
| BW_CLZ_NoSMT -> c_app !^"bw_clz_uf" [ aux false it1 ]
200-
| BW_CTZ_NoSMT -> c_app !^"bw_ctz_uf" [ aux false it1 ]
201-
| BW_FFS_NoSMT -> c_app !^"bw_ffs_uf" [ aux false it1 ]
202-
| BW_FLS_NoSMT -> c_app !^"bw_fls_uf" [ aux false it1 ]
203-
| Not -> mparens (!^"!" ^^ parens (aux false it1))
204-
| Negate -> mparens (!^"-" ^^ parens (aux false it1))
205-
| BW_Compl -> mparens (!^"~" ^^ parens (aux false it1)))
223+
| BW_CLZ_NoSMT -> c_app !^"bw_clz_uf" [ aux 0 it1 ]
224+
| BW_CTZ_NoSMT -> c_app !^"bw_ctz_uf" [ aux 0 it1 ]
225+
| BW_FFS_NoSMT -> c_app !^"bw_ffs_uf" [ aux 0 it1 ]
226+
| BW_FLS_NoSMT -> c_app !^"bw_fls_uf" [ aux 0 it1 ]
227+
| Not ->
228+
let infix p op l r =
229+
wrap_after p (flow (break 1 ^^ op ^^ space) [ aux p l; aux p r ])
230+
in
231+
(match it1 with
232+
| IT (Binop (EQ, l, r), _, _) -> infix 9 (!^"!" ^^ equals) l r
233+
| IT (Binop (LT, l, r), _, _) -> infix 10 (rangle () ^^ equals) l r
234+
| IT (Binop (LE, l, r), _, _) -> infix 10 (rangle ()) l r
235+
| IT (Binop (LTPointer, l, r), _, _) -> infix 10 (rangle () ^^ equals) l r
236+
| IT (Binop (LEPointer, l, r), _, _) -> infix 10 (rangle ()) l r
237+
| _ -> prefix 14 "!" 14)
238+
| Negate -> prefix 14 "-" 14
239+
| BW_Compl -> prefix 14 "~" 14)
206240
| Binop (bop, it1, it2) ->
241+
let infix x op l r = wrap_after x (flow (break_op op) [ aux l it1; aux r it2 ]) in
242+
let prefix x = c_app !^x [ aux 0 it1; aux 0 it2 ] in
207243
(match bop with
208-
| And ->
209-
mparens (flow (break_op (ampersand ^^ ampersand)) [ aux true it1; aux true it2 ])
210-
| Or -> mparens (flow (break_op (bar ^^ bar)) [ aux true it1; aux true it2 ])
211-
| Implies -> c_app !^"implies" [ aux true it1; aux true it2 ]
212-
| Add -> mparens (flow (break_op plus) [ aux true it1; aux true it2 ])
213-
| Sub -> mparens (flow (break_op minus) [ aux true it1; aux true it2 ])
214-
| Mul -> mparens (flow (break_op star) [ aux true it1; aux true it2 ])
215-
| MulNoSMT -> mparens (c_app !^"mul_uf" [ aux true it1; aux true it2 ])
216-
| Div -> mparens (flow (break_op slash) [ aux true it1; aux true it2 ])
217-
| DivNoSMT -> mparens (c_app !^"div_uf" [ aux true it1; aux true it2 ])
218-
| Exp -> c_app !^"power" [ aux true it1; aux true it2 ]
219-
| ExpNoSMT -> c_app !^"power_uf" [ aux true it1; aux true it2 ]
220-
| Rem -> c_app !^"rem" [ aux true it1; aux true it2 ]
221-
| RemNoSMT -> mparens (c_app !^"rem_uf" [ aux true it1; aux true it2 ])
222-
| Mod -> c_app !^"mod" [ aux true it1; aux true it2 ]
223-
| ModNoSMT -> mparens (c_app !^"mod_uf" [ aux true it1; aux true it2 ])
224-
| EQ -> mparens (flow (break_op (equals ^^ equals)) [ aux true it1; aux true it2 ])
225-
| LT -> mparens (flow (break_op @@ langle ()) [ aux true it1; aux true it2 ])
226-
| LE ->
227-
mparens (flow (break_op @@ langle () ^^ equals) [ aux true it1; aux true it2 ])
228-
| LTPointer ->
229-
mparens (flow (break_op @@ langle ()) [ aux true it1; aux true it2 ])
230-
| LEPointer ->
231-
mparens (flow (break_op @@ langle () ^^ equals) [ aux true it1; aux true it2 ])
232-
| Min -> c_app !^"min" [ aux false it1; aux false it2 ]
233-
| Max -> c_app !^"max" [ aux false it1; aux false it2 ]
234-
| XORNoSMT -> c_app !^"xor_uf" [ aux false it1; aux false it2 ]
235-
| BW_And -> c_app !^"bw_and_uf" [ aux false it1; aux false it2 ]
236-
| BWOrNoSMT -> c_app !^"bw_or_uf" [ aux false it1; aux false it2 ]
237-
| ShiftLeft -> c_app !^"shift_left" [ aux false it1; aux false it2 ]
238-
| ShiftRight -> c_app !^"shift_right" [ aux false it1; aux false it2 ]
239-
| SetMember -> c_app !^"member" [ aux false it1; aux false it2 ]
240-
| SetUnion -> c_app !^"union" [ aux false it1; aux false it2 ]
241-
| SetIntersection -> c_app !^"inter" [ aux false it1; aux false it2 ]
242-
| SetDifference -> c_app !^"difference" [ aux false it1; aux false it2 ]
243-
| Subset -> c_app !^"subset" [ aux false it1; aux false it2 ])
244+
| And -> infix 5 (ampersand ^^ ampersand) 5 5
245+
| Or -> infix 4 (bar ^^ bar) 4 4
246+
| Implies -> prefix "implies"
247+
| Add -> infix 12 !^"+" 12 12
248+
| Sub -> infix 12 !^"-" 12 13
249+
| Mul -> infix 13 !^"*" 13 13
250+
| MulNoSMT -> prefix "mul_uf"
251+
| Div -> infix 13 slash 14 14
252+
| DivNoSMT -> prefix "div_uf"
253+
| Exp -> prefix "power"
254+
| ExpNoSMT -> prefix "power_uf"
255+
| Rem -> infix 13 !^"%" 14 14
256+
| RemNoSMT -> prefix "rem_uf"
257+
| Mod -> prefix "mod"
258+
| ModNoSMT -> prefix "mod_uf"
259+
| EQ -> infix 9 (equals ^^ equals) 9 9
260+
| LT -> infix 10 (langle ()) 10 10
261+
| LE -> infix 10 (langle () ^^ equals) 10 10
262+
| LTPointer -> infix 10 (langle ()) 10 10
263+
| LEPointer -> infix 10 (langle () ^^ equals) 10 10
264+
| Min -> prefix "min"
265+
| Max -> prefix "max"
266+
| XORNoSMT -> infix 7 !^"^" 7 7
267+
| BW_And -> infix 8 ampersand 8 8
268+
| BWOrNoSMT -> infix 6 bar 6 6
269+
| ShiftLeft ->
270+
infix 0 (langle () ^^ langle ()) 1 1 (* easier to read with parens *)
271+
| ShiftRight ->
272+
infix 0 (rangle () ^^ rangle ()) 1 1 (* easier to read with parens *)
273+
| SetMember -> prefix "member"
274+
| SetUnion -> prefix "union"
275+
| SetIntersection -> prefix "inter"
276+
| SetDifference -> prefix "difference"
277+
| Subset -> prefix "subset")
244278
| ITE (o1, o2, o3) ->
245-
parens (flow (break 1) [ aux true o1; !^"?"; aux true o2; colon; aux true o3 ])
279+
wrap_after 2 (flow (break 1) [ aux 3 o1; !^"?"; aux 3 o2; colon; aux 3 o3 ])
246280
| EachI ((i1, (s, _), i2), t) ->
247281
Pp.(
248282
group
249283
@@ group (c_app !^"for" [ int i1; Sym.pp s; int i2 ])
250-
^/^ group ((nest 2 @@ lbrace ^^ break 0 ^^ aux false t) ^^ break 0 ^^ rbrace))
251-
| NthTuple (n, it2) -> mparens (aux true it2 ^^ dot ^^ !^("member" ^ string_of_int n))
252-
| Tuple its -> braces (separate_map (semi ^^ space) (aux false) its)
284+
^/^ group ((nest 2 @@ lbrace ^^ break 0 ^^ aux 0 t) ^^ break 0 ^^ rbrace))
285+
| NthTuple (n, it2) ->
286+
wrap_after 15 (aux 15 it2 ^^ dot ^^ !^("member" ^ string_of_int n))
287+
| Tuple its -> braces (separate_map (semi ^^ space) (aux 0) its)
253288
| Struct (_tag, members) ->
254289
lbrace
255290
^^ hardline
256291
^^ flow_map
257292
(comma ^^ hardline)
258293
(fun (member, it) ->
259-
Pp.group
260-
@@ (Pp.group @@ dot ^^ Id.pp member ^^^ equals)
261-
^^^ align (aux false it))
294+
Pp.group @@ (Pp.group @@ dot ^^ Id.pp member ^^^ equals) ^^^ align (aux 0 it))
262295
members
263296
^^^ rbrace
264-
| StructMember (t, member) -> prefix 0 0 (aux true t) (dot ^^ Id.pp member)
297+
| StructMember (t, member) -> wrap_after 15 (aux 15 t ^^ dot ^^ Id.pp member)
265298
| StructUpdate ((t, member), v) ->
266-
mparens
267-
(aux true t
268-
^^ braces
269-
@@ (Pp.group @@ dot ^^ Id.pp member ^^^ equals)
270-
^^^ align (aux true v))
299+
braces
300+
(!^"..."
301+
^^ aux 0 t
302+
^^ comma
303+
^^^ (Pp.group @@ dot ^^ Id.pp member ^^^ equals)
304+
^^^ align (aux 0 v))
271305
| Record members ->
272306
align
273307
@@ lbrace
@@ -276,79 +310,65 @@ let pp
276310
(fun (member, it) ->
277311
Pp.group
278312
@@ (Pp.group @@ dot ^^ Id.pp member ^^^ equals)
279-
^^^ align (aux false it))
313+
^^^ align (aux 0 it))
280314
members
281315
^^^ rbrace
282-
| RecordMember (t, member) -> prefix 0 0 (aux true t) (dot ^^ Id.pp member)
316+
| RecordMember (t, member) -> wrap_after 15 (aux 15 t ^^ dot ^^ Id.pp member)
283317
| RecordUpdate ((t, member), v) ->
284-
mparens
285-
(aux true t
286-
^^ braces
287-
@@ (Pp.group @@ dot ^^ Id.pp member ^^^ equals)
288-
^^^ align (aux true v))
289-
| Cast (cbt, t) ->
290-
mparens (align @@ parens (BaseTypes.pp cbt) ^^ break 0 ^^ aux true t)
291-
| MemberShift (t, tag, member) ->
292-
mparens
293-
(c_app (!^"member_shift" ^^ angles (Sym.pp tag)) [ aux false t; Id.pp member ])
294-
| ArrayShift { base; ct; index } ->
295-
mparens
296-
(c_app
297-
(!^"array_shift" ^^ angles (Sctypes.pp ct))
298-
[ aux false base; aux false index ])
299-
| CopyAllocId { addr; loc } ->
300-
mparens (c_app !^"copy_alloc_id" [ aux false addr; aux false loc ])
301-
| SizeOf t -> mparens (c_app !^"sizeof" [ Sctypes.pp t ])
302-
| OffsetOf (tag, member) -> mparens (c_app !^"offsetof" [ Sym.pp tag; Id.pp member ])
303-
| Aligned t -> mparens (c_app !^"aligned" [ aux false t.t; aux false t.align ])
304-
| Representable (rt, t) ->
305-
mparens (c_app (!^"repr" ^^ angles (CT.pp rt)) [ aux false t ])
306-
| Good (rt, t) -> mparens (c_app (!^"good" ^^ angles (CT.pp rt)) [ aux false t ])
307-
| WrapI (ity, t) ->
308-
mparens (c_app (!^"wrapI" ^^ angles (CT.pp (Integer ity))) [ aux false t ])
309-
| Head o1 -> mparens (c_app !^"hd" [ aux false o1 ])
310-
| Tail o1 -> mparens (c_app !^"tl" [ aux false o1 ])
318+
braces
319+
(!^"..."
320+
^^ aux 0 t
321+
^^ comma
322+
^^^ (Pp.group @@ dot ^^ Id.pp member ^^^ equals)
323+
^^^ align (aux 0 v))
324+
| Cast (cbt, t) -> wrap_after 14 (align @@ parens (BaseTypes.pp cbt) ^^ aux 14 t)
325+
| MemberShift (t, _tag, member) ->
326+
wrap_after 14 (ampersand ^^ aux 15 t ^^ (!^"-" ^^ rangle ()) ^^ Id.pp member)
327+
| ArrayShift { base; ct = _ct; index } ->
328+
wrap_after 14 (ampersand ^^ aux 15 base ^^ brackets (aux 0 index))
329+
| CopyAllocId { addr; loc } -> c_app !^"copy_alloc_id" [ aux 0 addr; aux 0 loc ]
330+
| SizeOf t -> c_app !^"sizeof" [ Sctypes.pp t ]
331+
| OffsetOf (tag, member) -> c_app !^"offsetof" [ Sym.pp tag; Id.pp member ]
332+
| Aligned t -> c_app !^"aligned" [ aux 0 t.t; aux 0 t.align ]
333+
| Representable (rt, t) -> c_app (!^"repr" ^^ angles (CT.pp rt)) [ aux 0 t ]
334+
| Good (rt, t) -> c_app (!^"good" ^^ angles (CT.pp rt)) [ aux 0 t ]
335+
| WrapI (ity, t) -> c_app (!^"wrapI" ^^ angles (CT.pp (Integer ity))) [ aux 0 t ]
336+
| Head o1 -> c_app !^"hd" [ aux 0 o1 ]
337+
| Tail o1 -> c_app !^"tl" [ aux 0 o1 ]
311338
| Nil bt -> !^"nil" ^^ angles (BaseTypes.pp bt)
312-
| Cons (t1, t2) -> mparens (aux true t1 ^^ colon ^^ colon ^^ aux true t2)
313-
| NthList (n, xs, d) ->
314-
mparens (c_app !^"nth_list" [ aux false n; aux false xs; aux false d ])
339+
| Cons (t1, t2) -> c_app !^"cons" [ aux 0 t1; aux 0 t2 ]
340+
| NthList (n, xs, d) -> c_app !^"nth_list" [ aux 0 n; aux 0 xs; aux 0 d ]
315341
| ArrayToList (arr, i, len) ->
316-
mparens (c_app !^"array_to_list" [ aux false arr; aux false i; aux false len ])
317-
| MapConst (_bt, t) -> mparens (c_app !^"const" [ aux false t ])
318-
| MapGet (t1, t2) -> mparens (aux true t1 ^^ brackets (aux false t2))
342+
c_app !^"array_to_list" [ aux 0 arr; aux 0 i; aux 0 len ]
343+
| MapConst (_bt, t) -> c_app !^"const" [ aux 0 t ]
344+
| MapGet (t1, t2) -> wrap_after 15 (aux 15 t1 ^^ brackets (aux 0 t2))
319345
| MapSet (t1, t2, t3) ->
320-
mparens (aux true t1 ^^ brackets (aux false t2 ^^^ equals ^^^ aux false t3))
321-
| MapDef ((s, _), t) -> brackets (Sym.pp s ^^^ !^"->" ^^^ aux false t)
322-
| Apply (name, args) -> c_app (Sym.pp name) (List.map (aux false) args)
346+
wrap_after 15 (aux 15 t1 ^^ brackets (aux 0 t2 ^^^ equals ^^^ aux 0 t3))
347+
| MapDef ((s, _), t) -> brackets (Sym.pp s ^^^ (!^"-" ^^ rangle ()) ^^^ aux 0 t)
348+
| Apply (name, args) -> c_app (Sym.pp name) (List.map (aux 0) args)
323349
| Let ((name, x1), x2) ->
324-
parens
325-
(!^"let"
326-
^^^ Sym.pp name
327-
^^^ Pp.equals
328-
^^^ aux false x1
329-
^^^ !^"in"
330-
^^^ aux false x2)
350+
parens (!^"let" ^^^ Sym.pp name ^^^ Pp.equals ^^^ aux 0 x1 ^^^ !^"in" ^^^ aux 0 x2)
331351
| Match (e, cases) ->
332352
!^"match"
333-
^^^ aux false e
353+
^^^ aux 0 e
334354
^^^ braces
335355
((* copying from mparens *)
336356
Pp.group
337357
(nest 2
338358
@@ separate_map
339359
(break 0)
340360
(fun (pattern, body) ->
341-
pp_pattern pattern ^^^ !^"=>" ^^^ braces (aux false body))
361+
pp_pattern pattern ^^^ !^"=>" ^^^ braces (aux 0 body))
342362
cases))
343363
| Constructor (s, args) ->
344364
Sym.pp s
345365
^^^ braces
346366
(separate_map
347367
(comma ^^ space)
348-
(fun (id, e) -> Id.pp id ^^ colon ^^^ aux false e)
368+
(fun (id, e) -> Id.pp id ^^ colon ^^^ aux 0 e)
349369
args)
350370
in
351-
fun (it : 'bt term) -> aux atomic it
371+
fun (it : 'bt term) -> aux prec it
352372
353373
354374
open Cerb_pp_prelude

0 commit comments

Comments
 (0)