Safe Haskell	None
Language	Haskell98

Language.Haskell.Liquid.UX.Config

Description

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

Synopsis

data Config = Config {
- loggingVerbosity :: Verbosity
- files :: [FilePath]
- idirs :: [FilePath]
- diffcheck :: Bool
- linear :: Bool
- stringTheory :: Bool
- higherorder :: Bool
- higherorderqs :: Bool
- smtTimeout :: Maybe Int
- fullcheck :: Bool
- saveQuery :: Bool
- checks :: [String]
- noCheckUnknown :: Bool
- notermination :: Bool
- nopositivity :: Bool
- rankNTypes :: Bool
- noclasscheck :: Bool
- nostructuralterm :: Bool
- gradual :: Bool
- bscope :: Bool
- gdepth :: Int
- ginteractive :: Bool
- totalHaskell :: Bool
- nowarnings :: Bool
- noannotations :: Bool
- checkDerived :: Bool
- caseExpandDepth :: Int
- 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
- expectErrorContaining :: [String]
- expectAnyError :: Bool
- scrapeInternals :: Bool
- elimStats :: Bool
- elimBound :: Maybe Int
- json :: Bool
- counterExamples :: Bool
- timeBinds :: Bool
- noPatternInline :: Bool
- untidyCore :: Bool
- noSimplifyCore :: Bool
- noslice :: Bool
- noLiftedImport :: Bool
- proofLogicEval :: Bool
- pleWithUndecidedGuards :: Bool
- oldPLE :: Bool
- interpreter :: Bool
- proofLogicEvalLocal :: Bool
- etabeta :: Bool
- dependantCase :: Bool
- extensionality :: Bool
- nopolyinfer :: Bool
- reflection :: Bool
- compileSpec :: Bool
- noCheckImports :: Bool
- typeclass :: Bool
- auxInline :: Bool
- rwTerminationCheck :: Bool
- skipModule :: Bool
- noLazyPLE :: Bool
- fuel :: Maybe Int
- environmentReduction :: Bool
- noEnvironmentReduction :: Bool
- inlineANFBindings :: Bool
- pandocHtml :: Bool
- excludeAutomaticAssumptionsFor :: [String]
- dumpOpaqueReflections :: Bool
- dumpPreNormalizedCore :: Bool
- allowUnsafeConstructors :: Bool
}
class HasConfig t where
- getConfig :: t -> Config
data Verbosity
- = Quiet
- | Minimal
- | Normal
- | Loud
allowPLE :: Config -> Bool
allowLocalPLE :: Config -> Bool
allowGlobalPLE :: Config -> Bool
cmdargsVerbosity :: Verbosity -> Verbosity
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

Documentation

data Config Source #

Constructors

Config

Fields

loggingVerbosity :: Verbosity
the logging verbosity to use (defaults to Minimal)
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
nopositivity :: Bool
disable positivity 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)
expectErrorContaining :: [String]
expect failure from Liquid with at least one of the following messages
expectAnyError :: Bool
expect failure from Liquid with any message
scrapeInternals :: Bool
scrape qualifiers from auto 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
pleWithUndecidedGuards :: Bool
Unfold invocations with undecided guards in PLE
oldPLE :: Bool
Enable proof-by-logical-evaluation
interpreter :: Bool
Use an interpreter to assist PLE
proofLogicEvalLocal :: Bool
Enable proof-by-logical-evaluation locally, per function
etabeta :: Bool
Eta expand and beta reduce terms to aid PLE
dependantCase :: Bool
Enable PLE for dependent cases
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
typeclass :: Bool
enable typeclass support.
auxInline :: Bool
rwTerminationCheck :: Bool
Enable termination checking for rewriting
skipModule :: Bool
Skip this module entirely (don't even compile any specs in it)
noLazyPLE :: Bool
fuel :: Maybe Int
Maximum PLE "fuel" (unfold depth) (default=infinite)
environmentReduction :: Bool
Perform environment reduction
noEnvironmentReduction :: Bool
Don't perform environment reduction
inlineANFBindings :: Bool
Inline ANF bindings. Sometimes improves performance and sometimes worsens it.
pandocHtml :: Bool
Use pandoc to generate html
excludeAutomaticAssumptionsFor :: [String]
dumpOpaqueReflections :: Bool
dumpPreNormalizedCore :: Bool
allowUnsafeConstructors :: Bool
Allow refining constructors with unsafe refinements

Instances

Instances details

Data Config Source #

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 #

Generic Config Source #

Instance details

Defined in Language.Haskell.Liquid.UX.Config

Associated Types

type Rep Config

Instance details

Defined in Language.Haskell.Liquid.UX.Config

Methods

from :: Config -> Rep Config x #

to :: Rep Config x -> Config #

Show Config Source #

Instance details

Defined in Language.Haskell.Liquid.UX.Config

Methods

showsPrec :: Int -> Config -> ShowS #

show :: Config -> String #

showList :: [Config] -> ShowS #

Eq Config Source #

Instance details

Defined in Language.Haskell.Liquid.UX.Config

Methods

(==) :: Config -> Config -> Bool #

(/=) :: Config -> Config -> Bool #

HasConfig Config Source #

Instance details

Defined in Language.Haskell.Liquid.UX.Config

Methods

getConfig :: Config -> Config Source #

type Rep Config Source #

Instance details

Defined in Language.Haskell.Liquid.UX.Config

class HasConfig t where Source #

Methods

getConfig :: t -> Config Source #

Instances

Instances details

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

data Verbosity Source #

Constructors

Quiet
Minimal
Normal
Loud

Instances

Instances details

Data Verbosity Source #

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) -> Verbosity -> c Verbosity #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Verbosity #

