liquidhaskell-0.8.0.2: Liquid Types for Haskell

Safe HaskellNone
LanguageHaskell98

Language.Haskell.Liquid.Measure

Contents

Synopsis

Specifications

data Spec ty bndr Source #

Constructors

Spec 

Fields

Instances

Binary BareSpec Source # 

Methods

put :: BareSpec -> Put #

get :: Get BareSpec #

putList :: [BareSpec] -> Put #

Generic (Spec ty bndr) Source # 

Associated Types

type Rep (Spec ty bndr) :: * -> * #

Methods

from :: Spec ty bndr -> Rep (Spec ty bndr) x #

to :: Rep (Spec ty bndr) x -> Spec ty bndr #

Monoid (Spec ty bndr) Source # 

Methods

mempty :: Spec ty bndr #

mappend :: Spec ty bndr -> Spec ty bndr -> Spec ty bndr #

mconcat :: [Spec ty bndr] -> Spec ty bndr #

type Rep (Spec ty bndr) Source # 
type Rep (Spec ty bndr) = D1 (MetaData "Spec" "Language.Haskell.Liquid.Measure" "liquidhaskell-0.8.0.2-4zWDXa3VLIUKANK5k7Jte1" False) (C1 (MetaCons "Spec" PrefixI True) ((:*:) ((:*:) ((:*:) ((:*:) ((:*:) (S1 (MetaSel (Just Symbol "measures") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [Measure ty bndr])) (S1 (MetaSel (Just Symbol "asmSigs") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [(LocSymbol, ty)]))) ((:*:) (S1 (MetaSel (Just Symbol "sigs") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [(LocSymbol, ty)])) (S1 (MetaSel (Just Symbol "localSigs") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [(LocSymbol, ty)])))) ((:*:) ((:*:) (S1 (MetaSel (Just Symbol "reflSigs") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [(LocSymbol, ty)])) (S1 (MetaSel (Just Symbol "invariants") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [ty]))) ((:*:) (S1 (MetaSel (Just Symbol "ialiases") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [(ty, ty)])) (S1 (MetaSel (Just Symbol "imports") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [Symbol]))))) ((:*:) ((:*:) ((:*:) (S1 (MetaSel (Just Symbol "dataDecls") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [DataDecl])) (S1 (MetaSel (Just Symbol "newtyDecls") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [DataDecl]))) ((:*:) (S1 (MetaSel (Just Symbol "includes") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [FilePath])) (S1 (MetaSel (Just Symbol "aliases") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [RTAlias Symbol BareType])))) ((:*:) ((:*:) (S1 (MetaSel (Just Symbol "ealiases") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [RTAlias Symbol Expr])) (S1 (MetaSel (Just Symbol "embeds") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (TCEmb LocSymbol)))) ((:*:) (S1 (MetaSel (Just Symbol "qualifiers") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [Qualifier])) ((:*:) (S1 (MetaSel (Just Symbol "decr") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [(LocSymbol, [Int])])) (S1 (MetaSel (Just Symbol "lvars") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [LocSymbol]))))))) ((:*:) ((:*:) ((:*:) ((:*:) (S1 (MetaSel (Just Symbol "lazy") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (HashSet LocSymbol))) (S1 (MetaSel (Just Symbol "reflects") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (HashSet LocSymbol)))) ((:*:) (S1 (MetaSel (Just Symbol "autois") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (HashMap LocSymbol (Maybe Int)))) (S1 (MetaSel (Just Symbol "hmeas") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (HashSet LocSymbol))))) ((:*:) ((:*:) (S1 (MetaSel (Just Symbol "hbounds") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (HashSet LocSymbol))) (S1 (MetaSel (Just Symbol "inlines") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (HashSet LocSymbol)))) ((:*:) (S1 (MetaSel (Just Symbol "autosize") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (HashSet LocSymbol))) (S1 (MetaSel (Just Symbol "pragmas") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [Located String]))))) ((:*:) ((:*:) ((:*:) (S1 (MetaSel (Just Symbol "cmeasures") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [Measure ty ()])) (S1 (MetaSel (Just Symbol "imeasures") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [Measure ty bndr]))) ((:*:) (S1 (MetaSel (Just Symbol "classes") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [RClass ty])) (S1 (MetaSel (Just Symbol "termexprs") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [(LocSymbol, [Located Expr])])))) ((:*:) ((:*:) (S1 (MetaSel (Just Symbol "rinstance") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [RInstance ty])) (S1 (MetaSel (Just Symbol "dvariance") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [(LocSymbol, [Variance])]))) ((:*:) (S1 (MetaSel (Just Symbol "bounds") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (RRBEnv ty))) ((:*:) (S1 (MetaSel (Just Symbol "defs") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 (HashMap LocSymbol Symbol))) (S1 (MetaSel (Just Symbol "axeqs") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 [AxiomEq])))))))))

