content: {- |
  Module      : Kore.Validate.ModuleVerifier
  Description : Tools for verifying the wellformedness of a Kore 'Module'.
  Copyright   : (c) Runtime Verification, 2018-2021
  License     : BSD-3-Clause
  Maintainer  : virgil.serbanuta@runtimeverification.com
  Stability   : experimental
  Portability : POSIX
  -}
  module Kore.Validate.ModuleVerifier (
      verifyModule,
      verifyUniqueNames,
  ) where
  
  import Control.Lens (
      (%=),
   )
  import Control.Lens qualified as Lens
  import Control.Monad.Reader.Class qualified as Reader
  import Control.Monad.State.Class qualified as State
  import Data.Generics.Product
  import Data.HashMap.Strict (HashMap)
  import Data.InternedText (InternedText)
  import Data.List qualified as List
  import Data.Map.Strict qualified as Map
  import Kore.AST.Error
  import Kore.Attribute.Parser (
      ParseAttributes,
   )
  import Kore.Attribute.Parser qualified as Attribute.Parser
  import Kore.Error
  import Kore.IndexedModule.IndexedModule as IndexedModule
  import Kore.Syntax
  import Kore.Syntax.Definition
  import Kore.Validate.AliasVerifier
  import Kore.Validate.Error
  import Kore.Validate.SentenceVerifier (
      SentenceVerifier,
      verifyAxioms,
      verifyClaims,
      verifyHookedSorts,
      verifyHookedSymbols,
      verifyNonHooks,
      verifySorts,
      verifySymbols,
   )
  import Kore.Validate.SentenceVerifier qualified as SentenceVerifier
  import Kore.Validate.Verifier
  import Prelude.Kore
  
  {- | 'verifyUniqueNames' verifies that names defined in a module are unique both
  within the module and outside, using the provided name set.
  -}
  verifyUniqueNames ::
      -- | Names that are already defined.
      HashMap InternedText AstLocation ->
      Module (Sentence pat) ->
      -- | On success returns the names that were previously defined together with
      -- the names defined in the given 'Module'.
      Either (Error VerifyError) (HashMap InternedText AstLocation)
  verifyUniqueNames existingNames koreModule =
      withContext
          ("module '" ++ getModuleNameForError (moduleName koreModule) ++ "'")
          ( SentenceVerifier.verifyUniqueNames
              (moduleSentences koreModule)
              existingNames
          )
  
  {- | Verify the named module.
  
  The cached 'VerifiedModule' is returned if available; otherwise the module is
  verified and cached.
  
  See also: 'verifyUncachedModule'
  -}
  verifyModule :: ModuleName -> Verifier VerifiedModule'
  verifyModule name = lookupVerifiedModule name >>= maybe notCached cached
    where
      cached = return
      notCached = verifyUncachedModule name
  
  -- | Verify the named module, irrespective of the cache.
  verifyUncachedModule :: ModuleName -> Verifier VerifiedModule'
  verifyUncachedModule name = whileImporting name $ do
      module' <- lookupParsedModule name
      let Module{moduleSentences} = module'
          sentences = List.sort moduleSentences
      (_, indexedModule) <-
          withModuleContext name (newVerifiedModule module')
              >>= SentenceVerifier.runSentenceVerifier
                  ( do
                      verifyImports sentences
                      withModuleContext name $ do
                          verifySorts sentences
                          verifySymbols sentences
                          verifyHookedSorts sentences
                          verifyHookedSymbols sentences
                          verifyNonHooks sentences
                          verifyAliases sentences
                          verifyAxioms sentences
                          verifyClaims sentences
                  )
      _ <-
          withModuleContext name $
              internalIndexedModuleSubsorts indexedModule
      field @"verifiedModules" %= Map.insert name indexedModule
      return indexedModule
  
  {- | Construct a new 'VerifiedModule' for the 'ParsedModule'.
  
  The new 'VerifiedModule' is empty except for its 'ModuleName', its 'Attributes',
  and the 'ImplicitModule' import.
  -}
  newVerifiedModule :: ParsedModule -> Verifier VerifiedModule'
  newVerifiedModule module' = do
      VerifierContext{implicitModule} <- Reader.ask
      let Module{moduleName, moduleAttributes} = module'
      attrs <- parseAttributes' moduleAttributes
      return
          ( indexedModuleWithDefaultImports moduleName (Just implicitModule)
              & Lens.set (field @"indexedModuleAttributes") (attrs, moduleAttributes)
          )
  
  {- | Project the 'SentenceImport's out the list and verify them.
  
  The named modules are verified and imported into the current 'VerifiedModule'.
  -}
  verifyImports :: [ParsedSentence] -> SentenceVerifier ()
  verifyImports = traverse_ verifyImport . mapMaybe projectSentenceImport
  
  verifyImport :: SentenceImport -> SentenceVerifier ()
  verifyImport sentence =
      withSentenceImportContext sentence $ do
          let SentenceImport{sentenceImportAttributes = attrs0} = sentence
          attrs1 <- parseAttributes' attrs0
          let importName = sentenceImportModuleName sentence
          verified <- lift $ verifyModule importName
          State.modify' $ addImport verified attrs1 attrs0
          State.modify' $ addImportSyntax verified attrs1 attrs0
    where
      addImport verified attrs1 attrs0 =
          Lens.over
              (field @"indexedModuleImports")
              ((attrs1, attrs0, verified) :)
      addImportSyntax verified attrs1 attrs0 =
          Lens.over
              (field @"indexedModuleSyntax" . field @"indexedModuleImportsSyntax")
              ((attrs1, attrs0, indexedModuleSyntax verified) :)
  
  parseAttributes' ::
      forall attrs error e.
      (MonadError (Error e) error, ParseAttributes attrs) =>
      Attributes ->
      error attrs
  parseAttributes' =
      Attribute.Parser.liftParser . Attribute.Parser.parseAttributes
  