-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
-- SPDX-License-Identifier: MIT
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}

module CLI.Helpers where

import AST
import Abridge (abridged)
import CLI.Types
import CLI.Validators (invalidCLIArguments)
import CST (EXPRESSION)
import Canonizer (canonizeExpr, lambdaNames)
import Compiled (compiled)
import Control.Exception
import Control.Monad (mfilter, when, (>=>))
import qualified Data.ByteString as BS
import Data.Char (isDigit, toLower)
import Data.Functor ((<&>))
import Data.IORef
import Data.List (intercalate, nub)
import qualified Data.Map.Strict as M
import Data.Maybe
import qualified Data.Text as T
import Data.Text.Encoding (encodeUtf8)
import Data.Time (getZonedTime)
import Data.Version (showVersion)
import qualified Data.Yaml as Yaml
import Deps (Evaluation (EvHeader, EvRun), Header (Header), Judgment, SaveEvalFunc, SaveStepFunc, World (World), dontSaveEval, emptyNesting, emptyProgress, emptyProtocol, endEval, endEvalXml, progressed, resited, saveEval, saveEvalXml, saveStep)
import Encoding
import Engine (Engine, fresh, yaml)
import Files (ensuredFile, overwrite)
import qualified Filter as F
import Functions (buildFunctions, execFunctions)
import GHC.Clock (getMonotonicTime)
import LaTeX (LatexContext (LatexContext), defaultMeetLength, defaultMeetPopularity, expressionToLaTeX, rewrittensToLatex)
import Lambdas (Lambdas, emptyLambdas, readLambdas, sized, taken)
import Lining (LineFormat (SINGLELINE))
import Locator (locatedExpression, withLocatedExpression)
import Logger
import Morph (ReduceContext (..), insideUniverse)
import Parser (Form, parseExpressionThrows, parseExpressionThrows')
import Paths_phino (version)
import qualified Printer as P
import qualified Random as R
import Rewriter (Rewrittens', stepHeaders)
import Sugar (SugarType (SALTY), withoutRho)
import System.Directory (createDirectoryIfMissing, doesDirectoryExist, doesFileExist, listDirectory, removeFile)
import System.FilePath (splitExtension, takeDirectory, takeExtension, (</>))
import System.IO (Handle, IOMode (WriteMode), getContents', hClose, hSetEncoding, openFile, utf8)
import Text.Printf (printf)
import XMIR (Atoms, expressionToXMIR, gitRevision, parseXMIRThrows, printXMIR, renameAtoms, xmirAtoms, xmirToPhi)
import Yaml (normalizationRules)
import qualified Yaml as Y

justMeetPopularity :: Maybe Int -> Int
justMeetPopularity :: Maybe Int -> Int
justMeetPopularity = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
defaultMeetPopularity

justMeetLength :: Maybe Int -> Int
justMeetLength :: Maybe Int -> Int
justMeetLength = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
defaultMeetLength

isStepFileName :: FilePath -> Bool
isStepFileName :: FilePath -> Bool
isStepFileName FilePath
name = FilePath -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length FilePath
base Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
5 Bool -> Bool -> Bool
&& (Char -> Bool) -> FilePath -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isDigit FilePath
base Bool -> Bool -> Bool
&& FilePath
ext FilePath -> [FilePath] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FilePath
".phi", FilePath
".xmir", FilePath
".tex"]
  where
    (FilePath
base, FilePath
ext) = FilePath -> (FilePath, FilePath)
splitExtension FilePath
name

clearedStepsDir :: Maybe FilePath -> IO ()
clearedStepsDir :: Maybe FilePath -> IO ()
clearedStepsDir Maybe FilePath
Nothing = () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
clearedStepsDir (Just FilePath
dir) = do
  Bool
exists <- FilePath -> IO Bool
doesDirectoryExist FilePath
dir
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
exists (FilePath -> IO [FilePath]
listDirectory FilePath
dir 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 ()) -> [FilePath] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ FilePath -> IO ()
removedIfStepFile)
  where
    removedIfStepFile :: FilePath -> IO ()
    removedIfStepFile :: FilePath -> IO ()
removedIfStepFile FilePath
name = Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FilePath -> Bool
isStepFileName FilePath
name) (FilePath -> IO ()
removedFile (FilePath
dir FilePath -> FilePath -> FilePath
</> FilePath
name))
    removedFile :: FilePath -> IO ()
    removedFile :: FilePath -> IO ()
removedFile FilePath
path = do
      Bool
isFile <- FilePath -> IO Bool
doesFileExist FilePath
path
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
isFile (FilePath -> IO ()
removeFile FilePath
path)

saveStepFunc :: Maybe FilePath -> PrintContext -> [Expression] -> [Expression] -> IO SaveStepFunc
saveStepFunc :: Maybe FilePath
-> PrintContext -> [Expression] -> [Expression] -> IO SaveStepFunc
saveStepFunc Maybe FilePath
stepsDir ctx :: PrintContext
ctx@PrintCtx{Bool
Int
Maybe Int
Maybe FilePath
Expression
SugarType
LineFormat
XmirContext
IOFormat
_sugar :: SugarType
_hideRho :: Bool
_abridged :: Maybe Int
_abridgedData :: Bool
_line :: LineFormat
_margin :: Int
_xmirCtx :: XmirContext
_nonumber :: Bool
_compress :: Bool
_canonize :: Bool
_sequence :: Bool
_headers :: Bool
_meetPopularity :: Int
_meetLength :: Int
_focus :: Expression
_expression :: Maybe FilePath
_label :: Maybe FilePath
_meetPrefix :: Maybe FilePath
_outputFormat :: IOFormat
$sel:_sugar:PrintCtx :: PrintContext -> SugarType
$sel:_hideRho:PrintCtx :: PrintContext -> Bool
$sel:_abridged:PrintCtx :: PrintContext -> Maybe Int
$sel:_abridgedData:PrintCtx :: PrintContext -> Bool
$sel:_line:PrintCtx :: PrintContext -> LineFormat
$sel:_margin:PrintCtx :: PrintContext -> Int
$sel:_xmirCtx:PrintCtx :: PrintContext -> XmirContext
$sel:_nonumber:PrintCtx :: PrintContext -> Bool
$sel:_compress:PrintCtx :: PrintContext -> Bool
$sel:_canonize:PrintCtx :: PrintContext -> Bool
$sel:_sequence:PrintCtx :: PrintContext -> Bool
$sel:_headers:PrintCtx :: PrintContext -> Bool
$sel:_meetPopularity:PrintCtx :: PrintContext -> Int
$sel:_meetLength:PrintCtx :: PrintContext -> Int
$sel:_focus:PrintCtx :: PrintContext -> Expression
$sel:_expression:PrintCtx :: PrintContext -> Maybe FilePath
$sel:_label:PrintCtx :: PrintContext -> Maybe FilePath
$sel:_meetPrefix:PrintCtx :: PrintContext -> Maybe FilePath
$sel:_outputFormat:PrintCtx :: PrintContext -> IOFormat
..} [Expression]
included [Expression]
excluded = do
  Maybe FilePath -> IO ()
clearedStepsDir Maybe FilePath
stepsDir
  IORef Int
counter <- Int -> IO (IORef Int)
forall a. a -> IO (IORef a)
newIORef (Int
0 :: Int)
  let ioToExt :: String
      ioToExt :: FilePath
ioToExt
        | IOFormat
_outputFormat IOFormat -> IOFormat -> Bool
forall a. Eq a => a -> a -> Bool
== IOFormat
LATEX = FilePath
"tex"
        | Bool
otherwise = IOFormat -> FilePath
forall a. Show a => a -> FilePath
show IOFormat
_outputFormat
      render :: Expression -> IO FilePath
render Expression
expr = do
        Expression
shown <- Expression -> [Expression] -> IO Expression
F.exclude' Expression
expr [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)
        PrintContext -> Expression -> IO FilePath