data MSpec ty ctor Source #

Constructors

MSpec 

Fields

Instances

Bifunctor MSpec Source # 

Methods

bimap :: (a -> b) -> (c -> d) -> MSpec a c -> MSpec b d #

first :: (a -> b) -> MSpec a c -> MSpec b c #

second :: (b -> c) -> MSpec a b -> MSpec a c #

Functor (MSpec ty) Source # 

Methods

fmap :: (a -> b) -> MSpec ty a -> MSpec ty b #

(<$) :: a -> MSpec ty b -> MSpec ty a #

(Data ctor, Data ty) => Data (MSpec ty ctor) Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MSpec ty ctor -> c (MSpec ty ctor) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (MSpec ty ctor) #

toConstr :: MSpec ty ctor -> Constr #

dataTypeOf :: MSpec ty ctor -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c (MSpec ty ctor)) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (MSpec ty ctor)) #

gmapT :: (forall b. Data b => b -> b) -> MSpec ty ctor -> MSpec ty ctor #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MSpec ty ctor -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MSpec ty ctor -> r #

gmapQ :: (forall d. Data d => d -> u) -> MSpec ty ctor -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> MSpec ty ctor -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> MSpec ty ctor -> m (MSpec ty ctor) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MSpec ty ctor -> m (MSpec ty ctor) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MSpec ty ctor -> m (MSpec ty ctor) #

(Show ty, Show ctor, PPrint ctor, PPrint ty) => Show (MSpec ty ctor) Source # 

Methods

showsPrec :: Int -> MSpec ty ctor -> ShowS #

show :: MSpec ty ctor -> String #

showList :: [MSpec ty ctor] -> ShowS #

Generic (MSpec ty ctor) Source # 

Associated Types

type Rep (MSpec ty ctor) :: * -> * #

Methods

from :: MSpec ty ctor -> Rep (MSpec ty ctor) x #

to :: Rep (MSpec ty ctor) x -> MSpec ty ctor #

Eq ctor => Monoid (MSpec ty ctor) Source # 

Methods

mempty :: MSpec ty ctor #

mappend :: MSpec ty ctor -> MSpec ty ctor -> MSpec ty ctor #

mconcat :: [MSpec ty ctor] -> MSpec ty ctor #

(PPrint t, PPrint a) => PPrint (MSpec t a) Source # 

Methods

pprintTidy :: Tidy -> MSpec t a -> Doc #

pprintPrec :: Int -> Tidy -> MSpec t a -> Doc #

type Rep (MSpec ty ctor) Source # 
type Rep (MSpec ty ctor)

Type Aliases

Constructors

mkM :: LocSymbol -> ty -> [Def ty bndr] -> Measure ty bndr Source #

mkMSpec' :: Symbolic ctor => [Measure ty ctor] -> MSpec ty ctor Source #

qualifySpec :: Symbol -> Spec ty bndr -> Spec ty bndr Source #

dataConTypes :: MSpec (RRType Reft) DataCon -> ([(Var, RRType Reft)], [(LocSymbol, RRType Reft)]) Source #