diff --git a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
index 7b1eccea4..4c8ea64f9 100644
--- a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
+++ b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax.hs
@@ -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
diff --git a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax/TypeAlias.hs b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax/TypeAlias.hs
index 092d61231..4428af6fb 100644
--- a/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax/TypeAlias.hs
+++ b/crucible-llvm-syntax/src/Lang/Crucible/LLVM/Syntax/TypeAlias.hs
@@ -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.
@@ -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)
@@ -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) =
diff --git a/crucible-syntax/crucible-syntax.cabal b/crucible-syntax/crucible-syntax.cabal
index 78463b867..2839dba14 100644
--- a/crucible-syntax/crucible-syntax.cabal
+++ b/crucible-syntax/crucible-syntax.cabal
@@ -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
diff --git a/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs b/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs
index 4249c850a..7337a898f 100644
--- a/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs
+++ b/crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs
@@ -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
@@ -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 =
@@ -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) ->
diff --git a/crucible-syntax/src/Lang/Crucible/Syntax/ExprParse.hs b/crucible-syntax/src/Lang/Crucible/Syntax/ExprParse.hs
index e33028c12..5719f863c 100644
--- a/crucible-syntax/src/Lang/Crucible/Syntax/ExprParse.hs
+++ b/crucible-syntax/src/Lang/Crucible/Syntax/ExprParse.hs
@@ -15,49 +15,12 @@
 {-# LANGUAGE ViewPatterns #-}
 
 module Lang.Crucible.Syntax.ExprParse
-  ( MonadSyntax(..)
-  , SyntaxParse
+  ( SyntaxParse
   , syntaxParseIO
 
-  -- * Describing syntax
-  , describe
-  , atom
-  , cons
-  , depCons
-  , depConsCond
-  , followedBy
-  , rep
-  , list
-  , backwards
-  , emptyList
-  , atomic
-  , anyList
-  , sideCondition
-  , sideCondition'
-  , satisfy
-
-  -- * Eliminating location information
-  , syntaxToDatum
-  , datum
-
-  -- * Parsing context
-  , position
-  , withProgressStep
-
-  -- * Control structures
-  , commit
-  , parse
-
-  -- * Progress through a parsing problem
-  , ProgressStep(..)
-  , Progress
-  , pushProgress
-
   -- * Errors
-  , later
   , SyntaxError(..)
   , printSyntaxError
-  , Reason(..)
 
   -- * Testing utilities
   , TrivialAtom(..)
@@ -70,12 +33,6 @@ import Control.Monad (MonadPlus(..), ap)
 import Control.Monad.IO.Class (MonadIO)
 import Control.Monad.Reader (MonadReader(..), ReaderT(..))
 import qualified Control.Monad.State.Strict as Strict
-import qualified Control.Monad.State.Lazy as Lazy
-import Control.Monad.State.Class
-import Control.Monad.Trans.Class (MonadTrans(..))
-import qualified Control.Monad.Writer.Strict as Strict
-import qualified Control.Monad.Writer.Lazy as Lazy
-import Control.Monad.Writer.Class
 
 import Data.Foldable as Foldable
 import Data.List
@@ -92,7 +49,7 @@ import Lang.Crucible.Syntax.SExpr
 
 import qualified Text.Megaparsec as MP
 
-import What4.ProgramLoc (Posd(..), Position)
+import Lang.Crucible.Syntax.Monad
 
 data Search a = Try a (Search a) | Fail | Cut
   deriving Functor
@@ -146,52 +103,6 @@ delimitSearch Cut = Fail
 cutSearch :: Search a
 cutSearch = Cut
 
--- | Components of a path taken through a syntax object to reach the
--- current focus.
-data ProgressStep =
-    First -- ^ The head of a list was followed
-  | Rest -- ^ The tail of a list was followed
-  | Late -- ^ The path was annotated as 'later'
-  deriving (Eq, Show)
-
-instance Ord ProgressStep where
-  compare First First = EQ
-  compare First _ = LT
-  compare Rest First = GT
-  compare Rest Rest = EQ
-  compare Rest _ = LT
-  compare Late Late = EQ
-  compare Late _ = GT
-
--- | The path taken through a syntax object to reach the current
--- focus.
-newtype Progress = Progress [ProgressStep]
-  deriving (Eq, Show)
-
--- | Add a step to a progress path
-pushProgress :: ProgressStep -> Progress -> Progress
-pushProgress p (Progress ps) = Progress (p : ps)
-
-instance Ord Progress where
-  compare (Progress xs) (Progress ys) =
-    case (xs, ys) of
-      ([], []) -> EQ
-      ([], _:_) -> LT
-      (_:_, []) -> GT
-      (x:xs', y:ys') ->
-        case compare (Progress xs') (Progress ys') of
-          LT -> LT
-          GT -> GT
-          EQ -> compare x y
-
-
--- | The reason why a failure has occurred, consisting of description
--- 'message' combined with the focus that was described.
-data Reason atom = Reason { expr :: Syntax atom
-                          , message :: Text
-                          }
-  deriving (Functor, Show, Eq)
-
 data Failure atom = Ok | Oops Progress (NonEmpty (Reason atom))
   deriving (Functor, Show)
 
@@ -234,10 +145,7 @@ instance MonadPlus (P atom) where
   mplus = (<|>)
 
 newtype STP atom a = STP { runSTP :: IO (P atom a) }
-  deriving (Semigroup, Monoid)
-
-instance Functor (STP atom) where
-  fmap f (STP x) = STP $ fmap (fmap f) x
+  deriving (Functor, Semigroup, Monoid)
 
 instance Applicative (STP atom) where
   pure = STP . pure . pure
@@ -290,35 +198,6 @@ instance MonadPlus (SyntaxParse atom) where
   mzero = empty
   mplus = (<|>)
 
--- | Monads that can parse syntax need a few fundamental operations.
--- A parsing monad maintains an implicit "focus", which is the syntax
--- currently being matched, as well as the progress, which is the path
--- taken through the surrounding syntactic context to reach the
--- current focus. Additionally, the reason for a failure will always
--- be reported with respect to explicit descriptions - these are
--- inserted through 'withReason'.
-class (Alternative m, Monad m) => MonadSyntax atom m | m -> atom where
-  -- | Succeed with the current focus.
-  anything :: m (Syntax atom)
-  -- | Succeed with the current progress.
-  progress :: m Progress
-  -- | Run a new parser with a different focus.
-  withFocus :: Syntax atom -> m a -> m a
-  -- | Run a parser in a modified notion of progress.
-  withProgress :: (Progress -> Progress) -> m a -> m a
-  -- | Run a parser with a new reason for failure.
-  withReason :: Reason atom -> m a -> m a
-  -- | Fail, and additionally prohibit backtracking across the failure.
-  cut :: m a
-  -- | Delimit the dynamic extent of a 'cut'.
-  delimit :: m a -> m a
-  -- | Make the first solution reported by a computation into the only
-  -- solution reported, eliminating further backtracking and previous
-  -- errors. This allows syntax to be matched in exclusive "layers",
-  -- reminiscent of the effect of trampolining through a macro
-  -- expander. Use when solutions are expected to be unique.
-  call :: m a -> m a
-
 instance MonadSyntax atom (SyntaxParse atom) where
   anything = view parseFocus
   progress = view parseProgress
@@ -347,305 +226,6 @@ instance MonadSyntax atom (SyntaxParse atom) where
         Cut -> P Cut e
         Fail -> P Fail e
 
-instance MonadSyntax atom m => MonadSyntax atom (ReaderT r m) where
-  anything = lift anything
-  cut = lift cut
-  progress = lift progress
-  delimit m =
-    do r <- ask
-       lift $ delimit (runReaderT m r)
-  call m =
-    do r <- ask
-       lift $ call (runReaderT m r)
-  withFocus stx m =
-    do r <- ask
-       lift $ withFocus stx (runReaderT m r)
-  withProgress p m =
-    do r <- ask
-       lift $ withProgress p (runReaderT m r)
-  withReason why m =
-    do r <- ask
-       lift $ withReason why (runReaderT m r)
-
-
-
-instance (MonadPlus m, MonadSyntax atom m) => MonadSyntax atom (Strict.StateT s m) where
-  anything = lift anything
-  cut = lift cut
-  progress = lift progress
-  delimit m =
-    do st <- get
-       (s, st') <- lift $ delimit (Strict.runStateT m st)
-       put st'
-       return s
-  call m =
-    do st <- get
-       (s, st') <- lift $ call (Strict.runStateT m st)
-       put st'
-       return s
-  withFocus stx m =
-    do st <- get
-       (s, st') <- lift $ withFocus stx (Strict.runStateT m st)
-       put st'
-       return s
-  withProgress p m =
-    do st <- get
-       (s, st') <- lift $ withProgress p (Strict.runStateT m st)
-       put st'
-       return s
-  withReason why m =
-    do st <- get
-       (s, st') <- lift $ withReason why (Strict.runStateT m st)
-       put st'
-       return s
-
-instance (MonadPlus m, MonadSyntax atom m) => MonadSyntax atom (Lazy.StateT s m) where
-  anything = lift anything
-  cut = lift cut
-  progress = lift progress
-  delimit m =
-    do st <- get
-       (s, st') <- lift $ delimit (Lazy.runStateT m st)
-       put st'
-       return s
-  call m =
-    do st <- get
-       (s, st') <- lift $ call (Lazy.runStateT m st)
-       put st'
-       return s
-  withFocus stx m =
-    do st <- get
-       (s, st') <- lift $ withFocus stx (Lazy.runStateT m st)
-       put st'
-       return s
-  withProgress p m =
-    do st <- get
-       (s, st') <- lift $ withProgress p (Lazy.runStateT m st)
-       put st'
-       return s
-  withReason why m =
-    do st <- get
-       (s, st') <- lift $ withReason why (Lazy.runStateT m st)
-       put st'
-       return s
-
-
-instance (Monoid w, MonadSyntax atom m) => MonadSyntax atom (Strict.WriterT w m) where
-  anything = lift anything
-  cut = lift cut
-  progress = lift progress
-  delimit m =
-    do (x, w) <- lift $ delimit $ Strict.runWriterT m
-       tell w
-       return x
-  call m =
-    do (x, w) <- lift $ call $ Strict.runWriterT m
-       tell w
-       return x
-  withFocus stx m =
-    do (x, w) <- lift $ withFocus stx $ Strict.runWriterT m
-       tell w
-       return x
-  withProgress p m =
-    do (x, w) <- lift $ withProgress p $ Strict.runWriterT m
-       tell w
-       return x
-  withReason why m =
-    do (x, w) <- lift $ withReason why $ Strict.runWriterT m
-       tell w
-       return x
-
-
-instance (Monoid w, MonadSyntax atom m) => MonadSyntax atom (Lazy.WriterT w m) where
-  anything = lift anything
-  cut = lift cut
-  progress = lift progress
-  delimit m =
-    do (x, w) <- lift $ delimit $ Lazy.runWriterT m
-       tell w
-       return x
-  call m =
-    do (x, w) <- lift $ call $ Lazy.runWriterT m
-       tell w
-       return x
-  withFocus stx m =
-    do (x, w) <- lift $ withFocus stx $ Lazy.runWriterT m
-       tell w
-       return x
-  withProgress p m =
-    do (x, w) <- lift $ withProgress p $ Lazy.runWriterT m
-       tell w
-       return x
-  withReason why m =
-    do (x, w) <- lift $ withReason why $ Lazy.runWriterT m
-       tell w
-       return x
-
-
-
-
--- | Strip location information from a syntax object
-syntaxToDatum :: Syntactic expr atom => expr -> Datum atom
-syntaxToDatum (A x) = Datum $ Atom x
-syntaxToDatum (L ls) = Datum $ List $ map syntaxToDatum ls
-syntaxToDatum _ = error "syntaxToDatum: impossible case - bad Syntactic instance"
-
--- | Succeed if and only if the focus satisfies a Boolean predicate.
-satisfy :: MonadSyntax atom m => (Syntax atom -> Bool) -> m (Syntax atom)
-satisfy p =
-  do foc <- anything
-     if p foc
-       then pure foc
-       else empty
-
--- | Succeed only if the focus, having been stripped of position
--- information, is structurally equal to some datum.
-datum :: (MonadSyntax atom m, IsAtom atom, Eq atom) => Datum atom -> m ()
-datum dat =
-  describe (datumToText mempty dat) $
-    satisfy (\stx -> dat == syntaxToDatum stx) *> pure ()
-
--- | Succeed if and only if the focus is some particular given atom.
-atom :: (MonadSyntax atom m, IsAtom atom, Eq atom) => atom -> m ()
-atom a = datum (Datum (Atom a))
-
--- | Succeed if and only if the focus is any atom, returning the atom.
-atomic :: MonadSyntax atom m => m atom
-atomic = sideCondition "an atom" perhapsAtom (syntaxToDatum <$> anything)
-  where perhapsAtom (Datum (Atom a)) = Just a
-        perhapsAtom _ = Nothing
-
--- | Annotate a parser with a description, documenting its role in the
--- grammar. These descriptions are used to construct error messages.
-describe :: MonadSyntax atom m => Text -> m a -> m a
-describe !d p =
-  do foc <- anything
-     withReason (Reason foc d) p
-
--- | Succeed if and only if the focus is the empty list.
-emptyList :: MonadSyntax atom m => m ()
-emptyList = describe (T.pack "empty expression ()") (satisfy (isNil . syntaxToDatum) *> pure ())
-  where isNil (Datum (List [])) = True
-        isNil _ = False
-
--- | Succeed if and only if the focus is a list, returning its contents.
-anyList :: MonadSyntax atom m => m [Syntax atom]
-anyList = sideCondition "zero or more expressions, in parentheses" isList anything
-  where isList (Syntax (pos_val -> List xs)) = Just xs
-        isList _ = Nothing
-
--- | If the current focus is a list, apply one parser to its head and
--- another to its tail.
-cons :: MonadSyntax atom m => m a -> m b -> m (a, b)
-cons a d = depCons a (\x -> d >>= \y -> pure (x, y))
-
--- | If the current focus is a list, apply one parser to its head and
--- another to its tail, ignoring the result of the head.
-followedBy :: MonadSyntax atom m => m a -> m b -> m b
-followedBy a d = depCons a (const d)
-
--- | Return the source position of the focus.
-position :: MonadSyntax atom m => m Position
-position = syntaxPos <$> anything
-
--- | Manually add a progress step to the current path through the
--- context. Use this to appropriately guard calls to 'parse'.
-withProgressStep :: (MonadSyntax atom m) => ProgressStep -> m a -> m a
-withProgressStep s = withProgress (pushProgress s)
-
-
--- | A dependent cons (see 'depcons') that can impose a validation
--- step on the head of a list focus. If the head fails the validation
--- (that is, the second action returns 'Left'), the error is reported
--- in the head position.
-depConsCond :: MonadSyntax atom m => m a -> (a -> m (Either Text b)) -> m b
-depConsCond a d =
-  do focus <- anything
-     case focus of
-       L (e:es) ->
-         do x <- withFocus e $ withProgressStep First $ a
-            let cdr = Syntax (Posd (syntaxPos focus) (List es))
-            res <- withFocus cdr $ withProgressStep Rest $ d x
-            case res of
-              Right answer -> return answer
-              Left what -> withFocus e $ withProgressStep First $ later $ describe what empty
-       _ -> empty
-
--- | Use the result of parsing the head of the current-focused list to
--- compute a parsing action to use for the tail of the list.
-depCons :: MonadSyntax atom m => m a -> (a -> m b) -> m b
-depCons a d =
-  do focus <- anything
-     case focus of
-       L (e:es) ->
-         do x <- withFocus e $ withProgressStep First $ a
-            let cdr = Syntax (Posd (syntaxPos focus) (List es))
-            withFocus cdr $ withProgressStep Rest $ d x
-       _ -> empty
-
--- | Produce a parser that matches a list of things matched by another
--- parser.
-rep :: MonadSyntax atom m => m a -> m [a]
-rep p =
-  do focus <- anything
-     case focus of
-       L [] ->
-         pure []
-       L (e:es) ->
-         do x <- withFocus e $ withProgressStep First p
-            let cdr = Syntax (Posd (syntaxPos focus) (List es))
-            xs <- withFocus cdr $ withProgressStep Rest $ rep p
-            pure (x : xs)
-       _ -> empty
-
--- | Manually override the focus. Use this with care - it can lead to
--- bogus error selection unless 'withProgress' is used to provide an
--- appropriate path.
-parse :: MonadSyntax atom m => Syntax atom -> m a -> m a
-parse = withFocus
-
--- | Match a list focus elementwise.
-list :: MonadSyntax atom m => [m a] -> m [a]
-list parsers = describe desc $ list' parsers
-  where desc =
-          mappend (T.pack (show (length parsers))) (T.pack " expressions")
-        list' ps =
-          do focus <- anything
-             case focus of
-               L es -> go (syntaxPos focus) ps es
-               _ -> empty
-
-        go _ [] [] = pure []
-        go _ (_:_) [] = empty
-        go _ [] (_:_) = empty
-        go loc (p:ps) (e:es) =
-          do x <- withFocus e $ withProgressStep First p
-             xs <- withFocus (Syntax (Posd loc (List es))) $
-                   withProgressStep Rest $
-                   list' ps
-             pure (x : xs)
-
--- | Transform a parser such that its errors are considered to occur
--- after others, and thus be reported with a higher priority.
-later :: MonadSyntax atom m => m a -> m a
-later = withProgressStep Late
-
--- | Impose a side condition on a parser, failing with the given
--- description if the side condition is 'Nothing'.
-sideCondition :: MonadSyntax atom m => Text -> (a -> Maybe b) -> m a -> m b
-sideCondition !msg ok p =
-  do x <- p
-     case ok x of
-       Just y -> pure y
-       Nothing ->
-         later $ describe msg empty
-
--- | Impose a Boolean side condition on a parser, failing with the
--- given description if the side condition is 'False'.
-sideCondition' :: MonadSyntax atom m => Text -> (a -> Bool) -> m a -> m a
-sideCondition' !msg ok p = sideCondition msg (\x -> if ok x then Just x else Nothing) p
-
-
 -- | Syntax errors explain why the error occurred.
 data SyntaxError atom = SyntaxError (NonEmpty (Reason atom))
   deriving (Show, Eq)
@@ -673,7 +253,7 @@ syntaxParseIO :: IsAtom atom => SyntaxParse atom a -> Syntax atom -> IO (Either
 syntaxParseIO p stx = do
   (P yes no) <-
         runSTP $ runReaderT (runSyntaxParse p) $
-          SyntaxParseCtx (Progress []) (Reason stx (T.pack "bad syntax")) stx
+          SyntaxParseCtx emptyProgress (Reason stx (T.pack "bad syntax")) stx
   case Foldable.toList yes of
     [] ->
       return $ Left $ SyntaxError $
@@ -682,19 +262,6 @@ syntaxParseIO p stx = do
           Oops _ rs -> rs
     (r:_) -> return $ Right r
 
--- | When the current focus is a list, reverse its contents while
--- invoking another parser. If it is not a list, fail.
-backwards :: MonadSyntax atom m => m a -> m a
-backwards p =
-  do foc <- anything
-     case foc of
-      l@(L xs) -> withFocus (Syntax (Posd (syntaxPos l) (List (reverse xs)))) p
-      _ -> empty
-
--- | Trivially succeed, but prevent backtracking.
-commit :: MonadSyntax atom m => m ()
-commit = pure () <|> cut
-
 -- | A trivial atom, which is a wrapper around 'Text', for use when testing the library.
 newtype TrivialAtom = TrivialAtom Text deriving (Show, Eq)
 
diff --git a/crucible-syntax/src/Lang/Crucible/Syntax/Monad.hs b/crucible-syntax/src/Lang/Crucible/Syntax/Monad.hs
new file mode 100644
index 000000000..6acecd8da
--- /dev/null
+++ b/crucible-syntax/src/Lang/Crucible/Syntax/Monad.hs
@@ -0,0 +1,524 @@
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PartialTypeSignatures #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ViewPatterns #-}
+
+module Lang.Crucible.Syntax.Monad
+  ( MonadSyntax(..)
+
+  -- * Describing syntax
+  , describe
+  , atom
+  , cons
+  , depCons
+  , depConsCond
+  , followedBy
+  , rep
+  , list
+  , backwards
+  , emptyList
+  , atomic
+  , anyList
+  , sideCondition
+  , sideCondition'
+  , satisfy
+
+  -- * Eliminating location information
+  , syntaxToDatum
+  , datum
+
+  -- * Parsing context
+  , position
+  , withProgressStep
+
+  -- * Control structures
+  , commit
+  , parse
+
+  -- * Progress through a parsing problem
+  , ProgressStep(..)
+  , Progress
+  , emptyProgress
+  , pushProgress
+
+  -- * Errors
+  , later
+  , Reason(..)
+  ) where
+
+import Control.Applicative
+import Control.Monad (MonadPlus(..), ap)
+import Control.Monad.Reader (MonadReader(..), ReaderT(..))
+import qualified Control.Monad.State.Strict as Strict
+import qualified Control.Monad.State.Lazy as Lazy
+import Control.Monad.State.Class
+import Control.Monad.Trans.Class (MonadTrans(..))
+import qualified Control.Monad.Writer.Strict as Strict
+import qualified Control.Monad.Writer.Lazy as Lazy
+import Control.Monad.Writer.Class
+
+import Data.Foldable as Foldable
+import Data.List.NonEmpty (NonEmpty(..))
+import Data.Text (Text)
+import qualified Data.Text as T
+
+import Lang.Crucible.Syntax.SExpr
+
+import What4.ProgramLoc (Posd(..), Position)
+
+data Search a = Try a (Search a) | Fail | Cut
+  deriving Functor
+
+instance Applicative Search where
+  pure x = Try x Fail
+  (<*>) = ap
+
+instance Alternative Search where
+  empty = Fail
+  x <|> y =
+    case x of
+      Try first rest -> Try first (rest <|> y)
+      Fail -> y
+      Cut -> Cut
+
+instance Monad Search where
+  m >>= f =
+    case m of
+      Try x more -> f x <|> (more >>= f)
+      Fail -> Fail
+      Cut -> Fail
+
+instance MonadPlus Search where
+  mzero = empty
+  mplus = (<|>)
+
+instance Semigroup (Search a) where
+  (<>) = (<|>)
+
+instance Monoid (Search a) where
+  mempty  = empty
+
+instance Foldable Search where
+  foldMap f (Try x xs) = f x `mappend` foldMap f xs
+  foldMap _ _ = mempty
+
+  toList (Try x xs) = x : toList xs
+  toList _          = []
+
+instance Traversable Search where
+  traverse f (Try x xs) = Try <$> f x <*> traverse f xs
+  traverse _ Fail = pure Fail
+  traverse _ Cut = pure Cut
+
+-- | Components of a path taken through a syntax object to reach the
+-- current focus.
+data ProgressStep =
+    First -- ^ The head of a list was followed
+  | Rest -- ^ The tail of a list was followed
+  | Late -- ^ The path was annotated as 'later'
+  deriving (Eq, Show)
+
+instance Ord ProgressStep where
+  compare First First = EQ
+  compare First _ = LT
+  compare Rest First = GT
+  compare Rest Rest = EQ
+  compare Rest _ = LT
+  compare Late Late = EQ
+  compare Late _ = GT
+
+-- | The path taken through a syntax object to reach the current
+-- focus.
+newtype Progress = Progress [ProgressStep]
+  deriving (Eq, Show)
+
+-- | An empty path, used to initialize parsers
+emptyProgress :: Progress
+emptyProgress = Progress []
+
+-- | Add a step to a progress path
+pushProgress :: ProgressStep -> Progress -> Progress
+pushProgress p (Progress ps) = Progress (p : ps)
+
+instance Ord Progress where
+  compare (Progress xs) (Progress ys) =
+    case (xs, ys) of
+      ([], []) -> EQ
+      ([], _:_) -> LT
+      (_:_, []) -> GT
+      (x:xs', y:ys') ->
+        case compare (Progress xs') (Progress ys') of
+          LT -> LT
+          GT -> GT
+          EQ -> compare x y
+
+
+-- | The reason why a failure has occurred, consisting of description
+-- 'message' combined with the focus that was described.
+data Reason atom = Reason { expr :: Syntax atom
+                          , message :: Text
+                          }
+  deriving (Functor, Show, Eq)
+
+data Failure atom = Ok | Oops Progress (NonEmpty (Reason atom))
+  deriving (Functor, Show)
+
+instance Semigroup (Failure atom) where
+  Ok              <> e2 = e2
+  e1@(Oops _ _)   <> Ok = e1
+  e1@(Oops p1 r1) <> e2@(Oops p2 r2) =
+    case compare p1 p2 of
+      LT -> e2
+      GT -> e1
+      EQ -> Oops p1 (r1 <> r2)
+
+instance Monoid (Failure atom) where
+  mempty = Ok
+
+data P atom a = P { _success :: Search a
+                  , _failure :: Failure atom
+                  }
+  deriving Functor
+
+-- | Monads that can parse syntax need a few fundamental operations.
+-- A parsing monad maintains an implicit "focus", which is the syntax
+-- currently being matched, as well as the progress, which is the path
+-- taken through the surrounding syntactic context to reach the
+-- current focus. Additionally, the reason for a failure will always
+-- be reported with respect to explicit descriptions - these are
+-- inserted through 'withReason'.
+class (Alternative m, Monad m) => MonadSyntax atom m | m -> atom where
+  -- | Succeed with the current focus.
+  anything :: m (Syntax atom)
+  -- | Succeed with the current progress.
+  progress :: m Progress
+  -- | Run a new parser with a different focus.
+  withFocus :: Syntax atom -> m a -> m a
+  -- | Run a parser in a modified notion of progress.
+  withProgress :: (Progress -> Progress) -> m a -> m a
+  -- | Run a parser with a new reason for failure.
+  withReason :: Reason atom -> m a -> m a
+  -- | Fail, and additionally prohibit backtracking across the failure.
+  cut :: m a
+  -- | Delimit the dynamic extent of a 'cut'.
+  delimit :: m a -> m a
+  -- | Make the first solution reported by a computation into the only
+  -- solution reported, eliminating further backtracking and previous
+  -- errors. This allows syntax to be matched in exclusive "layers",
+  -- reminiscent of the effect of trampolining through a macro
+  -- expander. Use when solutions are expected to be unique.
+  call :: m a -> m a
+
+instance MonadSyntax atom m => MonadSyntax atom (ReaderT r m) where
+  anything = lift anything
+  cut = lift cut
+  progress = lift progress
+  delimit m =
+    do r <- ask
+       lift $ delimit (runReaderT m r)
+  call m =
+    do r <- ask
+       lift $ call (runReaderT m r)
+  withFocus stx m =
+    do r <- ask
+       lift $ withFocus stx (runReaderT m r)
+  withProgress p m =
+    do r <- ask
+       lift $ withProgress p (runReaderT m r)
+  withReason why m =
+    do r <- ask
+       lift $ withReason why (runReaderT m r)
+
+instance (MonadPlus m, MonadSyntax atom m) => MonadSyntax atom (Strict.StateT s m) where
+  anything = lift anything
+  cut = lift cut
+  progress = lift progress
+  delimit m =
+    do st <- get
+       (s, st') <- lift $ delimit (Strict.runStateT m st)
+       put st'
+       return s
+  call m =
+    do st <- get
+       (s, st') <- lift $ call (Strict.runStateT m st)
+       put st'
+       return s
+  withFocus stx m =
+    do st <- get
+       (s, st') <- lift $ withFocus stx (Strict.runStateT m st)
+       put st'
+       return s
+  withProgress p m =
+    do st <- get
+       (s, st') <- lift $ withProgress p (Strict.runStateT m st)
+       put st'
+       return s
+  withReason why m =
+    do st <- get
+       (s, st') <- lift $ withReason why (Strict.runStateT m st)
+       put st'
+       return s
+
+instance (MonadPlus m, MonadSyntax atom m) => MonadSyntax atom (Lazy.StateT s m) where
+  anything = lift anything
+  cut = lift cut
+  progress = lift progress
+  delimit m =
+    do st <- get
+       (s, st') <- lift $ delimit (Lazy.runStateT m st)
+       put st'
+       return s
+  call m =
+    do st <- get
+       (s, st') <- lift $ call (Lazy.runStateT m st)
+       put st'
+       return s
+  withFocus stx m =
+    do st <- get
+       (s, st') <- lift $ withFocus stx (Lazy.runStateT m st)
+       put st'
+       return s
+  withProgress p m =
+    do st <- get
+       (s, st') <- lift $ withProgress p (Lazy.runStateT m st)
+       put st'
+       return s
+  withReason why m =
+    do st <- get
+       (s, st') <- lift $ withReason why (Lazy.runStateT m st)
+       put st'
+       return s
+
+instance (Monoid w, MonadSyntax atom m) => MonadSyntax atom (Strict.WriterT w m) where
+  anything = lift anything
+  cut = lift cut
+  progress = lift progress
+  delimit m =
+    do (x, w) <- lift $ delimit $ Strict.runWriterT m
+       tell w
+       return x
+  call m =
+    do (x, w) <- lift $ call $ Strict.runWriterT m
+       tell w
+       return x
+  withFocus stx m =
+    do (x, w) <- lift $ withFocus stx $ Strict.runWriterT m
+       tell w
+       return x
+  withProgress p m =
+    do (x, w) <- lift $ withProgress p $ Strict.runWriterT m
+       tell w
+       return x
+  withReason why m =
+    do (x, w) <- lift $ withReason why $ Strict.runWriterT m
+       tell w
+       return x
+
+instance (Monoid w, MonadSyntax atom m) => MonadSyntax atom (Lazy.WriterT w m) where
+  anything = lift anything
+  cut = lift cut
+  progress = lift progress
+  delimit m =
+    do (x, w) <- lift $ delimit $ Lazy.runWriterT m
+       tell w
+       return x
+  call m =
+    do (x, w) <- lift $ call $ Lazy.runWriterT m
+       tell w
+       return x
+  withFocus stx m =
+    do (x, w) <- lift $ withFocus stx $ Lazy.runWriterT m
+       tell w
+       return x
+  withProgress p m =
+    do (x, w) <- lift $ withProgress p $ Lazy.runWriterT m
+       tell w
+       return x
+  withReason why m =
+    do (x, w) <- lift $ withReason why $ Lazy.runWriterT m
+       tell w
+       return x
+
+-- | Strip location information from a syntax object
+syntaxToDatum :: Syntactic expr atom => expr -> Datum atom
+syntaxToDatum (A x) = Datum $ Atom x
+syntaxToDatum (L ls) = Datum $ List $ map syntaxToDatum ls
+syntaxToDatum _ = error "syntaxToDatum: impossible case - bad Syntactic instance"
+
+-- | Succeed if and only if the focus satisfies a Boolean predicate.
+satisfy :: MonadSyntax atom m => (Syntax atom -> Bool) -> m (Syntax atom)
+satisfy p =
+  do foc <- anything
+     if p foc
+       then pure foc
+       else empty
+
+-- | Succeed only if the focus, having been stripped of position
+-- information, is structurally equal to some datum.
+datum :: (MonadSyntax atom m, IsAtom atom, Eq atom) => Datum atom -> m ()
+datum dat =
+  describe (datumToText mempty dat) $
+    satisfy (\stx -> dat == syntaxToDatum stx) *> pure ()
+
+-- | Succeed if and only if the focus is some particular given atom.
+atom :: (MonadSyntax atom m, IsAtom atom, Eq atom) => atom -> m ()
+atom a = datum (Datum (Atom a))
+
+-- | Succeed if and only if the focus is any atom, returning the atom.
+atomic :: MonadSyntax atom m => m atom
+atomic = sideCondition "an atom" perhapsAtom (syntaxToDatum <$> anything)
+  where perhapsAtom (Datum (Atom a)) = Just a
+        perhapsAtom _ = Nothing
+
+-- | Annotate a parser with a description, documenting its role in the
+-- grammar. These descriptions are used to construct error messages.
+describe :: MonadSyntax atom m => Text -> m a -> m a
+describe !d p =
+  do foc <- anything
+     withReason (Reason foc d) p
+
+-- | Succeed if and only if the focus is the empty list.
+emptyList :: MonadSyntax atom m => m ()
+emptyList = describe (T.pack "empty expression ()") (satisfy (isNil . syntaxToDatum) *> pure ())
+  where isNil (Datum (List [])) = True
+        isNil _ = False
+
+-- | Succeed if and only if the focus is a list, returning its contents.
+anyList :: MonadSyntax atom m => m [Syntax atom]
+anyList = sideCondition "zero or more expressions, in parentheses" isList anything
+  where isList (Syntax (pos_val -> List xs)) = Just xs
+        isList _ = Nothing
+
+-- | If the current focus is a list, apply one parser to its head and
+-- another to its tail.
+cons :: MonadSyntax atom m => m a -> m b -> m (a, b)
+cons a d = depCons a (\x -> d >>= \y -> pure (x, y))
+
+-- | If the current focus is a list, apply one parser to its head and
+-- another to its tail, ignoring the result of the head.
+followedBy :: MonadSyntax atom m => m a -> m b -> m b
+followedBy a d = depCons a (const d)
+
+-- | Return the source position of the focus.
+position :: MonadSyntax atom m => m Position
+position = syntaxPos <$> anything
+
+-- | Manually add a progress step to the current path through the
+-- context. Use this to appropriately guard calls to 'parse'.
+withProgressStep :: (MonadSyntax atom m) => ProgressStep -> m a -> m a
+withProgressStep s = withProgress (pushProgress s)
+
+-- | A dependent cons (see 'depcons') that can impose a validation
+-- step on the head of a list focus. If the head fails the validation
+-- (that is, the second action returns 'Left'), the error is reported
+-- in the head position.
+depConsCond :: MonadSyntax atom m => m a -> (a -> m (Either Text b)) -> m b
+depConsCond a d =
+  do focus <- anything
+     case focus of
+       L (e:es) ->
+         do x <- withFocus e $ withProgressStep First $ a
+            let cdr = Syntax (Posd (syntaxPos focus) (List es))
+            res <- withFocus cdr $ withProgressStep Rest $ d x
+            case res of
+              Right answer -> return answer
+              Left what -> withFocus e $ withProgressStep First $ later $ describe what empty
+       _ -> empty
+
+-- | Use the result of parsing the head of the current-focused list to
+-- compute a parsing action to use for the tail of the list.
+depCons :: MonadSyntax atom m => m a -> (a -> m b) -> m b
+depCons a d =
+  do focus <- anything
+     case focus of
+       L (e:es) ->
+         do x <- withFocus e $ withProgressStep First $ a
+            let cdr = Syntax (Posd (syntaxPos focus) (List es))
+            withFocus cdr $ withProgressStep Rest $ d x
+       _ -> empty
+
+-- | Produce a parser that matches a list of things matched by another
+-- parser.
+rep :: MonadSyntax atom m => m a -> m [a]
+rep p =
+  do focus <- anything
+     case focus of
+       L [] ->
+         pure []
+       L (e:es) ->
+         do x <- withFocus e $ withProgressStep First p
+            let cdr = Syntax (Posd (syntaxPos focus) (List es))
+            xs <- withFocus cdr $ withProgressStep Rest $ rep p
+            pure (x : xs)
+       _ -> empty
+
+-- | Manually override the focus. Use this with care - it can lead to
+-- bogus error selection unless 'withProgress' is used to provide an
+-- appropriate path.
+parse :: MonadSyntax atom m => Syntax atom -> m a -> m a
+parse = withFocus
+
+-- | Match a list focus elementwise.
+list :: MonadSyntax atom m => [m a] -> m [a]
+list parsers = describe desc $ list' parsers
+  where desc =
+          mappend (T.pack (show (length parsers))) (T.pack " expressions")
+        list' ps =
+          do focus <- anything
+             case focus of
+               L es -> go (syntaxPos focus) ps es
+               _ -> empty
+
+        go _ [] [] = pure []
+        go _ (_:_) [] = empty
+        go _ [] (_:_) = empty
+        go loc (p:ps) (e:es) =
+          do x <- withFocus e $ withProgressStep First p
+             xs <- withFocus (Syntax (Posd loc (List es))) $
+                   withProgressStep Rest $
+                   list' ps
+             pure (x : xs)
+
+-- | Transform a parser such that its errors are considered to occur
+-- after others, and thus be reported with a higher priority.
+later :: MonadSyntax atom m => m a -> m a
+later = withProgressStep Late
+
+-- | Impose a side condition on a parser, failing with the given
+-- description if the side condition is 'Nothing'.
+sideCondition :: MonadSyntax atom m => Text -> (a -> Maybe b) -> m a -> m b
+sideCondition !msg ok p =
+  do x <- p
+     case ok x of
+       Just y -> pure y
+       Nothing ->
+         later $ describe msg empty
+
+-- | Impose a Boolean side condition on a parser, failing with the
+-- given description if the side condition is 'False'.
+sideCondition' :: MonadSyntax atom m => Text -> (a -> Bool) -> m a -> m a
+sideCondition' !msg ok p = sideCondition msg (\x -> if ok x then Just x else Nothing) p
+
+-- | When the current focus is a list, reverse its contents while
+-- invoking another parser. If it is not a list, fail.
+backwards :: MonadSyntax atom m => m a -> m a
+backwards p =
+  do foc <- anything
+     case foc of
+      l@(L xs) -> withFocus (Syntax (Posd (syntaxPos l) (List (reverse xs)))) p
+      _ -> empty
+
+-- | Trivially succeed, but prevent backtracking.
+commit :: MonadSyntax atom m => m ()
+commit = pure () <|> cut
diff --git a/crucible-syntax/test/Tests.hs b/crucible-syntax/test/Tests.hs
index f5a96309b..3db12baf8 100644
--- a/crucible-syntax/test/Tests.hs
+++ b/crucible-syntax/test/Tests.hs
@@ -15,6 +15,7 @@ import System.IO
 
 import Lang.Crucible.Syntax.Concrete (defaultParserHooks)
 import Lang.Crucible.Syntax.ExprParse
+import Lang.Crucible.Syntax.Monad
 import Lang.Crucible.Syntax.Prog (doParseCheck)
 import Lang.Crucible.Syntax.SExpr