Safe Haskell	None
Language	Haskell98

Language.Haskell.Liquid.Types

Contents

Options
Ghc Information
Located Things
Symbols
Default unknown name
Refined Type Constructors
Refinement Types
Worlds
Classes describing operations on RTypes
Predicate Variables
Refinements
Parse-time entities describing refined data types
Pre-instantiated RType
Instantiated RType
Constructing & Destructing RTypes
Manipulating Predicates
Some tests on RTypes
Traversing RType
???
Inferred Annotations
Overall Output
Refinement Hole
Converting To and From Sort
Class for values that can be pretty printed
Printer Configuration
Modules and Imports
Refinement Type Aliases
Final Result
Errors and Error Messages
Source information (associated with constraints)
Measures
Type Classes
KV Profiling
Misc
Strata
CoreToLogic
Refined Instances

Description

This module should contain all the global type definitions and basic instances.

Synopsis

Options

data Config Source

Command Line Config Options --------------------------------------------

Constructors

Config

Fields

files :: [FilePath]: source files to check
idirs :: [FilePath]: path to directory for including specs
diffcheck :: Bool: check subset of binders modified (+ dependencies) since last check
real :: Bool: supports real number arithmetic
fullcheck :: Bool: check all binders (overrides diffcheck)
binders :: [String]: set of binders to check
noCheckUnknown :: Bool: whether to complain about specifications for unexported and unused values
notermination :: Bool: disable termination check
nowarnings :: Bool: disable warnings output (only show errors)
trustinternals :: Bool: type all internal variables with true
nocaseexpand :: Bool: disable case expand
strata :: Bool: enable strata analysis
notruetypes :: Bool: disable truing top level types
totality :: Bool: check totality in definitions
noPrune :: Bool: disable prunning unsorted Refinements
maxParams :: Int: the maximum number of parameters to accept when mining qualifiers
smtsolver :: Maybe SMTSolver: name of smtsolver to use [default: try z3, cvc4, mathsat in order]
shortNames :: Bool: drop module qualifers from pretty-printed names.
shortErrors :: Bool: don't show subtyping errors and contexts.
ghcOptions :: [String]: command-line options to pass to GHC
cFiles :: [String]: .c files to compile and link against (for GHC)

Instances

Eq Config
Data Config
Show Config
Monoid Config	Monoid instances for updating options
Typeable * Config

Ghc Information

data GhcInfo Source

GHC Information : Code & Spec ------------------------------

Constructors

GI
Fields env :: !HscEnv cbs :: ![CoreBind] derVars :: ![Var] impVars :: ![Var] defVars :: ![Var] useVars :: ![Var] hqFiles :: ![FilePath] imports :: ![String] includes :: ![FilePath] spec :: !GhcSpec

Instances

Show GhcInfo
PPrint GhcInfo

data GhcSpec Source

The following is the overall type for specifications obtained from parsing the target source and dependent libraries

Constructors

SP

Fields

