Language.Haskell.Liquid.UX.Config

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

Documentation

data Config

Constructors

Config

Fields

• 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

• extensionality :: Bool

  allow function extentionality axioms

• alphaEquivalence :: Bool

  allow lambda alpha-equivalence axioms

• betaEquivalence :: Bool

  allow lambda beta-equivalence axioms

• normalForm :: Bool

  allow lambda normalization-equivalence axioms

• 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

• gradual :: Bool

  enable gradual type checking

• gdepth :: Int

  depth of gradual concretization

• ginteractive :: Bool

  interactive gradual solving

• totalHaskell :: Bool

  Check for termination and totality, Overrides no-termination flags

• autoproofs :: Bool

  automatically construct proofs from axioms

• nowarnings :: Bool

  disable warnings output (only show errors)

• noannotations :: Bool

  disable creation of intermediate annotation files

• trustInternals :: Bool

  type all internal variables with true

• nocaseexpand :: Bool

  disable case expand

• strata :: Bool

  enable strata analysis

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

• noMeasureFields :: Bool

  Do not automatically lift data constructor fields into measures

• 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

• nonLinCuts :: Bool

  treat non-linear kvars as cuts

• autoInstantiate :: Instantiate

  How to instantiate axioms NO-TRIGGER , proofMethod :: ProofMethod -- ^ How to create automatic instances NO-TRIGGER , fuel :: Int -- ^ Fuel for axiom instantiation

• debugInstantionation :: Bool

  Debug Instantiation

• noslice :: Bool

  Disable non-concrete KVar slicing

• noLiftedImport :: Bool

  Disable loading lifted specifications (for "legacy" libs)

• proofLogicEval :: Bool

  Enable proof-by-logical-evaluation

Instances

Eq Config

Methods

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

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

Data 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 :: (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

Methods

showsPrec :: Int -> Config -> ShowS

show :: Config -> String

showList :: [Config] -> ShowS

Generic Config

Associated Types

type Rep Config :: * -> *

Methods

from :: Config -> Rep Config x

to :: Rep Config x -> Config

Serialize Config

Methods

put :: Putter Config

get :: Get Config

HasConfig Config

Methods

getConfig :: Config -> Config

patternFlag :: Config -> Bool

higherOrderFlag :: Config -> Bool

pruneFlag :: Config -> Bool

expandFlag :: Config -> Bool

hasOpt :: Config -> (Config -> Bool) -> Bool

totalityCheck :: Config -> Bool

terminationCheck :: Config -> Bool

type Rep Config

type Rep Config

class HasConfig t where

Minimal complete definition

getConfig

Methods

getConfig :: t -> Config

patternFlag :: t -> Bool

higherOrderFlag :: t -> Bool

pruneFlag :: t -> Bool

expandFlag :: t -> Bool

hasOpt :: t -> (Config -> Bool) -> Bool

totalityCheck :: t -> Bool

terminationCheck :: t -> Bool

Instances

HasConfig Config

Methods

getConfig :: Config -> Config

patternFlag :: Config -> Bool

higherOrderFlag :: Config -> Bool

pruneFlag :: Config -> Bool

expandFlag :: Config -> Bool

hasOpt :: Config -> (Config -> Bool) -> Bool

totalityCheck :: Config -> Bool

terminationCheck :: Config -> Bool

HasConfig GhcSpec

Methods

getConfig :: GhcSpec -> Config

patternFlag :: GhcSpec -> Bool

higherOrderFlag :: GhcSpec -> Bool

pruneFlag :: GhcSpec -> Bool

expandFlag :: GhcSpec -> Bool

hasOpt :: GhcSpec -> (Config -> Bool) -> Bool

totalityCheck :: GhcSpec -> Bool

terminationCheck :: GhcSpec -> Bool

HasConfig GhcInfo

Methods

getConfig :: GhcInfo -> Config

patternFlag :: GhcInfo -> Bool

higherOrderFlag :: GhcInfo -> Bool

pruneFlag :: GhcInfo -> Bool

expandFlag :: GhcInfo -> Bool

hasOpt :: GhcInfo -> (Config -> Bool) -> Bool

totalityCheck :: GhcInfo -> Bool

terminationCheck :: GhcInfo -> Bool

HasConfig BareEnv

Methods

getConfig :: BareEnv -> Config

patternFlag :: BareEnv -> Bool

higherOrderFlag :: BareEnv -> Bool

pruneFlag :: BareEnv -> Bool

expandFlag :: BareEnv -> Bool

hasOpt :: BareEnv -> (Config -> Bool) -> Bool

totalityCheck :: BareEnv -> Bool

terminationCheck :: BareEnv -> Bool

HasConfig CGEnv

Methods

getConfig :: CGEnv -> Config

patternFlag :: CGEnv -> Bool

higherOrderFlag :: CGEnv -> Bool

pruneFlag :: CGEnv -> Bool

expandFlag :: CGEnv -> Bool

hasOpt :: CGEnv -> (Config -> Bool) -> Bool

totalityCheck :: CGEnv -> Bool

terminationCheck :: CGEnv -> Bool

allowPLE :: Config -> Bool

allowLocalPLE :: Config -> Bool

allowGlobalPLE :: Config -> Bool

Orphan instances

Serialize SMTSolver

Methods

put :: Putter SMTSolver

get :: Get SMTSolver