liquidtypes-0.1: Liquid Types for Haskell

Safe HaskellSafe-Infered

Language.Haskell.Liquid.Measure

Documentation

data Spec ty bndr Source

Constructors

Spec 

Fields

measures :: ![Measure ty bndr]

User-defined properties for ADTs

sigs :: ![(Symbol, ty)]

Imported functions and types

invariants :: ![ty]

Data type invariants

imports :: ![Symbol]

Loaded spec module names

dataDecls :: ![DataDecl]

Predicated data definitions

includes :: ![FilePath]

Included qualifier files

aliases :: ![RTAlias String BareType]

RefType aliases

paliases :: ![RTAlias Symbol Pred]

Refinement/Predicate aliases

embeds :: !(TCEmb String)

GHC-Tycon-to-fixpoint Tycon map

Instances

Bifunctor Spec 
Monoid (Spec ty bndr) 
Inputable (Spec BareType Symbol) 

data MSpec ty bndr Source

Constructors

MSpec 

Fields

ctorMap :: HashMap Symbol [Def bndr]
 
measMap :: HashMap Symbol (Measure ty bndr)
 

Instances

Bifunctor MSpec 
Functor (MSpec t) 
(Outputable t, Outputable a) => Outputable (MSpec t a) 

data Measure ty bndr Source

Instances

data Def bndr Source

Constructors

Def 

Fields

measure :: Symbol
 
ctor :: bndr
 
binds :: [Symbol]
 
body :: Body
 

Instances

Functor Def 
Show bndr => Show (Def bndr) 
Outputable a => Outputable (Def a) 

data Body Source

Constructors

E Expr

Measure Refinement: {v | v = e }

P Pred

Measure Refinement: {v | (? v) = p }

R Symbol Pred

Measure Refinement: {v | p}

Instances

mkM :: Symbol -> ty -> [Def bndr] -> Measure ty bndrSource

mkMSpec :: [Measure ty Symbol] -> MSpec ty SymbolSource

qualifySpec :: [Char] -> Spec ty bndr -> Spec ty bndrSource

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

dataConTypes :: MSpec RefType DataCon -> ([(Var, RefType)], [(Symbol, RefType)])Source

expandRTAliases :: Spec BareType Symbol -> Spec BareType SymbolSource