{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}

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

module CLI.Runners where

import AST
import CLI.Helpers
import CLI.Types
import CLI.Validators
import Condition (parseConditionThrows)
import Control.Exception
import Control.Monad (unless, when)
import Data.Foldable (traverse_)
import Data.IORef (newIORef)
import Data.List (intercalate)
import qualified Data.List.NonEmpty as NE
import qualified Data.Map.Strict as Map
import Data.Maybe (fromJust, isJust, isNothing, listToMaybe)
import qualified Data.Text as T
import Dataize
import Deps (Judgment (..), dontSaveMade)
import Emit (emitted)
import Encoding
import Engine (Engine (..), building, current, stepOf)
import Evaluate (evaluation)
import Files (overwrite)
import qualified Filter as F
import LaTeX (explainContextualizeRules, explainDataizeRules, explainMorphRules, explainRules)
import Logger
import Margin (defaultMargin)
import Merge (merge)
import Metas (Metas (..))
import Morph
import Parser (parseExpressionThrows)
import qualified Printer as P
import qualified Random as R
import Rewriter
import Rule (RuleContext (..), matchExpressionWithRule)
import Slots (anonymous)
import System.Directory (canonicalizePath, doesFileExist, getModificationTime)
import System.Exit (exitSuccess)
import System.FilePath (takeDirectory, (</>))
import System.Random (mkStdGen, setStdGen)
import Tau (seedTaus)
import Text.Printf (printf)
import XMIR
import qualified Yaml as Y

runRewrite :: OptsRewrite -> IO ()
runRewrite :: OptsRewrite -> IO ()
runRewrite OptsRewrite{Bool
Int
FilePath
[FilePath]
Maybe Int
Maybe FilePath
LogLevel
Must
Form
SugarType
LineFormat
IOFormat
_logLevel :: LogLevel
_logLines :: Int
_inputFormat :: IOFormat
_monoform :: Form
_outputFormat :: IOFormat
_sugarType :: SugarType
_hideRho :: Bool
_flat :: LineFormat
_must :: Must
_normalize :: Bool
_shuffle :: Bool
_seed :: Int
_omitListing :: Bool
_omitComments :: Bool
_depthSensitive :: Bool
_nonumber :: Bool
_inPlace :: Bool
_update :: Bool
_sequence :: Bool
_headers :: Bool
_canonize :: Bool
_compress :: Bool
_maxDepth :: Int
_maxCycles :: Int
_margin :: Int
_meetPopularity :: Maybe Int
_meetLength :: Maybe Int
_rules :: [FilePath]
_hide :: [FilePath]
_show :: [FilePath]
_locator :: FilePath
_focus :: FilePath
_expression :: Maybe FilePath
_label :: Maybe FilePath
_meetPrefix :: Maybe FilePath
_breakpoint :: Maybe FilePath
_targetFile :: Maybe FilePath
_stepsDir :: Maybe FilePath
_inputFile :: Maybe FilePath
$sel:_logLevel:OptsRewrite :: OptsRewrite -> LogLevel
$sel:_logLines:OptsRewrite :: OptsRewrite -> Int
$sel:_inputFormat:OptsRewrite :: OptsRewrite -> IOFormat
$sel:_monoform:OptsRewrite :: OptsRewrite -> Form
$sel:_outputFormat:OptsRewrite :: OptsRewrite -> IOFormat
$sel:_sugarType:OptsRewrite :: OptsRewrite -> SugarType
$sel:_hideRho:OptsRewrite :: OptsRewrite -> Bool
$sel:_flat:OptsRewrite :: OptsRewrite -> LineFormat
$sel:_must:OptsRewrite :: OptsRewrite -> Must
$sel:_normalize:OptsRewrite :: OptsRewrite -> Bool
$sel:_shuffle:OptsRewrite :: OptsRewrite -> Bool
$sel:_seed:OptsRewrite :: OptsRewrite -> Int
$sel:_omitListing:OptsRewrite :: OptsRewrite -> Bool
$sel:_omitComments:OptsRewrite :: OptsRewrite -> Bool
$sel:_depthSensitive:OptsRewrite :: OptsRewrite -> Bool
$sel:_nonumber:OptsRewrite :: OptsRewrite -> Bool
$sel:_inPlace:OptsRewrite :: OptsRewrite -> Bool
$sel:_update:OptsRewrite :: OptsRewrite -> Bool
$sel:_sequence:OptsRewrite :: OptsRewrite -> Bool
$sel:_headers:OptsRewrite :: OptsRewrite -> Bool
$sel:_canonize:OptsRewrite :: OptsRewrite -> Bool
$sel:_compress:OptsRewrite :: OptsRewrite -> Bool
$sel:_maxDepth:OptsRewrite :: OptsRewrite -> Int
$sel:_maxCycles:OptsRewrite :: OptsRewrite -> Int
$sel:_margin:OptsRewrite :: OptsRewrite -> Int
$sel:_meetPopularity:OptsRewrite :: OptsRewrite -> Maybe Int
$sel:_meetLength:OptsRewrite :: OptsRewrite -> Maybe Int
$sel:_rules:OptsRewrite :: OptsRewrite -> [FilePath]
$sel:_hide:OptsRewrite :: OptsRewrite -> [FilePath]
$sel:_show:OptsRewrite :: OptsRewrite -> [FilePath]
$sel:_locator:OptsRewrite :: OptsRewrite -> FilePath
$sel:_focus:OptsRewrite :: OptsRewrite -> FilePath
$sel:_expression:OptsRewrite :: OptsRewrite -> Maybe FilePath
$sel:_label:OptsRewrite :: OptsRewrite -> Maybe FilePath
$sel:_meetPrefix:OptsRewrite :: OptsRewrite -> Maybe FilePath
$sel:_breakpoint:OptsRewrite :: OptsRewrite -> Maybe FilePath
$sel:_targetFile:OptsRewrite :: OptsRewrite -> Maybe FilePath
$sel:_stepsDir:OptsRewrite :: OptsRewrite -> Maybe FilePath
$sel:_inputFile:OptsRewrite :: OptsRewrite -> Maybe FilePath
..} = do
  IO ()
validateOpts
  IO ()
checkUpdate
  [Expression]
excluded <- FilePath -> [FilePath] -> IO [Expression]
validatedDispatches FilePath
"hide" [FilePath]
_hide
  [Expression]
included <- FilePath -> [FilePath] -> IO [Expression]
validatedDispatches FilePath
"show" [FilePath]
_show
  [Expression
loc] <- FilePath -> [FilePath] -> IO [Expression]
validatedDispatches FilePath
"locator" [FilePath
_locator]
  [Expression
foc] <- FilePath -> [FilePath] -> IO [Expression]
validatedDispatches FilePath
"focus" [FilePath
_focus]
  FilePath -> [Expression] -> FilePath -> [Expression] -> IO ()
validateNoOverlap FilePath
"show" [Expression]
included FilePath
"hide" [Expression]
excluded
  StdGen -> IO ()
forall (m :: * -> *). MonadIO m => StdGen -> m ()
setStdGen (Int -> StdGen
mkStdGen Int
_seed)
  [Rule]
rules <- Bool -> Bool -> [FilePath] -> IO [Rule]
getRules Bool
_normalize Bool
_shuffle [FilePath]
_rules
  Engine
linked <- IO Engine
engine
  Maybe FilePath -> [Rule] -> IO ()
validateBreakpoint Maybe FilePath
_breakpoint [Rule]
rules
  FilePath
input <- Maybe FilePath -> IO FilePath
readInput Maybe FilePath
_inputFile
  (Expression
expr, Atoms
atoms) <- FilePath -> IOFormat -> Form -> IO (Expression, Atoms)
parseInputWithAtoms FilePath
input IOFormat
_inputFormat Form
_monoform
  IOFormat -> Expression -> IO ()
validateXmirTopLevel IOFormat
_outputFormat Expression
expr
  Expression -> IO ()
seedTaus Expression
expr
  FilePath -> IO ()
logDebug (FilePath -> Int -> Int -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"Amount of rewriting cycles across all the rules: %d, per rule: %d" Int
_maxCycles Int
_maxDepth)
  let listing :: Expression -> FilePath
listing = case ([Rule]
rules, IOFormat
_inputFormat) of
        ([], IOFormat
PHI) -> (\Expression
_ -> FilePath -> FilePath
escapeXMLText FilePath
input)
        ([Rule]
_, IOFormat
_) -> (\Expression
rewritten -> FilePath -> FilePath
escapeXMLText (Expression -> PrintConfig -> FilePath
P.printExpression' Expression
rewritten (SugarType
_sugarType, Encoding
UNICODE, LineFormat
_flat, Int
_margin)))
      xmirCtx :: XmirContext
xmirCtx = Bool
-> Bool -> Bool -> (Expression -> FilePath) -> Atoms -> XmirContext
XmirContext Bool
_omitListing Bool
_omitComments Bool
_hideRho Expression -> FilePath
listing Atoms
atoms
      printCtx :: PrintContext
printCtx = XmirContext -> Expression -> PrintContext
toPrintCtx XmirContext
xmirCtx Expression
foc
      exclude :: [Rewritten] -> IO [Rewritten]
exclude = ([Rewritten] -> [Expression] -> IO [Rewritten]
`F.exclude` [Expression]
excluded)
      include :: [Rewritten] -> IO [Rewritten]
include = ([Rewritten] -> [Expression] -> IO [Rewritten]
`F.include` [Expression]
included)
  Expression -> IO ()
