Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




imports :: TCM [ImportDecl] 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




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

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.

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.

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.

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.

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

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

Move somewhere else!

argpatts :: [NamedArg Pattern] -> [Pat] -> TCM [Pat] 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' ().

hslit :: Literal -> Literal Source

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

cdecl :: QName -> Nat -> ConDecl Source

tvaldecl Source


:: QName 
-> Induction

Is the type inductive or coinductive?

-> Nat 
-> Nat 
-> [ConDecl] 
-> Maybe Clause 
-> [Decl] 

infodecl :: QName -> Decl Source

hsCast :: Exp -> Exp Source

hsCast' :: Exp -> Exp Source

hsCoerce :: Exp -> Exp Source

writeModule :: Module -> TCM () Source

rteModule :: Module Source

outFile' :: (Pretty a, TransformBi ModuleName (Wrap a)) => a -> TCM (FilePath, FilePath) Source

outFile :: ModuleName -> TCM FilePath Source