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

module CLI.Validators where

import AST
import CLI.Types
import Control.Exception
import Control.Monad (forM_, unless, when, (>=>))
import Data.Char (isAlphaNum)
import Data.Foldable (for_)
import Data.List (isPrefixOf)
import Data.Maybe (isJust)
import Misc (fqnToAttrs)
import Must
import Parser (parseExpressionThrows)
import Printer
import Sugar (revealXi)
import Text.Printf (printf)

invalidCLIArguments :: String -> IO a
invalidCLIArguments :: forall a. String -> IO a
invalidCLIArguments String
msg = CmdException -> IO a
forall e a. Exception e => e -> IO a
throwIO (String -> CmdException
InvalidCLIArguments String
msg)

validatedDispatches :: String -> [String] -> IO [Expression]
validatedDispatches :: String -> [String] -> IO [Expression]
validatedDispatches String
opt = (String -> IO Expression) -> [String] -> IO [Expression]
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 (String -> IO Expression
parseExpressionThrows (String -> IO Expression)
-> (Expression -> IO Expression) -> String -> IO Expression
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Expression -> IO Expression
asDispatch)
  where
    asDispatch :: Expression -> IO Expression
    asDispatch :: Expression -> IO Expression
asDispatch Expression
expr = Expression -> IO Expression
go Expression
expr
      where
        go :: Expression -> IO Expression
        go :: Expression -> IO Expression
go ex :: Expression
ex@Expression
ExRoot = Expression -> IO Expression
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expression
ex
        go disp :: Expression
disp@(ExDispatch Expression
ex Attribute
_) = Expression -> IO Expression
go Expression
ex IO Expression -> IO Expression -> IO Expression
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Expression -> IO Expression
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expression
disp
        go Expression
_ =
          String -> IO Expression
forall a. String -> IO a
invalidCLIArguments
            ( String -> String -> String -> String
forall r. PrintfType r => String -> r
printf
                String
"Only dispatch expression started with Φ (or Q) can be used in --%s, but given: %s"
                String
opt
                ((SugarType -> EXPRESSION -> EXPRESSION)
-> Expression -> PrintConfig -> String
printExpressionWith SugarType -> EXPRESSION -> EXPRESSION
revealXi Expression
expr PrintConfig
logPrintConfig)
            )

validateNoOverlap :: String -> [Expression] -> String -> [Expression] -> IO ()
validateNoOverlap :: String -> [Expression] -> String -> [Expression] -> IO ()
validateNoOverlap String
showOpt [Expression]
shown String
hideOpt [Expression]
hidden =
  [Expression] -> (Expression -> IO ()) -> IO ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [Expression]
