| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell98 |
Language.Haskell.Liquid.Bare.Measure
Description
This module contains (most of) the code needed to lift Haskell entitites, . code- (CoreBind), and data- (Tycon) definitions into the spec level.
Synopsis
- makeHaskellMeasures :: Bool -> GhcSrc -> TycEnv -> LogicMap -> BareSpec -> [Measure (Located BareType) LocSymbol]
- makeHaskellInlines :: Bool -> GhcSrc -> TCEmb TyCon -> LogicMap -> BareSpec -> [(LocSymbol, LMap)]
- makeHaskellDataDecls :: Config -> ModName -> BareSpec -> [TyCon] -> [DataDecl]
- makeMeasureSelectors :: Config -> DataConMap -> Located DataConP -> [Measure SpecType DataCon]
- makeMeasureSpec :: Env -> SigEnv -> ModName -> (ModName, BareSpec) -> Lookup (MSpec SpecType DataCon)
- makeMeasureSpec' :: Bool -> MSpec SpecType DataCon -> ([(Var, SpecType)], [(LocSymbol, RRType Reft)])
- varMeasures :: Monoid r => Env -> [(Symbol, Located (RRType r))]
- makeClassMeasureSpec :: MSpec (RType c tv (UReft r2)) t -> [(LocSymbol, CMeasure (RType c tv r2))]
Documentation
makeHaskellMeasures :: Bool -> GhcSrc -> TycEnv -> LogicMap -> BareSpec -> [Measure (Located BareType) LocSymbol] Source #
makeHaskellInlines :: Bool -> GhcSrc -> TCEmb TyCon -> LogicMap -> BareSpec -> [(LocSymbol, LMap)] Source #
makeMeasureSelectors :: Config -> DataConMap -> Located DataConP -> [Measure SpecType DataCon] Source #
makeMeasureSelectors converts the DataCons and creates the measures for
the selectors and checkers that then enable reflection.
makeMeasureSpec :: Env -> SigEnv -> ModName -> (ModName, BareSpec) -> Lookup (MSpec SpecType DataCon) Source #