Explicit regions support

[melsman]

This pull-request initiates the support for explicit region annotations. The idea is to implement a system that is compatible with using plain Standard ML and in particular in such a way that Standard ML code compiled with the MLKit with regions can work well with the enriched source code files.

We use D to range over numbers, F to range over floating point numbers, S to range over strings, and C to range over constructors. Here is a summary of the added syntactic features:

dec ::= ... 
          | region r1 ... rn 
          | fun f `[r1 ... rn] atpat = exp
          | fun f `r atpat = exp
exp ::= ...
          | D | S`r | F`r | C`r 
          | C`r atexp
          | f `[r1 ... rn] atexp 
          | f `r atexp 
          | (exp,...,exp)`r 
          | {lab=exp,...,lab=exp}`r

Notice that immediate integers cannot be annotated (integers are not boxed) whereas strings and reals can.

Trying it

The added syntactic forms are supported when the mlkit executable is passed the flag --explicit_regions (short: -er). Consider compiling the file er1.sml:

fun g `[r] () = 4
fun f `[r2 r3 r1] () =
    let region r r8
        val v = g `[r2] ()
    in (v,v)
    end

Here is the result:

$ SML_LIB=.. ../bin/mlkit -Ppeast -no_gc -no_basislib --maximum_inline_size 0 -er er1.sml
[reading source file:	er1.sml]AST after elaboration:
val rec g [r] = fn {} => 4; 
val rec f [r2,r3,r1] = fn {} => let (region r r8; val v = g [r2] {}) in {1 = v, 2 = v} end
AST after opacity elimination:
val rec g [r] = fn {} => 4; 
val rec f [r2,r3,r1] = fn {} => let (region r r8; val v = g [r2] {}) in {1 = v, 2 = v} end[wrote X64 code file:	MLB/RI/er1.sml.s]
[wrote X64 code file:	MLB/RI/base-link_objects.s]
[wrote executable file:	run]

Features

• Support for allocation annotations in expressions:
  • Immediate strings and reals
  • Records and tuples
  • Function calls
  • Constructors (incl. ref)
• Early checks:
  • Check for duplicate region variables in region declarations.
  • Check for duplicate region variable parameters in function declarations.
  • Check that region variables are not scoped multiple times. Such a check is implemented by including the set of scoped region variables in the context.
• Extend CompileDec to compile region declarations into a letregion r in e construct.
• Extend CompileDec to compile allocation annotations properly.
• Finally, when compiling from LambdaExp to RegionExp, we need to make sure that the region annotations are enforced, which could result in error messages.
• We need to make sure that OptLambda preserves the region annotations when performing optimisations.

Future Features

Here is a list of some wishful future features:

• Support for region annotations in types:

  ty ::= ...
         | t`r | {lab:ty,...,lab:ty}`r
         | (ty * ty)`r | ty ->`r ty
  

• Extend CompileDec to compile region annotations in types into region annotations in LambdaExp types.

• We would also like support for writing effects in types.

• Make sure that OptLambda preserves the type annotations when performing optimisations, which can be tricky.

Design decisions

• Do not associate explicit region variables with region types.
  We could support that an explicit region variable is associated with a region type, which would allow the compiler to check early (before explicit region variables are associated with proper region variables) the consistent use of region variables. We could also just leave this check to the proper region variable system, which is what is implemented.

• Early checks. Another obvious strategy is to check early certain properties of the region annotations (before SpreadExpression and RegInf). Here are some properties we can check at ElabDec level:

  • No region duplicates in region decs
  • No region parameter duplicates in function definitions
  • Regions are in scope when referred to (assume all module decs are closed but that regions greg_top, greg_pair, greg_triple, greg_string, and greg_ref are in scope.)
  • Regions are not scoped multiple times. This restriction is also implemented for explicit type variables; it is not the best feature, but it allows us to move other checks to the later LambdaExp level. At the LambdaExp level, however, we need to be more clever, as OptLambda is performing inlining and such, which may require us to perform renaming of region variables.

We can leave other elaboration issues to the lower levels (LambdaExp and SpreadExpression / RegInf).

Further Ideas

• The mlkit could support rml-files (Region ML) and enable the flag -er implicitly.