Language.Haskell.Liquid.Measure

Documentation

data Spec ty bndr

Constructors

Spec

Fields

measures :: ![Measure ty bndr]

User-defined properties for ADTs

asmSigs :: ![(LocSymbol, ty)]

Assumed (unchecked) types

sigs :: ![(LocSymbol, ty)]

Imported functions and types

localSigs :: ![(LocSymbol, ty)]

Local type signatures

invariants :: ![Located ty]

Data type invariants

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

Data type invariants to be checked

imports :: ![Symbol]

Loaded spec module names

dataDecls :: ![DataDecl]

Predicated data definitions

includes :: ![FilePath]

Included qualifier files

aliases :: ![RTAlias Symbol BareType]

RefType aliases

paliases :: ![RTAlias Symbol Pred]

Refinement/Predicate 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

hmeas :: !(HashSet LocSymbol)

Binders to turn into measures using haskell definitions

inlines :: !(HashSet LocSymbol)

Binders to turn into logic inline using haskell definitions

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, [Expr])]

Terminating Conditions for functions

rinstance :: ![RInstance ty]

dvariance :: ![(LocSymbol, [Variance])]

Instances

Bifunctor Spec

Monoid (Spec ty bndr)

type BareSpec = Spec BareType LocSymbol

data MSpec ty ctor

Constructors

MSpec

Fields

ctorMap :: HashMap Symbol [Def ctor]

measMap :: HashMap LocSymbol (Measure ty ctor)

cmeasMap :: HashMap LocSymbol (Measure ty ())

imeas :: ![Measure ty ctor]

Instances

Bifunctor MSpec

Functor (MSpec t)

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

Eq ctor => Monoid (MSpec ty ctor)

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

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

mkMSpec :: [Measure ty (Located Symbol)] -> [Measure ty ()] -> [Measure ty (Located Symbol)] -> MSpec ty (Located Symbol)

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

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

mapTy :: (tya -> tyb) -> Measure tya c -> Measure tyb c

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

defRefType :: Def DataCon -> RRType Reft