  | 
 Module       :  . Attribute . Parser 
 Description : Attribute parsers 
 Copyright    : ( c ) Runtime Verification , 2018 - 2021 
 License      : BSD-3 - Clause 
 Maintainer   :  
 Stability    : experimental 
 Portability : portable 

 This module defines attribute parsers and a class ' ParseAttributes ' for types 
 which can be parsed from an attribute list . 

 This module is intended to be imported qualified or explicitly : 

 @ 
   import Kore . Attribute .  ( parseAttributes , ParseAttributes ( .. ) ) 
   import qualified Kore . Attribute .  as Attribute 
 @ 

Module      : Kore.Attribute.Parser
Description : Attribute parsers
Copyright   : (c) Runtime Verification, 2018-2021
License     : BSD-3-Clause
Maintainer  : 
Stability   : experimental
Portability : portable

This module defines attribute parsers and a class 'ParseAttributes' for types
which can be parsed from an attribute list.

This module is intended to be imported qualified or explicitly:

@
  import Kore.Attribute.Parser ( parseAttributes, ParseAttributes (..) )
  import qualified Kore.Attribute.Parser as Attribute
@
-}
module Kore.Attribute.Parser (
    -- * Parsing attributes
    ParseAttributes (..),
    toAttributes,
    Attributes (..),
    Parser,
    ParseError,
    parseAttributes,
    parseAttributesWith,
    liftParser,

  * Parsers
    failDuplicate,
    failConflicting,
    parseBoolAttribute,
    parseBoolAttributeAux,
    toBoolAttributes,
    toBoolAttributesAux,
    withApplication,
    getZeroParams,
    getTwoParams,
    getZeroArguments,
    getOneArgument,
    getZeroOrOneArguments,
    getTwoArguments,
    getSymbolOrAlias,
    Kore.Attribute.Parser.getStringLiteral,
    getVariable,
    parseSExpr,
    parseReadS,
    parseStringLiteral,
    parseInteger,

    -- * Re-exports
    AttributePattern,
    asAttributePattern,
    attributePattern,
    attributePattern_,
    attributeString,
    attributeInteger,
    attributeVariable,
    Default (..),
    StringLiteral (StringLiteral),
    Generic,
    NFData,
    module Kore.AST.Common,
    module Kore.Sort,
    module Kore.Syntax.Application,
) where

import Control.Lens (
    Getter,
    Iso',
 )
import Control.Lens qualified as Lens
import Control.Monad.Except (
    MonadError,
 )
import Control.Monad.Except qualified as Monad.Except
import Data.Coerce
import Data.Default (
    Default (..),
 )
import Data.Default qualified as Default
import Data.Functor.Foldable qualified as Recursive
import Data.List qualified as List
import Data.Text (
    Text,
 )
import Data.Text qualified as Text
import GHC.Generics (
    Generic,
 )
import Kore.AST.Common
import Kore.AST.Error qualified as Kore.Error
import Kore.Attribute.Attributes
import Kore.Attribute.Null qualified as Attribute (
    Null,
 )
import Kore.Attribute.Smtlib.Smtlib qualified as Attribute
import Kore.Error (
    Error,
    castError,
 )
import Kore.Error qualified
import Kore.Sort
import Kore.Syntax.Application
import Kore.Syntax.Pattern
import Kore.Syntax.StringLiteral (
    StringLiteral (StringLiteral),
 )
import Kore.Syntax.Variable (
    SomeVariable,
    VariableName,
 )
import Prelude.Kore
import SMT.SimpleSMT (
    SExpr,
    readSExprs,
 )

data ParseError

type Parser = Either (Error ParseError)

class (Default attrs, From attrs Attributes) => ParseAttributes attrs where
    -- | Parse a 'AttributePattern' from 'Attributes' to produce @attrs@.
    --
    --    Attributes are parsed individually and the list of attributes is parsed by
     folding over the list ; @parseAttributes@ takes a second argument which is
    --    the partial result obtained by folding over the preceeding attributes of the
    --    list.
    --
    --    Ignore unrecognized attributes by 'return'-ing the partial result. Signal
     errors with ' Control . Monad . Except.throwError ' to abort parsing .
    --
     See also : ' parseAttributes ' , ' withApplication ' , ' runParser '
    parseAttribute ::
        -- | attribute
        AttributePattern ->
        -- | partial parsing result
        attrs ->
        Parser attrs

