| 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 :: Config -> GhcSrc -> TycEnv -> LogicMap -> BareSpec -> [Measure (Located BareType) (Located LHName)]
- makeHaskellInlines :: Config -> GhcSrc -> TCEmb TyCon -> LogicMap -> BareSpec -> [(LocSymbol, LMap)]
- makeHaskellDataDecls :: 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)], [(Located LHName, RRType Reft)])
- makeOpaqueReflMeasures :: Env -> MeasEnv -> ModSpecs -> [(Var, LocSpecType, Equation)] -> ([MSpec SpecType DataCon], [(Var, Measure LocBareType ctor)])
- getReflDCs :: MeasEnv -> [Var] -> HashSet DataCon
- varMeasures :: IsReft r => Env -> [(Symbol, Located (RRType r))]
- getMeasVars :: Env -> MeasEnv -> [(Symbol, Located (RRType Reft))]
- makeClassMeasureSpec :: MSpec (RType c tv (UReft r2)) t -> [(Located LHName, CMeasure (RType c tv r2))]
- varLocSym :: Var -> LocSymbol
Documentation
makeHaskellMeasures :: Config -> GhcSrc -> TycEnv -> LogicMap -> BareSpec -> [Measure (Located BareType) (Located LHName)] Source #
makeHaskellInlines :: Config -> 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 #
makeMeasureSpec' :: Bool -> MSpec SpecType DataCon -> ([(Var, SpecType)], [(Located LHName, RRType Reft)]) Source #
makeOpaqueReflMeasures :: Env -> MeasEnv -> ModSpecs -> [(Var, LocSpecType, Equation)] -> ([MSpec SpecType DataCon], [(Var, Measure LocBareType ctor)]) Source #