module Language.Haskell.Liquid.UX.Config (
Config (..)
, HasConfig (..)
, hasOpt
, totalityCheck
, terminationCheck
, Instantiate (..)
, allowSMTInstationation
, allowLiquidInstationation
, allowLiquidInstationationGlobal
, allowLiquidInstationationLocal
, ProofMethod (..)
, allowRewrite
, allowArithmetic
) where
import Prelude hiding (error)
import Data.Serialize ( Serialize )
import Language.Fixpoint.Types.Config hiding (Config)
import GHC.Generics
import System.Console.CmdArgs
totalityCheck :: Config -> Bool
totalityCheck config
= totality config || totalHaskell config
terminationCheck :: Config -> Bool
terminationCheck config
= totalHaskell config || not (notermination config)
data Config = Config {
files :: [FilePath]
, idirs :: [FilePath]
, diffcheck :: Bool
, linear :: Bool
, stringTheory :: Bool
, higherorder :: Bool
, higherorderqs :: Bool
, extensionality :: Bool
, alphaEquivalence :: Bool
, betaEquivalence :: Bool
, normalForm :: Bool
, fullcheck :: Bool
, saveQuery :: Bool
, checks :: [String]
, noCheckUnknown :: Bool
, notermination :: Bool
, gradual :: Bool
, totalHaskell :: Bool
, autoproofs :: Bool
, nowarnings :: Bool
, noannotations :: Bool
, trustInternals :: Bool
, nocaseexpand :: Bool
, strata :: Bool
, notruetypes :: Bool
, totality :: 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
, noMeasureFields :: Bool
, scrapeImports :: Bool
, scrapeInternals :: Bool
, scrapeUsedImports :: Bool
, elimStats :: Bool
, elimBound :: Maybe Int
, json :: Bool
, counterExamples :: Bool
, timeBinds :: Bool
, noPatternInline :: Bool
, untidyCore :: Bool
, noSimplifyCore :: Bool
, nonLinCuts :: Bool
, autoInstantiate :: Instantiate
, proofMethod :: ProofMethod
, fuel :: Int
, debugInstantionation :: Bool
, noslice :: Bool
} deriving (Generic, Data, Typeable, Show, Eq)
instance Serialize ProofMethod
instance Serialize Instantiate
instance Serialize SMTSolver
instance Serialize Config
data Instantiate = NoInstances | SMTInstances | LiquidInstances | LiquidInstancesLocal
deriving (Eq, Data, Typeable, Generic)
data ProofMethod = Arithmetic | Rewrite | AllMethods
deriving (Eq, Data, Typeable, Generic)
allowSMTInstationation, allowLiquidInstationation, allowLiquidInstationationLocal, allowLiquidInstationationGlobal :: Config -> Bool
allowSMTInstationation cfg = autoInstantiate cfg == SMTInstances
allowLiquidInstationation cfg = autoInstantiate cfg == LiquidInstances
|| autoInstantiate cfg == LiquidInstancesLocal
allowLiquidInstationationGlobal cfg = autoInstantiate cfg == LiquidInstances
allowLiquidInstationationLocal cfg = autoInstantiate cfg == LiquidInstancesLocal
allowRewrite, allowArithmetic :: Config -> Bool
allowRewrite cfg = proofMethod cfg == Rewrite || proofMethod cfg == AllMethods
allowArithmetic cfg = proofMethod cfg == Arithmetic || proofMethod cfg == AllMethods
instance Default ProofMethod where
def = Rewrite
instance Show ProofMethod where
show Arithmetic = "arithmetic"
show Rewrite = "rewrite"
show AllMethods = "all"
instance Default Instantiate where
def = NoInstances
instance Show Instantiate where
show NoInstances = "none"
show SMTInstances = "SMT"
show LiquidInstancesLocal = "liquid-local"
show LiquidInstances = "liquid-global"
class HasConfig t where
getConfig :: t -> Config
patternFlag :: t -> Bool
patternFlag = const False
higherOrderFlag :: t -> Bool
higherOrderFlag = higherorder . getConfig
hasOpt :: HasConfig t => t -> (Config -> Bool) -> Bool
hasOpt t f = f (getConfig t)
instance HasConfig Config where
getConfig = id