[cn] Pretty print terms for humans

[yav]

The pretty printer for CN terms makes it pretty hard to read the constraints. It might be nice to improve the current one, or just have a different pretty printer that we use explicitly for rendering output intended to be viewed by the user.

Some of the features that would be nice to have:

• Use precedence rules to print fewer parend
• Use a notation that mirrors the input, or at even better C, so instead of member_shift<T>(e,x), we could just write e->x
• Optionally hide some information (e.g., some type annotations or casts can be quite noisy, so we might want to have a way to simply not show them
• It might also be nice to have the output of this pretty printer be something more structured than text, so that when we render it to, say, HTML, we can show information in clever ways (e.g., show types on hover), line up struct fields in a table, etc.

[cp526]

That would be very useful. Though I think CN's pretty-print should always produce output that CN could also parse (i.e. valid CN, not special different C-like syntax), for consistency.

[dc-mak]

Did this commit close this issue? https://github.com/rems-project/cerberus/commit/a955e58a7fd502b5e1b3641c8ea0f03ebd54116e

[cp526]

Not fully, no.

[dc-mak]

Ok, can the remaining things be put in a separate issue and this one closed then?

[dc-mak]

@yav @cp526 can you clarify what's done and what's remaining on this?

[yav]

I am not 100% sure, but based on the discussion on PR #470, these are some things that need to be done:

• Update all constructs tp pretty print using CN surface syntax (there are still some that are printed in a made up way, and some are done differently, for example, iterated resources use pointer arithmetic but on bytes instead of the pointer type, which looks like C but has a different meaning.)
• I changed the pretty printing for some constructs, @cp526 suggested that we should change the parser to match (e.g., using &p->x instead of shift_member(p,s) and &a[i] instead of shift_array(a,i).
  • At the moment we don't print the type of the pointer in the above shifts, while the surface syntax provides a way to provide it. I don't fully understand why users need to provided this type, but if we wanted to print it, we could do so with a cast, although I think that will reduce the readability of the output.

[dc-mak]

Thanks for clarifying, much appreciated.

Users need to provide a type for MemberShift for the same reason that OffsetOf needs one - to look up in the memory model. Similarly with ArrayShift (size of the C type). Index terms pointers don't have C type information attached. See https://github.com/rems-project/cerberus/issues/349 for further details, though I see some related discussion was present on on #470 already.

[peterohanley]

• Use a notation that mirrors the input, or at even better C, so instead of member_shift(e,x), we could just write e->x

I have written specs (in #361) that use member_shift with the same e but different T and x, so this needs to be a conditional pretty-printing.