Skip to content
Snippets Groups Projects
Config.hs 9.54 KiB
Newer Older
{-# language DeriveGeneric #-}
{-# language OverloadedStrings #-}
Johannes Waldmann's avatar
Johannes Waldmann committed
module Matchbox.Config where

import Options.Applicative
waldmann's avatar
waldmann committed
import Data.Monoid ((<>))
Johannes Waldmann's avatar
Johannes Waldmann committed
import Data.Maybe (isJust)
Johannes Waldmann's avatar
Johannes Waldmann committed
import Data.Either (lefts, rights)
import qualified Data.Text as T
Johannes Waldmann's avatar
Johannes Waldmann committed
import Default
import GHC.Generics
import Matchbox.Pretty (Pretty)
import Matchbox.Reader (Reader, as_read)
waldmann's avatar
waldmann committed
import Matchbox.Walker (Walker)
Johannes Waldmann's avatar
Johannes Waldmann committed

waldmann's avatar
waldmann committed
import qualified Matchbox.Pairs as P
import qualified Matchbox.Weight as W
import qualified Kachinuki.Modus as K
Johannes Waldmann's avatar
Johannes Waldmann committed
import Matchbox.Config.Data
import Matchbox.Control.AST.Name
import Data.String (fromString)
import qualified Data.Text  as T
import Matchbox.Control.AST.Data (AST)

Johannes Waldmann's avatar
Johannes Waldmann committed
-- | will contain all pairs `foo=bar`
-- picked from the command line.
-- #536 : bar can be any expression
data Env = Env [(Name, AST)]
Johannes Waldmann's avatar
Johannes Waldmann committed
  deriving Generic
instance Pretty Env

Johannes Waldmann's avatar
Johannes Waldmann committed
data Config =
waldmann's avatar
waldmann committed
  Config { modus :: Modus
waldmann's avatar
waldmann committed
         , strategy_syntax :: Syntax
waldmann's avatar
waldmann committed
         , strategy_source :: Maybe From
         , strategy_library :: Maybe FilePath
         , output_prefix :: Maybe FilePath
         , prove_termination :: Bool
Johannes Waldmann's avatar
Johannes Waldmann committed
         , prove_nontermination :: Bool
waldmann's avatar
waldmann committed
         , dp_transform :: Bool
Johannes Waldmann's avatar
Johannes Waldmann committed
         -- | Nothing: no pairing, Just Nothing: unbounded pairing,
         -- Just (Just d): pairing iterated at most d times
         , pairing_depth :: Maybe (Maybe Int)
waldmann's avatar
waldmann committed
         , pairing_mode :: P.Pairing_Method
         , kachinuki :: Bool
         , kachinuki_mode :: K.Modus
         , kachinuki_cutoff :: Int
waldmann's avatar
waldmann committed
         , kachinuki_weight_search :: K.Search
         , kachinuki_syllable_mode :: K.Syllable_Modus
         , dim_top :: Integer
         , dim_syl :: Integer
waldmann's avatar
waldmann committed
         , natural :: Bool
         , arctic :: Bool
Johannes Waldmann's avatar
Johannes Waldmann committed
         , rewrite_mode :: Rewrite_Mode
         , timeout :: Maybe Int
Johannes Waldmann's avatar
Johannes Waldmann committed
         , processes :: Int
         , cpf :: Bool
waldmann's avatar
waldmann committed
         , verbose :: Bool
waldmann's avatar
waldmann committed
         , trace :: Bool
         , proof :: Bool -- ^ print proof?
         , lanes :: Bool
Johannes Waldmann's avatar
Johannes Waldmann committed
         , input :: Input
waldmann's avatar
waldmann committed
         , store_stats :: Maybe FilePath
Johannes Waldmann's avatar
Johannes Waldmann committed
         , read_hints :: Bool
         , store_hints :: Bool
Johannes Waldmann's avatar
Johannes Waldmann committed
         , env :: Env
         , raw_args :: [T.Text] -- ^ used only in parsing
Johannes Waldmann's avatar
Johannes Waldmann committed
         }
   deriving Generic

instance Pretty Config
Johannes Waldmann's avatar
Johannes Waldmann committed

Johannes Waldmann's avatar
Johannes Waldmann committed
use_pairing = isJust . pairing_depth

config0 = Config
waldmann's avatar
waldmann committed
   { modus = Terminate
waldmann's avatar
waldmann committed
   , strategy_syntax = Detailed
waldmann's avatar
waldmann committed
   , strategy_source = Nothing
   , strategy_library = Nothing
   , output_prefix = Nothing
   , prove_termination = True
   , prove_nontermination = False
waldmann's avatar
waldmann committed
   , dp_transform = False
Johannes Waldmann's avatar
Johannes Waldmann committed
   , pairing_depth = Nothing
waldmann's avatar
waldmann committed
   , pairing_mode = P.Approximated_RFC_Pairs
waldmann's avatar
waldmann committed
   , weights = default_
   , kachinuki = False
   , kachinuki_mode = K.SAT
   , kachinuki_cutoff = 1000
waldmann's avatar
waldmann committed
   , kachinuki_weight_search = K.BFS
   , kachinuki_syllable_mode = K.Weight
waldmann's avatar
waldmann committed
   , bits = 3
   , dim_top = 3
   , dim_syl = 3
waldmann's avatar
waldmann committed
   , natural = True
   , arctic = False
   , rewrite_mode = Standard
   , timeout = Nothing
Johannes Waldmann's avatar
Johannes Waldmann committed
   , processes = 2
   , cpf = False
waldmann's avatar
waldmann committed
   , verbose = False
waldmann's avatar
waldmann committed
   , trace = False
   , proof = False
Johannes Waldmann's avatar
Johannes Waldmann committed
   , stats = False
   , lanes = False
Johannes Waldmann's avatar
Johannes Waldmann committed
   , input = Path "-"
waldmann's avatar
waldmann committed
   , store_stats = Nothing
Johannes Waldmann's avatar
Johannes Waldmann committed
   , read_hints = False
   , store_hints = False
Johannes Waldmann's avatar
Johannes Waldmann committed
   , env = Env []
   , raw_args = []
Johannes Waldmann's avatar
Johannes Waldmann committed
config :: Parser Config
config = Config
waldmann's avatar
waldmann committed
   <$> ( flag' Terminate (long "terminate" <> help "prove termination (output proof)" )
       <|> flag' Transform (long "transform" <> help "transform system (output resulting set of rules)" )
       <|> pure Terminate
       )
waldmann's avatar
waldmann committed
   <*> ( flag' Compact (long "compact" <> help "use compact syntax for strategy given with -S (prelude always uses detailed syntax)")
         <|> pure Detailed
       )
waldmann's avatar
waldmann committed
   <*> ( (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" )
Johannes Waldmann's avatar
Johannes Waldmann committed
   <*> switch ( long "noh" <> short 'n' <> help "prove nontermination" )
waldmann's avatar
waldmann committed
   <*> switch ( long "dp" <> short 'd' <> help "apply dependency pairs transformation" )
Johannes Waldmann's avatar
Johannes Waldmann committed
   <*> ( (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" )
Johannes Waldmann's avatar
Johannes Waldmann committed
         <|> pure Nothing
Johannes Waldmann's avatar
Johannes Waldmann committed
       )
waldmann's avatar
waldmann committed
   <*> option auto
      (long "pairing-mode" <> short 'b' <> metavar "MODUS"
waldmann's avatar
waldmann committed
       <> value P.Approximated_RFC_Pairs
waldmann's avatar
waldmann committed
       <> help (show [minBound .. maxBound :: P.Pairing_Method] ) )
waldmann's avatar
waldmann committed
   <*> option auto
      (long "weights" <> short 'w' <> metavar "MODUS"
waldmann's avatar
waldmann committed
       <> value default_
       <> help (show [default_ :: W.Modus] ) )
   <*> 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 )
waldmann's avatar
waldmann committed
   <*> 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"
Johannes Waldmann's avatar
Johannes Waldmann committed
                    <> value default_
waldmann's avatar
waldmann committed
                    <> help (show K.values ) )
   <*> option auto (short 'B' <> long "bits" <> metavar "Nat" <> value 3
waldmann's avatar
waldmann committed
                   <> help "bit width for weights in Kachinuki" )
   <*> 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" )
waldmann's avatar
waldmann committed
   <*> ( 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")
Johannes Waldmann's avatar
Johannes Waldmann committed
   <*> option ( Just <$> auto )
        ( long "timeout" <> short 't'
                     <> metavar "SECONDS" <> value Nothing <> help "timeout" )
Johannes Waldmann's avatar
Johannes Waldmann committed
   <*> 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)")
waldmann's avatar
waldmann committed
   <*> switch ( long "verbose" <> short 'v' <> help "print full proof (no abbreviations)")
waldmann's avatar
waldmann committed
   <*> 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")
       <|> pure False
   <*> ( 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
       )
Johannes Waldmann's avatar
Johannes Waldmann committed
   <*> pure (Path "-")
   <*> ( Just <$> strOption (long "store-stats" ) <|> pure Nothing )
Johannes Waldmann's avatar
Johannes Waldmann committed
   <*> 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" )
Johannes Waldmann's avatar
Johannes Waldmann committed
   <*> 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
Johannes Waldmann's avatar
Johannes Waldmann committed
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)
Johannes Waldmann's avatar
Johannes Waldmann committed
      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 = 
Johannes Waldmann's avatar
Johannes Waldmann committed
  let pairs [] = []
      pairs (l:r:later) = (l,r) : pairs later
  in  case raw_args c of
    [ fp ] ->
Johannes Waldmann's avatar
Johannes Waldmann committed
      c { input = Path fp, raw_args = [] }
Johannes Waldmann's avatar
Johannes Waldmann committed
    ws | even (length ws) ->
Johannes Waldmann's avatar
Johannes Waldmann committed
         c { input = Rules $ pairs ws, raw_args = [] }
Johannes Waldmann's avatar
Johannes Waldmann committed

Johannes Waldmann's avatar
Johannes Waldmann committed

main :: (Config -> IO a ) -> IO a
Johannes Waldmann's avatar
Johannes Waldmann committed
main continue = execParser (process_raw_args <$> opts)
  >>= continue


opts = info (helper <*> config)
Johannes Waldmann's avatar
Johannes Waldmann committed
     ( fullDesc <> progDesc "prove (non)termination" <> header "pure-matchbox" )
get args = case execParserPure defaultPrefs opts args of
  Success a -> a
  Failure f -> error $ show f