toAttributes :: forall attrs. From attrs Attributes => attrs -> Attributes
toAttributes = from

instance ParseAttributes Attributes where
    parseAttribute attr (Attributes attrs) =
        return (Attributes $ attr : attrs)

instance ParseAttributes Attribute.Null where
    parseAttribute _ _ = return mempty

parseAttributesWith ::
    ParseAttributes attrs =>
    Attributes ->
    attrs ->
    Parser attrs
parseAttributesWith (Attributes attrs) def' =
    foldlM (flip parseAttribute) def' attrs

parseAttributes :: ParseAttributes attrs => Attributes -> Parser attrs
parseAttributes attrs = parseAttributesWith attrs Default.def

-- | Run an attribute parser in any 'MonadError' with the given initial state.
liftParser ::
    MonadError (Error e) m =>
    -- | parser
    Parser a ->
    m a
liftParser = Monad.Except.liftEither . Kore.Error.castError

-- | Fail due to a duplicate attribute.
failDuplicate :: Id -> Parser a
failDuplicate ident =
    Kore.Error.koreFail ("duplicate attribute: " ++ getIdForError ident)

-- | Fail due to conflicting attributes.
failConflicting :: [Id] -> Parser a
failConflicting idents =
    Kore.Error.koreFail
        ( "conflicting attributes: "
            ++ List.intercalate ", " (getIdForError <$> idents)
        )

toBoolAttributes ::
    Coercible attr Bool => AttributePattern -> attr -> Attributes
toBoolAttributes = toBoolAttributesAux Lens.coerced

toBoolAttributesAux ::
    Getter attr Bool -> AttributePattern -> attr -> Attributes
toBoolAttributesAux asBool pattern1 attr =
    Attributes [pattern1 | Lens.view asBool attr]

parseBoolAttribute ::
    Coercible attr Bool =>
    Id ->
    AttributePattern ->
    attr ->
    Parser attr
parseBoolAttribute = parseBoolAttributeAux Lens.coerced

parseBoolAttributeAux ::
    Iso' attr Bool -> Id -> AttributePattern -> attr -> Parser attr
parseBoolAttributeAux asBool ident =
    withApplication' $ \params args attr -> do
        getZeroParams params
        getZeroArguments args
        when (Lens.view asBool attr) failDuplicate'
        return (Lens.review asBool True)
  where
    withApplication' = withApplication ident
    failDuplicate' = failDuplicate ident

withApplication ::
    Id ->
    ([Sort] -> [AttributePattern] -> attrs -> Parser attrs) ->
    AttributePattern ->
    attrs ->
    Parser attrs
withApplication ident go kore =
    case Recursive.project kore of
        _ :< ApplicationF app
            | symbolOrAliasConstructor == ident ->
                Kore.Error.withLocationAndContext symbol context
                    . go symbolOrAliasParams applicationChildren
          where
            ~context = "attribute '" <> Text.pack (show symbol) <> "'"
            Application{applicationSymbolOrAlias = symbol} = app
            Application{applicationChildren} = app
            SymbolOrAlias{symbolOrAliasConstructor} = symbol
            SymbolOrAlias{symbolOrAliasParams} = symbol
        _ -> return

getZeroParams :: [Sort] -> Parser ()
getZeroParams =
    \case
        [] -> return ()
        params ->
            Kore.Error.koreFailWithLocations
                params
                ("expected zero parameters, found " <> Text.pack (show arity))
          where
            arity = length params

getTwoParams :: [Sort] -> Parser (Sort, Sort)
getTwoParams =
    \case
        [param1, param2] -> return (param1, param2)
        params ->
            Kore.Error.koreFailWithLocations
                params
                ("expected two parameters, found " <> Text.pack (show arity))
          where
            arity = length params

  | Accept exactly zero arguments .
getZeroArguments ::
    [AttributePattern] ->
    Parser ()
getZeroArguments =
    \case
        [] -> return ()
        args ->
            Kore.Error.koreFail
                ("expected zero arguments, found " ++ show arity)
          where
            arity = length args

  | Accept exactly one argument .
getOneArgument ::
    [AttributePattern] ->
    Parser AttributePattern
getOneArgument =
    \case
        [arg] -> return arg
        args ->
            Kore.Error.koreFail
                ("expected one argument, found " ++ show arity)
          where
            arity = length args