tySigs :: ![(Var, Located SpecType)]: Asserted Reftypes eg. see include/Prelude.spec
asmSigs :: ![(Var, Located SpecType)]: Assumed Reftypes
ctors :: ![(Var, Located SpecType)]: Data Constructor Measure Sigs eg. (:) :: a -> xs:[a] -> {v: Int | v = 1 + len(xs) }
meas :: ![(Symbol, Located SpecType)]: Measure Types eg. len :: [a] -> Int
invariants :: ![Located SpecType]: Data Type Invariants
ialiases :: ![(Located SpecType, Located SpecType)]: Data Type Invariant Aliases eg. forall a. {v: [a] | len(v) >= 0}
dconsP :: ![(DataCon, DataConP)]: Predicated Data-Constructors e.g. see testsposMap.hs
tconsP :: ![(TyCon, TyConP)]: Predicated Type-Constructors eg. see testsposMap.hs
freeSyms :: ![(Symbol, Var)]: List of Symbol free in spec and corresponding GHC var eg. (Cons, Cons#7uz) from testsposex1.hs
tcEmbeds :: TCEmb TyCon: How to embed GHC Tycons into fixpoint sorts e.g. "embed Set as Set_set" from includeDataSet.spec
qualifiers :: ![Qualifier]: Qualifiers in Source/Spec files e.g testsposqualTest.hs
tgtVars :: ![Var]: Top-level Binders To Verify (empty means ALL binders)
decr :: ![(Var, [Int])]: Lexicographically ordered size witnesses for termination
texprs :: ![(Var, [Expr])]: Lexicographically ordered expressions for termination
lvars :: !(HashSet Var): Variables that should be checked in the environment they are used
lazy :: !(HashSet Var): Binders to IGNORE during termination checking
config :: !Config: Configuration Options
exports :: !NameSet: Names exported by the module being verified
measures :: [Measure SpecType DataCon]
tyconEnv :: HashMap TyCon RTyCon
dicts :: DEnv Var SpecType: Dictionary Environment

Instances

PPrint GhcSpec

data TargetVars Source

Which Top-Level Binders Should be Verified

Constructors

AllVars
Only ![Var]

Instances

PPrint TargetVars

Located Things

data Located a :: * -> *

Located Values ---------------------------------------------------------

Constructors

Loc
Fields loc :: !SourcePos val :: a

Instances

Functor Located
Foldable Located
Traversable Located
Inputable BareType	Bundling Parsers into a Typeclass ------------------------
TyConable LocSymbol
Resolvable LocSymbol
SubsTy Symbol BSort LocSymbol
SubsTy Symbol BSort BSort
Eq a => Eq (Located a)
Data a => Data (Located a)
Ord a => Ord (Located a)
Show a => Show (Located a)
IsString a => IsString (Located a)
Generic (Located a)
NFData a => NFData (Located a)
Hashable a => Hashable (Located a)
PPrint a => PPrint (Located a)
Fixpoint a => Fixpoint (Located a)
Expression a => Expression (Located a)
Subable a => Subable (Located a)
Symbolic a => Symbolic (Located a)
PPrint a => PPrint (Located a)
GhcLookup (Located Symbol)
Inputable (Measure BareType LocSymbol)
Typeable (* -> *) Located
type Rep (Located a) = D1 D1Located (C1 C1_0Located ((:*:) (S1 S1_0_0Located (Rec0 SourcePos)) (S1 S1_0_1Located (Rec0 a))))

dummyLoc :: a -> Located a

Symbols

type LocSymbol = Located Symbol

type LocText = Located Text

Default unknown name

dummyName :: Symbol

isDummy :: Symbolic a => a -> Bool

Refined Type Constructors

data RTyCon Source

Constructors

RTyCon TyCon ![RPVar] !TyConInfo

Instances

Eq Error
Eq RTyCon
Data RTyCon
Ord Error
Ord RTyCon
Show Error
Show RTyCon
Generic RTyCon
ToJSON Error
FromJSON Error
Exception Error
NFData PrType
NFData RTyCon
Hashable RTyCon
Fixpoint RTyCon
Error Error
Result Error
TyConable RTyCon	TyConable Instances -------------------------------------------------------
PPrint Error	Pretty Printing Error Messages ------------------------------------ Need to put `PPrint Error` instance here (instead of in Types), as it depends on `PPrint SpecTypes`, which lives in this module.
PPrint RTyCon
SubStratum SpecType
Typeable * RTyCon
(Reftable r, PPrint r) => RefTypable RTyCon RTyVar r
SubsTy RTyVar RSort SpecType
SubsTy RTyVar RSort PrType
SubsTy RTyVar RSort RSort
SubsTy RTyVar RSort RTyCon
SubsTy RTyVar RTyVar SpecType
(Freshable m Integer, Freshable m r, Reftable r, RefTypable RTyCon RTyVar r) => Freshable m (RRType r)
ToJSON (FixResult Error)
FromJSON (FixResult Error)
Exception [Error]
Fixpoint (FixResult Error)
Subable (RRProp Reft)	Subable Instances -----------------------------------------------------
Result [Error]
SubStratum (Annot SpecType)
(PPrint r, Reftable r) => Reftable (RType RTyCon RTyVar r)	Reftable Instances -------------------------------------------------------
type Rep RTyCon

data TyConInfo Source

Co- and Contra-variance for TyCon --------------------------------

Indexes start from 0 and type or predicate arguments can be both covariant and contravaariant e.g., for the below Foo dataType

data Foo a b c d :: b - Prop, q :: Int -> Prop, r :: a -> Prop> = F (ar -> bp) | Q (c -> a) | G (Intq -> ar)

there will be:

varianceTyArgs = [Bivariant , Covariant, Contravatiant, Invariant] variancePsArgs = [Covariant, Contravatiant, Bivariant]

Constructors

TyConInfo
Fields varianceTyArgs :: !VarianceInfo variance info for type variables variancePsArgs :: !VarianceInfo variance info for predicate variables sizeFunction :: !(Maybe (Symbol -> Expr)) logical function that computes the size of the structure

Instances

Data TyConInfo
Show TyConInfo
Generic TyConInfo
Default TyConInfo
Typeable * TyConInfo
type Rep TyConInfo

defaultTyConInfo :: TyConInfo Source

rTyConPVs :: RTyCon -> [RPVar] Source

rTyConPropVs :: RTyCon -> [PVar RSort] Source

isClassRTyCon :: RTyCon -> Bool Source

Accessors for RTyCon

isClassType :: TyConable c => RType c t t1 -> Bool Source

Refinement Types

data RType c tv r Source

Constructors

RVar
Fields rt_var :: !tv rt_reft :: !r
RFun
Fields rt_bind :: !Symbol rt_in :: !(RType c tv r) rt_out :: !(RType c tv r) rt_reft :: !r
RAllT
Fields rt_tvbind :: !tv rt_ty :: !(RType c tv r)
RAllP
Fields rt_pvbind :: !(PVar (RType c tv ())) rt_ty :: !(RType c tv r)
RAllS
Fields rt_sbind :: !Symbol rt_ty :: !(RType c tv r)
RApp
Fields rt_tycon :: !c rt_args :: ![RType c tv r] rt_pargs :: ![RTProp c tv r] rt_reft :: !r
RAllE
Fields rt_bind :: !Symbol rt_allarg :: !(RType c tv r) rt_ty :: !(RType c tv r)
REx
Fields rt_bind :: !Symbol rt_exarg :: !(RType c tv r) rt_ty :: !(RType c tv r)
RExprArg Expr	For expression arguments to type aliases see testsposvector2.hs
RAppTy
Fields rt_arg :: !(RType c tv r) rt_res :: !(RType c tv r) rt_reft :: !r
RRTy
Fields rt_env :: ![(Symbol, RType c tv r)] rt_ref :: !r rt_obl :: !Oblig rt_ty :: !(RType c tv r)
RHole r	let LH match against the Haskell type and add k-vars, e.g. `x:_` see testsposHoles.hs

Instances

Eq Error
Ord Error
Show Error
ToJSON Error
FromJSON Error
Exception Error
NFData PrType
Inputable BareType	Bundling Parsers into a Typeclass ------------------------
Error Error
Result Error
PPrint Error	Pretty Printing Error Messages ------------------------------------ Need to put `PPrint Error` instance here (instead of in Types), as it depends on `PPrint SpecTypes`, which lives in this module.
SubStratum SpecType
SubsTy Symbol BSort LocSymbol
SubsTy Symbol BSort BSort
SubsTy RTyVar RSort SpecType
SubsTy RTyVar RSort PrType
SubsTy RTyVar RSort RSort
SubsTy RTyVar RSort RTyCon
SubsTy RTyVar RTyVar SpecType
(SubsTy tv ty (UReft r), SubsTy tv ty (RType c tv ())) => SubsTy tv ty (RTProp c tv (UReft r))
(Freshable m Integer, Freshable m r, Reftable r, RefTypable RTyCon RTyVar r) => Freshable m (RRType r)
ToJSON (FixResult Error)
FromJSON (FixResult Error)
Exception [Error]
Fixpoint (FixResult Error)
Subable (RRProp Reft)	Subable Instances -----------------------------------------------------
Result [Error]
SubStratum (Annot SpecType)
Functor (RType a b)
Inputable (Measure BareType LocSymbol)
Typeable (* -> * -> * -> *) RType
RefTypable c tv () => Eq (RType c tv ())
(Data c, Data tv, Data r) => Data (RType c tv r)
PPrint (RTProp c tv r) => Show (RTProp c tv r)
PPrint (RType c tv r) => Show (RType c tv r)
Generic (RType c tv r)
(Monoid r, Reftable r, RefTypable b c r, RefTypable b c ()) => Monoid (RTProp b c r)
(SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c, Reftable r, RefTypable c tv (), RefTypable c tv (UReft r)) => Monoid (Ref (RType c tv ()) r (RType c tv (UReft r)))
(SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c, RefTypable c tv (), RefTypable c tv r, PPrint (RType c tv r)) => Monoid (RType c tv r)
(NFData b, NFData c, NFData e) => NFData (RType b c e)
(Reftable r, RefTypable c tv r) => Subable (RTProp c tv r)
(Subable r, RefTypable c tv r) => Subable (RType c tv r)
(Reftable r, RefTypable c tv r, RefTypable c tv ()) => Reftable (RTProp c tv r)
(PPrint r, Reftable r) => Reftable (RType RTyCon RTyVar r)	Reftable Instances -------------------------------------------------------
(Reftable s, PPrint s, PPrint p, Reftable p, PPrint t, PPrint (RType b c p)) => PPrint (Ref t s (RType b c p))
RefTypable c tv r => PPrint (RType c tv r)
Transformable r => Transformable (RType c v r)
type Rep (RType c tv r)

data Ref τ r t Source

Ref describes `Prop τ` and HProp arguments applied to type constructors. For example, in [a]- v > h}>, we apply (via RApp) * the RProp denoted by `{h -> v > h}` to * the RTyCon denoted by `[]`. Thus, Ref is used for abstract-predicate (arguments) that are associated with _type constructors_ i.e. whose semantics are _dependent upon_ the data-type. In contrast, the Predicate argument in ur_pred in the UReft applies directly to any type and has semantics _independent of_ the data-type.

