idris

Safe HaskellNone

IRTS.Defunctionalise

Documentation

data DExp Source

Constructors

DV LVar 
DApp Bool Name [DExp] 
DLet Name DExp DExp 
DUpdate Name DExp 
DProj DExp Int 
DC Int Name [DExp] 
DCase DExp [DAlt] 
DChkCase DExp [DAlt] 
DConst Const 
DForeign FLang FType String [(FType, DExp)] 
DOp PrimFn [DExp] 
DNothing 
DError String 

Instances

data DAlt Source

Constructors

DConCase Int Name [Name] DExp 
DConstCase Const DExp 
DDefaultCase DExp 

Instances

data DDecl Source

Constructors

DFun Name [Name] DExp 
DConstructor Name Int Int 

Instances

type DDefs = Ctxt DDeclSource

defunctionalise :: Int -> LDefs -> DDefsSource

getFn :: [(Name, LDecl)] -> [(Name, Int)]Source

addApps :: LDefs -> (Name, LDecl) -> State [Name] (Name, DDecl)Source

eEVAL :: DExp -> DExpSource

data EvalApply a Source

Constructors

EvalCase (Name -> a) 
ApplyCase a 

toCons :: [Name] -> (Name, Int) -> [(Name, Int, EvalApply DAlt)]Source

mkApplyCase :: Name -> Int -> Int -> [(Name, Int, EvalApply DAlt)]Source

mkEval :: [(Name, Int, EvalApply DAlt)] -> (Name, DDecl)Source

mkApply :: [(Name, Int, EvalApply DAlt)] -> (Name, DDecl)Source

declare :: Int -> [(Name, Int, EvalApply DAlt)] -> [(Name, DDecl)]Source

genArgs :: Int -> [Name]Source

mkFnCon :: Show a => a -> NameSource

mkUnderCon :: Name -> Int -> NameSource

mkBigCase :: t -> Int -> DExp -> [DAlt] -> DExpSource

groupsOf :: Int -> [DAlt] -> [[DAlt]]Source

dumpDefuns :: DDefs -> StringSource

module IRTS.Lang