content: {- |
  Copyright   : (c) Runtime Verification, 2021
  License     : BSD-3-Clause
  -}
  module Kore.Attribute.Definition (
      parseKFileAttributes,
      KFileLocations (..),
  ) where
  
  import Control.Monad.Catch (MonadThrow)
  import Data.Default qualified as Default
  import Data.Generics.Product (typed)
  import GHC.Generics qualified as GHC
  import Kore.Attribute.Attributes (Attributes (..))
  import Kore.Attribute.Parser (ParseAttributes (..))
  import Kore.Attribute.SourceLocation (SourceLocation)
  import Kore.Error (printError)
  import Kore.Log.ErrorParse
  import Prelude.Kore
  
  {- | Location attribute for some of the K files used during execution, displayed
  by the 'WarnIfLowProductivity' warning.
  -}
  newtype KFileLocations = KFileLocations
      {locations :: [SourceLocation]}
      deriving stock (Show)
      deriving stock (GHC.Generic)
      deriving anyclass (NFData)
  
  parseKFileAttributes :: MonadThrow m => Attributes -> m SourceLocation
  parseKFileAttributes (Attributes attrs) =
      case parser of
          Left err -> errorParse $ printError err
          Right sourceLocation ->
              return sourceLocation
    where
      parser = foldlM (flip parseDefinitionLocation) Default.def attrs
      parseDefinitionLocation source =
          typed @SourceLocation (parseAttribute source)
  