save <- Maybe FilePath
-> PrintContext
-> [Expression]
-> [Expression]
-> IO (Expression -> IO ())
saveStepFunc Maybe FilePath
_stepsDir PrintContext
printCtx [Expression]
included [Expression]
excluded
  let steps :: [Step]
steps = (Rule -> Step) -> [Rule] -> [Step]
forall a b. (a -> b) -> [a] -> [b]
map (Engine -> Rule -> Step
stepOf Engine
linked) [Rule]
rules
  (NonEmpty Rewritten
rewrittens, Bool
exceeded) <- Expression
-> [Step] -> RewriteContext -> IO (NonEmpty Rewritten, Bool)
rewrite Expression
expr [Step]
steps (Expression
-> Int
-> Int
-> Bool
-> Maybe Expression
-> BuildTermFunc
-> (Expression -> Bool)
-> (Maybe Expression -> Expression -> Set Int)
-> Must
-> Maybe FilePath
-> (Expression -> IO ())
-> SaveMadeFunc
-> RewriteContext
RewriteContext Expression
loc Int
_maxDepth Int
_maxCycles Bool
_depthSensitive Maybe Expression
forall a. Maybe a
Nothing (Engine -> BuildTermFunc
building Engine
linked) Engine
linked._normal ([Step] -> Maybe Expression -> Expression -> Set Int
every [Step]
steps) Must
_must Maybe FilePath
_breakpoint Expression -> IO ()
save SaveMadeFunc
dontSaveMade)
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Maybe FilePath -> Bool
forall a. Maybe a -> Bool
isJust Maybe FilePath
_breakpoint Bool -> Bool -> Bool
&& NonEmpty Rewritten -> Int
forall a. NonEmpty a -> Int
NE.length NonEmpty Rewritten
rewrittens Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1) (Maybe FilePath -> IO ()
clearedStepsDir Maybe FilePath
_stepsDir)
  [Rewritten]
rewrittens' <- [Rewritten] -> IO [Rewritten]
exclude (if Bool
_sequence then NonEmpty Rewritten -> [Rewritten]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty Rewritten
rewrittens else [NonEmpty Rewritten -> Rewritten
forall a. NonEmpty a -> a
NE.last NonEmpty Rewritten
rewrittens]) IO [Rewritten] -> ([Rewritten] -> IO [Rewritten]) -> IO [Rewritten]
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Rewritten] -> IO [Rewritten]
include
  FilePath -> IO ()
logDebug (FilePath -> FilePath -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"Printing rewritten 𝜑-expression as %s" (IOFormat -> FilePath
forall a. Show a => a -> FilePath
show IOFormat
_outputFormat))
  FilePath
exprs <- PrintContext -> Rewrittens' -> IO FilePath
printRewrittens PrintContext
printCtx ([Rewritten]
rewrittens', Bool
exceeded)
  Maybe FilePath -> FilePath -> IO ()
output Maybe FilePath
_targetFile FilePath
exprs
  where
    validateOpts :: IO ()
    validateOpts :: IO ()
validateOpts = do
      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) (FilePath -> IO ()
forall a. FilePath -> IO a
invalidCLIArguments FilePath
"The option --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) (FilePath -> IO ()
forall a. FilePath -> IO a
invalidCLIArguments FilePath
"The options --in-place and --target cannot be used together")
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
_inPlace Bool -> Bool -> Bool
&& IOFormat
_outputFormat IOFormat -> IOFormat -> Bool
forall a. Eq a => a -> a -> Bool
/= IOFormat
_inputFormat) (FilePath -> IO ()
forall a. FilePath -> IO a
invalidCLIArguments FilePath
"The option --in-place requires the output format to match the input format")
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
_inPlace Bool -> Bool -> Bool
&& Bool
_sequence) (FilePath -> IO ()
forall a. FilePath -> IO a
invalidCLIArguments FilePath
"The options --in-place and --sequence cannot be used together, since the file must keep one program")
      Expression
focusedExpr <- FilePath -> IO Expression
parseExpressionThrows FilePath
_focus
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
_inPlace Bool -> Bool -> Bool
&& Expression
focusedExpr Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
/= Expression
ExRoot) (FilePath -> IO ()
forall a. FilePath -> IO a
invalidCLIArguments FilePath
"The options --in-place and --focus cannot be used together, since the file must keep the whole program")
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
_inPlace Bool -> Bool -> Bool
&& Bool -> Bool
not ([FilePath] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FilePath]
_show)) (FilePath -> IO ()
forall a. FilePath -> IO a
invalidCLIArguments FilePath
"The options --in-place and --show cannot be used together, since the file must keep the whole program")
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
_inPlace Bool -> Bool -> Bool
&& Bool -> Bool
not ([FilePath] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FilePath]
_hide)) (FilePath -> IO ()
forall a. FilePath -> IO a
invalidCLIArguments FilePath
"The options --in-place and --hide cannot be used together, since the file must keep the whole program")
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
_inPlace Bool -> Bool -> Bool
&& Bool
_hideRho) (FilePath -> IO ()
forall a. FilePath -> IO a
invalidCLIArguments FilePath
"The options --in-place and --hide-rho cannot be used together, since the file must keep the whole program")
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
_update Bool -> Bool -> Bool
&& Bool
_inPlace) (FilePath -> IO ()
forall a. FilePath -> IO a
invalidCLIArguments FilePath
"The options --update and --in-place cannot be used together")
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
_update Bool -> Bool -> Bool
&& Maybe FilePath -> Bool
forall a. Maybe a -> Bool
isNothing Maybe FilePath
_targetFile) (FilePath -> IO ()
forall a. FilePath -> IO a
invalidCLIArguments FilePath
"The option --update requires --target")
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
_update Bool -> Bool -> Bool
&& Maybe FilePath -> Bool
forall a. Maybe a -> Bool
isNothing Maybe FilePath
_inputFile) (FilePath -> IO ()
forall a. FilePath -> IO a
invalidCLIArguments FilePath
"The option --update requires an input file")
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([FilePath] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [FilePath]
_show Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1) (FilePath -> IO ()
forall a. FilePath -> IO a
invalidCLIArguments FilePath
"The option --show can be used only once")
      IOFormat
-> [(Bool, FilePath)]
-> [(Maybe FilePath, FilePath)]
-> [(Maybe Int, FilePath)]
-> IO ()
validateLatexOptions
        IOFormat
_outputFormat
        [(Bool
_nonumber, FilePath
"nonumber"), (Bool
_compress, FilePath
"compress")]
        [(Maybe FilePath
_expression, FilePath
"expression"), (Maybe FilePath
_label, FilePath
"label"), (Maybe FilePath
_meetPrefix, FilePath
"meet-prefix")]
        [(Maybe Int
_meetPopularity, FilePath
"meet-popularity"), (Maybe Int
_meetLength, FilePath
"meet-length")]
      Must -> IO ()
validateMust' Must
_must
      IOFormat -> [(Bool, FilePath)] -> FilePath -> IO ()
validateXmirOptions IOFormat
_outputFormat [(Bool
_omitListing, FilePath
"omit-listing"), (Bool
_omitComments, FilePath
"omit-comments")] FilePath
_focus
    checkUpdate :: IO ()
    checkUpdate :: IO ()
checkUpdate = case (Bool
_update, Maybe FilePath
_inputFile, Maybe FilePath
_targetFile) of
      (Bool
True, Just FilePath
src, Just FilePath
tgt) -> do
        Bool
exists <- FilePath -> IO Bool
doesFileExist FilePath
tgt
        Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
