content: module Test.Kore.Rewrite.SMT.Representation.Builders (
      emptyDeclarations,
      unresolvedConstructorArg,
      unresolvedConstructorSymbolMap,
      unresolvedDataMap,
      unresolvedIndirectSortMap,
      unresolvedSmthookSymbolMap,
      unresolvedSmtlibSymbolMap,
      unresolvedSort,
      unresolvedSortConstructor,
      unresolvedSortMap,
  ) where
  
  import Data.Map.Strict qualified as Map
  import Data.Text (
      Text,
   )
  import Kore.Rewrite.SMT.AST qualified as AST (
      Declarations (Declarations),
      Encodable (AlreadyEncoded),
      IndirectSymbolDeclaration (IndirectSymbolDeclaration),
      KoreSortDeclaration (..),
      KoreSymbolDeclaration (..),
      Sort (Sort),
      SortReference (SortReference),
      SortSExprSpec (..),
      Symbol (Symbol),
      SymbolReference (SymbolReference),
      UnresolvedConstructor,
      UnresolvedConstructorArgument,
      UnresolvedSort,
      UnresolvedSymbol,
      encodable,
      encode,
   )
  import Kore.Rewrite.SMT.AST qualified as AST.DoNotUse
  import Kore.Sort qualified as Kore (
      Sort,
   )
  import Kore.Syntax.Id qualified as Kore (
      Id,
   )
  import Prelude.Kore
  import SMT.AST qualified as AST (
      Constructor (Constructor),
      ConstructorArgument (ConstructorArgument),
      DataTypeDeclaration (DataTypeDeclaration),
      FunctionDeclaration (FunctionDeclaration),
      SExpr (Atom),
      SortDeclaration (SortDeclaration),
   )
  import SMT.AST qualified as AST.DoNotUse
  import Test.Kore (
      testId,
   )
  import Test.Kore.Rewrite.SMT.Builders ()
  
  emptyDeclarations :: AST.Declarations sort symbol name
  emptyDeclarations = AST.Declarations{sorts = Map.empty, symbols = Map.empty}
  
  unresolvedSortMap :: Kore.Id -> (Kore.Id, AST.UnresolvedSort)
  unresolvedSortMap identifier = (identifier, unresolvedSort identifier)
  
  unresolvedSort :: Kore.Id -> AST.UnresolvedSort
  unresolvedSort identifier =
      AST.Sort
          { sortData = AST.ConstSExpr $ AST.encode encodable
          , sortDeclaration =
              AST.SortDeclarationSort
                  AST.SortDeclaration
                      { name = encodable
                      , arity = 0
                      }
          }
    where
      encodable = AST.encodable identifier
  
  unresolvedDataMap :: Kore.Id -> (Kore.Id, AST.UnresolvedSort)
  unresolvedDataMap identifier = (identifier, unresolvedData identifier)
  
  unresolvedData :: Kore.Id -> AST.UnresolvedSort
  unresolvedData identifier =
      AST.Sort
          { sortData = AST.ConstSExpr $ AST.encode encodable
          , sortDeclaration =
              AST.SortDeclarationDataType
                  AST.DataTypeDeclaration
                      { name = encodable
                      , typeArguments = []
                      , constructors = []
                      }
          }
    where
      encodable = AST.encodable identifier
  
  unresolvedSortConstructor :: Kore.Id -> AST.UnresolvedConstructor
  unresolvedSortConstructor identifier =
      AST.Constructor
          { name = AST.SymbolReference identifier
          , arguments = []
          }
  
  unresolvedConstructorArg ::
      Text -> Kore.Sort -> AST.UnresolvedConstructorArgument
  unresolvedConstructorArg name sort =
      AST.ConstructorArgument
          { name = AST.encodable (testId name)
          , argType = AST.SortReference sort
          }
  
  unresolvedIndirectSortMap ::
      Kore.Id -> AST.Encodable -> (Kore.Id, AST.UnresolvedSort)
  unresolvedIndirectSortMap identifier name =
      (identifier, unresolvedIndirectSort name)
  
  unresolvedIndirectSort :: AST.Encodable -> AST.UnresolvedSort
  unresolvedIndirectSort name =
      AST.Sort
          { sortData = AST.ConstSExpr $ AST.encode name
          , sortDeclaration = AST.SortDeclaredIndirectly name
          }
  
  unresolvedConstructorSymbolMap ::
      Kore.Id ->
      Kore.Sort ->
      [Kore.Sort] ->
      (Kore.Id, AST.UnresolvedSymbol)
  unresolvedConstructorSymbolMap identifier resultSort argumentSorts =
      ( identifier
      , unresolvedConstructorSymbol identifier resultSort argumentSorts
      )
  
  unresolvedConstructorSymbol ::
      Kore.Id -> Kore.Sort -> [Kore.Sort] -> AST.UnresolvedSymbol
  unresolvedConstructorSymbol identifier resultSort argumentSorts =
      AST.Symbol
          { symbolData = AST.encode encodable
          , symbolDeclaration =
              AST.SymbolConstructor
                  AST.IndirectSymbolDeclaration
                      { name = encodable
                      , sortDependencies =
                          AST.SortReference <$> resultSort : argumentSorts
                      }
          }
    where
      encodable = AST.encodable identifier
  
  unresolvedSmtlibSymbolMap ::
      Kore.Id ->
      Text ->
      [Kore.Sort] ->
      Kore.Sort ->
      (Kore.Id, AST.UnresolvedSymbol)
  unresolvedSmtlibSymbolMap identifier encodedName inputSorts resultSort =
      (identifier, unresolvedSmtlibSymbol encodedName inputSorts resultSort)
  
  unresolvedSmtlibSymbol ::
      Text ->
      [Kore.Sort] ->
      Kore.Sort ->
      AST.UnresolvedSymbol
  unresolvedSmtlibSymbol encodedName inputSorts resultSort =
      AST.Symbol
          { symbolData = AST.Atom encodedName
          , symbolDeclaration =
              AST.SymbolDeclaredDirectly
                  AST.FunctionDeclaration
                      { name = AST.AlreadyEncoded (AST.Atom encodedName)
                      , inputSorts = map AST.SortReference inputSorts
                      , resultSort = AST.SortReference resultSort
                      }
          }
  
  unresolvedSmthookSymbolMap ::
      Kore.Id ->
      Text ->
      [Kore.Sort] ->
      (Kore.Id, AST.UnresolvedSymbol)
  unresolvedSmthookSymbolMap identifier encodedName sortDependencies =
      (identifier, unresolvedSmthookSymbol encodedName sortDependencies)
  
  unresolvedSmthookSymbol ::
      Text -> [Kore.Sort] -> AST.UnresolvedSymbol
  unresolvedSmthookSymbol encodedName sortDependencies =
      AST.Symbol
          { symbolData = AST.Atom encodedName
          , symbolDeclaration =
              AST.SymbolBuiltin
                  AST.IndirectSymbolDeclaration
                      { name = AST.AlreadyEncoded (AST.Atom encodedName)
                      , sortDependencies = fmap AST.SortReference sortDependencies
                      }
          }
  