-- SPDX-FileCopyrightText: 2023 David Mosbach <david.mosbach@campus.lmu.de>
--
-- SPDX-License-Identifier: AGPL-3.0-or-later

{-# LANGUAGE OverloadedRecordDot, OverloadedStrings, NoFieldSelectors, DuplicateRecordFields, TupleSections #-}

module Transpiler where
  import DSL
  import Data.YAML (ToYAML (..), mapping, (.=))
  import Data.Text (Text, pack)
  import YamlParser (AnchorData (..))
  import Data.YAML.Event (ScalarStyle(Literal))
  import Control.Monad.State (State, evalState, get, put, unless, when)
  import Data.Map (Map, empty)
  import qualified Data.Map as M
  import Control.Monad.Except (ExceptT, runExceptT, throwError)
  import Data.Either (fromLeft)
  import Data.Maybe (fromJust, isNothing)
  

  data ResolvedLiteral = Pred' { pred :: Predicate }
                       | Neg' { pred :: Predicate }  deriving Show
  
  data DNFLiteral = DNFLit {
    anchor  :: AnchorData,
    literal :: ResolvedLiteral
  }

  type DNF = [[DNFLiteral]]
  
  instance ToYAML SubStage where
    toYAML(SubStage head body) = mapping [
        "mode"      .= if head.required then "required" else "optional" :: Text,
        "show-when" .= case head.showWhen of
                          Always      -> "always"
                          Fulfilled   -> "fulfilled"
                          Unfulfilled -> "unfulfilled" :: Text,
        "predicate" .= mapping [ "dnf-terms" .= ("" :: Text)] -- toYAML (resolve body) ]
      ]

  newtype ResolveError = ResolveError String

  data StateData = StateData {
    innerVariables :: Map String (Variable, Bool), -- True means "already used" => anchor ref. False means "not used before" => new anchor
    outerVariables :: Map String (Variable, Bool),
    disjunction    :: DNF
  }

  type Resolver = ExceptT ResolveError (State StateData) --(Either ResolveError)

  resolve :: Body -> Either ResolveError DNF
  resolve body = evalState (runExceptT (eval body)) initState
    where
      initState = StateData empty (M.map (, False) body.variables) []
  
  eval :: Body -> Resolver DNF
  eval (Body variables []) = get >>= \s -> return s.disjunction
  eval (Body variables (c:dnf)) = do
    conjunction <- evalConjunction c []
    state <- get
    put $ state {innerVariables = empty, disjunction = conjunction : state.disjunction}
    eval $ Body variables dnf
      where
        evalConjunction :: Conjunction -> [DNFLiteral] -> Resolver [DNFLiteral]
        evalConjunction [] acc = return acc
        evalConjunction (l:ls) acc = do
          lit <- evalLiteral l
          case lit of
            Left literal -> evalConjunction ls (literal : acc)
            Right block -> evalConjunction ls (block ++ acc) -- Merge content of block conjunction variables
        evalLiteral :: Literal -> Resolver (Either DNFLiteral [DNFLiteral])
        evalLiteral n@(Neg _) = Left <$> evalNegation n
        evalLiteral p@(Pred _) = Left <$> evalPredicate p
        evalLiteral v@(Var _) = evalVariable False v
        evalNegation :: Literal -> Resolver DNFLiteral -- Resolves redundant negations, e.g. `not not x` and also `let x = not y; let z = not x`
        evalNegation (Neg n) = do
          let (lit, count) = countNot 1 n
          lit' <- case lit of {
            Pred _ -> evalPredicate lit;
            Var _ -> evalVariable True lit >>= \l -> return $ fromLeft (error "Preventing negated blocks failed") l;
            Neg _ -> throwError . ResolveError $ "Could not resolve negation of: " ++ show n;
          }
          if even count then return lit' else do
            let sign = case lit'.literal of {
              Neg' _ -> Pred';
              Pred' _ -> Neg';
            }
            return lit' { literal = sign lit'.literal.pred }
        evalNegation x = throwError . ResolveError $ "Wrongfully labelt as negation:  " ++ show x
        countNot :: Word -> Literal -> (Literal, Word)
        countNot x (Neg n) = countNot (x+1) n
        countNot x lit = (lit, x)
        evalPredicate :: Literal -> Resolver DNFLiteral
        evalPredicate (Pred (EdgesInHistory _)) = undefined
        evalPredicate (Pred (NodesInHistory _)) = undefined
        evalPredicate (Pred (PayloadsFilled _)) = undefined
        evalPredicate (Pred (PreviousNodes _)) = undefined
        evalPredicate (Pred p) = return $ DNFLit { anchor = NoAnchor, literal = Pred' p }
        evalPredicate x = throwError . ResolveError $ "Wrongfully labelt as predicate: " ++ show x
        evalVariable :: Bool -> Literal -> Resolver (Either DNFLiteral [DNFLiteral])
        evalVariable negated (Var v) = do
          state <- get
          let maybeVar = M.lookup v state.innerVariables
          if isNothing maybeVar then throwError . ResolveError $ "Reference of unassigned variable: " ++ v else do
            let (var, alreadyUsed) = fromJust maybeVar
            unless alreadyUsed . put $ state { innerVariables = M.adjust (\(x,_) -> (x,True)) v state.innerVariables }
            let anchor = if alreadyUsed then AnchorAlias (pack v) else AnchorDef (pack v)
            case var of
              Single _ (Pred p) -> return $ Left DNFLit { anchor = anchor, literal = Pred' p }
              Single _ v'@(Var _) -> evalVariable negated v'
              Single _ n@(Neg _) -> Left <$> (evalNegation n >>= \x -> return $ if x.anchor == NoAnchor then x {anchor = anchor} else x)
              Block id conj -> preventBlockNegation negated id >> Right <$> evalConjunction conj []
        preventBlockNegation :: Bool -> String -> Resolver ()
        preventBlockNegation True s = throwError . ResolveError $ "Negating conjunction blocks is not permitted: " ++ s
        preventBlockNegation False _ = return ()



  instance ToYAML DNFLiteral where
    toYAML (DNFLit anchor literal) = mapping [
        -- "dnf-terms" .= toYAML
      ]