{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
-- SPDX-License-Identifier: MIT

module CLI (runCLI) where

import Ast (Program (Program))
import Control.Exception (Exception (displayException), SomeException, handle, throw, throwIO)
import Control.Exception.Base
import Control.Monad (when)
import Data.Char (toLower, toUpper)
import Data.List (intercalate)
import Data.Maybe (isJust, isNothing)
import Data.Version (showVersion)
import Dataize (DataizeContext (DataizeContext), dataize)
import Functions (buildTerm)
import qualified Functions
import LaTeX (explainRules, programToLaTeX)
import Logger
import Misc (ensuredFile)
import qualified Misc
import Must (Must (..))
import Options.Applicative
import Parser (parseProgramThrows)
import Paths_phino (version)
import Pretty (PrintMode (SALTY, SWEET), prettyBytes, prettyProgram', Encoding (UNICODE))
import Rewriter (RewriteContext (RewriteContext), rewrite')
import System.Exit (ExitCode (..), exitFailure)
import System.IO (getContents')
import Text.Printf (printf)
import XMIR (XmirContext (XmirContext), parseXMIRThrows, printXMIR, programToXMIR, xmirToPhi)
import Yaml (normalizationRules)
import qualified Yaml as Y

data CmdException
  = InvalidRewriteArguments {CmdException -> FilePath
message :: String}
  | CouldNotReadFromStdin {message :: String}
  | CouldNotDataize
  deriving (Show CmdException
Typeable CmdException
(Typeable CmdException, Show CmdException) =>
(CmdException -> SomeException)
-> (SomeException -> Maybe CmdException)
-> (CmdException -> FilePath)
-> Exception CmdException
SomeException -> Maybe CmdException
CmdException -> FilePath
CmdException -> SomeException
forall e.
(Typeable e, Show e) =>
(e -> SomeException)
-> (SomeException -> Maybe e) -> (e -> FilePath) -> Exception e
$ctoException :: CmdException -> SomeException
toException :: CmdException -> SomeException
$cfromException :: SomeException -> Maybe CmdException
fromException :: SomeException -> Maybe CmdException
$cdisplayException :: CmdException -> FilePath
displayException :: CmdException -> FilePath
Exception)

instance Show CmdException where
  show :: CmdException -> FilePath
show InvalidRewriteArguments {FilePath
message :: CmdException -> FilePath
message :: FilePath
..} = FilePath -> FilePath -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"Invalid set of arguments for 'rewrite' command: %s" FilePath
message
  show CouldNotReadFromStdin {FilePath
message :: CmdException -> FilePath
message :: FilePath
..} = FilePath -> FilePath -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"Could not read input from stdin\nReason: %s" FilePath
message
  show CmdException
CouldNotDataize = FilePath
"Could not dataize given program"

data Command
  = CmdRewrite OptsRewrite
  | CmdDataize OptsDataize
  | CmdExplain OptsExplain

data IOFormat = XMIR | PHI | LATEX
  deriving (IOFormat -> IOFormat -> Bool
(IOFormat -> IOFormat -> Bool)
-> (IOFormat -> IOFormat -> Bool) -> Eq IOFormat
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: IOFormat -> IOFormat -> Bool
== :: IOFormat -> IOFormat -> Bool
$c/= :: IOFormat -> IOFormat -> Bool
/= :: IOFormat -> IOFormat -> Bool
Eq)

instance Show IOFormat where
  show :: IOFormat -> FilePath
show IOFormat
XMIR = FilePath
"xmir"
  show IOFormat
PHI = FilePath
"phi"
  show IOFormat
LATEX = FilePath
"latex"

data OptsDataize = OptsDataize
  { OptsDataize -> LogLevel
logLevel :: LogLevel,
    OptsDataize -> IOFormat
inputFormat :: IOFormat,
    OptsDataize -> Integer
maxDepth :: Integer,
    OptsDataize -> Integer
maxCycles :: Integer,
    OptsDataize -> Bool
depthSensitive :: Bool,
    OptsDataize -> Maybe FilePath
inputFile :: Maybe FilePath
  }

data OptsExplain = OptsExplain
  { OptsExplain -> LogLevel
logLevel :: LogLevel,
    OptsExplain -> [FilePath]
rules :: [FilePath],
    OptsExplain -> Bool
normalize :: Bool,
    OptsExplain -> Bool
shuffle :: Bool,
    OptsExplain -> Maybe FilePath
targetFile :: Maybe FilePath
  }

data OptsRewrite = OptsRewrite
  { OptsRewrite -> LogLevel
logLevel :: LogLevel,
    OptsRewrite -> [FilePath]
rules :: [FilePath],
    OptsRewrite -> IOFormat
inputFormat :: IOFormat,
    OptsRewrite -> IOFormat
outputFormat :: IOFormat,
    OptsRewrite -> PrintMode
printMode :: PrintMode,
    OptsRewrite -> Bool
normalize :: Bool,
    OptsRewrite -> Bool
shuffle :: Bool,
    OptsRewrite -> Bool
omitListing :: Bool,
    OptsRewrite -> Bool
omitComments :: Bool,
    OptsRewrite -> Bool
depthSensitive :: Bool,
    OptsRewrite -> Must
must :: Must,
    OptsRewrite -> Integer
maxDepth :: Integer,
    OptsRewrite -> Integer
maxCycles :: Integer,
    OptsRewrite -> Bool
inPlace :: Bool,
    OptsRewrite -> Maybe FilePath
targetFile :: Maybe FilePath,
    OptsRewrite -> Maybe FilePath
inputFile :: Maybe FilePath
  }

parseIOFormat :: String -> ReadM IOFormat
parseIOFormat :: FilePath -> ReadM IOFormat
parseIOFormat FilePath
type' = (FilePath -> Either FilePath IOFormat) -> ReadM IOFormat
forall a. (FilePath -> Either FilePath a) -> ReadM a
eitherReader ((FilePath -> Either FilePath IOFormat) -> ReadM IOFormat)
-> (FilePath -> Either FilePath IOFormat) -> ReadM IOFormat
forall a b. (a -> b) -> a -> b
$ \FilePath
format -> case ((Char -> Char) -> FilePath -> FilePath
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower FilePath
format, FilePath
type') of
  (FilePath
"xmir", FilePath
_) -> IOFormat -> Either FilePath IOFormat
forall a b. b -> Either a b
Right IOFormat
XMIR
  (FilePath
"phi", FilePath
_) -> IOFormat -> Either FilePath IOFormat
forall a b. b -> Either a b
Right IOFormat
PHI
  (FilePath
"latex", FilePath
"output") -> IOFormat -> Either FilePath IOFormat
forall a b. b -> Either a b
Right IOFormat
LATEX
  (FilePath, FilePath)
_ -> FilePath -> Either FilePath IOFormat
forall a b. a -> Either a b
Left (FilePath -> FilePath -> FilePath -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"The value '%s' can't be used for '--%s' option, use --help to check possible values" FilePath
format FilePath
type')

argInputFile :: Parser (Maybe FilePath)
argInputFile :: Parser (Maybe FilePath)
argInputFile = Parser FilePath -> Parser (Maybe FilePath)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (ReadM FilePath -> Mod ArgumentFields FilePath -> Parser FilePath
forall a. ReadM a -> Mod ArgumentFields a -> Parser a
argument ReadM FilePath
forall s. IsString s => ReadM s
str (FilePath -> Mod ArgumentFields FilePath
forall (f :: * -> *) a. HasMetavar f => FilePath -> Mod f a
metavar FilePath
"FILE" Mod ArgumentFields FilePath
-> Mod ArgumentFields FilePath -> Mod ArgumentFields FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath -> Mod ArgumentFields FilePath
forall (f :: * -> *) a. FilePath -> Mod f a
help FilePath
"Path to input file"))

optMaxDepth :: Parser Integer
optMaxDepth :: Parser Integer
optMaxDepth = ReadM Integer -> Mod OptionFields Integer -> Parser Integer
forall a. ReadM a -> Mod OptionFields a -> Parser a
option ReadM Integer
forall a. Read a => ReadM a
auto (FilePath -> Mod OptionFields Integer
forall (f :: * -> *) a. HasName f => FilePath -> Mod f a
long FilePath
"max-depth" Mod OptionFields Integer
-> Mod OptionFields Integer -> Mod OptionFields Integer
forall a. Semigroup a => a -> a -> a
<> FilePath -> Mod OptionFields Integer
forall (f :: * -> *) a. HasMetavar f => FilePath -> Mod f a
metavar FilePath
"DEPTH" Mod OptionFields Integer
-> Mod OptionFields Integer -> Mod OptionFields Integer
forall a. Semigroup a => a -> a -> a
<> FilePath -> Mod OptionFields Integer
forall (f :: * -> *) a. FilePath -> Mod f a
help FilePath
"Maximum number of rewriting iterations per rule" Mod OptionFields Integer
-> Mod OptionFields Integer -> Mod OptionFields Integer
forall a. Semigroup a => a -> a -> a
<> Integer -> Mod OptionFields Integer
forall (f :: * -> *) a. HasValue f => a -> Mod f a
value Integer
25 Mod OptionFields Integer
-> Mod OptionFields Integer -> Mod OptionFields Integer
forall a. Semigroup a => a -> a -> a
<> Mod OptionFields Integer
forall a (f :: * -> *). Show a => Mod f a
showDefault)

optMaxCycles :: Parser Integer
optMaxCycles :: Parser Integer
optMaxCycles = ReadM Integer -> Mod OptionFields Integer -> Parser Integer
forall a. ReadM a -> Mod OptionFields a -> Parser a
option ReadM Integer
forall a. Read a => ReadM a
auto (FilePath -> Mod OptionFields Integer
forall (f :: * -> *) a. HasName f => FilePath -> Mod f a
long FilePath
"max-cycles" Mod OptionFields Integer
-> Mod OptionFields Integer -> Mod OptionFields Integer
forall a. Semigroup a => a -> a -> a
<> FilePath -> Mod OptionFields Integer
forall (f :: * -> *) a. HasMetavar f => FilePath -> Mod f a
metavar FilePath
"CYCLES" Mod OptionFields Integer
-> Mod OptionFields Integer -> Mod OptionFields Integer
forall a. Semigroup a => a -> a -> a
<> FilePath -> Mod OptionFields Integer
forall (f :: * -> *) a. FilePath -> Mod f a
help FilePath
"Maximum number of rewriting cycles across all rules" Mod OptionFields Integer
-> Mod OptionFields Integer -> Mod OptionFields Integer
forall a. Semigroup a => a -> a -> a
<> Integer -> Mod OptionFields Integer
forall (f :: * -> *) a. HasValue f => a -> Mod f a
value Integer
25 Mod OptionFields Integer
-> Mod OptionFields Integer -> Mod OptionFields Integer
forall a. Semigroup a => a -> a -> a
<> Mod OptionFields Integer
forall a (f :: * -> *). Show a => Mod f a
showDefault)

optInputFormat :: Parser IOFormat
optInputFormat :: Parser IOFormat
optInputFormat = ReadM IOFormat -> Mod OptionFields IOFormat -> Parser IOFormat
forall a. ReadM a -> Mod OptionFields a -> Parser a
option (FilePath -> ReadM IOFormat
parseIOFormat FilePath
"input") (FilePath -> Mod OptionFields IOFormat
forall (f :: * -> *) a. HasName f => FilePath -> Mod f a
long FilePath
"input" Mod OptionFields IOFormat
-> Mod OptionFields IOFormat -> Mod OptionFields IOFormat
forall a. Semigroup a => a -> a -> a
<> FilePath -> Mod OptionFields IOFormat
forall (f :: * -> *) a. HasMetavar f => FilePath -> Mod f a
metavar FilePath
"FORMAT" Mod OptionFields IOFormat
-> Mod OptionFields IOFormat -> Mod OptionFields IOFormat
forall a. Semigroup a => a -> a -> a
<> FilePath -> Mod OptionFields IOFormat
forall (f :: * -> *) a. FilePath -> Mod f a
help FilePath
"Program input format (phi, xmir, latex)" Mod OptionFields IOFormat
-> Mod OptionFields IOFormat -> Mod OptionFields IOFormat
forall a. Semigroup a => a -> a -> a
<> IOFormat -> Mod OptionFields IOFormat
forall (f :: * -> *) a. HasValue f => a -> Mod f a
value IOFormat
PHI Mod OptionFields IOFormat
-> Mod OptionFields IOFormat -> Mod OptionFields IOFormat
forall a. Semigroup a => a -> a -> a
<> Mod OptionFields IOFormat
forall a (f :: * -> *). Show a => Mod f a
showDefault)

optDepthSensitive :: Parser Bool
optDepthSensitive :: Parser Bool
optDepthSensitive = Mod FlagFields Bool -> Parser Bool
switch (FilePath -> Mod FlagFields Bool
forall (f :: * -> *) a. HasName f => FilePath -> Mod f a
long FilePath
"depth-sensitive" Mod FlagFields Bool -> Mod FlagFields Bool -> Mod FlagFields Bool
forall a. Semigroup a => a -> a -> a
<> FilePath -> Mod FlagFields Bool
forall (f :: * -> *) a. FilePath -> Mod f a
help FilePath
"Fail if rewriting is not finished after reaching max attempts (see --max-cycles or --max-depth)")

optLogLevel :: Parser LogLevel
optLogLevel :: Parser LogLevel
optLogLevel =
  ReadM LogLevel -> Mod OptionFields LogLevel -> Parser LogLevel
forall a. ReadM a -> Mod OptionFields a -> Parser a
option
    ReadM LogLevel
parseLogLevel
    ( FilePath -> Mod OptionFields LogLevel
forall (f :: * -> *) a. HasName f => FilePath -> Mod f a
long FilePath
"log-level"
        Mod OptionFields LogLevel
-> Mod OptionFields LogLevel -> Mod OptionFields LogLevel
forall a. Semigroup a => a -> a -> a
<> FilePath -> Mod OptionFields LogLevel
forall (f :: * -> *) a. HasMetavar f => FilePath -> Mod f a
metavar FilePath
"LEVEL"
        Mod OptionFields LogLevel
-> Mod OptionFields LogLevel -> Mod OptionFields LogLevel
forall a. Semigroup a => a -> a -> a
<> FilePath -> Mod OptionFields LogLevel
forall (f :: * -> *) a. FilePath -> Mod f a
help (FilePath
"Log level (" FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate FilePath
", " ((LogLevel -> FilePath) -> [LogLevel] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map LogLevel -> FilePath
forall a. Show a => a -> FilePath
show [LogLevel
DEBUG, LogLevel
INFO, LogLevel
WARNING, LogLevel
ERROR, LogLevel
NONE]) FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
")")
        Mod OptionFields LogLevel
-> Mod OptionFields LogLevel -> Mod OptionFields LogLevel
forall a. Semigroup a => a -> a -> a
<> LogLevel -> Mod OptionFields LogLevel
forall (f :: * -> *) a. HasValue f => a -> Mod f a
value LogLevel
INFO
        Mod OptionFields LogLevel
-> Mod OptionFields LogLevel -> Mod OptionFields LogLevel
forall a. Semigroup a => a -> a -> a
<> Mod OptionFields LogLevel
forall a (f :: * -> *). Show a => Mod f a
showDefault
    )
  where
    parseLogLevel :: ReadM LogLevel
    parseLogLevel :: ReadM LogLevel
parseLogLevel = (FilePath -> Either FilePath LogLevel) -> ReadM LogLevel
forall a. (FilePath -> Either FilePath a) -> ReadM a
eitherReader ((FilePath -> Either FilePath LogLevel) -> ReadM LogLevel)
-> (FilePath -> Either FilePath LogLevel) -> ReadM LogLevel
forall a b. (a -> b) -> a -> b
$ \FilePath
lvl -> case (Char -> Char) -> FilePath -> FilePath
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toUpper FilePath
lvl of
      FilePath
"DEBUG" -> LogLevel -> Either FilePath LogLevel
forall a b. b -> Either a b
Right LogLevel
DEBUG
      FilePath
"INFO" -> LogLevel -> Either FilePath LogLevel
forall a b. b -> Either a b
Right LogLevel
INFO
      FilePath
"WARNING" -> LogLevel -> Either FilePath LogLevel
forall a b. b -> Either a b
Right LogLevel
WARNING
      FilePath
"WARN" -> LogLevel -> Either FilePath LogLevel
forall a b. b -> Either a b
Right LogLevel
WARNING
      FilePath
"ERROR" -> LogLevel -> Either FilePath LogLevel
forall a b. b -> Either a b
Right LogLevel
ERROR
      FilePath
"ERR" -> LogLevel -> Either FilePath LogLevel
forall a b. b -> Either a b
Right LogLevel
ERROR
      FilePath
"NONE" -> LogLevel -> Either FilePath LogLevel
forall a b. b -> Either a b
Right LogLevel
NONE
      FilePath
_ -> FilePath -> Either FilePath LogLevel
forall a b. a -> Either a b
Left (FilePath -> Either FilePath LogLevel)
-> FilePath -> Either FilePath LogLevel
forall a b. (a -> b) -> a -> b
$ FilePath
"unknown log-level: " FilePath -> FilePath -> FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath
lvl

optRule :: Parser [FilePath]
optRule :: Parser [FilePath]
optRule = Parser FilePath -> Parser [FilePath]
forall a. Parser a -> Parser [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (Mod OptionFields FilePath -> Parser FilePath
forall s. IsString s => Mod OptionFields s -> Parser s
strOption (FilePath -> Mod OptionFields FilePath
forall (f :: * -> *) a. HasName f => FilePath -> Mod f a
long FilePath
"rule" Mod OptionFields FilePath
-> Mod OptionFields FilePath -> Mod OptionFields FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath -> Mod OptionFields FilePath
forall (f :: * -> *) a. HasMetavar f => FilePath -> Mod f a
metavar FilePath
"FILE" Mod OptionFields FilePath
-> Mod OptionFields FilePath -> Mod OptionFields FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath -> Mod OptionFields FilePath
forall (f :: * -> *) a. FilePath -> Mod f a
help FilePath
"Path to custom rule"))

optNormalize :: Parser Bool
optNormalize :: Parser Bool
optNormalize = Mod FlagFields Bool -> Parser Bool
switch (FilePath -> Mod FlagFields Bool
forall (f :: * -> *) a. HasName f => FilePath -> Mod f a
long FilePath
"normalize" Mod FlagFields Bool -> Mod FlagFields Bool -> Mod FlagFields Bool
forall a. Semigroup a => a -> a -> a
<> FilePath -> Mod FlagFields Bool
forall (f :: * -> *) a. FilePath -> Mod f a
help FilePath
"Use built-in normalization rules")

optTarget :: Parser (Maybe FilePath)
optTarget :: Parser (Maybe FilePath)
optTarget = Parser FilePath -> Parser (Maybe FilePath)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (Mod OptionFields FilePath -> Parser FilePath
forall s. IsString s => Mod OptionFields s -> Parser s
strOption (FilePath -> Mod OptionFields FilePath
forall (f :: * -> *) a. HasName f => FilePath -> Mod f a
long FilePath
"target" Mod OptionFields FilePath
-> Mod OptionFields FilePath -> Mod OptionFields FilePath
forall a. Semigroup a => a -> a -> a
<> Char -> Mod OptionFields FilePath
forall (f :: * -> *) a. HasName f => Char -> Mod f a
short Char
't' Mod OptionFields FilePath
-> Mod OptionFields FilePath -> Mod OptionFields FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath -> Mod OptionFields FilePath
forall (f :: * -> *) a. HasMetavar f => FilePath -> Mod f a
metavar FilePath
"FILE" Mod OptionFields FilePath
-> Mod OptionFields FilePath -> Mod OptionFields FilePath
forall a. Semigroup a => a -> a -> a
<> FilePath -> Mod OptionFields FilePath
forall (f :: * -> *) a. FilePath -> Mod f a
help FilePath
"File to save output to"))

optShuffle :: Parser Bool
optShuffle :: Parser Bool
optShuffle = Mod FlagFields Bool -> Parser Bool
switch (FilePath -> Mod FlagFields Bool
forall (f :: * -> *) a. HasName f => FilePath -> Mod f a
long FilePath
"shuffle" Mod FlagFields Bool -> Mod FlagFields Bool -> Mod FlagFields Bool
forall a. Semigroup a => a -> a -> a
<> FilePath -> Mod FlagFields Bool
forall (f :: * -> *) a. FilePath -> Mod f a
help FilePath
"Shuffle rules before applying")

explainParser :: Parser Command
explainParser :: Parser Command
explainParser =
  OptsExplain -> Command
CmdExplain
    (OptsExplain -> Command) -> Parser OptsExplain -> Parser Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ( LogLevel
-> [FilePath] -> Bool -> Bool -> Maybe FilePath -> OptsExplain
OptsExplain
            (LogLevel
 -> [FilePath] -> Bool -> Bool -> Maybe FilePath -> OptsExplain)
-> Parser LogLevel
-> Parser
     ([FilePath] -> Bool -> Bool -> Maybe FilePath -> OptsExplain)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser LogLevel
optLogLevel
            Parser
  ([FilePath] -> Bool -> Bool -> Maybe FilePath -> OptsExplain)
-> Parser [FilePath]
-> Parser (Bool -> Bool -> Maybe FilePath -> OptsExplain)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser [FilePath]
optRule
            Parser (Bool -> Bool -> Maybe FilePath -> OptsExplain)
-> Parser Bool -> Parser (Bool -> Maybe FilePath -> OptsExplain)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Bool
optNormalize
            Parser (Bool -> Maybe FilePath -> OptsExplain)
-> Parser Bool -> Parser (Maybe FilePath -> OptsExplain)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Bool
optShuffle
            Parser (Maybe FilePath -> OptsExplain)
-> Parser (Maybe FilePath) -> Parser OptsExplain
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser (Maybe FilePath)
optTarget
        )

dataizeParser :: Parser Command
dataizeParser :: Parser Command
dataizeParser =
  OptsDataize -> Command
CmdDataize
    (OptsDataize -> Command) -> Parser OptsDataize -> Parser Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ( LogLevel
-> IOFormat
-> Integer
-> Integer
-> Bool
-> Maybe FilePath
-> OptsDataize
OptsDataize
            (LogLevel
 -> IOFormat
 -> Integer
 -> Integer
 -> Bool
 -> Maybe FilePath
 -> OptsDataize)
-> Parser LogLevel
-> Parser
     (IOFormat
      -> Integer -> Integer -> Bool -> Maybe FilePath -> OptsDataize)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser LogLevel
optLogLevel
            Parser
  (IOFormat
   -> Integer -> Integer -> Bool -> Maybe FilePath -> OptsDataize)
-> Parser IOFormat
-> Parser
     (Integer -> Integer -> Bool -> Maybe FilePath -> OptsDataize)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser IOFormat
optInputFormat
            Parser
  (Integer -> Integer -> Bool -> Maybe FilePath -> OptsDataize)
-> Parser Integer
-> Parser (Integer -> Bool -> Maybe FilePath -> OptsDataize)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Integer
optMaxDepth
            Parser (Integer -> Bool -> Maybe FilePath -> OptsDataize)
-> Parser Integer -> Parser (Bool -> Maybe FilePath -> OptsDataize)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Integer
optMaxCycles
            Parser (Bool -> Maybe FilePath -> OptsDataize)
-> Parser Bool -> Parser (Maybe FilePath -> OptsDataize)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Bool
optDepthSensitive
            Parser (Maybe FilePath -> OptsDataize)
-> Parser (Maybe FilePath) -> Parser OptsDataize
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser (Maybe FilePath)
argInputFile
        )

rewriteParser :: Parser Command
rewriteParser :: Parser Command
rewriteParser =
  OptsRewrite -> Command
CmdRewrite
    (OptsRewrite -> Command) -> Parser OptsRewrite -> Parser Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ( LogLevel
-> [FilePath]
-> IOFormat
-> IOFormat
-> PrintMode
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Must
-> Integer
-> Integer
-> Bool
-> Maybe FilePath
-> Maybe FilePath
-> OptsRewrite
OptsRewrite
            (LogLevel
 -> [FilePath]
 -> IOFormat
 -> IOFormat
 -> PrintMode
 -> Bool
 -> Bool
 -> Bool
 -> Bool
 -> Bool
 -> Must
 -> Integer
 -> Integer
 -> Bool
 -> Maybe FilePath
 -> Maybe FilePath
 -> OptsRewrite)
-> Parser LogLevel
-> Parser
     ([FilePath]
      -> IOFormat
      -> IOFormat
      -> PrintMode
      -> Bool
      -> Bool
      -> Bool
      -> Bool
      -> Bool
      -> Must
      -> Integer
      -> Integer
      -> Bool
      -> Maybe FilePath
      -> Maybe FilePath
      -> OptsRewrite)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser LogLevel
optLogLevel
            Parser
  ([FilePath]
   -> IOFormat
   -> IOFormat
   -> PrintMode
   -> Bool
   -> Bool
   -> Bool
   -> Bool
   -> Bool
   -> Must
   -> Integer
   -> Integer
   -> Bool
   -> Maybe FilePath
   -> Maybe FilePath
   -> OptsRewrite)
-> Parser [FilePath]
-> Parser
     (IOFormat
      -> IOFormat
      -> PrintMode
      -> Bool
      -> Bool
      -> Bool
      -> Bool
      -> Bool
      -> Must
      -> Integer
      -> Integer
      -> Bool
      -> Maybe FilePath
      -> Maybe FilePath
      -> OptsRewrite)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser [FilePath]
optRule
            Parser
  (IOFormat
   -> IOFormat
   -> PrintMode
   -> Bool
   -> Bool
   -> Bool
   -> Bool
   -> Bool
   -> Must
   -> Integer
   -> Integer
   -> Bool
   -> Maybe FilePath
   -> Maybe FilePath
   -> OptsRewrite)
-> Parser IOFormat
-> Parser
     (IOFormat
      -> PrintMode
      -> Bool
      -> Bool
      -> Bool
      -> Bool
      -> Bool
      -> Must
      -> Integer
      -> Integer
      -> Bool
      -> Maybe FilePath
      -> Maybe FilePath
      -> OptsRewrite)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser IOFormat
optInputFormat
            Parser
  (IOFormat
   -> PrintMode
   -> Bool
   -> Bool
   -> Bool
   -> Bool
   -> Bool
   -> Must
   -> Integer
   -> Integer
   -> Bool
   -> Maybe FilePath
   -> Maybe FilePath
   -> OptsRewrite)
-> Parser IOFormat
-> Parser
     (PrintMode
      -> Bool
      -> Bool
      -> Bool
      -> Bool
      -> Bool
      -> Must
      -> Integer
      -> Integer
      -> Bool
      -> Maybe FilePath
      -> Maybe FilePath
      -> OptsRewrite)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReadM IOFormat -> Mod OptionFields IOFormat -> Parser IOFormat
forall a. ReadM a -> Mod OptionFields a -> Parser a
option (FilePath -> ReadM IOFormat
parseIOFormat FilePath
"output") (FilePath -> Mod OptionFields IOFormat
forall (f :: * -> *) a. HasName f => FilePath -> Mod f a
long FilePath
"output" Mod OptionFields IOFormat
-> Mod OptionFields IOFormat -> Mod OptionFields IOFormat
forall a. Semigroup a => a -> a -> a
<> FilePath -> Mod OptionFields IOFormat
forall (f :: * -> *) a. HasMetavar f => FilePath -> Mod f a
metavar FilePath
"FORMAT" Mod OptionFields IOFormat
-> Mod OptionFields IOFormat -> Mod OptionFields IOFormat
forall a. Semigroup a => a -> a -> a
<> FilePath -> Mod OptionFields IOFormat
forall (f :: * -> *) a. FilePath -> Mod f a
help FilePath
"Program output format (phi, xmir)" Mod OptionFields IOFormat
-> Mod OptionFields IOFormat -> Mod OptionFields IOFormat
forall a. Semigroup a => a -> a -> a
<> IOFormat -> Mod OptionFields IOFormat
forall (f :: * -> *) a. HasValue f => a -> Mod f a
value IOFormat
PHI Mod OptionFields IOFormat
-> Mod OptionFields IOFormat -> Mod OptionFields IOFormat
forall a. Semigroup a => a -> a -> a
<> Mod OptionFields IOFormat
forall a (f :: * -> *). Show a => Mod f a
showDefault)
            Parser
  (PrintMode
   -> Bool
   -> Bool
   -> Bool
   -> Bool
   -> Bool
   -> Must
   -> Integer
   -> Integer
   -> Bool
   -> Maybe FilePath
   -> Maybe FilePath
   -> OptsRewrite)
-> Parser PrintMode
-> Parser
     (Bool
      -> Bool
      -> Bool
      -> Bool
      -> Bool
      -> Must
      -> Integer
      -> Integer
      -> Bool
      -> Maybe FilePath
      -> Maybe FilePath
      -> OptsRewrite)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> PrintMode
-> PrintMode -> Mod FlagFields PrintMode -> Parser PrintMode
forall a. a -> a -> Mod FlagFields a -> Parser a
flag PrintMode
SALTY PrintMode
SWEET (FilePath -> Mod FlagFields PrintMode
forall (f :: * -> *) a. HasName f => FilePath -> Mod f a
long FilePath
"sweet" Mod FlagFields PrintMode
-> Mod FlagFields PrintMode -> Mod FlagFields PrintMode
forall a. Semigroup a => a -> a -> a
<> FilePath -> Mod FlagFields PrintMode
forall (f :: * -> *) a. FilePath -> Mod f a
help FilePath
"Print 𝜑-program using syntax sugar")
            Parser
  (Bool
   -> Bool
   -> Bool
   -> Bool
   -> Bool
   -> Must
   -> Integer
   -> Integer
   -> Bool
   -> Maybe FilePath
   -> Maybe FilePath
   -> OptsRewrite)
-> Parser Bool
-> Parser
     (Bool
      -> Bool
      -> Bool
      -> Bool
      -> Must
      -> Integer
      -> Integer
      -> Bool
      -> Maybe FilePath
      -> Maybe FilePath
      -> OptsRewrite)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Bool
optNormalize
            Parser
  (Bool
   -> Bool
   -> Bool
   -> Bool
   -> Must
   -> Integer
   -> Integer
   -> Bool
   -> Maybe FilePath
   -> Maybe FilePath
   -> OptsRewrite)
-> Parser Bool
-> Parser
     (Bool
      -> Bool
      -> Bool
      -> Must
      -> Integer
      -> Integer
      -> Bool
      -> Maybe FilePath
      -> Maybe FilePath
      -> OptsRewrite)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Bool
optShuffle
            Parser
  (Bool
   -> Bool
   -> Bool
   -> Must
   -> Integer
   -> Integer
   -> Bool
   -> Maybe FilePath
   -> Maybe FilePath
   -> OptsRewrite)
-> Parser Bool
-> Parser
     (Bool
      -> Bool
      -> Must
      -> Integer
      -> Integer
      -> Bool
      -> Maybe FilePath
      -> Maybe FilePath
      -> OptsRewrite)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Mod FlagFields Bool -> Parser Bool
switch (FilePath -> Mod FlagFields Bool
forall (f :: * -> *) a. HasName f => FilePath -> Mod f a
long FilePath
"omit-listing" Mod FlagFields Bool -> Mod FlagFields Bool -> Mod FlagFields Bool
forall a. Semigroup a => a -> a -> a
<> FilePath -> Mod FlagFields Bool
forall (f :: * -> *) a. FilePath -> Mod f a
help FilePath
"Omit full program listing in XMIR output")
            Parser
  (Bool
   -> Bool
   -> Must
   -> Integer
   -> Integer
   -> Bool
   -> Maybe FilePath
   -> Maybe FilePath
   -> OptsRewrite)
-> Parser Bool
-> Parser
     (Bool
      -> Must
      -> Integer
      -> Integer
      -> Bool
      -> Maybe FilePath
      -> Maybe FilePath
      -> OptsRewrite)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Mod FlagFields Bool -> Parser Bool
switch (FilePath -> Mod FlagFields Bool
forall (f :: * -> *) a. HasName f => FilePath -> Mod f a
long FilePath
"omit-comments" Mod FlagFields Bool -> Mod FlagFields Bool -> Mod FlagFields Bool
forall a. Semigroup a => a -> a -> a
<> FilePath -> Mod FlagFields Bool
forall (f :: * -> *) a. FilePath -> Mod f a
help FilePath
"Omit comments in XMIR output")
            Parser
  (Bool
   -> Must
   -> Integer
   -> Integer
   -> Bool
   -> Maybe FilePath
   -> Maybe FilePath
   -> OptsRewrite)
-> Parser Bool
-> Parser
     (Must
      -> Integer
      -> Integer
      -> Bool
      -> Maybe FilePath
      -> Maybe FilePath
      -> OptsRewrite)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Bool
optDepthSensitive
            Parser
  (Must
   -> Integer
   -> Integer
   -> Bool
   -> Maybe FilePath
   -> Maybe FilePath
   -> OptsRewrite)
-> Parser Must
-> Parser
     (Integer
      -> Integer
      -> Bool
      -> Maybe FilePath
      -> Maybe FilePath
      -> OptsRewrite)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReadM Must -> Mod OptionFields Must -> Parser Must
forall a. ReadM a -> Mod OptionFields a -> Parser a
option
              ReadM Must
forall a. Read a => ReadM a
auto
              ( FilePath -> Mod OptionFields Must
forall (f :: * -> *) a. HasName f => FilePath -> Mod f a
long FilePath
"must"
                  Mod OptionFields Must
-> Mod OptionFields Must -> Mod OptionFields Must
forall a. Semigroup a => a -> a -> a
<> FilePath -> Mod OptionFields Must
forall (f :: * -> *) a. HasMetavar f => FilePath -> Mod f a
metavar FilePath
"RANGE"
                  Mod OptionFields Must
-> Mod OptionFields Must -> Mod OptionFields Must
forall a. Semigroup a => a -> a -> a
<> FilePath -> Mod OptionFields Must
forall (f :: * -> *) a. FilePath -> Mod f a
help FilePath
"Must-rewrite range (e.g., '3', '..5', '3..', '3..5'). Stops execution if number of rules applied is not in range. Use 0 to disable."
                  Mod OptionFields Must
-> Mod OptionFields Must -> Mod OptionFields Must
forall a. Semigroup a => a -> a -> a
<> Must -> Mod OptionFields Must
forall (f :: * -> *) a. HasValue f => a -> Mod f a
value Must
MtDisabled
                  Mod OptionFields Must
-> Mod OptionFields Must -> Mod OptionFields Must
forall a. Semigroup a => a -> a -> a
<> (Must -> FilePath) -> Mod OptionFields Must
forall a (f :: * -> *). (a -> FilePath) -> Mod f a
showDefaultWith Must -> FilePath
forall a. Show a => a -> FilePath
show
              )
            Parser
  (Integer
   -> Integer
   -> Bool
   -> Maybe FilePath
   -> Maybe FilePath
   -> OptsRewrite)
-> Parser Integer
-> Parser
     (Integer
      -> Bool -> Maybe FilePath -> Maybe FilePath -> OptsRewrite)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Integer
optMaxDepth
            Parser
  (Integer
   -> Bool -> Maybe FilePath -> Maybe FilePath -> OptsRewrite)
-> Parser Integer
-> Parser (Bool -> Maybe FilePath -> Maybe FilePath -> OptsRewrite)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Integer
optMaxCycles
            Parser (Bool -> Maybe FilePath -> Maybe FilePath -> OptsRewrite)
-> Parser Bool
-> Parser (Maybe FilePath -> Maybe FilePath -> OptsRewrite)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Mod FlagFields Bool -> Parser Bool
switch (FilePath -> Mod FlagFields Bool
forall (f :: * -> *) a. HasName f => FilePath -> Mod f a
long FilePath
"in-place" Mod FlagFields Bool -> Mod FlagFields Bool -> Mod FlagFields Bool
forall a. Semigroup a => a -> a -> a
<> FilePath -> Mod FlagFields Bool
forall (f :: * -> *) a. FilePath -> Mod f a
help FilePath
"Edit file in-place instead of printing to output")
            Parser (Maybe FilePath -> Maybe FilePath -> OptsRewrite)
-> Parser (Maybe FilePath)
-> Parser (Maybe FilePath -> OptsRewrite)
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser (Maybe FilePath)
optTarget
            Parser (Maybe FilePath -> OptsRewrite)
-> Parser (Maybe FilePath) -> Parser OptsRewrite
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser (Maybe FilePath)
argInputFile
        )

commandParser :: Parser Command
commandParser :: Parser Command
commandParser =
  Mod CommandFields Command -> Parser Command
forall a. Mod CommandFields a -> Parser a
hsubparser
    ( FilePath -> ParserInfo Command -> Mod CommandFields Command
forall a. FilePath -> ParserInfo a -> Mod CommandFields a
command FilePath
"rewrite" (Parser Command -> InfoMod Command -> ParserInfo Command
forall a. Parser a -> InfoMod a -> ParserInfo a
info Parser Command
rewriteParser (FilePath -> InfoMod Command
forall a. FilePath -> InfoMod a
progDesc FilePath
"Rewrite the program"))
        Mod CommandFields Command
-> Mod CommandFields Command -> Mod CommandFields Command
forall a. Semigroup a => a -> a -> a
<> FilePath -> ParserInfo Command -> Mod CommandFields Command
forall a. FilePath -> ParserInfo a -> Mod CommandFields a
command FilePath
"dataize" (Parser Command -> InfoMod Command -> ParserInfo Command
forall a. Parser a -> InfoMod a -> ParserInfo a
info Parser Command
dataizeParser (FilePath -> InfoMod Command
forall a. FilePath -> InfoMod a
progDesc FilePath
"Dataize the program"))
        Mod CommandFields Command
-> Mod CommandFields Command -> Mod CommandFields Command
forall a. Semigroup a => a -> a -> a
<> FilePath -> ParserInfo Command -> Mod CommandFields Command
forall a. FilePath -> ParserInfo a -> Mod CommandFields a
command FilePath
"explain" (Parser Command -> InfoMod Command -> ParserInfo Command
forall a. Parser a -> InfoMod a -> ParserInfo a
info Parser Command
explainParser (FilePath -> InfoMod Command
forall a. FilePath -> InfoMod a
progDesc FilePath
"Explain rules in LaTeX format"))
    )

parserInfo :: ParserInfo Command
parserInfo :: ParserInfo Command
parserInfo =
  Parser Command -> InfoMod Command -> ParserInfo Command
forall a. Parser a -> InfoMod a -> ParserInfo a
info
    (Parser Command
commandParser Parser Command -> Parser (Command -> Command) -> Parser Command
forall (f :: * -> *) a b. Applicative f => f a -> f (a -> b) -> f b
<**> Parser (Command -> Command)
forall a. Parser (a -> a)
helper Parser Command -> Parser (Command -> Command) -> Parser Command
forall (f :: * -> *) a b. Applicative f => f a -> f (a -> b) -> f b
<**> FilePath -> Parser (Command -> Command)
forall a. FilePath -> Parser (a -> a)
simpleVersioner (Version -> FilePath
showVersion Version
version))
    (InfoMod Command
forall a. InfoMod a
fullDesc InfoMod Command -> InfoMod Command -> InfoMod Command
forall a. Semigroup a => a -> a -> a
<> FilePath -> InfoMod Command
forall a. FilePath -> InfoMod a
header FilePath
"Phino - CLI Manipulator of 𝜑-Calculus Expressions")

handler :: SomeException -> IO ()
handler :: SomeException -> IO ()
handler SomeException
e = case SomeException -> Maybe ExitCode
forall e. Exception e => SomeException -> Maybe e
fromException SomeException
e of
  Just ExitCode
ExitSuccess -> () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure () -- prevent printing error on --version etc.
  Maybe ExitCode
_ -> do
    FilePath -> IO ()
logError (SomeException -> FilePath
forall e. Exception e => e -> FilePath
displayException SomeException
e)
    IO ()
forall a. IO a
exitFailure

setLogLevel' :: Command -> IO ()
setLogLevel' :: Command -> IO ()
setLogLevel' Command
cmd =
  let level :: LogLevel
level = case Command
cmd of
        CmdRewrite OptsRewrite {LogLevel
logLevel :: OptsRewrite -> LogLevel
logLevel :: LogLevel
logLevel} -> LogLevel
logLevel
        CmdDataize OptsDataize {LogLevel
logLevel :: OptsDataize -> LogLevel
logLevel :: LogLevel
logLevel} -> LogLevel
logLevel
        CmdExplain OptsExplain {LogLevel
logLevel :: OptsExplain -> LogLevel
logLevel :: LogLevel
logLevel} -> LogLevel
logLevel
   in LogLevel -> IO ()
setLogLevel LogLevel
level

runCLI :: [String] -> IO ()
runCLI :: [FilePath] -> IO ()
runCLI [FilePath]
args = (SomeException -> IO ()) -> IO () -> IO ()
forall e a. Exception e => (e -> IO a) -> IO a -> IO a
handle SomeException -> IO ()
handler (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
  Command
cmd <- ParserResult Command -> IO Command
forall a. ParserResult a -> IO a
handleParseResult (ParserPrefs
-> ParserInfo Command -> [FilePath] -> ParserResult Command
forall a.
ParserPrefs -> ParserInfo a -> [FilePath] -> ParserResult a
execParserPure ParserPrefs
defaultPrefs ParserInfo Command
parserInfo [FilePath]
args)
  Command -> IO ()
setLogLevel' Command
cmd
  case Command
cmd of
    CmdRewrite opts :: OptsRewrite
opts@OptsRewrite {Bool
Integer
[FilePath]
Maybe FilePath
LogLevel
Must
PrintMode
IOFormat
logLevel :: OptsRewrite -> LogLevel
rules :: OptsRewrite -> [FilePath]
inputFormat :: OptsRewrite -> IOFormat
outputFormat :: OptsRewrite -> IOFormat
printMode :: OptsRewrite -> PrintMode
normalize :: OptsRewrite -> Bool
shuffle :: OptsRewrite -> Bool
omitListing :: OptsRewrite -> Bool
omitComments :: OptsRewrite -> Bool
depthSensitive :: OptsRewrite -> Bool
must :: OptsRewrite -> Must
maxDepth :: OptsRewrite -> Integer
maxCycles :: OptsRewrite -> Integer
inPlace :: OptsRewrite -> Bool
targetFile :: OptsRewrite -> Maybe FilePath
inputFile :: OptsRewrite -> Maybe FilePath
logLevel :: LogLevel
rules :: [FilePath]
inputFormat :: IOFormat
outputFormat :: IOFormat
printMode :: PrintMode
normalize :: Bool
shuffle :: Bool
omitListing :: Bool
omitComments :: Bool
depthSensitive :: Bool
must :: Must
maxDepth :: Integer
maxCycles :: Integer
inPlace :: Bool
targetFile :: Maybe FilePath
inputFile :: Maybe FilePath
..} -> do
      IO ()
validateOpts
      FilePath -> IO ()
logDebug (FilePath -> Integer -> Integer -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"Amount of rewriting cycles across all the rules: %d, per rule: %d" Integer
maxCycles Integer
maxDepth)
      FilePath
input <- Maybe FilePath -> IO FilePath
readInput Maybe FilePath
inputFile
      [Rule]
rules' <- Bool -> Bool -> [FilePath] -> IO [Rule]
getRules Bool
normalize Bool
shuffle [FilePath]
rules
      Program
program <- FilePath -> IOFormat -> IO Program
parseProgram FilePath
input IOFormat
inputFormat
      Program
rewritten <- Program -> [Rule] -> RewriteContext -> IO Program
rewrite' Program
program [Rule]
rules' (Program
-> Integer
-> Integer
-> Bool
-> BuildTermFunc
-> Must
-> RewriteContext
RewriteContext Program
program Integer
maxDepth Integer
maxCycles Bool
depthSensitive BuildTermFunc
buildTerm Must
must)
      FilePath -> IO ()
logDebug (FilePath -> FilePath -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"Printing rewritten 𝜑-program as %s" (IOFormat -> FilePath
forall a. Show a => a -> FilePath
show IOFormat
outputFormat))
      FilePath
prog <- Program -> IOFormat -> PrintMode -> FilePath -> IO FilePath
printProgram Program
rewritten IOFormat
outputFormat PrintMode
printMode FilePath
input
      Maybe FilePath -> FilePath -> IO ()
output Maybe FilePath
targetFile FilePath
prog
      where
        validateOpts :: IO ()
        validateOpts :: IO ()
validateOpts = do
          Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when
            (PrintMode
printMode PrintMode -> PrintMode -> Bool
forall a. Eq a => a -> a -> Bool
== PrintMode
SWEET Bool -> Bool -> Bool
&& IOFormat
outputFormat IOFormat -> IOFormat -> Bool
forall a. Eq a => a -> a -> Bool
== IOFormat
XMIR)
            (CmdException -> IO ()
forall e a. Exception e => e -> IO a
throwIO (FilePath -> CmdException
InvalidRewriteArguments FilePath
"The --sweet and --output=xmir can't stay together"))
          Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when
            (Bool
inPlace Bool -> Bool -> Bool
&& Maybe FilePath -> Bool
forall a. Maybe a -> Bool
isNothing Maybe FilePath
inputFile)
            (CmdException -> IO ()
forall e a. Exception e => e -> IO a
throwIO (FilePath -> CmdException
InvalidRewriteArguments FilePath
"--in-place requires an input file"))
          Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when
            (Bool
inPlace Bool -> Bool -> Bool
&& Maybe FilePath -> Bool
forall a. Maybe a -> Bool
isJust Maybe FilePath
targetFile)
            (CmdException -> IO ()
forall e a. Exception e => e -> IO a
throwIO (FilePath -> CmdException
InvalidRewriteArguments FilePath
"--in-place and --target cannot be used together"))
          Integer -> IO ()
validateMaxDepth Integer
maxDepth
          Integer -> IO ()
validateMaxCycles Integer
maxCycles
          Must -> IO ()
validateMust Must
must
        printProgram :: Program -> IOFormat -> PrintMode -> String -> IO String
        printProgram :: Program -> IOFormat -> PrintMode -> FilePath -> IO FilePath
printProgram Program
prog IOFormat
PHI PrintMode
mode FilePath
_ = FilePath -> IO FilePath
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Program -> PrintMode -> Encoding -> FilePath
prettyProgram' Program
prog PrintMode
mode Encoding
UNICODE)
        printProgram Program
prog IOFormat
XMIR PrintMode
_ FilePath
listing = do
          Document
xmir <- Program -> XmirContext -> IO Document
programToXMIR Program
prog (Bool -> Bool -> FilePath -> XmirContext
XmirContext Bool
omitListing Bool
omitComments FilePath
listing)
          FilePath -> IO FilePath
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Document -> FilePath
printXMIR Document
xmir)
        printProgram Program
prog IOFormat
LATEX PrintMode
mode FilePath
_ = FilePath -> IO FilePath
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Program -> PrintMode -> FilePath
programToLaTeX Program
prog PrintMode
mode)
        output :: Maybe FilePath -> String -> IO ()
        output :: Maybe FilePath -> FilePath -> IO ()
output Maybe FilePath
target FilePath
prog = case (Bool
inPlace, Maybe FilePath
target, Maybe FilePath
inputFile) of
          (Bool
True, Maybe FilePath
_, Just FilePath
file) -> do
            FilePath -> IO ()
logDebug (FilePath -> FilePath -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"The option '--in-place' is specified, writing back to '%s'..." FilePath
file)
            FilePath -> FilePath -> IO ()
writeFile FilePath
file FilePath
prog
            FilePath -> IO ()
logInfo (FilePath -> FilePath -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"The file '%s' was modified in-place" FilePath
file)
          (Bool
False, Just FilePath
file, Maybe FilePath
_) -> do
            FilePath -> IO ()
logDebug (FilePath -> FilePath -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"The option '--target' is specified, printing to '%s'..." FilePath
file)
            FilePath -> FilePath -> IO ()
writeFile FilePath
file FilePath
prog
            FilePath -> IO ()
logInfo (FilePath -> FilePath -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"The command result was saved in '%s'" FilePath
file)
          (Bool
False, Maybe FilePath
Nothing, Maybe FilePath
_) -> do
            FilePath -> IO ()
logDebug FilePath
"The option '--target' is not specified, printing to console..."
            FilePath -> IO ()
putStrLn FilePath
prog
    CmdDataize opts :: OptsDataize
opts@OptsDataize {Bool
Integer
Maybe FilePath
LogLevel
IOFormat
logLevel :: OptsDataize -> LogLevel
inputFormat :: OptsDataize -> IOFormat
maxDepth :: OptsDataize -> Integer
maxCycles :: OptsDataize -> Integer
depthSensitive :: OptsDataize -> Bool
inputFile :: OptsDataize -> Maybe FilePath
logLevel :: LogLevel
inputFormat :: IOFormat
maxDepth :: Integer
maxCycles :: Integer
depthSensitive :: Bool
inputFile :: Maybe FilePath
..} -> do
      IO ()
validateOpts
      FilePath
input <- Maybe FilePath -> IO FilePath
readInput Maybe FilePath
inputFile
      Program
prog <- FilePath -> IOFormat -> IO Program
parseProgram FilePath
input IOFormat
inputFormat
      Maybe Bytes
dataized <- Program -> DataizeContext -> IO (Maybe Bytes)
dataize Program
prog (Program
-> Integer -> Integer -> Bool -> BuildTermFunc -> DataizeContext
DataizeContext Program
prog Integer
maxDepth Integer
maxCycles Bool
depthSensitive BuildTermFunc
buildTerm)
      IO () -> (Bytes -> IO ()) -> Maybe Bytes -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (CmdException -> IO ()
forall e a. Exception e => e -> IO a
throwIO CmdException
CouldNotDataize) (FilePath -> IO ()
putStrLn (FilePath -> IO ()) -> (Bytes -> FilePath) -> Bytes -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bytes -> FilePath
prettyBytes) Maybe Bytes
dataized
      where
        validateOpts :: IO ()
        validateOpts :: IO ()
validateOpts = do
          Integer -> IO ()
validateMaxDepth Integer
maxDepth
          Integer -> IO ()
validateMaxCycles Integer
maxCycles
    CmdExplain opts :: OptsExplain
opts@OptsExplain {Bool
[FilePath]
Maybe FilePath
LogLevel
logLevel :: OptsExplain -> LogLevel
rules :: OptsExplain -> [FilePath]
normalize :: OptsExplain -> Bool
shuffle :: OptsExplain -> Bool
targetFile :: OptsExplain -> Maybe FilePath
logLevel :: LogLevel
rules :: [FilePath]
normalize :: Bool
shuffle :: Bool
targetFile :: Maybe FilePath
..} -> do
      IO ()
validateOpts
      [Rule]
rules' <- Bool -> Bool -> [FilePath] -> IO [Rule]
getRules Bool
normalize Bool
shuffle [FilePath]
rules
      let latex :: FilePath
latex = [Rule] -> FilePath
explainRules [Rule]
rules'
      Maybe FilePath -> FilePath -> IO ()
output Maybe FilePath
targetFile ([Rule] -> FilePath
explainRules [Rule]
rules')
      where
        validateOpts :: IO ()
        validateOpts :: IO ()
validateOpts =
          Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when
            ([FilePath] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FilePath]
rules Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
normalize)
            (CmdException -> IO ()
forall e a. Exception e => e -> IO a
throwIO (FilePath -> CmdException
InvalidRewriteArguments FilePath
"Either --rule or --normalize must be specified"))
  where
    validateIntArgument :: Integer -> (Integer -> Bool) -> String -> IO ()
    validateIntArgument :: Integer -> (Integer -> Bool) -> FilePath -> IO ()
validateIntArgument Integer
num Integer -> Bool
cmp FilePath
msg =
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when
        (Integer -> Bool
cmp Integer
num)
        (CmdException -> IO ()
forall e a. Exception e => e -> IO a
throwIO (FilePath -> CmdException
InvalidRewriteArguments FilePath
msg))
    validateMaxDepth :: Integer -> IO ()
    validateMaxDepth :: Integer -> IO ()
validateMaxDepth Integer
depth = Integer -> (Integer -> Bool) -> FilePath -> IO ()
validateIntArgument Integer
depth (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
0) FilePath
"--max-depth must be positive"
    validateMaxCycles :: Integer -> IO ()
    validateMaxCycles :: Integer -> IO ()
validateMaxCycles Integer
cycles = Integer -> (Integer -> Bool) -> FilePath -> IO ()
validateIntArgument Integer
cycles (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
0) FilePath
"--max-cycles must be positive"
    validateMust :: Must -> IO ()
    validateMust :: Must -> IO ()
validateMust Must
MtDisabled = () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    validateMust (MtExact Integer
n) = Integer -> (Integer -> Bool) -> FilePath -> IO ()
validateIntArgument Integer
n (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
0) FilePath
"--must exact value must be positive"
    validateMust (MtRange Maybe Integer
minVal Maybe Integer
maxVal) = do
      IO () -> (Integer -> IO ()) -> Maybe Integer -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) (\Integer
n -> Integer -> (Integer -> Bool) -> FilePath -> IO ()
validateIntArgument Integer
n (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0) FilePath
"--must minimum must be non-negative") Maybe Integer
minVal
      IO () -> (Integer -> IO ()) -> Maybe Integer -> IO ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (() -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) (\Integer
n -> Integer -> (Integer -> Bool) -> FilePath -> IO ()
validateIntArgument Integer
n (Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0) FilePath
"--must maximum must be non-negative") Maybe Integer
maxVal
      case (Maybe Integer
minVal, Maybe Integer
maxVal) of
        (Just Integer
min, Just Integer
max)
          | Integer
min Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
max ->
              CmdException -> IO ()
forall e a. Exception e => e -> IO a
throwIO
                ( FilePath -> CmdException
InvalidRewriteArguments
                    (FilePath -> Integer -> Integer -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"--must range invalid: minimum (%d) is greater than maximum (%d)" Integer
min Integer
max)
                )
        (Maybe Integer, Maybe Integer)
_ -> () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    readInput :: Maybe FilePath -> IO String
    readInput :: Maybe FilePath -> IO FilePath
readInput Maybe FilePath
inputFile' = case Maybe FilePath
inputFile' of
      Just FilePath
pth -> do
        FilePath -> IO ()
logDebug (FilePath -> FilePath -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"Reading from file: '%s'" FilePath
pth)
        FilePath -> IO FilePath
readFile (FilePath -> IO FilePath) -> IO FilePath -> IO FilePath
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< FilePath -> IO FilePath
ensuredFile FilePath
pth
      Maybe FilePath
Nothing -> do
        FilePath -> IO ()
logDebug FilePath
"Reading from stdin"
        IO FilePath
getContents' IO FilePath -> (SomeException -> IO FilePath) -> IO FilePath
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` (\(SomeException
e :: SomeException) -> CmdException -> IO FilePath
forall e a. Exception e => e -> IO a
throwIO (FilePath -> CmdException
CouldNotReadFromStdin (SomeException -> FilePath
forall a. Show a => a -> FilePath
show SomeException
e)))
    parseProgram :: String -> IOFormat -> IO Program
    parseProgram :: FilePath -> IOFormat -> IO Program
parseProgram FilePath
phi IOFormat
PHI = FilePath -> IO Program
parseProgramThrows FilePath
phi
    parseProgram FilePath
xmir IOFormat
XMIR = do
      Document
doc <- FilePath -> IO Document
parseXMIRThrows FilePath
xmir
      Document -> IO Program
xmirToPhi Document
doc
    getRules :: Bool -> Bool -> [FilePath] -> IO [Y.Rule]
    getRules :: Bool -> Bool -> [FilePath] -> IO [Rule]
getRules Bool
normalize Bool
shuffle [FilePath]
rules = do
      [Rule]
ordered <-
        if Bool
normalize
          then do
            let rules' :: [Rule]
rules' = [Rule]
normalizationRules
            FilePath -> IO ()
logDebug (FilePath -> Int -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"The --normalize option is provided, %d built-it normalization rules are used" ([Rule] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Rule]
rules'))
            [Rule] -> IO [Rule]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Rule]
rules'
          else
            if [FilePath] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FilePath]
rules
              then do
                FilePath -> IO ()
logDebug FilePath
"No --rule and no --normalize options are provided, no rules are used"
                [Rule] -> IO [Rule]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
              else do
                FilePath -> IO ()
logDebug (FilePath -> FilePath -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"Using rules from files: [%s]" (FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate FilePath
", " [FilePath]
rules))
                [FilePath]
yamls <- (FilePath -> IO FilePath) -> [FilePath] -> IO [FilePath]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM FilePath -> IO FilePath
ensuredFile [FilePath]
rules
                (FilePath -> IO Rule) -> [FilePath] -> IO [Rule]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM FilePath -> IO Rule
Y.yamlRule [FilePath]
yamls
      if Bool
shuffle
        then do
          FilePath -> IO ()
logDebug FilePath
"The --shuffle option is provided, rules are used in random order"
          [Rule] -> IO [Rule]
forall a. [a] -> IO [a]
Misc.shuffle [Rule]
ordered
        else [Rule] -> IO [Rule]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Rule]
ordered
    output :: Maybe FilePath -> String -> IO ()
    output :: Maybe FilePath -> FilePath -> IO ()
output Maybe FilePath
target FilePath
content = case Maybe FilePath
target of
      Maybe FilePath
Nothing -> do
        FilePath -> IO ()
logDebug FilePath
"The option '--target' is not specified, printing to console..."
        FilePath -> IO ()
putStrLn FilePath
content
      Just FilePath
file -> do
        FilePath -> IO ()
logDebug (FilePath -> FilePath -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"The option '--target' is specified, printing to '%s'..." FilePath
file)
        FilePath -> FilePath -> IO ()
writeFile FilePath
file FilePath
content
        FilePath -> IO ()
logInfo (FilePath -> FilePath -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"The command result was saved in '%s'" FilePath
file)