liquidhaskell- Liquid Types for Haskell

Safe HaskellNone



data Spec ty bndr Source




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])]


Bifunctor Spec 
Monoid (Spec ty bndr) 

data MSpec ty ctor Source




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


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 Source

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

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

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