idris-0.9.17.1: Functional Programming Language with Dependent Types

Safe HaskellNone
LanguageHaskell98

IRTS.Defunctionalise

Documentation

data DExp Source

Constructors

DV LVar 
DApp Bool Name [DExp] 
DLet Name DExp DExp 
DUpdate Name DExp 
DProj DExp Int 
DC (Maybe LVar) Int Name [DExp] 
DCase CaseType DExp [DAlt] 
DChkCase DExp [DAlt] 
DConst Const 
DForeign FDesc FDesc [(FDesc, 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 DDecl Source

defunctionalise :: Int -> LDefs -> DDefs Source

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

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

eEVAL :: DExp -> DExp Source

data EvalApply a Source

Constructors

EvalCase (Name -> a) 
ApplyCase a 

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

toConsA :: [(Name, Int)] -> (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 -> Name Source

mkUnderCon :: Name -> Int -> Name Source

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

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

dumpDefuns :: DDefs -> String Source

module IRTS.Lang