| Safe Haskell | None |
|---|---|
| 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 :: GhcSrc -> TycEnv -> LogicMap -> BareSpec -> [Measure (Located BareType) LocSymbol]
- makeHaskellInlines :: 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) -> MSpec SpecType DataCon
- makeMeasureSpec' :: 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 :: GhcSrc -> TycEnv -> LogicMap -> BareSpec -> [Measure (Located BareType) LocSymbol] #
makeMeasureSelectors :: Config -> DataConMap -> Located DataConP -> [Measure SpecType DataCon] #
makeMeasureSelectors converts the DataCons and creates the measures for
the selectors and checkers that then enable reflection.