{-# 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.Version (showVersion)
import Dataize (DataizeContext (DataizeContext), dataize)
import Functions (buildTermFromFunction)
import qualified Functions
import Logger
import Misc (ensuredFile)
import qualified Misc
import Options.Applicative
import Parser (parseProgramThrows)
import Paths_phino (version)
import Pretty (PrintMode (SALTY, SWEET), prettyProgram', prettyBytes)
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 -> String
message :: String}
  | CouldNotReadFromStdin {message :: String}
  | CouldNotDataize
  deriving (Show CmdException
Typeable CmdException
(Typeable CmdException, Show CmdException) =>
(CmdException -> SomeException)
-> (SomeException -> Maybe CmdException)
-> (CmdException -> String)
-> Exception CmdException
SomeException -> Maybe CmdException
CmdException -> String
CmdException -> SomeException
forall e.
(Typeable e, Show e) =>
(e -> SomeException)
-> (SomeException -> Maybe e) -> (e -> String) -> Exception e
$ctoException :: CmdException -> SomeException
toException :: CmdException -> SomeException
$cfromException :: SomeException -> Maybe CmdException
fromException :: SomeException -> Maybe CmdException
$cdisplayException :: CmdException -> String
displayException :: CmdException -> String
Exception)

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

data Command
  = CmdRewrite OptsRewrite
  | CmdDataize OptsDataize

data IOFormat = XMIR | PHI
  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 -> String
show IOFormat
XMIR = String
"xmir"
  show IOFormat
PHI = String
"phi"

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

data OptsRewrite = OptsRewrite
  { OptsRewrite -> LogLevel
logLevel :: LogLevel,
    OptsRewrite -> [String]
rules :: [FilePath],
    OptsRewrite -> IOFormat
inputFormat :: IOFormat,
    OptsRewrite -> IOFormat
outputFormat :: IOFormat,
    OptsRewrite -> PrintMode
printMode :: PrintMode,
    OptsRewrite -> Bool
normalize :: Bool,
    OptsRewrite -> Bool
nothing :: Bool,
    OptsRewrite -> Bool
shuffle :: Bool,
    OptsRewrite -> Bool
omitListing :: Bool,
    OptsRewrite -> Bool
omitComments :: Bool,
    OptsRewrite -> Integer
maxDepth :: Integer,
    OptsRewrite -> Maybe String
inputFile :: Maybe FilePath
  }

parseIOFormat :: String -> ReadM IOFormat
parseIOFormat :: String -> ReadM IOFormat
parseIOFormat String
type' = (String -> Either String IOFormat) -> ReadM IOFormat
forall a. (String -> Either String a) -> ReadM a
eitherReader ((String -> Either String IOFormat) -> ReadM IOFormat)
-> (String -> Either String IOFormat) -> ReadM IOFormat
forall a b. (a -> b) -> a -> b
$ \String
format -> case (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
format of
  String
"xmir" -> IOFormat -> Either String IOFormat
forall a b. b -> Either a b
Right IOFormat
XMIR
  String
"phi" -> IOFormat -> Either String IOFormat
forall a b. b -> Either a b
Right IOFormat
PHI
  String
_ -> String -> Either String IOFormat
forall a b. a -> Either a b
Left (String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf String
"invalid %s format: expected '%s' or '%s'" String
type' (IOFormat -> String
forall a. Show a => a -> String
show IOFormat
PHI) (IOFormat -> String
forall a. Show a => a -> String
show IOFormat
XMIR))

argInputFile :: Parser (Maybe FilePath)
argInputFile :: Parser (Maybe String)
argInputFile = Parser String -> Parser (Maybe String)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (ReadM String -> Mod ArgumentFields String -> Parser String
forall a. ReadM a -> Mod ArgumentFields a -> Parser a
argument ReadM String
forall s. IsString s => ReadM s
str (String -> Mod ArgumentFields String
forall (f :: * -> *) a. HasMetavar f => String -> Mod f a
metavar String
"FILE" Mod ArgumentFields String
-> Mod ArgumentFields String -> Mod ArgumentFields String
forall a. Semigroup a => a -> a -> a
<> String -> Mod ArgumentFields String
forall (f :: * -> *) a. String -> Mod f a
help String
"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 (String -> Mod OptionFields Integer
forall (f :: * -> *) a. HasName f => String -> Mod f a
long String
"max-depth" Mod OptionFields Integer
-> Mod OptionFields Integer -> Mod OptionFields Integer
forall a. Semigroup a => a -> a -> a
<> String -> Mod OptionFields Integer
forall (f :: * -> *) a. HasMetavar f => String -> Mod f a
metavar String
"DEPTH" Mod OptionFields Integer
-> Mod OptionFields Integer -> Mod OptionFields Integer
forall a. Semigroup a => a -> a -> a
<> String -> Mod OptionFields Integer
forall (f :: * -> *) a. String -> Mod f a
help String
"Max amount of rewritng cycles" 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 (String -> ReadM IOFormat
parseIOFormat String
"input") (String -> Mod OptionFields IOFormat
forall (f :: * -> *) a. HasName f => String -> Mod f a
long String
"input" Mod OptionFields IOFormat
-> Mod OptionFields IOFormat -> Mod OptionFields IOFormat
forall a. Semigroup a => a -> a -> a
<> String -> Mod OptionFields IOFormat
forall (f :: * -> *) a. HasMetavar f => String -> Mod f a
metavar String
"FORMAT" Mod OptionFields IOFormat
-> Mod OptionFields IOFormat -> Mod OptionFields IOFormat
forall a. Semigroup a => a -> a -> a
<> String -> Mod OptionFields IOFormat
forall (f :: * -> *) a. String -> Mod f a
help String
"Program input 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)

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
    ( String -> Mod OptionFields LogLevel
forall (f :: * -> *) a. HasName f => String -> Mod f a
long String
"log-level"
        Mod OptionFields LogLevel
-> Mod OptionFields LogLevel -> Mod OptionFields LogLevel
forall a. Semigroup a => a -> a -> a
<> String -> Mod OptionFields LogLevel
forall (f :: * -> *) a. HasMetavar f => String -> Mod f a
metavar String
"LEVEL"
        Mod OptionFields LogLevel
-> Mod OptionFields LogLevel -> Mod OptionFields LogLevel
forall a. Semigroup a => a -> a -> a
<> String -> Mod OptionFields LogLevel
forall (f :: * -> *) a. String -> Mod f a
help (String
"Log level (" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((LogLevel -> String) -> [LogLevel] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map LogLevel -> String
forall a. Show a => a -> String
show [LogLevel
DEBUG, LogLevel
INFO, LogLevel
WARNING, LogLevel
ERROR, LogLevel
NONE]) String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
")")
        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 = (String -> Either String LogLevel) -> ReadM LogLevel
forall a. (String -> Either String a) -> ReadM a
eitherReader ((String -> Either String LogLevel) -> ReadM LogLevel)
-> (String -> Either String LogLevel) -> ReadM LogLevel
forall a b. (a -> b) -> a -> b
$ \String
lvl -> case (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toUpper String
lvl of
      String
"DEBUG" -> LogLevel -> Either String LogLevel
forall a b. b -> Either a b
Right LogLevel
DEBUG
      String
"INFO" -> LogLevel -> Either String LogLevel
forall a b. b -> Either a b
Right LogLevel
INFO
      String
"WARNING" -> LogLevel -> Either String LogLevel
forall a b. b -> Either a b
Right LogLevel
WARNING
      String
"WARN" -> LogLevel -> Either String LogLevel
forall a b. b -> Either a b
Right LogLevel
WARNING
      String
"ERROR" -> LogLevel -> Either String LogLevel
forall a b. b -> Either a b
Right LogLevel
ERROR
      String
"ERR" -> LogLevel -> Either String LogLevel
forall a b. b -> Either a b
Right LogLevel
ERROR
      String
"NONE" -> LogLevel -> Either String LogLevel
forall a b. b -> Either a b
Right LogLevel
NONE
      String
_ -> String -> Either String LogLevel
forall a b. a -> Either a b
Left (String -> Either String LogLevel)
-> String -> Either String LogLevel
forall a b. (a -> b) -> a -> b
$ String
"unknown log-level: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
lvl

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 -> Maybe String -> OptsDataize
OptsDataize
            (LogLevel -> IOFormat -> Integer -> Maybe String -> OptsDataize)
-> Parser LogLevel
-> Parser (IOFormat -> Integer -> Maybe String -> OptsDataize)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser LogLevel
optLogLevel
            Parser (IOFormat -> Integer -> Maybe String -> OptsDataize)
-> Parser IOFormat
-> Parser (Integer -> Maybe String -> 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 -> Maybe String -> OptsDataize)
-> Parser Integer -> Parser (Maybe String -> 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 (Maybe String -> OptsDataize)
-> Parser (Maybe String) -> 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 String)
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
-> [String]
-> IOFormat
-> IOFormat
-> PrintMode
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Integer
-> Maybe String
-> OptsRewrite
OptsRewrite
            (LogLevel
 -> [String]
 -> IOFormat
 -> IOFormat
 -> PrintMode
 -> Bool
 -> Bool
 -> Bool
 -> Bool
 -> Bool
 -> Integer
 -> Maybe String
 -> OptsRewrite)
-> Parser LogLevel
-> Parser
     ([String]
      -> IOFormat
      -> IOFormat
      -> PrintMode
      -> Bool
      -> Bool
      -> Bool
      -> Bool
      -> Bool
      -> Integer
      -> Maybe String
      -> OptsRewrite)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser LogLevel
optLogLevel
            Parser
  ([String]
   -> IOFormat
   -> IOFormat
   -> PrintMode
   -> Bool
   -> Bool
   -> Bool
   -> Bool
   -> Bool
   -> Integer
   -> Maybe String
   -> OptsRewrite)
-> Parser [String]
-> Parser
     (IOFormat
      -> IOFormat
      -> PrintMode
      -> Bool
      -> Bool
      -> Bool
      -> Bool
      -> Bool
      -> Integer
      -> Maybe String
      -> 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 String -> Parser [String]
forall a. Parser a -> Parser [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (Mod OptionFields String -> Parser String
forall s. IsString s => Mod OptionFields s -> Parser s
strOption (String -> Mod OptionFields String
forall (f :: * -> *) a. HasName f => String -> Mod f a
long String
"rule" Mod OptionFields String
-> Mod OptionFields String -> Mod OptionFields String
forall a. Semigroup a => a -> a -> a
<> String -> Mod OptionFields String
forall (f :: * -> *) a. HasMetavar f => String -> Mod f a
metavar String
"FILE" Mod OptionFields String
-> Mod OptionFields String -> Mod OptionFields String
forall a. Semigroup a => a -> a -> a
<> String -> Mod OptionFields String
forall (f :: * -> *) a. String -> Mod f a
help String
"Path to custom rule"))
            Parser
  (IOFormat
   -> IOFormat
   -> PrintMode
   -> Bool
   -> Bool
   -> Bool
   -> Bool
   -> Bool
   -> Integer
   -> Maybe String
   -> OptsRewrite)
-> Parser IOFormat
-> Parser
     (IOFormat
      -> PrintMode
      -> Bool
      -> Bool
      -> Bool
      -> Bool
      -> Bool
      -> Integer
      -> Maybe String
      -> 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
   -> Integer
   -> Maybe String
   -> OptsRewrite)
-> Parser IOFormat
-> Parser
     (PrintMode
      -> Bool
      -> Bool
      -> Bool
      -> Bool
      -> Bool
      -> Integer
      -> Maybe String
      -> 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 (String -> ReadM IOFormat
parseIOFormat String
"output") (String -> Mod OptionFields IOFormat
forall (f :: * -> *) a. HasName f => String -> Mod f a
long String
"output" Mod OptionFields IOFormat
-> Mod OptionFields IOFormat -> Mod OptionFields IOFormat
forall a. Semigroup a => a -> a -> a
<> String -> Mod OptionFields IOFormat
forall (f :: * -> *) a. HasMetavar f => String -> Mod f a
metavar String
"FORMAT" Mod OptionFields IOFormat
-> Mod OptionFields IOFormat -> Mod OptionFields IOFormat
forall a. Semigroup a => a -> a -> a
<> String -> Mod OptionFields IOFormat
forall (f :: * -> *) a. String -> Mod f a
help String
"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
   -> Integer
   -> Maybe String
   -> OptsRewrite)
-> Parser PrintMode
-> Parser
     (Bool
      -> Bool
      -> Bool
      -> Bool
      -> Bool
      -> Integer
      -> Maybe String
      -> 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 (String -> Mod FlagFields PrintMode
forall (f :: * -> *) a. HasName f => String -> Mod f a
long String
"sweet" Mod FlagFields PrintMode
-> Mod FlagFields PrintMode -> Mod FlagFields PrintMode
forall a. Semigroup a => a -> a -> a
<> String -> Mod FlagFields PrintMode
forall (f :: * -> *) a. String -> Mod f a
help String
"Print 𝜑-program using syntax sugar")
            Parser
  (Bool
   -> Bool
   -> Bool
   -> Bool
   -> Bool
   -> Integer
   -> Maybe String
   -> OptsRewrite)
-> Parser Bool
-> Parser
     (Bool
      -> Bool -> Bool -> Bool -> Integer -> Maybe String -> 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 (String -> Mod FlagFields Bool
forall (f :: * -> *) a. HasName f => String -> Mod f a
long String
"normalize" Mod FlagFields Bool -> Mod FlagFields Bool -> Mod FlagFields Bool
forall a. Semigroup a => a -> a -> a
<> String -> Mod FlagFields Bool
forall (f :: * -> *) a. String -> Mod f a
help String
"Use built-in normalization rules")
            Parser
  (Bool
   -> Bool -> Bool -> Bool -> Integer -> Maybe String -> OptsRewrite)
-> Parser Bool
-> Parser
     (Bool -> Bool -> Bool -> Integer -> Maybe String -> 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 (String -> Mod FlagFields Bool
forall (f :: * -> *) a. HasName f => String -> Mod f a
long String
"nothing" Mod FlagFields Bool -> Mod FlagFields Bool -> Mod FlagFields Bool
forall a. Semigroup a => a -> a -> a
<> String -> Mod FlagFields Bool
forall (f :: * -> *) a. String -> Mod f a
help String
"Just desugar provided 𝜑-program")
            Parser
  (Bool -> Bool -> Bool -> Integer -> Maybe String -> OptsRewrite)
-> Parser Bool
-> Parser (Bool -> Bool -> Integer -> Maybe String -> 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 (String -> Mod FlagFields Bool
forall (f :: * -> *) a. HasName f => String -> Mod f a
long String
"shuffle" Mod FlagFields Bool -> Mod FlagFields Bool -> Mod FlagFields Bool
forall a. Semigroup a => a -> a -> a
<> String -> Mod FlagFields Bool
forall (f :: * -> *) a. String -> Mod f a
help String
"Shuffle rules before applying")
            Parser (Bool -> Bool -> Integer -> Maybe String -> OptsRewrite)
-> Parser Bool
-> Parser (Bool -> Integer -> Maybe String -> 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 (String -> Mod FlagFields Bool
forall (f :: * -> *) a. HasName f => String -> Mod f a
long String
"omit-listing" Mod FlagFields Bool -> Mod FlagFields Bool -> Mod FlagFields Bool
forall a. Semigroup a => a -> a -> a
<> String -> Mod FlagFields Bool
forall (f :: * -> *) a. String -> Mod f a
help String
"Omit full program listing in XMIR output")
            Parser (Bool -> Integer -> Maybe String -> OptsRewrite)
-> Parser Bool -> Parser (Integer -> Maybe String -> 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 (String -> Mod FlagFields Bool
forall (f :: * -> *) a. HasName f => String -> Mod f a
long String
"omit-comments" Mod FlagFields Bool -> Mod FlagFields Bool -> Mod FlagFields Bool
forall a. Semigroup a => a -> a -> a
<> String -> Mod FlagFields Bool
forall (f :: * -> *) a. String -> Mod f a
help String
"Omit comments in XMIR output")
            Parser (Integer -> Maybe String -> OptsRewrite)
-> Parser Integer -> Parser (Maybe String -> 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 (Maybe String -> OptsRewrite)
-> Parser (Maybe String) -> 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 String)
argInputFile
        )

commandParser :: Parser Command
commandParser :: Parser Command
commandParser =
  Mod CommandFields Command -> Parser Command
forall a. Mod CommandFields a -> Parser a
hsubparser
    ( String -> ParserInfo Command -> Mod CommandFields Command
forall a. String -> ParserInfo a -> Mod CommandFields a
command String
"rewrite" (Parser Command -> InfoMod Command -> ParserInfo Command
forall a. Parser a -> InfoMod a -> ParserInfo a
info (Parser Command
rewriteParser 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) (String -> InfoMod Command
forall a. String -> InfoMod a
progDesc String
"Rewrite the program"))
        Mod CommandFields Command
-> Mod CommandFields Command -> Mod CommandFields Command
forall a. Semigroup a => a -> a -> a
<> String -> ParserInfo Command -> Mod CommandFields Command
forall a. String -> ParserInfo a -> Mod CommandFields a
command String
"dataize" (Parser Command -> InfoMod Command -> ParserInfo Command
forall a. Parser a -> InfoMod a -> ParserInfo a
info (Parser Command
dataizeParser 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) (String -> InfoMod Command
forall a. String -> InfoMod a
progDesc String
"Dataize the program"))
    )

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
<**> String -> Parser (Command -> Command)
forall a. String -> Parser (a -> a)
simpleVersioner (Version -> String
showVersion Version
version))
    (InfoMod Command
forall a. InfoMod a
fullDesc InfoMod Command -> InfoMod Command -> InfoMod Command
forall a. Semigroup a => a -> a -> a
<> String -> InfoMod Command
forall a. String -> InfoMod a
header String
"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
    String -> IO ()
logError (SomeException -> String
forall e. Exception e => e -> String
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
   in LogLevel -> IO ()
setLogLevel LogLevel
level

runCLI :: [String] -> IO ()
runCLI :: [String] -> IO ()
runCLI [String]
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 -> [String] -> ParserResult Command
forall a. ParserPrefs -> ParserInfo a -> [String] -> ParserResult a
execParserPure ParserPrefs
defaultPrefs ParserInfo Command
parserInfo [String]
args)
  Command -> IO ()
setLogLevel' Command
cmd
  case Command
cmd of
    CmdRewrite OptsRewrite {Bool
Integer
[String]
Maybe String
LogLevel
PrintMode
IOFormat
logLevel :: OptsRewrite -> LogLevel
rules :: OptsRewrite -> [String]
inputFormat :: OptsRewrite -> IOFormat
outputFormat :: OptsRewrite -> IOFormat
printMode :: OptsRewrite -> PrintMode
normalize :: OptsRewrite -> Bool
nothing :: OptsRewrite -> Bool
shuffle :: OptsRewrite -> Bool
omitListing :: OptsRewrite -> Bool
omitComments :: OptsRewrite -> Bool
maxDepth :: OptsRewrite -> Integer
inputFile :: OptsRewrite -> Maybe String
logLevel :: LogLevel
rules :: [String]
inputFormat :: IOFormat
outputFormat :: IOFormat
printMode :: PrintMode
normalize :: Bool
nothing :: Bool
shuffle :: Bool
omitListing :: Bool
omitComments :: Bool
maxDepth :: Integer
inputFile :: Maybe String
..} -> do
      Integer -> IO ()
validateMaxDepth Integer
maxDepth
      String -> IO ()
logDebug (String -> Integer -> String
forall r. PrintfType r => String -> r
printf String
"Amount of rewriting cycles: %d" Integer
maxDepth)
      String
input <- Maybe String -> IO String
readInput Maybe String
inputFile
      [Rule]
rules' <- IO [Rule]
getRules
      Program
program <- String -> IOFormat -> IO Program
parseProgram String
input IOFormat
inputFormat
      Program
rewritten <- Program -> [Rule] -> RewriteContext -> IO Program
rewrite' Program
program [Rule]
rules' (Program -> Integer -> BuildTermFunc -> RewriteContext
RewriteContext Program
program Integer
maxDepth BuildTermFunc
buildTermFromFunction)
      String -> IO ()
logDebug (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Printing rewritten 𝜑-program as %s" (IOFormat -> String
forall a. Show a => a -> String
show IOFormat
outputFormat))
      String
out <- Program -> IOFormat -> PrintMode -> IO String
printProgram Program
rewritten IOFormat
outputFormat PrintMode
printMode
      String -> IO ()
putStrLn String
out
      where
        getRules :: IO [Y.Rule]
        getRules :: IO [Rule]
getRules = do
          [Rule]
ordered <-
            if Bool
nothing
              then do
                String -> IO ()
logDebug String
"The --nothing option is provided, no rules are used"
                [Rule] -> IO [Rule]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
              else
                if Bool
normalize
                  then do
                    let rules' :: [Rule]
rules' = [Rule]
normalizationRules
                    String -> IO ()
logDebug (String -> Int -> String
forall r. PrintfType r => String -> r
printf String
"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 [String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
rules
                      then CmdException -> IO [Rule]
forall e a. Exception e => e -> IO a
throwIO (String -> CmdException
InvalidRewriteArguments String
"no --rule, no --normalize, no --nothing are provided")
                      else do
                        String -> IO ()
logDebug (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Using rules from files: [%s]" (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " [String]
rules))
                        [String]
yamls <- (String -> IO String) -> [String] -> IO [String]
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 String -> IO String
ensuredFile [String]
rules
                        (String -> IO Rule) -> [String] -> 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 String -> IO Rule
Y.yamlRule [String]
yamls
          if Bool
shuffle
            then do
              String -> IO ()
logDebug String
"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
        printProgram :: Program -> IOFormat -> PrintMode -> IO String
        printProgram :: Program -> IOFormat -> PrintMode -> IO String
printProgram Program
prog IOFormat
PHI PrintMode
mode = String -> IO String
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Program -> PrintMode -> String
prettyProgram' Program
prog PrintMode
mode)
        printProgram Program
prog IOFormat
XMIR PrintMode
mode = do
          Document
xmir <- Program -> XmirContext -> IO Document
programToXMIR Program
prog (Bool -> Bool -> PrintMode -> XmirContext
XmirContext Bool
omitListing Bool
omitComments PrintMode
printMode)
          String -> IO String
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Document -> String
printXMIR Document
xmir)
    CmdDataize OptsDataize {Integer
Maybe String
LogLevel
IOFormat
logLevel :: OptsDataize -> LogLevel
inputFormat :: OptsDataize -> IOFormat
maxDepth :: OptsDataize -> Integer
inputFile :: OptsDataize -> Maybe String
logLevel :: LogLevel
inputFormat :: IOFormat
maxDepth :: Integer
inputFile :: Maybe String
..} -> do
      Integer -> IO ()
validateMaxDepth Integer
maxDepth
      String
input <- Maybe String -> IO String
readInput Maybe String
inputFile
      Program
prog <- String -> IOFormat -> IO Program
parseProgram String
input IOFormat
inputFormat
      Maybe Bytes
dataized <- Program -> DataizeContext -> IO (Maybe Bytes)
dataize Program
prog (Program -> Integer -> BuildTermFunc -> DataizeContext
DataizeContext Program
prog Integer
maxDepth BuildTermFunc
buildTermFromFunction)
      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) (String -> IO ()
putStrLn (String -> IO ()) -> (Bytes -> String) -> Bytes -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bytes -> String
prettyBytes) Maybe Bytes
dataized
  where
    validateMaxDepth :: Integer -> IO ()
    validateMaxDepth :: Integer -> IO ()
validateMaxDepth Integer
depth =
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when
        (Integer
depth Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
0)
        (CmdException -> IO ()
forall e a. Exception e => e -> IO a
throwIO (String -> CmdException
InvalidRewriteArguments String
"--max-depth must be positive"))
    readInput :: Maybe FilePath -> IO String
    readInput :: Maybe String -> IO String
readInput Maybe String
inputFile' = case Maybe String
inputFile' of
      Just String
pth -> do
        String -> IO ()
logDebug (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"Reading from file: '%s'" String
pth)
        String -> IO String
readFile (String -> IO String) -> IO String -> IO String
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< String -> IO String
ensuredFile String
pth
      Maybe String
Nothing -> do
        String -> IO ()
logDebug String
"Reading from stdin"
        IO String
getContents' IO String -> (SomeException -> IO String) -> IO String
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` (\(SomeException
e :: SomeException) -> CmdException -> IO String
forall e a. Exception e => e -> IO a
throwIO (String -> CmdException
CouldNotReadFromStdin (SomeException -> String
forall a. Show a => a -> String
show SomeException
e)))
    parseProgram :: String -> IOFormat -> IO Program
    parseProgram :: String -> IOFormat -> IO Program
parseProgram String
phi IOFormat
PHI = String -> IO Program
parseProgramThrows String
phi
    parseProgram String
xmir IOFormat
XMIR = do
      Document
doc <- String -> IO Document
parseXMIRThrows String
xmir
      Document -> IO Program
xmirToPhi Document
doc