{-# Language DeriveDataTypeable #-} -- for GHC <= 7.8
-- |
-- Module      : Test.Speculate.CondReason
-- Copyright   : (c) 2016-2019 Rudy Matela
-- License     : 3-Clause BSD  (see the file LICENSE)
-- Maintainer  : Rudy Matela <rudy@matela.com.br>
--
-- This module is part o Speculate.
--
-- Arguments to the 'speculate' function and parsing of command line arguments.
module Test.Speculate.Args
  ( Args (..)
  , args

  , constant
  , showConstant
  , foreground
  , background

  , getArgs
  , computeMaxSemiSize
  , computeMaxCondSize
  , computeInstances
  , types
  , atoms
  , keepExpr
  , timeout
  , shouldShowEquation
  , shouldShowConditionalEquation
  , reallyShowConditions

  , foregroundConstants
  , backgroundConstants

  , about

  , allAbout

  -- TODO: remove the following exports eventually:
  , prepareArgs
  , module System.Console.CmdArgs.Explicit
  )
where

import Test.Speculate.Expr
import Test.Speculate.Utils
import System.Console.CmdArgs.Explicit

import Test.LeanCheck ((\/))
import qualified Data.List as L (insert)
import Data.List hiding (insert)
import Data.Maybe (catMaybes)
import Data.Monoid ((<>))

import Data.Maybe

-- | Arguments to Speculate
data Args = Args
  { Args -> Int
maxSize     :: Int         -- ^ maximum size of considered expressions
  , Args -> Int
maxTests    :: Int         -- ^ maximum number of test for each law
  , Args -> [Expr]
constants   :: [Expr]      -- ^ constants considered when generating expressions
  , Args -> [[Expr]]
instances   :: [Instances] -- ^ typeclass instance information for @Eq@, @Ord@ and @Listable@
  , Args -> Int
maxSemiSize :: Int         -- ^ maximum size of inqualities RHS/LHS
  , Args -> Int
maxCondSize :: Int         -- ^ maximum size of considered condition
  , Args -> Int
maxVars     :: Int         -- ^ maximum number of variables allowed in inequalities and conditional equations

  , Args -> Bool
showConstants     :: Bool  -- ^ repeat constants on output
  , Args -> Bool
showEquations     :: Bool  -- ^ whether to show equations
  , Args -> Bool
showSemiequations :: Bool  -- ^ whether to show inequalties
  , Args -> Bool
showConditions    :: Bool  -- ^ whether to show conditional equations
  , Args -> Bool
showConstantLaws  :: Bool  -- ^ whether to show laws with no variables
  , Args -> Bool
autoConstants     :: Bool  -- ^ automatically include constants taken from tiers of values

  , Args -> Int -> Int
minTests    :: Int -> Int  -- ^ __(intermediary)__ minimum number of tests
                               --   for passing postconditions in function of
                               --   maximum number of tests
  , Args -> Maybe Int
maxConstants :: Maybe Int  -- ^ __(intermediary)__ maximum nubmer of constants allowed when considering expressions
  , Args -> Maybe Int
maxDepth     :: Maybe Int  -- ^ __(intermediary)__ maximum depth of considered expressions
  , Args -> Bool
showCounts   :: Bool       -- ^ __(intermediary)__ show counts of equations, inequalities and conditional equations
  , Args -> Bool
showTheory   :: Bool       -- ^ __(debug)__ whether to show raw theory
  , Args -> Bool
showArgs     :: Bool       -- ^ __(debug)__ show _this_ args before running
  , Args -> Bool
showHelp     :: Bool       -- ^ __(advanced)__ whether to show the command line help
  , Args -> Maybe Double
evalTimeout :: Maybe Double -- ^ __(advanced)__ timeout when evaluating ground expressions
  , Args -> Bool
force        :: Bool       -- ^ __(advanced)__ ignore errors
  , Args -> [String]
extra        :: [String]   -- ^ __(advanced)__ unused, user-defined meaning
  , Args -> [String]
exclude      :: [String]   -- ^ __(advanced)__ exclude this symbols from signature before running
  , Args -> [String]
onlyTypes    :: [String]   -- ^ __(advanced)__ only allow those types at top-level equations / semi-equations
  , Args -> [Int]
showClassesFor :: [Int]    -- ^ __(advanced)__ show equivalence classes of expressions
  , Args -> Bool
showDot      :: Bool       -- ^ __(advanced)__ whether to show a Graphviz dotfile with an Ord lattice
  , Args -> Bool
quietDot     :: Bool       -- ^ __(advanced)__ whether to show a Graphviz dotfiel with an Ord lattice (less verbose)
  }
  deriving Typeable -- for GHC <= 7.8
-- TODO: future options:
--, closureLimit      :: Int
--, order             :: OptOrder  -- data OptOrder = Dershowitz | KnuthBendix
--, maxRuleSize       :: Maybe Int
--, maxEquationSize   :: Maybe Int
--, keepRewriteRules  :: Bool
-- Maybe add an empty Thy here.

-- | Default arguments to Speculate
args :: Args
args :: Args
args = Args :: Int
-> Int
-> [Expr]
-> [[Expr]]
-> Int
-> Int
-> Int
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> (Int -> Int)
-> Maybe Int
-> Maybe Int
-> Bool
-> Bool
-> Bool
-> Bool
-> Maybe Double
-> Bool
-> [String]
-> [String]
-> [String]
-> [Int]
-> Bool
-> Bool
-> Args
Args
  { maxSize :: Int
maxSize              = Int
5
  , maxTests :: Int
maxTests             = Int
500
  , minTests :: Int -> Int
minTests             = \Int
n -> Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
20 -- defaults to 5% of maxTests
  , maxSemiSize :: Int
maxSemiSize          = -Int
1
  , maxCondSize :: Int
maxCondSize          = -Int
1
  , maxDepth :: Maybe Int
maxDepth             = Maybe Int
forall a. Maybe a
Nothing
  , instances :: [[Expr]]
instances            = []
  , showConstants :: Bool
showConstants        = Bool
True
  , autoConstants :: Bool
autoConstants        = Bool
False
  , showArgs :: Bool
showArgs             = Bool
True
  , showTheory :: Bool
showTheory           = Bool
False
  , showEquations :: Bool
showEquations        = Bool
True
  , showSemiequations :: Bool
showSemiequations    = Bool
True
  , showConditions :: Bool
showConditions       = Bool
True
  , showConstantLaws :: Bool
showConstantLaws     = Bool
False
  , showCounts :: Bool
showCounts           = Bool
False
  , showDot :: Bool
showDot              = Bool
False
  , quietDot :: Bool
quietDot             = Bool
False
  , showClassesFor :: [Int]
showClassesFor       = []
  , maxVars :: Int
maxVars              = Int
2
  , maxConstants :: Maybe Int
maxConstants         = Maybe Int
forall a. Maybe a
Nothing
  , evalTimeout :: Maybe Double
evalTimeout          = Maybe Double
forall a. Maybe a
Nothing
--, closureLimit         = 2
--, order                = Dershowitz
--, maxRuleSize          = Nothing
--, maxEquationSize      = Nothing
--, keepRewriteRules     = False
  , showHelp :: Bool
showHelp             = Bool
False
  , force :: Bool
force                = Bool
False
  , extra :: [String]
extra                = []
  , constants :: [Expr]
constants            = []
  , exclude :: [String]
exclude              = []
  , onlyTypes :: [String]
onlyTypes            = []
  }


computeMaxSemiSize :: Args -> Int
computeMaxSemiSize :: Args -> Int
computeMaxSemiSize Args
args
  | Args -> Int
maxSemiSize Args
args Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 = Args -> Int
maxSemiSize Args
args
  | Bool
otherwise            = Args -> Int
maxSize Args
args Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Args -> Int
maxSemiSize Args
args

computeMaxCondSize :: Args -> Int
computeMaxCondSize :: Args -> Int
computeMaxCondSize Args
args
  | Args -> Int
maxCondSize Args
args Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 = Args -> Int
maxCondSize Args
args
  | Bool
otherwise            = Args -> Int
maxSize Args
args Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Args -> Int
maxCondSize Args
args

computeInstances :: Args -> Instances
computeInstances :: Args -> [Expr]
computeInstances Args
args = [[Expr]] -> [Expr]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Args -> [[Expr]]
instances Args
args) [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr]
preludeInstances

