Safe Haskell	None
Language	Haskell98

Language.Haskell.Liquid.Measure

Synopsis

Documentation

data Spec ty bndr Source

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
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 :: !(HashSet LocSymbol): Binders to turn into axiomatized functions
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, [Expr])]: Terminating Conditions for functions
rinstance :: ![RInstance ty]
dvariance :: ![(LocSymbol, [Variance])]
bounds :: !(RRBEnv ty)

Instances

Monoid (Spec ty bndr) Source

type BareSpec = Spec BareType LocSymbol Source

data MSpec ty ctor Source

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 Source
Functor (MSpec ty) Source
(Data ty, Data ctor) => Data (MSpec ty ctor) Source
(Show ty, Show ctor, PPrint ctor, PPrint ty) => Show (MSpec ty ctor) Source
Generic (MSpec ty ctor) Source
Eq ctor => Monoid (MSpec ty ctor) Source
(PPrint t, PPrint a) => PPrint (MSpec t a) Source
type Rep (MSpec ty ctor) Source

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

mkMSpec :: [Measure ty (Located Symbol)] -> [Measure ty ()] -> [Measure ty (Located Symbol)] -> MSpec ty (Located Symbol) 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

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

strLen :: Measure SpecType ctor Source

A wired-in measure strLen that describes the length of a string literal, with type Addr#.

wiredInMeasures :: MSpec SpecType DataCon Source