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)

Used to parse .spec files

singleSpecP :: SourcePos -> String -> Either Error BPspec

type BPspec = Pspec (Located BareType) LocSymbol

data Pspec ty ctor

Constructors

Meas (Measure ty ctor)

Assm (LocSymbol, ty)

Asrt (LocSymbol, ty)

LAsrt (LocSymbol, ty)

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

Impt Symbol

DDecl DataDecl

NTDecl DataDecl

Incl FilePath

Invt ty

IAlias (ty, ty)

Alias (RTAlias Symbol BareType)

EAlias (RTAlias Symbol Expr)

Embed (LocSymbol, FTycon)

Qualif Qualifier

Decr (LocSymbol, [Int])

LVars LocSymbol

Lazy LocSymbol

Insts (LocSymbol, Maybe Int)

HMeas LocSymbol

Reflect LocSymbol

Inline LocSymbol

ASize LocSymbol

HBound LocSymbol

PBound (Bound ty Expr)

Pragma (Located String)

CMeas (Measure ty ())

IMeas (Measure ty ctor)

Class (RClass ty)

RInst (RInstance ty)

Varia (LocSymbol, [Variance])

BFix ()

Define (LocSymbol, Symbol)

Instances

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

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 :: (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)

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

Methods

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

show :: Pspec ty ctor -> String

showList :: [Pspec ty ctor] -> ShowS

parseSymbolToLogic :: SourceName -> String -> Either Error LogicMap