content: {- |
  Module      : Kore.Attribute.Axiom
  Description : Axiom sentence attributes
  Copyright   : (c) Runtime Verification, 2018-2021
  License     : BSD-3-Clause
  Maintainer  : thomas.tuegel@runtimeverification.com
  -}
  module Kore.Attribute.Axiom (
      Axiom (..),
      ProductionID (..),
      Priority (..),
      Owise (..),
      Assoc (..),
      Comm (..),
      Unit (..),
      Idem (..),
      Trusted (..),
      Concrete (..),
      Symbolic (..),
      Simplification (..),
      Overload (..),
      SmtLemma (..),
      Label (..),
      SourceLocation (..),
      Constructor (..),
      RuleIndex (..),
      RuleIndexCase (..),
      UniqueId (..),
      NonExecutable (..),
      PriorityAttributes (..),
      axiomSymbolToSymbolOrAlias,
      mapAxiomVariables,
      parseAxiomAttributes,
      getPriorityOfAxiom,
  ) where
  
  import Control.Lens qualified as Lens
  import Control.Monad qualified as Monad
  import Data.Default (
      Default (..),
   )
  import Data.Default qualified as Default
  import Data.Generics.Product
  import Data.Proxy
  import GHC.Generics qualified as GHC
  import Generics.SOP qualified as SOP
  import Kore.Attribute.Assoc
  import Kore.Attribute.Attributes
  import Kore.Attribute.Axiom.Concrete
  import Kore.Attribute.Axiom.Constructor
  import Kore.Attribute.Axiom.NonExecutable
  import Kore.Attribute.Axiom.Symbolic
  import Kore.Attribute.Axiom.Unit
  import Kore.Attribute.Comm
  import Kore.Attribute.Idem
  import Kore.Attribute.Label
  import Kore.Attribute.Overload
  import Kore.Attribute.Owise
  import Kore.Attribute.Parser (
      ParseAttributes (..),
      Parser,
      SymbolOrAlias,
      toAttributes,
   )
  import Kore.Attribute.Priority
  import Kore.Attribute.ProductionID
  import Kore.Attribute.RuleIndex
  import Kore.Attribute.Simplification
  import Kore.Attribute.SmtLemma
  import Kore.Attribute.SourceLocation
  import Kore.Attribute.Subsort
  import Kore.Attribute.Total
  import Kore.Attribute.Trusted
  import Kore.Attribute.UniqueId
  import Kore.Debug
  import Kore.Internal.Symbol (
      Symbol (..),
      toSymbolOrAlias,
   )
  import Kore.Syntax.Variable hiding (
      Concrete,
   )
  import Prelude.Kore
  import SQL qualified
  
  -- | Attributes specific to Kore axiom sentences.
  data Axiom symbol variable = Axiom
      { productionID :: !ProductionID
      -- ^ The identifier from the front-end identifying a rule or group of rules.
      , priority :: !Priority
      -- ^ A number associated to each rule,
      -- which specifies the order of application
      , assoc :: !Assoc
      -- ^ The axiom is an associativity axiom.
      , comm :: !Comm
      -- ^ The axiom is a commutativity axiom.
      , unit :: !Unit
      -- ^ The axiom is a left- or right-unit axiom.
      , idem :: !Idem
      -- ^ The axiom is an idempotency axiom.
      , trusted :: !Trusted
      -- ^ The claim is trusted
      , concrete :: !(Concrete variable)
      , symbolic :: !(Symbolic variable)
      , simplification :: !Simplification
      -- ^ This is an axiom used for simplification
      -- (as opposed to, e.g., function evaluation).
      , overload :: !(Overload symbol)
      -- ^ The axiom is an overloaded-production axiom.
      , smtLemma :: !SmtLemma
      -- ^ The axiom should be sent to SMT as a lemma.
      , label :: !Label
      -- ^ The user-defined label associated with the axiom.
      , sourceLocation :: !SourceLocation
      -- ^ Source and location in the original file.
      , constructor :: !Constructor
      -- ^ Shows that this is one of the constructor axioms
      -- (e.g. no confusion, no junk)
      , total :: !Total
      -- ^ Shows that this is one of the functionality axioms
      , subsorts :: !Subsorts
      -- ^ Shows that this describes a subsorting axiom
      , identifier :: !RuleIndex
      -- ^ Used to identify an axiom in the repl.
      , uniqueId :: !UniqueId
      -- ^ Unique id, usually generated by the frontend on request.
      , owise :: !Owise
      -- ^ This is an owise evaluation rule.
      , nonExecutable :: !NonExecutable
      -- ^ Won't be used during execution.
      }
      deriving stock (Eq, Ord, Show)
      deriving stock (GHC.Generic)
      deriving anyclass (NFData)
      deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo)
      deriving anyclass (Debug, Diff)
      deriving anyclass (Hashable)
  
  instance Default (Axiom symbol variable) where
      def =
          Axiom
              { productionID = def
              , priority = def
              , assoc = def
              , comm = def
              , unit = def
              , idem = def
              , trusted = def
              , concrete = def
              , symbolic = def
              , simplification = def
              , overload = def
              , smtLemma = def
              , label = def
              , sourceLocation = def
              , constructor = def
              , total = def
              , subsorts = def
              , identifier = def
              , uniqueId = def
              , owise = def
              , nonExecutable = def
              }
  
  instance
      From symbol SymbolOrAlias =>
      From (Axiom symbol VariableName) Attributes
      where
      from =
          mconcat
              . sequence
                  [ from . productionID
                  , from . priority
                  , from . assoc
                  , from . comm
                  , from . unit
                  , from . idem
                  , from . trusted
                  , from . concrete
                  , from . symbolic
                  , from . simplification
                  , from . overload
                  , from . smtLemma
                  , from . label
                  , from . sourceLocation
                  , from . constructor
                  , from . total
                  , from . subsorts
                  , from . uniqueId
                  , from . nonExecutable
                  , from . owise
                  ]
  
  instance From (Axiom symbol variable) PriorityAttributes where
      from Axiom{priority, owise, simplification} =
          PriorityAttributes
              { priorityAttr = priority
              , owiseAttr = owise
              , simplificationAttr = simplification
              }
  
  instance SQL.Column (Axiom SymbolOrAlias VariableName) where
      -- TODO (thomas.tuegel): Use a foreign key.
      defineColumn tableName _ =
          SQL.defineColumn tableName (Proxy @AttributePattern)
      toColumn = SQL.toColumn . toAttributes
  
  instance SQL.Column (Axiom Symbol VariableName) where
      -- TODO (thomas.tuegel): Use a foreign key.
      defineColumn tableName _ =
          SQL.defineColumn tableName (Proxy @AttributePattern)
      toColumn = SQL.toColumn . toAttributes
  
  axiomSymbolToSymbolOrAlias ::
      Axiom Symbol variable ->
      Axiom SymbolOrAlias variable
  axiomSymbolToSymbolOrAlias axiom =
      axiom & field @"overload" Lens.%~ fmap toSymbolOrAlias
  
  parseAxiomAttribute ::
      FreeVariables VariableName ->
      AttributePattern ->
      Axiom SymbolOrAlias VariableName ->
      Parser (Axiom SymbolOrAlias VariableName)
  parseAxiomAttribute freeVariables attr =
      typed @ProductionID (parseAttribute attr)
          Monad.>=> typed @Priority (parseAttribute attr)
          Monad.>=> typed @Assoc (parseAttribute attr)
          Monad.>=> typed @Comm (parseAttribute attr)
          Monad.>=> typed @Unit (parseAttribute attr)
          Monad.>=> typed @Idem (parseAttribute attr)
          Monad.>=> typed @Trusted (parseAttribute attr)
          Monad.>=> typed @(Concrete VariableName)
              (parseConcreteAttribute freeVariables attr)
          Monad.>=> typed @(Symbolic VariableName)
              (parseSymbolicAttribute freeVariables attr)
          Monad.>=> typed @Simplification (parseAttribute attr)
          Monad.>=> typed @(Overload SymbolOrAlias) (parseAttribute attr)
          Monad.>=> typed @SmtLemma (parseAttribute attr)
          Monad.>=> typed @Label (parseAttribute attr)
          Monad.>=> typed @SourceLocation (parseAttribute attr)
          Monad.>=> typed @Constructor (parseAttribute attr)
          Monad.>=> typed @Total (parseAttribute attr)
          Monad.>=> typed @Subsorts (parseAttribute attr)
          Monad.>=> typed @UniqueId (parseAttribute attr)
          Monad.>=> typed @NonExecutable (parseAttribute attr)
          Monad.>=> typed @Owise (parseAttribute attr)
  
  parseAxiomAttributes ::
      FreeVariables VariableName ->
      Attributes ->
      Parser (Axiom SymbolOrAlias VariableName)
  parseAxiomAttributes freeVariables (Attributes attrs) =
      foldlM (flip $ parseAxiomAttribute freeVariables) Default.def attrs
  
  mapAxiomVariables ::
      Ord variable2 =>
      AdjSomeVariableName (variable1 -> variable2) ->
      Axiom symbol variable1 ->
      Axiom symbol variable2
  mapAxiomVariables adj axiom@Axiom{concrete, symbolic} =
      axiom
          { concrete = mapConcreteVariables adj concrete
          , symbolic = mapSymbolicVariables adj symbolic
          }
  
  data PriorityAttributes = PriorityAttributes
      { priorityAttr :: !Priority
      , owiseAttr :: !Owise
      , simplificationAttr :: !Simplification
      }
  
  getPriorityOfAxiom ::
      forall attrs.
      HasCallStack =>
      From attrs PriorityAttributes =>
      attrs ->
      Integer
  getPriorityOfAxiom
      ( from @attrs ->
              PriorityAttributes
                  { priorityAttr
                  , owiseAttr
                  , simplificationAttr
                  }
          ) =
          case (priorityAttr, owiseAttr, simplificationAttr) of
              (Priority Nothing, Owise True, NotSimplification) ->
                  owisePriority
              (Priority Nothing, Owise False, NotSimplification) ->
                  defaultPriority
              (Priority (Just value), Owise False, NotSimplification) ->
                  value
              (Priority Nothing, Owise False, IsSimplification Nothing) ->
                  defaultSimplificationPriority
              (Priority Nothing, Owise False, IsSimplification (Just value)) ->
                  value
              -- TODO: remove this case once the frontend
              -- modifies the simplification attribute
              -- to take an optional priority value
              (Priority (Just value), Owise False, IsSimplification Nothing) ->
                  value
              errorCase@(_, _, _) ->
                  error
                      ( "An axiom cannot have the following \
                        \ combination of attributes: "
                          <> show errorCase
                          <> " Please report this error."
                      )
  