exists (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
          Bool
newer <- UTCTime -> UTCTime -> Bool
forall a. Ord a => a -> a -> Bool
(>) (UTCTime -> UTCTime -> Bool) -> IO UTCTime -> IO (UTCTime -> Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FilePath -> IO UTCTime
getModificationTime FilePath
tgt IO (UTCTime -> Bool) -> IO UTCTime -> IO Bool
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> FilePath -> IO UTCTime
getModificationTime FilePath
src
          Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
newer (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
            FilePath -> IO ()
logDebug (FilePath -> FilePath -> FilePath -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"Target '%s' is newer than source '%s', skipping rewriting (--update)" FilePath
tgt FilePath
src)
            IO ()
forall a. IO a
exitSuccess
      (Bool, Maybe FilePath, Maybe FilePath)
_ -> () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    validateBreakpoint :: Maybe String -> [Y.Rule] -> IO ()
    validateBreakpoint :: Maybe FilePath -> [Rule] -> IO ()
validateBreakpoint Maybe FilePath
Nothing [Rule]
_ = () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    validateBreakpoint (Just FilePath
rule) [Rule]
rules =
      let names :: [FilePath]
names = (Rule -> FilePath) -> [Rule] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (.name) [Rule]
rules
       in Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless
            (FilePath
rule FilePath -> [FilePath] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FilePath]
names)
            (FilePath -> IO ()
forall a. FilePath -> IO a
invalidCLIArguments (FilePath -> FilePath -> FilePath -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"The rule '%s' provided in '--breakpoint' option is absent across given rewriting rules: %s" FilePath
rule (FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate FilePath
", " [FilePath]
names)))
    output :: Maybe FilePath -> String -> IO ()
    output :: Maybe FilePath -> FilePath -> IO ()
output Maybe FilePath
target FilePath
expr = 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 ()
overwrite FilePath
file (FilePath
expr FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"\n")
        FilePath -> IO ()
logDebug (FilePath -> FilePath -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"The file '%s' was modified in-place" FilePath
file)
      (Bool
True, Maybe FilePath
_, Maybe FilePath
Nothing) ->
        FilePath -> IO ()
forall a. HasCallStack => FilePath -> a
error FilePath
"The option --in-place requires an input 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 ()
overwrite FilePath
file (FilePath
expr FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"\n")
        FilePath -> IO ()
logDebug (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
expr
    toPrintCtx :: XmirContext -> Expression -> PrintContext
    toPrintCtx :: XmirContext -> Expression -> PrintContext
toPrintCtx XmirContext
xmirCtx Expression
focus =
      SugarType
-> Bool
-> Maybe Int
-> Bool
-> LineFormat
-> Int
-> XmirContext
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Int
-> Int
-> Expression
-> Maybe FilePath
-> Maybe FilePath
-> Maybe FilePath
-> IOFormat
-> PrintContext
PrintCtx
        SugarType
_sugarType
        Bool
_hideRho
        Maybe Int
forall a. Maybe a
Nothing
        Bool
False
        LineFormat
_flat
        Int
_margin
        XmirContext
xmirCtx
        Bool
_nonumber
        Bool
_compress
        Bool
_canonize
        Bool
_sequence
        Bool
_headers
        (Maybe Int -> Int
justMeetPopularity Maybe Int
_meetPopularity)
        (Maybe Int -> Int
justMeetLength Maybe Int
_meetLength)
        Expression
focus
        Maybe FilePath
_expression
        Maybe FilePath
_label
        Maybe FilePath
_meetPrefix
        IOFormat
_outputFormat

runDataize :: [String] -> OptsDataize -> IO ()
runDataize :: [FilePath] -> OptsDataize -> IO ()
runDataize [FilePath]
args OptsDataize{Bool
Int
FilePath
[FilePath]
Maybe Int
Maybe FilePath
Maybe Acyclic
LogLevel
Form
SugarType
LineFormat
IOFormat
_logLevel :: LogLevel
_logLines :: Int
_inputFormat :: IOFormat
_monoform :: Form
_outputFormat :: IOFormat
_sugarType :: SugarType
_hideRho :: Bool
_flat :: LineFormat
_omitListing :: Bool
_omitComments :: Bool
_nonumber :: Bool
_sequence :: Bool
_headers :: Bool
_canonize :: Bool
_depthSensitive :: Bool
_shuffle :: Bool
_seed :: Int
_quiet :: Bool
_partial :: Bool
_acyclic :: Maybe Acyclic
_maxLoops :: Int
_compress :: Bool
_maxDepth :: Int
_maxCycles :: Int
_maxSteps :: Int
_maxFirings :: Maybe Int
_maxSeconds :: Maybe Int
_margin :: Int
_meetPopularity :: Maybe Int
_meetLength :: Maybe Int
_hide :: [FilePath]
_show :: [FilePath]
_locator :: FilePath
_focus :: FilePath
_expression :: Maybe FilePath
_label :: Maybe FilePath
_meetPrefix :: Maybe FilePath
_inside :: Maybe FilePath
_stepsDir :: Maybe FilePath
_protocol :: Maybe FilePath
_abridged :: Maybe Int
_abridgedData :: Bool
_symbolic :: Maybe FilePath
_inputFile :: Maybe FilePath
$sel:_logLevel:OptsDataize :: OptsDataize -> LogLevel
$sel:_logLines:OptsDataize :: OptsDataize -> Int
$sel:_inputFormat:OptsDataize :: OptsDataize -> IOFormat
$sel:_monoform:OptsDataize :: OptsDataize -> Form
$sel:_outputFormat:OptsDataize :: OptsDataize -> IOFormat
$sel:_sugarType:OptsDataize :: OptsDataize -> SugarType
$sel:_hideRho:OptsDataize :: OptsDataize -> Bool
$sel:_flat:OptsDataize :: OptsDataize -> LineFormat
$sel:_omitListing:OptsDataize :: OptsDataize -> Bool
$sel:_omitComments:OptsDataize :: OptsDataize -> Bool
$sel:_nonumber:OptsDataize :: OptsDataize -> Bool
$sel:_sequence:OptsDataize :: OptsDataize -> Bool
$sel:_headers:OptsDataize :: OptsDataize -> Bool
$sel:_canonize:OptsDataize :: OptsDataize -> Bool
$sel:_depthSensitive:OptsDataize :: OptsDataize -> Bool
$sel:_shuffle:OptsDataize :: OptsDataize -> Bool
$sel:_seed:OptsDataize :: OptsDataize -> Int
$sel:_quiet:OptsDataize :: OptsDataize -> Bool
$sel:_partial:OptsDataize :: OptsDataize -> Bool
$sel:_acyclic:OptsDataize :: OptsDataize -> Maybe Acyclic
$sel:_maxLoops:OptsDataize :: OptsDataize -> Int
$sel:_compress:OptsDataize :: OptsDataize -> Bool
$sel:_maxDepth:OptsDataize :: OptsDataize -> Int
$sel:_maxCycles:OptsDataize :: OptsDataize -> Int
$sel:_maxSteps:OptsDataize :: OptsDataize -> Int
$sel:_maxFirings:OptsDataize :: OptsDataize -> Maybe Int
$sel:_maxSeconds:OptsDataize :: OptsDataize -> Maybe Int
$sel:_margin:OptsDataize :: OptsDataize -> Int
$sel:_meetPopularity:OptsDataize :: OptsDataize -> Maybe Int
$sel:_meetLength:OptsDataize :: OptsDataize -> Maybe Int
$sel:_hide:OptsDataize :: OptsDataize -> [FilePath]
$sel:_show:OptsDataize :: OptsDataize -> [FilePath]
$sel:_locator:OptsDataize :: OptsDataize -> FilePath
$sel:_focus:OptsDataize :: OptsDataize -> FilePath
$sel:_expression:OptsDataize :: OptsDataize -> Maybe FilePath
$sel:_label:OptsDataize :: OptsDataize -> Maybe FilePath
$sel:_meetPrefix:OptsDataize :: OptsDataize -> Maybe FilePath
$sel:_inside:OptsDataize :: OptsDataize -> Maybe FilePath
$sel:_stepsDir:OptsDataize :: OptsDataize -> Maybe FilePath
$sel:_protocol:OptsDataize :: OptsDataize -> Maybe FilePath
$sel:_abridged:OptsDataize :: OptsDataize -> Maybe Int
$sel:_abridgedData:OptsDataize :: OptsDataize -> Bool
$sel:_symbolic:OptsDataize :: OptsDataize -> Maybe FilePath
$sel:_inputFile:OptsDataize :: OptsDataize -> Maybe FilePath
..} = do
  IO ()
validateOpts
  Maybe Deadline
deadline <- Maybe Int -> IO (Maybe Deadline)
timed Maybe Int
_maxSeconds
  Lambdas
lambdas <- Maybe FilePath -> IO Lambdas
lambdasOf Maybe FilePath
_symbolic
  [Expression]
excluded <- FilePath -> [FilePath] -> IO [Expression]
validatedDispatches FilePath
"hide" [FilePath]
_hide
  [Expression]
included <- FilePath -> [FilePath] -> IO [Expression]
validatedDispatches FilePath
"show" [FilePath]
_show
  [Expression
loc] <- FilePath -> [FilePath] -> IO [Expression]
validatedDispatches FilePath
"locator" [FilePath
_locator]
  [Expression
foc] <- FilePath -> [FilePath] -> IO [Expression]
validatedDispatches FilePath
"focus" [FilePath
_focus]
  FilePath -> [Expression] -> FilePath -> [Expression] -> IO ()
validateNoOverlap FilePath
"show" [Expression]
included FilePath
"hide" [Expression]
excluded
  FilePath
input <- Maybe FilePath -> IO FilePath
readInput Maybe FilePath
_inputFile
  (Expression
expr, Atoms
atoms) <- FilePath -> IOFormat -> Form -> IO (Expression, Atoms)
parseInputWithAtoms FilePath
input IOFormat
_inputFormat Form
_monoform
  StdGen -> IO ()
forall (m :: * -> *). MonadIO m => StdGen -> m ()
setStdGen (Int -> StdGen
mkStdGen Int
_seed)
  Expression -> IO ()
seedTaus Expression
expr
  let printCtx :: PrintContext
printCtx = Atoms -> Expression -> PrintContext
toPrintCtx Atoms
atoms Expression
foc
      exclude :: [Rewritten] -> IO [Rewritten]
exclude = ([Rewritten] -> [Expression] -> IO [Rewritten]
`F.exclude` [Expression]
excluded)
      include :: [Rewritten] -> IO [Rewritten]
include = ([Rewritten] -> [Expression] -> IO [Rewritten]
`F.include` [Expression]
included)
  Expression -> IO ()
save <- Maybe FilePath
-> PrintContext
-> [Expression]
-> [Expression]
-> IO (Expression -> IO ())
saveStepFunc Maybe FilePath
_stepsDir PrintContext
printCtx [Expression]
included [Expression]
excluded
  Maybe Tally
tally <- Maybe Int -> IO (Maybe Tally)
tallied Maybe Int
_maxFirings
  IORef Int
minted <- Int -> IO (IORef Int)
forall a. a -> IO (IORef a)
newIORef Int
0
  Maybe Memo
memo <- Maybe Acyclic -> IO (Maybe Memo)
memoized Maybe Acyclic
_acyclic
  Engine
linked <- IO Engine
engine
  Header
header <- [FilePath]
-> Maybe FilePath
-> FilePath
-> Expression
-> Maybe FilePath
-> Lambdas
-> IO Header
headerOf [FilePath]
args Maybe FilePath
_inputFile FilePath
input Expression
expr Maybe FilePath
_symbolic Lambdas
lambdas
  ((Outcome
outcome, [Rewritten]
chain, State
_), Expression
universe, Expression
aim) <-
    Maybe FilePath
-> PrintContext
-> (SaveEvalFunc
    -> IO ((Outcome, [Rewritten], State), Expression, Expression))
-> IO ((Outcome, [Rewritten], State), Expression, Expression)
forall a.
Maybe FilePath -> PrintContext -> (SaveEvalFunc -> IO a) -> IO a
withEvalFunc
      Maybe FilePath
_protocol
      PrintContext
printCtx
      ( \SaveEvalFunc
record -> do
          let ctx :: ReduceContext
ctx = Expression
-> Expression
-> Maybe Expression
-> Int
-> Int
-> Steps
-> Maybe Tally
-> IORef Int
-> Maybe Deadline
-> Maybe Memo
-> Int
-> Maybe (Int, Judgment, Expression)
-> Bool
-> Bool
-> Bool
-> Maybe Acyclic
-> Int
-> Judgment
-> [Text]
-> Seen
-> Maybe (Expression, [Binding], Expression)
-> Lambdas
-> BuildTermFunc
-> ReductionFunc
-> EvaluationFunc
-> (Expression -> IO ())
-> SaveEvalFunc
-> Engine
-> ReduceContext
ReduceContext Expression
loc Expression
loc Maybe Expression
forall a. Maybe a
Nothing Int
_maxDepth Int
_maxCycles (Int -> Int -> Steps
Steps Int
_maxSteps Int
0) Maybe Tally
tally IORef Int
minted Maybe Deadline
deadline Maybe Memo
memo Int
1 ((Int, Judgment, Expression) -> Maybe (Int, Judgment, Expression)
forall a. a -> Maybe a
Just (Int
1, Judgment
Dataization, Expression
loc)) Bool
_depthSensitive Bool
_shuffle Bool
_partial Maybe Acyclic
_acyclic Int
_maxLoops Judgment
Dataization [] Seen
forall k a. Map k a
Map.empty Maybe (Expression, [Binding], Expression)
forall a. Maybe a
Nothing Lambdas
lambdas (Engine -> BuildTermFunc
building Engine
linked) ReductionFunc
reduction EvaluationFunc
evaluation Expression -> IO ()
save SaveEvalFunc
record Engine
linked
          (Expression
universe, ReduceContext
aiming) <- PrintContext
-> Judgment
-> Header
-> Maybe FilePath
-> Expression
-> ReduceContext
-> IO (Expression, ReduceContext)
aimed PrintContext
printCtx Judgment
Dataization Header
header Maybe FilePath
_inside Expression
expr ReduceContext
ctx
          Expression -> ReduceContext -> IO ()
started Expression
universe ReduceContext
aiming
          (,Expression
universe,ReduceContext
aiming._locator) ((Outcome, [Rewritten], State)
 -> ((Outcome, [Rewritten], State), Expression, Expression))
-> IO (Outcome, [Rewritten], State)
-> IO ((Outcome, [Rewritten], State), Expression, Expression)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression
-> State -> ReduceContext -> IO (Outcome, [Rewritten], State)
dataize Expression
universe State
emptyState ReduceContext
aiming
      )
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
_sequence ([Rewritten] -> IO [Rewritten]
exclude [Rewritten]
chain IO [Rewritten] -> ([Rewritten] -> IO [Rewritten]) -> IO [Rewritten]
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Rewritten] -> IO [Rewritten]
include IO [Rewritten] -> ([Rewritten] -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \[Rewritten]
shown -> PrintContext -> Rewrittens' -> IO FilePath
printRewrittens PrintContext
printCtx ([Rewritten]
shown, Bool
False) IO FilePath -> (FilePath -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= FilePath -> IO ()
putStrLn)
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
_quiet (PrintContext
-> (Expression -> IO Expression) -> Outcome -> IO FilePath
printOutcome PrintContext
printCtx (Expression
-> Expression
-> [Expression]
-> [Expression]
-> Expression
-> IO Expression
filteredAt Expression
aim Expression
universe [Expression]
excluded [Expression]
included) Outcome
outcome IO FilePath -> (FilePath -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= FilePath -> IO ()
putStrLn)
  where
    printOutcome :: PrintContext -> (Expression -> IO Expression) -> Outcome -> IO String
    printOutcome :: PrintContext
-> (Expression -> IO Expression) -> Outcome -> IO FilePath
printOutcome PrintContext
_ Expression -> IO Expression
_ (Dataized Bytes
bytes) = FilePath -> IO FilePath
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bytes -> FilePath
P.printBytes Bytes
bytes)
    printOutcome PrintContext
ctx Expression -> IO Expression
narrowed (Residual Expression
residue) = do
      FilePath -> IO ()
logDebug FilePath
"Dataization got stuck on a λ function that cannot fire, printing the residual program (--partial)"
      Expression
answer <- Expression -> IO Expression
narrowed Expression
residue
      IOFormat -> Expression -> IO ()
validateXmirTopLevel IOFormat
_outputFormat Expression
answer
      PrintContext -> Expression -> IO FilePath
printAnswer PrintContext
ctx Expression
answer
    validateOpts :: IO ()
    validateOpts :: IO ()
validateOpts = do
      IOFormat
-> [(Bool, FilePath)]
-> [(Maybe FilePath, FilePath)]
-> [(Maybe Int, FilePath)]
-> IO ()
validateLatexOptions
        IOFormat
_outputFormat
        [(Bool
_nonumber, FilePath
"nonumber"), (Bool
_compress, FilePath
"compress")]
        [(Maybe FilePath
_expression, FilePath
"expression"), (Maybe FilePath
_label, FilePath
"label"), (Maybe FilePath
_meetPrefix, FilePath
"meet-prefix")]
        [(Maybe Int
_meetPopularity, FilePath
"meet-popularity"), (Maybe Int
_meetLength, FilePath
"meet-length")]
      IOFormat -> [(Bool, FilePath)] -> FilePath -> IO ()
validateXmirOptions IOFormat
_outputFormat [(Bool
_omitListing, FilePath
"omit-listing"), (Bool
_omitComments, FilePath
"omit-comments")] FilePath
_focus
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([FilePath] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [FilePath]
_show Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1) (FilePath -> IO ()
forall a. FilePath -> IO a
invalidCLIArguments FilePath
"The option --show can be used only once")
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Maybe Int -> Bool
forall a. Maybe a -> Bool
isJust Maybe Int
_abridged Bool -> Bool -> Bool
&& Maybe FilePath -> Bool
forall a. Maybe a -> Bool
isNothing Maybe FilePath
_protocol) (FilePath -> IO ()
forall a. FilePath -> IO a
invalidCLIArguments FilePath
"The option --abridged requires --protocol, since only the protocol is abridged")
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
_abridgedData Bool -> Bool -> Bool
&& Maybe Int -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Int
_abridged) (FilePath -> IO ()
forall a. FilePath -> IO a
invalidCLIArguments FilePath
"The option --abridged-data requires --abridged, since only an abridged protocol cuts its data")
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
_maxLoops Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 Bool -> Bool -> Bool
&& Maybe Acyclic -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Acyclic
_acyclic) (FilePath -> IO ()
forall a. FilePath -> IO a
invalidCLIArguments FilePath
"The option --max-loops requires --acyclic, since only --acyclic cuts a loop")
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Maybe FilePath -> Bool
forall a. Maybe a -> Bool
isJust Maybe FilePath
_inside) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
        Expression
