content: {- |
  Copyright   : (c) Runtime Verification, 2018-2021
  License     : BSD-3-Clause
  -}
  module Kore.Simplify.Pattern (
      simplifyTopConfiguration,
      simplifyTopConfigurationDefined,
      simplify,
      makeEvaluate,
  ) where
  
  import Control.Monad (
      (>=>),
   )
  import Kore.Internal.Conditional qualified as Conditional
  import Kore.Internal.OrPattern (
      OrPattern,
   )
  import Kore.Internal.OrPattern qualified as OrPattern
  import Kore.Internal.Pattern (
      Condition,
      Conditional (..),
      Pattern,
   )
  import Kore.Internal.Pattern qualified as Pattern
  import Kore.Internal.Predicate (
      makeCeilPredicate,
   )
  import Kore.Internal.SideCondition (
      SideCondition,
   )
  import Kore.Internal.SideCondition qualified as SideCondition (
      addConditionWithReplacements,
      assumeDefined,
      top,
   )
  import Kore.Internal.Substitution (
      toMap,
   )
  import Kore.Internal.TermLike (
      pattern Exists_,
   )
  import Kore.Rewrite.RewritingVariable (
      RewritingVariableName,
   )
  import Kore.Simplify.Simplify (
      Simplifier,
      liftSimplifier,
      simplifyCondition,
      simplifyTerm,
   )
  import Kore.Substitute
  import Logic qualified
  import Prelude.Kore
  
  -- | Simplifies the 'Pattern' and removes the exists quantifiers at the top.
  simplifyTopConfiguration ::
      Pattern RewritingVariableName ->
      Simplifier (OrPattern RewritingVariableName)
  simplifyTopConfiguration =
      simplify >=> return . removeTopExists
  
  {- | Simplifies the 'Pattern', with the assumption that the term is defined,
  and removes the exists quantifiers at the top.
  -}
  simplifyTopConfigurationDefined ::
      Pattern RewritingVariableName ->
      Simplifier (OrPattern RewritingVariableName)
  simplifyTopConfigurationDefined configuration =
      maybe
          (return OrPattern.bottom)
          (worker definedConfiguration)
          sideCondition
    where
      worker patt condition =
          makeEvaluate condition patt
              >>= return . removeTopExists
  
      term = Conditional.term configuration
      sideCondition = SideCondition.assumeDefined term
      definedConfiguration =
          makeCeilPredicate term
              & from @_ @(Condition _)
              & Pattern.andCondition configuration
  
  -- | Removes all existential quantifiers at the top of every 'Pattern''s 'term'.
  removeTopExists ::
      OrPattern RewritingVariableName ->
      OrPattern RewritingVariableName
  removeTopExists = OrPattern.map removeTopExistsWorker
    where
      removeTopExistsWorker ::
          Pattern RewritingVariableName ->
          Pattern RewritingVariableName
      removeTopExistsWorker p@Conditional{term = Exists_ _ _ quantified} =
          removeTopExistsWorker p{term = quantified}
      removeTopExistsWorker p = p
  
  -- | Simplifies an 'Pattern', returning an 'OrPattern'.
  simplify ::
      Pattern RewritingVariableName ->
      Simplifier (OrPattern RewritingVariableName)
  simplify = makeEvaluate SideCondition.top
  
  {- | Simplifies a 'Pattern' with a custom 'SideCondition'.
  This should only be used when it's certain that the
  'SideCondition' was not created from the 'Condition' of
  the 'Pattern'.
  -}
  makeEvaluate ::
      SideCondition RewritingVariableName ->
      Pattern RewritingVariableName ->
      Simplifier (OrPattern RewritingVariableName)
  makeEvaluate sideCondition =
      loop . OrPattern.fromPattern
    where
      loop input = do
          output <-
              OrPattern.traverse worker input
                  & fmap OrPattern.flatten
          if input == output
              then pure output
              else loop output
  
      worker pattern' =
          OrPattern.observeAllT $ do
              withSimplifiedCondition <-
                  simplifyCondition sideCondition pattern'
              let (term, simplifiedCondition) =
                      Conditional.splitTerm withSimplifiedCondition
                  term' = substitute (toMap $ substitution simplifiedCondition) term
                  termSideCondition =
                      SideCondition.addConditionWithReplacements
                          simplifiedCondition
                          sideCondition
              simplifiedTerm <-
                  liftSimplifier (simplifyTerm termSideCondition term')
                      >>= Logic.scatter
              let simplifiedPattern =
                      Conditional.andCondition simplifiedTerm simplifiedCondition
              simplifyCondition sideCondition simplifiedPattern
  