Safe Haskell	None
Language	Haskell98

Language.Haskell.Liquid.Transforms.CoreToLogic

Contents

Orphan instances

Synopsis

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
inlineSpecType :: Var -> SpecType
measureSpecType :: Var -> SpecType
weakenResult :: Var -> SpecType -> SpecType
normalize :: Simplify a => a -> a

Documentation

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

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

coreToLogic :: CoreExpr -> LogicM Expr Source #

mkLit :: Literal -> Maybe Expr Source #

mkI :: Integer -> Maybe Expr Source #

mkS :: ByteString -> Maybe Expr Source #

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

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

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

inlineSpecType :: Var -> SpecType Source #

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 :: Var -> SpecType Source #

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 :: Var -> SpecType -> SpecType Source #

'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 => a -> a Source #

Orphan instances

Show CoreExpr Source #
Instance details Methods showsPrec :: Int -> CoreExpr -> ShowS # show :: CoreExpr -> String # showList :: [CoreExpr] -> ShowS #