parsed <- FilePath -> IO Expression
parseExpressionThrows FilePath
_locator
        Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when
          (Expression
parsed Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
/= Expression
ExRoot)
          (FilePath -> IO ()
forall a. FilePath -> IO a
invalidCLIArguments FilePath
"The options --inside and --locator cannot be used together, since --inside aims the run at the binding it mints")
    toPrintCtx :: Atoms -> Expression -> PrintContext
    toPrintCtx :: Atoms -> Expression -> PrintContext
toPrintCtx Atoms
atoms Expression
focus =
      SugarType
-> Bool
-> Maybe Int
-> Bool
-> LineFormat
-> Int
-> XmirContext
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Int
-> Int
-> Expression
-> Maybe FilePath
-> Maybe FilePath
-> Maybe FilePath
-> IOFormat
-> PrintContext
PrintCtx
        SugarType
_sugarType
        Bool
_hideRho
        Maybe Int
_abridged
        Bool
_abridgedData
        LineFormat
_flat
        Int
_margin
        (Bool
-> Bool -> Bool -> (Expression -> FilePath) -> Atoms -> XmirContext
XmirContext Bool
_omitListing Bool
_omitComments Bool
_hideRho Expression -> FilePath
listing Atoms
atoms)
        Bool
_nonumber
        Bool
_compress
        Bool
_canonize
        Bool
_sequence
        Bool
_headers
        (Maybe Int -> Int
justMeetPopularity Maybe Int
_meetPopularity)
        (Maybe Int -> Int
justMeetLength Maybe Int
_meetLength)
        Expression
focus
        Maybe FilePath
_expression
        Maybe FilePath
_label
        Maybe FilePath
_meetPrefix
        IOFormat
_outputFormat
    listing :: Expression -> String
    listing :: Expression -> FilePath
listing Expression
e = FilePath -> FilePath
escapeXMLText (Expression -> PrintConfig -> FilePath
P.printExpression' Expression
e (SugarType
_sugarType, Encoding
UNICODE, LineFormat
_flat, Int
_margin))