getZeroOrOneArguments ::
    [AttributePattern] ->
    Parser (Maybe AttributePattern)
getZeroOrOneArguments =
    \case
        [] -> return Nothing
        [arg] -> return (Just arg)
        args ->
            Kore.Error.koreFail
                ("expected at most one argument, found " <> show arity)
          where
            arity = length args

  | Accept exactly two arguments .
getTwoArguments ::
    [AttributePattern] ->
    Parser (AttributePattern, AttributePattern)
getTwoArguments =
    \case
        [arg1, arg2] -> return (arg1, arg2)
        args ->
            Kore.Error.koreFail
                ("expected two arguments, found " ++ show arity)
          where
            arity = length args

-- | Accept a symbol or alias applied to no arguments.
getSymbolOrAlias :: AttributePattern -> Parser SymbolOrAlias
getSymbolOrAlias kore =
    case Recursive.project kore of
        _ :< ApplicationF app
            | [] <- applicationChildren -> return symbol
            | otherwise ->
                Kore.Error.withLocationAndContext
                    symbol
                    ("symbol '" <> Text.pack (show symbol) <> "'")
                    (Kore.Error.koreFail "expected zero arguments")
          where
            Application{applicationSymbolOrAlias = symbol} = app
            Application{applicationChildren} = app
        _ -> Kore.Error.koreFail "expected symbol or alias application"

-- | Accept a string literal.
getStringLiteral :: AttributePattern -> Parser StringLiteral
getStringLiteral kore =
    case Recursive.project kore of
        _ :< StringLiteralF (Const lit) -> return lit
        _ -> Kore.Error.koreFail "expected string literal pattern"

-- | Accept a variable.
getVariable :: AttributePattern -> Parser (SomeVariable VariableName)
getVariable kore =
    case Recursive.project kore of
        _ :< VariableF (Const var) -> return var
        _ -> Kore.Error.koreFail "expected variable pattern"

{- | Parse a 'Text' through 'ReadS'.

See also: 'parseInteger'
-}
parseReadS :: ReadS a -> Text -> Parser a
parseReadS aReadS (Text.unpack -> syntax) =
    case aReadS syntax of
        [] -> noParse
        r : rs ->
            case rs of
                _ : _ -> ambiguousParse
                _
                    | null unparsed -> return a
                    | otherwise -> incompleteParse unparsed
          where
            (a, unparsed) = r
  where
    noParse = Kore.Error.koreFail ("failed to parse \"" ++ syntax ++ "\"")
    ambiguousParse =
        Kore.Error.koreFail $
            "parsing \"" ++ syntax ++ "\" was ambiguous"
    incompleteParse unparsed =
        Kore.Error.koreFail $
            "incomplete parse: failed to parse \"" ++ unparsed ++ "\""

  | Parse an ' Integer ' from a ' StringLiteral ' .
parseInteger :: StringLiteral -> Parser Integer
parseInteger = parseStringLiteral reads

  | Parse from a ' StringLiteral ' .
parseStringLiteral :: ReadS a -> StringLiteral -> Parser a
parseStringLiteral reads' (StringLiteral literal) = parseReadS reads' literal

  |  an ' SExpr ' for the @smtlib@ attribute . 

 An error is signalled in '  ' if we can not parse the ' SExpr ' , or if the 
 entire argument is not consumed by the parser . 


An error is signalled in 'Parser' if we cannot parse the 'SExpr', or if the
entire argument is not consumed by the parser.
-}
parseSExpr ::
  | text representing an ' SExpr '
    Text ->
    Parser SExpr
parseSExpr syntax =
    case readSExprs syntax of
        [] -> noParse
        sExpr : rest ->
            case rest of
                [] -> return sExpr
                _ -> incompleteParse
  where
    noParse = Kore.Error.koreFail "failed to parse S-expression"
    incompleteParse = Kore.Error.koreFail "failed to parse entire argument"

