Language.Haskell.Liquid.Parse

Documentation

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

Top Level Parsing API -----------------------------------------------------

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

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

singleSpecP :: SourcePos -> String -> Either Error 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 -- RJ: what is this

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

RJ: what is this

Impt Symbol

'import' a specification module

DDecl DataDecl

refined 'data' declaration

NTDecl DataDecl

refined 'newtype' declaration

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

Decr (LocSymbol, [Int])

decreasing annotation -- TODO: deprecate

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

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) => 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 Error LogicMap