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.

Sign up for GitHub

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

crucible-syntax: Separate interface and implementation of parsing monad #1133

Merged
merged 1 commit into from
Nov 15, 2023
Merged

crucible-syntax: Separate interface and implementation of parsing monad #1133

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
4 changes: 2 additions & 2 deletions crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,8 +51,8 @@ import Lang.Crucible.Syntax.Atoms (Atomic)
import Lang.Crucible.Syntax.Atoms qualified as Atom
import Lang.Crucible.Syntax.Concrete (ParserHooks(..), SyntaxState)
import Lang.Crucible.Syntax.Concrete qualified as Parse
import Lang.Crucible.Syntax.ExprParse (MonadSyntax)
import Lang.Crucible.Syntax.ExprParse qualified as Parse
import Lang.Crucible.Syntax.Monad (MonadSyntax)
import Lang.Crucible.Syntax.Monad qualified as Parse

-- | A 'ParserHooks' instance that adds no further extensions to the language.
emptyParserHooks :: ParserHooks ext
Expand Down
6 changes: 3 additions & 3 deletions crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax/TypeAlias.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ import Data.Parameterized.Some ( Some(..) )
import qualified Lang.Crucible.LLVM.MemModel as LCLM
import qualified Lang.Crucible.Syntax.Atoms as LCSA
import qualified Lang.Crucible.Syntax.Concrete as LCSC
import qualified Lang.Crucible.Syntax.ExprParse as LCSE
import qualified Lang.Crucible.Syntax.Monad as LCSM
import qualified Lang.Crucible.Types as LCT

-- | Additional types beyond those built into crucible-llvm-syntax.
Expand Down Expand Up @@ -81,7 +81,7 @@ x86_64LinuxTypes =

-- | Parser for type extensions to Crucible syntax
typeMapParser ::
LCSE.MonadSyntax LCSA.Atomic m =>
LCSM.MonadSyntax LCSA.Atomic m =>
-- | A mapping from type names to the crucible types they represent
Map.Map LCSA.AtomName (Some LCT.TypeRepr) ->
m (Some LCT.TypeRepr)
Expand All @@ -93,7 +93,7 @@ typeMapParser types = do

-- | Parser for type aliases for the Crucible-LLVM syntax
typeAliasParser ::
LCSE.MonadSyntax LCSA.Atomic m =>
LCSM.MonadSyntax LCSA.Atomic m =>
TypeLookup ->
m (Some LCT.TypeRepr)
typeAliasParser (TypeLookup lookupFn) =
Expand Down
1 change: 1 addition & 0 deletions crucible-syntax/crucible-syntax.cabal
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -112,6 +112,7 @@ library
Lang.Crucible.Syntax.SExpr
Lang.Crucible.Syntax.Overrides
Lang.Crucible.Syntax.ExprParse
Lang.Crucible.Syntax.Monad
Lang.Crucible.Syntax.Prog

ghc-options: -Wall -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns
Expand Down
4 changes: 2 additions & 2 deletions crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -92,6 +92,7 @@ import Numeric.Natural
import qualified Lang.Crucible.CFG.Extension as LCCE
import Lang.Crucible.Syntax.ExprParse hiding (SyntaxError)
import qualified Lang.Crucible.Syntax.ExprParse as SP
import Lang.Crucible.Syntax.Monad

import What4.ProgramLoc
import What4.FunctionName
Expand All @@ -109,7 +110,6 @@ import Lang.Crucible.FunctionHandle
import Numeric.Natural ()
import qualified Data.Set as Set


liftSyntaxParse :: (MonadError (ExprErr s) m, MonadIO m)
=> SyntaxParse Atomic a -> AST s -> m a
liftSyntaxParse p ast =
Expand Down Expand Up @@ -790,7 +790,7 @@ synthExpr typeHint =
describe (T.pack (show n) <> " is an invalid index into " <> T.pack (show ts)) empty
Just (Some idx) ->
do let ty = view (ixF' idx) ts
out <- withProgressStep Rest $ withProgressStep Rest $ withProgressStep SP.First $
out <- withProgressStep Rest $ withProgressStep Rest $ withProgressStep First $
parse e (check ty)
return $ SomeE (VariantRepr ts) $ EApp $ InjectVariant ts idx out
Just (Some t) ->
Expand Down
Loading
Loading