Language.Haskell.Liquid.Measure

Specifications

data Spec ty bndr

Constructors

Spec

Fields

• measures :: ![Measure ty bndr]

  User-defined properties for ADTs

• asmSigs :: ![(LocSymbol, ty)]

  Assumed (unchecked) types; including reflected signatures

• sigs :: ![(LocSymbol, ty)]

  Imported functions and types

• localSigs :: ![(LocSymbol, ty)]

  Local type signatures

• reflSigs :: ![(LocSymbol, ty)]

  Reflected type signatures

• invariants :: ![ty]

  Data type invariants

• ialiases :: ![(ty, ty)]

  Data type invariants to be checked

• imports :: ![Symbol]

  Loaded spec module names

• dataDecls :: ![DataDecl]

  Predicated data definitions

• newtyDecls :: ![DataDecl]

  Predicated new type definitions

• includes :: ![FilePath]

  Included qualifier files

• aliases :: ![RTAlias Symbol BareType]

  RefType aliases

• ealiases :: ![RTAlias Symbol Expr]

  Expression aliases

• embeds :: !(TCEmb LocSymbol)

  GHC-Tycon-to-fixpoint Tycon map

• qualifiers :: ![Qualifier]

  Qualifiers in source/spec files

• decr :: ![(LocSymbol, [Int])]

  Information on decreasing arguments

• lvars :: ![LocSymbol]

  Variables that should be checked in the environment they are used

• lazy :: !(HashSet LocSymbol)

  Ignore Termination Check in these Functions , axioms :: !(S.HashSet LocSymbol) -- ^ Binders to turn into SMT axioms

• reflects :: !(HashSet LocSymbol)

  Binders to reflect

• autois :: !(HashMap LocSymbol (Maybe Int))

  Automatically instantiate axioms in these Functions with maybe specified fuel

• hmeas :: !(HashSet LocSymbol)

  Binders to turn into measures using haskell definitions

• hbounds :: !(HashSet LocSymbol)

  Binders to turn into bounds using haskell definitions

• inlines :: !(HashSet LocSymbol)

  Binders to turn into logic inline using haskell definitions

• autosize :: !(HashSet LocSymbol)

  Type Constructors that get automatically sizing info

• pragmas :: ![Located String]

  Command-line configurations passed in through source

• cmeasures :: ![Measure ty ()]

  Measures attached to a type-class

• imeasures :: ![Measure ty bndr]

  Mappings from (measure,type) -> measure

• classes :: ![RClass ty]

  Refined Type-Classes

• termexprs :: ![(LocSymbol, [Located Expr])]

  Terminating Conditions for functions

• rinstance :: ![RInstance ty]
• dvariance :: ![(LocSymbol, [Variance])]

  ? Where do these come from ?!

• bounds :: !(RRBEnv ty)
• defs :: !(HashMap LocSymbol Symbol)

  Temporary (?) hack to deal with dictionaries in specifications see testsposNatClass.hs

• axeqs :: ![AxiomEq]

  AxiomEqualities used for Proof-By-Evaluation

Instances

Binary BareSpec

Methods

put :: BareSpec -> Put

get :: Get BareSpec

putList :: [BareSpec] -> Put

Generic (Spec ty bndr)

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)

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)

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

Constructors

MSpec

Fields

• ctorMap :: HashMap Symbol [Def ty ctor]
• measMap :: HashMap LocSymbol (Measure ty ctor)
• cmeasMap :: HashMap LocSymbol (Measure ty ())
• imeas :: ![Measure ty ctor]

Instances

Bifunctor MSpec

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)

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)

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)

Methods

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

show :: MSpec ty ctor -> String

showList :: [MSpec ty ctor] -> ShowS

Generic (MSpec ty ctor)

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)

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)

Methods

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

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

type Rep (MSpec ty ctor)

type Rep (MSpec ty ctor)

Type Aliases

type BareSpec = Spec LocBareType LocSymbol

type BareMeasure = Measure LocBareType LocSymbol

type SpecMeasure = Measure LocSpecType DataCon

Constructors

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

mkMSpec :: [Measure t LocSymbol] -> [Measure t ()] -> [Measure t LocSymbol] -> MSpec t LocSymbol

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

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

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

defRefType :: Type -> Def (RRType Reft) DataCon -> RRType Reft