printAnswer PrintContext
ctx Expression
shown
      save :: SaveStepFunc
      save :: SaveStepFunc
save Expression
expr = do
        Int
step <- IORef Int -> (Int -> (Int, Int)) -> IO Int
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef' IORef Int
counter (\Int
value -> (Int
value Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, Int
value Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1))
        Maybe FilePath
-> FilePath -> (Expression -> IO FilePath) -> Int -> SaveStepFunc
saveStep Maybe FilePath
stepsDir FilePath
ioToExt Expression -> IO FilePath
render Int
step Expression
expr
  SaveStepFunc -> IO SaveStepFunc
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SaveStepFunc
save

withEvalFunc :: forall a. Maybe FilePath -> PrintContext -> (SaveEvalFunc -> IO a) -> IO a
withEvalFunc :: forall a.
Maybe FilePath
-> PrintContext -> ((Evaluation -> IO ()) -> IO a) -> IO a
withEvalFunc Maybe FilePath
target PrintContext
ctx (Evaluation -> IO ()) -> IO a
action = Maybe FilePath
-> PrintContext -> ((Evaluation -> IO ()) -> IO a) -> IO a
forall a.
Maybe FilePath
-> PrintContext -> ((Evaluation -> IO ()) -> IO a) -> IO a
withEvalFunc' Maybe FilePath
target PrintContext
ctx ((Evaluation -> IO ()) -> IO (Evaluation -> IO ())
tracked ((Evaluation -> IO ()) -> IO (Evaluation -> IO ()))
-> ((Evaluation -> IO ()) -> IO a) -> (Evaluation -> IO ()) -> IO a
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> (Evaluation -> IO ()) -> IO a
action)
  where
    tracked :: SaveEvalFunc -> IO SaveEvalFunc
    tracked :: (Evaluation -> IO ()) -> IO (Evaluation -> IO ())
tracked Evaluation -> IO ()
record = do
      Bool
enabled <- LogLevel -> IO Bool
logging LogLevel
INFO
      if Bool
enabled
        then do
          IORef Progress
cursor <- Progress -> IO (IORef Progress)
forall a. a -> IO (IORef a)
newIORef (Progress -> IO (IORef Progress))
-> (Double -> Progress) -> Double -> IO (IORef Progress)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Progress
emptyProgress (Double -> IO (IORef Progress)) -> IO Double -> IO (IORef Progress)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IO Double
getMonotonicTime
          (Evaluation -> IO ()) -> IO (Evaluation -> IO ())
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (IORef Progress
-> Double
-> (Expression -> IO FilePath)
-> (Evaluation -> IO ())
-> Evaluation
-> IO ()
progressed IORef Progress
cursor Double
5 (PrintContext -> Expression -> IO FilePath
flattened PrintContext
ctx) Evaluation -> IO ()
record)
        else (Evaluation -> IO ()) -> IO (Evaluation -> IO ())
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Evaluation -> IO ()
record

withEvalFunc' :: forall a. Maybe FilePath -> PrintContext -> (SaveEvalFunc -> IO a) -> IO a
withEvalFunc' :: forall a.
Maybe FilePath
-> PrintContext -> ((Evaluation -> IO ()) -> IO a) -> IO a
withEvalFunc' Maybe FilePath
Nothing PrintContext
_ (Evaluation -> IO ()) -> IO a
action = (Evaluation -> IO ()) -> IO a
action Evaluation -> IO ()
dontSaveEval
withEvalFunc' (Just FilePath
file) PrintContext
ctx (Evaluation -> IO ()) -> IO a
action = do
  Bool -> FilePath -> IO ()
createDirectoryIfMissing Bool
True (FilePath -> FilePath
takeDirectory FilePath
file)
  FilePath -> IO ()
logDebug (FilePath -> FilePath -> FilePath -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"The option '--protocol' is specified, every firing will be recorded in '%s' as %s" FilePath
file (if Bool
markup then FilePath
"XML" else FilePath
"text"))
  if Bool
markup then IO a
markedUp else IO a
plain
  where
    markup :: Bool
    markup :: Bool
markup = (Char -> Char) -> FilePath -> FilePath
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (FilePath -> FilePath
takeExtension FilePath
file) FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
".xml"
    markedUp :: IO a
    markedUp :: IO a
markedUp = do
      IORef Nesting
cursor <- Nesting -> IO (IORef Nesting)
forall a. a -> IO (IORef a)
newIORef Nesting
emptyNesting
      Double
began <- IO Double
getMonotonicTime
      IO Handle -> (Handle -> IO ()) -> (Handle -> IO a) -> IO a
forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
bracket IO Handle
opened (\Handle
protocol -> Handle -> IORef Nesting -> Double -> IO ()
endEvalXml Handle
protocol IORef Nesting
cursor Double
began IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO a
`finally` Handle -> IO ()
hClose Handle
protocol) ((Handle -> IO a) -> IO a) -> (Handle -> IO a) -> IO a
forall a b. (a -> b) -> a -> b
$ \Handle
protocol ->
        (Evaluation -> IO ()) -> IO a
action (Handle
-> IORef Nesting
-> (Expression -> IO FilePath)
-> Evaluation
-> IO ()
saveEvalXml Handle
protocol IORef Nesting
cursor (PrintContext -> Expression -> IO FilePath
flattened PrintContext
ctx))
    plain :: IO a
    plain :: IO a
plain = do
      IORef Protocol
cursor <- Protocol -> IO (IORef Protocol)
forall a. a -> IO (IORef a)
newIORef Protocol
emptyProtocol
      Double
began <- IO Double
getMonotonicTime
      IO Handle -> (Handle -> IO ()) -> (Handle -> IO a) -> IO a
forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
bracket IO Handle
opened (\Handle
protocol -> Handle -> IORef Protocol -> Double -> IO ()
endEval Handle
protocol IORef Protocol
cursor Double
began IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO a
`finally` Handle -> IO ()
hClose Handle
protocol) ((Handle -> IO a) -> IO a) -> (Handle -> IO a) -> IO a
forall a b. (a -> b) -> a -> b
$ \Handle
protocol ->
        (Evaluation -> IO ()) -> IO a
action (Handle
-> IORef Protocol
-> (Expression -> IO FilePath)
-> (Expression -> IO FilePath)
-> Evaluation
-> IO ()
saveEval Handle
protocol IORef Protocol
cursor (PrintContext -> Expression -> IO FilePath
flattened PrintContext
ctx) (PrintContext -> Expression -> IO FilePath
salted PrintContext
ctx))
    opened :: IO Handle
    opened :: IO Handle
opened = do
      Handle
protocol <- FilePath -> IOMode -> IO Handle
openFile FilePath
file IOMode
WriteMode
      Handle -> TextEncoding -> IO ()
hSetEncoding Handle
protocol TextEncoding
utf8
      Handle -> IO Handle
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Handle
protocol

lambdasOf :: Maybe FilePath -> IO Lambdas
lambdasOf :: Maybe FilePath -> IO Lambdas
lambdasOf Maybe FilePath
Nothing = do
  FilePath -> IO ()
logDebug FilePath
"The option '--symbolic' is not specified, no λ function can be fired"
  Lambdas -> IO Lambdas
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Lambdas
emptyLambdas
lambdasOf (Just FilePath
file) = do
  FilePath -> IO ()
logDebug (FilePath -> FilePath -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"The option '--symbolic' is specified, reading the λ functions from '%s'" FilePath
file)
  FilePath -> IO FilePath
ensuredFile FilePath
file IO FilePath -> (FilePath -> IO Lambdas) -> IO Lambdas
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 Lambdas
readLambdas

started :: Expression -> ReduceContext -> IO ()
started :: Expression -> ReduceContext -> IO ()
started Expression
expr ReduceContext
ctx = IORef Int -> (Int -> Int) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' ReduceContext
ctx._minted (Int -> Int -> Int
forall a. Ord a => a -> a -> a
max (Expression -> Int
taken Expression
expr))

