Safe Haskell	None
Language	Haskell98

Agda.Compiler.MAlonzo.Compiler

Synopsis

Documentation

compilerMain :: Bool -> Interface -> TCM () Source

compile :: Interface -> TCM () Source

imports :: TCM [ImportDecl] Source

definitions :: Definitions -> TCM [Decl] Source

definition :: Maybe CoinductionKit -> Definition -> TCM [Decl] Source

Note that the INFINITY, SHARP and FLAT builtins are translated as follows (if a CoinductionKit is given):

  type Infinity a b = b

  sharp :: a -> a
  sharp x = x

  flat :: a -> a
  flat x = x

data CCEnv Source

Environment for naming of local variables. Invariant: reverse ccCxt ++ ccNameSupply

Constructors

CCEnv
Fields ccFunName :: Maybe QName Agda function we are currently compiling. ccNameSupply :: NameSupply Supply of fresh names ccCxt :: CCContext Names currently in scope ccCatchAll :: Maybe CompiledClauses Naive catch-all implementation. If an inner case has no catch-all clause, we use the one from its parent.

type NameSupply = [Name] Source

type CCContext = [Name] Source

mapNameSupply :: (NameSupply -> NameSupply) -> CCEnv -> CCEnv Source

mapContext :: (CCContext -> CCContext) -> CCEnv -> CCEnv Source

initCCEnv :: Maybe QName -> CCEnv Source

Initial environment for expression generation.

lookupIndex :: Int -> CCContext -> Name Source

Term variables are de Bruijn indices.

lookupLevel :: Int -> CCContext -> Name Source

Case variables are de Bruijn levels.

type CC = ReaderT CCEnv TCM Source

casetree :: CompiledClauses -> CC Exp Source

Compile a case tree into nested case and record expressions.

updateCatchAll :: Maybe CompiledClauses -> CC a -> CC a Source

Replace the current catch-all clause with a new one, if given.

conAlts :: Int -> Map QName (WithArity CompiledClauses) -> CC [Alt] Source

litAlts :: Map Literal CompiledClauses -> CC [Alt] Source

catchAllAlts :: Maybe CompiledClauses -> CC [Alt] Source

branch :: Pat -> CompiledClauses -> CC Alt Source

replaceVar :: Int -> Int -> ([Name] -> CC a) -> CC a Source

Replace de Bruijn Level x by n new variables.

mkRecord :: Map QName Exp -> CC Exp Source

Precondition: Map not empty.

recConFromProj :: QName -> TCM ConHead Source

lambdasUpTo :: Int -> CC Exp -> CC Exp Source

Introduce lambdas such that n variables are in scope.

lambdas :: Int -> CC Exp -> CC Exp Source

Introduce n lambdas.

intros :: Int -> ([Name] -> CC Exp) -> CC Exp Source

Introduce n variables into the context.

mkLams :: [Name] -> Exp -> Exp Source

Prefix a Haskell expression with lambda abstractions.

checkConstructorType :: QName -> TCM [Decl] Source

checkCover :: QName -> HaskellType -> Nat -> [QName] -> TCM [Decl] Source

conArityAndPars :: QName -> TCM (Nat, Nat) Source

Move somewhere else!

clause :: QName -> Maybe String -> (Nat, Bool, Clause) -> TCM Decl Source

argpatts :: [NamedArg Pattern] -> [Pat] -> TCM [Pat] Source

clausebody :: ClauseBody -> TCM Exp Source

closedTerm :: Term -> TCM Exp Source

term :: Term -> CC Exp Source

Extract Agda term to Haskell expression. Irrelevant arguments are extracted as (). Types are extracted as (). DontCare outside of irrelevant arguments is extracted as error.

term' :: Arg Term -> CC Exp Source

Irrelevant arguments are replaced by Haskells' ().

literal :: Literal -> TCM Exp Source

hslit :: Literal -> Literal Source

litqname :: QName -> Exp Source

litqnamepat :: QName -> Pat Source

condecl :: QName -> TCM (Nat, ConDecl) Source

cdecl :: QName -> Nat -> ConDecl Source

tvaldecl Source

Arguments