Newer
Older
waldmann
committed
import Data.Bool
import qualified Data.Text as T
import GHC.Generics
import Matchbox.Pretty (Pretty)
import Matchbox.Reader (Reader, as_read)
import qualified Matchbox.Pairs as P
import qualified Matchbox.Weight as W
import Matchbox.Control.AST.Name
import Data.String (fromString)
import qualified Data.Text as T
import Matchbox.Control.AST.Data (AST)
-- picked from the command line.
-- #536 : bar can be any expression
data Env = Env [(Name, AST)]
, strategy_library :: Maybe FilePath
, output_prefix :: Maybe FilePath
-- | Nothing: no pairing, Just Nothing: unbounded pairing,
-- Just (Just d): pairing iterated at most d times
, pairing_depth :: Maybe (Maybe Int)
waldmann
committed
, weights :: W.Modus
, kachinuki_syllable_mode :: K.Syllable_Modus
waldmann
committed
, bits :: Integer
, dim_top :: Integer
, dim_syl :: Integer
, stats :: Bool
, raw_args :: [T.Text] -- ^ used only in parsing
deriving Generic
instance Pretty Config
, strategy_library = Nothing
, output_prefix = Nothing
, kachinuki_syllable_mode = K.Weight
, rewrite_mode = Standard
, timeout = Nothing
<$> ( flag' Terminate (long "terminate" <> help "prove termination (output proof)" )
<|> flag' Transform (long "transform" <> help "transform system (output resulting set of rules)" )
<|> pure Terminate
)
<*> ( flag' Compact (long "compact" <> help "use compact syntax for strategy given with -S (prelude always uses detailed syntax)")
<|> pure Detailed
)
<*> ( (Just . From_File) <$> strOption (long "strategy-file" <> short 'S' <> help "read stragegy from file (and ignore all options from command line)")
<|> (Just . From_Text . T.pack) <$> strOption (long "strategy" <> short 'C' <> help "stragegy expression (and ignore all options from command line)")
<|> pure Nothing
)
<*> ( Just <$> strOption (long "prelude" <> short 'P' <> help "read strategy definitions from this file first" )
<|> pure Nothing )
<*> ( Just <$> strOption (long "output-prefix" <> short 'O' <> help "filename prefix for outputs (automata drawings)" ) <|> pure Nothing )
<*> switch ( long "yes" <> short 'y' <> help "prove termination" )
<*> switch ( long "noh" <> short 'n' <> help "prove nontermination" )
<*> switch ( long "dp" <> short 'd' <> help "apply dependency pairs transformation" )
<*> ( (Just . Just) <$> option auto ( long "pairs" <> short 'a' <> metavar "NAT"
<> help "bound for pairing depth" )
<|> flag' (Just Nothing) ( long "iterated-pairs" <> short 'i'
<> help "unbounded pairing depth" )
<*> option auto
(long "pairing-mode" <> short 'b' <> metavar "MODUS"
<> help (show [minBound .. maxBound :: P.Pairing_Method] ) )
<*> switch ( long "kachinuki" <> short 'k' <> help "use kachinuki ordering" )
<*> option auto
(long "kachinuki-mode" <> short 'K' <> metavar "MODUS"
<> value K.SAT
<> help (show [minBound .. maxBound :: K.Modus] ) )
<*> option auto (long "kachinuki-cutoff" <> metavar "Nat" <> value 1000 )
<*> option auto (short 'S' <> long "kachinuki-search" <> metavar "MODUS" <> value K.BFS
<> help (show [minBound .. maxBound :: K.Search] ) )
<*> option auto (short 'Y' <> long "kachinuki-syllable-mode"
<*> option auto (short 'B' <> long "bits" <> metavar "Nat" <> value 3
<*> option auto (short 'T' <> long "dim-top" <> metavar "Nat" <> value 3
<> help "matrix dimension for top symbols in Kachinuki" )
<*> option auto (short 'D' <> long "dim-syl" <> metavar "Nat" <> value 3
<> help "matrix dimension for syllable symbols in Kachinuki" )
<*> ( flag' True (long "natural" <> help "use matrices over naturals" )
<|> flag' False (long "no-natural" <> help "don't use matrices over naturals" )
<|> pure True
)
<*> ( flag' True (long "arctic" <> help "matrices over arctic numbers" )
<|> flag' False (long "no-arctic" <> help "don't use matrices over arctic numbers" )
<|> pure False
)
<*> flag Standard Cycles ( long "cycles" <> short 'c' <> help "for cycle rewriting")
<*> option ( Just <$> auto )
( long "timeout" <> short 't'
<> metavar "SECONDS" <> value Nothing <> help "timeout" )
<*> option ( auto )
( long "processes" <> metavar "NAT" <> value 1
<> help "max no. of processes in one Kachinuki search" )
<*> switch ( long "cpf" <> short 'p' <> help "print CPF certificate (after YES/NO first line)")
<*> switch ( long "verbose" <> short 'v' <> help "print full proof (no abbreviations)")
<*> switch ( long "trace" <> short 'r' <> help "trace proof search on stderr")
<*> ( flag' False (long "omit-proof" <> help "don't print full proof (just summary and skeleton)" )
<|> flag' True (long "print-proof" <> help "print full proof")
<*> ( flag' False (long "omit-stats" <> help "don't print statistics" )
<|> flag' True (long "print-stats" <> help "print statistics")
<|> pure False
)
<*> ( flag' False (long "omit-lanes" <> help "don't print swimlanes" )
<|> flag' True (long "print-lanes" <> help "print swimlanes")
<|> pure False
)
<*> ( Just <$> strOption (long "store-stats" ) <|> pure Nothing )
<*> switch ( long "read-hints" <> help "read hints froms DBs that are named in Advice records" )
<*> switch ( long "store-hints" <> help "write hints to DBs that are named in Advice records" )
<*> pure (Env [])
<*> many (argument str (help "file containing SRS, - for stdin, or SRS on command line" ))
-- | compute `input` and `env` from `raw_args`:
-- move all `foo=bar` pairs to `env`, for the remains:
-- if no argument remains: `input = Path "-"`
-- if exactly one argument `fp` remains: `input = Path fp`
-- if an even number of arguments remains: `input = Rules ..."
-- if any other number (odd, greater than 1) of arguments remains: error
process_raw_args :: Config -> Config
process_raw_args = extract_input . extract_env
-- | move `foo=bar` from `raw_args` to `env`
extract_env :: Config -> Config
extract_env c =
let assign w =
let (pre, post) = T.span (/= '=') w
in if T.null post
then Left w
else Right (Name pre, as_read $ T.tail post)
ass = map assign $ raw_args c
in c { raw_args = lefts ass
, env = Env $ rights ass
}
-- | move `fp` or rules from `raw_args` to `input`
extract_input c =
let pairs [] = []
pairs (l:r:later) = (l,r) : pairs later
in case raw_args c of
[ fp ] ->
main continue = execParser (process_raw_args <$> opts)
>>= continue
opts = info (helper <*> config)
( fullDesc <> progDesc "prove (non)termination" <> header "pure-matchbox" )