shouldShow2 :: Args -> (Expr,Expr) -> Bool
shouldShow2 :: Args -> (Expr, Expr) -> Bool
shouldShow2 Args
args (Expr
e1,Expr
e2) = Args -> Bool
showConstantLaws Args
args Bool -> Bool -> Bool
|| Expr -> Bool
hasVar Expr
e1 Bool -> Bool -> Bool
|| Expr -> Bool
hasVar Expr
e2
-- `allAbout` constants // (conditionAtoms `union` equationAtoms)

shouldShowEquation :: Args -> (Expr,Expr) -> Bool
shouldShowEquation :: Args -> (Expr, Expr) -> Bool
shouldShowEquation Args
args (Expr
e1,Expr
e2) =
  Args -> (Expr, Expr) -> Bool
shouldShow2 Args
args (Expr
e1,Expr
e2) Bool -> Bool -> Bool
&& (Expr
e1 Expr -> [Expr] -> Bool
`about` [Expr]
fore Bool -> Bool -> Bool
|| Expr
e2 Expr -> [Expr] -> Bool
`about` [Expr]
fore)
  where
  fore :: [Expr]
fore = Args -> [Expr]
foregroundConstants Args
args

shouldShow3 :: Args -> (Expr,Expr,Expr) -> Bool
shouldShow3 :: Args -> (Expr, Expr, Expr) -> Bool
shouldShow3 Args
args (Expr
e1,Expr
e2,Expr
e3) = Args -> Bool
showConstantLaws Args
args
                           Bool -> Bool -> Bool