Constructors

RPropP	Parse-time `RProp`
Fields rf_args :: [(Symbol, τ)] rf_reft :: r
RProp	Abstract refinement associated with `RTyCon`
Fields rf_args :: [(Symbol, τ)] rf_body :: t
RHProp	Abstract heap-refinement associated with `RTyCon`
Fields rf_args :: [(Symbol, τ)] rf_heap :: World t

Instances

(SubsTy tv ty (UReft r), SubsTy tv ty (RType c tv ())) => SubsTy tv ty (RTProp c tv (UReft r))
Subable (RRProp Reft)	Subable Instances -----------------------------------------------------
Typeable (* -> * -> * -> *) Ref
(Data τ, Data r, Data t) => Data (Ref τ r t)
PPrint (RTProp c tv r) => Show (RTProp c tv r)
Generic (Ref τ r t)
(Monoid r, Reftable r, RefTypable b c r, RefTypable b c ()) => Monoid (RTProp b c r)
(SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c, Reftable r, RefTypable c tv (), RefTypable c tv (UReft r)) => Monoid (Ref (RType c tv ()) r (RType c tv (UReft r)))
(NFData a, NFData b, NFData t) => NFData (Ref t a b)
(Reftable r, RefTypable c tv r) => Subable (RTProp c tv r)
(Reftable r, RefTypable c tv r, RefTypable c tv ()) => Reftable (RTProp c tv r)
(Reftable s, PPrint s, PPrint p, Reftable p, PPrint t, PPrint (RType b c p)) => PPrint (Ref t s (RType b c p))
type Rep (Ref τ r t)

type RTProp c tv r = Ref (RType c tv ()) r (RType c tv r) Source

RTProp is a convenient alias for Ref that will save a bunch of typing. In general, perhaps we need not expose Ref directly at all.

newtype RTyVar Source

Constructors

RTV TyVar

Instances