heading :: SaveEvalFunc -> PrintContext -> Judgment -> Expression -> IO ()
heading :: (Evaluation -> IO ()) -> PrintContext -> Judgment -> SaveStepFunc
heading Evaluation -> IO ()
record PrintContext
ctx Judgment
judgment Expression
locator =
  Evaluation -> IO ()
record (Evaluation -> IO ())
-> (FilePath -> Evaluation) -> FilePath -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Judgment -> Text -> Evaluation
EvRun Judgment
judgment (Text -> Evaluation)
-> (FilePath -> Text) -> FilePath -> Evaluation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Text
T.pack (FilePath -> IO ()) -> IO FilePath -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< PrintContext -> Expression -> IO FilePath
flattened PrintContext
ctx Expression
locator

flattened :: PrintContext -> Expression -> IO String
flattened :: PrintContext -> Expression -> IO FilePath
flattened ctx :: PrintContext
ctx@PrintCtx{Bool
Int
Maybe Int
Maybe FilePath
Expression
SugarType
LineFormat
XmirContext
IOFormat
$sel:_sugar:PrintCtx :: PrintContext -> SugarType
$sel:_hideRho:PrintCtx :: PrintContext -> Bool
$sel:_abridged:PrintCtx :: PrintContext -> Maybe Int
$sel:_abridgedData:PrintCtx :: PrintContext -> Bool
$sel:_line:PrintCtx :: PrintContext -> LineFormat
$sel:_margin:PrintCtx :: PrintContext -> Int
$sel:_xmirCtx:PrintCtx :: PrintContext -> XmirContext
$sel:_nonumber:PrintCtx :: PrintContext -> Bool
$sel:_compress:PrintCtx :: PrintContext -> Bool
$sel:_canonize:PrintCtx :: PrintContext -> Bool
$sel:_sequence:PrintCtx :: PrintContext -> Bool
$sel:_headers:PrintCtx :: PrintContext -> Bool
$sel:_meetPopularity:PrintCtx :: PrintContext -> Int
$sel:_meetLength:PrintCtx :: PrintContext -> Int
$sel:_focus:PrintCtx :: PrintContext -> Expression
$sel:_expression:PrintCtx :: PrintContext -> Maybe FilePath
$sel:_label:PrintCtx :: PrintContext -> Maybe FilePath
$sel:_meetPrefix:PrintCtx :: PrintContext -> Maybe FilePath
$sel:_outputFormat:PrintCtx :: PrintContext -> IOFormat
_sugar :: SugarType
_hideRho :: Bool
_abridged :: Maybe Int
_abridgedData :: Bool
_line :: LineFormat
_margin :: Int
_xmirCtx :: XmirContext
_nonumber :: Bool
_compress :: Bool
_canonize :: Bool
_sequence :: Bool
_headers :: Bool
_meetPopularity :: Int
_meetLength :: Int
_focus :: Expression
_expression :: Maybe FilePath
_label :: Maybe FilePath
_meetPrefix :: Maybe FilePath
_outputFormat :: IOFormat
..} Expression
expr =
  FilePath -> IO FilePath
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((SugarType -> EXPRESSION -> EXPRESSION)
-> Expression -> PrintConfig -> FilePath
P.printExpressionWith SugarType -> EXPRESSION -> EXPRESSION
shaped Expression
expr (SugarType
_sugar, Encoding
UNICODE, LineFormat
SINGLELINE, Int
_margin))
  where
    shaped :: SugarType -> EXPRESSION -> EXPRESSION
    shaped :: SugarType -> EXPRESSION -> EXPRESSION
shaped SugarType
sugar = (EXPRESSION -> EXPRESSION)
-> (Int -> EXPRESSION -> EXPRESSION)
-> Maybe Int
-> EXPRESSION
-> EXPRESSION
forall b a. b -> (a -> b) -> Maybe a -> b
maybe EXPRESSION -> EXPRESSION
forall a. a -> a
id (Bool -> Int -> EXPRESSION -> EXPRESSION
abridged Bool
_abridgedData) Maybe Int
_abridged (EXPRESSION -> EXPRESSION)
-> (EXPRESSION -> EXPRESSION) -> EXPRESSION -> EXPRESSION
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrintContext -> SugarType -> EXPRESSION -> EXPRESSION
hidden PrintContext
ctx SugarType
sugar

salted :: PrintContext -> Expression -> IO String
salted :: PrintContext -> Expression -> IO FilePath
salted PrintContext
ctx = PrintContext -> Expression -> IO FilePath
flattened PrintContext
ctx{_sugar = SALTY}

headerOf :: [String] -> Maybe FilePath -> String -> Expression -> Maybe FilePath -> Lambdas -> IO Header
headerOf :: [FilePath]
-> Maybe FilePath
-> FilePath
-> Expression
-> Maybe FilePath
-> Lambdas
-> IO Header
headerOf [FilePath]
args Maybe FilePath
file FilePath
input Expression
expr Maybe FilePath
table Lambdas
lambdas = do
  ZonedTime
now <- IO ZonedTime
getZonedTime
  Header -> IO Header
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    ( FilePath
-> Maybe FilePath
-> ZonedTime
-> [FilePath]
-> World
-> Maybe (FilePath, Int)
-> Header
Header
        (Version -> FilePath
showVersion Version
version)
        ((FilePath -> Bool) -> Maybe FilePath -> Maybe FilePath
forall (m :: * -> *) a. MonadPlus m => (a -> Bool) -> m a -> m a
mfilter (FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
/= FilePath
"UNKNOWN") (FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just FilePath
gitRevision))
        ZonedTime
now
        [FilePath]
args
        (Maybe FilePath -> Int -> Int -> Int -> Int -> World
World Maybe FilePath
file ([FilePath] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (FilePath -> [FilePath]
lines FilePath
input)) (ByteString -> Int
BS.length (Text -> ByteString
encodeUtf8 (FilePath -> Text
T.pack FilePath
input))) (Expression -> Int
tops Expression
expr) (Expression -> Int
bindings Expression
expr))
        ((,Lambdas -> Int
sized Lambdas
lambdas) (FilePath -> (FilePath, Int))
-> Maybe FilePath -> Maybe (FilePath, Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe FilePath
table)
    )
  where
    tops :: Expression -> Int
    tops :: Expression -> Int
tops (ExFormation [Binding]
bds) = [Attribute] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Attribute
attr | BiTau Attribute
attr Expression
_ <- [Binding]
bds]
    tops Expression
_ = Int
0
    bindings :: Expression -> Int
    bindings :: Expression -> Int
bindings (ExFormation [Binding]
bds) = [Binding] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Binding]
bds Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Int] -> Int
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Expression -> Int
bindings Expression
inner | BiTau Attribute
_ Expression
inner <- [Binding]
bds]
    bindings (ExApplication Expression
inner (ArTau Attribute
_ Expression
arg)) = Expression -> Int
bindings Expression
inner Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Expression -> Int
bindings Expression
arg
    bindings (ExApplication Expression
inner (ArAlpha Alpha
_ Expression
arg)) = Expression -> Int
bindings Expression
inner Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Expression -> Int
bindings Expression
arg
    bindings (ExDispatch Expression
inner Attribute
_) = Expression -> Int
bindings Expression
inner
    bindings (ExPhiMeet Maybe FilePath
_ Int
_ Expression
inner) = Expression -> Int
bindings Expression
inner
    bindings (ExPhiAgain Maybe FilePath
_ Int
_ Expression
inner) = Expression -> Int
bindings Expression
inner
    bindings Expression
_ = Int
0

aimed :: PrintContext -> Judgment -> Header -> Maybe String -> Expression -> ReduceContext -> IO (Expression, ReduceContext)
aimed :: PrintContext
-> Judgment
-> Header
-> Maybe FilePath
-> Expression
-> ReduceContext
-> IO (Expression, ReduceContext)
aimed PrintContext
printCtx Judgment
judgment Header
header Maybe FilePath
Nothing Expression
expr ReduceContext
ctx = do
  ReduceContext
