liquidhaskell-boot-0.9.10.1.2: Liquid Types for Haskell
Safe HaskellNone
LanguageHaskell98

Language.Haskell.Liquid.Parse

Synopsis

Documentation

hsSpecificationP :: ModuleName -> [BPspec] -> (ModName, BareSpecParsed) Source #

parseSpecComments :: [(SourcePos, String)] -> Either [Error] [BPspec] Source #

Parse comments in .hs and .lhs files

singleSpecP :: SourcePos -> String -> Either (ParseErrorBundle String Void) BPspec Source #

data BPspec Source #

The AST for a single parsed spec.

Constructors

Meas (MeasureV LocSymbol LocBareTypeParsed (Located LHName))

measure definition

Assm (Located LHName, LocBareTypeParsed)

assume signature (unchecked)

AssmReflect (Located LHName, Located LHName)

'assume reflects' signature (unchecked)

Asrt (Located LHName, LocBareTypeParsed)

assert signature (checked)

Asrts ([Located LHName], (LocBareTypeParsed, Maybe [Located (ExprV LocSymbol)]))

sym0, ..., symn :: ty / [m0,..., mn]

DDecl DataDeclParsed

refined 'data' declaration

NTDecl DataDeclParsed

refined 'newtype' declaration

Relational (Located LHName, Located LHName, LocBareTypeParsed, LocBareTypeParsed, RelExprV LocSymbol, RelExprV LocSymbol)

relational signature

AssmRel (Located LHName, Located LHName, LocBareTypeParsed, LocBareTypeParsed, RelExprV LocSymbol, RelExprV LocSymbol)

assume relational signature

Class (RClass LocBareTypeParsed)

refined 'class' definition

RInst (RInstance LocBareTypeParsed)

refined 'instance' definition

Invt LocBareTypeParsed

invariant specification

Using (LocBareTypeParsed, LocBareTypeParsed)

using declaration (for local invariants on a type)

Alias (Located (RTAlias Symbol BareTypeParsed))

'type' alias declaration

EAlias (Located (RTAlias Symbol (ExprV LocSymbol)))

predicate alias declaration

Embed (Located LHName, FTycon, TCArgs)

embed declaration

Qualif (QualifierV LocSymbol)

qualif definition

LVars (Located LHName)

lazyvar annotation, defer checks to *use* sites

Lazy (Located LHName)

lazy annotation, skip termination check on binder

Fail (Located LHName)

fail annotation, the binder should be unsafe

Rewrite (Located LHName)

rewrite annotation, the binder generates a rewrite rule

Rewritewith (Located LHName, [Located LHName])

rewritewith annotation, the first binder is using the rewrite rules of the second list,

Insts (Located LHName)

'auto-inst' or ple annotation; use ple locally on binder

HMeas (Located LHName)

measure annotation; lift Haskell binder as measure

Reflect (Located LHName)

reflect annotation; reflect Haskell binder as function in logic

PrivateReflect LocSymbol

'private-reflect' annotation

OpaqueReflect (Located LHName)

'opaque-reflect' annotation

Inline (Located LHName)

inline annotation; inline (non-recursive) binder as an alias

Ignore (Located LHName)

ignore annotation; skip all checks inside this binder

ASize (Located LHName)

autosize annotation; automatically generate size metric for this type

PBound (Bound LocBareTypeParsed (ExprV LocSymbol))

bound definition

Pragma (Located String)

LIQUID pragma, used to save configuration options in source files

CMeas (MeasureV LocSymbol LocBareTypeParsed ())

'class measure' definition

IMeas (MeasureV LocSymbol LocBareTypeParsed (Located LHName))

'instance measure' definition

Varia (Located LHName, [Variance])

variance annotations, marking type constructor params as co-, contra-, or in-variant

DSize ([LocBareTypeParsed], LocSymbol)

'data size' annotations, generating fancy termination metric

BFix ()

fixity annotation

Define (Located LHName, ([Symbol], ExprV LocSymbol))

define annotation for specifying logic aliases

Instances

Instances details
Data BPspec Source # 
Instance details

Defined in Language.Haskell.Liquid.Parse

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BPspec -> c BPspec #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BPspec #

toConstr :: BPspec -> Constr #

dataTypeOf :: BPspec -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BPspec) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BPspec) #

gmapT :: (forall b. Data b => b -> b) -> BPspec -> BPspec #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BPspec -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BPspec -> r #

gmapQ :: (forall d. Data d => d -> u) -> BPspec -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> BPspec -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> BPspec -> m BPspec #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BPspec -> m BPspec #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BPspec -> m BPspec #

PPrint BPspec Source # 
Instance details

Defined in Language.Haskell.Liquid.Parse

Methods

pprintTidy :: Tidy -> BPspec -> Doc #

pprintPrec :: Int -> Tidy -> BPspec -> Doc #

parseTest' :: Show a => Parser a -> String -> IO () Source #

Function to test parsers interactively.

Orphan instances