liquidhaskell-0.6.0.0: Liquid Types for Haskell

Safe HaskellNone
LanguageHaskell98

Language.Haskell.Liquid.Constraint.ProofToCore

Synopsis

Documentation

type HId = Id Source

combineProofs :: CmbExpr -> CoreExpr -> [CoreExpr] -> CoreExpr Source

combineProofs :: combinator -> default expressions -> list of proofs | -> combined result

combine :: Show t1 => [t1] -> (Expr Var -> t -> Expr Var) -> Expr Var -> [t] -> Expr Var Source

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

anf :: ([CoreBind], [CoreExpr], [Int]) -> CoreExpr -> ([CoreBind], [CoreExpr], [Int]) Source

ANF

makeDictionaries :: Id -> CoreExpr -> [Expr b] Source

Filling up dictionaries

instantiateVars :: [(Var, Type)] -> Expr CoreBndr -> Expr CoreBndr Source

Filling up types

resolveVs :: [Id] -> [(Type, Type)] -> [(Id, Type)] Source

resolveVar :: Var -> Type -> [(Var, Type)] -> Type Source

substTyV :: (Id, Type) -> (Type, Type) -> (Type, Type) Source

varCombine :: Show a => a -> Type -> Var Source

varANF :: Show a => a -> Type -> Var Source

varANFPr :: Show a => a -> Type -> Var Source

bkArrow :: Type -> ([Var], [Type]) Source