ctx._saveEval (Evaluation -> IO ()) -> (Expression -> Evaluation) -> SaveStepFunc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Header -> Expression -> Expression -> Evaluation
EvHeader Header
header ReduceContext
ctx._locator SaveStepFunc -> IO Expression -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expression -> Expression -> IO Expression
locatedExpression ReduceContext
ctx._locator Expression
expr
  (Evaluation -> IO ()) -> PrintContext -> Judgment -> SaveStepFunc
heading ReduceContext
ctx._saveEval PrintContext
printCtx Judgment
judgment ReduceContext
ctx._locator
  (Expression, ReduceContext) -> IO (Expression, ReduceContext)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression
expr, ReduceContext
ctx)
aimed PrintContext
printCtx Judgment
judgment Header
header (Just FilePath
src) expr :: Expression
expr@(ExFormation [Binding]
_) ReduceContext
ctx = do
  Expression
target <- FilePath -> IO Expression
parseExpressionThrows FilePath
src
  FilePath -> IO ()
logDebug (FilePath -> FilePath -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"The option '--inside' is specified, reducing '%s' inside the given universe" (Expression -> FilePath
P.printExpression Expression
target))
  IORef [Evaluation]
held <- [Evaluation] -> IO (IORef [Evaluation])
forall a. a -> IO (IORef a)
newIORef []
  (Expression
universe, ReduceContext
aiming) <- Expression
-> Expression -> ReduceContext -> IO (Expression, ReduceContext)
insideUniverse Expression
target Expression
expr ReduceContext
ctx{_saveEval = \Evaluation
record -> IORef [Evaluation] -> ([Evaluation] -> [Evaluation]) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef [Evaluation]
held (Evaluation
record Evaluation -> [Evaluation] -> [Evaluation]
forall a. a -> [a] -> [a]
:)}
  ReduceContext
ctx._saveEval (Header -> Expression -> Expression -> Evaluation
EvHeader Header
header ReduceContext
aiming._locator Expression
target)
  (Evaluation -> IO ()) -> PrintContext -> Judgment -> SaveStepFunc
heading ReduceContext
ctx._saveEval PrintContext
printCtx Judgment
judgment ReduceContext
aiming._locator
  (Evaluation -> IO ()) -> [Evaluation] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (ReduceContext
ctx._saveEval (Evaluation -> IO ())
-> (Evaluation -> Evaluation) -> Evaluation -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expression -> Expression -> Evaluation -> Evaluation
resited ReduceContext
ctx._site ReduceContext
aiming._locator) ([Evaluation] -> IO ())
-> ([Evaluation] -> [Evaluation]) -> [Evaluation] -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Evaluation] -> [Evaluation]
forall a. [a] -> [a]
reverse ([Evaluation] -> IO ()) -> IO [Evaluation] -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IORef [Evaluation] -> IO [Evaluation]
forall a. IORef a -> IO a
readIORef IORef [Evaluation]
held
  (Expression, ReduceContext) -> IO (Expression, ReduceContext)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression
universe, ReduceContext
aiming{_site = aiming._locator, _saveEval = ctx._saveEval})
aimed PrintContext
_ Judgment
_ Header
_ (Just FilePath
_) Expression
expr ReduceContext
_ =
  FilePath -> IO (Expression, ReduceContext)
forall a. FilePath -> IO a
invalidCLIArguments
    (FilePath -> FilePath -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"The option --inside requires the input expression to be a formation, but given: %s" (Expression -> FilePath
P.printExpression Expression
expr))

readInput :: Maybe FilePath -> IO String
readInput :: Maybe FilePath -> IO FilePath
readInput Maybe FilePath
inputFile' =
  FilePath -> FilePath
withoutBOM (FilePath -> FilePath) -> IO FilePath -> IO FilePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> case Maybe FilePath
inputFile' of
    Just FilePath
pth -> do
      FilePath -> IO ()
logDebug (FilePath -> FilePath -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"Reading from file: '%s'" FilePath
pth)
      FilePath -> IO FilePath
readFile (FilePath -> IO FilePath) -> IO FilePath -> IO FilePath
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< FilePath -> IO FilePath
ensuredFile FilePath
pth
    Maybe FilePath
Nothing -> do
      FilePath -> IO ()
logDebug FilePath
"Reading from stdin"
      IO FilePath
