content: {-# OPTIONS_GHC -Wno-orphans #-}
  {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
  
  {-# HLINT ignore "Use <$>" #-}
  
  module Vehicle.Compile.Print.Warning where
  
  import Data.Bifunctor (Bifunctor (..))
  import Data.List (sortOn)
  import Data.List.NonEmpty (NonEmpty, sort)
  import Data.List.NonEmpty qualified as NonEmpty
  import Data.Map qualified as Map
  import Data.Tuple (swap)
  import Vehicle.Data.Assertion (UnderConstrainedVariableStatus, prettyUnderConstrainedVariable)
  import Vehicle.Data.Tensor (TensorIndices)
  import Vehicle.Prelude
  import Vehicle.Prelude.Warning
  import Vehicle.Verify.Core
  
  instance Pretty SummarisedCompileWarning where
    pretty = \case
      UnusedResourcesSummary resourceType unusedResources ->
        "the following"
          <+> pretty resourceType
          <> "s were provided"
            <+> "but not used by the specification:"
            <+> prettySet unusedResources
      TrivialPropertySummary propertyName status ->
        "The property"
          <+> quotePretty propertyName
          <+> "was found to evaluate to"
          <+> quotePretty status
          <+> "without needing to call the verifier. This usually indicates a fault with either the"
          <+> "specification or any external datasets used."
      UnderSpecifiedProblemSpaceVariablesSummary _ propertyName unsolvedVars -> do
        "In property"
          <+> quotePretty propertyName
          <+> "there are quantified variables that not always directly related to the input or output of a network."
          <+> "This is frequently indicative of a bug in the specification. These variables are:"
          <> line
          <> prettyObjectsAndTensorIndicesList prettyVariables propertyName unsolvedVars
      UnsoundStrictOrderConversionsSummary queryFormatID _ propertyAddress _ ->
        "In property"
          <+> quotePretty propertyAddress
          <> ", at least one of the generated queries were found"
            <+> "to contain a strict inequality (i.e. constraints of the form 'x < y')."
            <+> "Unfortunately the"
            <+> pretty queryFormatID
            <+> "only supports non-strict"
            <+> "inequalities (i.e. constraints of the form 'x <= y')."
          <> line
          <> line
          <> "In order to provide support, Vehicle has automatically converted the"
            <+> "strict inequalities to non-strict inequalites."
            <+> "This is not sound, but errors will be at most the floating point epsilon"
            <+> "used by the verifier, which is usually very small (e.g. 1e-9)."
            <+> "However, this may lead to unexpected behaviour (e.g. loss of the law of excluded middle)."
          <> line
          <> line
          <> "See https://github.com/vehicle-lang/vehicle/issues/74 for further details."
      AllConstantNetworkInputVariablesSummary _ _ propertyName queryIDs ->
        "In some of the queries generated by property"
          <+> quotePretty propertyName
          <+> "all network inputs were fixed to be constants."
          <+> "Unfortunately there is a known bug in Marabou that it sometimes erroneously returns"
          <+> "'unsat' for these type of queries. The queries are:"
          <> line
          <> prettyObjectsAndTensorIndicesList prettyQueryIDs propertyName queryIDs
          <> line
          <> line
          <> "See https://github.com/NeuralNetworkVerification/Marabou/issues/670 for details."
      UnboundedNetworkInputVariablesSummary queryFormat _ propertyAddress varsByQueryID ->
        "In property"
          <+> quotePretty propertyAddress
          <> ", the following network input variables do not always have both"
            <+> "a lower and a upper bound."
            <+> "This is not currently supported by the"
            <+> pretty queryFormat
          <> "."
          <> line
          <> indent 2 (vsep $ fmap prettyQueries (sortOn (\(qs, _) -> sort qs) varsByQueryID))
        where
          prettyQueries :: (NonEmpty QueryID, [(Name, UnderConstrainedVariableStatus)]) -> Doc a
          prettyQueries (queryIDs, vars) =
            "In" <+> prettyQueryIDs queryIDs
              <> ":"
              <> line
              <> indent 2 (vsep $ dotDotList 5 $ fmap prettyUnderConstrainedVariable vars)
  
  prettyObjects :: (Ord a, Pretty a) => Bool -> Doc b -> Doc b -> NonEmpty a -> Doc b
  prettyObjects quote single plural ids =
    (if length ids == 1 then single else plural)
      <+> prettyNonEmptyList (fmap (if quote then quotePretty else pretty) (sort ids))
  
  prettyQueryIDs :: NonEmpty QueryID -> Doc b
  prettyQueryIDs = prettyObjects False "query" "queries"
  
  prettyVariables :: NonEmpty Name -> Doc a
  prettyVariables = prettyObjects True "variable" "variables"
  
  prettyTensorIndices :: PropertyName -> NonEmpty TensorIndices -> Maybe (Doc b)
  prettyTensorIndices name indices
    | indices == [[]] = Nothing
    | otherwise = do
        let addresses = fmap (quotePretty . PropertyAddress (-1) name) indices
        Just $ prettyNonEmptyList addresses
  
  prettyObjectsAndTensorIndices :: (NonEmpty a -> Doc b) -> PropertyName -> (NonEmpty a, NonEmpty TensorIndices) -> Doc b
  prettyObjectsAndTensorIndices prettyObject name (ids, indices) = do
    let indicesDoc = prettyTensorIndices name indices
    prettyObject ids <> maybe "" (" in" <+>) indicesDoc
  
  prettyObjectsAndTensorIndicesList :: (Ord a) => (NonEmpty a -> Doc b) -> PropertyName -> NonEmpty (a, TensorIndices) -> Doc b
  prettyObjectsAndTensorIndicesList prettyObject name objectsAndIndices = do
    -- Singleton.nonEmpty doesn't exist until base 4.15
    let nonEmptySingleton x = [x]
    -- First map by indices that share the same objects
    let indicesMap = Map.fromListWith (<>) (NonEmpty.toList $ fmap (second nonEmptySingleton) objectsAndIndices)
    -- Then find the objects that share the same queries
    let objectsMap = Map.fromListWith (<>) $ fmap (second nonEmptySingleton . swap) (Map.toList indicesMap)
    let finalGroups = fmap swap $ Map.toList objectsMap
    indent 2 (vsep (fmap (\x -> "-" <+> prettyObjectsAndTensorIndices prettyObject name x) finalGroups))
  