runMorph :: [String] -> OptsMorph -> IO ()
runMorph :: [FilePath] -> OptsMorph -> IO ()
runMorph [FilePath]
args OptsMorph{Bool
Int
FilePath
[FilePath]
Maybe Int
Maybe FilePath
Maybe Acyclic
LogLevel
Form
SugarType
LineFormat
IOFormat
_logLevel :: LogLevel
_logLines :: Int
_inputFormat :: IOFormat
_monoform :: Form
_outputFormat :: IOFormat
_sugarType :: SugarType
_hideRho :: Bool
_flat :: LineFormat
_omitListing :: Bool
_omitComments :: Bool
_nonumber :: Bool
_sequence :: Bool
_headers :: Bool
_canonize :: Bool
_depthSensitive :: Bool
_shuffle :: Bool
_seed :: Int
_quiet :: Bool
_partial :: Bool
_acyclic :: Maybe Acyclic
_maxLoops :: Int
_compress :: Bool
_maxDepth :: Int
_maxCycles :: Int
_maxSteps :: Int
_maxFirings :: Maybe Int
_maxSeconds :: Maybe Int
_margin :: Int
_meetPopularity :: Maybe Int
_meetLength :: Maybe Int
_hide :: [FilePath]
_show :: [FilePath]
_locator :: FilePath
_focus :: FilePath
_expression :: Maybe FilePath
_label :: Maybe FilePath
_meetPrefix :: Maybe FilePath
_inside :: Maybe FilePath
_stepsDir :: Maybe FilePath
_protocol :: Maybe FilePath
_abridged :: Maybe Int
_abridgedData :: Bool
_symbolic :: Maybe FilePath
_inputFile :: Maybe FilePath
$sel:_logLevel:OptsMorph :: OptsMorph -> LogLevel
$sel:_logLines:OptsMorph :: OptsMorph -> Int
$sel:_inputFormat:OptsMorph :: OptsMorph -> IOFormat
$sel:_monoform:OptsMorph :: OptsMorph -> Form
$sel:_outputFormat:OptsMorph :: OptsMorph -> IOFormat
$sel:_sugarType:OptsMorph :: OptsMorph -> SugarType
$sel:_hideRho:OptsMorph :: OptsMorph -> Bool
$sel:_flat:OptsMorph :: OptsMorph -> LineFormat
$sel:_omitListing:OptsMorph :: OptsMorph -> Bool
$sel:_omitComments:OptsMorph :: OptsMorph -> Bool
$sel:_nonumber:OptsMorph :: OptsMorph -> Bool
$sel:_sequence:OptsMorph :: OptsMorph -> Bool
$sel:_headers:OptsMorph :: OptsMorph -> Bool
$sel:_canonize:OptsMorph :: OptsMorph -> Bool
$sel:_depthSensitive:OptsMorph :: OptsMorph -> Bool
$sel:_shuffle:OptsMorph :: OptsMorph -> Bool
$sel:_seed:OptsMorph :: OptsMorph -> Int
$sel:_quiet:OptsMorph :: OptsMorph -> Bool
$sel:_partial:OptsMorph :: OptsMorph -> Bool
$sel:_acyclic:OptsMorph :: OptsMorph -> Maybe Acyclic
$sel:_maxLoops:OptsMorph :: OptsMorph -> Int
$sel:_compress:OptsMorph :: OptsMorph -> Bool
$sel:_maxDepth:OptsMorph :: OptsMorph -> Int
$sel:_maxCycles:OptsMorph :: OptsMorph -> Int
$sel:_maxSteps:OptsMorph :: OptsMorph -> Int
$sel:_maxFirings:OptsMorph :: OptsMorph -> Maybe Int
$sel:_maxSeconds:OptsMorph :: OptsMorph -> Maybe Int
$sel:_margin:OptsMorph :: OptsMorph -> Int
$sel:_meetPopularity:OptsMorph :: OptsMorph -> Maybe Int
$sel:_meetLength:OptsMorph :: OptsMorph -> Maybe Int
$sel:_hide:OptsMorph :: OptsMorph -> [FilePath]
$sel:_show:OptsMorph :: OptsMorph -> [FilePath]
$sel:_locator:OptsMorph :: OptsMorph -> FilePath
$sel:_focus:OptsMorph :: OptsMorph -> FilePath
$sel:_expression:OptsMorph :: OptsMorph -> Maybe FilePath
$sel:_label:OptsMorph :: OptsMorph -> Maybe FilePath
$sel:_meetPrefix:OptsMorph :: OptsMorph -> Maybe FilePath
$sel:_inside:OptsMorph :: OptsMorph -> Maybe FilePath
$sel:_stepsDir:OptsMorph :: OptsMorph -> Maybe FilePath
$sel:_protocol:OptsMorph :: OptsMorph -> Maybe FilePath
$sel:_abridged:OptsMorph :: OptsMorph -> Maybe Int
$sel:_abridgedData:OptsMorph :: OptsMorph -> Bool
$sel:_symbolic:OptsMorph :: OptsMorph -> Maybe FilePath
$sel:_inputFile:OptsMorph :: OptsMorph -> Maybe FilePath
..} = do
  IO ()
validateOpts
  Maybe Deadline
deadline <- Maybe Int -> IO (Maybe Deadline)
timed Maybe Int
_maxSeconds
  Lambdas
lambdas <- Maybe FilePath -> IO Lambdas
lambdasOf Maybe FilePath
_symbolic
  [Expression]
excluded <- FilePath -> [FilePath] -> IO [Expression]
validatedDispatches FilePath
"hide" [FilePath]
_hide
  [Expression]
included <- FilePath -> [FilePath] -> IO [Expression]
validatedDispatches FilePath
"show" [FilePath]
_show
  [Expression
loc] <- FilePath -> [FilePath] -> IO [Expression]
validatedDispatches FilePath
"locator" [FilePath
_locator]
  [Expression
foc] <- FilePath -> [FilePath] -> IO [Expression]
validatedDispatches FilePath
"focus" [FilePath
_focus]
  FilePath -> [Expression] -> FilePath -> [Expression] -> IO ()
validateNoOverlap FilePath
"show" [Expression]
included FilePath
"hide" [Expression]
excluded
  FilePath
input <- Maybe FilePath -> IO FilePath
readInput Maybe FilePath
_inputFile
  (Expression
expr, Atoms
atoms) <- FilePath -> IOFormat -> Form -> IO (Expression, Atoms)
parseInputWithAtoms FilePath
input IOFormat
_inputFormat Form
_monoform
  StdGen -> IO ()
forall (m :: * -> *). MonadIO m => StdGen -> m ()
setStdGen (Int -> StdGen
mkStdGen Int
_seed)
  Expression -> IO ()
seedTaus Expression
expr
  let printCtx :: PrintContext
printCtx = Atoms -> Expression -> PrintContext
toPrintCtx Atoms
atoms Expression
foc
      exclude :: [Rewritten] -> IO [Rewritten]
exclude = ([Rewritten] -> [Expression] -> IO [Rewritten]
`F.exclude` [Expression]
excluded)
      include :: [Rewritten] -> IO [Rewritten]
include = ([Rewritten] -> [Expression] -> IO [Rewritten]
`F.include` [Expression]
included)
  Expression -> IO ()
save <- Maybe FilePath
-> PrintContext
-> [Expression]
-> [Expression]
-> IO (Expression -> IO ())
saveStepFunc Maybe FilePath
_stepsDir PrintContext
printCtx [Expression]
included [Expression]
excluded
  Maybe Tally
tally <- Maybe Int -> IO (Maybe Tally)
tallied Maybe Int
_maxFirings
  IORef Int
minted <- Int -> IO (IORef Int)
forall a. a -> IO (IORef a)
newIORef Int
0
  Maybe Memo
memo <- Maybe Acyclic -> IO (Maybe Memo)
memoized Maybe Acyclic
_acyclic
  Engine
linked <- IO Engine
engine
  Header
header <- [FilePath]
-> Maybe FilePath
-> FilePath
-> Expression
-> Maybe FilePath
-> Lambdas
-> IO Header
headerOf [FilePath]
args Maybe FilePath
_inputFile FilePath
input Expression
expr Maybe FilePath
_symbolic Lambdas
lambdas
  ((Expression
morphed, [Rewritten]
chain, State
_), Expression
universe, Expression
aim) <-
    Maybe FilePath
-> PrintContext
-> (SaveEvalFunc
    -> IO ((Expression, [Rewritten], State), Expression, Expression))
-> IO ((Expression, [Rewritten], State), Expression, Expression)
forall a.
Maybe FilePath -> PrintContext -> (SaveEvalFunc -> IO a) -> IO a
withEvalFunc
      Maybe FilePath
_protocol
      PrintContext
