Module Checker

If you are interested in how the borrow checker of this demo is implemented, you may read through the modules in the Interesting Modules section. The modules in the Internal Helper Modules section are mainly for testing/presentation purpose, and are not related to the mechanisms of the borrow checker.

The recommended order to read the source code from scratch is:

  1. Syntax
  2. IR
  3. the interface of Typecheck
  4. (Typecheck at anytime if you are interested how the IR is generated)
  5. the interface and document of Location
  6. the interface and document of Type
  7. ComputeConstraint
  8. Check
  9. implementations of Location, Type that you are interested in

The overall structure of the borrow checker is:

  1. the surface syntax tree is converted to IR
  2. in the first phase, constraints (see Location.ConstrSet) representing alias information and owner information of borrows are computed. The main functionality of this phase is to compute the constraint fixed-point for loops. See ComputeConstraint for more details
  3. in the second phase, the set of invalid locations are tracked, and uses of invalid locations are detected and reported. The uses of some invalid locations (those that are invalidated in a loop and used incorrectly in the next loop. See "loop/effect-of-prev-loop2" in Examples for a concrete example) cannot be detected at this phase. This kind of invalid locations are recorded after this phase, and the next phase detect incorrect uses of them
  4. in the third phase, the invalid uses of the aforementioned loop-related locations are detected, using information recorded in the second phase

Interesting Modules

module Syntax : sig ... end

the module holding definitions of the surface syntax of the demo language, including expressions, programs, and syntactic types.

module IR : sig ... end

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

module Typecheck : sig ... end

the module that performs type checking (not borrow checking) and convert a source program into the ANF IR. This module also defines a data structure holding source information that link IR values to their source in the surface syntax. See Typecheck.type_info

module Location : sig ... end

the module for locations, a compile-time notion of memory locations. This is the object that the borrow checker use to represent and track values at compile-time This module also contains some important location-related helper data structures.

module Type : sig ... end

the module holding the definition of semantic types, and various operations on them

module ComputeConstraint : sig ... end

the module holding constraint generation primitives of the borrow checker. It contains the first phase of the borrow checker, as well as several utilities used by later phases.

module Check : sig ... end

the module holding the second and third phases of the borrow checker.

Internal Helper Modules

module Pretty : sig ... end
module Parser : sig ... end
module Lexer : sig ... end
module Examples : sig ... end
val check_program : Syntax.function_def list -> unit

check_program functions combines all modules and phases of the borrow checker, and perform a complete check on functions. If it returns normally, there's no error in functions, otherwise an exception is raised.