Safe Haskell	None
Language	Haskell98

Language.Haskell.Liquid.Parse

Synopsis

hsSpecificationP :: ModuleName -> [(SourcePos, String)] -> [BPspec] -> Either [Error] (ModName, BareSpec)
specSpecificationP :: SourceName -> String -> Either Error (ModName, BareSpec)
singleSpecP :: SourcePos -> String -> Either Error BPspec
type BPspec = Pspec LocBareType LocSymbol
data Pspec ty ctor
- = 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
- | Class (RClass ty)
- | CLaws (RClass ty)
- | ILaws (RILaws ty)
- | RInst (RInstance ty)
- | Incl FilePath
- | Invt ty
- | Using (ty, ty)
- | Alias (Located (RTAlias Symbol BareType))
- | EAlias (Located (RTAlias Symbol Expr))
- | Embed (LocSymbol, FTycon, TCArgs)
- | Qualif Qualifier
- | Decr (LocSymbol, [Int])
- | LVars LocSymbol
- | Lazy LocSymbol
- | Fail LocSymbol
- | Rewrite LocSymbol
- | Rewritewith (LocSymbol, [LocSymbol])
- | Insts (LocSymbol, Maybe Int)
- | HMeas LocSymbol
- | Reflect LocSymbol
- | Inline LocSymbol
- | Ignore LocSymbol
- | ASize LocSymbol
- | HBound LocSymbol
- | PBound (Bound ty Expr)
- | Pragma (Located String)
- | CMeas (Measure ty ())
- | IMeas (Measure ty ctor)
- | Varia (LocSymbol, [Variance])
- | BFix ()
- | Define (LocSymbol, Symbol)
parseSymbolToLogic :: SourceName -> String -> Either Error LogicMap

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

Instances details

(Data ty, Data ctor) => Data (Pspec ty ctor) #
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) -> 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) #
Instance details 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 #