Eq Error
Eq RTyVar
Data RTyVar
Ord Error
Ord RTyVar
Show Error
Show RTyVar
Generic RTyVar
ToJSON Error
FromJSON Error
Exception Error
NFData PrType
NFData RTyVar
Hashable RTyVar
Symbolic RTyVar
Error Error
Result Error
PPrint Error	Pretty Printing Error Messages ------------------------------------ Need to put `PPrint Error` instance here (instead of in Types), as it depends on `PPrint SpecTypes`, which lives in this module.
PPrint RTyVar
SubStratum SpecType
Typeable * RTyVar
(Reftable r, PPrint r) => RefTypable RTyCon RTyVar r
SubsTy RTyVar RSort SpecType
SubsTy RTyVar RSort PrType
SubsTy RTyVar RSort RSort
SubsTy RTyVar RSort RTyCon
SubsTy RTyVar RTyVar SpecType
(Freshable m Integer, Freshable m r, Reftable r, RefTypable RTyCon RTyVar r) => Freshable m (RRType r)
ToJSON (FixResult Error)
FromJSON (FixResult Error)
Exception [Error]
Fixpoint (FixResult Error)
Subable (RRProp Reft)	Subable Instances -----------------------------------------------------
Result [Error]
SubStratum (Annot SpecType)
(PPrint r, Reftable r) => Reftable (RType RTyCon RTyVar r)	Reftable Instances -------------------------------------------------------
type Rep RTyVar

data RTAlias tv ty Source

Refinement Type Aliases

Constructors

RTA
Fields rtName :: Symbol rtTArgs :: [tv] rtVArgs :: [tv] rtBody :: ty rtPos :: SourcePos

Instances

(Show tv, Show ty) => Show (RTAlias tv ty)

Worlds

data HSeg t Source

Constructors

HBind
Fields hs_addr :: !Symbol hs_val :: t
HVar UsedPVar

Instances

Data t => Data (HSeg t)
Generic (HSeg t)
Typeable (* -> *) HSeg
type Rep (HSeg t)

newtype World t Source

A World is a Separation Logic predicate that is essentially a sequence of binders that satisfies two invariants (TODO:LIQUID): 1. Each `hs_addr :: Symbol` appears at most once, 2. There is at most one HVar in a list.

Constructors

World [HSeg t]

Instances

Data t => Data (World t)
Generic (World t)
Monoid (World t)
Typeable (* -> *) World
type Rep (World t)

Classes describing operations on `RTypes`

class Eq c => TyConable c where Source

Minimal complete definition

isFun, isList, isTuple, ppTycon

Methods

isFun :: c -> Bool Source

isList :: c -> Bool Source

isTuple :: c -> Bool Source

ppTycon :: c -> Doc Source

isClass :: c -> Bool Source

isNumCls :: c -> Bool Source

isFracCls :: c -> Bool Source

Instances

TyConable LocSymbol
TyConable Symbol
TyConable RTyCon	TyConable Instances -------------------------------------------------------

class (TyConable c, Eq c, Eq tv, Hashable tv, Reftable r, PPrint r) => RefTypable c tv r where Source

Methods

ppRType :: Prec -> RType c tv r -> Doc Source

Instances

(TyConable c, Reftable r, PPrint r, PPrint c) => RefTypable c Symbol r
(Reftable r, PPrint r) => RefTypable RTyCon RTyVar r

class SubsTy tv ty a where Source

Methods

subt :: (tv, ty) -> a -> a Source

Instances

SubsTy tv ty Reft
SubsTy tv ty ()
SubsTy Symbol BSort LocSymbol
SubsTy Symbol BSort BSort
SubsTy RTyVar RSort SpecType
SubsTy RTyVar RSort PrType
SubsTy RTyVar RSort RSort
SubsTy RTyVar RSort RTyCon
SubsTy RTyVar RTyVar SpecType
SubsTy tv ty ty => SubsTy tv ty (PVar ty)
SubsTy tv ty ty => SubsTy tv ty (PVKind ty)
(SubsTy tv ty (UReft r), SubsTy tv ty (RType c tv ())) => SubsTy tv ty (RTProp c tv (UReft r))

Predicate Variables

data PVar t Source

Abstract Predicate Variables ----------------------------------

Constructors

PV
Fields pname :: !Symbol ptype :: !(PVKind t) parg :: !Symbol pargs :: ![(t, Symbol, Expr)]

Instances

Functor PVar
Subable UsedPVar
SubsTy tv ty ty => SubsTy tv ty (PVar ty)
Eq (PVar t)
Data t => Data (PVar t)
Ord (PVar t)
Show t => Show (PVar t)
Generic (PVar t)
NFData a => NFData (PVar a)
Hashable (PVar a)
PPrint a => PPrint (PVar a)
Resolvable t => Resolvable (PVar t)
Typeable (* -> *) PVar
type Rep (PVar t)

isPropPV :: PVar t -> Bool Source

pvType :: PVar t -> t Source

data PVKind t Source

Constructors

PVProp t
PVHProp

Instances

Functor PVKind
Foldable PVKind
Traversable PVKind
SubsTy tv ty ty => SubsTy tv ty (PVKind ty)
Data t => Data (PVKind t)
Show t => Show (PVKind t)
Generic (PVKind t)
NFData a => NFData (PVKind a)
Typeable (* -> *) PVKind
type Rep (PVKind t)

newtype Predicate Source

Constructors

Pr [UsedPVar]

Instances

