Documentation

Utility function to desugar and compile a thing, given a desugaring function for it.

Compile a typechecked term (ATerm) directly to a Core term, by desugaring and then compiling.

Compile a typechecked property (AProperty) directly to a Core term, by desugaring and then compilling.

Compile a context of typechecked definitions (Defn) to a sequence of compiled Core bindings, such that the body of each binding depends only on previous ones in the list. First topologically sorts the definitions into mutually recursive groups, then compiles recursive definitions specially in terms of delay and force.

Compile a group of mutually recursive definitions, using delay to compile recursion via references to memory cells.

Compile a typechecked, desugared DTerm to an untyped Core term.

Compile a natural number. A separate function is needed in case the number is of a finite type, in which case we must mod it by its type. compileNat :: Member Fresh r => Type -> Integer -> Sem r Core compileNat (TyFin n) x = return $ CNum Fraction ((x mod n) % 1) compileNat _ x = return $ CNum Fraction (x % 1)

Compile a primitive. Typically primitives turn into a corresponding function constant in the core language, but sometimes the particular constant it turns into may depend on the type.

Compile a case expression of type τ to a core language expression of type (Unit → τ), in order to delay evaluation until explicitly applying it to the unit value.

Compile a branch of a case expression of type τ to a core language expression of type (Unit → τ) → τ. The idea is that it takes a failure continuation representing the subsequent branches in the case expression. If the branch succeeds, it just returns the associated expression of type τ; if it fails, it calls the continuation to proceed with the case analysis.

compileGuards takes a list of guards, the name of the failure continuation of type (Unit → τ), and a Core term of type τ to return in the case of success, and compiles to an expression of type τ which evaluates the guards in sequence, ultimately returning the given expression if all guards succeed, or calling the failure continuation at any point if a guard fails.

compileMatch takes a pattern, the compiled scrutinee, the name of the failure continuation, and a Core term representing the compilation of any guards which come after this one, and returns a Core expression of type τ that performs the match and either calls the failure continuation in the case of failure, or the rest of the guards in the case of success.

Compile a unary operator.

Compile a binary operator. This function needs to know the types of the arguments and result since some operators are overloaded and compile to different code depending on their type.

arg1 ty -> arg2 ty -> result ty -> op -> result