instance ParseAttributes Attribute.Smtlib where
    parseAttribute =
        withApplication' $ \params args Attribute.Smtlib{getSmtlib} -> do
            getZeroParams params
            arg <- getOneArgument args
            StringLiteral syntax <- getStringLiteral arg
            sExpr <- parseSExpr syntax
            unless (isNothing getSmtlib) failDuplicate'
            return Attribute.Smtlib{getSmtlib = Just sExpr}
      where
        withApplication' = withApplication Attribute.smtlibId
        failDuplicate' = failDuplicate Attribute.smtlibId

 * Parsing attributes
 * Re-exports
 | Parse a 'AttributePattern' from 'Attributes' to produce @attrs@.

    Attributes are parsed individually and the list of attributes is parsed by
    the partial result obtained by folding over the preceeding attributes of the
    list.

    Ignore unrecognized attributes by 'return'-ing the partial result. Signal

 | attribute
 | partial parsing result
 | Run an attribute parser in any 'MonadError' with the given initial state.
 | parser
 | Fail due to a duplicate attribute.
 | Fail due to conflicting attributes.
 | Accept a symbol or alias applied to no arguments.
 | Accept a string literal.
 | Accept a variable.
 | Parse a 'Text' through 'ReadS'.

See also: 'parseInteger'

  | 
 Module       :  . Attribute . Parser 
 Description : Attribute parsers 
 Copyright    : ( c ) Runtime Verification , 2018 - 2021 
 License      : BSD-3 - Clause 
 Maintainer   :  
 Stability    : experimental 
 Portability : portable 

 This module defines attribute parsers and a class ' ParseAttributes ' for types 
 which can be parsed from an attribute list . 

 This module is intended to be imported qualified or explicitly : 

 @ 
   import Kore . Attribute .  ( parseAttributes , ParseAttributes ( .. ) ) 
   import qualified Kore . Attribute .  as Attribute 
 @ 

Module      : Kore.Attribute.Parser
Description : Attribute parsers
Copyright   : (c) Runtime Verification, 2018-2021
License     : BSD-3-Clause
Maintainer  : 
Stability   : experimental
Portability : portable

This module defines attribute parsers and a class 'ParseAttributes' for types
which can be parsed from an attribute list.

This module is intended to be imported qualified or explicitly:

@
  import Kore.Attribute.Parser ( parseAttributes, ParseAttributes (..) )
  import qualified Kore.Attribute.Parser as Attribute
@
-}
module Kore.Attribute.Parser (
    ParseAttributes (..),
    toAttributes,
    Attributes (..),
    Parser,
    ParseError,
    parseAttributes,
    parseAttributesWith,
    liftParser,

  * Parsers
    failDuplicate,
    failConflicting,
    parseBoolAttribute,
    parseBoolAttributeAux,
    toBoolAttributes,
    toBoolAttributesAux,
    withApplication,
    getZeroParams,
    getTwoParams,
    getZeroArguments,
    getOneArgument,
    getZeroOrOneArguments,
    getTwoArguments,
    getSymbolOrAlias,
    Kore.Attribute.Parser.getStringLiteral,
    getVariable,
    parseSExpr,
    parseReadS,
    parseStringLiteral,
    parseInteger,

    AttributePattern,
    asAttributePattern,
    attributePattern,
    attributePattern_,
    attributeString,
    attributeInteger,
    attributeVariable,
    Default (..),
    StringLiteral (StringLiteral),
    Generic,
    NFData,
    module Kore.AST.Common,
    module Kore.Sort,
    module Kore.Syntax.Application,
) where

import Control.Lens (
    Getter,
    Iso',
 )
import Control.Lens qualified as Lens
import Control.Monad.Except (
    MonadError,
 )
import Control.Monad.Except qualified as Monad.Except
import Data.Coerce
import Data.Default (
    Default (..),
 )
import Data.Default qualified as Default
import Data.Functor.Foldable qualified as Recursive
import Data.List qualified as List
import Data.Text (
    Text,
 )
import Data.Text qualified as Text
import GHC.Generics (
    Generic,
 )
import Kore.AST.Common
import Kore.AST.Error qualified as Kore.Error
import Kore.Attribute.Attributes
import Kore.Attribute.Null qualified as Attribute (
    Null,
 )
import Kore.Attribute.Smtlib.Smtlib qualified as Attribute
import Kore.Error (
    Error,
    castError,
 )
import Kore.Error qualified
import Kore.Sort
import Kore.Syntax.Application
import Kore.Syntax.Pattern
import Kore.Syntax.StringLiteral (
    StringLiteral (StringLiteral),
 )
import Kore.Syntax.Variable (
    SomeVariable,
    VariableName,
 )
import Prelude.Kore
import SMT.SimpleSMT (
    SExpr,
    readSExprs,
 )

data ParseError

type Parser = Either (Error ParseError)