Eq Predicate	Wrappers for GHC Type Elements --------------------------------
Data Predicate
Show Predicate
Generic Predicate
Monoid Predicate
NFData PrType
NFData Predicate
Subable Predicate
Reftable Predicate
PPrint Predicate
Resolvable Predicate
Typeable * Predicate
SubsTy RTyVar RSort PrType
type Rep Predicate

Refinements

data UReft r Source

Constructors

U
Fields ur_reft :: !r ur_pred :: !Predicate ur_strata :: !Strata

Instances

Eq Error
Functor UReft
Ord Error
Show Error
ToJSON Error
FromJSON Error
Exception Error
Inputable BareType	Bundling Parsers into a Typeclass ------------------------
Error Error
Result Error
PPrint Error	Pretty Printing Error Messages ------------------------------------ Need to put `PPrint Error` instance here (instead of in Types), as it depends on `PPrint SpecTypes`, which lives in this module.
SubStratum SpecType
Transformable RReft
Freshable m Integer => Freshable m RReft
SubsTy RTyVar RSort SpecType
SubsTy RTyVar RTyVar SpecType
(SubsTy tv ty (UReft r), SubsTy tv ty (RType c tv ())) => SubsTy tv ty (RTProp c tv (UReft r))
Data r => Data (UReft r)
PPrint (UReft r) => Show (UReft r)
Generic (UReft r)
ToJSON (FixResult Error)
FromJSON (FixResult Error)
Exception [Error]
Monoid a => Monoid (UReft a)
NFData r => NFData (UReft r)
Fixpoint (FixResult Error)
Subable r => Subable (UReft r)
(PPrint r, Reftable r) => Reftable (UReft r)
Result [Error]
(PPrint r, Reftable r) => PPrint (UReft r)
SubStratum (Annot SpecType)
Resolvable (UReft Reft)
Inputable (Measure BareType LocSymbol)
Typeable (* -> *) UReft
(SubsTy tv (RType c tv ()) (RType c tv ()), SubsTy tv (RType c tv ()) c, Reftable r, RefTypable c tv (), RefTypable c tv (UReft r)) => Monoid (Ref (RType c tv ()) r (RType c tv (UReft r)))
type Rep (UReft r)

Parse-time entities describing refined data types

data DataDecl Source

Values Related to Specifications ------------------------------------

Data type refinements

Constructors

D
Fields tycName :: LocSymbol Type Constructor Name tycTyVars :: [Symbol] Tyvar Parameters tycPVars :: [PVar BSort] PVar Parameters tycTyLabs :: [Symbol] PLabel Parameters tycDCons :: [(LocSymbol, [(Symbol, BareType)])] DataCon, [(fieldName, fieldType) ] tycSrcPos :: !SourcePos Source Position tycSFun :: Maybe (Symbol -> Expr) Measure that should decrease in recursive calls

Instances

Eq DataDecl
Ord DataDecl
Show DataDecl	For debugging.

data DataConP Source

Constructors

DataConP
Fields dc_loc :: !SourcePos freeTyVars :: ![RTyVar] freePred :: ![PVar RSort] freeLabels :: ![Symbol] tyConsts :: ![SpecType] FIXME: WHAT IS THIS?? tyArgs :: ![(Symbol, SpecType)] These are backwards, why?? tyRes :: !SpecType

Instances

Data DataConP
Show DataConP
PPrint DataConP
Transformable DataConP
Typeable * DataConP

data TyConP Source

Constructors

TyConP
Fields freeTyVarsTy :: ![RTyVar] freePredTy :: ![PVar RSort] freeLabelTy :: ![Symbol] varianceTs :: !VarianceInfo variancePs :: !VarianceInfo sizeFun :: !(Maybe (Symbol -> Expr))

Instances

Data TyConP
Show TyConP
PPrint TyConP
Typeable * TyConP

Pre-instantiated RType

type RRType = RType RTyCon RTyVar Source

type BRType = RType LocSymbol Symbol Source

type RRProp r = Ref RSort r (RRType r) Source

type BSort = BRType () Source

type BPVar = PVar BSort Source

Instantiated RType

type BareType = BRType RReft Source

type PrType = RRType Predicate Source

type SpecType = RRType RReft Source

type SpecProp = RRProp RReft Source

type RSort = RRType () Source

type UsedPVar = PVar () Source

type RPVar = PVar RSort Source

type RReft = UReft Reft Source

newtype REnv Source

Error Data Type ---------------------------------------------------

The type used during constraint generation, used also to define contexts for errors, hence in this file, and NOT in Constraint.hs

Constructors

REnv (HashMap Symbol SpecType)

Instances

NFData REnv
PPrint REnv

Constructing & Destructing RTypes

data RTypeRep c tv r Source

Constructor and Destructors for RTypes ----------------------------

Constructors

RTypeRep
Fields ty_vars :: [tv] ty_preds :: [PVar (RType c tv ())] ty_labels :: [Symbol] ty_binds :: [Symbol] ty_args :: [RType c tv r] ty_res :: RType c tv r

fromRTypeRep :: Monoid r => RTypeRep c tv r -> RType c tv r Source

toRTypeRep :: RType c tv r -> RTypeRep c tv r Source

mkArrow :: Monoid r => [a] -> [PVar (RType c a ())] -> [Symbol] -> [(Symbol, RType c a r)] -> RType c a r -> RType c a r Source

bkArrowDeep :: RType t t1 t2 -> ([Symbol], [RType t t1 t2], RType t t1 t2) Source

bkArrow :: RType t t1 t2 -> ([Symbol], [RType t t1 t2], RType t t1 t2) Source

