| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Haskell.Liquid.Transforms.CoreToLogic
Contents
Synopsis
- coreToDef :: IsReft r => Located LHName -> 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 -> Expr
- runToLogic :: TCEmb TyCon -> LogicMap -> DataConMap -> Config -> (String -> Error) -> LogicM t -> Either Error t
- runToLogicWithBoolBinds :: [Var] -> TCEmb TyCon -> LogicMap -> DataConMap -> Config -> (String -> Error) -> LogicM t -> Either Error t
- logicType :: IsReft r => Bool -> Type -> RRType r
- inlineSpecType :: Bool -> Var -> SpecType
- measureSpecType :: Bool -> Var -> SpecType
- weakenResult :: Bool -> Var -> SpecType -> SpecType
- normalizeCoreExpr :: Bool -> CoreExpr -> CoreExpr
Documentation
coreToDef :: IsReft r => Located LHName -> Var -> CoreExpr -> LogicM [Def (Located (RRType r)) DataCon] Source #
coreToLogic :: CoreExpr -> LogicM Expr Source #
mkS :: ByteString -> Expr Source #
runToLogic :: TCEmb TyCon -> LogicMap -> DataConMap -> Config -> (String -> Error) -> LogicM t -> Either Error t Source #
runToLogicWithBoolBinds :: [Var] -> TCEmb TyCon -> LogicMap -> DataConMap -> Config -> (String -> Error) -> LogicM t -> Either Error t Source #
measureSpecType :: Bool -> 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 :: Bool -> 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.
normalizeCoreExpr :: Bool -> CoreExpr -> CoreExpr Source #
'normalizeCoreExpr allowTC e' simplifies the Core expression e by:
1. inlining predicates (i.e. applications of measures that return Bool)
2. inlining ANF variables (i.e. variables that are introduced by the ANF transformation)
3. simplifying the expression by removing dead binders and applications of
type arguments and dictionaries.
The allowTC flag controls whether type class dictionaries are considered erasable
and will be removed from the expression.