Language.Haskell.Liquid.Transforms.CoreToLogic

Documentation

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

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

coreToLogic :: Bool -> 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 => Bool -> Type -> RRType r

inlineSpecType :: Bool -> Var -> SpecType

NOTE:inlineSpecType type

the refinement depends on whether the result type is a Bool or not: CASE1: measure flogic :: X -> Bool = fhaskell :: x:X -> {v:Bool | v = (flogic x)} CASE2: measure flogic :: X -> Y = fhaskell :: x:X -> {v:Y | v = (flogic x)}

measureSpecType :: Bool -> Var -> SpecType

Refine types of measures: keep going until you find the last data con! this code is a hack! we refine the last data constructor, it got complicated to support both 1. multi parameter measures (see testsposHasElem.hs) 2. measures returning functions (fromReader :: Reader r a -> (r -> a) ) TODO: SIMPLIFY by dropping support for multi parameter measures

weakenResult :: Bool -> Var -> SpecType -> SpecType

'weakenResult foo t' drops the singleton constraint `v = foo x y` that is added, e.g. for measures in /strengthenResult'. This should only be used _when_ checking the body of foo where the output, is, by definition, equal to the singleton.

normalize :: Simplify a => Bool -> a -> a

Orphan instances

Show CoreExpr

Methods

showsPrec :: Int -> CoreExpr -> ShowS

show :: CoreExpr -> String

showList :: [CoreExpr] -> ShowS