|| Expr -> Bool
hasVar Expr
e1 Bool -> Bool -> Bool
|| Expr -> Bool
hasVar Expr
e2 Bool -> Bool -> Bool
|| Expr -> Bool
hasVar Expr
e3

shouldShowConditionalEquation :: Args -> (Expr,Expr,Expr) -> Bool
shouldShowConditionalEquation :: Args -> (Expr, Expr, Expr) -> Bool
shouldShowConditionalEquation Args
args (Expr
ce,Expr
e1,Expr
e2) = Args -> (Expr, Expr, Expr) -> Bool
shouldShow3 Args
args (Expr
ce,Expr
e1,Expr
e2)
                                             Bool -> Bool -> Bool
&& Expr -> Expr -> Expr -> Bool
cem Expr
ce Expr
e1 Expr
e2
                                             Bool -> Bool -> Bool
&& (Expr
ce Expr -> [Expr] -> Bool
`about` [Expr]
fore
                                              Bool -> Bool -> Bool
|| Expr
e1 Expr -> [Expr] -> Bool
`about` [Expr]
fore
                                              Bool -> Bool -> Bool
|| Expr
e2 Expr -> [Expr] -> Bool
`about` [Expr]
fore)
  where
  cem :: Expr -> Expr -> Expr -> Bool
cem = [Expr] -> Int -> Int -> Expr -> Expr -> Expr -> Bool
condEqualM (Args -> [Expr]
computeInstances Args
args) (Args -> Int
maxTests Args
args) (Args -> Int -> Int
minTests Args
args (Args -> Int
maxTests Args
args))
  fore :: [Expr]
fore = Args -> [Expr]
foregroundConstants Args
args

keepExpr :: Args -> Expr -> Bool
keepExpr :: Args -> Expr -> Bool
keepExpr Args{maxConstants :: Args -> Maybe Int
maxConstants = Just Int
n} Expr
e | [Expr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Expr -> [Expr]
nubConsts Expr
e) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
n = Bool
False
keepExpr Args{maxDepth :: Args -> Maybe Int
maxDepth     = Just Int
n} Expr
e |             Expr -> Int
depth Expr
e  Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
n = Bool
False
keepExpr Args
_                           Expr
_                            = Bool
True

