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

makeHaskellDataDecls :: Config -> BareSpec -> [TyCon] -> [DataDecl]

makeHaskellMeasures :: TCEmb TyCon -> [CoreBind] -> BareSpec -> BareM [Measure (Located BareType) LocSymbol]

makeHaskellInlines :: TCEmb TyCon -> [CoreBind] -> BareSpec -> BareM [(LocSymbol, LMap)]

makeHaskellBounds :: TCEmb TyCon -> CoreProgram -> HashSet (Var, LocSymbol) -> BareM RBEnv

makeMeasureSpec :: (ModName, BareSpec) -> BareM (MSpec SpecType DataCon)

makeMeasureSpec' :: MSpec SpecType DataCon -> ([(Var, SpecType)], [(LocSymbol, RRType Reft)])

makeClassMeasureSpec :: MSpec (RType c tv (UReft r2)) t -> [(LocSymbol, CMeasure (RType c tv r2))]

makeMeasureSelectors :: Config -> DataConMap -> (DataCon, Located DataConP) -> [Measure SpecType DataCon]

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

strengthenHaskellMeasures :: HashSet (Located Var) -> [(Var, LocSpecType)] -> [(Var, LocSpecType)]

strengthenHaskellInlines :: HashSet (Located Var) -> [(Var, LocSpecType)] -> [(Var, LocSpecType)]

varMeasures :: Monoid r => [Var] -> [(Symbol, Located (RRType r))]