liquidhaskell-boot-0.9.2.5.0: Liquid Types for Haskell
Safe HaskellSafe-Inferred
LanguageHaskell98

Language.Haskell.Liquid.Measure

Synopsis

Specifications

data Spec ty bndr Source #

A generic Spec type, polymorphic over the inner choice of type and binder.

Constructors

Spec 

Fields

Instances

Instances details
Qualify ModSpecs Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Qualify BareSpec Source # 
Instance details

Defined in Language.Haskell.Liquid.Bare.Resolve

Monoid (Spec ty bndr) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Methods

mempty :: Spec ty bndr #

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

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

Semigroup (Spec ty bndr) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Methods

(<>) :: Spec ty bndr -> Spec ty bndr -> Spec ty bndr #

sconcat :: NonEmpty (Spec ty bndr) -> Spec ty bndr #

stimes :: Integral b => b -> Spec ty bndr -> Spec ty bndr #

Generic (Spec ty bndr) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Associated Types

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

Methods

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

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

(PPrint ty, PPrint bndr, Show ty) => Show (Spec ty bndr) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Methods

showsPrec :: Int -> Spec ty bndr -> ShowS #

show :: Spec ty bndr -> String #

showList :: [Spec ty bndr] -> ShowS #

Binary (Spec LocBareType LocSymbol) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

(Show ty, Show bndr, PPrint ty, PPrint bndr) => PPrint (Spec ty bndr) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

Methods

pprintTidy :: Tidy -> Spec ty bndr -> Doc #

pprintPrec :: Int -> Tidy -> Spec ty bndr -> Doc #

type Rep (Spec ty bndr) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Specs

type Rep (Spec ty bndr) = D1 ('MetaData "Spec" "Language.Haskell.Liquid.Types.Specs" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" 'False) (C1 ('MetaCons "Spec" 'PrefixI 'True) (((((S1 ('MetaSel ('Just "measures") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Measure ty bndr]) :*: S1 ('MetaSel ('Just "impSigs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(Symbol, Sort)])) :*: (S1 ('MetaSel ('Just "expSigs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(Symbol, Sort)]) :*: (S1 ('MetaSel ('Just "asmSigs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(LocSymbol, ty)]) :*: S1 ('MetaSel ('Just "sigs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(LocSymbol, ty)])))) :*: ((S1 ('MetaSel ('Just "localSigs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(LocSymbol, ty)]) :*: (S1 ('MetaSel ('Just "reflSigs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(LocSymbol, ty)]) :*: S1 ('MetaSel ('Just "invariants") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(Maybe LocSymbol, ty)]))) :*: (S1 ('MetaSel ('Just "ialiases") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(ty, ty)]) :*: (S1 ('MetaSel ('Just "imports") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Symbol]) :*: S1 ('MetaSel ('Just "dataDecls") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [DataDecl]))))) :*: (((S1 ('MetaSel ('Just "newtyDecls") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [DataDecl]) :*: S1 ('MetaSel ('Just "includes") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [FilePath])) :*: (S1 ('MetaSel ('Just "aliases") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Located (RTAlias Symbol BareType)]) :*: (S1 ('MetaSel ('Just "ealiases") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Located (RTAlias Symbol Expr)]) :*: S1 ('MetaSel ('Just "embeds") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (TCEmb LocSymbol))))) :*: ((S1 ('MetaSel ('Just "qualifiers") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Qualifier]) :*: (S1 ('MetaSel ('Just "lvars") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol)) :*: S1 ('MetaSel ('Just "lazy") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol)))) :*: (S1 ('MetaSel ('Just "rewrites") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol)) :*: (S1 ('MetaSel ('Just "rewriteWith") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashMap LocSymbol [LocSymbol])) :*: S1 ('MetaSel ('Just "fails") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol))))))) :*: ((((S1 ('MetaSel ('Just "reflects") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol)) :*: S1 ('MetaSel ('Just "autois") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashMap LocSymbol (Maybe Int)))) :*: (S1 ('MetaSel ('Just "hmeas") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol)) :*: (S1 ('MetaSel ('Just "hbounds") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol)) :*: S1 ('MetaSel ('Just "inlines") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol))))) :*: ((S1 ('MetaSel ('Just "ignores") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol)) :*: (S1 ('MetaSel ('Just "autosize") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashSet LocSymbol)) :*: S1 ('MetaSel ('Just "pragmas") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Located String]))) :*: (S1 ('MetaSel ('Just "cmeasures") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Measure ty ()]) :*: (S1 ('MetaSel ('Just "imeasures") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Measure ty bndr]) :*: S1 ('MetaSel ('Just "classes") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [RClass ty]))))) :*: (((S1 ('MetaSel ('Just "claws") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [RClass ty]) :*: S1 ('MetaSel ('Just "relational") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)])) :*: (S1 ('MetaSel ('Just "asmRel") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)]) :*: (S1 ('MetaSel ('Just "termexprs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(LocSymbol, [Located Expr])]) :*: S1 ('MetaSel ('Just "rinstance") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [RInstance ty])))) :*: ((S1 ('MetaSel ('Just "ilaws") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [RILaws ty]) :*: (S1 ('MetaSel ('Just "dvariance") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [(LocSymbol, [Variance])]) :*: S1 ('MetaSel ('Just "dsize") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [([ty], LocSymbol)]))) :*: (S1 ('MetaSel ('Just "bounds") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (RRBEnv ty)) :*: (S1 ('MetaSel ('Just "defs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (HashMap LocSymbol Symbol)) :*: S1 ('MetaSel ('Just "axeqs") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 [Equation]))))))))

data MSpec ty ctor Source #

Constructors

MSpec 

Fields

Instances

Instances details
Bifunctor MSpec Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

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 # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

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

Defined in Language.Haskell.Liquid.Types.Types

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 :: forall r r'. (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) #

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

Defined in Language.Haskell.Liquid.Types.Types

Methods

mempty :: MSpec ty ctor #

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

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

Eq ctor => Semigroup (MSpec ty ctor) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Methods

(<>) :: MSpec ty ctor -> MSpec ty ctor -> MSpec ty ctor #

sconcat :: NonEmpty (MSpec ty ctor) -> MSpec ty ctor #

stimes :: Integral b => b -> MSpec ty ctor -> MSpec ty ctor #

Generic (MSpec ty ctor) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

Associated Types

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

Methods

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

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

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

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

show :: MSpec ty ctor -> String #

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

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

Defined in Language.Haskell.Liquid.Types.Types

Methods

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

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

type Rep (MSpec ty ctor) Source # 
Instance details

Defined in Language.Haskell.Liquid.Types.Types

type Rep (MSpec ty ctor)

Type Aliases

Constructors

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

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