reallyShowConditions :: Args -> Bool
reallyShowConditions :: Args -> Bool
reallyShowConditions Args
args = Args -> Bool
showConditions Args
args
                         Bool -> Bool -> Bool
&& TypeRep
boolTy TypeRep -> [TypeRep] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (Expr -> TypeRep) -> [Expr] -> [TypeRep]
forall a b. (a -> b) -> [a] -> [b]
map (TypeRep -> TypeRep
finalResultTy (TypeRep -> TypeRep) -> (Expr -> TypeRep) -> Expr -> TypeRep
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> TypeRep
typ) (Args -> [Expr]
allConstants Args
args)

atoms :: Args -> [[Expr]]
atoms :: Args -> [[Expr]]
atoms Args
args = [ [Expr] -> [Expr]
forall a. Ord a => [a] -> [a]
nubSort ((TypeRep -> Maybe Expr) -> [TypeRep] -> [Expr]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ([Expr] -> TypeRep -> Maybe Expr
maybeHoleOfTy [Expr]
is) [TypeRep]
ts)
       [Expr] -> [Expr] -> [Expr]
forall a. Eq a => [a] -> [a] -> [a]
`union` Args -> [Expr]
allConstants Args
args
       [Expr] -> [Expr] -> [Expr]
forall a. Eq a => [a] -> [a] -> [a]
`union` [Bool -> Expr
forall a. (Typeable a, Show a) => a -> Expr
val Bool
True  | Bool
showConds Bool -> Bool -> Bool
|| Args -> Bool
showDot Args
args]
       [Expr] -> [Expr] -> [Expr]
forall a. Eq a => [a] -> [a] -> [a]
`union` [Bool -> Expr
forall a. (Typeable a, Show a) => a -> Expr
val Bool
False | Bool
showConds Bool -> Bool -> Bool
|| Args -> Bool
showDot Args
args]
       [Expr] -> [Expr] -> [Expr]
forall a. Eq a => [a] -> [a] -> [a]
`union` ([Expr] -> [Expr]
forall a. Ord a => [a] -> [a]
nubSort ([Expr] -> [Expr])
-> ([Maybe Expr] -> [Expr]) -> [Maybe Expr] -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Maybe Expr] -> [Expr]
forall a. [Maybe a] -> [a]
catMaybes) [String -> TypeRep -> [Expr] -> Maybe Expr
lookupComparison String
"==" TypeRep
t [Expr]
is | Bool
showConds, TypeRep
t <- [TypeRep]
ts] ]
         [[Expr]] -> [[Expr]] -> [[Expr]]
forall a. Eq a => [[a]] -> [[a]] -> [[a]]
\-/ ([[Expr]] -> [[Expr]] -> [[Expr]])
-> [[Expr]] -> [[[Expr]]] -> [[Expr]]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr [[Expr]] -> [[Expr]] -> [[Expr]]
forall a. [[a]] -> [[a]] -> [[a]]
(\/) [] [[Expr] -> TypeRep -> [[Expr]]
lookupTiersT [Expr]
is TypeRep
t | Args -> Bool
autoConstants Args
args, TypeRep
t <- [TypeRep]
ts, [Expr] -> TypeRep -> Bool
isListableT [Expr]
is TypeRep
t]
  where
  ts :: [TypeRep]
ts = Args -> [TypeRep]
types Args
args
  is :: [Expr]
is = Args -> [Expr]
computeInstances Args
args
  showConds :: Bool
showConds = Args -> Bool
reallyShowConditions Args
args
  []  \-/ :: [[a]] -> [[a]] -> [[a]]
\-/ []   =  []
  [[a]]
xss \-/ []   =  [[a]]
xss
  []  \-/ [[a]]