printCtx
      ( \SaveEvalFunc
record -> do
          let ctx :: ReduceContext
ctx = Expression
-> Expression
-> Maybe Expression
-> Int
-> Int
-> Steps
-> Maybe Tally
-> IORef Int
-> Maybe Deadline
-> Maybe Memo
-> Int
-> Maybe (Int, Judgment, Expression)
-> Bool
-> Bool
-> Bool
-> Maybe Acyclic
-> Int
-> Judgment
-> [Text]
-> Seen
-> Maybe (Expression, [Binding], Expression)
-> Lambdas
-> BuildTermFunc
-> ReductionFunc
-> EvaluationFunc
-> (Expression -> IO ())
-> SaveEvalFunc
-> Engine
-> ReduceContext
ReduceContext Expression
loc Expression
loc Maybe Expression
forall a. Maybe a
Nothing Int
_maxDepth Int
_maxCycles (Int -> Int -> Steps
Steps Int
_maxSteps Int
0) Maybe Tally
tally IORef Int
minted Maybe Deadline
deadline Maybe Memo
memo Int
1 ((Int, Judgment, Expression) -> Maybe (Int, Judgment, Expression)
forall a. a -> Maybe a
Just (Int
1, Judgment
Morphing, Expression
loc)) Bool
_depthSensitive Bool
_shuffle Bool
_partial Maybe Acyclic
_acyclic Int
_maxLoops Judgment
Morphing [] Seen
forall k a. Map k a
Map.empty Maybe (Expression, [Binding], Expression)
forall a. Maybe a
Nothing Lambdas
lambdas (Engine -> BuildTermFunc
building Engine
linked) ReductionFunc
reduction EvaluationFunc
evaluation Expression -> IO ()
save SaveEvalFunc
record Engine
linked
          (Expression
universe, ReduceContext
aiming) <- PrintContext
-> Judgment
-> Header
-> Maybe FilePath
-> Expression
-> ReduceContext
-> IO (Expression, ReduceContext)
aimed PrintContext
printCtx Judgment
Morphing Header
header Maybe FilePath
_inside Expression
expr ReduceContext
ctx
          Expression -> ReduceContext -> IO ()
started Expression
universe ReduceContext
aiming
          (,Expression
universe,ReduceContext
aiming._locator) ((Expression, [Rewritten], State)
 -> ((Expression, [Rewritten], State), Expression, Expression))
-> IO (Expression, [Rewritten], State)
-> IO ((Expression, [Rewritten], State), Expression, Expression)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression
-> State -> ReduceContext -> IO (Expression, [Rewritten], State)
morph Expression
universe State
emptyState ReduceContext
aiming
      )
  Maybe FilePath
printed <-
    if Bool
_quiet
      then Maybe FilePath -> IO (Maybe FilePath)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe FilePath
forall a. Maybe a
Nothing
      else do
        Expression
answer <-
          if Expression
foc Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
== Expression
ExRoot
            then Expression
-> Expression
-> [Expression]
-> [Expression]
-> Expression
-> IO Expression
filteredAt Expression
aim Expression
universe [Expression]
excluded [Expression]
included Expression
morphed
            else Expression -> [Expression] -> IO Expression
F.exclude' (Expression
-> (Rewritten -> Expression) -> Maybe Rewritten -> Expression
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Expression
morphed Rewritten -> Expression
forall a b. (a, b) -> a
fst ([Rewritten] -> Maybe Rewritten
forall a. [a] -> Maybe a
lastMaybe [Rewritten]
chain)) [Expression]
excluded IO Expression -> (Expression -> IO Expression) -> IO Expression
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Expression -> [Expression] -> IO Expression
`F.include'` [Expression]
included)
        IOFormat -> Expression -> IO ()
validateXmirTopLevel IOFormat
_outputFormat Expression
answer
        FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just (FilePath -> Maybe FilePath) -> IO FilePath -> IO (Maybe FilePath)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PrintContext -> Expression -> IO FilePath
printAnswer PrintContext
printCtx Expression
answer
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
_sequence ([Rewritten] -> IO [Rewritten]
exclude [Rewritten]
chain IO [Rewritten] -> ([Rewritten] -> IO [Rewritten]) -> IO [Rewritten]
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Rewritten] -> IO [Rewritten]
include IO [Rewritten] -> ([Rewritten] -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \[Rewritten]
shown -> PrintContext -> Rewrittens' -> IO FilePath
printRewrittens PrintContext
printCtx ([Rewritten]
shown, Bool
False) IO FilePath -> (FilePath -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= FilePath -> IO ()
putStrLn)
  (FilePath -> IO ()) -> Maybe FilePath -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ FilePath -> IO ()
putStrLn Maybe FilePath
printed
  where
    lastMaybe :: [a] -> Maybe a
    lastMaybe :: forall a. [a] -> Maybe a
lastMaybe [] = Maybe a
forall a. Maybe a
Nothing
    lastMaybe [a]
items = a -> Maybe a
forall a. a -> Maybe a
Just ([a] -> a
forall a. HasCallStack => [a] -> a
last [a]
items)
    validateOpts :: IO ()
    validateOpts :: IO ()
validateOpts = do
      IOFormat
-> [(Bool, FilePath)]
-> [(Maybe FilePath, FilePath)]
-> [(Maybe Int, FilePath)]
-> IO ()
validateLatexOptions
        IOFormat
_outputFormat
        [(Bool
_nonumber, FilePath
"nonumber"), (Bool
_compress, FilePath
"compress")]
        [(Maybe FilePath
_expression, FilePath
"expression"), (Maybe FilePath
_label, FilePath
"label"), (Maybe FilePath
_meetPrefix, FilePath
"meet-prefix")]
        [(Maybe Int
_meetPopularity, FilePath
"meet-popularity"), (Maybe Int
_meetLength, FilePath
"meet-length")]
      IOFormat -> [(Bool, FilePath)] -> FilePath -> IO ()
validateXmirOptions IOFormat
_outputFormat [(Bool
_omitListing, FilePath
"omit-listing"), (Bool
_omitComments, FilePath
"omit-comments")] FilePath
_focus
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([FilePath] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [FilePath]
_show Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1) (FilePath -> IO ()
forall a. FilePath -> IO a
invalidCLIArguments FilePath
"The option --show can be used only once")
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Maybe Int -> Bool
forall a. Maybe a -> Bool
isJust Maybe Int
_abridged Bool -> Bool -> Bool
&& Maybe FilePath -> Bool
forall a. Maybe a -> Bool
isNothing Maybe FilePath
_protocol) (FilePath -> IO ()
forall a. FilePath -> IO a
invalidCLIArguments FilePath
"The option --abridged requires --protocol, since only the protocol is abridged")
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
_abridgedData Bool -> Bool -> Bool
&& Maybe Int -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Int
_abridged) (FilePath -> IO ()
forall a. FilePath -> IO a
invalidCLIArguments FilePath
"The option --abridged-data requires --abridged, since only an abridged protocol cuts its data")
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
_maxLoops Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 Bool -> Bool -> Bool
&& Maybe Acyclic -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Acyclic
_acyclic) (FilePath -> IO ()
forall a. FilePath -> IO a
invalidCLIArguments FilePath
"The option --max-loops requires --acyclic, since only --acyclic cuts a loop")
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Maybe FilePath -> Bool
forall a. Maybe a -> Bool
isJust Maybe FilePath
_inside) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
        Expression
parsed <- FilePath -> IO Expression
parseExpressionThrows FilePath
_locator
        Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when
          (Expression
parsed Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
/= Expression
ExRoot)
          (FilePath -> IO ()
forall a. FilePath -> IO a
invalidCLIArguments FilePath
"The options --inside and --locator cannot be used together, since --inside aims the run at the binding it mints")
    toPrintCtx :: Atoms -> Expression -> PrintContext
    toPrintCtx :: Atoms -> Expression -> PrintContext
toPrintCtx Atoms
atoms Expression
focus =
      SugarType
-> Bool
-> Maybe Int
-> Bool
-> LineFormat
-> Int
-> XmirContext
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Int
-> Int
-> Expression
-> Maybe FilePath
-> Maybe FilePath
-> Maybe FilePath
-> IOFormat
-> PrintContext
PrintCtx
        SugarType
_sugarType
        Bool
_hideRho
        Maybe Int
_abridged
        Bool
_abridgedData
        LineFormat
_flat
        Int
_margin
        (Bool
-> Bool -> Bool -> (Expression -> FilePath) -> Atoms -> XmirContext
XmirContext Bool
_omitListing Bool
_omitComments Bool
_hideRho Expression -> FilePath
listing Atoms
atoms)
        Bool
_nonumber
        Bool
_compress
        Bool
_canonize
        Bool
_sequence
        Bool
_headers
        (Maybe Int -> Int
justMeetPopularity Maybe Int
_meetPopularity)
        (Maybe Int -> Int
justMeetLength Maybe Int
_meetLength)
        Expression
focus
        Maybe FilePath
_expression
        Maybe FilePath
_label
        Maybe FilePath
_meetPrefix
        IOFormat
_outputFormat
    listing :: Expression -> String
    listing :: Expression -> FilePath
listing Expression
e = FilePath -> FilePath
escapeXMLText (Expression -> PrintConfig -> FilePath
P.printExpression' Expression
e (SugarType
_sugarType, Encoding
UNICODE, LineFormat
_flat, Int
_margin))

runExplain :: OptsExplain -> IO ()
runExplain :: OptsExplain -> IO ()
runExplain OptsExplain{Bool
Int
[FilePath]
Maybe FilePath
LogLevel
_logLevel :: LogLevel
_logLines :: Int
_rules :: [FilePath]
_normalize :: Bool
_morph :: Bool
_dataize :: Bool
_contextualize :: Bool
_shuffle :: Bool
_seed :: Int
_targetFile :: Maybe FilePath
$sel:_logLevel:OptsExplain :: OptsExplain -> LogLevel
$sel:_logLines:OptsExplain :: OptsExplain -> Int
$sel:_rules:OptsExplain :: OptsExplain -> [FilePath]
$sel:_normalize:OptsExplain :: OptsExplain -> Bool
$sel:_morph:OptsExplain :: OptsExplain -> Bool
$sel:_dataize:OptsExplain :: OptsExplain -> Bool
$sel:_contextualize:OptsExplain :: OptsExplain -> Bool
$sel:_shuffle:OptsExplain :: OptsExplain -> Bool
$sel:_seed:OptsExplain :: OptsExplain -> Int
$sel:_targetFile:OptsExplain :: OptsExplain -> Maybe FilePath
..} = do
  StdGen -> IO ()
forall (m :: * -> *). MonadIO m => StdGen -> m ()
setStdGen (Int -> StdGen
mkStdGen Int
_seed)
  IO ()
