Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove uses of klabel{}(_) attribute for special-casing symbols #3741

Merged
merged 9 commits into from
Mar 20, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions kore/src/Kore/Attribute/Symbol/SymbolKywd.hs
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ import Prelude.Kore
Hold an optional Text, which is an empty string if the attribute had
no argument. Use sites can check emptiness to achieve old behaviour.
-}
newtype SymbolKywd = SymbolKywd {getSymbol :: Maybe Text}
newtype SymbolKywd = SymbolKywd {getSymbolKywd :: Maybe Text}
deriving stock (Eq, Ord, Show)
deriving stock (GHC.Generic)
deriving anyclass (Hashable, NFData)
Expand Down Expand Up @@ -50,13 +50,13 @@ instance ParseAttributes SymbolKywd where
-- if an argument is present, use it for the contents, otherwise
-- leave it empty (but present) to signal presence of the attribute.
parseAttribute =
withApplication symbolKywdId $ \params args SymbolKywd{getSymbol} -> do
withApplication symbolKywdId $ \params args SymbolKywd{getSymbolKywd} -> do
Parser.getZeroParams params
mbArg <- Parser.getZeroOrOneArguments args
unless (isNothing getSymbol) $ failDuplicate symbolKywdId
unless (isNothing getSymbolKywd) $ failDuplicate symbolKywdId
StringLiteral arg <- maybe (pure $ StringLiteral "") getStringLiteral mbArg
pure $ SymbolKywd (Just arg)

instance From SymbolKywd Attributes where
from =
maybe def (from @AttributePattern . symbolKywdAttribute) . getSymbol
maybe def (from @AttributePattern . symbolKywdAttribute) . getSymbolKywd
4 changes: 2 additions & 2 deletions kore/src/Kore/Builtin/Endianness.hs
Original file line number Diff line number Diff line change
Expand Up @@ -62,9 +62,9 @@ endiannessVerifier ctor =
worker application = do
-- TODO (thomas.tuegel): Move the checks into the symbol verifiers.
unless (null arguments) (koreFail "expected zero arguments")
let Attribute.Symbol.SymbolKywd{getSymbol} =
let Attribute.Symbol.SymbolKywd{getSymbolKywd} =
Attribute.Symbol.symbolKywd $ symbolAttributes symbol
unless (isJust getSymbol) (koreFail "expected symbol'Kywd'{}() attribute")
unless (isJust getSymbolKywd) (koreFail "expected symbol'Kywd'{}() attribute")
return (EndiannessF . Const $ ctor symbol)
where
arguments = applicationChildren application
Expand Down
4 changes: 2 additions & 2 deletions kore/src/Kore/Builtin/Signedness.hs
Original file line number Diff line number Diff line change
Expand Up @@ -62,9 +62,9 @@ signednessVerifier ctor =
worker application = do
-- TODO (thomas.tuegel): Move the checks into the symbol verifiers.
unless (null arguments) (koreFail "expected zero arguments")
let Attribute.Symbol.SymbolKywd{getSymbol} =
let Attribute.Symbol.SymbolKywd{getSymbolKywd} =
Attribute.Symbol.symbolKywd $ symbolAttributes symbol
unless (isJust getSymbol) (koreFail "expected symbol'Kywd'{}() attribute")
unless (isJust getSymbolKywd) (koreFail "expected symbol'Kywd'{}() attribute")
return (SignednessF . Const $ ctor symbol)
where
arguments = applicationChildren application
Expand Down
7 changes: 6 additions & 1 deletion kore/src/Kore/Builtin/Verifiers.hs
Original file line number Diff line number Diff line change
Expand Up @@ -171,7 +171,7 @@ lookupApplicationVerifier ::
ApplicationVerifiers patternType ->
Maybe (ApplicationVerifier patternType)
lookupApplicationVerifier symbol verifiers = do
key <- getHook symbol <|> getKlabel symbol
key <- getHook symbol <|> getKlabel symbol <|> getSymbolKywd symbol
HashMap.lookup key verifiers
where
getHook =
Expand All @@ -184,6 +184,11 @@ lookupApplicationVerifier symbol verifiers = do
. Attribute.Symbol.getKlabel
. Attribute.Symbol.klabel
. symbolAttributes
getSymbolKywd =
fmap KlabelSymbolKey
. Attribute.Symbol.getSymbolKywd
. Attribute.Symbol.symbolKywd
. symbolAttributes