yss  =  [[a]]
yss
  ([a]
xs:[[a]]
xss) \-/ ([a]
ys:[[a]]
yss)  =  [a]
xs [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
`union` [a]
ys  [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
:  [[a]]
xss [[a]] -> [[a]] -> [[a]]
\-/ [[a]]
yss

-- misnomer: these are not all types, but just the star kinded ones...
types :: Args -> [TypeRep]
types :: Args -> [TypeRep]
types = [TypeRep] -> [TypeRep]
typesInList ([TypeRep] -> [TypeRep])
-> (Args -> [TypeRep]) -> Args -> [TypeRep]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> TypeRep) -> [Expr] -> [TypeRep]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> TypeRep
typ ([Expr] -> [TypeRep]) -> (Args -> [Expr]) -> Args -> [TypeRep]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Args -> [Expr]
allConstants

foregroundConstants, backgroundConstants :: Args -> [Expr]
foregroundConstants :: Args -> [Expr]
foregroundConstants = ([Expr], [Expr]) -> [Expr]
forall a b. (a, b) -> a
fst (([Expr], [Expr]) -> [Expr])
-> (Args -> ([Expr], [Expr])) -> Args -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr -> [Expr] -> ([Expr], [Expr])
forall a. Eq a => a -> a -> [a] -> ([a], [a])
partitionByMarkers Expr
foreground Expr
background ([Expr] -> ([Expr], [Expr]))
-> (Args -> [Expr]) -> Args -> ([Expr], [Expr])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Args -> [Expr]
constants
backgroundConstants :: Args -> [Expr]
backgroundConstants = ([Expr], [Expr]) -> [Expr]
forall a b. (a, b) -> b
snd (([Expr], [Expr]) -> [Expr])
-> (Args -> ([Expr], [Expr])) -> Args -> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr -> [Expr] -> ([Expr], [Expr])
forall a. Eq a => a -> a -> [a] -> ([a], [a])
partitionByMarkers Expr
foreground Expr
background ([Expr] -> ([Expr], [Expr]))
-> (Args -> [Expr]) -> Args -> ([Expr], [Expr])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Args -> [Expr]
constants

allConstants :: Args -> [Expr]
allConstants :: Args -> [Expr]
allConstants Args
args = (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
discard (\Expr
c -> (String -> Bool) -> [String] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Expr
c Expr -> String -> Bool
`isConstantNamed`) (Args -> [String]
exclude Args
args))
                  ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
discard (\Expr
e -> Expr
e Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
foreground Bool -> Bool -> Bool
|| Expr
e Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
background)
                  ([Expr] -> [Expr]) -> [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ Args -> [Expr]
constants Args
args

-- | Are all constants in an expression about a list of constants?
-- Examples in pseudo-Haskell:
--
-- > x + y `allAbout` [(+)] == True
-- > x + y == z `allAbout` [(+)] == False
-- > x + y == z `allAbout` [(+),(==)] == True
allAbout :: Expr -> [Expr] -> Bool
Expr
e allAbout :: Expr -> [Expr] -> Bool
`allAbout` [Expr]
es = Expr -> [Expr]
nubConsts Expr
e [Expr] -> (Expr -> Bool) -> Bool
forall a. [a] -> (a -> Bool) -> Bool
`areAll` (Expr -> [Expr] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Expr]
es)

about :: Expr -> [Expr] -> Bool
Expr
e about :: Expr -> [Expr] -> Bool
`about` [Expr]
es = Expr -> [Expr]
nubConsts Expr
e [Expr] -> (Expr -> Bool) -> Bool
forall a. [a] -> (a -> Bool) -> Bool
`areAny` (Expr -> [Expr] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Expr]
es)

timeout :: Args -> Bool -> Bool
timeout :: Args -> Bool -> Bool
timeout Args{evalTimeout :: Args -> Maybe Double
evalTimeout = Maybe Double
Nothing} = Bool -> Bool
forall a. a -> a
id
timeout Args{evalTimeout :: Args -> Maybe Double
evalTimeout = Just Double
t}  = Double -> Bool -> Bool
forall s. RealFrac s => s -> Bool -> Bool
timeoutToFalse Double
t