validateOpts
  IO FilePath
explained IO FilePath -> (FilePath -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Maybe FilePath -> FilePath -> IO ()
printOut Maybe FilePath
_targetFile
  where
    explained :: IO String
    explained :: IO FilePath
explained
      | Bool
_morph = [MorphRule] -> FilePath
explainMorphRules ([MorphRule] -> FilePath) -> IO [MorphRule] -> IO FilePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [MorphRule] -> IO [MorphRule]
forall a. [a] -> IO [a]
shuffled [MorphRule]
Y.morphingRules
      | Bool
_dataize = [DataizeRule] -> FilePath
explainDataizeRules ([DataizeRule] -> FilePath) -> IO [DataizeRule] -> IO FilePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataizeRule] -> IO [DataizeRule]
forall a. [a] -> IO [a]
shuffled [DataizeRule]
Y.dataizationRules
      | Bool
_contextualize = [ContextualizeRule] -> FilePath
explainContextualizeRules ([ContextualizeRule] -> FilePath)
-> IO [ContextualizeRule] -> IO FilePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ContextualizeRule] -> IO [ContextualizeRule]
forall a. [a] -> IO [a]
shuffled [ContextualizeRule]
Y.contextualizationRules
      | Bool
otherwise = [Rule] -> FilePath
explainRules ([Rule] -> FilePath) -> IO [Rule] -> IO FilePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> Bool -> [FilePath] -> IO [Rule]
getRules Bool
_normalize Bool
_shuffle [FilePath]
_rules
    shuffled :: [a] -> IO [a]
    shuffled :: forall a. [a] -> IO [a]
shuffled [a]
xs
      | Bool
_shuffle = [a] -> IO [a]
forall a. [a] -> IO [a]
R.shuffle [a]
xs
      | Bool
otherwise = [a] -> IO [a]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [a]
xs
    validateOpts :: IO ()
    validateOpts :: IO ()
validateOpts = do
      let selected :: Int
selected = [Bool] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((Bool -> Bool) -> [Bool] -> [Bool]
forall a. (a -> Bool) -> [a] -> [a]
filter Bool -> Bool
forall a. a -> a
id [Bool
_morph, Bool
_dataize, Bool
_contextualize])
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
selected Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 Bool -> Bool -> Bool
&& [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) (FilePath -> IO ()
forall a. FilePath -> IO a
invalidCLIArguments FilePath
"Either --rule, --normalize, --morph, --dataize or --contextualize must be specified")
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
selected Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1) (FilePath -> IO ()
forall a. FilePath -> IO a
invalidCLIArguments FilePath
"Only one of --morph, --dataize or --contextualize can be specified")
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
selected Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 Bool -> Bool -> Bool
&& Bool -> Bool
not ([FilePath] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FilePath]
_rules)) (FilePath -> IO ()
forall a. FilePath -> IO a
invalidCLIArguments FilePath
"The --rule option cannot be used together with --morph, --dataize or --contextualize")
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
selected Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 Bool -> Bool -> Bool
&& Bool
_normalize) (FilePath -> IO ()
forall a. FilePath -> IO a
invalidCLIArguments FilePath
"The --normalize option cannot be used together with --morph, --dataize or --contextualize")

runMerge :: OptsMerge -> IO ()
runMerge :: OptsMerge -> IO ()
runMerge OptsMerge{Bool
Int
[FilePath]
Maybe FilePath
LogLevel
Form
SugarType
LineFormat
IOFormat
_logLevel :: LogLevel
_logLines :: Int
_inputFormat :: IOFormat
_monoform :: Form
_outputFormat :: IOFormat
_sugarType :: SugarType
_flat :: LineFormat
_omitListing :: Bool
_omitComments :: Bool
_margin :: Int
_targetFile :: Maybe FilePath
_inputs :: [FilePath]
_seed :: Int
$sel:_logLevel:OptsMerge :: OptsMerge -> LogLevel
$sel:_logLines:OptsMerge :: OptsMerge -> Int
$sel:_inputFormat:OptsMerge :: OptsMerge -> IOFormat
$sel:_monoform:OptsMerge :: OptsMerge -> Form
$sel:_outputFormat:OptsMerge :: OptsMerge -> IOFormat
$sel:_sugarType:OptsMerge :: OptsMerge -> SugarType
$sel:_flat:OptsMerge :: OptsMerge -> LineFormat
$sel:_omitListing:OptsMerge :: OptsMerge -> Bool
$sel:_omitComments:OptsMerge :: OptsMerge -> Bool
$sel:_margin:OptsMerge :: OptsMerge -> Int
$sel:_targetFile:OptsMerge :: OptsMerge -> Maybe FilePath
$sel:_inputs:OptsMerge :: OptsMerge -> [FilePath]
$sel:_seed:OptsMerge :: OptsMerge -> Int
..} = do
  IO ()
validateOpts
  [FilePath]
inputs' <- (FilePath -> IO FilePath) -> [FilePath] -> IO [FilePath]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (Maybe FilePath -> IO FilePath
readInput (Maybe FilePath -> IO FilePath)
-> (FilePath -> Maybe FilePath) -> FilePath -> IO FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just) [FilePath]
_inputs
  StdGen -> IO ()
forall (m :: * -> *). MonadIO m => StdGen -> m ()
setStdGen (Int -> StdGen
mkStdGen Int
_seed)
  ([Expression]
exprs, [Atoms]
atoms) <- [(Expression, Atoms)] -> ([Expression], [Atoms])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(Expression, Atoms)] -> ([Expression], [Atoms]))
-> IO [(Expression, Atoms)] -> IO ([Expression], [Atoms])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (FilePath -> IO (Expression, Atoms))
-> [FilePath] -> IO [(Expression, Atoms)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (\FilePath
input -> FilePath -> IOFormat -> Form -> IO (Expression, Atoms)
parseInputWithAtoms FilePath
input IOFormat
_inputFormat Form
_monoform) [FilePath]
inputs'
  Expression
expr <- [Expression] -> IO Expression
merge [Expression]
exprs
  IOFormat -> Expression -> IO ()
validateXmirTopLevel IOFormat
_outputFormat Expression
expr
  let listing :: b -> FilePath
listing = FilePath -> b -> FilePath
forall a b. a -> b -> a
const (FilePath -> FilePath
escapeXMLText (Expression -> PrintConfig -> FilePath
P.printExpression' Expression
expr (SugarType
_sugarType, Encoding
UNICODE, LineFormat
_flat, Int
_margin)))
      xmirCtx :: XmirContext
xmirCtx = Bool
-> Bool -> Bool -> (Expression -> FilePath) -> Atoms -> XmirContext
XmirContext Bool
_omitListing Bool
_omitComments Bool
False Expression -> FilePath
forall {b}. b -> FilePath
listing ([Atoms] -> Atoms
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions [Atoms]
atoms)
      printCtx :: PrintContext
printCtx = XmirContext -> PrintContext
toPrintCtx XmirContext
xmirCtx
  FilePath
expr' <- PrintContext -> Expression -> IO FilePath
printInFormat PrintContext
printCtx Expression
expr
  Maybe FilePath -> FilePath -> IO ()
printOut Maybe FilePath
_targetFile FilePath
expr'
  where
    validateOpts :: IO ()
    validateOpts :: IO ()
validateOpts = do
      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]
_inputs) (CmdException -> IO ()
forall e a. Exception e => e -> IO a
throwIO (FilePath -> CmdException
InvalidCLIArguments FilePath
"At least one input file must be specified for 'merge' command"))
      IOFormat -> [(Bool, FilePath)] -> FilePath -> IO ()
validateXmirOptions IOFormat
_outputFormat [(Bool
_omitListing, FilePath
"omit-listing"), (Bool
_omitComments, FilePath
"omit-comments")] FilePath
"Q"
    toPrintCtx :: XmirContext -> PrintContext
    toPrintCtx :: XmirContext -> PrintContext
toPrintCtx XmirContext
xmirCtx =
      SugarType
-> Bool
-> Maybe Int
-> Bool
-> LineFormat
-> Int
-> XmirContext
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> Int
-> Int
-> Expression
-> Maybe FilePath
-> Maybe FilePath
-> Maybe FilePath
-> IOFormat
-> PrintContext
PrintCtx
        SugarType
_sugarType
        Bool
False
        Maybe Int
forall a. Maybe a
Nothing
        Bool
False
        LineFormat
_flat
        Int
_margin
        XmirContext
xmirCtx
        Bool
False
        Bool
False
        Bool
False
        Bool
False
        Bool
False
        (Maybe Int -> Int
justMeetPopularity Maybe Int
forall a. Maybe a
Nothing)
        (Maybe Int -> Int
justMeetLength Maybe Int
forall a. Maybe a
Nothing)
        Expression
ExRoot
        Maybe FilePath
forall a. Maybe a
Nothing
        Maybe FilePath
forall a. Maybe a
Nothing
        Maybe FilePath
forall a. Maybe a
Nothing
        IOFormat
_outputFormat

