Safe Haskell	None
Language	Haskell98

Language.Haskell.Liquid.UX.Config

Description

Command Line Configuration Options ----------------------------------------

Documentation

data Config #

Constructors

Config

Fields

loggingVerbosity :: Verbosity
the logging verbosity to use (defaults to Quiet)
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
linear :: Bool
uninterpreted integer multiplication and division
stringTheory :: Bool
interpretation of string theory in the logic
higherorder :: Bool
allow higher order binders into the logic
higherorderqs :: Bool
allow higher order qualifiers
smtTimeout :: Maybe Int
smt timeout
fullcheck :: Bool
check all binders (overrides diffcheck)
saveQuery :: Bool
save fixpoint query
checks :: [String]
set of binders to check
noCheckUnknown :: Bool
whether to complain about specifications for unexported and unused values
notermination :: Bool
disable termination check
rankNTypes :: Bool
Adds precise reasoning on presence of rankNTypes
noclasscheck :: Bool
disable checking class instances , structuralTerm :: Bool -- ^ use structural termination checker
nostructuralterm :: Bool
disable structural termination check
gradual :: Bool
enable gradual type checking
bscope :: Bool
scope of the outer binders on the inner refinements
gdepth :: Int
depth of gradual concretization
ginteractive :: Bool
interactive gradual solving
totalHaskell :: Bool
Check for termination and totality, Overrides no-termination flags
nowarnings :: Bool
disable warnings output (only show errors)
noannotations :: Bool
disable creation of intermediate annotation files
checkDerived :: Bool
check internal (GHC-derived) binders
caseExpandDepth :: Int
maximum case expand nesting depth.
notruetypes :: Bool
disable truing top level types
nototality :: Bool
disable totality check in definitions
pruneUnsorted :: Bool
enable prunning unsorted Refinements
cores :: Maybe Int
number of cores used to solve constraints
minPartSize :: Int
Minimum size of a partition
maxPartSize :: Int
Maximum size of a partition. Overrides minPartSize
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.
cabalDir :: Bool
find and use .cabal file to include paths to sources for imported modules
ghcOptions :: [String]
command-line options to pass to GHC
cFiles :: [String]
.c files to compile and link against (for GHC)
eliminate :: Eliminate
eliminate (i.e. don't use qualifs for) for "none", "cuts" or "all" kvars
port :: Int
port at which lhi should listen
exactDC :: Bool
Automatically generate singleton types for data constructors
noADT :: Bool
Disable ADTs (only used with exactDC)
scrapeImports :: Bool
scrape qualifiers from imported specifications
scrapeInternals :: Bool
scrape qualifiers from auto specifications
scrapeUsedImports :: Bool
scrape qualifiers from used, imported specifications
elimStats :: Bool
print eliminate stats
elimBound :: Maybe Int
eliminate upto given depth of KVar chains
json :: Bool
print results (safe/errors) as JSON
counterExamples :: Bool
attempt to generate counter-examples to type errors
timeBinds :: Bool
check and time each (asserted) type-sig separately
noPatternInline :: Bool
treat code patterns (e.g. e1 >>= x -> e2) specially for inference
untidyCore :: Bool
print full blown core (with untidy names) in verbose mode
noSimplifyCore :: Bool
simplify GHC core before constraint-generation PLE-OPT , autoInst ntiate :: Instantiate -- ^ How to instantiate axioms
noslice :: Bool
Disable non-concrete KVar slicing
noLiftedImport :: Bool
Disable loading lifted specifications (for "legacy" libs)
proofLogicEval :: Bool
Enable proof-by-logical-evaluation
oldPLE :: Bool
Enable proof-by-logical-evaluation
proofLogicEvalLocal :: Bool
Enable proof-by-logical-evaluation locally, per function
extensionality :: Bool
Enable extensional interpretation of function equality
nopolyinfer :: Bool
No inference of polymorphic type application.
reflection :: Bool
Allow "reflection"; switches on "--higherorder" and "--exactdc"
compileSpec :: Bool
Only "compile" the spec -- into .bspec file -- don't do any checking.
noCheckImports :: Bool
Do not check the transitive imports
typedHoles :: Bool
Warn about "typed-holes"
maxMatchDepth :: Int
maxAppDepth :: Int
maxArgsDepth :: Int
maxRWOrderingConstraints :: Maybe Int
rwTerminationCheck :: Bool

Instances

Instances details

Eq Config #
Instance details Defined in Language.Haskell.Liquid.UX.Config Methods (==) :: Config -> Config -> Bool # (/=) :: Config -> Config -> Bool #
Data Config #
Instance details Defined in Language.Haskell.Liquid.UX.Config Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Config -> c Config # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Config # toConstr :: Config -> Constr # dataTypeOf :: Config -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Config) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Config) # gmapT :: (forall b. Data b => b -> b) -> Config -> Config # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Config -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Config -> r # gmapQ :: (forall d. Data d => d -> u) -> Config -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Config -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Config -> m Config # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Config -> m Config # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Config -> m Config #
Show Config #
Instance details Defined in Language.Haskell.Liquid.UX.Config Methods showsPrec :: Int -> Config -> ShowS # show :: Config -> String # showList :: [Config] -> ShowS #
Generic Config #
Instance details Defined in Language.Haskell.Liquid.UX.Config Associated Types type Rep Config :: Type -> Type # Methods from :: Config -> Rep Config x # to :: Rep Config x -> Config #
HasConfig Config #
Instance details Defined in Language.Haskell.Liquid.UX.Config Methods getConfig :: Config -> Config #
type Rep Config #
Instance details Defined in Language.Haskell.Liquid.UX.Config type Rep Config = D1 ('MetaData "Config" "Language.Haskell.Liquid.UX.Config" "liquidhaskell-0.8.10.1-inplace" 'False) (C1 ('MetaCons "Config" 'PrefixI 'True) ((((((S1 ('MetaSel ('Just "loggingVerbosity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Verbosity) :: S1 ('MetaSel ('Just "files") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FilePath])) :: (S1 ('MetaSel ('Just "idirs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [FilePath]) :: S1 ('MetaSel ('Just "diffcheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :: ((S1 ('MetaSel ('Just "linear") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "stringTheory") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :: (S1 ('MetaSel ('Just "higherorder") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "higherorderqs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))) :: (((S1 ('MetaSel ('Just "smtTimeout") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Int)) :: S1 ('MetaSel ('Just "fullcheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :: (S1 ('MetaSel ('Just "saveQuery") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "checks") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String]))) :: ((S1 ('MetaSel ('Just "noCheckUnknown") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "notermination") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :: (S1 ('MetaSel ('Just "rankNTypes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: (S1 ('MetaSel ('Just "noclasscheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "nostructuralterm") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))))) :: ((((S1 ('MetaSel ('Just "gradual") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "bscope") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :: (S1 ('MetaSel ('Just "gdepth") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :: S1 ('MetaSel ('Just "ginteractive") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :: ((S1 ('MetaSel ('Just "totalHaskell") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "nowarnings") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :: (S1 ('MetaSel ('Just "noannotations") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: (S1 ('MetaSel ('Just "checkDerived") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "caseExpandDepth") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))))) :: (((S1 ('MetaSel ('Just "notruetypes") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "nototality") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :: (S1 ('MetaSel ('Just "pruneUnsorted") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "cores") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Int)))) :: ((S1 ('MetaSel ('Just "minPartSize") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :: S1 ('MetaSel ('Just "maxPartSize") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :: (S1 ('MetaSel ('Just "maxParams") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :: (S1 ('MetaSel ('Just "smtsolver") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe SMTSolver)) :: S1 ('MetaSel ('Just "shortNames") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))))))) :: (((((S1 ('MetaSel ('Just "shortErrors") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "cabalDir") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :: (S1 ('MetaSel ('Just "ghcOptions") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String]) :: S1 ('MetaSel ('Just "cFiles") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String]))) :: ((S1 ('MetaSel ('Just "eliminate") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Eliminate) :: S1 ('MetaSel ('Just "port") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :: (S1 ('MetaSel ('Just "exactDC") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "noADT") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))) :: (((S1 ('MetaSel ('Just "scrapeImports") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "scrapeInternals") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :: (S1 ('MetaSel ('Just "scrapeUsedImports") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "elimStats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :: ((S1 ('MetaSel ('Just "elimBound") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Int)) :: S1 ('MetaSel ('Just "json") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :: (S1 ('MetaSel ('Just "counterExamples") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: (S1 ('MetaSel ('Just "timeBinds") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "noPatternInline") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))))) :: ((((S1 ('MetaSel ('Just "untidyCore") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "noSimplifyCore") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :: (S1 ('MetaSel ('Just "noslice") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "noLiftedImport") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :: ((S1 ('MetaSel ('Just "proofLogicEval") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "oldPLE") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :: (S1 ('MetaSel ('Just "proofLogicEvalLocal") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: (S1 ('MetaSel ('Just "extensionality") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "nopolyinfer") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))))) :: (((S1 ('MetaSel ('Just "reflection") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "compileSpec") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :: (S1 ('MetaSel ('Just "noCheckImports") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "typedHoles") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :: ((S1 ('MetaSel ('Just "maxMatchDepth") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :: S1 ('MetaSel ('Just "maxAppDepth") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :: (S1 ('MetaSel ('Just "maxArgsDepth") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :: (S1 ('MetaSel ('Just "maxRWOrderingConstraints") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Int)) :*: S1 ('MetaSel ('Just "rwTerminationCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))))))))

class HasConfig t where #

Methods

getConfig :: t -> Config #

Instances

Instances details

HasConfig Config #
Instance details Defined in Language.Haskell.Liquid.UX.Config Methods getConfig :: Config -> Config #
HasConfig GhcSpec #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods getConfig :: GhcSpec -> Config #
HasConfig TargetSpec #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods getConfig :: TargetSpec -> Config #
HasConfig TargetInfo #
Instance details Defined in Language.Haskell.Liquid.Types.Specs Methods getConfig :: TargetInfo -> Config #
HasConfig Env #
Instance details Defined in Language.Haskell.Liquid.Bare.Types Methods getConfig :: Env -> Config #
HasConfig CGEnv #
Instance details Defined in Language.Haskell.Liquid.Constraint.Types Methods getConfig :: CGEnv -> Config #

allowPLE :: Config -> Bool #

allowLocalPLE :: Config -> Bool #

allowGlobalPLE :: Config -> Bool #

patternFlag :: HasConfig t => t -> Bool #

higherOrderFlag :: HasConfig t => t -> Bool #

pruneFlag :: HasConfig t => t -> Bool #

maxCaseExpand :: HasConfig t => t -> Int #

exactDCFlag :: HasConfig t => t -> Bool #

hasOpt :: HasConfig t => t -> (Config -> Bool) -> Bool #

totalityCheck :: HasConfig t => t -> Bool #

terminationCheck :: HasConfig t => t -> Bool #

structuralTerm :: HasConfig a => a -> Bool #