applicationPatternVerifierHooks ::
ApplicationVerifiers patternType ->
Expand Down
6 changes: 3 additions & 3 deletions kore/src/Kore/Internal/Symbol.hs
Original file line number Diff line number Diff line change
Expand Up @@ -229,11 +229,11 @@ klabel name =
(typed @Attribute.Symbol . typed @Attribute.Klabel)
Attribute.Klabel{getKlabel = Just name}

symbolKywd :: Symbol -> Symbol
symbolKywd =
symbolKywd :: Text -> Symbol -> Symbol
symbolKywd name =
Lens.set
(typed @Attribute.Symbol . typed @Attribute.SymbolKywd)
Attribute.SymbolKywd{getSymbol = Just ""}
Attribute.SymbolKywd{getSymbolKywd = Just name}

{- | Coerce a sort injection symbol's source and target sorts.

Expand Down
2 changes: 1 addition & 1 deletion kore/test/Test/Kore/Attribute/Symbol.hs
Original file line number Diff line number Diff line change
Expand Up @@ -187,7 +187,7 @@ test_SymbolKywd =
[ testCase "parseAttribute" $
assertEqual
"[symbolKywd{}()]"
(Right SymbolKywd{getSymbol = Just ""})
(Right SymbolKywd{getSymbolKywd = Just ""})
(symbolKywd <$> parse [symbolKywdAttribute ""])
, testCase "defaultSymbolAttributes" $
assertEqual
Expand Down
4 changes: 2 additions & 2 deletions kore/test/Test/Kore/Attribute/Symbol/SymbolKywd.hs
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ parseSymbolKywd = parseAttributes
test_symbolKywd :: TestTree
test_symbolKywd =
testCase "[symbolKywd{}()] :: SymbolKywd" $
expectSuccess SymbolKywd{getSymbol = Just ""} $
expectSuccess SymbolKywd{getSymbolKywd = Just ""} $
parseSymbolKywd $
Attributes [symbolKywdAttribute ""]

Expand All @@ -42,7 +42,7 @@ test_duplicate =
test_argument :: TestTree
test_argument =
testCase "[symbolKywd{}(\"legal\")]" $
expectSuccess SymbolKywd{getSymbol = Just "legal"} $
expectSuccess SymbolKywd{getSymbolKywd = Just "legal"} $
parseSymbolKywd $
Attributes [legalAttribute]
where
Expand Down
13 changes: 4 additions & 9 deletions kore/test/Test/Kore/Builtin/Definition.hs
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,6 @@ import Kore.Internal.Symbol (
function,
hook,
injective,
klabel,
smthook,
sortInjection,
symbolKywd,
Expand Down Expand Up @@ -732,32 +731,28 @@ concatString x y = mkApplySymbol concatStringSymbol [x, y]
littleEndianBytesSymbol :: Internal.Symbol
littleEndianBytesSymbol =
builtinSymbol "littleEndianBytes" endiannessSort []
& klabel "littleEndianBytes"
& symbolKywd
& symbolKywd "littleEndianBytes"
littleEndianBytes :: InternalVariable variable => TermLike variable
littleEndianBytes =
mkEndianness (Endianness.LittleEndian littleEndianBytesSymbol)
bigEndianBytesSymbol :: Internal.Symbol
bigEndianBytesSymbol =
builtinSymbol "bigEndianBytes" endiannessSort []
& klabel "bigEndianBytes"
& symbolKywd
& symbolKywd "bigEndianBytes"
bigEndianBytes :: InternalVariable variable => TermLike variable
bigEndianBytes =
mkEndianness (Endianness.BigEndian bigEndianBytesSymbol)
signedBytesSymbol :: Internal.Symbol
signedBytesSymbol =
builtinSymbol "signedBytes" signednessSort []
& klabel "signedBytes"
& symbolKywd
& symbolKywd "signedBytes"
signedBytes :: InternalVariable variable => TermLike variable
signedBytes =
mkSignedness (Signedness.Signed signedBytesSymbol)
unsignedBytesSymbol :: Internal.Symbol
unsignedBytesSymbol =
builtinSymbol "unsignedBytes" signednessSort []
& klabel "unsignedBytes"
& symbolKywd
& symbolKywd "unsignedBytes"
unsignedBytes :: InternalVariable variable => TermLike variable
unsignedBytes =
mkSignedness (Signedness.Unsigned unsignedBytesSymbol)
Expand Down
Loading
Loading