Safe Haskell | None |
---|---|
Language | Haskell98 |
- 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
This module should contain all the global type definitions and basic instances.
- data Config = Config {
- files :: [FilePath]
- idirs :: [FilePath]
- diffcheck :: Bool
- real :: Bool
- fullcheck :: Bool
- binders :: [String]
- noCheckUnknown :: Bool
- notermination :: Bool
- nowarnings :: Bool
- trustinternals :: Bool
- nocaseexpand :: Bool
- strata :: Bool
- notruetypes :: Bool
- totality :: Bool
- noPrune :: Bool
- maxParams :: Int
- smtsolver :: Maybe SMTSolver
- shortNames :: Bool
- shortErrors :: Bool
- ghcOptions :: [String]
- cFiles :: [String]
- data GhcInfo = GI {}
- data GhcSpec = SP {
- tySigs :: ![(Var, Located SpecType)]
- asmSigs :: ![(Var, Located SpecType)]
- ctors :: ![(Var, Located SpecType)]
- meas :: ![(Symbol, Located SpecType)]
- invariants :: ![Located SpecType]
- ialiases :: ![(Located SpecType, Located SpecType)]
- dconsP :: ![(DataCon, DataConP)]
- tconsP :: ![(TyCon, TyConP)]
- freeSyms :: ![(Symbol, Var)]
- tcEmbeds :: TCEmb TyCon
- qualifiers :: ![Qualifier]
- tgtVars :: ![Var]
- decr :: ![(Var, [Int])]
- texprs :: ![(Var, [Expr])]
- lvars :: !(HashSet Var)
- lazy :: !(HashSet Var)
- config :: !Config
- exports :: !NameSet
- measures :: [Measure SpecType DataCon]
- tyconEnv :: HashMap TyCon RTyCon
- dicts :: DEnv Var SpecType
- data TargetVars
- data Located a :: * -> * = Loc {}
- dummyLoc :: a -> Located a
- type LocSymbol = Located Symbol
- type LocText = Located Text
- dummyName :: Symbol
- isDummy :: Symbolic a => a -> Bool
- data RTyCon = RTyCon TyCon ![RPVar] !TyConInfo
- data TyConInfo = TyConInfo {
- varianceTyArgs :: !VarianceInfo
- variancePsArgs :: !VarianceInfo
- sizeFunction :: !(Maybe (Symbol -> Expr))
- defaultTyConInfo :: TyConInfo
- rTyConPVs :: RTyCon -> [RPVar]
- rTyConPropVs :: RTyCon -> [PVar RSort]
- isClassRTyCon :: RTyCon -> Bool
- isClassType :: TyConable c => RType c t t1 -> Bool
- data RType c tv r
- data Ref τ r t
- type RTProp c tv r = Ref (RType c tv ()) r (RType c tv r)
- newtype RTyVar = RTV TyVar
- data RTAlias tv ty = RTA {}
- data HSeg t
- newtype World t = World [HSeg t]
- class Eq c => TyConable c where
- class (TyConable c, Eq c, Eq tv, Hashable tv, Reftable r, PPrint r) => RefTypable c tv r where
- class SubsTy tv ty a where
- subt :: (tv, ty) -> a -> a
- data PVar t = PV {}
- isPropPV :: PVar t -> Bool
- pvType :: PVar t -> t
- data PVKind t
- newtype Predicate = Pr [UsedPVar]
- data UReft r = U {}
- data DataDecl = D {}
- data DataConP = DataConP {}
- data TyConP = TyConP {
- freeTyVarsTy :: ![RTyVar]
- freePredTy :: ![PVar RSort]
- freeLabelTy :: ![Symbol]
- varianceTs :: !VarianceInfo
- variancePs :: !VarianceInfo
- sizeFun :: !(Maybe (Symbol -> Expr))
- type RRType = RType RTyCon RTyVar
- type BRType = RType LocSymbol Symbol
- type RRProp r = Ref RSort r (RRType r)
- type BSort = BRType ()
- type BPVar = PVar BSort
- type BareType = BRType RReft
- type PrType = RRType Predicate
- type SpecType = RRType RReft
- type SpecProp = RRProp RReft
- type RSort = RRType ()
- type UsedPVar = PVar ()
- type RPVar = PVar RSort
- type RReft = UReft Reft
- newtype REnv = REnv (HashMap Symbol SpecType)
- data RTypeRep c tv r = RTypeRep {}
- fromRTypeRep :: Monoid r => RTypeRep c tv r -> RType c tv r
- toRTypeRep :: RType c tv r -> RTypeRep c tv r
- mkArrow :: Monoid r => [a] -> [PVar (RType c a ())] -> [Symbol] -> [(Symbol, RType c a r)] -> RType c a r -> RType c a r
- bkArrowDeep :: RType t t1 t2 -> ([Symbol], [RType t t1 t2], RType t t1 t2)
- bkArrow :: RType t t1 t2 -> ([Symbol], [RType t t1 t2], RType t t1 t2)
- safeBkArrow :: RType t t1 t2 -> ([Symbol], [RType t t1 t2], RType t t1 t2)
- mkUnivs :: [a] -> [PVar (RType c a ())] -> [Symbol] -> RType c a r -> RType c a r
- bkUniv :: RType t1 a t2 -> ([a], [PVar (RType t1 a ())], [Symbol], RType t1 a t2)
- bkClass :: TyConable c => RType c tv r -> ([(c, [RType c tv r])], RType c tv r)
- rFun :: Monoid r => Symbol -> RType c tv r -> RType c tv r -> RType c tv r
- rCls :: Monoid r => TyCon -> [RType RTyCon tv r] -> RType RTyCon tv r
- rRCls :: Monoid r => c -> [RType c tv r] -> RType c tv r
- pvars :: Predicate -> [UsedPVar]
- pappSym :: Show a => a -> Symbol
- pToRef :: PVar a -> Refa
- pApp :: Symbol -> [Expr] -> Pred
- isBase :: RType t t1 t2 -> Bool
- isFunTy :: RType t t1 t2 -> Bool
- isTrivial :: (TyConable c, Reftable r) => RType c tv r -> Bool
- 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
- foldReft :: (TyConable c, Reftable r) => (r -> c1 -> c1) -> c1 -> RType c tv r -> c1
- mapReft :: (r1 -> r2) -> RType c tv r1 -> RType c tv r2
- mapReftM :: Monad m => (r1 -> m r2) -> RType c tv r1 -> m (RType c tv r2)
- mapBot :: (RType c tv s -> RType c tv s) -> RType c tv s -> RType c tv s
- mapBind :: (Symbol -> Symbol) -> RType c tv r -> RType c tv r
- data Oblig
- ignoreOblig :: RType t t1 t2 -> RType t t1 t2
- addTermCond :: SpecType -> RReft -> SpecType
- addInvCond :: SpecType -> RReft -> SpecType
- newtype AnnInfo a = AI (HashMap SrcSpan [(Maybe Text, a)])
- data Annot t
- data Output a = O {}
- hole :: Refa
- isHole :: Refa -> Bool
- hasHole :: Reftable r => r -> Bool
- ofRSort :: Reftable r => RType c tv () -> RType c tv r
- toRSort :: RType c tv r -> RType c tv ()
- rTypeValueVar :: Reftable r => RType c tv r -> Symbol
- rTypeReft :: Reftable r => RType c tv r -> Reft
- stripRTypeBase :: RType t t1 a -> Maybe a
- class PPrint a where
- pprint :: a -> Doc
- pprintTidy :: Tidy -> a -> Doc
- showpp :: PPrint a => a -> String
- data PPEnv = PP {}
- data Tidy
- ppEnv :: PPEnv
- ppEnvShort :: PPEnv -> PPEnv
- data ModName = ModName !ModType !ModuleName
- data ModType
- isSrcImport :: ModName -> Bool
- isSpecImport :: ModName -> Bool
- getModName :: ModName -> ModuleName
- getModString :: ModName -> String
- data RTEnv = RTE {}
- mapRT :: (HashMap Symbol (RTAlias RTyVar SpecType) -> HashMap Symbol (RTAlias RTyVar SpecType)) -> RTEnv -> RTEnv
- mapRP :: (HashMap Symbol (RTAlias Symbol Pred) -> HashMap Symbol (RTAlias Symbol Pred)) -> RTEnv -> RTEnv
- mapRE :: (HashMap Symbol (RTAlias Symbol Expr) -> HashMap Symbol (RTAlias Symbol Expr)) -> RTEnv -> RTEnv
- class Result a where
- type Error = TError SpecType
- data TError t
- = ErrSubType { }
- | ErrAssType { }
- | ErrParse { }
- | ErrTySpec { }
- | ErrTermSpec { }
- | ErrDupAlias { }
- | ErrDupSpecs { }
- | ErrBadData { }
- | ErrInvt { }
- | ErrIAl { }
- | ErrIAlMis { }
- | ErrMeas { }
- | ErrHMeas { }
- | ErrUnbound { }
- | ErrGhc { }
- | ErrMismatch { }
- | ErrAliasCycle { }
- | ErrIllegalAliasApp { }
- | ErrAliasApp { }
- | ErrSaved { }
- | ErrTermin { }
- | ErrRClass { }
- | ErrOther { }
- newtype EMsg = EMsg String
- type ErrorResult = FixResult Error
- errSpan :: TError a -> SrcSpan
- errOther :: Doc -> Error
- data Cinfo = Ci {}
- data Measure ty ctor = M {}
- data CMeasure ty = CM {}
- data Def ctor = Def {}
- data Body
- data RClass ty = RClass {}
- data KVKind
- data KVProf
- emptyKVProf :: KVProf
- updKVProf :: KVKind -> [Symbol] -> KVProf -> KVProf
- mapRTAVars :: (a -> tv) -> RTAlias a ty -> RTAlias tv ty
- insertsSEnv :: SEnv a -> [(Symbol, a)] -> SEnv a
- data Stratum
- type Strata = [Stratum]
- isSVar :: Stratum -> Bool
- getStrata :: RType t t1 (UReft r) -> [Stratum]
- makeDivType :: SpecType -> SpecType
- makeFinType :: SpecType -> SpecType
- type LogicMap = HashMap Symbol LMap
- toLogicMap :: [(Symbol, [Symbol], Expr)] -> HashMap Symbol LMap
- eAppWithMap :: (Hashable k, Eq k) => HashMap k LMap -> Located k -> [Expr] -> Expr -> Expr
- data LMap = LMap {}
- type RDEnv = DEnv Var SpecType
- newtype DEnv x ty = DEnv (HashMap x (HashMap Symbol ty))
- data RInstance t = RI {}
Options
Command Line Config Options --------------------------------------------
Config | |
|
Ghc Information
GHC Information : Code & Spec ------------------------------
The following is the overall type for specifications obtained from parsing the target source and dependent libraries
SP | |
|
data TargetVars Source
Which Top-Level Binders Should be Verified
Located Things
data Located a :: * -> *
Located Values ---------------------------------------------------------
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)))) |
Symbols
Default unknown name
Refined Type Constructors
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]
TyConInfo | |
|
rTyConPropVs :: RTyCon -> [PVar RSort] Source
isClassRTyCon :: RTyCon -> Bool Source
Accessors for RTyCon
isClassType :: TyConable c => RType c t t1 -> Bool Source
Refinement Types
RVar | |
RFun | |
RAllT | |
RAllP | |
RAllS | |
RApp | |
RAllE | |
REx | |
RExprArg Expr | For expression arguments to type aliases see testsposvector2.hs |
RAppTy | |
RRTy | |
RHole r | let LH match against the Haskell type and add k-vars, e.g. `x:_` see testsposHoles.hs |
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 |
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) |
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.
RPropP | Parse-time |
RProp | Abstract refinement associated with |
RHProp | Abstract heap-refinement associated with |
(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.
Refinement Type Aliases
Worlds
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.
Classes describing operations on RTypes
class (TyConable c, Eq c, Eq tv, Hashable tv, Reftable r, PPrint r) => RefTypable c tv r where Source
class SubsTy tv ty a where Source
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
Abstract Predicate Variables ----------------------------------
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) |
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
Parse-time entities describing refined data types
Values Related to Specifications ------------------------------------
Data type refinements
D | |
|
TyConP | |
|
Pre-instantiated RType
Instantiated RType
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
Constructing & Destructing RTypes
Constructor and Destructors for RTypes ----------------------------
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
Manipulating Predicates
Some tests on RTypes
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
???
ignoreOblig :: RType t t1 t2 -> RType t t1 t2 Source
addTermCond :: SpecType -> RReft -> SpecType Source
addInvCond :: SpecType -> RReft -> SpecType Source
Inferred Annotations
Annotations -------------------------------------------------------
Overall Output
Output ------------------------------------------------------------
Refinement Hole
Converting To and From Sort
rTypeValueVar :: Reftable r => RType c tv r -> Symbol Source
stripRTypeBase :: RType t t1 a -> Maybe a Source
Class for values that can be pretty printed
Printer Configuration
Printer ----------------------------------------------------------------
ppEnvShort :: PPEnv -> PPEnv Source
Modules and Imports
isSrcImport :: ModName -> Bool Source
isSpecImport :: ModName -> Bool Source
getModName :: ModName -> ModuleName Source
getModString :: ModName -> String Source
Refinement Type Aliases
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
Converting Results To Answers -------------------------------------
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.
INVARIANT : all Error constructors should have a pos field
ErrSubType | liquid type error |
ErrAssType | liquid type error |
ErrParse | specification parse error |
ErrTySpec | sort error in specification |
ErrTermSpec | sort error in specification |
ErrDupAlias | multiple alias with same name error |
ErrDupSpecs | multiple specs for same binder error |
ErrBadData | multiple specs for same binder error |
ErrInvt | Invariant sort error |
ErrIAl | Using sort error |
ErrIAlMis | Incompatible using error |
ErrMeas | Measure sort error |
ErrHMeas | Haskell bad Measure error |
ErrUnbound | Unbound symbol in specification |
ErrGhc | GHC error: parsing or type checking |
ErrMismatch | Mismatch between Liquid and Haskell types |
ErrAliasCycle | Cyclic Refined Type Alias Definitions |
ErrIllegalAliasApp | Illegal RTAlias application (from BSort, eg. in PVar) |
ErrAliasApp | |
ErrSaved | Previously saved error, that carries over after DiffCheck |
ErrTermin | Termination Error |
ErrRClass | Refined Class/Interfaces Conflict |
ErrOther | Unexpected PANIC |
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 |
ToJSON (FixResult Error) | |
FromJSON (FixResult Error) | |
Exception [Error] | |
Fixpoint (FixResult Error) | |
Result [Error] | |
Typeable (* -> *) TError |
type ErrorResult = FixResult Error Source
Source information (associated with constraints)
Source Information Associated With Constraints --------------------
Measures
Type Classes
KV Profiling
KVar Profile -----------------------------------------
Misc
mapRTAVars :: (a -> tv) -> RTAlias a ty -> RTAlias tv ty Source
insertsSEnv :: SEnv a -> [(Symbol, a)] -> SEnv a Source
Strata
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 |
makeDivType :: SpecType -> SpecType Source
makeFinType :: SpecType -> SpecType Source