Internal Compiler API

If you want to write a plugin for LM, then it may be necessary to interface with compiler objects. These APIs presented here are stable and will be supported by their nominal type signature.

If something is not present here in the type signature, then it may not be stable. For example, destructuring types used in these functions may be unstable.

Type Definitions

Types here should be treated as opaque, even if they are not defined as explicitly opaque.

# Terms are defined more generally as an AST node
# Not all AST nodes are valid terms
type AST;

# Types are just called `Type`s
type Type;

# `TypeContext`s store all information necessary to validate logical inferences and judgements
type TypeContext;

# `SourceLocation`s should ideally be a Span, but currently they are just File Line/Columns
type SourceLocation;

Global Indexes

Global indexes are accessible through helper functions.

# var-to-def-index permits lookup from variable reference to variable definition
#
# a variable reference will resolve to either
#    a local variable: finding the original local binding definition
#    a global variable: finding the original global binding definition
#
#    if the variable definition is specialized, then the specialized version will be referenced
#
let var-to-def(var: AST): AST;

Type Constructors

Ground types have short-hand constructors.

# Ground Types
let t0(tag: String): Type;
let t1(tag: String, p1: Type): Type;
let t2(tag: String, p1: Type, p2: Type): Type;
let t3(tag: String, p1: Type, p2: Type, p3: Typ): Type;

# Type Variables
let tv(tag: String): Type;

# Top Type
let ta: Type;

# Conjunction
let $"&&"(lt: Type, rt: Type): Type;

Type Destructors

Ground types have short-hand destructors.

# Get the tag of a ground type
let .tag(tt: Type): String; # T<a,b,c,d> .tag = T

# Get type parameter, starting from left (l1) moving left (l2), (l3), ...
let .l1(tt: Type): Type;    # T<a,b,c,d> .l1 = a
let .l2(tt: Type): Type;    # T<a,b,c,d> .l2 = b
let .l3(tt: Type): Type;    # T<a,b,c,d> .l3 = c
let .l4(tt: Type): Type;    # T<a,b,c,d> .l4 = d
let .l(tt: Type, i: USize): Type; # ...

# Get type parameter, starting from right (r1) moving left (r2), (r3), ...
let .r1(tt: Type): Type;    # T<a,b,c,d> .r1 = d
let .r2(tt: Type): Type;    # T<a,b,c,d> .r2 = c
let .r3(tt: Type): Type;    # T<a,b,c,d> .r3 = b
let .r4(tt: Type): Type;    # T<a,b,c,d> .r4 = a
let .r(tt: Type, i: USize): Type; # ...

Type Normalization

Types have a normal form with minimal inferable information, and a denormal form with maximal inferable information. Super-normal form refers to the type of a left-hand-side binding such as a variable, which may discard some information.

let normalize(tt: Type): Type;
let denormalize(tt: Type): Type;
let supernormalize(tt: Type): Type;

Unification

Unification is a process by which type information is compared or merged. can-unify is much faster than unify.

let can-unify(supertype: Type, subtype: Type): Bool;
let unify(supertype: Type, subtype: Type): TypeContext?;

AST Constructors

The AST is starting to stabilize.

let mk-lit(val: String): AST;

let mk-var(val: String): AST;

let mk-atype(tt: Type): AST;
let .ascript(t: AST, tt: Type): AST;

let mk-app(l: AST, r: AST): AST;
let mk-cons(l: AST, r: AST): AST;

let .with-location(t: AST, loc: SourceLocation): AST;

Conveniences

These methods are provided for common convenience.

let .into(t: AST, tgt: Type<String>): String;
let .into(tt: Type, tgt: Type<String>): String;