constant :: Typeable a => String -> a -> Expr
constant :: String -> a -> Expr
constant = String -> a -> Expr
forall a. Typeable a => String -> a -> Expr
value

showConstant :: (Typeable a, Show a) => a -> Expr
showConstant :: a -> Expr
showConstant = a -> Expr
forall a. (Typeable a, Show a) => a -> Expr
val

-- | A special 'Expr' value.
--   When provided on the 'constants' list, 
--   makes all the following constants 'foreground' constants.
foreground :: Expr
foreground :: Expr
foreground = String -> Args -> Expr
forall a. Typeable a => String -> a -> Expr
constant String
"foreground" (Args
forall a. HasCallStack => a
undefined :: Args)

-- | A special 'Expr' value.
--   When provided on the 'constants' list,
--   makes all the following constants 'background' constants.
--   Background constants can appear in laws about other constants, but not by
--   themselves.
background :: Expr
background :: Expr
background = String -> Args -> Expr
forall a. Typeable a => String -> a -> Expr
constant String
"background" (Args
forall a. HasCallStack => a
undefined :: Args)
-- NOTE: Hack!  TODO: add reason why

-- for cmdArgs
prepareArgs :: Args -> Mode Args
prepareArgs :: Args -> Mode Args
prepareArgs Args
args =
  String -> Args -> String -> Arg Args -> [Flag Args] -> Mode Args
