Language.Haskell.Liquid.Transforms.CoreToLogic

Documentation

coreToDef :: Reftable r => LocSymbol -> Var -> CoreExpr -> LogicM [Def (Located (RRType r)) DataCon]

coreToFun :: LocSymbol -> Var -> CoreExpr -> LogicM ([Var], Either Expr Expr)

coreToLogic :: CoreExpr -> LogicM Expr

mkLit :: Literal -> Maybe Expr

mkI :: Integer -> Maybe Expr

mkS :: ByteString -> Maybe Expr

runToLogic :: TCEmb TyCon -> LogicMap -> DataConMap -> (String -> Error) -> LogicM t -> Either Error t

runToLogicWithBoolBinds :: [Var] -> TCEmb TyCon -> LogicMap -> DataConMap -> (String -> Error) -> LogicM t -> Either Error t

logicType :: Reftable r => Type -> RRType r

strengthenResult :: Var -> SpecType

strengthenResult' :: Var -> SpecType

normalize :: Simplify a => a -> a

Orphan instances

Show CoreExpr

Methods

showsPrec :: Int -> CoreExpr -> ShowS

show :: CoreExpr -> String

showList :: [CoreExpr] -> ShowS