Agda.Compiler.MAlonzo.Compiler

Synopsis

• compilerMain :: IsMain -> Interface -> TCM ()
• compile :: Interface -> TCM ()
• imports :: TCM [ImportDecl]
• definitions :: Definitions -> TCM [Decl]
• definition :: Maybe CoinductionKit -> Definition -> TCM [Decl]
• data CCEnv = CCEnv {
  • ccNameSupply :: NameSupply
  • ccCxt :: CCContext
  }
• type NameSupply = [Name]
• type CCContext = [Name]
• mapNameSupply :: (NameSupply -> NameSupply) -> CCEnv -> CCEnv
• mapContext :: (CCContext -> CCContext) -> CCEnv -> CCEnv
• initCCEnv :: CCEnv
• lookupIndex :: Int -> CCContext -> Name
• type CC = ReaderT CCEnv TCM
• freshNames :: Int -> ([Name] -> CC a) -> CC a
• intros :: Int -> ([Name] -> CC a) -> CC a
• checkConstructorType :: QName -> TCM [Decl]
• checkCover :: QName -> HaskellType -> Nat -> [QName] -> TCM [Decl]
• closedTerm :: TTerm -> TCM Exp
• term :: TTerm -> CC Exp
• compilePrim :: TPrim -> Exp
• alt :: Int -> TAlt -> CC Alt
• literal :: Literal -> TCM Exp
• hslit :: Literal -> Literal
• litString :: String -> Exp
• litqname :: QName -> Exp
• litqnamepat :: QName -> Pat
• condecl :: QName -> TCM (Nat, ConDecl)
• cdecl :: QName -> Nat -> ConDecl
• tvaldecl :: QName -> Induction -> Nat -> Nat -> [ConDecl] -> Maybe Clause -> [Decl]
• infodecl :: QName -> [Decl] -> [Decl]
• hsCast :: Exp -> Exp
• hsCast' :: Exp -> Exp
• hsCastApp :: Exp -> Exp
• hsCoerce :: Exp -> Exp
• copyRTEModules :: TCM ()
• writeModule :: Module -> TCM ()
• outFile' :: (Pretty a, TransformBi ModuleName (Wrap a)) => a -> TCM (FilePath, FilePath)
• outFile :: ModuleName -> TCM FilePath
• outFile_ :: TCM FilePath
• callGHC :: IsMain -> Interface -> TCM ()

Documentation

  type Infinity a b = b

  sharp :: a -> a
  sharp x = x

  flat :: a -> a
  flat x = x