liquidhaskell-0.5.0.1: Liquid Types for Haskell

Safe HaskellNone
LanguageHaskell98

Language.Haskell.Liquid.Bare.Measure

Documentation

makeHaskellMeasures :: [CoreBind] -> ModName -> (ModName, BareSpec) -> BareM (MSpec SpecType DataCon) Source

makeHaskellInlines :: [CoreBind] -> ModName -> (ModName, BareSpec) -> BareM () Source

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

makeMeasureSpec :: (ModName, Spec BareType LocSymbol) -> BareM (MSpec SpecType DataCon) Source

makeMeasureSpec' :: MSpec (RType RTyCon RTyVar (UReft Reft)) DataCon -> ([(Var, RType RTyCon RTyVar (UReft Reft))], [(LocSymbol, RRType Reft)]) Source

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

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

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

varMeasures :: Monoid r => [Id] -> [(Symbol, Located (RType RTyCon RTyVar r))] Source