runMatch :: OptsMatch -> IO ()
runMatch :: OptsMatch -> IO ()
runMatch OptsMatch{Int
Maybe FilePath
LogLevel
Form
SugarType
LineFormat
_logLevel :: LogLevel
_logLines :: Int
_monoform :: Form
_sugarType :: SugarType
_flat :: LineFormat
_pattern :: Maybe FilePath
_when :: Maybe FilePath
_inputFile :: Maybe FilePath
_seed :: Int
$sel:_logLevel:OptsMatch :: OptsMatch -> LogLevel
$sel:_logLines:OptsMatch :: OptsMatch -> Int
$sel:_monoform:OptsMatch :: OptsMatch -> Form
$sel:_sugarType:OptsMatch :: OptsMatch -> SugarType
$sel:_flat:OptsMatch :: OptsMatch -> LineFormat
$sel:_pattern:OptsMatch :: OptsMatch -> Maybe FilePath
$sel:_when:OptsMatch :: OptsMatch -> Maybe FilePath
$sel:_inputFile:OptsMatch :: OptsMatch -> Maybe FilePath
$sel:_seed:OptsMatch :: OptsMatch -> Int
..} = do
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Maybe FilePath -> Bool
forall a. Maybe a -> Bool
isJust Maybe FilePath
_when Bool -> Bool -> Bool
&& Maybe FilePath -> Bool
forall a. Maybe a -> Bool
isNothing Maybe FilePath
_pattern) (FilePath -> IO ()
forall a. FilePath -> IO a
invalidCLIArguments FilePath
"The option --when requires --pattern, since there is nothing to check it against")
  StdGen -> IO ()
forall (m :: * -> *). MonadIO m => StdGen -> m ()
setStdGen (Int -> StdGen
mkStdGen Int
_seed)
  FilePath
input <- Maybe FilePath -> IO FilePath
readInput Maybe FilePath
_inputFile
  Expression
expr <- FilePath -> IOFormat -> Form -> IO Expression
parseInput FilePath
input IOFormat
PHI Form
_monoform
  if Maybe FilePath -> Bool
forall a. Maybe a -> Bool
isNothing Maybe FilePath
_pattern
    then FilePath -> IO ()
logDebug FilePath
"The --pattern is not provided, no substitutions are built"
    else do
      Expression
ptn <- FilePath -> IO Expression
parseExpressionThrows (Maybe FilePath -> FilePath
forall a. HasCallStack => Maybe a -> a
fromJust Maybe FilePath
_pattern)
      Maybe Condition
condition <- (FilePath -> IO Condition)
-> Maybe FilePath -> IO (Maybe Condition)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse FilePath -> IO Condition
parseConditionThrows Maybe FilePath
_when
      (Text -> IO Any) -> Maybe Text -> IO ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (CmdException -> IO Any
forall e a. Exception e => e -> IO a
throwIO (CmdException -> IO Any)
-> (Text -> CmdException) -> Text -> IO Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> CmdException
AnonymousMetaInCondition (FilePath -> CmdException)
-> (Text -> FilePath) -> Text -> CmdException
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> FilePath
T.unpack) (Maybe Condition -> Maybe Text
forall a. Slots a => a -> Maybe Text
anonymous Maybe Condition
condition)
      (Text -> IO Any) -> Maybe Text -> IO ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (CmdException -> IO Any
forall e a. Exception e => e -> IO a
throwIO (CmdException -> IO Any)
-> (Text -> CmdException) -> Text -> IO Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> CmdException
UnboundMetaInCondition (FilePath -> CmdException)
-> (Text -> FilePath) -> Text -> CmdException
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> FilePath
T.unpack) ([Text] -> Maybe Text
forall a. [a] -> Maybe a
listToMaybe (Expression -> Maybe Condition -> [Text]
unboundMetas Expression
ptn Maybe Condition
condition))
      Engine
linked <- IO Engine
engine
      [Subst]
substs <- Expression -> Rule -> RuleContext -> IO [Subst]
matchExpressionWithRule Expression
expr (Expression -> Maybe Condition -> Rule
rule Expression
ptn Maybe Condition
condition) (BuildTermFunc
-> Maybe Expression -> (Expression -> Bool) -> RuleContext
RuleContext (Engine -> BuildTermFunc
building Engine
linked) Maybe Expression
forall a. Maybe a
Nothing Engine
linked._normal)
      if [Subst] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Subst]
substs
        then CmdException -> IO ()
forall e a. Exception e => e -> IO a
throwIO CmdException
EmptySubstsOnMatch
        else FilePath -> IO ()
putStrLn ([Subst] -> PrintConfig -> FilePath
P.printSubsts' [Subst]
substs (SugarType
_sugarType, Encoding
UNICODE, LineFormat
_flat, Int
defaultMargin))
  where
    rule :: Expression -> Maybe Y.Condition -> Y.Rule
    rule :: Expression -> Maybe Condition -> Rule
rule Expression
ptn Maybe Condition
cnd = FilePath
-> Maybe FilePath
-> Maybe FilePath
-> Expression
-> Expression
-> Maybe Condition
-> Maybe [Extra]
-> Maybe Condition
-> Rule
Y.Rule FilePath
"custom" Maybe FilePath
forall a. Maybe a
Nothing Maybe FilePath
forall a. Maybe a
Nothing Expression
ptn Expression
ExRoot Maybe Condition
cnd Maybe [Extra]
forall a. Maybe a
Nothing Maybe Condition
forall a. Maybe a
Nothing
    unboundMetas :: Expression -> Maybe Y.Condition -> [T.Text]
    unboundMetas :: Expression -> Maybe Condition -> [Text]
unboundMetas Expression
ptn Maybe Condition
condition = (Text -> Bool) -> [Text] -> [Text]
forall a. (a -> Bool) -> [a] -> [a]
filter (Text -> [Text] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Expression -> [Text]
forall a. Metas a => a -> [Text]
namedMetas Expression
ptn) (Maybe Condition -> [Text]
forall a. Metas a => a -> [Text]
namedMetas Maybe Condition
condition)
    namedMetas :: (Metas a) => a -> [T.Text]
    namedMetas :: forall a. Metas a => a -> [Text]
namedMetas a
term = (Text -> Bool) -> [Text] -> [Text]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1) (Int -> Bool) -> (Text -> Int) -> Text -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Int
T.length) (a -> [Text]
forall a. Metas a => a -> [Text]
metas a
term)

runCompile :: OptsCompile -> IO ()
runCompile :: OptsCompile -> IO ()
runCompile OptsCompile{Int
FilePath
[FilePath]
LogLevel
_logLevel :: LogLevel
_logLines :: Int
_rules :: [FilePath]
_targetFile :: FilePath
$sel:_logLevel:OptsCompile :: OptsCompile -> LogLevel
$sel:_logLines:OptsCompile :: OptsCompile -> Int
$sel:_rules:OptsCompile :: OptsCompile -> [FilePath]
$sel:_targetFile:OptsCompile :: OptsCompile -> FilePath
..} = do
  [Rule]
custom <- Bool -> Bool -> [FilePath] -> IO [Rule]
getRules Bool
False Bool
False [FilePath]
_rules
  FilePath
source <- (FilePath -> IO FilePath)
-> (FilePath -> IO FilePath)
-> Either FilePath FilePath
-> IO FilePath
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (CmdException -> IO FilePath
forall e a. Exception e => e -> IO a
throwIO (CmdException -> IO FilePath)
-> (FilePath -> CmdException) -> FilePath -> IO FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> CmdException
CouldNotCompile) FilePath -> IO FilePath
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Rule]
-> [Rule]
-> [ContextualizeRule]
-> [MorphRule]
-> [DataizeRule]
-> [FilePath]
-> Either FilePath FilePath
emitted [Rule]
Y.normalizationRules [Rule]
custom [ContextualizeRule]
Y.contextualizationRules [MorphRule]
Y.morphingRules [DataizeRule]
Y.dataizationRules [FilePath]
current)
  FilePath -> FilePath -> IO ()
overwrite FilePath
_targetFile FilePath
source
  FilePath -> IO ()
logInfo (FilePath -> FilePath -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"The rules were compiled into '%s'" FilePath
_targetFile)
  Maybe FilePath
root <- FilePath -> IO (Maybe FilePath)
projectRootOf (FilePath -> FilePath
takeDirectory FilePath
_targetFile)
  case Maybe FilePath
root of
    Maybe FilePath
Nothing -> FilePath -> IO ()
putStrLn FilePath
"package phino\n  flags: +compiled"
    Just FilePath
dir -> do
      let localFile :: FilePath
localFile = FilePath
dir FilePath -> FilePath -> FilePath
</> FilePath
"cabal.project.local"
      Bool
exists <- FilePath -> IO Bool
doesFileExist FilePath
localFile
      if Bool
exists
        then FilePath -> IO ()
putStrLn (FilePath -> FilePath -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"The file '%s' exists, so add these lines to it to link the compiled rules in:\npackage phino\n  flags: +compiled" FilePath
localFile)
        else do
          FilePath -> FilePath -> IO ()
overwrite FilePath
localFile FilePath
"package phino\n  flags: +compiled\n"
          FilePath -> IO ()
logInfo (FilePath -> FilePath -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"The file '%s' was written, so the next build links the compiled rules in" FilePath
localFile)
  where
    projectRootOf :: FilePath -> IO (Maybe FilePath)
    projectRootOf :: FilePath -> IO (Maybe FilePath)
projectRootOf FilePath
dir = do
      FilePath
full <- FilePath -> IO FilePath
canonicalizePath FilePath
dir
      Bool
found <- FilePath -> IO Bool
doesFileExist (FilePath
full FilePath -> FilePath -> FilePath
</> FilePath
"phino.cabal")
      let parent :: FilePath
parent = FilePath -> FilePath
takeDirectory FilePath
full
      if Bool
found
        then Maybe FilePath -> IO (Maybe FilePath)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just FilePath
full)
        else if FilePath
parent FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
full then Maybe FilePath -> IO (Maybe FilePath)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe FilePath
forall a. Maybe a
Nothing else FilePath -> IO (Maybe FilePath)
projectRootOf FilePath
parent