Language.Haskell.Liquid.UX.Config

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

• 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

• 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

• 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

• 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]

Instances

Data Config

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

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

Show Config

Defined in Language.Haskell.Liquid.UX.Config

Methods

showsPrec :: Int -> Config -> ShowS

show :: Config -> String

showList :: [Config] -> ShowS

Eq Config

Defined in Language.Haskell.Liquid.UX.Config

Methods

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

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

HasConfig Config

Defined in Language.Haskell.Liquid.UX.Config

Methods

getConfig :: Config -> Config

type Rep Config

Defined in Language.Haskell.Liquid.UX.Config

type Rep Config = D1 ('MetaData "Config" "Language.Haskell.Liquid.UX.Config" "liquidhaskell-boot-0.9.2.5.0-JuBNLAGIRFD6ItsPyAO3oF" '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 "nopositivity") '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 "expectErrorContaining") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String])))) :*: ((S1 ('MetaSel ('Just "expectAnyError") '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 "pleWithUndecidedGuards") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "oldPLE") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :*: (S1 ('MetaSel ('Just "interpreter") '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 "typeclass") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))))) :*: (((S1 ('MetaSel ('Just "auxInline") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "rwTerminationCheck") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :*: (S1 ('MetaSel ('Just "skipModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "noLazyPLE") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "fuel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Int))))) :*: ((S1 ('MetaSel ('Just "environmentReduction") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "noEnvironmentReduction") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :*: (S1 ('MetaSel ('Just "inlineANFBindings") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "pandocHtml") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "excludeAutomaticAssumptionsFor") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String])))))))))

class HasConfig t where

Methods

getConfig :: t -> Config

Instances

HasConfig Env

Defined in Language.Haskell.Liquid.Bare.Types

Methods

getConfig :: Env -> Config

HasConfig CGEnv

Defined in Language.Haskell.Liquid.Constraint.Types

Methods

getConfig :: CGEnv -> Config

HasConfig GhcSpec

Defined in Language.Haskell.Liquid.Types.Specs

Methods

getConfig :: GhcSpec -> Config

HasConfig TargetInfo

Defined in Language.Haskell.Liquid.Types.Specs

Methods

getConfig :: TargetInfo -> Config

HasConfig TargetSpec

Defined in Language.Haskell.Liquid.Types.Specs

Methods

getConfig :: TargetSpec -> Config

HasConfig Config

Defined in Language.Haskell.Liquid.UX.Config

Methods

getConfig :: Config -> 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