Language.Haskell.Liquid.Parse

Documentation

hsSpecificationP :: ModuleName -> [(SourcePos, String)] -> [BPspec] -> Either [Error] (ModName, BareSpec)

Used to parse .hs and .lhs files (via ApiAnnotations).

specSpecificationP :: SourceName -> String -> Either (ParseErrorBundle String Void) (ModName, BareSpec)

Used to parse .spec files.

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

type BPspec = Pspec LocBareType LocSymbol

data Pspec ty ctor

The AST for a single parsed spec.

Constructors

Meas (Measure ty ctor)

measure definition

Assm (LocSymbol, ty)

assume signature (unchecked)

Asrt (LocSymbol, ty)

assert signature (checked)

LAsrt (LocSymbol, ty)

local assertion -- TODO RJ: what is this

Asrts ([LocSymbol], (ty, Maybe [Located Expr]))

TODO RJ: what is this

Impt Symbol

'import' a specification module

DDecl DataDecl

refined 'data' declaration

NTDecl DataDecl

refined 'newtype' declaration

Relational (LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)

relational signature

AssmRel (LocSymbol, LocSymbol, ty, ty, RelExpr, RelExpr)

assume relational signature

Class (RClass ty)

refined 'class' definition

CLaws (RClass ty)

'class laws' definition

ILaws (RILaws ty)

RInst (RInstance ty)

refined 'instance' definition

Incl FilePath

include a path -- TODO: deprecate

Invt ty

invariant specification

Using (ty, ty)

using declaration (for local invariants on a type)

Alias (Located (RTAlias Symbol BareType))

'type' alias declaration

EAlias (Located (RTAlias Symbol Expr))

predicate alias declaration

Embed (LocSymbol, FTycon, TCArgs)

embed declaration

Qualif Qualifier

qualif definition

LVars LocSymbol

lazyvar annotation, defer checks to *use* sites

Lazy LocSymbol

lazy annotation, skip termination check on binder

Fail LocSymbol

fail annotation, the binder should be unsafe

Rewrite LocSymbol

rewrite annotation, the binder generates a rewrite rule

Rewritewith (LocSymbol, [LocSymbol])

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

Insts (LocSymbol, Maybe Int)

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

HMeas LocSymbol

measure annotation; lift Haskell binder as measure

Reflect LocSymbol

reflect annotation; reflect Haskell binder as function in logic

Inline LocSymbol

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

Ignore LocSymbol

ignore annotation; skip all checks inside this binder

ASize LocSymbol

autosize annotation; automatically generate size metric for this type

HBound LocSymbol

bound annotation; lift Haskell binder as an abstract-refinement "bound"

PBound (Bound ty Expr)

bound definition

Pragma (Located String)

LIQUID pragma, used to save configuration options in source files

CMeas (Measure ty ())

'class measure' definition

IMeas (Measure ty ctor)

'instance measure' definition

Varia (LocSymbol, [Variance])

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

DSize ([ty], LocSymbol)

'data size' annotations, generating fancy termination metric

BFix ()

fixity annotation

Define (LocSymbol, Symbol)

define annotation for specifying aliases c.f. `include-CoreToLogic.lg`

Instances

(Data ty, Data ctor) => Data (Pspec ty ctor)

Defined in Language.Haskell.Liquid.Parse

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Pspec ty ctor -> c (Pspec ty ctor)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Pspec ty ctor)

toConstr :: Pspec ty ctor -> Constr

dataTypeOf :: Pspec ty ctor -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Pspec ty ctor))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Pspec ty ctor))

gmapT :: (forall b. Data b => b -> b) -> Pspec ty ctor -> Pspec ty ctor

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pspec ty ctor -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pspec ty ctor -> r

gmapQ :: (forall d. Data d => d -> u) -> Pspec ty ctor -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Pspec ty ctor -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Pspec ty ctor -> m (Pspec ty ctor)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Pspec ty ctor -> m (Pspec ty ctor)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Pspec ty ctor -> m (Pspec ty ctor)

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

Defined in Language.Haskell.Liquid.Parse

Methods

showsPrec :: Int -> Pspec ty ctor -> ShowS

show :: Pspec ty ctor -> String

showList :: [Pspec ty ctor] -> ShowS

(PPrint ty, PPrint ctor) => PPrint (Pspec ty ctor)

Defined in Language.Haskell.Liquid.Parse

Methods

pprintTidy :: Tidy -> Pspec ty ctor -> Doc

pprintPrec :: Int -> Tidy -> Pspec ty ctor -> Doc

parseSymbolToLogic :: SourceName -> String -> Either (ParseErrorBundle String Void) LogicMap

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

Function to test parsers interactively.