getContents' IO FilePath -> (SomeException -> IO FilePath) -> IO FilePath
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` (\(SomeException
e :: SomeException) -> CmdException -> IO FilePath
forall e a. Exception e => e -> IO a
throwIO (FilePath -> CmdException
CouldNotReadFromStdin (SomeException -> FilePath
forall a. Show a => a -> FilePath
show SomeException
e)))

withoutBOM :: String -> String
withoutBOM :: FilePath -> FilePath
withoutBOM (Char
'\xFEFF' : FilePath
rest) = FilePath
rest
withoutBOM FilePath
input = FilePath
input

parseInput :: String -> IOFormat -> Form -> IO Expression
parseInput :: FilePath -> IOFormat -> Form -> IO Expression
parseInput FilePath
phi IOFormat
PHI Form
form = Form -> FilePath -> IO Expression
parseExpressionThrows' Form
form FilePath
phi
parseInput FilePath
xmir IOFormat
XMIR Form
_ = FilePath -> IO Document
parseXMIRThrows FilePath
xmir IO Document -> (Document -> 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
>>= Document -> IO Expression
xmirToPhi
parseInput FilePath
_ IOFormat
LATEX Form
_ = FilePath -> IO Expression
forall a. FilePath -> IO a
invalidCLIArguments FilePath
"LaTeX cannot be used as input format"

parseInputWithAtoms :: String -> IOFormat -> Form -> IO (Expression, Atoms)
parseInputWithAtoms :: FilePath -> IOFormat -> Form -> IO (Expression, Atoms)
parseInputWithAtoms FilePath
xmir IOFormat
XMIR Form
_ = do
  Document
doc <- FilePath -> IO Document
parseXMIRThrows FilePath
xmir
  (,) (Expression -> Atoms -> (Expression, Atoms))
-> IO Expression -> IO (Atoms -> (Expression, Atoms))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Document -> IO Expression
xmirToPhi Document
doc IO (Atoms -> (Expression, Atoms))
-> IO Atoms -> IO (Expression, Atoms)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Document -> IO Atoms
xmirAtoms Document
doc
parseInputWithAtoms FilePath
input IOFormat
format Form
form = (,Atoms
forall k a. Map k a
M.empty) (Expression -> (Expression, Atoms))
-> IO Expression -> IO (Expression, Atoms)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FilePath -> IOFormat -> Form -> IO Expression
parseInput FilePath
input IOFormat
format Form
form

printRewrittens :: PrintContext -> Rewrittens' -> IO String
printRewrittens :: PrintContext -> Rewrittens' -> IO FilePath
printRewrittens ctx :: PrintContext
ctx@PrintCtx{Bool
Int
Maybe Int
Maybe FilePath
Expression
SugarType
LineFormat
XmirContext
IOFormat
$sel:_sugar:PrintCtx :: PrintContext -> SugarType
$sel:_hideRho:PrintCtx :: PrintContext -> Bool
$sel:_abridged:PrintCtx :: PrintContext -> Maybe Int
$sel:_abridgedData:PrintCtx :: PrintContext -> Bool
$sel:_line:PrintCtx :: PrintContext -> LineFormat
$sel:_margin:PrintCtx :: PrintContext -> Int
$sel:_xmirCtx:PrintCtx :: PrintContext -> XmirContext
$sel:_nonumber:PrintCtx :: PrintContext -> Bool
$sel:_compress:PrintCtx :: PrintContext -> Bool
$sel:_canonize:PrintCtx :: PrintContext -> Bool
$sel:_sequence:PrintCtx :: PrintContext -> Bool
$sel:_headers:PrintCtx :: PrintContext -> Bool
$sel:_meetPopularity:PrintCtx :: PrintContext -> Int
$sel:_meetLength:PrintCtx :: PrintContext -> Int
$sel:_focus:PrintCtx :: PrintContext -> Expression
$sel:_expression:PrintCtx :: PrintContext -> Maybe FilePath
$sel:_label:PrintCtx :: PrintContext -> Maybe FilePath
$sel:_meetPrefix:PrintCtx :: PrintContext -> Maybe FilePath
$sel:_outputFormat:PrintCtx :: PrintContext -> IOFormat
_sugar :: SugarType
_hideRho :: Bool
_abridged :: Maybe Int
_abridgedData :: Bool
_line :: LineFormat
_margin :: Int
_xmirCtx :: XmirContext
_nonumber :: Bool
_compress :: Bool
_canonize :: Bool
_sequence :: Bool
_headers :: Bool
_meetPopularity :: Int
_meetLength :: Int
_focus :: Expression
_expression :: Maybe FilePath
_label :: Maybe FilePath
_meetPrefix :: Maybe FilePath
_outputFormat :: IOFormat
..} rewrittens :: Rewrittens'
rewrittens@([Rewritten]
chain, Bool
_)
  | IOFormat
_outputFormat IOFormat -> IOFormat -> Bool
forall a. Eq a => a -> a -> Bool
== IOFormat
LATEX Bool -> Bool -> Bool
&& Bool
_sequence = Rewrittens' -> LatexContext -> IO FilePath
rewrittensToLatex Rewrittens'
rewrittens (PrintContext -> LatexContext
printCtxToLatexCtx PrintContext
ctx)
  | Bool
otherwise = [FilePath] -> FilePath
withHeaders ([FilePath] -> FilePath) -> IO [FilePath] -> IO FilePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Rewritten -> IO FilePath) -> [Rewritten] -> IO [FilePath]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (PrintContext -> Expression -> IO FilePath
printAnswer PrintContext
ctx (Expression -> IO FilePath)
-> (Rewritten -> Expression) -> Rewritten -> IO FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rewritten -> Expression
forall a b. (a, b) -> a
fst) [Rewritten]
chain
  where
    withHeaders :: [String] -> String
    withHeaders :: [FilePath] -> FilePath
withHeaders [FilePath]
rendered
      | Bool
_headers Bool -> Bool -> Bool
&& Bool
_sequence = FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate FilePath
"\n" ((FilePath -> FilePath -> FilePath)
-> [FilePath] -> [FilePath] -> [FilePath]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith FilePath -> FilePath -> FilePath
prefixed ([Rewritten] -> [FilePath]
stepHeaders [Rewritten]
chain) [FilePath]
rendered)
      | Bool
otherwise = FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate FilePath
"\n" [FilePath]
rendered
      where
        prefixed :: String -> String -> String
        prefixed :: FilePath -> FilePath -> FilePath
prefixed = FilePath -> FilePath -> FilePath -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"\n%s\n%s"

printAnswer :: PrintContext -> Expression -> IO String
printAnswer :: PrintContext -> Expression -> IO FilePath
printAnswer ctx :: PrintContext
ctx@PrintCtx{Bool
Int
Maybe Int
Maybe FilePath
Expression
SugarType
LineFormat
XmirContext
IOFormat
$sel:_sugar:PrintCtx :: PrintContext -> SugarType
$sel:_hideRho:PrintCtx :: PrintContext -> Bool
$sel:_abridged:PrintCtx :: PrintContext -> Maybe Int
$sel:_abridgedData:PrintCtx :: PrintContext -> Bool
$sel:_line:PrintCtx :: PrintContext -> LineFormat
$sel:_margin:PrintCtx :: PrintContext -> Int
$sel:_xmirCtx:PrintCtx :: PrintContext -> XmirContext
$sel:_nonumber:PrintCtx :: PrintContext -> Bool
$sel:_compress:PrintCtx :: PrintContext -> Bool
$sel:_canonize:PrintCtx :: PrintContext -> Bool
$sel:_sequence:PrintCtx :: PrintContext -> Bool
$sel:_headers:PrintCtx :: PrintContext -> Bool
$sel:_meetPopularity:PrintCtx :: PrintContext -> Int
$sel:_meetLength:PrintCtx :: PrintContext -> Int
$sel:_focus:PrintCtx :: PrintContext -> Expression
$sel:_expression:PrintCtx :: PrintContext -> Maybe FilePath
$sel:_label:PrintCtx :: PrintContext -> Maybe FilePath
$sel:_meetPrefix:PrintCtx :: PrintContext -> Maybe FilePath
$sel:_outputFormat:PrintCtx :: PrintContext -> IOFormat
_sugar :: SugarType
_hideRho :: Bool
_abridged :: Maybe Int
_abridgedData :: Bool
_line :: LineFormat
_margin :: Int
_xmirCtx :: XmirContext
_nonumber :: Bool
_compress :: Bool
_canonize :: Bool
_sequence :: Bool
_headers :: Bool
_meetPopularity :: Int
_meetLength :: Int
_focus :: Expression
_expression :: Maybe FilePath
_label :: Maybe FilePath
_meetPrefix :: Maybe FilePath
_outputFormat :: IOFormat
..} Expression
expr
  | Bool
_canonize = PrintContext -> Expression -> IO FilePath
printFocused PrintContext
ctx{_xmirCtx = renameAtoms (zip (lambdaNames expr) (lambdaNames canonized)) _xmirCtx} Expression
canonized
  | Bool
otherwise = PrintContext -> Expression -> IO FilePath
printFocused PrintContext
ctx Expression
expr
  where
    canonized :: Expression
    canonized :: Expression
canonized = Expression -> Expression
canonizeExpr Expression
expr

printFocused :: PrintContext -> Expression -> IO String
printFocused :: PrintContext -> Expression -> IO FilePath
printFocused ctx :: PrintContext
ctx@PrintCtx{Bool
Int
Maybe Int
Maybe FilePath
Expression
SugarType
LineFormat
XmirContext
IOFormat
$sel:_sugar:PrintCtx :: PrintContext -> SugarType
$sel:_hideRho:PrintCtx :: PrintContext -> Bool
$sel:_abridged:PrintCtx :: PrintContext -> Maybe Int
$sel:_abridgedData:PrintCtx :: PrintContext -> Bool
$sel:_line:PrintCtx :: PrintContext -> LineFormat
$sel:_margin:PrintCtx :: PrintContext -> Int
$sel:_xmirCtx:PrintCtx :: PrintContext -> XmirContext
$sel:_nonumber:PrintCtx :: PrintContext -> Bool
$sel:_compress:PrintCtx :: PrintContext -> Bool
$sel:_canonize:PrintCtx :: PrintContext -> Bool
$sel:_sequence:PrintCtx :: PrintContext -> Bool
$sel:_headers:PrintCtx :: PrintContext -> Bool
$sel:_meetPopularity:PrintCtx :: PrintContext -> Int
$sel:_meetLength:PrintCtx :: PrintContext -> Int
$sel:_focus:PrintCtx :: PrintContext -> Expression
$sel:_expression:PrintCtx :: PrintContext -> Maybe FilePath
$sel:_label:PrintCtx :: PrintContext -> Maybe FilePath
$sel:_meetPrefix:PrintCtx :: PrintContext -> Maybe FilePath
$sel:_outputFormat:PrintCtx :: PrintContext -> IOFormat
_sugar :: SugarType
_hideRho :: Bool
_abridged :: Maybe Int
_abridgedData :: Bool
_line :: LineFormat
_margin :: Int
_xmirCtx :: XmirContext
_nonumber :: Bool
_compress :: Bool
_canonize :: Bool
_sequence :: Bool
_headers :: Bool
_meetPopularity :: Int
_meetLength :: Int
_focus :: Expression
_expression :: Maybe FilePath
_label :: Maybe FilePath
_meetPrefix :: Maybe FilePath
_outputFormat :: IOFormat
..} Expression
expr
  | Expression
_focus Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
== Expression
ExRoot = PrintContext -> Expression -> IO FilePath
printInFormat PrintContext
ctx Expression
expr
  | Bool
otherwise = Expression -> Expression -> IO Expression
locatedExpression Expression
_focus Expression
expr IO Expression -> (Expression -> IO FilePath) -> IO FilePath
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= PrintContext -> Expression -> IO FilePath
printExpression PrintContext
ctx

filteredAt :: Expression -> Expression -> [Expression] -> [Expression] -> Expression -> IO Expression
filteredAt :: Expression
-> Expression
-> [Expression]
-> [Expression]
-> Expression
-> IO Expression
filteredAt Expression
locator Expression
universe [Expression]
excluded [Expression]
included Expression
answer = do
  Expression
placed <- Expression -> Expression -> Expression -> IO Expression
withLocatedExpression Expression
locator Expression
answer Expression
universe
  Expression
shown <- Expression -> [Expression] -> IO Expression
F.exclude' Expression
placed [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)
  Expression -> Expression -> IO Expression
locatedExpression Expression
locator Expression
shown

printExpression :: PrintContext -> Expression -> IO String
printExpression :: PrintContext -> Expression -> IO FilePath
printExpression ctx :: PrintContext
ctx@PrintCtx{Bool
Int
Maybe Int
Maybe FilePath
Expression
SugarType
LineFormat
XmirContext
IOFormat
$sel:_sugar:PrintCtx :: PrintContext -> SugarType
$sel:_hideRho:PrintCtx :: PrintContext -> Bool
$sel:_abridged:PrintCtx :: PrintContext -> Maybe Int
$sel:_abridgedData:PrintCtx :: PrintContext -> Bool
$sel:_line:PrintCtx :: PrintContext -> LineFormat
$sel:_margin:PrintCtx :: PrintContext -> Int
$sel:_xmirCtx:PrintCtx :: PrintContext -> XmirContext
$sel:_nonumber:PrintCtx :: PrintContext -> Bool
$sel:_compress:PrintCtx :: PrintContext -> Bool
$sel:_canonize:PrintCtx :: PrintContext -> Bool
$sel:_sequence:PrintCtx :: PrintContext -> Bool
$sel:_headers:PrintCtx :: PrintContext -> Bool
$sel:_meetPopularity:PrintCtx :: PrintContext -> Int
$sel:_meetLength:PrintCtx :: PrintContext -> Int
$sel:_focus:PrintCtx :: PrintContext -> Expression
$sel:_expression:PrintCtx :: PrintContext -> Maybe FilePath
$sel:_label:PrintCtx :: PrintContext -> Maybe FilePath
$sel:_meetPrefix:PrintCtx :: PrintContext -> Maybe FilePath
$sel:_outputFormat:PrintCtx :: PrintContext -> IOFormat
_sugar :: SugarType
_hideRho :: Bool
_abridged :: Maybe Int
_abridgedData :: Bool
_line :: LineFormat
_margin :: Int
_xmirCtx :: XmirContext
_nonumber :: Bool
_compress :: Bool
_canonize :: Bool
_sequence :: Bool
_headers :: Bool
_meetPopularity :: Int
_meetLength :: Int
_focus :: Expression
_expression :: Maybe FilePath
_label :: Maybe FilePath
_meetPrefix :: Maybe FilePath
_outputFormat :: IOFormat
..} Expression
ex = case IOFormat
_outputFormat of
  IOFormat
PHI -> FilePath -> IO FilePath
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PrintContext -> Expression -> FilePath
printPhi PrintContext
ctx Expression
ex)
  IOFormat
XMIR -> CmdException -> IO FilePath
forall e a. Exception e => e -> IO a
throwIO CmdException
CouldNotPrintExpressionInXMIR
  IOFormat
LATEX -> FilePath -> IO FilePath
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression -> LatexContext -> FilePath
expressionToLaTeX Expression
ex (PrintContext -> LatexContext
printCtxToLatexCtx PrintContext
ctx))

printInFormat :: PrintContext -> Expression -> IO String
printInFormat :: PrintContext -> Expression -> IO FilePath
printInFormat ctx :: PrintContext
ctx@PrintCtx{Bool
Int
Maybe Int
Maybe FilePath
Expression
SugarType
LineFormat
XmirContext
IOFormat
$sel:_sugar:PrintCtx :: PrintContext -> SugarType
$sel:_hideRho:PrintCtx :: PrintContext -> Bool
$sel:_abridged:PrintCtx :: PrintContext -> Maybe Int
$sel:_abridgedData:PrintCtx :: PrintContext -> Bool
$sel:_line:PrintCtx :: PrintContext -> LineFormat
$sel:_margin:PrintCtx :: PrintContext -> Int
$sel:_xmirCtx:PrintCtx :: PrintContext -> XmirContext
$sel:_nonumber:PrintCtx :: PrintContext -> Bool
$sel:_compress:PrintCtx :: PrintContext -> Bool
$sel:_canonize:PrintCtx :: PrintContext -> Bool
$sel:_sequence:PrintCtx :: PrintContext -> Bool
$sel:_headers:PrintCtx :: PrintContext -> Bool
$sel:_meetPopularity:PrintCtx :: PrintContext -> Int
$sel:_meetLength:PrintCtx :: PrintContext -> Int
$sel:_focus:PrintCtx :: PrintContext -> Expression
$sel:_expression:PrintCtx :: PrintContext -> Maybe FilePath
$sel:_label:PrintCtx :: PrintContext -> Maybe FilePath
$sel:_meetPrefix:PrintCtx :: PrintContext -> Maybe FilePath
$sel:_outputFormat:PrintCtx :: PrintContext -> IOFormat
_sugar :: SugarType
_hideRho :: Bool
_abridged :: Maybe Int
_abridgedData :: Bool
_line :: LineFormat
_margin :: Int
_xmirCtx :: XmirContext
_nonumber :: Bool
_compress :: Bool
_canonize :: Bool
_sequence :: Bool
_headers :: Bool
_meetPopularity :: Int
_meetLength :: Int
_focus :: Expression
_expression :: Maybe FilePath
_label :: Maybe FilePath
_meetPrefix :: Maybe FilePath
_outputFormat :: IOFormat
..} Expression
expr = case IOFormat
_outputFormat of
  IOFormat
PHI -> FilePath -> IO FilePath
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PrintContext -> Expression -> FilePath
printPhi PrintContext
ctx Expression
expr)
  IOFormat
XMIR -> Expression -> XmirContext -> IO Document
expressionToXMIR Expression
expr XmirContext
_xmirCtx IO Document -> (Document -> FilePath) -> IO FilePath
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> Document -> FilePath
printXMIR
  IOFormat
LATEX -> FilePath -> IO FilePath
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression -> LatexContext -> FilePath
expressionToLaTeX Expression
expr (PrintContext -> LatexContext
printCtxToLatexCtx PrintContext
ctx))

printPhi :: PrintContext -> Expression -> String
printPhi :: PrintContext -> Expression -> FilePath
printPhi PrintCtx{Bool
Int
Maybe Int
Maybe FilePath
Expression
SugarType
LineFormat
XmirContext
IOFormat
$sel:_sugar:PrintCtx :: PrintContext -> SugarType
$sel:_hideRho:PrintCtx :: PrintContext -> Bool
$sel:_abridged:PrintCtx :: PrintContext -> Maybe Int
$sel:_abridgedData:PrintCtx :: PrintContext -> Bool
$sel:_line:PrintCtx :: PrintContext -> LineFormat
$sel:_margin:PrintCtx :: PrintContext -> Int
$sel:_xmirCtx:PrintCtx :: PrintContext -> XmirContext
$sel:_nonumber:PrintCtx :: PrintContext -> Bool
$sel:_compress:PrintCtx :: PrintContext -> Bool
$sel:_canonize:PrintCtx :: PrintContext -> Bool
$sel:_sequence:PrintCtx :: PrintContext -> Bool
$sel:_headers:PrintCtx :: PrintContext -> Bool
$sel:_meetPopularity:PrintCtx :: PrintContext -> Int
$sel:_meetLength:PrintCtx :: PrintContext -> Int
$sel:_focus:PrintCtx :: PrintContext -> Expression
$sel:_expression:PrintCtx :: PrintContext -> Maybe FilePath
$sel:_label:PrintCtx :: PrintContext -> Maybe FilePath
$sel:_meetPrefix:PrintCtx :: PrintContext -> Maybe FilePath
$sel:_outputFormat:PrintCtx :: PrintContext -> IOFormat
_sugar :: SugarType
_hideRho :: Bool
_abridged :: Maybe Int
_abridgedData :: Bool
_line :: LineFormat
_margin :: Int
_xmirCtx :: XmirContext
_nonumber :: Bool
_compress :: Bool
_canonize :: Bool
_sequence :: Bool
_headers :: Bool
_meetPopularity :: Int
_meetLength :: Int
_focus :: Expression
_expression :: Maybe FilePath
_label :: Maybe FilePath
_meetPrefix :: Maybe FilePath
_outputFormat :: IOFormat
..} Expression
expr = Expression -> PrintConfig -> FilePath
P.printExpression' (if Bool
_hideRho then Expression -> Expression
rholess Expression
expr else Expression
expr) (SugarType
_sugar, Encoding
UNICODE, LineFormat
_line, Int
_margin)
  where
    rholess :: Expression -> Expression
    rholess :: Expression -> Expression
rholess (ExFormation [Binding]
bds) = [Binding] -> Expression
ExFormation [Binding -> Binding
binding Binding
bd | Binding
bd <- [Binding]
bds, Bool -> Bool
not (Binding -> Bool
rho Binding
bd)]
    rholess (ExDispatch Expression
inner Attribute
attr) = Expression -> Attribute -> Expression
ExDispatch (Expression -> Expression
rholess Expression
inner) Attribute
attr
    rholess (ExApplication Expression
inner (ArTau Attribute
AtRho Expression
_)) = Expression -> Expression
rholess Expression
inner
    rholess (ExApplication Expression
inner (ArTau Attribute
attr Expression
arg)) = Expression -> Argument -> Expression
ExApplication (Expression -> Expression
rholess Expression
inner) (Attribute -> Expression -> Argument
ArTau Attribute
attr (Expression -> Expression
rholess Expression
arg))
    rholess (ExApplication Expression
inner (ArAlpha Alpha
alpha Expression
arg)) = Expression -> Argument -> Expression
ExApplication (Expression -> Expression
rholess Expression
inner) (Alpha -> Expression -> Argument
ArAlpha Alpha
alpha (Expression -> Expression
rholess Expression
arg))
    rholess (ExPhiMeet Maybe FilePath
prefix Int
idx Expression
inner) = Maybe FilePath -> Int -> Expression -> Expression
ExPhiMeet Maybe FilePath
prefix Int
idx (Expression -> Expression
rholess Expression
inner)
    rholess (ExPhiAgain Maybe FilePath
prefix Int
idx Expression
inner) = Maybe FilePath -> Int -> Expression -> Expression
ExPhiAgain Maybe FilePath
prefix Int
idx (Expression -> Expression
rholess Expression
inner)
    rholess Expression
other = Expression
other
    binding :: Binding -> Binding
    binding :: Binding -> Binding
binding (BiTau Attribute
attr Expression
inner) = Attribute -> Expression -> Binding
BiTau Attribute
attr (Expression -> Expression
rholess Expression
inner)
    binding Binding
other = Binding
other
    rho :: Binding -> Bool
    rho :: Binding -> Bool
rho (BiTau Attribute
AtRho Expression
_) = Bool
True
    rho (BiVoid Attribute
AtRho) = Bool
True
    rho Binding
_ = Bool
False

hidden :: PrintContext -> SugarType -> EXPRESSION -> EXPRESSION
hidden :: PrintContext -> SugarType -> EXPRESSION -> EXPRESSION
hidden PrintCtx{Bool
Int
Maybe Int
Maybe FilePath
Expression
SugarType
LineFormat
XmirContext
IOFormat
$sel:_sugar:PrintCtx :: PrintContext -> SugarType
$sel:_hideRho:PrintCtx :: PrintContext -> Bool
$sel:_abridged:PrintCtx :: PrintContext -> Maybe Int
$sel:_abridgedData:PrintCtx :: PrintContext -> Bool
$sel:_line:PrintCtx :: PrintContext -> LineFormat
$sel:_margin:PrintCtx :: PrintContext -> Int
$sel:_xmirCtx:PrintCtx :: PrintContext -> XmirContext
$sel:_nonumber:PrintCtx :: PrintContext -> Bool
$sel:_compress:PrintCtx :: PrintContext -> Bool
$sel:_canonize:PrintCtx :: PrintContext -> Bool
$sel:_sequence:PrintCtx :: PrintContext -> Bool
$sel:_headers:PrintCtx :: PrintContext -> Bool
$sel:_meetPopularity:PrintCtx :: PrintContext -> Int
$sel:_meetLength:PrintCtx :: PrintContext -> Int
$sel:_focus:PrintCtx :: PrintContext -> Expression
$sel:_expression:PrintCtx :: PrintContext -> Maybe FilePath
$sel:_label:PrintCtx :: PrintContext -> Maybe FilePath
$sel:_meetPrefix:PrintCtx :: PrintContext -> Maybe FilePath
$sel:_outputFormat:PrintCtx :: PrintContext -> IOFormat
_sugar :: SugarType
_hideRho :: Bool
_abridged :: Maybe Int
_abridgedData :: Bool
_line :: LineFormat
_margin :: Int
_xmirCtx :: XmirContext
_nonumber :: Bool
_compress :: Bool
_canonize :: Bool
_sequence :: Bool
_headers :: Bool
_meetPopularity :: Int
_meetLength :: Int
_focus :: Expression
_expression :: Maybe FilePath
_label :: Maybe FilePath
_meetPrefix :: Maybe FilePath
_outputFormat :: IOFormat
..} SugarType
sugar
  | Bool
_hideRho = SugarType -> EXPRESSION -> EXPRESSION
withoutRho SugarType
sugar
  | Bool
otherwise = EXPRESSION -> EXPRESSION
forall a. a -> a
id

printCtxToLatexCtx :: PrintContext -> LatexContext
printCtxToLatexCtx :: PrintContext -> LatexContext
printCtxToLatexCtx PrintCtx{Bool
Int
Maybe Int
Maybe FilePath
Expression
SugarType
LineFormat
XmirContext
IOFormat
$sel:_sugar:PrintCtx :: PrintContext -> SugarType
$sel:_hideRho:PrintCtx :: PrintContext -> Bool
$sel:_abridged:PrintCtx :: PrintContext -> Maybe Int
$sel:_abridgedData:PrintCtx :: PrintContext -> Bool
$sel:_line:PrintCtx :: PrintContext -> LineFormat
$sel:_margin:PrintCtx :: PrintContext -> Int
$sel:_xmirCtx:PrintCtx :: PrintContext -> XmirContext
$sel:_nonumber:PrintCtx :: PrintContext -> Bool
$sel:_compress:PrintCtx :: PrintContext -> Bool
$sel:_canonize:PrintCtx :: PrintContext -> Bool
$sel:_sequence:PrintCtx :: PrintContext -> Bool
$sel:_headers:PrintCtx :: PrintContext -> Bool
$sel:_meetPopularity:PrintCtx :: PrintContext -> Int
$sel:_meetLength:PrintCtx :: PrintContext -> Int
$sel:_focus:PrintCtx :: PrintContext -> Expression
$sel:_expression:PrintCtx :: PrintContext -> Maybe FilePath
$sel:_label:PrintCtx :: PrintContext -> Maybe FilePath
$sel:_meetPrefix:PrintCtx :: PrintContext -> Maybe FilePath
$sel:_outputFormat:PrintCtx :: PrintContext -> IOFormat
_sugar :: SugarType
_hideRho :: Bool
_abridged :: Maybe Int
_abridgedData :: Bool
_line :: LineFormat
_margin :: Int
_xmirCtx :: XmirContext
_nonumber :: Bool
_compress :: Bool
_canonize :: Bool
_sequence :: Bool
_headers :: Bool
_meetPopularity :: Int
_meetLength :: Int
_focus :: Expression
_expression :: Maybe FilePath
_label :: Maybe FilePath
_meetPrefix :: Maybe FilePath
_outputFormat :: IOFormat
..} =
  SugarType
-> LineFormat
-> Int
-> Bool
-> Bool
-> Bool
-> Int
-> Int
-> Expression
-> Maybe FilePath
-> Maybe FilePath
-> Maybe FilePath
-> Bool
-> Bool
-> LatexContext
LatexContext SugarType
_sugar LineFormat
_line Int
_margin Bool
_nonumber Bool
_compress Bool
_canonize Int
_meetPopularity Int
_meetLength Expression
_focus Maybe FilePath
_expression Maybe FilePath
_label Maybe FilePath
_meetPrefix Bool
_headers Bool
_hideRho

getRules :: Bool -> Bool -> [FilePath] -> IO [Y.Rule]
getRules :: Bool -> Bool -> [FilePath] -> IO [Rule]
getRules Bool
normalize Bool
shuffle [FilePath]
rules = do
  [Rule]
ordered <- [Rule] -> [Rule] -> [Rule]
forall a. [a] -> [a] -> [a]
(++) ([Rule] -> [Rule] -> [Rule]) -> IO [Rule] -> IO ([Rule] -> [Rule])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO [Rule]
builtin IO ([Rule] -> [Rule]) -> IO [Rule] -> IO [Rule]
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> IO [Rule]
custom
  if Bool
shuffle
    then do
      FilePath -> IO ()
logDebug FilePath
"The --shuffle option is provided, rules are used in random order"
      [Rule] -> IO [Rule]
forall a. [a] -> IO [a]
R.shuffle [Rule]
ordered
    else [Rule] -> IO [Rule]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Rule]
ordered
  where
    builtin :: IO [Y.Rule]
    builtin :: IO [Rule]
builtin
      | Bool
normalize = do
          FilePath -> IO ()
logDebug (FilePath -> Int -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"The --normalize option is provided, %d built-it normalization rules are used" ([Rule] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Rule]
normalizationRules))
          [Rule] -> IO [Rule]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Rule]
normalizationRules
      | Bool
otherwise = [Rule] -> IO [Rule]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    custom :: IO [Y.Rule]
    custom :: IO [Rule]
custom
      | [FilePath] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FilePath]
rules = do
          FilePath -> IO ()
logDebug FilePath
"No --rule option is provided, no user rules are used"
          [Rule] -> IO [Rule]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
      | Bool
otherwise = do
          FilePath -> IO ()
logDebug (FilePath -> FilePath -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"Using rules from files: [%s]" (FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate FilePath
", " [FilePath]
rules))
          [FilePath]
yamls <- (FilePath -> IO FilePath) -> [FilePath] -> IO [FilePath]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM FilePath -> IO FilePath
ensuredFile ([FilePath] -> [FilePath]
forall a. Eq a => [a] -> [a]
nub [FilePath]
rules)
          (FilePath -> IO Rule) -> [FilePath] -> IO [Rule]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (FilePath -> IO Rule
loadRule (FilePath -> IO Rule) -> (Rule -> IO Rule) -> FilePath -> IO Rule
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Rule -> IO Rule
validateRewriteRule) [FilePath]
yamls

loadRule :: FilePath -> IO Y.Rule
loadRule :: FilePath -> IO Rule
loadRule FilePath
file =
  IO Rule -> (ParseException -> IO Rule) -> IO Rule
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
catch (FilePath -> IO Rule
Y.yamlRule FilePath
file) ParseException -> IO Rule
reportInvalidRule
  where
    reportInvalidRule :: Yaml.ParseException -> IO Y.Rule
    reportInvalidRule :: ParseException -> IO Rule
reportInvalidRule ParseException
err =
      FilePath -> IO Rule
forall a. FilePath -> IO a
invalidCLIArguments (FilePath -> FilePath -> FilePath -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"Could not load rule from '%s'\n%s" FilePath
file (FilePath -> FilePath
Y.shiftYamlError (ParseException -> FilePath
Yaml.prettyPrintParseException ParseException
err)))

validateRewriteRule :: Y.Rule -> IO Y.Rule
validateRewriteRule :: Rule -> IO Rule
validateRewriteRule Rule
rule =
  let used :: [FilePath]
used = [FilePath]
-> ([Extra] -> [FilePath]) -> Maybe [Extra] -> [FilePath]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] ((Extra -> FilePath) -> [Extra] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map Extra -> FilePath
Y.function) Rule
rule.where_
   in case (FilePath -> Bool) -> [FilePath] -> [FilePath]
forall a. (a -> Bool) -> [a] -> [a]
filter (\FilePath
fn -> FilePath
fn FilePath -> [FilePath] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` ([FilePath]
buildFunctions [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ [FilePath]
execFunctions)) [FilePath]
used of
        (FilePath
fn : [FilePath]
_) -> FilePath -> IO Rule
forall a. FilePath -> IO a
invalidCLIArguments (FilePath -> FilePath -> FilePath -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"Function '%s' in rule '%s' is not supported" FilePath
fn Rule
rule.name)
        [] -> case (FilePath -> Bool) -> [FilePath] -> [FilePath]
