Disco.Compile

Compiling the typechecked, desugared AST to the untyped core language.

Documentation

compileThing :: (a -> Sem '[Fresh] DTerm) -> a -> Core

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

compileTerm :: ATerm -> Core

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

compileProperty :: AProperty -> Core

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

compileDefns :: Ctx ATerm Defn -> [(QName Core, Core)]

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.

compileDefnGroup :: Member Fresh r => [(QName ATerm, Defn)] -> Sem r [(QName Core, Core)]

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

compileDTerm :: Member Fresh r => DTerm -> Sem r Core

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

compilePrim :: Member Fresh r => Type -> Prim -> Sem r Core

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.

compilePrimErr :: Prim -> Type -> a

compileCase :: Member Fresh r => [DBranch] -> Sem r Core

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.

compileBranch :: Member Fresh r => DBranch -> Sem r Core

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 :: Member Fresh r => [DGuard] -> Name Core -> Core -> Sem r Core

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 :: Member Fresh r => DPattern -> Core -> Name Core -> Core -> Sem r Core

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.

compileUOp

Arguments

:: Type

Type of the operator argument

-> UOp

-> Core

Compile a unary operator.

compileBOp :: Type -> Type -> Type -> BOp -> Core

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