shown ((Expression -> IO ()) -> IO ()) -> (Expression -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Expression
shown' ->
    [Expression] -> (Expression -> IO ()) -> IO ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [Expression]
hidden ((Expression -> IO ()) -> IO ()) -> (Expression -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Expression
hidden' -> do
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Expression -> String
printExpression Expression
shown' String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Expression -> String
printExpression Expression
hidden') (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
        String -> IO ()
forall a. String -> IO a
invalidCLIArguments
          ( String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf
              String
"The --%s locator '%s' is also listed in --%s, which would hide it from the result"
              String
showOpt
              (Expression -> String
printExpression Expression
shown')
              String
hideOpt
          )
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Maybe [Attribute] -> Maybe [Attribute] -> Bool
inside (Expression -> Maybe [Attribute]
fqnToAttrs Expression
shown') (Expression -> Maybe [Attribute]
fqnToAttrs Expression
hidden')) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
        String -> IO ()
forall a. String -> IO a
invalidCLIArguments
          ( String -> String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf
              String
"The --%s locator '%s' lies inside the --%s locator '%s', which would hide it from the result"
              String
showOpt
              (Expression -> String
printExpression Expression
shown')
              String
hideOpt
              (Expression -> String
printExpression Expression
hidden')
          )
  where
    inside :: Maybe [Attribute] -> Maybe [Attribute] -> Bool
    inside :: Maybe [Attribute] -> Maybe [Attribute] -> Bool
inside (Just [Attribute]
inner) (Just [Attribute]
outer) = [Attribute] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Attribute]
outer Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [Attribute] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Attribute]
inner Bool -> Bool -> Bool
&& [Attribute]
outer [Attribute] -> [Attribute] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` [Attribute]
inner
    inside Maybe [Attribute]
_ Maybe [Attribute]
_ = Bool
False

validateLatexOptions :: IOFormat -> [(Bool, String)] -> [(Maybe String, String)] -> [(Maybe Int, String)] -> IO ()
validateLatexOptions :: IOFormat
-> [(Bool, String)]
-> [(Maybe String, String)]
-> [(Maybe Int, String)]
-> IO ()
validateLatexOptions IOFormat
LATEX [(Bool, String)]
_ [(Maybe String, String)]
strings [(Maybe Int, String)]
_ = [(Maybe String, String)]
-> ((Maybe String, String) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Maybe String, String)]
strings (Maybe String, String) -> IO ()
forall {t :: * -> *}.
Foldable t =>
(Maybe (t Char), String) -> IO ()
validateLatexString
  where
    validateLatexString :: (Maybe (t Char), String) -> IO ()
validateLatexString (Just t Char
label, String
"label") =
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ((Char -> Bool) -> t Char -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
safeLabelCharacter t Char
label) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
        String -> IO ()
forall a. String -> IO a
invalidCLIArguments
          String
"The --label option must contain only letters, numbers, colons, periods, underscores, and hyphens"
    validateLatexString (Maybe (t Char), String)
_ = () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    safeLabelCharacter :: Char -> Bool
safeLabelCharacter Char
character = Char -> Bool
isAlphaNum Char
character Bool -> Bool -> Bool
|| Char
character Char -> String -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
":._-"
validateLatexOptions IOFormat
_ [(Bool, String)]
bools [(Maybe String, String)]
strings [(Maybe Int, String)]
ints = do
  let ([Bool]
bools', [String]
opts) = [(Bool, String)] -> ([Bool], [String])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Bool, String)]
bools
      msg :: String
msg = String
"The --%s option can stay together with --output=latex only"
      callback :: (Maybe a, String) -> IO ()
      callback :: forall a. (Maybe a, String) -> IO ()
callback (Maybe a
maybe', String
opt) = Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Maybe a -> Bool
forall a. Maybe a -> Bool
isJust Maybe a
maybe') (String -> IO ()
forall a. String -> IO a
invalidCLIArguments (String -> String -> String
forall r. PrintfType r => String -> r
printf String
msg String
opt))
  [(Bool, String)] -> IO ()
validateBoolOpts ([Bool] -> [String] -> [(Bool, String)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Bool]
bools' ((String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> String -> String
forall r. PrintfType r => String -> r
printf String
msg) [String]
opts))
  [(Maybe String, String)]
-> ((Maybe String, String) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Maybe String, String)]
strings (Maybe String, String) -> IO ()
forall a. (Maybe a, String) -> IO ()
callback
  [(Maybe Int, String)] -> ((Maybe Int, String) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Maybe Int, String)]
ints (Maybe Int, String) -> IO ()
forall a. (Maybe a, String) -> IO ()
callback

validateMust' :: Must -> IO ()
validateMust' :: Must -> IO ()
validateMust' Must
must = Maybe String -> (String -> IO Any) -> IO ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ (Must -> Maybe String
validateMust Must
must) String -> IO Any
forall a. String -> IO a
invalidCLIArguments

validateXmirOptions :: IOFormat -> [(Bool, String)] -> String -> IO ()
validateXmirOptions :: IOFormat -> [(Bool, String)] -> String -> IO ()
validateXmirOptions IOFormat
XMIR [(Bool, String)]
_ String
focus = do
  Expression
parsed <- String -> IO Expression
parseExpressionThrows String
focus
  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) (String -> IO ()
forall a. String -> IO a
invalidCLIArguments String
"Only --focus=Q is allowed to be used with --output=xmir")
validateXmirOptions IOFormat
_ [(Bool, String)]
bools String
_ =
  let ([Bool]
bools', [String]
opts) = [(Bool, String)] -> ([Bool], [String])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Bool, String)]
bools
   in [(Bool, String)] -> IO ()
validateBoolOpts ([Bool] -> [String] -> [(Bool, String)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Bool]
bools' ((String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> String -> String
forall r. PrintfType r => String -> r
printf String
"The --%s can be used only with --output=xmir") [String]
opts))

validateXmirTopLevel :: IOFormat -> Expression -> IO ()
validateXmirTopLevel :: IOFormat -> Expression -> IO ()
validateXmirTopLevel IOFormat
XMIR (ExFormation (Binding
_ : [Binding]
_)) = () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
validateXmirTopLevel IOFormat
XMIR Expression
expr =
  String -> IO ()
forall a. String -> IO a
invalidCLIArguments
    ( String -> String -> String
forall r. PrintfType r => String -> r
printf
        String
"Expression cannot be printed with --output=xmir: its top level must be a formation with at least one binding, but got: %s"
        (Expression -> String
printExpression Expression
expr)
    )
validateXmirTopLevel IOFormat
_ Expression
_ = () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

validateBoolOpts :: [(Bool, String)] -> IO ()
validateBoolOpts :: [(Bool, String)] -> IO ()
validateBoolOpts [(Bool, String)]
bools = [(Bool, String)] -> ((Bool, String) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [(Bool, String)]
bools (\(Bool
bool, String
msg) -> Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
bool (String -> IO ()
forall a. String -> IO a
invalidCLIArguments String
msg))