class (Default attrs, From attrs Attributes) => ParseAttributes attrs where
     folding over the list ; @parseAttributes@ takes a second argument which is
     errors with ' Control . Monad . Except.throwError ' to abort parsing .
     See also : ' parseAttributes ' , ' withApplication ' , ' runParser '
    parseAttribute ::
        AttributePattern ->
        attrs ->
        Parser attrs

toAttributes :: forall attrs. From attrs Attributes => attrs -> Attributes
toAttributes = from

instance ParseAttributes Attributes where
    parseAttribute attr (Attributes attrs) =
        return (Attributes $ attr : attrs)

instance ParseAttributes Attribute.Null where
    parseAttribute _ _ = return mempty

parseAttributesWith ::
    ParseAttributes attrs =>
    Attributes ->
    attrs ->
    Parser attrs
parseAttributesWith (Attributes attrs) def' =
    foldlM (flip parseAttribute) def' attrs

parseAttributes :: ParseAttributes attrs => Attributes -> Parser attrs
parseAttributes attrs = parseAttributesWith attrs Default.def

liftParser ::
    MonadError (Error e) m =>
    Parser a ->
    m a
liftParser = Monad.Except.liftEither . Kore.Error.castError

failDuplicate :: Id -> Parser a
failDuplicate ident =
    Kore.Error.koreFail ("duplicate attribute: " ++ getIdForError ident)

failConflicting :: [Id] -> Parser a
failConflicting idents =
    Kore.Error.koreFail
        ( "conflicting attributes: "
            ++ List.intercalate ", " (getIdForError <$> idents)
        )

toBoolAttributes ::
    Coercible attr Bool => AttributePattern -> attr -> Attributes
toBoolAttributes = toBoolAttributesAux Lens.coerced

toBoolAttributesAux ::
    Getter attr Bool -> AttributePattern -> attr -> Attributes
toBoolAttributesAux asBool pattern1 attr =
    Attributes [pattern1 | Lens.view asBool attr]

parseBoolAttribute ::
    Coercible attr Bool =>
    Id ->
    AttributePattern ->
    attr ->
    Parser attr
parseBoolAttribute = parseBoolAttributeAux Lens.coerced

parseBoolAttributeAux ::
    Iso' attr Bool -> Id -> AttributePattern -> attr -> Parser attr
parseBoolAttributeAux asBool ident =
    withApplication' $ \params args attr -> do
        getZeroParams params
        getZeroArguments args
        when (Lens.view asBool attr) failDuplicate'
        return (Lens.review asBool True)
  where
    withApplication' = withApplication ident
    failDuplicate' = failDuplicate ident

withApplication ::
    Id ->
    ([Sort] -> [AttributePattern] -> attrs -> Parser attrs) ->
    AttributePattern ->
    attrs ->
    Parser attrs
withApplication ident go kore =
    case Recursive.project kore of
        _ :< ApplicationF app
            | symbolOrAliasConstructor == ident ->
                Kore.Error.withLocationAndContext symbol context
                    . go symbolOrAliasParams applicationChildren
          where
            ~context = "attribute '" <> Text.pack (show symbol) <> "'"
            Application{applicationSymbolOrAlias = symbol} = app
            Application{applicationChildren} = app
            SymbolOrAlias{symbolOrAliasConstructor} = symbol
            SymbolOrAlias{symbolOrAliasParams} = symbol
        _ -> return

getZeroParams :: [Sort] -> Parser ()
getZeroParams =
    \case
        [] -> return ()
        params ->
            Kore.Error.koreFailWithLocations
                params
                ("expected zero parameters, found " <> Text.pack (show arity))
          where
            arity = length params

getTwoParams :: [Sort] -> Parser (Sort, Sort)
getTwoParams =
    \case
        [param1, param2] -> return (param1, param2)
        params ->
            Kore.Error.koreFailWithLocations
                params
                ("expected two parameters, found " <> Text.pack (show arity))
          where
            arity = length params

  | Accept exactly zero arguments .
getZeroArguments ::
    [AttributePattern] ->
    Parser ()
getZeroArguments =
    \case
        [] -> return ()
        args ->
            Kore.Error.koreFail
                ("expected zero arguments, found " ++ show arity)
          where
            arity = length args

  | Accept exactly one argument .
getOneArgument ::
    [AttributePattern] ->
    Parser AttributePattern
