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

syntax: Simplify parsing of endianness #458

Merged
merged 1 commit into from
Dec 19, 2024
Merged
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
35 changes: 14 additions & 21 deletions symbolic-syntax/src/Data/Macaw/Symbolic/Syntax.hs
Original file line number Diff line number Diff line change
Expand Up @@ -175,26 +175,18 @@ extensionParser wrappers hooks =
-- Pointer reads are a special case because we must parse the type of
-- the value to read as well as the endianness of the read before
-- parsing the additional arguments as Atoms.
LCSM.depCons LCSC.isType $ \(Some tp) ->
LCSM.depCons LCSC.atomName $ \endiannessName ->
case endiannessFromAtomName endiannessName of
Just endianness ->
let readWrapper =
buildPointerReadWrapper tp endianness in
go (SomeExtensionWrapper readWrapper)
Nothing -> empty
LCSM.depCons LCSC.isType $ \(Some tp) -> do
LCSM.depCons endianness $ \end ->
let readWrapper = buildPointerReadWrapper tp end in
go (SomeExtensionWrapper readWrapper)
LCSA.AtomName "pointer-write" -> do
-- Pointer writes are a special case because we must parse the type of
-- the value to write out as well as the endianness of the write before
-- parsing the additional arguments as Atoms.
LCSM.depCons LCSC.isType $ \(Some tp) ->
LCSM.depCons LCSC.atomName $ \endiannessName ->
case endiannessFromAtomName endiannessName of
Just endianness ->
let writeWrapper =
buildPointerWriteWrapper tp endianness in
go (SomeExtensionWrapper writeWrapper)
Nothing -> empty
LCSM.depCons endianness $ \end ->
let writeWrapper = buildPointerWriteWrapper tp end in
go (SomeExtensionWrapper writeWrapper)
LCSA.AtomName "bv-typed-literal" -> do
-- Bitvector literals with a type argument are a special case. We must
-- parse the type argument separately before parsing the remaining
Expand Down Expand Up @@ -223,12 +215,13 @@ extensionParser wrappers hooks =
return (Some endAtom)

-- Parse an 'LCSA.AtomName' representing an endianness into a
-- 'Maybe DMM.Endianness'
endiannessFromAtomName endianness =
case endianness of
LCSA.AtomName "le" -> Just DMM.LittleEndian
LCSA.AtomName "be" -> Just DMM.BigEndian
_ -> Nothing
-- 'DMM.Endianness'
endianness = do
LCSA.AtomName nm <- LCSC.atomName
case nm of
"le" -> pure DMM.LittleEndian
"be" -> pure DMM.BigEndian
_ -> empty

-- | Wrap a statement extension binary operator
binop :: (KnownNat w, Monad m)
Expand Down
Loading