Module Checker.IR

the module holding definitions of the ANF intermediate language used by the borrow checker.

type mutability = Syntax.mutability
type variable = int

the type of IR variables

type label = int

the type of labels used for identifying IR blocks

type source = Syntax.expr

the source of a IR value in the surface syntax. To save some memory, use source code locations instead of full surface syntax expressions

type var_kind =
| Tmp
| SrcVar

the kind of IR variables. Tmp means variables holding temporary expressions. These variables are always used exactly once, and it is safe to not consider them during borrow checking. SrcVar means variables corresponding to a program variable in the surface syntax.

val generator : < gen_label : label; gen_var : variable; reset : unit; >
val gen_var : unit -> variable
val gen_label : unit -> label
type path = path_node list
and path_node =
| Field of int

a field of a tuple

| Deref

data pointed by a borrow

type lvalue = {
lv_src : source;
lv_var : variable;
lv_path : path;
}

a lvalue is a value that corresponds to a memory location and can be assigned to.

type value =
| Loc of lvalue
| Lit of int
type expr =
| Val of value
| Fun of string
| Borrow of mutability * lvalue
| Assign of lvalue * value
| App of value * value list
| Tuple of value list
| ExitScope of variable list * value

ExitScope(vars, value) means leaving a scope with variables vars, returning value as the result of the whole scope. The point of having this construct is, after dropping vars, value may become invalid. By combining the operations of dropping variables and returning from a scope, the borrow checker and identify this kind of patterns and correctly handle them.

type program =
| Jump of label * value
| Decl of variable * expr * program
| If of value * program * program
| Block of block * program
| Loop of block
  • Block(blk, body) defines a non-recursive block blk, and then executes body, which may jump to blk
  • Loop blk defines a recursive block blk, and executes the block immediately. The parameter of blk is of type Int and is meaningless
and block = {
blk_label : label;
blk_param : variable;
blk_body : program;
}
type function_def = {
func_src : Syntax.function_def;
func_name : string;
func_label : label;
func_params : variable list;
func_body : program;
}

func_label is used to record the state of execution after the function returns

module VarMap : sig ... end