| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Haskell.Liquid.Types
Contents
- Options
- Ghc Information
- F.Located Things
- Symbols
- Default unknown name
- Bare Type Constructors and Variables
- Refined Type Constructors
- Refinement Types
- Worlds
- Classes describing operations on
RTypes - Type Variables
- 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
- Errors and Error Messages
- Source information (associated with constraints)
- Measures
- Type Classes
- KV Profiling
- Misc
- Strata
- CoreToLogic
- Refined Instances
- Ureftable Instances
- String Literals
- Orphan instances
Description
This module should contain all the global type definitions and basic instances.
- data Config = Config {
- files :: [FilePath]
- idirs :: [FilePath]
- diffcheck :: Bool
- linear :: Bool
- stringTheory :: Bool
- higherorder :: Bool
- higherorderqs :: Bool
- extensionality :: Bool
- alphaEquivalence :: Bool
- betaEquivalence :: Bool
- normalForm :: Bool
- fullcheck :: Bool
- saveQuery :: Bool
- checks :: [String]
- noCheckUnknown :: Bool
- notermination :: Bool
- gradual :: Bool
- gdepth :: Int
- ginteractive :: Bool
- totalHaskell :: Bool
- autoproofs :: Bool
- nowarnings :: Bool
- noannotations :: Bool
- trustInternals :: Bool
- nocaseexpand :: Bool
- strata :: Bool
- notruetypes :: Bool
- nototality :: Bool
- pruneUnsorted :: Bool
- cores :: Maybe Int
- minPartSize :: Int
- maxPartSize :: Int
- maxParams :: Int
- smtsolver :: Maybe SMTSolver
- shortNames :: Bool
- shortErrors :: Bool
- cabalDir :: Bool
- ghcOptions :: [String]
- cFiles :: [String]
- eliminate :: Eliminate
- port :: Int
- exactDC :: Bool
- noADT :: Bool
- noMeasureFields :: Bool
- scrapeImports :: Bool
- scrapeInternals :: Bool
- scrapeUsedImports :: Bool
- elimStats :: Bool
- elimBound :: Maybe Int
- json :: Bool
- counterExamples :: Bool
- timeBinds :: Bool
- noPatternInline :: Bool
- untidyCore :: Bool
- noSimplifyCore :: Bool
- nonLinCuts :: Bool
- autoInstantiate :: Instantiate
- debugInstantionation :: Bool
- noslice :: Bool
- noLiftedImport :: Bool
- proofLogicEval :: Bool
- class HasConfig t where
- data GhcInfo = GI {}
- data GhcSpec = SP {
- gsTySigs :: ![(Var, LocSpecType)]
- gsAsmSigs :: ![(Var, LocSpecType)]
- gsInSigs :: ![(Var, LocSpecType)]
- gsCtors :: ![(Var, LocSpecType)]
- gsLits :: ![(Symbol, LocSpecType)]
- gsMeas :: ![(Symbol, LocSpecType)]
- gsInvariants :: ![(Maybe Var, LocSpecType)]
- gsIaliases :: ![(LocSpecType, LocSpecType)]
- gsDconsP :: ![Located DataCon]
- gsTconsP :: ![(TyCon, TyConP)]
- gsFreeSyms :: ![(Symbol, Var)]
- gsTcEmbeds :: TCEmb TyCon
- gsQualifiers :: ![Qualifier]
- gsADTs :: ![DataDecl]
- gsTgtVars :: ![Var]
- gsDecr :: ![(Var, [Int])]
- gsTexprs :: ![(Var, [Located Expr])]
- gsNewTypes :: ![(TyCon, LocSpecType)]
- gsLvars :: !(HashSet Var)
- gsLazy :: !(HashSet Var)
- gsAutosize :: !(HashSet TyCon)
- gsAutoInst :: !(HashMap Var (Maybe Int))
- gsConfig :: !Config
- gsExports :: !NameSet
- gsMeasures :: [Measure SpecType DataCon]
- gsTyconEnv :: HashMap TyCon RTyCon
- gsDicts :: DEnv Var SpecType
- gsAxioms :: [AxiomEq]
- gsReflects :: [Var]
- gsLogicMap :: LogicMap
- gsProofType :: Maybe Type
- gsRTAliases :: !RTEnv
- 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 BTyCon = BTyCon {}
- mkBTyCon :: LocSymbol -> BTyCon
- mkClassBTyCon :: LocSymbol -> BTyCon
- mkPromotedBTyCon :: LocSymbol -> BTyCon
- isClassBTyCon :: BTyCon -> Bool
- newtype BTyVar = BTV Symbol
- data RTyCon = RTyCon TyCon ![RPVar] !TyConInfo
- data TyConInfo = TyConInfo {}
- defaultTyConInfo :: TyConInfo
- rTyConPVs :: RTyCon -> [RPVar]
- rTyConPropVs :: RTyCon -> [PVar RSort]
- isClassType :: TyConable c => RType c t t1 -> Bool
- isEqType :: TyConable c => RType c t t1 -> Bool
- isRVar :: RType c tv r -> Bool
- isBool :: RType RTyCon t t1 -> Bool
- data RType c tv r
- data Ref τ t = RProp {}
- type RTProp c tv r = Ref (RType c tv ()) (RType c tv r)
- rPropP :: [(Symbol, τ)] -> r -> Ref τ (RType c tv r)
- newtype RTyVar = RTV TyVar
- data RTAlias x a = RTA {}
- type OkRT c tv r = (TyConable c, PPrint tv, PPrint c, PPrint r, Reftable r, Reftable (RTProp c tv ()), Reftable (RTProp c tv r), Eq c, Eq tv, Hashable tv)
- lmapEAlias :: LMap -> RTAlias Symbol Expr
- data HSeg t
- newtype World t = World [HSeg t]
- class Eq c => TyConable c where
- class SubsTy tv ty a where
- data RTVar tv s = RTVar {
- ty_var_value :: tv
- ty_var_info :: RTVInfo s
- data RTVInfo s
- makeRTVar :: tv -> RTVar tv s
- mapTyVarValue :: (tv1 -> tv2) -> RTVar tv1 s -> RTVar tv2 s
- dropTyVarInfo :: RTVar tv s1 -> RTVar tv s2
- rTVarToBind :: RTVar RTyVar s -> Maybe (Symbol, s)
- data PVar t = PV {}
- isPropPV :: PVar t -> Bool
- pvType :: PVar t -> t
- data PVKind t
- newtype Predicate = Pr [UsedPVar]
- data UReft r = MkUReft {}
- data SizeFun
- szFun :: SizeFun -> Symbol -> Expr
- data DataDecl = D {}
- data DataName
- dataNameSymbol :: DataName -> LocSymbol
- data DataCtor = DataCtor {}
- data DataConP = DataConP {}
- data HasDataDecl
- hasDecl :: DataDecl -> HasDataDecl
- data DataDeclKind
- data TyConP = TyConP {
- ty_loc :: !SourcePos
- freeTyVarsTy :: ![RTyVar]
- freePredTy :: ![PVar RSort]
- freeLabelTy :: ![Symbol]
- varianceTs :: !VarianceInfo
- variancePs :: !VarianceInfo
- sizeFun :: !(Maybe SizeFun)
- type RRType = RType RTyCon RTyVar
- type RRProp r = Ref RSort (RRType r)
- type BRType = RType BTyCon BTyVar
- type BRProp r = Ref BSort (BRType r)
- type BSort = BRType ()
- type BPVar = PVar BSort
- type RTVU c tv = RTVar tv (RType c tv ())
- type PVU c tv = PVar (RType c tv ())
- type BareType = BRType RReft
- type PrType = RRType Predicate
- type SpecType = RRType RReft
- type SpecProp = RRProp RReft
- type SpecRep = RRep RReft
- type LocBareType = Located BareType
- type LocSpecType = Located SpecType
- type RSort = RRType ()
- type UsedPVar = PVar ()
- type RPVar = PVar RSort
- type RReft = UReft Reft
- data REnv = REnv {}
- data RTypeRep c tv r = RTypeRep {}
- fromRTypeRep :: RTypeRep c tv r -> RType c tv r
- toRTypeRep :: RType c tv r -> RTypeRep c tv r
- mkArrow :: [RTVar tv (RType c tv ())] -> [PVar (RType c tv ())] -> [Symbol] -> [(Symbol, RType c tv r, r)] -> RType c tv r -> RType c tv r
- bkArrowDeep :: RType t t1 a -> ([Symbol], [RType t t1 a], [a], RType t t1 a)
- bkArrow :: RType t t1 a -> ([Symbol], [RType t t1 a], [a], RType t t1 a)
- safeBkArrow :: RType t t1 a -> ([Symbol], [RType t t1 a], [a], RType t t1 a)
- mkUnivs :: (Foldable t, Foldable t1, Foldable t2) => t (RTVar tv (RType c tv ())) -> t1 (PVar (RType c tv ())) -> t2 Symbol -> RType c tv r -> RType c tv r
- bkUniv :: RType tv c r -> ([RTVar c (RType tv c ())], [PVar (RType tv c ())], [Symbol], RType tv c r)
- 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
- pApp :: Symbol -> [Expr] -> Expr
- isBase :: RType t t1 t2 -> Bool
- isFunTy :: RType t t1 t2 -> Bool
- isTrivial :: (Reftable r, TyConable c) => RType c tv r -> Bool
- efoldReft :: (Reftable r, TyConable c) => (Symbol -> RType c tv r -> Bool) -> (c -> [RType c tv r] -> [(Symbol, a)]) -> (RTVar tv (RType c tv ()) -> [(Symbol, a)]) -> (RType c tv r -> a) -> (SEnv a -> Maybe (RType c tv r) -> r -> b -> b) -> (PVar (RType c tv ()) -> SEnv a -> SEnv a) -> SEnv a -> b -> RType c tv r -> b
- foldReft :: (Reftable r, TyConable c) => (SEnv (RType c tv r) -> r -> a -> a) -> a -> RType c tv r -> a
- foldReft' :: (Reftable r, TyConable c) => (Symbol -> RType c tv r -> Bool) -> (RType c tv r -> b) -> (SEnv b -> Maybe (RType c tv r) -> r -> a -> a) -> a -> RType c tv r -> a
- 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)
- mapPropM :: Monad m => (RTProp c tv r -> m (RTProp c tv r)) -> RType c tv r -> m (RType c tv r)
- mapExprReft :: (Expr -> Expr) -> RType c tv RReft -> RType c tv RReft
- mapBot :: (RType c tv r -> RType c tv r) -> RType c tv r -> RType c tv r
- mapBind :: (Symbol -> Symbol) -> RType c tv r -> RType c tv r
- foldRType :: (acc -> RType c tv r -> acc) -> acc -> RType c tv r -> acc
- data Oblig
- ignoreOblig :: RType t t1 t2 -> RType t t1 t2
- addInvCond :: SpecType -> RReft -> SpecType
- newtype AnnInfo a = AI (HashMap SrcSpan [(Maybe Text, a)])
- data Annot t
- data Output a = O {}
- hole :: Expr
- isHole :: Expr -> 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 c tv r -> Maybe r
- topRTypeBase :: Reftable r => RType c tv r -> RType c tv r
- class PPrint a where
- pprint :: PPrint a => a -> Doc
- showpp :: PPrint a => a -> String
- data PPEnv = PP {}
- ppEnv :: PPEnv
- ppEnvShort :: PPEnv -> PPEnv
- data ModName = ModName !ModType !ModuleName
- data ModType
- isSrcImport :: ModName -> Bool
- isSpecImport :: ModName -> Bool
- getModName :: ModName -> ModuleName
- getModString :: ModName -> String
- qualifyModName :: ModName -> Symbol -> Symbol
- data RTEnv = RTE {
- typeAliases :: HashMap Symbol (RTAlias RTyVar SpecType)
- exprAliases :: HashMap Symbol (RTAlias Symbol Expr)
- mapRT :: (HashMap Symbol (RTAlias RTyVar SpecType) -> HashMap Symbol (RTAlias RTyVar SpecType)) -> RTEnv -> RTEnv
- mapRE :: (HashMap Symbol (RTAlias Symbol Expr) -> HashMap Symbol (RTAlias Symbol Expr)) -> RTEnv -> RTEnv
- module Language.Haskell.Liquid.Types.Errors
- type Error = TError SpecType
- type ErrorResult = FixResult UserError
- data Cinfo = Ci {}
- data Measure ty ctor = M {}
- data CMeasure ty = CM {}
- data Def ty ctor = Def {}
- data Body
- data MSpec ty ctor = MSpec {}
- data RClass ty = RClass {}
- data KVKind
- data KVProf
- emptyKVProf :: KVProf
- updKVProf :: KVKind -> Kuts -> 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
- data LogicMap = LM {}
- toLogicMap :: [(LocSymbol, [Symbol], Expr)] -> LogicMap
- eAppWithMap :: LogicMap -> Located Symbol -> [Expr] -> Expr -> Expr
- data LMap = LMap {}
- type RDEnv = DEnv Var SpecType
- newtype DEnv x ty = DEnv (HashMap x (HashMap Symbol (RISig ty)))
- data RInstance t = RI {}
- data RISig t
- class Reftable r => UReftable r where
- liquidBegin :: String
- liquidEnd :: String
- data Axiom b s e = Axiom {}
- type HAxiom = Axiom Var Type CoreExpr
- type AxiomEq = Equation
- rtyVarType :: RTyVar -> Type
Options
Constructors
| Config | |
Fields
| |
class HasConfig t where Source #
Minimal complete definition
Ghc Information
GHC Information : Code & Spec ------------------------------
Constructors
| GI | |
Fields
| |
The following is the overall type for specifications obtained from parsing the target source and dependent libraries
Constructors
| SP | |
Fields
| |
F.Located Things
Instances
| Functor Located | |
| Foldable Located | |
| Traversable Located | |
| Binary BareSpec # | |
| TyConable LocSymbol Source # | |
| Resolvable LocSymbol Source # | |
| 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) | |
| Binary a => Binary (Located a) | |
| NFData a => NFData (Located a) | |
| Hashable a => Hashable (Located a) | |
| Expression a => Expression (Located a) | |
| Subable a => Subable (Located a) | |
| Symbolic a => Symbolic (Located a) | |
| Loc (Located a) | |
| Fixpoint a => Fixpoint (Located a) | |
| PPrint a => PPrint (Located a) | |
| GhcLookup (Located Symbol) Source # | |
| ExpandAliases a => ExpandAliases (Located a) Source # | |
| type Rep (Located a) | |
Symbols
type LocSymbol = Located Symbol #
Located Symbols -----------------------------------------------------
Default unknown name
Bare Type Constructors and Variables
Constructors
| BTyCon | |
Instances
mkClassBTyCon :: LocSymbol -> BTyCon Source #
mkPromotedBTyCon :: LocSymbol -> BTyCon Source #
isClassBTyCon :: BTyCon -> Bool Source #
Constructors
| BTV Symbol |
Instances
Refined Type Constructors
Instances
| Eq RTyCon Source # | |
| Data RTyCon Source # | |
| Show RTyCon Source # | |
| Generic RTyCon Source # | |
| NFData RTyCon Source # | |
| Fixpoint RTyCon Source # | |
| PPrint RTyCon Source # | |
| TyConable RTyCon Source # | TyConable Instances ------------------------------------------------------- |
| SubStratum SpecType Source # | |
| Result Error Source # | |
| ExpandAliases SpecType Source # | |
| FreeVar RTyCon RTyVar Source # | |
| Freshable BareM Integer Source # |
|
| (Freshable m Integer, Freshable m r, Reftable r) => Freshable m (RRType r) Source # | |
| SubStratum (Annot SpecType) Source # | |
| Result [Error] Source # | |
| type Rep RTyCon 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
| |
Refinement Types
Constructors
| RVar | |
| RFun | |
| RAllT | |
| RAllP | "forall x y :: Nat, w :: Int . TYPE" ^^^^^^^^^^^^^^^^^^^ (rt_pvbind) |
| RAllS | "forall w . TYPE" ^^^^^ (rt_sbind) |
| RApp | |
| RAllE | |
| REx | |
| RExprArg (Located 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 |
Instances
| Binary BareSpec # | |
| SubStratum SpecType Source # | |
| Result Error Source # | |
| ExpandAliases SpecType Source # | |
| Freshable BareM Integer Source # |
|
| (Freshable m Integer, Freshable m r, Reftable r) => Freshable m (RRType r) Source # | |
| SubStratum (Annot SpecType) Source # | |
| Result [Error] Source # | |
| Functor (RType c tv) Source # | |
| Show tv => Show (RTVU c tv) Source # | |
| (PPrint r, Reftable r, PPrint t, PPrint (RType c tv r)) => PPrint (Ref t (RType c tv r)) Source # | |
| (Data r, Data tv, Data c) => Data (RType c tv r) Source # | |
| Generic (RType c tv r) Source # | |
| (Binary c, Binary tv, Binary r) => Binary (RType c tv r) Source # | |
| (NFData c, NFData tv, NFData r) => NFData (RType c tv r) Source # | |
| (Reftable r, TyConable c) => Subable (RTProp c tv r) Source # | |
| (Subable r, Reftable r, TyConable c) => Subable (RType c tv r) Source # | |
| type Rep (RType c tv r) 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
| RProp | |
Instances
| Functor (Ref τ) Source # | |
| (Data t, Data τ) => Data (Ref τ t) Source # | |
| Generic (Ref τ t) Source # | |
| (Binary τ, Binary t) => Binary (Ref τ t) Source # | |
| (NFData τ, NFData t) => NFData (Ref τ t) Source # | |
| (PPrint r, Reftable r, PPrint t, PPrint (RType c tv r)) => PPrint (Ref t (RType c tv r)) Source # | |
| (Reftable r, TyConable c) => Subable (RTProp c tv r) Source # | |
| type Rep (Ref τ t) Source # | |
type RTProp c tv r = Ref (RType c tv ()) (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.
Instances
| Data RTyVar Source # | |
| Generic RTyVar Source # | |
| NFData RTyVar Source # | |
| Symbolic RTyVar Source # | |
| PPrint RTyVar Source # | |
| SubStratum SpecType Source # | |
| Result Error Source # | |
| ExpandAliases SpecType Source # | |
| FreeVar RTyCon RTyVar Source # | |
| Freshable BareM Integer Source # |
|
| (Freshable m Integer, Freshable m r, Reftable r) => Freshable m (RRType r) Source # | |
| SubStratum (Annot SpecType) Source # | |
| Result [Error] Source # | |
| type Rep RTyVar Source # | |
Refinement Type Aliases
Constructors
| RTA | |
type OkRT c tv r = (TyConable c, PPrint tv, PPrint c, PPrint r, Reftable r, Reftable (RTProp c tv ()), Reftable (RTProp c tv r), Eq c, Eq tv, Hashable tv) Source #
lmapEAlias :: LMap -> RTAlias Symbol Expr Source #
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
Type Variables
Constructors
| RTVar | |
Fields
| |
Instances
| Eq tv => Eq (RTVar tv s) Source # | |
| (Data s, Data tv) => Data (RTVar tv s) Source # | |
| Show tv => Show (RTVU c tv) Source # | |
| Generic (RTVar tv s) Source # | |
| (Binary tv, Binary s) => Binary (RTVar tv s) Source # | |
| (NFData tv, NFData s) => NFData (RTVar tv s) Source # | |
| PPrint v => PPrint (RTVar v s) Source # | |
| type Rep (RTVar tv s) Source # | |
mapTyVarValue :: (tv1 -> tv2) -> RTVar tv1 s -> RTVar tv2 s Source #
dropTyVarInfo :: RTVar tv s1 -> RTVar tv s2 Source #
Predicate Variables
Abstract Predicate Variables ----------------------------------
Constructors
| PV | |
Instances
| Functor PVar Source # | |
| Subable UsedPVar Source # | |
| Eq (PVar t) Source # | |
| Data t => Data (PVar t) Source # | |
| Ord (PVar t) Source # | |
| Show t => Show (PVar t) Source # | |
| Generic (PVar t) Source # | |
| Binary t => Binary (PVar t) Source # | |
| NFData t => NFData (PVar t) Source # | |
| Hashable (PVar a) Source # | |
| PPrint (PVar a) Source # | |
| Resolvable t => Resolvable (PVar t) Source # | |
| type Rep (PVar t) Source # | |
Refinements
Instances
| Functor UReft Source # | |
| Foldable UReft Source # | |
| Traversable UReft Source # | |
| Binary BareSpec # | |
| SubStratum SpecType Source # | |
| Result Error Source # | |
| ExpandAliases SpecType Source # | |
| ExpandAliases RReft Source # | |
| Freshable m Integer => Freshable m RReft Source # | |
| Freshable BareM Integer Source # |
|
| Data r => Data (UReft r) Source # | |
| Generic (UReft r) Source # | |
| Monoid a => Monoid (UReft a) Source # | |
| Binary r => Binary (UReft r) Source # | |
| NFData r => NFData (UReft r) Source # | |
| Expression (UReft ()) Source # | |
| Subable r => Subable (UReft r) Source # | |
| (PPrint r, Reftable r) => Reftable (UReft r) Source # | |
| UReftable (UReft Reft) Source # | |
| SubStratum (Annot SpecType) Source # | |
| Result [Error] Source # | |
| Resolvable (UReft Reft) Source # | |
| type Rep (UReft r) Source # | |
Parse-time entities describing refined data types
Termination expressions
Constructors
| IdSizeFun | x -> F.EVar x |
| SymSizeFun LocSymbol | x -> f x |
Data type refinements
Constructors
| D | |
Fields
| |
Constructors
| DnName !LocSymbol | for |
| DnCon !LocSymbol | for |
Instances
dataNameSymbol :: DataName -> LocSymbol Source #
Data Constructor
Constructors
| DataCtor | |
Constructors
| DataConP | |
Fields
| |
Instances
| Data DataConP Source # | |
| Generic DataConP Source # | |
| Loc DataConP Source # |
Here the |
| ExpandAliases DataConP Source # | |
| type Rep DataConP Source # | |
data HasDataDecl Source #
Instances
hasDecl :: DataDecl -> HasDataDecl Source #
data DataDeclKind Source #
What kind of DataDecl is it?
Constructors
| DataUser | User defined data-definitions (should have refined fields) |
| DataReflected | Automatically lifted data-definitions (do not have refined fields) |
Instances
Constructors
| TyConP | |
Fields
| |
Pre-instantiated RType
type RTVU c tv = RTVar tv (RType c tv ()) Source #
Unified Representation of Refinement Types --------------------------------
Instantiated RType
type LocBareType = Located BareType Source #
type LocSpecType = Located SpecType Source #
type UsedPVar = PVar () Source #
Predicates ----------------------------------------------------------------
The type used during constraint generation, used also to define contexts for errors, hence in this file, and NOT in elsewhere. **DO NOT ATTEMPT TO MOVE** Am splitting into + global : many bindings, shared across all constraints + local : few bindings, relevant to particular constraints
Constructors
| REnv | |
Constructing & Destructing RTypes
Constructor and Destructors for RTypes ------------------------------------
fromRTypeRep :: RTypeRep c tv r -> RType c tv r Source #
toRTypeRep :: RType c tv r -> RTypeRep c tv r Source #
mkArrow :: [RTVar tv (RType c tv ())] -> [PVar (RType c tv ())] -> [Symbol] -> [(Symbol, RType c tv r, r)] -> RType c tv r -> RType c tv r Source #
mkUnivs :: (Foldable t, Foldable t1, Foldable t2) => t (RTVar tv (RType c tv ())) -> t1 (PVar (RType c tv ())) -> t2 Symbol -> RType c tv r -> RType c tv r Source #
bkUniv :: RType tv c r -> ([RTVar c (RType tv c ())], [PVar (RType tv c ())], [Symbol], RType tv c r) Source #
Manipulating Predicates
Some tests on RTypes
Traversing RType
efoldReft :: (Reftable r, TyConable c) => (Symbol -> RType c tv r -> Bool) -> (c -> [RType c tv r] -> [(Symbol, a)]) -> (RTVar tv (RType c tv ()) -> [(Symbol, a)]) -> (RType c tv r -> a) -> (SEnv a -> Maybe (RType c tv r) -> r -> b -> b) -> (PVar (RType c tv ()) -> SEnv a -> SEnv a) -> SEnv a -> b -> RType c tv r -> b Source #
foldReft :: (Reftable r, TyConable c) => (SEnv (RType c tv r) -> r -> a -> a) -> a -> RType c tv r -> a Source #
foldReft' :: (Reftable r, TyConable c) => (Symbol -> RType c tv r -> Bool) -> (RType c tv r -> b) -> (SEnv b -> Maybe (RType c tv r) -> r -> a -> a) -> a -> RType c tv r -> a Source #
mapPropM :: Monad m => (RTProp c tv r -> m (RTProp c tv r)) -> RType c tv r -> m (RType c tv r) Source #
mapExprReft :: (Expr -> Expr) -> RType c tv RReft -> RType c tv RReft Source #
Visitors ------------------------------------------------------------------
???
Different kinds of Check Obligations ------------------------------------
ignoreOblig :: RType t t1 t2 -> RType t t1 t2 Source #
Inferred Annotations
Annotations -------------------------------------------------------
Overall Output
Output --------------------------------------------------------------------
Constructors
| O | |
Refinement Hole
Converting To and From Sort
rTypeValueVar :: Reftable r => RType c tv r -> Symbol Source #
stripRTypeBase :: RType c tv r -> Maybe r Source #
Class for values that can be pretty printed
Implement either pprintTidy or pprintPrec
Instances
Printer Configuration
Printer ----------------------------------------------------------------
ppEnvShort :: PPEnv -> PPEnv Source #
Modules and Imports
Module Names --------------------------------------------------------------
Constructors
| ModName !ModType !ModuleName |
Constructors
| Target | |
| SrcImport | |
| SpecImport |
isSrcImport :: ModName -> Bool Source #
isSpecImport :: ModName -> Bool Source #
getModName :: ModName -> ModuleName Source #
getModString :: ModName -> String Source #
qualifyModName :: ModName -> Symbol -> Symbol Source #
Refinement Type Aliases
Refinement Type Aliases ---------------------------------------------------
Constructors
| RTE | |
Fields
| |
mapRT :: (HashMap Symbol (RTAlias RTyVar SpecType) -> HashMap Symbol (RTAlias RTyVar SpecType)) -> RTEnv -> RTEnv Source #
mapRE :: (HashMap Symbol (RTAlias Symbol Expr) -> HashMap Symbol (RTAlias Symbol Expr)) -> RTEnv -> RTEnv Source #
Errors and Error Messages
type ErrorResult = FixResult UserError Source #
Error Data Type -----------------------------------------------------------
Source information (associated with constraints)
Source Information Associated With Constraints ----------------------------
Measures
Instances
| Bifunctor Measure Source # | |
| Functor (Measure ty) Source # | |
| (Data ctor, Data ty) => Data (Measure ty ctor) Source # | |
| PPrint (Measure t a) => Show (Measure t a) Source # | |
| Generic (Measure ty ctor) Source # | |
| (Binary t, Binary c) => Binary (Measure t c) Source # | |
| Subable (Measure ty ctor) Source # | |
| (PPrint t, PPrint a) => PPrint (Measure t a) Source # | |
| ExpandAliases ty => ExpandAliases (Measure ty ctor) Source # | |
| type Rep (Measure ty ctor) Source # | |
Constructors
| Def | |
Instances
| Bifunctor Def Source # | |
| Functor (Def ty) Source # | |
| (Eq ctor, Eq ty) => Eq (Def ty ctor) Source # | |
| (Data ctor, Data ty) => Data (Def ty ctor) Source # | |
| (Show ctor, Show ty) => Show (Def ty ctor) Source # | |
| Generic (Def ty ctor) Source # | |
| (Binary t, Binary c) => Binary (Def t c) Source # | |
| Subable (Def ty ctor) Source # | |
| PPrint a => PPrint (Def t a) Source # | |
| ExpandAliases ty => ExpandAliases (Def ty ctor) Source # | |
| type Rep (Def ty ctor) Source # | |
Measures
Constructors
| MSpec | |
Instances
| Bifunctor MSpec Source # | |
| Functor (MSpec ty) Source # | |
| (Data ctor, Data ty) => Data (MSpec ty ctor) Source # | |
| (Show ty, Show ctor, PPrint ctor, PPrint ty) => Show (MSpec ty ctor) Source # | |
| Generic (MSpec ty ctor) Source # | |
| Eq ctor => Monoid (MSpec ty ctor) Source # | |
| (PPrint t, PPrint a) => PPrint (MSpec t a) Source # | |
| type Rep (MSpec ty ctor) Source # | |
Type Classes
Constructors
| RClass | |
KV Profiling
KVar Profile --------------------------------------------------------------
emptyKVProf :: KVProf Source #
Misc
mapRTAVars :: (a -> tv) -> RTAlias a ty -> RTAlias tv ty Source #
insertsSEnv :: SEnv a -> [(Symbol, a)] -> SEnv a Source #
Strata
Instances
| Eq Stratum Source # | |
| Data Stratum Source # | |
| Show Stratum Source # | F.PPrint ----------------------------------------------------------------- |
| Generic Stratum Source # | |
| Monoid Strata Source # | |
| Binary Stratum Source # | |
| NFData Stratum Source # | |
| Subable Stratum Source # | |
| Reftable Strata Source # | |
| PPrint Strata Source # | |
| PPrint Stratum Source # | |
| SubStratum Stratum Source # | |
| Freshable m Integer => Freshable m Strata Source # | |
| type Rep Stratum Source # | |
makeDivType :: SpecType -> SpecType Source #
makeFinType :: SpecType -> SpecType Source #
CoreToLogic
Constructors
| LM | |
toLogicMap :: [(LocSymbol, [Symbol], Expr)] -> LogicMap Source #
eAppWithMap :: LogicMap -> Located Symbol -> [Expr] -> Expr -> Expr Source #
Refined Instances
Refined Instances ---------------------------------------------------------
Ureftable Instances
String Literals
liquidBegin :: String Source #
Values Related to Specifications ------------------------------------
Constructors
| Axiom | |
rtyVarType :: RTyVar -> Type Source #