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
- Errors and Error Messages
- Source information (associated with constraints)
- Measures
- Type Classes
- KV Profiling
- Misc
- Strata
- CoreToLogic
- Refined Instances
- Ureftable Instances
- String Literals
This module should contain all the global type definitions and basic instances.
- data Config = Config {
- files :: [FilePath]
- idirs :: [FilePath]
- newcheck :: Bool
- diffcheck :: Bool
- linear :: Bool
- higherorder :: Bool
- fullcheck :: Bool
- saveQuery :: Bool
- binders :: [String]
- noCheckUnknown :: Bool
- notermination :: Bool
- autoproofs :: Bool
- nowarnings :: Bool
- trustinternals :: Bool
- nocaseexpand :: Bool
- strata :: Bool
- notruetypes :: Bool
- totality :: Bool
- noPrune :: Bool
- cores :: Maybe Int
- minPartSize :: Int
- maxPartSize :: Int
- maxParams :: Int
- smtsolver :: Maybe SMTSolver
- shortNames :: Bool
- shortErrors :: Bool
- cabalDir :: Bool
- ghcOptions :: [String]
- cFiles :: [String]
- eliminate :: Bool
- port :: Int
- exactDC :: Bool
- scrapeImports :: Bool
- scrapeUsedImports :: Bool
- elimStats :: Bool
- class HasConfig t where
- hasOpt :: HasConfig t => t -> (Config -> Bool) -> Bool
- data GhcInfo = GI {}
- data GhcSpec = SP {
- tySigs :: ![(Var, Located SpecType)]
- asmSigs :: ![(Var, Located SpecType)]
- inSigs :: ![(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)
- autosize :: !(HashSet TyCon)
- config :: !Config
- exports :: !NameSet
- measures :: [Measure SpecType DataCon]
- tyconEnv :: HashMap TyCon RTyCon
- dicts :: DEnv Var SpecType
- axioms :: [HAxiom]
- logicMap :: LogicMap
- proofType :: Maybe Type
- 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
- isEqType :: TyConable c => RType c 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 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 = MkUReft {}
- 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 (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
- 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 :: (Foldable t, Foldable t1, Foldable t2, Foldable t3) => t tv -> t1 (PVar (RType c tv ())) -> t2 Symbol -> t3 (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 tv -> t1 (PVar (RType c tv ())) -> t2 Symbol -> RType c tv r -> RType c tv 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
- 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) => (c -> [RType c tv r] -> [(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) => (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)
- 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
- 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 t t1 a -> Maybe a
- class PPrint a where
- pprintTidy :: Tidy -> a -> Doc
- pprintPrec :: Int -> Tidy -> a -> Doc
- 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
- data RTEnv = RTE {}
- 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 :: [(Symbol, [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 ty))
- data RInstance t = RI {}
- class Reftable r => UReftable r where
- liquidBegin :: String
- liquidEnd :: String
- data Axiom b s e = Axiom {}
- type HAxiom = Axiom Var Type CoreExpr
- type LAxiom = Axiom Symbol Sort Expr
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 | |
|
Located Things
data Located a :: * -> *
Functor Located | |
Foldable Located | |
Traversable Located | |
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 | |
type Rep (Located a) = D1 D1Located (C1 C1_0Located ((:*:) (S1 S1_0_0Located (Rec0 SourcePos)) ((:*:) (S1 S1_0_1Located (Rec0 SourcePos)) (S1 S1_0_2Located (Rec0 a))))) |
Symbols
type LocSymbol = Located Symbol
Located Symbols -----------------------------------------------------
Default unknown name
Refined Type Constructors
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 | |
(Freshable m Integer, Freshable m r, Reftable r, RefTypable RTyCon RTyVar 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]
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 (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 |
SubStratum SpecType Source | |
Result Error Source | |
(Freshable m Integer, Freshable m r, Reftable r, RefTypable RTyCon RTyVar r) => Freshable m (RRType r) Source | |
SubStratum (Annot SpecType) Source | |
Result [Error] Source | |
Functor (RType c tv) Source | |
(PPrint r, Reftable r, PPrint t, PPrint (RType c tv r)) => PPrint (Ref t (RType c tv r)) Source | |
(Data c, Data tv, Data r) => Data (RType c tv r) Source | |
Generic (RType c tv r) Source | |
(NFData c, NFData tv, NFData r) => NFData (RType c tv r) Source | |
(Reftable r, RefTypable c tv r) => Subable (RTProp c tv r) Source | |
(Subable r, RefTypable c tv r) => Subable (RType c tv r) Source | |
Transformable r => Transformable (RType c v 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.
Functor (Ref τ) Source | |
(Data τ, Data t) => Data (Ref τ t) Source | |
Generic (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, RefTypable c tv r) => 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.
Data RTyVar Source | |
Generic RTyVar Source | |
NFData RTyVar Source | |
Symbolic RTyVar Source | |
PPrint RTyVar Source | |
SubStratum SpecType Source | |
Result Error Source | |
(Freshable m Integer, Freshable m r, Reftable r, RefTypable RTyCon RTyVar r) => Freshable m (RRType r) Source | |
SubStratum (Annot SpecType) Source | |
Result [Error] Source | |
type Rep RTyVar Source |
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
Predicate Variables
Abstract Predicate Variables ----------------------------------
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 | |
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
Functor UReft Source | |
SubStratum SpecType Source | |
Result Error Source | |
Transformable RReft Source | |
Freshable m Integer => Freshable m RReft Source | |
Data r => Data (UReft r) Source | |
Generic (UReft r) Source | |
Monoid a => Monoid (UReft a) Source | |
NFData r => NFData (UReft r) 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
Values Related to Specifications ------------------------------------
Data type refinements
D | |
|
TyConP | |
|
Pre-instantiated RType
Instantiated RType
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
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 :: (Foldable t, Foldable t1, Foldable t2, Foldable t3) => t tv -> t1 (PVar (RType c tv ())) -> t2 Symbol -> t3 (Symbol, RType c tv r, r) -> RType c tv r -> RType c tv r Source
mkUnivs :: (Foldable t, Foldable t1, Foldable t2) => t tv -> t1 (PVar (RType c tv ())) -> t2 Symbol -> RType c tv r -> RType c tv r Source
Manipulating Predicates
Some tests on RTypes
Traversing RType
efoldReft :: (Reftable r, TyConable c) => (c -> [RType c tv r] -> [(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) => (RType c tv r -> b) -> (SEnv b -> Maybe (RType c tv r) -> r -> a -> a) -> a -> RType c tv r -> a Source
???
Different kinds of Check Obligations ------------------------------------
ignoreOblig :: RType t t1 t2 -> RType t t1 t2 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
class PPrint a where
Implement either pprintTidy
or pprintPrec
Nothing
pprintTidy :: Tidy -> a -> Doc
pprintPrec :: Int -> Tidy -> a -> Doc
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
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
Bifunctor Measure Source | |
Functor (Measure ty) Source | |
(Data ty, Data ctor) => Data (Measure ty ctor) Source | |
PPrint (Measure t a) => Show (Measure t a) Source | |
Generic (Measure ty ctor) Source | |
Subable (Measure ty ctor) Source | |
(PPrint t, PPrint a) => PPrint (Measure t a) Source | |
Transformable (Measure t c) Source | |
type Rep (Measure ty ctor) Source |
Bifunctor Def Source | |
Functor (Def ty) Source | |
(Eq ty, Eq ctor) => Eq (Def ty ctor) Source | |
(Data ty, Data ctor) => Data (Def ty ctor) Source | |
(Show ty, Show ctor) => Show (Def ty ctor) Source | |
Generic (Def ty ctor) Source | |
Subable (Def ty ctor) Source | |
PPrint a => PPrint (Def t a) Source | |
Transformable (Def t c) Source | |
type Rep (Def ty ctor) Source |
Bifunctor MSpec Source | |
Functor (MSpec ty) Source | |
(Data ty, Data ctor) => 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
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 Source | |
Data Stratum Source | |
Show Stratum Source | PPrint ----------------------------------------------------------------- |
Generic Stratum Source | |
Monoid Strata 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
Refined Instances
Refined Instances ---------------------------------------------------
Ureftable Instances
String Literals
Values Related to Specifications ------------------------------------