safeBkArrow :: RType t t1 t2 -> ([Symbol], [RType t t1 t2], RType t t1 t2) Source

mkUnivs :: [a] -> [PVar (RType c a ())] -> [Symbol] -> RType c a r -> RType c a r Source

bkUniv :: RType t1 a t2 -> ([a], [PVar (RType t1 a ())], [Symbol], RType t1 a t2) Source

bkClass :: TyConable c => RType c tv r -> ([(c, [RType c tv r])], RType c tv r) Source

rFun :: Monoid r => Symbol -> RType c tv r -> RType c tv r -> RType c tv r Source

rCls :: Monoid r => TyCon -> [RType RTyCon tv r] -> RType RTyCon tv r Source

rRCls :: Monoid r => c -> [RType c tv r] -> RType c tv r Source

Manipulating `Predicates`

pvars :: Predicate -> [UsedPVar] Source

pappSym :: Show a => a -> Symbol Source

pToRef :: PVar a -> Refa Source

pApp :: Symbol -> [Expr] -> Pred Source

Some tests on RTypes

isBase :: RType t t1 t2 -> Bool Source

isFunTy :: RType t t1 t2 -> Bool Source

isTrivial :: (TyConable c, Reftable r) => RType c tv r -> Bool Source

Traversing `RType`

efoldReft :: (TyConable c, Reftable r) => (c -> [RType c tv r] -> [(Symbol, a)]) -> (RType c tv r -> a) -> (SEnv a -> Maybe (RType c tv r) -> r -> c1 -> c1) -> (PVar (RType c tv ()) -> SEnv a -> SEnv a) -> SEnv a -> c1 -> RType c tv r -> c1 Source

foldReft :: (TyConable c, Reftable r) => (r -> c1 -> c1) -> c1 -> RType c tv r -> c1 Source

mapReft :: (r1 -> r2) -> RType c tv r1 -> RType c tv r2 Source

mapReftM :: Monad m => (r1 -> m r2) -> RType c tv r1 -> m (RType c tv r2) Source

mapBot :: (RType c tv s -> RType c tv s) -> RType c tv s -> RType c tv s Source

mapBind :: (Symbol -> Symbol) -> RType c tv r -> RType c tv r Source

???

data Oblig Source

Constructors

OTerm	Obligation that proves termination
OInv	Obligation that proves invariants
OCons	Obligation that proves constraints

Instances

Data Oblig
Show Oblig
Generic Oblig
PPrint Oblig
Typeable * Oblig
type Rep Oblig

ignoreOblig :: RType t t1 t2 -> RType t t1 t2 Source

addTermCond :: SpecType -> RReft -> SpecType Source

addInvCond :: SpecType -> RReft -> SpecType Source

Inferred Annotations

newtype AnnInfo a Source

Annotations -------------------------------------------------------

Constructors

AI (HashMap SrcSpan [(Maybe Text, a)])

Instances

Functor AnnInfo
Generic (AnnInfo a)
ToJSON a => ToJSON (AnnInfo a)
FromJSON a => FromJSON (AnnInfo a)
Monoid (AnnInfo a)
NFData a => NFData (AnnInfo a)
PPrint a => PPrint (AnnInfo a)
type Rep (AnnInfo a)

data Annot t Source

Constructors

AnnUse t
AnnDef t
AnnRDf t
AnnLoc SrcSpan

Instances

NFData (Annot a)
PPrint t => PPrint (Annot t)
SubStratum (Annot SpecType)

Overall Output

data Output a Source

Output ------------------------------------------------------------

Constructors

O
Fields o_vars :: Maybe [String] o_errors :: ![Error] o_types :: !(AnnInfo a) o_templs :: !(AnnInfo a) o_bots :: ![SrcSpan] o_result :: FixResult Error

Instances

Generic (Output a)
ToJSON (Output Doc)
FromJSON (Output Doc)
Monoid (Output a)
type Rep (Output a)

Refinement Hole

hole :: Refa Source

isHole :: Refa -> Bool Source

hasHole :: Reftable r => r -> Bool Source

Converting To and From Sort

ofRSort :: Reftable r => RType c tv () -> RType c tv r Source

toRSort :: RType c tv r -> RType c tv () Source

rTypeValueVar :: Reftable r => RType c tv r -> Symbol Source

rTypeReft :: Reftable r => RType c tv r -> Reft Source

stripRTypeBase :: RType t t1 a -> Maybe a Source

Class for values that can be pretty printed

class PPrint a where Source

Minimal complete definition

pprint

Methods

pprint :: a -> Doc Source

pprintTidy :: Tidy -> a -> Doc Source

Instances

