Improved ReML pretty printing

[melsman]

Get-regions

ReML allows for explicit region parameters to be dropped. For instance, in the program below, r1 has no put-effects:

fun f `[r1 r2] (s:string`r1) : string`r2 =      (* OK ReML *) 
  s ^ ""      

• The above ReML program should be pretty-printed as (e.g., using -Pcee):

fun f `[r1 | r2] (s:string`r1) : string`r2 =      (* PROPOSAL *) 
  s ^[`r2] ""

Here the bar (i.e., |) in the parameter list separates "get-only region parameters" (and explicit effect parameters) from region parameters with put effects.

Anti-aliasing

ReML has support for specifying "anti-aliasing":

fun g `[r1 r2] (s:string`r1) : (string`r2) while r1 # r2 = 
 s ^ ""

Here we are specifying that g cannot be applied to identical regions and it will be checked that this property is guaranteed for all calls.

• With this PR, the above program is pretty printed (with -Pcee -print_constraints) as:

fun g [`r1 # {`r2}:inf|`r2:inf] s = s ^[attop `r2] ""

• Notice also that with -print_control_abbrev_layout, explicit region variables and explicit effect variables are printed without unique ids...

Improved case-handling

• This PR also provides support for improved pretty-printing of case expressions:

fun cp (xs : int list) =
   case xs of
       nil => nil
     | x :: xs => x :: cp xs

Here is the pretty-printed version of cp (-Pcee):

fun cp [r77:inf] xs = 
   case xs of
      nil => nil
    | :: v127 => let val v128 = #0 v127; val v129 = #1 v127 in :: (v128, cp[sat r77] v129)attop r77 end

Previously, a decon_:: expression was shown to extract v127 from xs through an addtional let-binding.

Finally, this PR also pretty-prints many primitive using prettier qualified names (e.g., W64.>> and W63.andb instead of __shift_right_unsigned_word64ub and __andb_word63).

Note on Constraints

ReML also allows for specifying a constraint saying that there are no put-effects on an effect (i.e., noput e) . However, ReML does not allow specifying that there are no put-effects on a region variable:

fun f `[r1 r2] (s:string`r1) : (string`r2) while noput r1 =      (* NOT SUPPORTED - WRONG *) 
  s ^ ""      

Here the programmer has attempted to specify that there are no direct put-effects on r1 inside the body of f. No attempts are made to restrict r2. The purpose of the specification is to guarantee that, at runtime, only the instantiated region for r2 will be passed (there will be no need to pass the instantiated region for r1). Whereas such a constraint may be satisfied when f is declared, it may likely not be satisfied at a particular instantiation site, which would suggest that there would be no put-effects in the region instantiated for r1!

Instead, what would be ok for a programmer to suggest is that the type scheme for f is as follows:

$$\forall e \forall r. \mbox{string}`r \,\stackrel{e}{\rightarrow} \, \tau \,\mbox{while}\, \{put\,r\} \#\# e$$