forall a. String -> a -> String -> Arg a -> [Flag a] -> Mode a
mode String
"speculate" Args
args String
"" (Update Args -> String -> Arg Args
forall a. Update a -> String -> Arg a
flagArg (\String
s Args
a -> Args -> Either String Args
forall a b. b -> Either a b
Right Args
a {extra :: [String]
extra = String
sString -> [String] -> [String]
forall a. a -> [a] -> [a]
:Args -> [String]
extra Args
a}) String
"")
  [ String
"ssize"              String -> (String -> Args -> Args) -> Flag Args
forall a. String -> (String -> a -> a) -> Flag a
--= \String
s Args
a -> Args
a {maxSize :: Int
maxSize  = String -> Int
forall a. Read a => String -> a
read String
s}
  , String
"ttests"             String -> (String -> Args -> Args) -> Flag Args
forall a. String -> (String -> a -> a) -> Flag a
--= \String
s Args
a -> Args
a {maxTests :: Int
maxTests = String -> Int
forall a. Read a => String -> a
read String
s}
  , String
"mmin-tests"         String -> (String -> Args -> Args) -> Flag Args
forall a. String -> (String -> a -> a) -> Flag a
--= \String
s Args
a -> Args
a {minTests :: Int -> Int
minTests = String -> Int -> Int
parseMinTests String
s}
  , String
"zsemisize"          String -> (String -> Args -> Args) -> Flag Args
forall a. String -> (String -> a -> a) -> Flag a
--= \String
s Args
a -> Args
a {maxSemiSize :: Int
maxSemiSize = String -> Int
forall a. Read a => String -> a
read String
s}
  , String
"xcondsize"          String -> (String -> Args -> Args) -> Flag Args
forall a. String -> (String -> a -> a) -> Flag a
--= \String
s Args
a -> Args
a {maxCondSize :: Int
maxCondSize = String -> Int
forall a. Read a => String -> a
read String
s}
  , String
"Aconstants"         String -> (Args -> Args) -> Flag Args
forall a. String -> (a -> a) -> Flag a
--.   \Args
a -> Args
a {showConstants :: Bool
showConstants = Bool
False} -- TODO: fix name
  , String
"Uauto-constants"    String -> (Args -> Args) -> Flag Args
forall a. String -> (a -> a) -> Flag a
--.   \Args
a -> Args
a {autoConstants :: Bool
autoConstants = Bool
True}
  , String
"Ohide-args"         String -> (Args -> Args) -> Flag Args
forall a. String -> (a -> a) -> Flag a
--.   \Args
a -> Args
a {showArgs :: Bool
showArgs = Bool
False}
  , String
"Ttheory"            String -> (Args -> Args) -> Flag Args
forall a. String -> (a -> a) -> Flag a
--.   \Args
a -> Args
a {showTheory :: Bool
showTheory = Bool
True}
  , String
"Eno-equations"      String -> (Args -> Args) -> Flag Args
forall a. String -> (a -> a) -> Flag a
--.   \Args
a -> Args
a {showEquations :: Bool
showEquations = Bool
False}
  , String
"Sno-semiequations"  String -> (Args -> Args) -> Flag Args
forall a. String -> (a -> a) -> Flag a
--.   \Args
a -> Args
a {showSemiequations :: Bool
showSemiequations = Bool
False}
  , String
"Cno-sideconditions" String -> (Args -> Args) -> Flag Args
forall a. String -> (a -> a) -> Flag a
--.   \Args
a -> Args
a {showConditions :: Bool
showConditions = Bool
False}
  , String
"0no-constant-laws"  String -> (Args -> Args) -> Flag Args
forall a. String -> (a -> a) -> Flag a
--.   \Args
a -> Args
a {showConstantLaws :: Bool
showConstantLaws = Bool
True}
  , String
"rclass-reps-for"    String -> (String -> Args -> Args) -> Flag Args
forall a. String -> (String -> a -> a) -> Flag a
--= \String
s Args
a -> Args
a {showClassesFor :: [Int]
showClassesFor = String -> Int
forall a. Read a => String -> a
read String
s Int -> [Int] -> [Int]
forall a. Ord a => a -> [a] -> [a]
`L.insert` Args -> [Int]
showClassesFor Args
a}
  , String
"vvars"              String -> (String -> Args -> Args) -> Flag Args
forall a. String -> (String -> a -> a) -> Flag a
--= \String
s Args
a -> Args
a {maxVars :: Int
maxVars = String -> Int
forall a. Read a => String -> a
read String
s}
  , String
"cmax-constants"     String -> (String -> Args -> Args) -> Flag Args
forall a. String -> (String -> a -> a) -> Flag a
--= \String
s Args
a -> Args
a {maxConstants :: Maybe Int
maxConstants = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ String -> Int
forall a. Read a => String -> a
read String
s}
  , String
"eeval-timeout"      String -> (String -> Args -> Args) -> Flag Args
forall a. String -> (String -> a -> a) -> Flag a
--= \String
s Args
a -> Args
a {evalTimeout :: Maybe Double
evalTimeout = Double -> Maybe Double
forall a. a -> Maybe a
Just (Double -> Maybe Double) -> Double -> Maybe Double
forall a b. (a -> b) -> a -> b
$ String -> Double
forall a. Read a => String -> a
read String
s}
  , String
"ddepth"             String -> (String -> Args -> Args) -> Flag Args
forall a. String -> (String -> a -> a) -> Flag a
--= \String
s Args
a -> Args
a {maxDepth :: Maybe Int
maxDepth = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ String -> Int
forall a. Read a => String -> a
read String
s}
  , String
" counts"            String -> (Args -> Args) -> Flag Args
forall a. String -> (a -> a) -> Flag a
--.   \Args
a -> Args
a {showCounts :: Bool
showCounts = Bool
True}
  , String
"gsemi-digraph"      String -> (Args -> Args) -> Flag Args
forall a. String -> (a -> a) -> Flag a
--.   \Args
a -> Args
a {showDot :: Bool
showDot = Bool
True
                                       ,quietDot :: Bool
quietDot = Bool
False
                                       ,showConstants :: Bool
showConstants = Bool
False
                                       ,showEquations :: Bool
showEquations = Bool
False
                                       ,showSemiequations :: Bool
showSemiequations = Bool
False
                                       ,showConditions :: Bool
showConditions = Bool
False
                                       ,showArgs :: Bool
showArgs = Bool
False}
  , String
"Dquiet-dot"         String -> (Args -> Args) -> Flag Args
forall a. String -> (a -> a) -> Flag a
--.   \Args
a -> Args
a {showDot :: Bool
showDot = Bool
True
                                       ,quietDot :: Bool
quietDot = Bool
True
                                       ,showConstants :: Bool
showConstants = Bool
False
                                       ,showEquations :: Bool
showEquations = Bool
False
                                       ,showSemiequations :: Bool
showSemiequations = Bool
False
                                       ,showConditions :: Bool
showConditions = Bool
False
                                       ,showArgs :: Bool
showArgs = Bool
False}
  , String
" only-types"        String -> (String -> Args -> Args) -> Flag Args
forall a. String -> (String -> a -> a) -> Flag a
--= \String
s Args
a -> Args
a {onlyTypes :: [String]
onlyTypes = Args -> [String]
onlyTypes Args
a [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ String -> [String]
splitAtCommas String
s}
  , String
"fforce"             String -> (Args -> Args) -> Flag Args
forall a. String -> (a -> a) -> Flag a
--.   \Args
a -> Args
a {force :: Bool
force = Bool
True}
  , String
"hhelp"              String -> (Args -> Args) -> Flag Args
forall a. String -> (a -> a) -> Flag a
--.   \Args
a -> Args
a {showHelp :: Bool
showHelp = Bool
True}
  , String
" exclude"           String -> (String -> Args -> Args) -> Flag Args
forall a. String -> (String -> a -> a) -> Flag a
--= \String
s Args
a -> Args
a {exclude :: [String]
exclude = Args -> [String]
exclude Args
a [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ String -> [String]
splitAtCommas String
s}
  , String
"aall-foreground"    String -> (Args -> Args) -> Flag Args
forall a. String -> (a -> a) -> Flag a
--.   \Args
a -> Args
a {constants :: [Expr]
constants = (Expr -> Bool) -> [Expr] -> [Expr]
forall a. (a -> Bool) -> [a] -> [a]
discard (Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
background) (Args -> [Expr]
constants Args
a)}
  ]
  where
  (Char
short:String
long) --= :: String -> (String -> a -> a) -> Flag a
--= String -> a -> a
fun = [String] -> Update a -> String -> String -> Flag a
forall a. [String] -> Update a -> String -> String -> Flag a
flagReq  ((String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
" ") [[Char
short],String
long]) ((a -> Either String a
forall a b. b -> Either a b
Right (a -> Either String a) -> (a -> a) -> a -> Either String a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((a -> a) -> a -> Either String a)
-> (String -> a -> a) -> Update a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> a -> a
fun) String
"X" String
""
  String
_            --= String -> a -> a
_   = String -> Flag a
forall a. HasCallStack => String -> a
error String
"(--=): first argument can't be \"\""
  (Char
short:String
long) --. :: String -> (a -> a) -> Flag a
--. a -> a
fun = [String] -> (a -> a) -> String -> Flag a
forall a. [String] -> (a -> a) -> String -> Flag a
flagNone ((String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
" ") [[Char
short],String
long]) a -> a
fun                   String
""
  String
_            --. a -> a
_   = String -> Flag a
forall a. HasCallStack => String -> a
error String
"(--.): first argument can't be \"\""
  parseMinTests :: String -> Int -> Int
  parseMinTests :: String -> Int -> Int
parseMinTests String
s | String -> Char
forall a. [a] -> a
last String
s Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'%' = \Int
x -> String -> Int
forall a. Read a => String -> a
read (String -> String
forall a. [a] -> [a]
init String
s) Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
x Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
100
                  | Bool
otherwise     = Int -> Int -> Int
forall a b. a -> b -> a
const (String -> Int
forall a. Read a => String -> a
read String
s)

getArgs :: Args -> IO Args
getArgs :: Args -> IO Args
getArgs = Mode Args -> IO Args
forall a. Mode a -> IO a
processArgs (Mode Args -> IO Args) -> (Args -> Mode Args) -> Args -> IO Args
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Args -> Mode Args
prepareArgs