Safe Haskell | None |
---|---|
Language | Haskell98 |
- type HId = Id
- type HVar = Var HId
- type HAxiom = Axiom HId
- type HCtor = Ctor HId
- type HVarCtor = VarCtor HId
- type HQuery = Query HId
- type HInstance = Instance HId
- type HProof = Proof HId
- type HExpr = Expr HId
- type CmbExpr = CoreExpr -> CoreExpr -> CoreExpr
- class ToCore a where
- combineProofs :: CmbExpr -> CoreExpr -> [CoreExpr] -> CoreExpr
- combine :: Show t1 => [t1] -> (Expr Var -> t -> Expr Var) -> Expr Var -> [t] -> Expr Var
- makeApp :: CoreExpr -> [CoreExpr] -> CoreExpr
- anf :: ([CoreBind], [CoreExpr], [Int]) -> CoreExpr -> ([CoreBind], [CoreExpr], [Int])
- makeDictionaries :: Id -> CoreExpr -> [Expr b]
- makeDictionary :: Id -> Type -> Expr b
- instantiateVars :: [(Var, Type)] -> Expr CoreBndr -> Expr CoreBndr
- resolveVs :: [Id] -> [(Type, Type)] -> [(Id, Type)]
- resolveVar :: Var -> Type -> [(Var, Type)] -> Type
- substTyV :: (Id, Type) -> (Type, Type) -> (Type, Type)
- varCombine :: Show a => a -> Type -> Var
- varANF :: Show a => a -> Type -> Var
- varANFPr :: Show a => a -> Type -> Var
- bkArrow :: Type -> ([Var], [Type])
Documentation
combineProofs :: CmbExpr -> CoreExpr -> [CoreExpr] -> CoreExpr Source
combineProofs :: combinator -> default expressions -> list of proofs | -> combined result
makeApp :: CoreExpr -> [CoreExpr] -> CoreExpr Source
To make application we need to instantiate expressions irrelevant to logic | type application and dictionaries. | Then, ANF the final expression
makeDictionaries :: Id -> CoreExpr -> [Expr b] Source
Filling up dictionaries
makeDictionary :: Id -> Type -> Expr b Source
varCombine :: Show a => a -> Type -> Var Source