Language.Haskell.Liquid.Bare.Measure

This module contains (most of) the code needed to lift Haskell entitites, . code- (CoreBind), and data- (Tycon) definitions into the spec level.

Documentation

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]

makeMeasureSelectors converts the DataCons and creates the measures for the selectors and checkers that then enable reflection.

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))]