PPrint Int
PPrint Integer
PPrint String
PPrint ()
PPrint Text
PPrint SourceError
PPrint ErrMsg
PPrint Class
PPrint DataCon
PPrint Var
PPrint SrcSpan
PPrint Type
PPrint Name
PPrint Doc
PPrint Sort
PPrint SymConst
PPrint Constant
PPrint Brel
PPrint Bop
PPrint Expr
PPrint Pred
PPrint Refa
PPrint Reft
PPrint SortedReft
PPrint Symbol
PPrint ParseError
PPrint SourcePos
PPrint KVProf
PPrint KVKind
PPrint Body
PPrint Error	Pretty Printing Error Messages ------------------------------------ Need to put `PPrint Error` instance here (instead of in Types), as it depends on `PPrint SpecTypes`, which lives in this module.
PPrint EMsg
PPrint REnv
PPrint Strata
PPrint Stratum
PPrint Oblig
PPrint RTyCon
PPrint RTyVar
PPrint Predicate
PPrint TargetVars
PPrint DataConP
PPrint TyConP
PPrint GhcSpec
PPrint GhcInfo
PPrint CGInfo
PPrint WfC
PPrint SubC
PPrint CGEnv
PPrint a => PPrint [a]
PPrint [CoreBind]
PPrint a => PPrint (Maybe a)
PPrint a => PPrint (Located a)
PPrint t => PPrint (Annot t)
PPrint a => PPrint (AnnInfo a)
PPrint a => PPrint (Def a)
PPrint t => PPrint (CMeasure t)
(PPrint r, Reftable r) => PPrint (UReft r)
PPrint a => PPrint (PVar a)
(PPrint a, PPrint b) => PPrint (a, b)
(Ord k, PPrint k, PPrint v) => PPrint (HashMap k v)
(PPrint t, PPrint a) => PPrint (Measure t a)
(PPrint t, PPrint a) => PPrint (MSpec t a)
(Reftable s, PPrint s, PPrint p, Reftable p, PPrint t, PPrint (RType b c p)) => PPrint (Ref t s (RType b c p))
RefTypable c tv r => PPrint (RType c tv r)

showpp :: PPrint a => a -> String Source

Printer Configuration

data PPEnv Source

Constructors

PP
Fields ppPs :: Bool ppTyVar :: Bool ppSs :: Bool ppShort :: Bool

data Tidy Source

Printer ----------------------------------------------------------------

Constructors

Lossy
Full

Instances

Eq Tidy
Ord Tidy

ppEnv :: PPEnv Source

ppEnvShort :: PPEnv -> PPEnv Source

Modules and Imports

data ModName Source

Constructors

ModName !ModType !ModuleName

Instances

Eq ModName
Ord ModName
Show ModName
Symbolic ModName

data ModType Source

Constructors

Target
SrcImport
SpecImport

Instances

Eq ModType
Ord ModType

isSrcImport :: ModName -> Bool Source

isSpecImport :: ModName -> Bool Source

getModName :: ModName -> ModuleName Source

getModString :: ModName -> String Source

Refinement Type Aliases

data RTEnv Source

Constructors

RTE
Fields typeAliases :: HashMap Symbol (RTAlias RTyVar SpecType) predAliases :: HashMap Symbol (RTAlias Symbol Pred) exprAliases :: HashMap Symbol (RTAlias Symbol Expr)

Instances

Monoid RTEnv

mapRT :: (HashMap Symbol (RTAlias RTyVar SpecType) -> HashMap Symbol (RTAlias RTyVar SpecType)) -> RTEnv -> RTEnv Source

mapRP :: (HashMap Symbol (RTAlias Symbol Pred) -> HashMap Symbol (RTAlias Symbol Pred)) -> RTEnv -> RTEnv Source

mapRE :: (HashMap Symbol (RTAlias Symbol Expr) -> HashMap Symbol (RTAlias Symbol Expr)) -> RTEnv -> RTEnv Source

Final Result

class Result a where Source

Converting Results To Answers -------------------------------------

Methods

result :: a -> FixResult Error Source

Instances

Result SourceError	Convert a GHC error into one of ours
Result Error
Result [Error]
Result (FixResult Cinfo)

Errors and Error Messages

type Error = TError SpecType Source

In the below, we use EMsg instead of, say, SpecType because the latter is impossible to serialize, as it contains GHC internals like TyCon and Class inside it.

data TError t Source

INVARIANT : all Error constructors should have a pos field

Constructors

ErrSubType	liquid type error
Fields pos :: !SrcSpan msg :: !Doc ctx :: !(HashMap Symbol t) tact :: !t texp :: !t
ErrAssType	liquid type error
Fields pos :: !SrcSpan obl :: !Oblig msg :: !Doc ref :: !RReft
ErrParse	specification parse error
Fields pos :: !SrcSpan msg :: !Doc err :: !ParseError
ErrTySpec	sort error in specification
Fields pos :: !SrcSpan var :: !Doc typ :: !t msg :: !Doc
ErrTermSpec	sort error in specification
Fields pos :: !SrcSpan var :: !Doc exp :: !Expr msg :: !Doc
ErrDupAlias	multiple alias with same name error
Fields pos :: !SrcSpan var :: !Doc kind :: !Doc locs :: ![SrcSpan]
ErrDupSpecs	multiple specs for same binder error
Fields pos :: !SrcSpan var :: !Doc locs :: ![SrcSpan]
ErrBadData	multiple specs for same binder error
Fields pos :: !SrcSpan var :: !Doc msg :: !Doc
ErrInvt	Invariant sort error
Fields pos :: !SrcSpan inv :: !t msg :: !Doc
ErrIAl	Using sort error
Fields pos :: !SrcSpan inv :: !t msg :: !Doc
ErrIAlMis	Incompatible using error
Fields pos :: !SrcSpan t1 :: !t t2 :: !t msg :: !Doc
ErrMeas	Measure sort error
Fields pos :: !SrcSpan ms :: !Symbol msg :: !Doc
ErrHMeas	Haskell bad Measure error
Fields pos :: !SrcSpan ms :: !Symbol msg :: !Doc
ErrUnbound	Unbound symbol in specification
Fields pos :: !SrcSpan var :: !Doc
ErrGhc	GHC error: parsing or type checking
Fields pos :: !SrcSpan msg :: !Doc
ErrMismatch	Mismatch between Liquid and Haskell types
Fields pos :: !SrcSpan var :: !Doc hs :: !Type texp :: !t
ErrAliasCycle	Cyclic Refined Type Alias Definitions
Fields pos :: !SrcSpan acycle :: ![(SrcSpan, Doc)]
ErrIllegalAliasApp	Illegal RTAlias application (from BSort, eg. in PVar)
Fields pos :: !SrcSpan dname :: !Doc dpos :: !SrcSpan
ErrAliasApp
Fields pos :: !SrcSpan nargs :: !Int dname :: !Doc dpos :: !SrcSpan dargs :: !Int
ErrSaved	Previously saved error, that carries over after DiffCheck
Fields pos :: !SrcSpan msg :: !Doc
ErrTermin	Termination Error
Fields bind :: ![Var] pos :: !SrcSpan msg :: !Doc
ErrRClass	Refined Class/Interfaces Conflict
Fields pos :: !SrcSpan cls :: !Doc insts :: ![(SrcSpan, Doc)]
ErrOther	Unexpected PANIC
Fields pos :: !SrcSpan msg :: !Doc