getOneArgument =
    \case
        [arg] -> return arg
        args ->
            Kore.Error.koreFail
                ("expected one argument, found " ++ show arity)
          where
            arity = length args

getZeroOrOneArguments ::
    [AttributePattern] ->
    Parser (Maybe AttributePattern)
getZeroOrOneArguments =
    \case
        [] -> return Nothing
        [arg] -> return (Just arg)
        args ->
            Kore.Error.koreFail
                ("expected at most one argument, found " <> show arity)
          where
            arity = length args

  | Accept exactly two arguments .
getTwoArguments ::
    [AttributePattern] ->
    Parser (AttributePattern, AttributePattern)
getTwoArguments =
    \case
        [arg1, arg2] -> return (arg1, arg2)
        args ->
            Kore.Error.koreFail
                ("expected two arguments, found " ++ show arity)
          where
            arity = length args

getSymbolOrAlias :: AttributePattern -> Parser SymbolOrAlias
getSymbolOrAlias kore =
    case Recursive.project kore of
        _ :< ApplicationF app
            | [] <- applicationChildren -> return symbol
            | otherwise ->
                Kore.Error.withLocationAndContext
                    symbol
                    ("symbol '" <> Text.pack (show symbol) <> "'")
                    (Kore.Error.koreFail "expected zero arguments")
          where
            Application{applicationSymbolOrAlias = symbol} = app
            Application{applicationChildren} = app
        _ -> Kore.Error.koreFail "expected symbol or alias application"

getStringLiteral :: AttributePattern -> Parser StringLiteral
getStringLiteral kore =
    case Recursive.project kore of
        _ :< StringLiteralF (Const lit) -> return lit
        _ -> Kore.Error.koreFail "expected string literal pattern"

getVariable :: AttributePattern -> Parser (SomeVariable VariableName)
getVariable kore =
    case Recursive.project kore of
        _ :< VariableF (Const var) -> return var
        _ -> Kore.Error.koreFail "expected variable pattern"

parseReadS :: ReadS a -> Text -> Parser a
parseReadS aReadS (Text.unpack -> syntax) =
    case aReadS syntax of
        [] -> noParse
        r : rs ->
            case rs of
                _ : _ -> ambiguousParse
                _
                    | null unparsed -> return a
                    | otherwise -> incompleteParse unparsed
          where
            (a, unparsed) = r
  where
    noParse = Kore.Error.koreFail ("failed to parse \"" ++ syntax ++ "\"")
    ambiguousParse =
        Kore.Error.koreFail $
            "parsing \"" ++ syntax ++ "\" was ambiguous"
    incompleteParse unparsed =
        Kore.Error.koreFail $
            "incomplete parse: failed to parse \"" ++ unparsed ++ "\""

  | Parse an ' Integer ' from a ' StringLiteral ' .
parseInteger :: StringLiteral -> Parser Integer
parseInteger = parseStringLiteral reads

  | Parse from a ' StringLiteral ' .
parseStringLiteral :: ReadS a -> StringLiteral -> Parser a
parseStringLiteral reads' (StringLiteral literal) = parseReadS reads' literal

  |  an ' SExpr ' for the @smtlib@ attribute . 

 An error is signalled in '  ' if we can not parse the ' SExpr ' , or if the 
 entire argument is not consumed by the parser . 


An error is signalled in 'Parser' if we cannot parse the 'SExpr', or if the
entire argument is not consumed by the parser.
-}
parseSExpr ::
  | text representing an ' SExpr '
    Text ->
    Parser SExpr
parseSExpr syntax =
    case readSExprs syntax of
        [] -> noParse
        sExpr : rest ->
            case rest of
                [] -> return sExpr
                _ -> incompleteParse
  where
    noParse = Kore.Error.koreFail "failed to parse S-expression"
    incompleteParse = Kore.Error.koreFail "failed to parse entire argument"

instance ParseAttributes Attribute.Smtlib where
    parseAttribute =
        withApplication' $ \params args Attribute.Smtlib{getSmtlib} -> do
            getZeroParams params
            arg <- getOneArgument args
            StringLiteral syntax <- getStringLiteral arg
            sExpr <- parseSExpr syntax
            unless (isNothing getSmtlib) failDuplicate'
            return Attribute.Smtlib{getSmtlib = Just sExpr}
      where
        withApplication' = withApplication Attribute.smtlibId
        failDuplicate' = failDuplicate Attribute.smtlibId
