Pp imrovements

[yav]

Changes in this PR:

• Add 2 additional rewrites to remove double negations

• A couple of small tweaks the CSS style for reports

• A bunch of improvements to the pretty printer for terms, namely:

  • 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 [CN] Allow ' in numeric constants #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
      ~

[cp526]

Thanks, that's very useful. Two comments:

The commits don't seem to include the css file.

The pretty-printing has to be in sync with CN's parser:

• for the operations rem -- shift_right, that looks good, but we should then use that syntax in the c_parser.mly

• the record/struct update syntax is different from the one we use in CN. CN uses a Rust-like notation: e.g. the CN specification function below returns a struct-as-a-value with updated member x and unchanged member y:

  struct s { int x; int y; };
  
  /*@  
  function (struct s) update_x (struct s str) 
  {
    { x: 0i32, ..str}
  }
  @*/
  

• For member and array shift it's not clear whether it's always ok to omit the C-type. At least in the case of array shifts there's some ambiguity, because the pointer doesn't carry the C-type information (in a way that we're considering to change in the future.)

[yav]

I didn't know that we had surface notation for updating structs, I'll update the printer to match.

For array_shift perhaps we can print it as &(T)p[l]. I really think we should just change CN to not throw away the types thought, I can't image that's a big change, would be happy to look into it (in a separate PR).

I modified the CSS file in report.ml is there another one I need to change? My changes are tiny , use pre in the tables (not sure if that's a good idea, but it allows us to experiment with the layout of the Pprint library), and alternate the colors of the rows in the table, you

More generally on the properties of the pretty-printer:

• I do agree that it's a good plan to have it match the surface syntax
• Currently it does not really (e.,g., struct update is printer like in Haskell ((s { x = 0 }), EachI has a completely made up notation, etc.)
• I made a comment note in resourceTypes.ml which seems to be used for the printing of resources to note that the notation used there can be confusing (it prints things as if the math is done on bytes, but in C the types of things are usually taken into account)
• Do you mean that we want all of term to be printed in CN surface notation, or just the ones that correspond to "values" (i.e., things the solver might make).

[cp526]

I didn't know that we had surface notation for updating structs, I'll update the printer to match.

Thanks! I think we use the same notation for both structs and records.

For array_shift perhaps we can print it as &(T)p[l]. I really think we should just change CN to not throw away the types thought, I can't image that's a big change, would be happy to look into it (in a separate PR).

That's something we're considering – I think there should be an open issue related to that: it would make for a better user interface, because Owned, array_shift, and member_shift would no longer need to take the C-type as an explicit argument. It's a big change though, because the Core language CN actually type checks and the Cerberus frontend would have to be changed substantially to track the C-type information in a corresponding way for this to work.

I modified the CSS file in report.ml is there another one I need to change? My changes are tiny , use pre in the tables (not sure if that's a good idea, but it allows us to experiment with the layout of the Pprint library), and alternate the colors of the rows in the table, you

Ah, sorry, I missed that.

More generally on the properties of the pretty-printer:

• I do agree that it's a good plan to have it match the surface syntax
• Currently it does not really (e.,g., struct update is printer like in Haskell ((s { x = 0 }), EachI has a completely made up notation, etc.)

Thanks! I wasn't aware of that mismatch, then we should fix those at some point.

• I made a comment note in resourceTypes.ml which seems to be used for the printing of resources to note that the notation used there can be confusing (it prints things as if the math is done on bytes, but in C the types of things are usually taken into account)

Good point. Here, too, we should make the pretty-print produce the same output. Though here this might require us to remember the C-type annotation on the array shift from the frontend for the step, which is a bit awkward.

• Do you mean that we want all of term to be printed in CN surface notation, or just the ones that correspond to "values" (i.e., things the solver might make).

Everything, I'd say. If we're not already doing that (including the places you listed) that's a bug.

[yav]

I think we probably don't want to make changes to the parser until #342 is merged. How do you want to proceed?

• We could keep the syntax changes (e.g., &p->x) with the plan to also update the parser after Separating the C and CN parsing #342 is merged
• I could undo them (reverting back to member_shift) but we'd still get the fewer parens

[septract]

My opinion: it’s high impact to make the pretty printed output more readable. So we should merge this change now, and plan to align the parser later once #342 is merged. On Aug 8, 2024, at 11:38 AM, Iavor S. Diatchki ***@***.***> wrote: I think we probably don't want to make changes to the parser until #342 is merged. How do you want to proceed? We could keep the syntax changes (e.g., &p->x) with the plan to also update the parser after #342 is merged I could undo them (reverting back to member_shift) but we'd still get the fewer parens —Reply to this email directly, view it on GitHub, or unsubscribe.You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[cp526]

Just merged that.

Regarding the parser, @kmemarian is that going to make your life harder (wrt to the Cerberus/CN separation) if we tweak or extend the CN parser now?

[dc-mak]

Relevant issue for pointers carrying C types: #349