Instances

Eq Error
Functor TError
Ord Error
Show Error
ToJSON Error
FromJSON Error
Exception Error
Error Error
Result Error
PPrint Error	Pretty Printing Error Messages ------------------------------------ Need to put `PPrint Error` instance here (instead of in Types), as it depends on `PPrint SpecTypes`, which lives in this module.
ToJSON (FixResult Error)
FromJSON (FixResult Error)
Exception [Error]
Fixpoint (FixResult Error)
Result [Error]
Typeable (* -> *) TError

newtype EMsg Source

Constructors

EMsg String

Instances

Data EMsg
Generic EMsg
PPrint EMsg
Typeable * EMsg
type Rep EMsg

type ErrorResult = FixResult Error Source

errSpan :: TError a -> SrcSpan Source

errOther :: Doc -> Error Source

Source information (associated with constraints)

data Cinfo Source

Source Information Associated With Constraints --------------------

Constructors

Ci
Fields ci_loc :: !SrcSpan ci_err :: !(Maybe Error)

Instances

Eq Cinfo
Ord Cinfo
NFData Cinfo
Result (FixResult Cinfo)

Measures

data Measure ty ctor Source

Constructors

M
Fields name :: LocSymbol sort :: ty eqns :: [Def ctor]

Instances

Bifunctor Measure
Functor (Measure t)
(Data ty, Data ctor) => Data (Measure ty ctor)
PPrint (Measure t a) => Show (Measure t a)
Inputable (Measure BareType LocSymbol)
Subable (Measure ty ctor)
(PPrint t, PPrint a) => PPrint (Measure t a)
Transformable (Measure t c)
Typeable (* -> * -> *) Measure

data CMeasure ty Source

Constructors

CM
Fields cName :: LocSymbol cSort :: ty

Instances

Functor CMeasure
PPrint (CMeasure t) => Show (CMeasure t)
PPrint t => PPrint (CMeasure t)

data Def ctor Source

Constructors

Def
Fields measure :: LocSymbol ctor :: ctor binds :: [Symbol] body :: Body

Instances

Functor Def
Eq ctor => Eq (Def ctor)
Data ctor => Data (Def ctor)
Show ctor => Show (Def ctor)
Subable (Def ctor)
PPrint a => PPrint (Def a)
Transformable (Def c)
Typeable (* -> *) Def

data Body Source

Constructors

E Expr	Measure Refinement: {v \| v = e }
P Pred	Measure Refinement: {v \| (? v) = p }
R Symbol Pred	Measure Refinement: {v \| p}

Instances

Eq Body
Data Body
Show Body
Subable Body
PPrint Body
Transformable Body
Typeable * Body

Type Classes

data RClass ty Source

Constructors

RClass
Fields rcName :: LocSymbol rcSupers :: [ty] rcTyVars :: [Symbol] rcMethods :: [(LocSymbol, ty)]

Instances

Functor RClass
Show ty => Show (RClass ty)

KV Profiling

data KVKind Source

KVar Profile -----------------------------------------

Constructors

RecBindE
NonRecBindE
TypeInstE
PredInstE
LamE
CaseE
LetE

Instances

Enum KVKind
Eq KVKind
Data KVKind
Ord KVKind
Show KVKind
Generic KVKind
NFData KVKind
Hashable KVKind
PPrint KVKind
Typeable * KVKind
type Rep KVKind

data KVProf Source

Instances

NFData KVProf
PPrint KVProf

emptyKVProf :: KVProf Source

updKVProf :: KVKind -> [Symbol] -> KVProf -> KVProf Source

Misc

mapRTAVars :: (a -> tv) -> RTAlias a ty -> RTAlias tv ty Source

insertsSEnv :: SEnv a -> [(Symbol, a)] -> SEnv a Source

Strata

data Stratum Source

Constructors

SVar Symbol
SDiv
SWhnf
SFin

Instances

Eq Stratum
Data Stratum
Show Stratum	PPrint -----------------------------------------------------------------
Generic Stratum
Monoid Strata
NFData Strata
Subable Strata
Subable Stratum
Reftable Strata
PPrint Strata
PPrint Stratum
SubStratum Stratum
Typeable * Stratum
Freshable m Integer => Freshable m Strata
type Rep Stratum