toConstr :: Verbosity -> Constr #

dataTypeOf :: Verbosity -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Verbosity) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Verbosity) #

gmapT :: (forall b. Data b => b -> b) -> Verbosity -> Verbosity #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Verbosity -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Verbosity -> r #

gmapQ :: (forall d. Data d => d -> u) -> Verbosity -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Verbosity -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Verbosity -> m Verbosity #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Verbosity -> m Verbosity #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Verbosity -> m Verbosity #

Generic Verbosity Source #

Instance details

Defined in Language.Haskell.Liquid.UX.Config

Associated Types

type Rep Verbosity

Instance details

Defined in Language.Haskell.Liquid.UX.Config

type Rep Verbosity = D1 ('MetaData "Verbosity" "Language.Haskell.Liquid.UX.Config" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) ((C1 ('MetaCons "Quiet" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Minimal" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Normal" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Loud" 'PrefixI 'False) (U1 :: Type -> Type)))

Methods

from :: Verbosity -> Rep Verbosity x #

to :: Rep Verbosity x -> Verbosity #

Show Verbosity Source #

Instance details

Defined in Language.Haskell.Liquid.UX.Config

Methods

showsPrec :: Int -> Verbosity -> ShowS #

show :: Verbosity -> String #

showList :: [Verbosity] -> ShowS #

Eq Verbosity Source #

Instance details

Defined in Language.Haskell.Liquid.UX.Config

Methods

(==) :: Verbosity -> Verbosity -> Bool #

(/=) :: Verbosity -> Verbosity -> Bool #

Ord Verbosity Source #

Instance details

Defined in Language.Haskell.Liquid.UX.Config

Methods

compare :: Verbosity -> Verbosity -> Ordering #

(<) :: Verbosity -> Verbosity -> Bool #

(<=) :: Verbosity -> Verbosity -> Bool #

(>) :: Verbosity -> Verbosity -> Bool #

(>=) :: Verbosity -> Verbosity -> Bool #

max :: Verbosity -> Verbosity -> Verbosity #

min :: Verbosity -> Verbosity -> Verbosity #

type Rep Verbosity Source #

Instance details

Defined in Language.Haskell.Liquid.UX.Config

type Rep Verbosity = D1 ('MetaData "Verbosity" "Language.Haskell.Liquid.UX.Config" "liquidhaskell-boot-0.9.10.1.2-inplace" 'False) ((C1 ('MetaCons "Quiet" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Minimal" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Normal" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Loud" 'PrefixI 'False) (U1 :: Type -> Type)))

allowPLE :: Config -> Bool Source #

allowLocalPLE :: Config -> Bool Source #

allowGlobalPLE :: Config -> Bool Source #

cmdargsVerbosity :: Verbosity -> Verbosity Source #

liquid-fixpoint uses CmdArg.Verbosity at least to show the progress bar.

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

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

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

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

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

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

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

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

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

Key	Shortcut
s	Open this search box
esc	Close this search box
↓,ctrl + j	Move down in search results
↑,ctrl + k	Move up in search results
↵	Go to active search result