forall a. (a -> Bool) -> [a] -> [a]
filter (FilePath -> [FilePath] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [FilePath]
execFunctions) [FilePath]
used of
          [] -> Rule -> IO Rule
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Rule
rule
          (FilePath
fn : [FilePath]
_) ->
            FilePath -> IO Rule
forall a. FilePath -> IO a
invalidCLIArguments
              (FilePath -> FilePath -> FilePath -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"Function '%s' in rule '%s' is available only for dataization and morphing, not for rewriting" FilePath
fn Rule
rule.name)

printOut :: Maybe FilePath -> String -> IO ()
printOut :: Maybe FilePath -> FilePath -> IO ()
printOut Maybe FilePath
target FilePath
content = case Maybe FilePath
target of
  Maybe FilePath
Nothing -> do
    FilePath -> IO ()
logDebug FilePath
"The option '--target' is not specified, printing to console..."
    FilePath -> IO ()
putStrLn FilePath
content
  Just FilePath
file -> do
    FilePath -> IO ()
logDebug (FilePath -> FilePath -> FilePath
forall r. PrintfType r => FilePath -> r
printf FilePath
"The option '--target' is specified, printing to '%s'..." FilePath
file)
    FilePath -> FilePath -> IO ()
overwrite FilePath
file (FilePath
content 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)

engine :: IO Engine
engine :: IO Engine
engine = case Maybe Engine
compiled of
  Maybe Engine
Nothing -> Engine -> IO Engine
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Engine
yaml
  Just Engine
linked
    | Engine -> Bool
fresh Engine
linked -> FilePath -> IO ()
logDebug FilePath
"The built-in rules run compiled, as 'phino compile' wrote them" IO () -> IO Engine -> IO Engine
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Engine -> IO Engine
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Engine
linked
    | Bool
otherwise -> CmdException -> IO Engine
forall e a. Exception e => e -> IO a
throwIO CmdException
StaleEngine