diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,83 @@
+
+# 0.4.1 -- 2025-03-21
+
+* Add a `Pretty` instance for ExprError.
+
+* Allow exotic characters (including Unicode symbols) in fresh atom
+names instead of having them be restricted to plain text identifiers.
+
+# 0.4 -- 2024-02-05
+
+* The type `ACFG` has been removed in favor of `Lang.Crucible.CFG.Reg.AnyCFG`,
+  which serves a similar purpose (hiding the argument and return types). The
+  CFG argument and return types can be recovered via
+  `Lang.Crucible.CFG.Reg.{cfgArgTypes,cfgReturnType}`.
+* `crucible-syntax` now supports simulating CFGs with language-specific syntax
+  extensions:
+
+  * `SimulateProgramHooks` now has a `setupHook` field that can run an arbitrary
+    override action before simulation. (For example, this is used in
+    `crucible-llvm-syntax` to initialize the LLVM memory global variable.)
+  * `SimulateProgramHooks` now has an extra `ext` type variable so that hooks
+    can be extension-specific.
+* `execCommand` and related data types in `Lang.Crucible.Syntax.Prog` have been
+  split off into a separate `crucible-cli` library.
+
+# 0.3
+
+* The return type of `prog`:
+
+  ```hs
+  TopParser s (Map GlobalName (Pair TypeRepr GlobalVar), [ACFG ext])
+  ```
+
+  Has been changed to:
+
+  ```hs
+  TopParser s (ParsedProgram ext)
+  ```
+
+  Where the `parsedProgGlobals :: Map GlobalName (Some GlobalVar)` and
+  `parsedProgCFGs :: [ACFG ext]` fields of `ParsedProgram` now serve the roles
+  previously filled by the first and second fields of the returned tuple. (Note
+  that `Pair TypeRepr GlobalVar` has been simplified to `Some GlobalVar`, as
+  the `TypeRepr` of a `GlobalVar` can be retrieved through its `globalType`
+  field.)
+* The type of `simulateProgram`'s last argument:
+
+  ```hs
+  simulateProgram
+    :: ...
+    -> (forall p sym ext t st fs. (IsSymInterface sym, sym ~ (ExprBuilder t st fs)) =>
+          sym -> HandleAllocator -> IO [(FnBinding p sym ext,Position)])
+    -> ...
+  ```
+
+  Has changed to the following:
+
+  ```hs
+  simulateProgram
+    :: ...
+    -> SimulateProgramHooks
+    -> ...
+  ```
+
+  Where the `setupOverridesHook` field of `SimulateProgramHooks` now serves the
+  role previously filled by the function argument.
+
+* `crucible-syntax` now supports _forward declarations_. A forward declaration
+  is like a function, but lacking a body, and is useful for situations where
+  one does not know what the implementation of a function will be until after
+  the `.cbl` file is parsed. See the `crucible-syntax` `README` for more
+  information.
+
+  There is also now an `extern` keyword, that acts like a forward declaration
+  for global variables.
+
+# 0.2
+
+* Various functions now take a `?parserHooks :: ParserHooks ext` implicit
+  argument, which supports arbitrary syntax extensions. Various data types now
+  also have an additional `ext` type parameter, which represents the type of
+  the parser extension being used. If you do not care about parser extensions,
+  a reasonable default choice is `?parserHooks = defaultParserHooks`.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2013-2022 Galois Inc.
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+  * Redistributions of source code must retain the above copyright
+    notice, this list of conditions and the following disclaimer.
+
+  * Redistributions in binary form must reproduce the above copyright
+    notice, this list of conditions and the following disclaimer in
+    the documentation and/or other materials provided with the
+    distribution.
+
+  * Neither the name of Galois, Inc. nor the names of its contributors
+    may be used to endorse or promote products derived from this
+    software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
+IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
+OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.txt b/README.txt
new file mode 100644
--- /dev/null
+++ b/README.txt
@@ -0,0 +1,135 @@
+This project defines a concrete syntax for a certain subset of the
+registerized Crucible CFGs.
+
+Some features are intentionally omitted, because they require
+compile-time additions to Crucible in the form of type class
+instances. In particular, there is no syntax for:
+
+ * Recursive types
+
+ * Extensions
+
+ * Concrete types
+
+
+How to use
+
+
+General syntax
+
+The basic syntax is based on a simplified variant of Lisp
+S-expressions, without support for dotted pairs or special syntax for
+quote or quasiquote. A syntactic form is either an atom or matching
+opening and closing parentheses with a whitespace-delimited sequence
+of syntactic forms between them.
+
+
+The atoms are as follows:
+
+ * Identifiers are either keywords or Crucible atom names. Every
+   identifier that is not a language keyword is a Crucible atom
+   name. Identifiers consist of a letter-like character followed by
+   zero or more digits or letter-like characters. Letter-like
+   characters are those considered letters by Unicode, or any of the
+   characters <, >, =, +, -, *, /, !, _, \, or ?.
+
+   The keywords are documented below, under each special form.
+
+ * Function names consist of an @ character followed by an identifier.
+
+ * Register names consist of a $ character followed by an identifier.
+
+ * Numbers consist of an optional '+' or '-' followed by an unsigned
+   number and an optional denominator. Unsigned numbers are either
+   decimal literals, octal literals, or hexadecimal literals, using
+   the typical syntax with a 0-prefix. A denominator is a '/'
+   character followed by an unsigned number.
+
+ * Boolean literals are #t or #T and #f or #F.
+
+ * String literals are delimited by double-quotes, and support
+   escaping with \.
+
+
+Line comments are preceded by ;, and block comments are delimited by
+#| and |#.
+
+
+Functions
+
+A program consists of a sequence of function definitions. A function
+definition is a form that begins with the keyword "defun", followed by
+a function name, argument list, return type, and body. A function name
+is a function name atom. An argument list is a form that contains zero
+or more argument specs. An argument spec is a two-element form, where
+the first is a Crucible atom name, and the second is a form that
+denotes a type. A return type is a form that denotes a type.
+
+A function body consists of an optional list of registers, a start
+block, and zero or more further blocks. A list of registers is a form
+that begins with the keyword "registers" and is followed by zero or
+more register specifications. A register specification is a form
+containing an atom name and a type.
+
+Blocks consist of the defblock keyword followed by a block body. Block
+bodies are zero or more ordinary statements followed by a terminating
+statement. The first block must begin with "start" instead of
+"defblock". In the future, the restriction that the start block comes
+first may be relaxed.
+
+Forward declarations
+
+A forward declaration is a form that begins with the keyword "declare",
+followed by a function name, argument list, and return type. A forward
+declaration is like a function but without the function body. Forward
+declarations are useful in situations where you do not know the definition
+of a function ahead of time, but you will know it at some point after parsing
+the program. It is the responsibility of the client to ensure that forward
+declarations are resolved to Crucible definitions before being invoked.
+
+Global variables
+
+A global variable is a form that begins with the keyword "defglobal", followed
+by an identifier prefixed with two dollar signs (e.g., $$global-name) as well
+as a type. A global variable is a mutable reference that scopes over all of the
+functions defined in the program. The value of a global variable can be set
+with the "set-global!" form.
+
+A program can reference a global variable defined externally by using an extern
+declaration. An extern declaration is exactly like a "defglobal" declaration,
+but using the "extern" keyword instead of "defglobal". The difference between
+an extern and a normal global variable is that the value of an extern may
+already have been set by the time that the .cbl file which declares the extern
+uses it. It is the responsibility of the client to ensure that externs are
+inserted into the Crucible symbolic global state before being accessed.
+
+Types
+
+si ::= 'Unicode' | 'Char16' | 'Char8'
+
+fi ::= 'Half' | 'Float' | 'Double' | 'Quad'
+     | 'X86_80' | 'DoubleDouble'
+
+t ::= 'Any' | 'Unit' | 'Bool' | 'Nat' | 'Integer' | 'Real'
+    | 'ComplexReal' | 'Char' | '(' 'String' si ')'
+    | '(' 'FP' fi ')' | '(' 'BitVector' n ')'
+    | '(' '->' t ... t ')' | '(' 'Maybe' t ')'
+    | '(' 'Sequence' t ')' | '(' 'Vector' t ')' | '(' 'Ref' t ')'
+    | '(' 'Struct' t ... t ')' | '(' 'Variant' t ... t ')'
+
+
+Expressions
+
+
+
+Registers
+
+
+Blocks
+
+
+Statements
+
+
+
+
diff --git a/crucible-syntax.cabal b/crucible-syntax.cabal
new file mode 100644
--- /dev/null
+++ b/crucible-syntax.cabal
@@ -0,0 +1,142 @@
+Cabal-version: 2.2
+Name:          crucible-syntax
+Version:       0.4.1
+Author:        Galois Inc.
+Maintainer:    dtc@galois.com
+Build-type:    Simple
+License:       BSD-3-Clause
+License-file:  LICENSE
+Category:      Language
+Synopsis:      A syntax for reading and writing Crucible control-flow graphs
+Description:
+  This package provides a syntax for directly constructing Crucible
+  control-flow graphs, as well as for observing them.
+
+extra-doc-files: README.txt, CHANGELOG.md
+extra-source-files:
+
+common shared
+  -- Specifying -Wall and -Werror can cause the project to fail to build on
+  -- newer versions of GHC simply due to new warnings being added to -Wall. To
+  -- prevent this from happening we manually list which warnings should be
+  -- considered errors. We also list some warnings that are not in -Wall, though
+  -- try to avoid "opinionated" warnings (though this judgement is clearly
+  -- subjective).
+  --
+  -- Warnings are grouped by the GHC version that introduced them, and then
+  -- alphabetically.
+  --
+  -- A list of warnings and the GHC version in which they were introduced is
+  -- available here:
+  -- https://ghc.gitlab.haskell.org/ghc/doc/users_guide/using-warnings.html
+
+  -- Since GHC 8.10 or earlier:
+  ghc-options:
+    -Wall
+    -Werror=compat-unqualified-imports
+    -Werror=deferred-type-errors
+    -Werror=deprecated-flags
+    -Werror=deprecations
+    -Werror=deriving-defaults
+    -Werror=dodgy-foreign-imports
+    -Werror=duplicate-exports
+    -Werror=empty-enumerations
+    -Werror=identities
+    -Werror=inaccessible-code
+    -Werror=incomplete-patterns
+    -Werror=incomplete-record-updates
+    -Werror=incomplete-uni-patterns
+    -Werror=inline-rule-shadowing
+    -Werror=missed-extra-shared-lib
+    -Werror=missing-exported-signatures
+    -Werror=missing-fields
+    -Werror=missing-home-modules
+    -Werror=missing-methods
+    -Werror=overflowed-literals
+    -Werror=overlapping-patterns
+    -Werror=partial-fields
+    -Werror=partial-type-signatures
+    -Werror=simplifiable-class-constraints
+    -Werror=star-binder
+    -Werror=star-is-type
+    -Werror=tabs
+    -Werror=typed-holes
+    -Werror=unrecognised-pragmas
+    -Werror=unrecognised-warning-flags
+    -Werror=unsupported-calling-conventions
+    -Werror=unsupported-llvm-version
+    -Werror=unticked-promoted-constructors
+    -Werror=unused-imports
+    -Werror=warnings-deprecations
+    -Werror=wrong-do-bind
+
+  if impl(ghc >= 9.2)
+    ghc-options:
+      -Werror=ambiguous-fields
+      -Werror=operator-whitespace
+      -Werror=operator-whitespace-ext-conflict
+      -Werror=redundant-bang-patterns
+
+  if impl(ghc >= 9.4)
+    ghc-options:
+      -Werror=forall-identifier
+      -Werror=misplaced-pragmas
+      -Werror=redundant-strictness-flags
+      -Werror=type-equality-out-of-scope
+      -Werror=type-equality-requires-operators
+
+  ghc-prof-options: -O2 -fprof-auto-top
+  default-language: Haskell2010
+
+library
+  default-language: Haskell2010
+
+  build-depends:
+    base >= 4.9 && < 4.20,
+    bv-sized >= 1.0.0,
+    containers,
+    crucible >= 0.1,
+    lens,
+    mtl,
+    parameterized-utils >= 0.1.7,
+    prettyprinter >= 1.7.0,
+    megaparsec >= 7.0 && < 9.7,
+    text,
+    transformers,
+    vector,
+    what4
+
+  hs-source-dirs: src
+
+  exposed-modules:
+    Lang.Crucible.Syntax.Atoms
+    Lang.Crucible.Syntax.Concrete
+    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
+  ghc-prof-options: -O2 -fprof-auto-top
+
+test-suite crucible-syntax-tests
+  import: shared
+  type: exitcode-stdio-1.0
+  main-is: Tests.hs
+  hs-source-dirs: test
+  build-depends:
+    base,
+    containers,
+    crucible,
+    crucible-syntax,
+    directory,
+    filepath,
+    megaparsec,
+    parameterized-utils,
+    tasty,
+    tasty-golden,
+    tasty-hunit,
+    text,
+    what4
+
diff --git a/src/Lang/Crucible/Syntax/Atoms.hs b/src/Lang/Crucible/Syntax/Atoms.hs
new file mode 100644
--- /dev/null
+++ b/src/Lang/Crucible/Syntax/Atoms.hs
@@ -0,0 +1,344 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedStrings#-}
+
+-- | Atoms used by the Crucible CFG concrete syntax.
+module Lang.Crucible.Syntax.Atoms
+  (
+    -- * The atom datatype
+    Atomic(..)
+  , atom
+    -- * Individual atoms
+  , AtomName(..)
+  , LabelName(..)
+  , RegName(..)
+  , FunName(..)
+  , GlobalName(..)
+  , Keyword(..)
+  ) where
+
+import Control.Applicative
+
+import Data.Char
+import Data.Functor
+import Data.Ratio
+import Data.Text (Text)
+import qualified Data.Text as T
+
+import Lang.Crucible.Syntax.SExpr
+import Numeric
+import qualified Prettyprinter as PP
+
+import Text.Megaparsec as MP hiding (many, some)
+import Text.Megaparsec.Char
+
+-- | The name of an atom (non-keyword identifier)
+newtype AtomName = AtomName Text deriving (Eq, Ord, PP.Pretty, Show)
+-- | The name of a label (identifier followed by colon)
+newtype LabelName = LabelName Text deriving (Eq, Ord, PP.Pretty, Show)
+-- | The name of a register (dollar sign followed by identifier)
+newtype RegName = RegName Text deriving (Eq, Ord, PP.Pretty, Show)
+-- | The name of a function (at-sign followed by identifier)
+newtype FunName = FunName Text deriving (Eq, Ord, PP.Pretty, Show)
+-- | The name of a global variable (two dollar signs followed by identifier)
+newtype GlobalName = GlobalName Text deriving (Eq, Ord, PP.Pretty, Show)
+
+-- | Individual language keywords (reserved identifiers)
+data Keyword = Defun | DefBlock | DefGlobal | Declare | Extern
+             | Registers
+             | Start
+             | SetGlobal
+             | SetRef | DropRef_
+             | Plus | Minus | Times | Div | Negate | Abs
+             | Just_ | Nothing_ | FromJust
+             | Inj | Proj
+             | AnyT | UnitT | BoolT | NatT | IntegerT | RealT | ComplexRealT | CharT | StringT
+             | BitvectorT | VectorT | SequenceT | FPT | FunT | MaybeT | VariantT | StructT | RefT
+             | Half_ | Float_ | Double_ | Quad_ | X86_80_ | DoubleDouble_
+             | Unicode_ | Char8_ | Char16_
+             | The
+             | Equalp | Integerp
+             | If
+             | Not_ | And_ | Or_ | Xor_
+             | Mod
+             | Lt | Le
+             | Show
+             | StringConcat_ | StringEmpty_ | StringLength_
+             | ToAny | FromAny
+             | VectorLit_ | VectorReplicate_ | VectorIsEmpty_ | VectorSize_
+             | VectorGetEntry_ | VectorSetEntry_ | VectorCons_
+             | MkStruct_ | GetField_ | SetField_
+             | SequenceNil_ | SequenceCons_ | SequenceAppend_
+             | SequenceIsNil_ | SequenceLength_
+             | SequenceHead_ | SequenceTail_ | SequenceUncons_
+             | Deref | Ref | EmptyRef
+             | Jump_ | Return_ | Branch_ | MaybeBranch_ | TailCall_ | Error_ | Output_ | Case
+             | Print_ | PrintLn_
+             | Let | Fresh
+             | Assert_ | Assume_
+             | SetRegister
+             | Funcall
+             | Breakpoint_
+             | BV | BVConcat_ | BVSelect_ | BVTrunc_
+             | BVZext_ | BVSext_ | BVNonzero_ | BoolToBV_
+             | BVCarry_ | BVSCarry_ | BVSBorrow_
+             | BVNot_ | BVAnd_ | BVOr_ | BVXor_ | BVShl_ | BVLshr_ | BVAshr_
+             | Sle | Slt | Sdiv | Smod | ZeroExt | SignExt
+             | RNE_ | RNA_ | RTP_ | RTN_ | RTZ_
+             | FPToUBV_ | FPToSBV_ | UBVToFP_ | SBVToFP_ | BinaryToFP_ | FPToBinary_
+             | FPToReal_ | RealToFP_
+  deriving (Eq, Ord)
+
+keywords :: [(Text, Keyword)]
+keywords =
+    -- function/block defintion
+  [ ("defun" , Defun)
+  , ("start" , Start)
+  , ("defblock", DefBlock)
+  , ("defglobal", DefGlobal)
+  , ("declare", Declare)
+  , ("extern", Extern)
+  , ("registers", Registers)
+
+    -- statements
+  , ("let", Let)
+  , ("set-global!", SetGlobal)
+  , ("set-ref!", SetRef)
+  , ("drop-ref!", DropRef_)
+  , ("fresh", Fresh)
+  , ("jump" , Jump_)
+  , ("case", Case)
+  , ("return" , Return_)
+  , ("branch" , Branch_)
+  , ("maybe-branch" , MaybeBranch_)
+  , ("tail-call" , TailCall_)
+  , ("error", Error_)
+  , ("output", Output_)
+  , ("print" , Print_)
+  , ("println" , PrintLn_)
+  , ("Ref", RefT)
+  , ("deref", Deref)
+  , ("ref", Ref)
+  , ("empty-ref", EmptyRef)
+  , ("set-register!", SetRegister)
+  , ("assert!", Assert_)
+  , ("assume!", Assume_)
+  , ("funcall", Funcall)
+  , ("breakpoint", Breakpoint_)
+
+    -- types
+  , ("Any" , AnyT)
+  , ("Unit" , UnitT)
+  , ("Bool" , BoolT)
+  , ("Nat" , NatT)
+  , ("Integer" , IntegerT)
+  , ("FP", FPT)
+  , ("Real" , RealT)
+  , ("ComplexReal" , ComplexRealT)
+  , ("Char" , CharT)
+  , ("String" , StringT)
+  , ("Bitvector" , BitvectorT)
+  , ("Vector", VectorT)
+  , ("Sequence", SequenceT)
+  , ("->", FunT)
+  , ("Maybe", MaybeT)
+  , ("Variant", VariantT)
+  , ("Struct", StructT)
+
+    -- string sorts
+  , ("Unicode", Unicode_)
+  , ("Char16", Char16_)
+  , ("Char8", Char8_)
+
+    -- floating-point variants
+  , ("Half", Half_)
+  , ("Float", Float_)
+  , ("Double", Double_)
+  , ("Quad", Quad_)
+  , ("X86_80", X86_80_)
+  , ("DoubleDouble", DoubleDouble_)
+
+    -- misc
+  , ("the" , The)
+  , ("equal?" , Equalp)
+  , ("if" , If)
+
+    -- ANY types
+  , ("to-any", ToAny)
+  , ("from-any", FromAny)
+
+    -- booleans
+  , ("not" , Not_)
+  , ("and" , And_)
+  , ("or" , Or_)
+  , ("xor" , Xor_)
+
+    -- arithmetic
+  , ("+" , Plus)
+  , ("-" , Minus)
+  , ("*" , Times)
+  , ("/" , Div)
+  , ("<" , Lt)
+  , ("<=" , Le)
+  , ("<=$" , Sle)
+  , ("<$" , Slt)
+  , ("/$" , Sdiv)
+  , ("smod", Smod)
+  , ("negate", Negate)
+  , ("abs", Abs)
+  , ("mod" , Mod)
+  , ("integer?" , Integerp)
+
+    -- Variants
+  , ("inj", Inj)
+  , ("proj", Proj)
+
+    -- Structs
+  , ("struct", MkStruct_)
+  , ("get-field", GetField_)
+  , ("set-field", SetField_)
+
+    -- Maybe
+  , ("just" , Just_)
+  , ("nothing" , Nothing_)
+  , ("from-just" , FromJust)
+
+    -- Vectors
+  , ("vector", VectorLit_)
+  , ("vector-replicate", VectorReplicate_)
+  , ("vector-empty?", VectorIsEmpty_)
+  , ("vector-size", VectorSize_)
+  , ("vector-get", VectorGetEntry_)
+  , ("vector-set", VectorSetEntry_)
+  , ("vector-cons", VectorCons_)
+
+    -- Sequences
+  , ("seq-nil", SequenceNil_)
+  , ("seq-cons", SequenceCons_)
+  , ("seq-append", SequenceAppend_)
+  , ("seq-nil?", SequenceIsNil_)
+  , ("seq-length", SequenceLength_)
+  , ("seq-head", SequenceHead_)
+  , ("seq-tail", SequenceTail_)
+  , ("seq-uncons", SequenceUncons_)
+
+    -- strings
+  , ("show", Show)
+  , ("string-concat", StringConcat_)
+  , ("string-empty", StringEmpty_)
+  , ("string-length", StringLength_)
+
+    -- bitvector
+  , ("bv", BV)
+  , ("bv-concat", BVConcat_)
+  , ("bv-select", BVSelect_)
+  , ("bv-trunc", BVTrunc_)
+  , ("zero-extend", BVZext_)
+  , ("sign-extend", BVSext_)
+  , ("bv-nonzero", BVNonzero_)
+  , ("bool-to-bv", BoolToBV_)
+  , ("bv-carry", BVCarry_)
+  , ("bv-scarry", BVSCarry_)
+  , ("bv-sborrow", BVSBorrow_)
+  , ("bv-not", BVNot_)
+  , ("bv-and", BVAnd_)
+  , ("bv-or", BVOr_)
+  , ("bv-xor", BVXor_)
+  , ("shl", BVShl_)
+  , ("lshr", BVLshr_)
+  , ("ashr", BVAshr_)
+
+    -- floating-point
+  , ("fp-to-ubv", FPToUBV_)
+  , ("fp-to-sbv", FPToSBV_)
+  , ("ubv-to-fp", UBVToFP_)
+  , ("sbv-to-fp", SBVToFP_)
+  , ("fp-to-binary", FPToBinary_)
+  , ("binary-to-fp", BinaryToFP_)
+  , ("real-to-fp", RealToFP_)
+  , ("fp-to-real", FPToReal_)
+  , ("rne" , RNE_)
+  , ("rna" , RNA_)
+  , ("rtp" , RTP_)
+  , ("rtn" , RTN_)
+  , ("rtz" , RTZ_)
+  ]
+
+instance Show Keyword where
+  show k = case [str | (str, k') <- keywords, k == k'] of
+             [] -> "UNKNOWN KW"
+             (s:_) -> T.unpack s
+
+
+-- | The atoms of the language
+data Atomic = Kw !Keyword -- ^ Keywords are all the built-in operators and expression formers
+            | Lbl !LabelName -- ^ Labels, but not the trailing colon
+            | At !AtomName -- ^ Atom names (which look like Scheme symbols)
+            | Rg !RegName -- ^ Registers, whose names have a leading single $
+            | Gl !GlobalName -- ^ Global variables, whose names have a leading double $$
+            | Fn !FunName -- ^ Function names, minus the leading @
+            | Int !Integer -- ^ Literal integers
+            | Rat !Rational -- ^ Literal rational numbers
+            | Bool !Bool   -- ^ Literal Booleans
+            | StrLit !Text -- ^ Literal strings
+  deriving (Eq, Ord, Show)
+
+
+instance IsAtom Atomic where
+  showAtom (Kw s) = T.pack (show s)
+  showAtom (Lbl (LabelName l)) = l <> ":"
+  showAtom (Rg (RegName r)) = "$" <> r
+  showAtom (Gl (GlobalName r)) = "$$" <> r
+  showAtom (At (AtomName a)) = a
+  showAtom (Fn (FunName a)) = "@" <> a
+  showAtom (Int i) = T.pack (show i)
+  showAtom (Rat r) = T.pack (show (numerator r) ++ "/" ++ show (denominator r))
+  showAtom (Bool b) = if b then "#t" else "#f"
+  showAtom (StrLit s) = T.pack $ show s
+
+-- | Parse an atom
+atom :: Parser Atomic
+atom =  try (Lbl . LabelName <$> identifier <* char ':')
+    <|> Fn . FunName <$> (char '@' *> identifier)
+    <|> (char '$' *> ((char '$' *> (Gl . GlobalName <$> identifier)) <|> Rg . RegName <$> identifier))
+    <|> try (mkNum <$> signedPrefixedNumber <*> ((Just <$> (try (char '/') *> prefixedNumber)) <|> pure Nothing))
+    <|> kwOrAtom
+    <|> char '#' *>  ((char 't' <|> char 'T') $> Bool True <|> (char 'f' <|> char 'F') $> Bool False)
+    <|> char '"' *> (StrLit . T.pack <$> stringContents)
+  where
+    mkNum x Nothing = Int x
+    mkNum x (Just y) = Rat (x % y)
+
+stringContents :: Parser [Char]
+stringContents =  (char '\\' *> ((:) <$> escapeChar <*> stringContents))
+              <|> (char '"' $> [])
+              <|> ((:) <$> satisfy (const True) <*> stringContents)
+
+escapeChar :: Parser Char
+escapeChar =  (char '\\' *> pure '\\')
+          <|> (char '"' *> pure '"')
+          <|> (char 'n' *> pure '\n')
+          <|> (char 't' *> pure '\t')
+          <?> "valid escape character"
+
+kwOrAtom :: Parser Atomic
+kwOrAtom = do x <- identifier
+              return $ maybe (At (AtomName x)) Kw (lookup x keywords)
+
+
+signedPrefixedNumber :: (Eq a, Num a) => Parser a
+signedPrefixedNumber =
+  char '+' *> prefixedNumber <|>
+  char '-' *> (negate <$> prefixedNumber) <|>
+  prefixedNumber
+
+prefixedNumber :: (Eq a, Num a) => Parser a
+prefixedNumber = try (char '0' *> maybehex) <|> decimal
+  where decimal = fromInteger . read <$> some (satisfy isDigit <?> "decimal digit")
+        maybehex = char 'x' *> hex <|> return 0
+        hex = reading $ readHex <$> some (satisfy (\c -> isDigit c || elem c ("abcdefABCDEF" :: String)) <?> "hex digit")
+        reading p =
+          p >>=
+            \case
+              [(x, "")] -> pure x
+              _ -> empty
diff --git a/src/Lang/Crucible/Syntax/Concrete.hs b/src/Lang/Crucible/Syntax/Concrete.hs
new file mode 100644
--- /dev/null
+++ b/src/Lang/Crucible/Syntax/Concrete.hs
@@ -0,0 +1,2280 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE LiberalTypeSynonyms #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PartialTypeSignatures #-}
+{-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ViewPatterns #-}
+
+module Lang.Crucible.Syntax.Concrete
+  ( -- * Errors
+    ExprErr(..)
+  -- * Parsing and Results
+  , ParserHooks(..)
+  , ParsedProgram(..)
+  , defaultParserHooks
+  , top
+  , cfgs
+  , prog
+  -- * Low level parsing operations
+  , SyntaxState(..)
+  , atomName
+  , freshAtom
+  , nat
+  , string
+  , isType
+  , operands
+  , BoundedNat(..)
+  , PosNat
+  , posNat
+  , someAssign
+  -- * Rules for pretty-printing language syntax
+  , printExpr
+  )
+where
+
+import Prelude hiding (fail)
+
+import Control.Lens hiding (cons, backwards)
+import Control.Applicative
+import Control.Monad (MonadPlus(..), forM, join)
+import Control.Monad.Error.Class (MonadError(..))
+import Control.Monad.Identity ()
+import Control.Monad.IO.Class (MonadIO(..))
+import Control.Monad.Reader (MonadReader, ReaderT(..))
+import Control.Monad.State.Strict (MonadState(..), StateT(..))
+import Control.Monad.Trans.Class (MonadTrans(..))
+import Control.Monad.Trans.Except (ExceptT(..))
+import Control.Monad.Writer.Strict (MonadWriter(..), WriterT(..))
+
+import Lang.Crucible.Types
+
+import qualified Data.BitVector.Sized as BV
+import Data.Foldable
+import Data.Functor
+import qualified Data.Functor.Product as Functor
+import Data.Kind (Type)
+import Data.Maybe
+import Data.Parameterized.Some(Some(..))
+import Data.Parameterized.Pair (Pair(..))
+import Data.Parameterized.TraversableFC
+import Data.Parameterized.Classes
+import Data.Parameterized.Nonce ( NonceGenerator, Nonce
+                                , freshNonce )
+import qualified Data.Parameterized.Context as Ctx
+import Data.Map (Map)
+import qualified Data.Map as Map
+import qualified Data.Sequence as Seq
+import Data.Text (Text)
+import qualified Data.Text as T
+import qualified Data.Vector as V
+import Numeric.Natural
+import qualified Prettyprinter as PP
+
+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
+import What4.Symbol
+import What4.Utils.StringLiteral
+
+import Lang.Crucible.Syntax.SExpr (Syntax, pattern L, pattern A, toText, PrintRules(..), PrintStyle(..), syntaxPos, withPosFrom, showAtom)
+import Lang.Crucible.Syntax.Atoms hiding (atom)
+
+import Lang.Crucible.CFG.Reg hiding (globalName)
+import Lang.Crucible.CFG.Expr
+
+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 =
+  liftIO (syntaxParseIO p ast) >>= \case
+    Left e -> throwError (SyntaxParseError e)
+    Right v -> return v
+
+type AST s = Syntax Atomic
+
+
+
+printExpr :: AST s -> Text
+printExpr = toText (PrintRules rules)
+  where rules (Kw Defun) = Just (Special 3)
+        rules (Kw DefBlock) = Just (Special 1)
+        rules (Kw Start) = Just (Special 1)
+        rules (Kw Registers) = Just (Special 0)
+        rules _ = Nothing
+
+data E ext s t where
+  EAtom  :: !(Atom s t) -> E ext s t
+  EReg   :: !Position -> !(Reg s t) -> E ext s t
+  EGlob  :: !Position -> !(GlobalVar t) -> E ext s t
+  EDeref :: !Position -> !(E ext s (ReferenceType t)) -> E ext s t
+  EApp   :: !(App ext (E ext s) t) -> E ext s t
+
+data SomeExpr ext s where
+  SomeE :: TypeRepr t -> E ext s t -> SomeExpr ext s
+  SomeOverloaded :: AST s -> Keyword -> [SomeExpr ext s] -> SomeExpr ext s
+  SomeIntLiteral :: AST s -> Integer -> SomeExpr ext s
+
+data SomeBVExpr ext s where
+  SomeBVExpr :: (1 <= w) => NatRepr w -> E ext s (BVType w) -> SomeBVExpr ext s
+
+data ExprErr s where
+  TrivialErr :: Position -> ExprErr s
+  Errs :: ExprErr s -> ExprErr s -> ExprErr s
+  DuplicateAtom :: Position -> AtomName -> ExprErr s
+  DuplicateLabel :: Position -> LabelName -> ExprErr s
+  EmptyBlock :: Position -> ExprErr s
+  NotGlobal :: Position -> AST s -> ExprErr s
+  InvalidRegister :: Position -> AST s -> ExprErr s
+  SyntaxParseError :: SP.SyntaxError Atomic -> ExprErr s
+
+deriving instance Show (ExprErr s)
+
+instance Semigroup (ExprErr s) where
+  (<>) = Errs
+
+instance Monoid (ExprErr s) where
+  mempty = TrivialErr (OtherPos "mempty")
+
+instance PP.Pretty (ExprErr s) where
+  pretty =
+    \case
+      TrivialErr p ->
+        "Trivial error at" PP.<+> PP.viaShow p
+      Errs e1 e2 ->
+        PP.vcat ["Multiple errors:" , PP.pretty e1 , PP.pretty e2]
+      DuplicateAtom p a ->
+        PP.hsep ["Duplicate atom", backticks (PP.pretty a), "at", PP.viaShow p]
+      DuplicateLabel p l ->
+        PP.hsep ["Duplicate label", backticks (PP.pretty l), "at", PP.viaShow p]
+      EmptyBlock p ->
+        "Empty block at" PP.<+> PP.viaShow p
+      NotGlobal p _ast ->
+        "Expected a global at" PP.<+> PP.viaShow p
+      InvalidRegister p _ast ->
+        "Expected a register at" PP.<+> PP.viaShow p
+      SyntaxParseError err ->
+        PP.pretty (printSyntaxError err)
+    where backticks = PP.enclose "`" "`"
+
+-- | ParserHooks enables support for arbitrary syntax extensions by allowing
+-- users to supply their own parsers for types and syntax extensions.
+data ParserHooks ext = ParserHooks {
+    -- | extensionTypeParser is called for all type specifications and enables
+    -- the addition of new types to crucible-syntax.
+    extensionTypeParser :: forall m. MonadSyntax Atomic m => m (Some TypeRepr)
+
+    -- | extensionParser is called when parsing statements and let bindings
+    -- (everywhere function calls are supported) and enables the addition of
+    -- syntax extensions to crucible-syntax.
+  , extensionParser
+    :: forall s m
+     . ( MonadSyntax Atomic m
+       , MonadWriter [Posd (Stmt ext s)] m
+       , MonadState (SyntaxState s) m
+       , MonadIO m
+       , IsSyntaxExtension ext
+       , ?parserHooks :: ParserHooks ext
+       -- ParserHooks instance to use recursively when parsing.
+       )
+    => m (Some (Atom s))
+    -- ^ The atom computed from evaluating the syntax extension.
+}
+
+-- | A ParserHooks instance that adds no extensions to the crucible-syntax
+-- language.
+defaultParserHooks :: ParserHooks ()
+defaultParserHooks = ParserHooks empty empty
+
+-- | The results of parsing a program.
+data ParsedProgram ext = ParsedProgram
+  { parsedProgGlobals :: Map GlobalName (Some GlobalVar)
+    -- ^ The parsed @defglobal@s.
+  , parsedProgExterns :: Map GlobalName (Some GlobalVar)
+    -- ^ For each parsed @extern@, map its name to its global variable. It is
+    --   the responsibility of the caller to insert each global variable into
+    --   the 'SymGlobalState' alongside an appropriate 'RegValue'.
+  , parsedProgCFGs :: [AnyCFG ext]
+    -- ^ The CFGs for each parsed @defun@.
+  , parsedProgForwardDecs :: Map FunctionName SomeHandle
+    -- ^ For each parsed @declare@, map its name to its function handle. It is
+    --   the responsibility of the caller to register each handle with an
+    --   appropriate 'FnState'.
+  }
+
+
+kw :: MonadSyntax Atomic m => Keyword -> m ()
+kw k = describe ("the keyword " <> showAtom (Kw k)) (atom (Kw k))
+
+int :: MonadSyntax Atomic m => m Integer
+int = sideCondition "integer literal" numeric atomic
+  where numeric (Int i) = Just i
+        numeric _ = Nothing
+
+nat :: MonadSyntax Atomic m => m Natural
+nat = sideCondition "natural literal" isNat atomic
+  where isNat (Int i) | i >= 0 = Just (fromInteger i)
+        isNat _ = Nothing
+
+labelName :: MonadSyntax Atomic m => m LabelName
+labelName = sideCondition "label name" lbl atomic
+  where lbl (Lbl l) = Just l
+        lbl _ = Nothing
+
+regName :: MonadSyntax Atomic m => m RegName
+regName = sideCondition "register name" reg atomic
+  where reg (Rg rn) = Just rn
+        reg _ = Nothing
+
+globalName :: MonadSyntax Atomic m => m GlobalName
+globalName = sideCondition "name of global variable" glob atomic
+  where glob (Gl x) = Just x
+        glob _ = Nothing
+
+
+rational :: MonadSyntax Atomic m => m Rational
+rational = sideCondition "rational number literal" numeric atomic
+  where numeric (Rat r) = Just r
+        numeric _ = Nothing
+
+
+string :: MonadSyntax Atomic m => m Text
+string = sideCondition "string literal" stringy atomic
+  where stringy (StrLit t) = Just t
+        stringy _ = Nothing
+
+atomName :: MonadSyntax Atomic m => m AtomName
+atomName = sideCondition "Crucible atom literal" isCAtom atomic
+  where isCAtom (At a) = Just a
+        isCAtom _ = Nothing
+
+roundingMode :: MonadSyntax Atomic m => m RoundingMode
+roundingMode = describe "rounding mode" $
+        asum [ kw RNE_ $> RNE
+             , kw RNA_ $> RNA
+             , kw RTP_ $> RTP
+             , kw RTN_ $> RTN
+             , kw RTZ_ $> RTZ
+             ]
+
+fpinfo :: MonadSyntax Atomic m => m (Some FloatInfoRepr)
+fpinfo = asum [ kw Half_         $> Some HalfFloatRepr
+              , kw Float_        $> Some SingleFloatRepr
+              , kw Double_       $> Some DoubleFloatRepr
+              , kw Quad_         $> Some QuadFloatRepr
+              , kw X86_80_       $> Some X86_80FloatRepr
+              , kw DoubleDouble_ $> Some DoubleDoubleFloatRepr
+              ]
+
+bool :: MonadSyntax Atomic m => m  Bool
+bool = sideCondition "Boolean literal" isBool atomic
+  where isBool (Bool b) = Just b
+        isBool _ = Nothing
+
+funName :: MonadSyntax Atomic m => m  FunctionName
+funName = functionNameFromText <$> sideCondition "function name literal" isFn atomic
+  where isFn (Fn (FunName n)) = Just n
+        isFn _ = Nothing
+
+toCtx :: forall f . [Some f] -> Some (Ctx.Assignment f)
+toCtx fs = toCtx' (reverse fs)
+  where toCtx' :: [Some f] -> Some (Ctx.Assignment f)
+        toCtx' [] = Some Ctx.empty
+        toCtx' (Some x : (toCtx' -> Some xs)) =
+          Some $ Ctx.extend xs x
+
+unary :: MonadSyntax Atomic m => Keyword -> m a -> m a
+unary k p = followedBy (kw k) (commit *> cons p emptyList) <&> fst
+
+binary :: MonadSyntax Atomic m => Keyword -> m a -> m b -> m (a, b)
+binary k p1 p2 = followedBy (kw k) (commit *> cons p1 (cons p2 emptyList)) <&> \(x, (y, ())) -> (x, y)
+
+
+mkFunRepr :: [Some TypeRepr] -> Some TypeRepr -> Some TypeRepr
+mkFunRepr (toCtx -> Some doms) (Some ran) = Some $ FunctionHandleRepr doms ran
+
+repUntilLast :: MonadSyntax Atomic m => m a -> m ([a], a)
+repUntilLast sp = describe "zero or more followed by one" $ repUntilLast' sp
+  where repUntilLast' p =
+          (cons p emptyList <&> \(x, ()) -> ([], x)) <|>
+          (cons p (repUntilLast' p) <&> \(x, (xs, lst)) -> (x:xs, lst))
+
+_isBaseType :: ( ?parserHooks :: ParserHooks ext, MonadSyntax Atomic m )
+            => m (Some BaseTypeRepr)
+_isBaseType =
+  describe "base type" $
+  do Some tp <- isType
+     case asBaseType tp of
+       NotBaseType -> empty
+       AsBaseType bt -> return (Some bt)
+
+_isFloatingType :: ( ?parserHooks :: ParserHooks ext, MonadSyntax Atomic m )
+                => m (Some FloatInfoRepr)
+_isFloatingType =
+  describe "floating-point type" $
+  do Some tp <- isType
+     case tp of
+       FloatRepr fi -> return (Some fi)
+       _ -> empty
+
+data BoundedNat bnd =
+  forall w. (bnd <= w) => BoundedNat (NatRepr w)
+
+type PosNat = BoundedNat 1
+
+posNat :: MonadSyntax Atomic m => m PosNat
+posNat =
+   do i <- sideCondition "positive nat literal" checkPosNat nat
+      maybe empty return $ do Some x <- return $ mkNatRepr i
+                              LeqProof <- isPosNat x
+                              return $ BoundedNat x
+  where checkPosNat i | i > 0 = Just i
+        checkPosNat _ = Nothing
+
+natRepr :: MonadSyntax Atomic m => m (Some NatRepr)
+natRepr = mkNatRepr <$> nat
+
+stringSort :: MonadSyntax Atomic m => m (Some StringInfoRepr)
+stringSort =
+  later $ describe "string sort" $
+    asum [ kw Unicode_ $> Some UnicodeRepr
+         , kw Char16_  $> Some Char16Repr
+         , kw Char8_   $> Some Char8Repr
+         ]
+
+isType :: ( ?parserHooks :: ParserHooks ext, MonadSyntax Atomic m )
+       => m (Some TypeRepr)
+isType =
+  describe "type" $ call
+    (atomicType <|> stringT <|> vector <|> seqt <|> ref <|> bv <|> fp <|> fun <|> maybeT <|> var <|> struct <|> (extensionTypeParser ?parserHooks))
+
+  where
+    atomicType =
+      later $ describe "atomic type" $
+        asum [ kw AnyT         $> Some AnyRepr
+             , kw UnitT        $> Some UnitRepr
+             , kw BoolT        $> Some BoolRepr
+             , kw NatT         $> Some NatRepr
+             , kw IntegerT     $> Some IntegerRepr
+             , kw RealT        $> Some RealValRepr
+             , kw ComplexRealT $> Some ComplexRealRepr
+             , kw CharT        $> Some CharRepr
+             ]
+    vector = unary VectorT isType <&> \(Some t) -> Some (VectorRepr t)
+    seqt   = unary SequenceT isType <&> \(Some t) -> Some (SequenceRepr t)
+    ref    = unary RefT isType <&> \(Some t) -> Some (ReferenceRepr t)
+    bv :: MonadSyntax Atomic m => m  (Some TypeRepr)
+    bv     = do BoundedNat len <- unary BitvectorT posNat
+                return $ Some $ BVRepr len
+
+    fp :: MonadSyntax Atomic m => m (Some TypeRepr)
+    fp = do Some fpi <- unary FPT fpinfo
+            return $ Some $ FloatRepr fpi
+
+    fun :: MonadSyntax Atomic m => m (Some TypeRepr)
+    fun = cons (kw FunT) (repUntilLast isType) <&> \((), (args, ret)) -> mkFunRepr args ret
+
+    stringT :: MonadSyntax Atomic m => m (Some TypeRepr)
+    stringT = unary StringT stringSort <&> \(Some si) -> Some (StringRepr si)
+
+    maybeT = unary MaybeT isType <&> \(Some t) -> Some (MaybeRepr t)
+
+    var :: MonadSyntax Atomic m => m (Some TypeRepr)
+    var = cons (kw VariantT) (rep isType) <&> \((), toCtx -> Some tys) -> Some (VariantRepr tys)
+
+    struct ::  MonadSyntax Atomic m => m (Some TypeRepr)
+    struct = cons (kw StructT) (rep isType) <&> \((), toCtx -> Some tys) -> Some (StructRepr tys)
+
+someExprType :: SomeExpr ext s -> Maybe (Some TypeRepr)
+someExprType (SomeE tpr _) = Just (Some tpr)
+someExprType _ = Nothing
+
+
+findJointType :: Maybe (Some TypeRepr) -> [SomeExpr ext s] -> Maybe (Some TypeRepr)
+findJointType = foldr (\y x -> f x (someExprType y))
+ where
+ f Nothing y    = y
+ f x@(Just _) _ = x
+
+evalOverloaded :: forall m s t ext. MonadSyntax Atomic m => AST s -> TypeRepr t -> Keyword -> [SomeExpr ext s] -> m (E ext s t)
+evalOverloaded ast tpr k = withFocus ast .
+  case (k, tpr) of
+    (Plus, NatRepr)     -> nary NatAdd    (NatLit 0)
+    (Plus, IntegerRepr) -> nary IntAdd    (IntLit 0)
+    (Plus, RealValRepr) -> nary RealAdd   (RationalLit 0)
+    (Plus, BVRepr w)    -> nary (BVAdd w) (BVLit w (BV.zero w))
+
+    (Times, NatRepr)     -> nary NatMul    (NatLit 1)
+    (Times, IntegerRepr) -> nary IntMul    (IntLit 1)
+    (Times, RealValRepr) -> nary RealMul   (RationalLit 1)
+    (Times, BVRepr w)    -> nary (BVMul w) (BVLit w (BV.one w))
+
+    (Minus, NatRepr)     -> bin NatSub
+    (Minus, IntegerRepr) -> bin IntSub
+    (Minus, RealValRepr) -> bin RealSub
+    (Minus, BVRepr w)    -> bin (BVSub w)
+
+    (Div, NatRepr)       -> bin NatDiv
+    (Div, IntegerRepr)   -> bin IntDiv
+    (Div, RealValRepr)   -> bin RealDiv
+    (Div, BVRepr w)      -> bin (BVUdiv w)
+
+    (Mod, NatRepr)       -> bin NatMod
+    (Mod, IntegerRepr)   -> bin IntMod
+    (Mod, RealValRepr)   -> bin RealMod
+    (Mod, BVRepr w)      -> bin (BVUrem w)
+
+    (Negate, IntegerRepr) -> u IntNeg
+    (Negate, RealValRepr) -> u RealNeg
+    (Negate, BVRepr w)    -> u (BVNeg w)
+
+    (Abs, IntegerRepr)   -> u IntAbs
+
+    _ -> \_ -> later $ describe ("operation at type " <> T.pack (show tpr)) $ empty
+ where
+ u :: (E ext s t -> App ext (E ext s) t) -> [SomeExpr ext s] -> m (E ext s t)
+ u f [x] = EApp . f <$> evalSomeExpr tpr x
+ u _ _ = later $ describe "one argument" $ empty
+
+ bin :: (E ext s t -> E ext s t -> App ext (E ext s) t) -> [SomeExpr ext s] -> m (E ext s t)
+ bin f [x,y] = EApp <$> (f <$> evalSomeExpr tpr x <*> evalSomeExpr tpr y)
+ bin _ _ = later $ describe "two arguments" $ empty
+
+ nary :: (E ext s t -> E ext s t -> App ext (E ext s) t) -> App ext (E ext s) t -> [SomeExpr ext s] -> m (E ext s t)
+ nary _ z []     = return $ EApp z
+ nary _ _ [x]    = evalSomeExpr tpr x
+ nary f _ (x:xs) = go f <$> evalSomeExpr tpr x <*> mapM (evalSomeExpr tpr) xs
+
+ go f x (y:ys) = go f (EApp $ f x y) ys
+ go _ x []     = x
+
+
+evalSomeExpr :: MonadSyntax Atomic m => TypeRepr t -> SomeExpr ext s -> m (E ext s t)
+evalSomeExpr tpr (SomeE tpr' e)
+  | Just Refl <- testEquality tpr tpr' = return e
+  | otherwise = later $ describe ("matching types (" <> T.pack (show tpr)
+                                  <> " /= " <> T.pack (show tpr') <> ")") empty
+evalSomeExpr tpr (SomeOverloaded ast k args) = evalOverloaded ast tpr k args
+evalSomeExpr tpr (SomeIntLiteral ast i) = evalIntLiteral ast tpr i
+
+applyOverloaded ::
+  MonadSyntax Atomic m => AST s -> Keyword -> Maybe (Some TypeRepr) -> [SomeExpr ext s] -> m (SomeExpr ext s)
+applyOverloaded ast k mtp args =
+  case findJointType mtp args of
+    Nothing -> return $ SomeOverloaded ast k args
+    Just (Some tp) -> SomeE tp <$> evalOverloaded ast tp k args
+
+evalIntLiteral :: MonadSyntax Atomic m => AST s -> TypeRepr tpr -> Integer -> m (E ext s tpr)
+evalIntLiteral _ NatRepr i | i >= 0 = return $ EApp $ NatLit (fromInteger i)
+evalIntLiteral _ IntegerRepr i = return $ EApp $ IntLit i
+evalIntLiteral _ RealValRepr i = return $ EApp $ RationalLit (fromInteger i)
+evalIntLiteral ast tpr _i =
+  withFocus ast $ later $ describe ("literal " <> T.pack (show tpr) <> " value") empty
+
+forceSynth :: MonadSyntax Atomic m => SomeExpr ext s -> m (Pair TypeRepr (E ext s))
+forceSynth (SomeE tp e) = return $ Pair tp e
+forceSynth (SomeOverloaded ast _ _) =
+  withFocus ast $ later (describe "unambiguous expression (add type annotation to disambiguate)" empty)
+forceSynth (SomeIntLiteral ast _) =
+  withFocus ast $ later (describe "unambiguous numeric literal (add type annotation to disambiguate)" empty)
+
+synth
+  :: forall m s ext
+   . ( MonadReader (SyntaxState s) m
+     , MonadSyntax Atomic m
+     , ?parserHooks :: ParserHooks ext )
+  => m (Pair TypeRepr (E ext s))
+synth = forceSynth =<< synth'
+
+synth' :: forall m s ext
+        .  ( MonadReader (SyntaxState s) m
+           , MonadSyntax Atomic m
+           , ?parserHooks :: ParserHooks ext )
+       => m (SomeExpr ext s)
+synth' = synthExpr Nothing
+
+synthExpr :: forall m s ext
+           . ( MonadReader (SyntaxState s) m
+             , MonadSyntax Atomic m
+             , ?parserHooks :: ParserHooks ext )
+          => Maybe (Some TypeRepr)
+          -> m (SomeExpr ext s)
+synthExpr typeHint =
+  describe "expression" $
+    call (the <|> crucibleAtom <|> regRef <|> globRef <|> deref <|>
+     bvExpr <|>
+     naryBool And_ And True <|> naryBool Or_ Or False <|> naryBool Xor_ BoolXor False <|>
+     unaryArith Negate <|> unaryArith Abs <|>
+     naryArith Plus <|> binaryArith Minus <|> naryArith Times <|> binaryArith Div <|> binaryArith Mod <|>
+     unitCon <|> boolLit <|> stringLit <|> funNameLit <|>
+     notExpr <|> equalp <|> lessThan <|> lessThanEq <|>
+     toAny <|> fromAny <|> stringAppend <|> stringEmpty <|> stringLength <|> showExpr <|>
+     just <|> nothing <|> fromJust_ <|> injection <|> projection <|>
+     vecLit <|> vecCons <|> vecRep <|> vecLen <|> vecEmptyP <|> vecGet <|> vecSet <|>
+     struct <|> getField <|> setField <|>
+     seqNil <|> seqCons <|> seqAppend <|> seqNilP <|> seqLen <|>
+     seqHead <|> seqTail <|> seqUncons <|>
+     ite <|>  intLit <|> rationalLit <|> intp <|>
+     binaryToFp <|> fpToBinary <|> realToFp <|> fpToReal <|>
+     ubvToFloat <|> floatToUBV <|> sbvToFloat <|> floatToSBV <|>
+     unaryBV BVNonzero_ BVNonzero <|> compareBV BVCarry_ BVCarry <|>
+     compareBV BVSCarry_ BVSCarry <|> compareBV BVSBorrow_ BVSBorrow <|>
+     compareBV Slt BVSlt <|> compareBV Sle BVSle)
+
+-- Syntactic constructs still to add (see issue #74)
+
+-- BvToInteger, SbvToInteger, BvToNat
+-- NatToInteger, IntegerToReal
+-- RealRound, RealFloor, RealCeil
+-- IntegerToBV, RealToNat
+
+-- EmptyWordMap, InsertWordMap, LookupWordMap, LookupWordMapWithDefault
+-- EmptyStringMap, LookupStringMapEntry, InsertStringMapEntry
+-- SymArrayLookup, SymArrayUpdate
+-- Complex, RealPart, ImagPart
+-- IsConcrete
+-- Closure
+-- All the floating-point operations
+-- What to do about RollRecursive, UnrollRecursive?
+-- AddSideCondition????
+-- BVUndef ????
+
+  where
+    the :: m (SomeExpr ext s)
+    the = do describe "type-annotated expression" $
+               kw The `followedBy`
+                 (depCons isType $
+                  \(Some t) ->
+                    do (e, ()) <- cons (check t) emptyList
+                       return $ SomeE t e)
+
+    okAtom theAtoms x =
+      case Map.lookup x theAtoms of
+        Nothing -> Nothing
+        Just (Some anAtom) -> Just $ SomeE (typeOfAtom anAtom) (EAtom anAtom)
+
+    regRef :: m (SomeExpr ext s)
+    regRef =
+      do Some r <- regRef'
+         loc <- position
+         return (SomeE (typeOfReg r) (EReg loc r))
+
+    deref :: m (SomeExpr ext s)
+    deref =
+      do let newhint = case typeHint of
+                         Just (Some t) -> Just (Some (ReferenceRepr t))
+                         _ -> Nothing
+         unary Deref (forceSynth =<< synthExpr newhint) >>= \case
+           Pair (ReferenceRepr t') e ->
+             do loc <- position
+                return (SomeE t' (EDeref loc e))
+           Pair notRef _ -> later $ describe ("reference type (provided a "<> T.pack (show notRef) <>")") empty
+
+    globRef :: m (SomeExpr ext s)
+    globRef =
+      do Some g <- globRef'
+         loc <- position
+         return (SomeE (globalType g) (EGlob loc g))
+
+    crucibleAtom :: m (SomeExpr ext s)
+    crucibleAtom =
+      do theAtoms <- view stxAtoms
+         sideCondition "known atom" (okAtom theAtoms) atomName
+
+    unitCon = describe "unit constructor" (emptyList $> SomeE UnitRepr (EApp EmptyApp))
+
+    boolLit = bool <&> SomeE BoolRepr . EApp . BoolLit
+
+    stringLit = string <&> SomeE (StringRepr UnicodeRepr) . EApp . StringLit . UnicodeLiteral
+
+    intLit =
+      do ast <- anything
+         case typeHint of
+           Just (Some tpr) -> SomeE tpr <$> (evalIntLiteral ast tpr =<< int)
+           Nothing         -> SomeIntLiteral ast <$> int
+
+    rationalLit = rational <&> SomeE RealValRepr . EApp . RationalLit
+
+    naryBool k f u =
+      do ((), args) <- cons (kw k) (rep (check BoolRepr))
+         case args of
+           [] -> return $ SomeE BoolRepr $ EApp (BoolLit u)
+           (x:xs) -> go x xs
+
+      where
+      go x [] = return $ SomeE BoolRepr x
+      go x (y:ys) = go (EApp $ f x y) ys
+
+    bvExpr :: m (SomeExpr ext s)
+    bvExpr =
+      do let nathint = case typeHint of Just (Some (BVRepr w)) -> NatHint w; _ -> NoHint
+         SomeBVExpr w x <- synthBV nathint
+         return $ SomeE (BVRepr w) x
+
+    intp =
+      do e <- unary Integerp (check RealValRepr)
+         return $ SomeE BoolRepr $ EApp $ RealIsInteger e
+
+    funNameLit =
+      do fn <- funName
+         fh <- view $ stxFunctions . at fn
+         dh <- view $ stxForwardDecs . at fn
+         describe "known function name" $
+           -- First look for a function with the given name, and failing that,
+           -- look for a forward declaration with the given name.
+           case fh <|> dh of
+             Nothing -> empty
+             Just (FunctionHeader _ funArgs ret handle _) ->
+               return $ SomeE (FunctionHandleRepr (argTypes funArgs) ret) (EApp $ HandleLit handle)
+
+    notExpr =
+      do e <- describe "negation expression" $ unary Not_ (check BoolRepr)
+         return $ SomeE BoolRepr $ EApp $ Not e
+
+    matchingExprs ::
+      Maybe (Some TypeRepr) -> SomeExpr ext s -> SomeExpr ext s ->
+      (forall tp. TypeRepr tp -> E ext s tp -> E ext s tp -> m a) ->
+      m a
+    matchingExprs h e1 e2 k =
+      case findJointType h [e1,e2] of
+        Just (Some tp) ->
+          do e1' <- evalSomeExpr tp e1
+             e2' <- evalSomeExpr tp e2
+             k tp e1' e2'
+        Nothing ->
+          later $ describe ("type annotation required to disambiguate types") empty
+
+    equalp :: m (SomeExpr ext s)
+    equalp =
+      do (e1, e2) <- describe "equality test" $ binary Equalp synth' synth'
+         matchingExprs Nothing e1 e2 $ \tp e1' e2' ->
+          case tp of
+            FloatRepr _fi ->
+              return $ SomeE BoolRepr $ EApp $ FloatEq e1' e2'
+            ReferenceRepr rtp ->
+              return $ SomeE BoolRepr $ EApp $ ReferenceEq rtp e1' e2'
+            NatRepr ->
+              return $ SomeE BoolRepr $ EApp $ NatEq e1' e2'
+            (asBaseType -> AsBaseType bt) ->
+              return $ SomeE BoolRepr $ EApp $ BaseIsEq bt e1' e2'
+            _ ->
+              later $ describe ("a base type or floating point type or reference type (got " <> T.pack (show tp) <> ")") empty
+
+    compareBV ::
+      Keyword ->
+      (forall w. (1 <= w) => NatRepr w -> E ext s (BVType w) -> E ext s (BVType w) -> App ext (E ext s) BoolType) ->
+      m (SomeExpr ext s)
+    compareBV k f =
+      do (e1, e2) <- describe "bitvector compaprison" $ binary k synth' synth'
+         matchingExprs Nothing e1 e2 $ \tp e1' e2' ->
+           case tp of
+             BVRepr w ->
+               return $ SomeE BoolRepr $ EApp $ f w e1' e2'
+             _ ->
+               later $ describe ("a bitvector type (got " <> T.pack (show tp) <> ")") empty
+
+    lessThan :: m (SomeExpr ext s)
+    lessThan =
+      do (e1, e2) <- describe "less-than test" $ binary Lt synth' synth'
+         matchingExprs Nothing e1 e2 $ \tp e1' e2' ->
+           case tp of
+             NatRepr     -> return $ SomeE BoolRepr $ EApp $ NatLt e1' e2'
+             IntegerRepr -> return $ SomeE BoolRepr $ EApp $ IntLt e1' e2'
+             RealValRepr -> return $ SomeE BoolRepr $ EApp $ RealLt e1' e2'
+             BVRepr w    -> return $ SomeE BoolRepr $ EApp $ BVUlt w e1' e2'
+             other ->
+               describe ("valid comparison type (got " <> T.pack (show other) <> ")") empty
+
+    lessThanEq :: m (SomeExpr ext s)
+    lessThanEq =
+      do (e1, e2) <- describe "less-than-or-equal test" $ binary Le synth' synth'
+         matchingExprs Nothing e1 e2 $ \tp e1' e2' ->
+           case tp of
+             NatRepr     -> return $ SomeE BoolRepr $ EApp $ NatLe e1' e2'
+             IntegerRepr -> return $ SomeE BoolRepr $ EApp $ IntLe e1' e2'
+             RealValRepr -> return $ SomeE BoolRepr $ EApp $ RealLe e1' e2'
+             BVRepr w    -> return $ SomeE BoolRepr $ EApp $ BVUle w e1' e2'
+             other ->
+               describe ("valid comparison type (got " <> T.pack (show other) <> ")") empty
+
+    naryArith :: Keyword -> m (SomeExpr ext s)
+    naryArith k =
+      do ast <- anything
+         args <- followedBy (kw k) (commit *> (rep (synthExpr typeHint)))
+         applyOverloaded ast k typeHint args
+
+    binaryArith :: Keyword -> m (SomeExpr ext s)
+    binaryArith k =
+      do ast <- anything
+         (x, y) <- binary k (synthExpr typeHint) (synthExpr typeHint)
+         applyOverloaded ast k typeHint [x,y]
+
+    unaryArith :: Keyword -> m (SomeExpr ext s)
+    unaryArith k =
+      do ast <- anything
+         x <- unary k (synthExpr typeHint)
+         applyOverloaded ast k typeHint [x]
+
+    unaryBV ::
+      Keyword ->
+      (forall w. (1 <= w) => NatRepr w -> E ext s (BVType w) -> App ext (E ext s) BoolType) ->
+      m (SomeExpr ext s)
+    unaryBV k f =
+      do Pair t x <- unary k synth
+         case t of
+           BVRepr w ->return $ SomeE BoolRepr $ EApp $ f w x
+           _ -> later $ describe "bitvector argument" empty
+
+    just :: m (SomeExpr ext s)
+    just =
+      do let newhint = case typeHint of
+                         Just (Some (MaybeRepr t)) -> Just (Some t)
+                         _ -> Nothing
+         Pair t x <- unary Just_ (forceSynth =<< synthExpr newhint)
+         return $ SomeE (MaybeRepr t) $ EApp $ JustValue t x
+
+    nothing :: m (SomeExpr ext s)
+    nothing =
+      do Some t <- unary Nothing_ isType
+         return $ SomeE (MaybeRepr t) $ EApp $ NothingValue t
+      <|>
+      kw Nothing_ *>
+      case typeHint of
+        Just (Some (MaybeRepr t)) ->
+          return $ SomeE (MaybeRepr t) $ EApp $ NothingValue t
+        Just (Some t) ->
+          later $ describe ("value of type " <> T.pack (show t)) empty
+        Nothing ->
+          later $ describe ("unambiguous nothing value") empty
+
+    fromJust_ :: m (SomeExpr ext s)
+    fromJust_ =
+      do let newhint = case typeHint of
+                         Just (Some t) -> Just (Some (MaybeRepr t))
+                         _ -> Nothing
+         describe "coercion from Maybe (fromJust-expression)" $
+           followedBy (kw FromJust) $
+           depCons (forceSynth =<< synthExpr newhint) $ \(Pair t e) ->
+             case t of
+               MaybeRepr elemT ->
+                 depCons (check (StringRepr UnicodeRepr)) $ \str ->
+                   do emptyList
+                      return $ SomeE elemT $ EApp $ FromJustValue elemT e str
+               _ -> later $ describe "maybe expression" nothing
+
+    projection :: m (SomeExpr ext s)
+    projection =
+      do (n, Pair t e) <- describe "projection from variant type" $ binary Proj int synth
+         case t of
+           VariantRepr ts ->
+             case Ctx.intIndex (fromInteger n) (Ctx.size ts) of
+               Nothing ->
+                 describe (T.pack (show n) <> " is an invalid index into " <> T.pack (show ts)) empty
+               Just (Some idx) ->
+                 do let ty = MaybeRepr (ts^.ixF' idx)
+                    return $ SomeE ty $ EApp $ ProjectVariant ts idx e
+           _ -> describe ("variant type (got " <> T.pack (show t) <> ")") empty
+
+    injection :: m (SomeExpr ext s)
+    injection =
+      do (n, e) <- describe "injection into variant type" $ binary Inj int anything
+         case typeHint of
+           Just (Some (VariantRepr ts)) ->
+             case Ctx.intIndex (fromInteger n) (Ctx.size ts) of
+               Nothing ->
+                 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 First $
+                             parse e (check ty)
+                    return $ SomeE (VariantRepr ts) $ EApp $ InjectVariant ts idx out
+           Just (Some t) ->
+             describe ("context expecting variant type (got " <> T.pack (show t) <> ")") empty
+           Nothing ->
+             describe ("unambiguous variant") empty
+
+    fpToBinary :: m (SomeExpr ext s)
+    fpToBinary =
+       kw FPToBinary_ `followedBy`
+       (depConsCond synth $ \(Pair tp x) ->
+         case tp of
+           FloatRepr fpi
+             | BaseBVRepr w <- floatInfoToBVTypeRepr fpi
+             , Just LeqProof <- isPosNat w ->
+                 emptyList $> (Right $ SomeE (BVRepr w) $ EApp $ FloatToBinary fpi x)
+           _ -> pure $ Left $ "floating-point value")
+
+    binaryToFp :: m (SomeExpr ext s)
+    binaryToFp =
+       kw BinaryToFP_ `followedBy`
+       (depCons fpinfo $ \(Some fpi) ->
+        depCons (check (baseToType (floatInfoToBVTypeRepr fpi))) $ \x ->
+        emptyList $> (SomeE (FloatRepr fpi) $ EApp $ FloatFromBinary fpi x))
+
+    fpToReal :: m (SomeExpr ext s)
+    fpToReal =
+       kw FPToReal_ `followedBy`
+       (depConsCond synth $ \(Pair tp x) ->
+         case tp of
+           FloatRepr _fpi -> emptyList $> (Right $ SomeE RealValRepr $ EApp $ FloatToReal x)
+           _ -> pure $ Left "floating-point value")
+
+    realToFp :: m (SomeExpr ext s)
+    realToFp =
+       kw RealToFP_ `followedBy`
+       (depCons fpinfo $ \(Some fpi) ->
+        depCons roundingMode $ \rm ->
+        depCons (check RealValRepr) $ \x ->
+        emptyList $> (SomeE (FloatRepr fpi) $ EApp $ FloatFromReal fpi rm x))
+
+    ubvToFloat :: m (SomeExpr ext s)
+    ubvToFloat =
+       kw UBVToFP_ `followedBy`
+       (depCons fpinfo $ \(Some fpi) ->
+        depCons roundingMode $ \rm ->
+        depConsCond synth $ \(Pair tp x) ->
+          case tp of
+            BVRepr _w ->
+              emptyList $> (Right $ SomeE (FloatRepr fpi) $ EApp $ FloatFromBV fpi rm x)
+            _ -> pure $ Left $ "bitvector value"
+        )
+
+    sbvToFloat :: m (SomeExpr ext s)
+    sbvToFloat =
+       kw SBVToFP_ `followedBy`
+       (depCons fpinfo $ \(Some fpi) ->
+        depCons roundingMode $ \rm ->
+        depConsCond synth $ \(Pair tp x) ->
+          case tp of
+            BVRepr _w ->
+              emptyList $> (Right $ SomeE (FloatRepr fpi) $ EApp $ FloatFromSBV fpi rm x)
+            _ -> pure $ Left $ "bitvector value"
+       )
+
+    floatToUBV :: m (SomeExpr ext s)
+    floatToUBV =
+       kw FPToUBV_ `followedBy`
+       (depCons posNat $ \(BoundedNat w) ->
+        depCons roundingMode $ \rm ->
+        depConsCond synth $ \(Pair tp x) ->
+          case tp of
+            FloatRepr _fpi ->
+              emptyList $> (Right $ SomeE (BVRepr w) $ EApp $ FloatToBV w rm x)
+            _ -> pure $ Left $ "floating-point value")
+
+    floatToSBV :: m (SomeExpr ext s)
+    floatToSBV =
+       kw FPToSBV_ `followedBy`
+       (depCons posNat $ \(BoundedNat w) ->
+        depCons roundingMode $ \rm ->
+        depConsCond synth $ \(Pair tp x) ->
+          case tp of
+            FloatRepr _fpi ->
+              emptyList $> (Right $ SomeE (BVRepr w) $ EApp $ FloatToSBV w rm x)
+            _ -> pure $ Left $ "floating-point value")
+
+    ite :: m (SomeExpr ext s)
+    ite =
+      do (c, (et, (ef, ()))) <-
+           followedBy (kw If) $
+           cons (check BoolRepr) $
+           cons (synthExpr typeHint) $
+           cons (synthExpr typeHint) $
+           emptyList
+         matchingExprs typeHint et ef $ \tp t f ->
+          case tp of
+            FloatRepr fi ->
+               return $ SomeE tp $ EApp $ FloatIte fi c t f
+            NatRepr ->
+               return $ SomeE tp $ EApp $ NatIte c t f
+            (asBaseType -> AsBaseType bty) ->
+               return $ SomeE tp $ EApp $ BaseIte bty c t f
+            _ ->
+               let msg = T.concat [ "conditional where branches have base or floating point type, but got "
+                                  , T.pack (show tp)
+                                  ]
+               in later $ describe msg empty
+
+    toAny =
+      do Pair tp e <- unary ToAny synth
+         return $ SomeE AnyRepr (EApp (PackAny tp e))
+    fromAny =
+      (binary FromAny isType (check AnyRepr)) <&>
+        \(Some ty, e) -> SomeE (MaybeRepr ty) (EApp (UnpackAny ty e))
+
+    stringLength :: m (SomeExpr ext s)
+    stringLength =
+      do unary StringLength_
+           (do (Pair ty e) <- forceSynth =<< synthExpr Nothing
+               case ty of
+                 StringRepr _si -> return $ SomeE IntegerRepr $ EApp (StringLength e)
+                 _ -> later $ describe "string expression" empty)
+
+    stringEmpty =
+      unary StringEmpty_ stringSort <&> \(Some si) -> SomeE (StringRepr si) $ EApp $ StringEmpty si
+
+    stringAppend :: m (SomeExpr ext s)
+    stringAppend =
+      do (e1,(e2,())) <-
+           followedBy (kw StringConcat_) $
+           cons (synthExpr typeHint) $
+           cons (synthExpr typeHint) $
+           emptyList
+         matchingExprs typeHint e1 e2 $ \tp s1 s2 ->
+           case tp of
+             StringRepr si -> return $ SomeE (StringRepr si) $ EApp $ StringConcat si s1 s2
+             _ -> later $ describe "string expressions" empty
+
+    vecRep :: m (SomeExpr ext s)
+    vecRep =
+      do let newhint = case typeHint of
+                         Just (Some (VectorRepr t)) -> Just (Some t)
+                         _ -> Nothing
+         (n, Pair t e) <-
+           binary VectorReplicate_ (check NatRepr) (forceSynth =<< synthExpr newhint)
+         return $ SomeE (VectorRepr t) $ EApp $ VectorReplicate t n e
+
+    vecLen :: m (SomeExpr ext s)
+    vecLen =
+      do Pair t e <- unary VectorSize_ synth
+         case t of
+           VectorRepr _ -> return $ SomeE NatRepr $ EApp $ VectorSize e
+           other -> later $ describe ("vector (found " <> T.pack (show other) <> ")") empty
+
+    vecEmptyP :: m (SomeExpr ext s)
+    vecEmptyP =
+      do Pair t e <- unary VectorIsEmpty_ synth
+         case t of
+           VectorRepr _ -> return $ SomeE BoolRepr $ EApp $ VectorIsEmpty e
+           other -> later $ describe ("vector (found " <> T.pack (show other) <> ")") empty
+
+    vecLit :: m (SomeExpr ext s)
+    vecLit =
+      let newhint = case typeHint of
+                       Just (Some (VectorRepr t)) -> Just (Some t)
+                       _ -> Nothing
+       in describe "vector literal" $
+          do ((),ls) <- cons (kw VectorLit_) (commit *> rep (synthExpr newhint))
+             case findJointType newhint ls of
+               Nothing -> later $ describe "unambiguous vector literal (add a type ascription to disambiguate)" empty
+               Just (Some t) ->
+                 SomeE (VectorRepr t) . EApp . VectorLit t . V.fromList
+                   <$> mapM (evalSomeExpr t) ls
+
+    vecCons :: m (SomeExpr ext s)
+    vecCons =
+      do let newhint = case typeHint of
+                         Just (Some (VectorRepr t)) -> Just (Some t)
+                         _ -> Nothing
+         (a, d) <- binary VectorCons_ (later (synthExpr newhint)) (later (synthExpr typeHint))
+         let g Nothing = Nothing
+             g (Just (Some t)) = Just (Some (VectorRepr t))
+         case join (find isJust [ typeHint, g (someExprType a), someExprType d ]) of
+           Just (Some (VectorRepr t)) ->
+             SomeE (VectorRepr t) . EApp <$> (VectorCons t <$> evalSomeExpr t a <*> evalSomeExpr (VectorRepr t) d)
+           _ -> later $ describe "unambiguous vector cons (add a type ascription to disambiguate)" empty
+
+    vecGet :: m (SomeExpr ext s)
+    vecGet =
+      do let newhint = case typeHint of
+                         Just (Some t) -> Just (Some (VectorRepr t))
+                         _ -> Nothing
+         (Pair t e, n) <-
+            binary VectorGetEntry_ (forceSynth =<< synthExpr newhint) (check NatRepr)
+         case t of
+           VectorRepr elemT -> return $ SomeE elemT $ EApp $ VectorGetEntry elemT e n
+           other -> later $ describe ("vector (found " <> T.pack (show other) <> ")") empty
+
+    vecSet :: m (SomeExpr ext s)
+    vecSet =
+      do (kw VectorSetEntry_) `followedBy` (
+           depCons (forceSynth =<< synthExpr typeHint) $
+            \ (Pair t vec) ->
+              case t of
+                VectorRepr elemT ->
+                  do (n, (elt, ())) <- cons (check NatRepr) $
+                                       cons (check elemT) $
+                                       emptyList
+                     return $ SomeE (VectorRepr elemT) $ EApp $ VectorSetEntry elemT vec n elt
+                _ -> later $ describe "argument with vector type" empty)
+
+    struct :: m (SomeExpr ext s)
+    struct = describe "struct literal" $ followedBy (kw MkStruct_) (commit *>
+      do ls <- case typeHint of
+                  Just (Some (StructRepr ctx)) ->
+                     list (toListFC (\t -> forceSynth =<< synthExpr (Just (Some t))) ctx)
+                  Just (Some t) -> later $ describe ("value of type " <> T.pack (show t) <> " but got struct") empty
+                  Nothing -> rep (forceSynth =<< synthExpr Nothing)
+         pure $! buildStruct ls)
+
+    getField :: m (SomeExpr ext s)
+    getField =
+      describe "struct field projection" $
+      followedBy (kw GetField_) (commit *>
+      depCons int (\n ->
+      depCons synth (\(Pair t e) ->
+         case t of
+           StructRepr ts ->
+             case Ctx.intIndex (fromInteger n) (Ctx.size ts) of
+               Nothing ->
+                 describe (T.pack (show n) <> " is an invalid index into " <> T.pack (show ts)) empty
+               Just (Some idx) ->
+                 do let ty = ts^.ixF' idx
+                    return $ SomeE ty $ EApp $ GetStruct e idx ty
+           _ -> describe ("struct type (got " <> T.pack (show t) <> ")") empty)))
+
+    setField :: m (SomeExpr ext s)
+    setField = describe "update to a struct type" $
+      followedBy (kw SetField_) (commit *>
+      depConsCond (forceSynth =<< synthExpr typeHint) (\ (Pair tp e) ->
+        case tp of
+          StructRepr ts -> Right <$>
+            depConsCond int (\n ->
+              case Ctx.intIndex (fromInteger n) (Ctx.size ts) of
+                Nothing -> pure (Left (T.pack (show n) <> " is an invalid index into " <> T.pack (show ts)))
+                Just (Some idx) -> Right <$>
+                  do let ty = ts^.ixF' idx
+                     (v,()) <- cons (check ty) emptyList
+                     pure $ SomeE (StructRepr ts) $ EApp $ SetStruct ts e idx v)
+          _ -> pure $ Left $ ("struct type, but got " <> T.pack (show tp))))
+
+    seqNil :: m (SomeExpr ext s)
+    seqNil =
+      do Some t <- unary SequenceNil_ isType
+         return $ SomeE (SequenceRepr t) $ EApp $ SequenceNil t
+      <|>
+      kw SequenceNil_ *>
+      case typeHint of
+        Just (Some (SequenceRepr t)) ->
+          return $ SomeE (SequenceRepr t) $ EApp $ SequenceNil t
+        Just (Some t) ->
+          later $ describe ("value of type " <> T.pack (show t)) empty
+        Nothing ->
+          later $ describe ("unambiguous nil value") empty
+
+    seqCons :: m (SomeExpr ext s)
+    seqCons =
+      do let newhint = case typeHint of
+                         Just (Some (SequenceRepr t)) -> Just (Some t)
+                         _ -> Nothing
+         (a, d) <- binary SequenceCons_ (later (synthExpr newhint)) (later (synthExpr typeHint))
+         let g Nothing = Nothing
+             g (Just (Some t)) = Just (Some (SequenceRepr t))
+         case join (find isJust [ typeHint, g (someExprType a), someExprType d ]) of
+           Just (Some (SequenceRepr t)) ->
+             SomeE (SequenceRepr t) . EApp <$> (SequenceCons t <$> evalSomeExpr t a <*> evalSomeExpr (SequenceRepr t) d)
+           _ -> later $ describe "unambiguous sequence cons (add a type ascription to disambiguate)" empty
+
+    seqAppend :: m (SomeExpr ext s)
+    seqAppend =
+      do (x, y) <- binary SequenceAppend_ (later (synthExpr typeHint)) (later (synthExpr typeHint))
+         case join (find isJust [ typeHint, someExprType x, someExprType y ]) of
+           Just (Some (SequenceRepr t)) ->
+             SomeE (SequenceRepr t) . EApp <$>
+               (SequenceAppend t <$> evalSomeExpr (SequenceRepr t) x <*> evalSomeExpr (SequenceRepr t) y)
+           _ -> later $ describe "unambiguous sequence append (add a type ascription to disambiguate)" empty
+
+    seqNilP :: m (SomeExpr ext s)
+    seqNilP =
+      do Pair t e <- unary SequenceIsNil_ synth
+         case t of
+           SequenceRepr t' -> return $ SomeE BoolRepr $ EApp $ SequenceIsNil t' e
+           other -> later $ describe ("sequence (found " <> T.pack (show other) <> ")") empty
+
+    seqLen :: m (SomeExpr ext s)
+    seqLen =
+      do Pair t e <- unary SequenceLength_ synth
+         case t of
+           SequenceRepr t' -> return $ SomeE NatRepr $ EApp $ SequenceLength t' e
+           other -> later $ describe ("sequence (found " <> T.pack (show other) <> ")") empty
+
+    seqHead :: m (SomeExpr ext s)
+    seqHead =
+      do let newhint = case typeHint of
+                         Just (Some (MaybeRepr t)) -> Just (Some (SequenceRepr t))
+                         _ -> Nothing
+         (Pair t e) <-
+            unary SequenceHead_ (forceSynth =<< synthExpr newhint)
+         case t of
+           SequenceRepr elemT -> return $ SomeE (MaybeRepr elemT) $ EApp $ SequenceHead elemT e
+           other -> later $ describe ("sequence (found " <> T.pack (show other) <> ")") empty
+
+    seqTail :: m (SomeExpr ext s)
+    seqTail =
+      do let newhint = case typeHint of
+                         Just (Some (MaybeRepr t)) -> Just (Some t)
+                         _ -> Nothing
+         (Pair t e) <-
+            unary SequenceTail_ (forceSynth =<< synthExpr newhint)
+         case t of
+           SequenceRepr elemT -> return $ SomeE (MaybeRepr (SequenceRepr elemT)) $ EApp $ SequenceTail elemT e
+           other -> later $ describe ("sequence (found " <> T.pack (show other) <> ")") empty
+
+    seqUncons :: m (SomeExpr ext s)
+    seqUncons =
+      do let newhint = case typeHint of
+                         Just (Some (MaybeRepr (StructRepr (Ctx.Empty Ctx.:> t Ctx.:> _)))) ->
+                           Just (Some (SequenceRepr t))
+                         _ -> Nothing
+         (Pair t e) <-
+            unary SequenceUncons_ (forceSynth =<< synthExpr newhint)
+         case t of
+           SequenceRepr elemT ->
+             return $ SomeE (MaybeRepr (StructRepr (Ctx.Empty Ctx.:> elemT Ctx.:> SequenceRepr elemT))) $
+               EApp $ SequenceUncons elemT e
+           other -> later $ describe ("sequence (found " <> T.pack (show other) <> ")") empty
+
+    showExpr :: m (SomeExpr ext s)
+    showExpr =
+      do Pair t1 e <- unary Show synth
+         case t1 of
+           FloatRepr fi ->
+             return $ SomeE (StringRepr UnicodeRepr) $ EApp $ ShowFloat fi e
+           NatRepr ->
+             let toint = EApp $ NatToInteger e
+                 showint = EApp $ ShowValue BaseIntegerRepr toint
+             in return $ SomeE (StringRepr UnicodeRepr) showint
+           (asBaseType -> AsBaseType bt) ->
+             return $ SomeE (StringRepr UnicodeRepr) $ EApp $ ShowValue bt e
+           _ -> later $ describe ("base or floating point type, but got " <> T.pack (show t1)) empty
+
+
+buildStruct :: [Pair TypeRepr (E ext s)] -> SomeExpr ext s
+buildStruct = loop Ctx.Empty Ctx.Empty
+  where
+    loop :: Ctx.Assignment TypeRepr ctx -> Ctx.Assignment (E ext s) ctx -> [Pair TypeRepr (E ext s)] -> SomeExpr ext s
+    loop tps vs [] = SomeE (StructRepr tps) (EApp (MkStruct tps vs))
+    loop tps vs (Pair tp x:xs) = loop (tps Ctx.:> tp) (vs Ctx.:> x) xs
+
+data NatHint
+  = NoHint
+  | forall w. (1 <= w) => NatHint (NatRepr w)
+
+synthBV :: forall m s ext.
+  ( MonadReader (SyntaxState s) m
+  , MonadSyntax Atomic m
+  , ?parserHooks :: ParserHooks ext ) =>
+  NatHint ->
+  m (SomeBVExpr ext s)
+synthBV widthHint =
+   bvLit <|> bvConcat <|> bvSelect <|> bvTrunc <|>
+   bvZext <|> bvSext <|> boolToBV <|>
+   naryBV BVAnd_ BVAnd 1 <|> naryBV BVOr_ BVOr 0 <|> naryBV BVXor_ BVXor 0 <|>
+   binaryBV Sdiv BVSdiv <|> binaryBV Smod BVSrem <|>
+   binaryBV BVShl_ BVShl <|> binaryBV BVLshr_ BVLshr <|> binaryBV BVAshr_ BVAshr <|>
+   unaryBV Negate BVNeg <|> unaryBV BVNot_ BVNot
+
+ where
+    bvSubterm :: NatHint -> m (SomeBVExpr ext s)
+    bvSubterm hint =
+      do let newhint = case hint of
+                         NatHint w -> Just (Some (BVRepr w))
+                         _ -> Nothing
+         (Pair t x) <- forceSynth =<< synthExpr newhint
+         case t of
+           BVRepr w -> return (SomeBVExpr w x)
+           _ -> later $ describe "bitvector expression" $ empty
+
+    bvLit :: m (SomeBVExpr ext s)
+    bvLit =
+      describe "bitvector literal" $
+      do (BoundedNat w, i) <- binary BV posNat int
+         return $ SomeBVExpr w $ EApp $ BVLit w (BV.mkBV w i)
+
+    unaryBV :: Keyword
+          -> (forall w. (1 <= w) => NatRepr w -> E ext s (BVType w) -> App ext (E ext s) (BVType w))
+          -> m (SomeBVExpr ext s)
+    unaryBV k f =
+      do SomeBVExpr wx x <- unary k (bvSubterm widthHint)
+         return $ SomeBVExpr wx $ EApp $ f wx x
+
+    binaryBV :: Keyword
+          -> (forall w. (1 <= w) => NatRepr w -> E ext s (BVType w) -> E ext s (BVType w) -> App ext (E ext s) (BVType w))
+          -> m (SomeBVExpr ext s)
+    binaryBV k f =
+      do (SomeBVExpr wx x, SomeBVExpr wy y) <- binary k (bvSubterm widthHint) (bvSubterm widthHint)
+         case testEquality wx wy of
+           Just Refl -> return $ SomeBVExpr wx $ EApp $ f wx x y
+           Nothing -> later $
+             describe ("bitwise expression arguments with matching widths (" <>
+                       T.pack (show wx) <> " /= " <> T.pack (show wy) <> ")")
+                      empty
+
+    naryBV :: Keyword
+          -> (forall w. (1 <= w) => NatRepr w -> E ext s (BVType w) -> E ext s (BVType w) -> App ext (E ext s) (BVType w))
+          -> Integer
+          -> m (SomeBVExpr ext s)
+    naryBV k f u =
+      do args <- kw k `followedBy` rep (later (bvSubterm widthHint))
+         case args of
+           [] -> case widthHint of
+                   NoHint    -> later $ describe "ambiguous width" empty
+                   NatHint w -> return $ SomeBVExpr w $ EApp $ BVLit w (BV.mkBV w u)
+           (SomeBVExpr wx x:xs) -> SomeBVExpr wx <$> go wx x xs
+
+     where
+     go :: forall w. NatRepr w -> E ext s (BVType w) -> [SomeBVExpr ext s] -> m (E ext s (BVType w))
+     go _wx x [] = return x
+     go wx x (SomeBVExpr wy y : ys) =
+       case testEquality wx wy of
+         Just Refl -> go wx (EApp $ f wx x y) ys
+         Nothing   -> later $
+              describe ("bitwise expression arguments with matching widths (" <>
+                        T.pack (show wx) <> " /= " <> T.pack (show wy) <> ")")
+                       empty
+
+    boolToBV :: m (SomeBVExpr ext s)
+    boolToBV =
+      do (BoundedNat w, x) <- binary BoolToBV_ posNat (check BoolRepr)
+         return $ SomeBVExpr w $ EApp $ BoolToBV w x
+
+    bvSelect :: m (SomeBVExpr ext s)
+    bvSelect =
+      do (Some idx, (BoundedNat len, (SomeBVExpr w x, ()))) <-
+             followedBy (kw BVSelect_) (commit *> cons natRepr (cons posNat (cons (bvSubterm NoHint) emptyList)))
+         case testLeq (addNat idx len) w of
+           Just LeqProof -> return $ SomeBVExpr len $ EApp $ BVSelect idx len w x
+           _ -> later $ describe ("valid bitvector select") $ empty
+
+    bvConcat :: m (SomeBVExpr ext s)
+    bvConcat =
+      do (SomeBVExpr wx x, SomeBVExpr wy y) <- binary BVConcat_ (bvSubterm NoHint) (bvSubterm NoHint)
+         withLeqProof (leqAdd (leqProof (knownNat @1) wx) wy) $
+           return $ SomeBVExpr (addNat wx wy) (EApp $ BVConcat wx wy x y)
+
+    bvTrunc :: m (SomeBVExpr ext s)
+    bvTrunc =
+      do (BoundedNat r, SomeBVExpr w x) <- binary BVTrunc_ posNat (bvSubterm NoHint)
+         case testLeq (incNat r) w of
+           Just LeqProof -> return $ SomeBVExpr r (EApp $ BVTrunc r w x)
+           _ -> later $ describe "valid bitvector truncation" $ empty
+
+    bvZext :: m (SomeBVExpr ext s)
+    bvZext =
+      do (BoundedNat r, SomeBVExpr w x) <- binary BVZext_ posNat (bvSubterm NoHint)
+         case testLeq (incNat w) r of
+           Just LeqProof -> return $ SomeBVExpr r (EApp $ BVZext r w x)
+           _ -> later $ describe "valid zero extension" $ empty
+
+    bvSext :: m (SomeBVExpr ext s)
+    bvSext =
+      do (BoundedNat r, SomeBVExpr w x) <- binary BVSext_ posNat (bvSubterm NoHint)
+         case testLeq (incNat w) r of
+           Just LeqProof -> return $ SomeBVExpr r (EApp $ BVSext r w x)
+           _ -> later $ describe "valid zero extension" $ empty
+
+
+check :: forall m t s ext
+       . ( MonadReader (SyntaxState s) m
+         , MonadSyntax Atomic m
+         , ?parserHooks :: ParserHooks ext )
+       => TypeRepr t -> m (E ext s t)
+check t =
+  describe ("inhabitant of " <> T.pack (show t)) $
+    do Pair t' e <- forceSynth =<< synthExpr (Just (Some t))
+       later $ describe ("a " <> T.pack (show t) <> " rather than a " <> T.pack (show t')) $
+         case testEquality t t' of
+           Nothing -> later empty
+           Just Refl -> return e
+
+-------------------------------------------------------------------------
+
+data LabelInfo :: Type -> Type where
+  NoArgLbl :: Label s -> LabelInfo s
+  ArgLbl :: forall s ty . LambdaLabel s ty -> LabelInfo s
+
+data ProgramState s =
+  ProgramState { _progFunctions :: Map FunctionName FunctionHeader
+               , _progForwardDecs :: Map FunctionName FunctionHeader
+               , _progGlobals :: Map GlobalName (Some GlobalVar)
+               , _progExterns :: Map GlobalName (Some GlobalVar)
+               , _progHandleAlloc :: HandleAllocator
+               }
+
+progFunctions :: Simple Lens (ProgramState s) (Map FunctionName FunctionHeader)
+progFunctions = lens _progFunctions (\s v -> s { _progFunctions = v })
+
+progForwardDecs :: Simple Lens (ProgramState s) (Map FunctionName FunctionHeader)
+progForwardDecs = lens _progForwardDecs (\s v -> s { _progForwardDecs = v })
+
+progGlobals :: Simple Lens (ProgramState s) (Map GlobalName (Some GlobalVar))
+progGlobals = lens _progGlobals (\s v -> s { _progGlobals = v })
+
+progExterns :: Simple Lens (ProgramState s) (Map GlobalName (Some GlobalVar))
+progExterns = lens _progExterns (\s v -> s { _progExterns = v })
+
+progHandleAlloc :: Simple Lens (ProgramState s) HandleAllocator
+progHandleAlloc = lens _progHandleAlloc (\s v -> s { _progHandleAlloc = v })
+
+
+data SyntaxState s =
+  SyntaxState { _stxLabels :: Map LabelName (LabelInfo s)
+              , _stxAtoms :: Map AtomName (Some (Atom s))
+              , _stxRegisters :: Map RegName (Some (Reg s))
+              , _stxNonceGen :: NonceGenerator IO s
+              , _stxProgState :: ProgramState s
+              }
+
+initProgState :: [(SomeHandle,Position)] -> HandleAllocator -> ProgramState s
+initProgState builtIns ha = ProgramState fns Map.empty Map.empty Map.empty ha
+  where
+  f tps = Ctx.generate
+            (Ctx.size tps)
+            (\i -> Arg (AtomName ("arg" <> (T.pack (show i)))) InternalPos (tps Ctx.! i))
+  fns = Map.fromList
+        [ (handleName h,
+            FunctionHeader
+              (handleName h)
+              (f (handleArgTypes h))
+              (handleReturnType h)
+              h
+              p
+           )
+        | (SomeHandle h,p) <- builtIns
+        ]
+
+initSyntaxState :: NonceGenerator IO s -> ProgramState s -> SyntaxState s
+initSyntaxState =
+  SyntaxState Map.empty Map.empty Map.empty
+
+stxLabels :: Simple Lens (SyntaxState s) (Map LabelName (LabelInfo s))
+stxLabels = lens _stxLabels (\s v -> s { _stxLabels = v })
+
+stxAtoms :: Simple Lens (SyntaxState s) (Map AtomName (Some (Atom s)))
+stxAtoms = lens _stxAtoms (\s v -> s { _stxAtoms = v })
+
+stxRegisters :: Simple Lens (SyntaxState s) (Map RegName (Some (Reg s)))
+stxRegisters = lens _stxRegisters (\s v -> s { _stxRegisters = v })
+
+stxNonceGen :: Getter (SyntaxState s) (NonceGenerator IO s)
+stxNonceGen = to _stxNonceGen
+
+stxProgState :: Simple Lens (SyntaxState s) (ProgramState s)
+stxProgState = lens _stxProgState (\s v -> s { _stxProgState = v })
+
+stxFunctions :: Simple Lens (SyntaxState s) (Map FunctionName FunctionHeader)
+stxFunctions = stxProgState . progFunctions
+
+stxForwardDecs :: Simple Lens (SyntaxState s) (Map FunctionName FunctionHeader)
+stxForwardDecs = stxProgState . progForwardDecs
+
+stxGlobals :: Simple Lens (SyntaxState s) (Map GlobalName (Some GlobalVar))
+stxGlobals = stxProgState . progGlobals
+
+stxExterns :: Simple Lens (SyntaxState s) (Map GlobalName (Some GlobalVar))
+stxExterns = stxProgState . progExterns
+
+newtype CFGParser s ret a =
+  CFGParser { runCFGParser :: (?returnType :: TypeRepr ret)
+                           => ExceptT (ExprErr s)
+                                (StateT (SyntaxState s) IO)
+                                a
+            }
+  deriving (Functor)
+
+instance Applicative (CFGParser s ret) where
+  pure x = CFGParser (pure x)
+  (CFGParser f) <*> (CFGParser x) = CFGParser (f <*> x)
+
+instance Alternative (CFGParser s ret) where
+  empty = CFGParser $ throwError $ TrivialErr InternalPos
+  (CFGParser x) <|> (CFGParser y) = CFGParser (x <|> y)
+
+instance Semigroup (CFGParser s ret a) where
+  (<>) = (<|>)
+
+instance Monoid (CFGParser s ret a) where
+  mempty = empty
+
+instance Monad (CFGParser s ret) where
+  (CFGParser m) >>= f = CFGParser $ m >>= \a -> runCFGParser (f a)
+
+instance MonadError (ExprErr s) (CFGParser s ret) where
+  throwError e = CFGParser $ throwError e
+  catchError m h = CFGParser $ catchError (runCFGParser m) (\e -> runCFGParser $ h e)
+
+instance MonadState (SyntaxState s) (CFGParser s ret) where
+  get = CFGParser get
+  put s = CFGParser $ put s
+
+instance MonadIO (CFGParser s ret) where
+  liftIO io = CFGParser $ lift $ lift io
+
+
+freshId :: (MonadState (SyntaxState s) m, MonadIO m) => m (Nonce s tp)
+freshId =
+  do ng <- use stxNonceGen
+     liftIO $ freshNonce ng
+
+freshLabel :: (MonadState (SyntaxState s) m, MonadIO m) => m (Label s)
+freshLabel = Label <$> freshId
+
+freshAtom :: ( MonadWriter [Posd (Stmt ext s)] m
+             , MonadState (SyntaxState s) m
+             , MonadIO m
+             , IsSyntaxExtension ext )
+          => Position -> AtomValue ext s t -> m (Atom s t)
+freshAtom loc v =
+  do i <- freshId
+     let theAtom = Atom { atomPosition = OtherPos "Parser internals"
+                        , atomId = i
+                        , atomSource = Assigned
+                        , typeOfAtom = typeOfAtomValue v
+                        }
+         stmt = DefineAtom theAtom v
+     tell [Posd loc stmt]
+     pure theAtom
+
+
+
+newLabel :: (MonadState (SyntaxState s) m, MonadIO m) => LabelName -> m (Label s)
+newLabel x =
+  do theLbl <- freshLabel
+     stxLabels %= Map.insert x (NoArgLbl theLbl)
+     return theLbl
+
+freshLambdaLabel :: (MonadState (SyntaxState s) m, MonadIO m) => TypeRepr tp -> m (LambdaLabel s tp, Atom s tp)
+freshLambdaLabel t =
+  do n <- freshId
+     i <- freshId
+     let lbl = LambdaLabel n a
+         a   = Atom { atomPosition = OtherPos "Parser internals"
+                    , atomId = i
+                    , atomSource = LambdaArg lbl
+                    , typeOfAtom = t
+                    }
+     return (lbl, a)
+
+with :: MonadState s m => Lens' s a -> (a -> m b) -> m b
+with l act = do x <- use l; act x
+
+
+lambdaLabelBinding :: ( MonadSyntax Atomic m
+                      , MonadState (SyntaxState s) m
+                      , MonadIO m
+                      , ?parserHooks :: ParserHooks ext )
+                   => m (LabelName, Some (LambdaLabel s))
+lambdaLabelBinding =
+  call $
+  depCons uniqueLabel $
+  \l ->
+    depCons uniqueAtom $
+    \x ->
+      depCons isType $
+      \(Some t) ->
+        do (lbl, anAtom) <- freshLambdaLabel t
+           stxLabels %= Map.insert l (ArgLbl lbl)
+           stxAtoms %= Map.insert x (Some anAtom)
+           return (l, Some lbl)
+
+  where uniqueLabel =
+          do labels <- use stxLabels
+             sideCondition "unique label"
+               (\l -> case Map.lookup l labels of
+                        Nothing -> Just l
+                        Just _ -> Nothing)
+               labelName
+
+
+uniqueAtom :: (MonadSyntax Atomic m, MonadState (SyntaxState s) m) => m AtomName
+uniqueAtom =
+  do atoms <- use stxAtoms
+     sideCondition "unique Crucible atom"
+       (\x -> case Map.lookup x atoms of
+                Nothing -> Just x
+                Just _ -> Nothing)
+       atomName
+
+newUnassignedReg :: (MonadState (SyntaxState s) m, MonadIO m) => TypeRepr t -> m (Reg s t)
+newUnassignedReg t =
+  do i <- freshId
+     let fakePos = OtherPos "Parser internals"
+     return $! Reg { regPosition = fakePos
+                   , regId = i
+                   , typeOfReg = t
+                   }
+
+regRef' :: (MonadSyntax Atomic m, MonadReader (SyntaxState s) m) => m (Some (Reg s))
+regRef' =
+  describe "known register name" $
+  do rn <- regName
+     perhapsReg <- view (stxRegisters . at rn)
+     case perhapsReg of
+       Just reg -> return reg
+       Nothing -> empty
+
+globRef' :: (MonadSyntax Atomic m, MonadReader (SyntaxState s) m) => m (Some GlobalVar)
+globRef' =
+  describe "known global variable name" $
+  do x <- globalName
+     perhapsGlobal <- view (stxGlobals . at x)
+     perhapsExtern <- view (stxExterns . at x)
+     case perhapsGlobal <|> perhapsExtern of
+       Just glob -> return glob
+       Nothing -> empty
+
+
+
+reading :: MonadState r m => ReaderT r m b -> m b
+reading m = get >>= runReaderT m
+
+--------------------------------------------------------------------------
+
+atomSetter :: forall m ext s
+            . ( MonadSyntax Atomic m
+              , MonadWriter [Posd (Stmt ext s)] m
+              , MonadState (SyntaxState s) m
+              , MonadIO m
+              , IsSyntaxExtension ext
+              , ?parserHooks :: ParserHooks ext )
+           => AtomName -- ^ The name of the atom being set, used for fresh name internals
+           -> m (Some (Atom s))
+atomSetter (AtomName anText) =
+  call ( newref
+     <|> emptyref
+     <|> fresh
+     <|> funcall
+     <|> evaluated
+     <|> (extensionParser ?parserHooks) )
+  where
+    fresh, emptyref, newref
+      :: ( MonadSyntax Atomic m
+         , MonadWriter [Posd (Stmt ext s)] m
+         , MonadState (SyntaxState s) m
+         , MonadIO m
+         , IsSyntaxExtension ext
+         )
+      => m (Some (Atom s))
+
+    newref =
+      do Pair _ e <- reading $ unary Ref synth
+         loc <- position
+         anAtom <- eval loc e
+         anotherAtom <- freshAtom loc (NewRef anAtom)
+         return $ Some anotherAtom
+
+    emptyref =
+      do Some t' <- reading $ unary EmptyRef isType
+         loc <- position
+         anAtom <- freshAtom loc (NewEmptyRef t')
+         return $ Some anAtom
+
+    fresh =
+      do t <- reading (unary Fresh isType)
+         -- Note that we are using safeSymbol below to create a What4 symbol
+         -- name, which will Z-encode names that aren't legal solver names. This
+         -- includes names that include hyphens, which are very common in
+         -- S-expression syntax. This is fine to do, since the Z-encoded name
+         -- name is only used for solver purposes; the original, unencoded name
+         -- is recorded separately.
+         let nm = safeSymbol (T.unpack anText)
+         loc <- position
+         case t of
+           Some (FloatRepr fi) ->
+             Some <$>
+               freshAtom loc (FreshFloat fi (Just nm))
+           Some NatRepr ->
+             Some <$> freshAtom loc (FreshNat (Just nm))
+           Some tp
+             | AsBaseType bt <- asBaseType tp ->
+                 Some <$> freshAtom loc (FreshConstant bt (Just nm))
+             | otherwise -> describe "atomic type" $ empty
+
+    evaluated =
+       do Pair _ e' <- reading synth
+          loc <- position
+          anAtom <- eval loc e'
+          return $ Some anAtom
+
+-- | Parse a list of operands (for example, the arguments to a function)
+operands :: forall s ext m tps
+          . ( MonadState (SyntaxState s) m
+            , MonadWriter [Posd (Stmt ext s)] m
+            , MonadIO m
+            , MonadSyntax Atomic m
+            , IsSyntaxExtension ext
+            , ?parserHooks :: ParserHooks ext )
+            -- ParserHooks to use for syntax extensions
+         => Ctx.Assignment TypeRepr tps
+         -- ^ Types of the operands
+         -> m (Ctx.Assignment (Atom s) tps)
+         -- ^ Atoms for the operands
+operands args = do
+  operandExprs <- backwards $ go $ Ctx.viewAssign args
+  traverseFC (\(Rand a ex) -> eval (syntaxPos a) ex) operandExprs
+  where
+    go :: (MonadState (SyntaxState s) m, MonadSyntax Atomic m)
+       => Ctx.AssignView TypeRepr args
+       -> m (Ctx.Assignment (Rand ext s) args)
+    go Ctx.AssignEmpty = emptyList *> pure Ctx.empty
+    go (Ctx.AssignExtend ctx' ty) =
+      depCons (reading $ check ty) $ \e ->
+        do rest <- go (Ctx.viewAssign ctx')
+           this <- anything
+           return $ Ctx.extend rest $ Rand this e
+
+funcall
+  :: forall ext s m
+   . ( MonadSyntax Atomic m
+     , MonadWriter [Posd (Stmt ext s)] m
+     , MonadState (SyntaxState s) m
+     , MonadIO m
+     , IsSyntaxExtension ext
+     , ?parserHooks :: ParserHooks ext
+     )
+  => m (Some (Atom s))
+funcall =
+  followedBy (kw Funcall) $
+  depConsCond (reading synth) $
+    \x ->
+      case x of
+        (Pair (FunctionHandleRepr funArgs ret) fun) ->
+          do loc <- position
+             funAtom <- eval loc fun
+             operandAtoms <- operands funArgs
+             endAtom <- freshAtom loc $ Call funAtom operandAtoms ret
+             return $ Right $ Some endAtom
+        _ -> return $ Left "a function"
+
+
+located :: MonadSyntax atom m => m a -> m (Posd a)
+located p = Posd <$> position <*> p
+
+normStmt' :: forall s m ext
+           . ( MonadWriter [Posd (Stmt ext s)] m
+             , MonadSyntax Atomic m
+             , MonadState (SyntaxState s) m
+             , MonadIO m
+             , IsSyntaxExtension ext
+             , ?parserHooks :: ParserHooks ext) =>
+             m ()
+normStmt' =
+  call (printStmt <|> printLnStmt <|> letStmt <|> (void funcall) <|>
+        setGlobal <|> setReg <|> setRef <|> dropRef <|>
+        assertion <|> assumption <|> breakpoint <|>
+        (void (extensionParser ?parserHooks)))
+
+  where
+    printStmt, printLnStmt, letStmt, setGlobal, setReg, setRef, dropRef, assertion, breakpoint :: m ()
+    printStmt =
+      do Posd loc e <- unary Print_ (located $ reading $ check (StringRepr UnicodeRepr))
+         strAtom <- eval loc e
+         tell [Posd loc (Print strAtom)]
+
+    printLnStmt =
+      do Posd loc e <- unary PrintLn_ (located $ reading $ check (StringRepr UnicodeRepr))
+         strAtom <- eval loc (EApp (StringConcat UnicodeRepr e (EApp (StringLit "\n"))))
+         tell [Posd loc (Print strAtom)]
+
+    letStmt =
+      followedBy (kw Let) $
+      depCons uniqueAtom $
+        \x ->
+          do setter <- fst <$> cons (atomSetter x) emptyList
+             stxAtoms %= Map.insert x setter
+
+    setGlobal =
+      followedBy (kw SetGlobal) $
+      depConsCond globalName $
+        \g ->
+          use (stxGlobals . at g) >>=
+            \case
+              Nothing -> return $ Left "known global variable name"
+              Just (Some var) ->
+                do (Posd loc e) <- fst <$> cons (located $ reading $ check $ globalType var) emptyList
+                   a <- eval loc e
+                   tell [Posd loc $ WriteGlobal var a]
+                   return (Right ())
+
+    setReg =
+      followedBy (kw SetRegister) $
+      depCons (reading regRef') $
+      \(Some r) ->
+        depCons (reading $ located $ check $ typeOfReg r) $
+        \(Posd loc e) ->
+          do emptyList
+             v <- eval loc e
+             tell [Posd loc $ SetReg r v]
+
+    setRef =
+      do stmtLoc <- position
+         followedBy (kw SetRef) $
+           depConsCond (located $ reading $ synth) $
+           \case
+             (Posd refLoc (Pair (ReferenceRepr t') refE)) ->
+               depCons (located $ reading $ check t') $
+               \(Posd valLoc valE) ->
+                 do emptyList
+                    refAtom <- eval refLoc refE
+                    valAtom <- eval valLoc valE
+                    tell [Posd stmtLoc $ WriteRef refAtom valAtom]
+                    return (Right ())
+             (Posd _ _) ->
+               return $ Left "expression with reference type"
+
+    dropRef =
+      do loc <- position
+         followedBy (kw DropRef_) $
+           depConsCond (located $ reading synth) $
+            \(Posd eLoc (Pair t refE)) ->
+               emptyList *>
+               case t of
+                 ReferenceRepr _ ->
+                   do refAtom <- eval eLoc refE
+                      tell [Posd loc $ DropRef refAtom]
+                      return $ Right ()
+                 _ -> return $ Left "expression with reference type"
+
+    assertion =
+      do (Posd loc (Posd cLoc cond, Posd mLoc msg)) <-
+           located $
+           binary Assert_
+             (located $ reading $ check BoolRepr)
+             (located $ reading $ check (StringRepr UnicodeRepr))
+         cond' <- eval cLoc cond
+         msg' <- eval mLoc msg
+         tell [Posd loc $ Assert cond' msg']
+
+    assumption =
+      do (Posd loc (Posd cLoc cond, Posd mLoc msg)) <-
+           located $
+           binary Assume_
+             (located $ reading $ check BoolRepr)
+             (located $ reading $ check (StringRepr UnicodeRepr))
+         cond' <- eval cLoc cond
+         msg' <- eval mLoc msg
+         tell [Posd loc $ Assume cond' msg']
+
+    breakpoint =
+      do (Posd loc (nm, arg_list)) <-
+           located $ binary Breakpoint_
+             (string <&> BreakpointName)
+             (rep ra_value)
+         case toCtx arg_list of
+           Some args -> tell [Posd loc $ Breakpoint nm args]
+      where
+        ra_value :: m (Some (Value s))
+        ra_value = (reading synth) >>= \case
+          Pair _ (EReg _ reg) -> pure $ Some $ RegValue reg
+          Pair _ (EAtom atm) -> pure $ Some $ AtomValue atm
+          _ -> empty
+
+
+blockBody' :: forall s ret m ext
+            . ( MonadSyntax Atomic m
+              , MonadState (SyntaxState s) m
+              , MonadIO m
+              , IsSyntaxExtension ext
+              , ?parserHooks :: ParserHooks ext )
+           => TypeRepr ret
+           -> m (Posd (TermStmt s ret), [Posd (Stmt ext s)])
+blockBody' ret = runWriterT go
+ where
+ go :: WriterT [Posd (Stmt ext s)] m (Posd (TermStmt s ret))
+ go = (fst <$> (cons (later (termStmt' ret)) emptyList)) <|>
+      (snd <$> (cons (later normStmt') go))
+
+termStmt' :: forall m s ret ext.
+   ( MonadWriter [Posd (Stmt ext s)] m
+   , MonadSyntax Atomic m
+   , MonadState (SyntaxState s) m
+   , MonadIO m
+   , IsSyntaxExtension ext
+   , ?parserHooks :: ParserHooks ext ) =>
+   TypeRepr ret -> m (Posd (TermStmt s ret))
+termStmt' retTy =
+  do stx <- anything
+     call (withPosFrom stx <$>
+       (jump <|> branch <|> maybeBranch <|> cases <|> ret <|> err <|> tailCall <|> out))
+
+  where
+    normalLabel =
+      do x <- labelName
+         l <- use (stxLabels . at x)
+         later $ describe "known label with no arguments" $
+           case l of
+             Nothing -> empty
+             Just (ArgLbl _) -> empty
+             Just (NoArgLbl lbl) -> pure lbl
+
+    lambdaLabel :: m (Some (LambdaLabel s))
+    lambdaLabel =
+      do x <- labelName
+         l <- use (stxLabels . at x)
+         later $ describe "known label with an argument" $
+           case l of
+             Nothing -> empty
+             Just (ArgLbl lbl) -> pure $ Some lbl
+             Just (NoArgLbl _) -> empty
+
+    typedLambdaLabel :: TypeRepr t -> m (LambdaLabel s t)
+    typedLambdaLabel t =
+      do x <- labelName
+         l <- use (stxLabels . at x)
+         later $ describe ("known label with an " <> T.pack (show t) <> " argument") $
+           case l of
+             Nothing -> empty
+             Just (ArgLbl lbl) ->
+               case testEquality (typeOfAtom (lambdaAtom lbl)) t of
+                 Nothing -> empty
+                 Just Refl -> pure lbl
+             Just (NoArgLbl _) -> empty
+
+    jump = unary Jump_ normalLabel <&> Jump
+
+    branch = kw Branch_ `followedBy`
+             (depCons (located (reading (check BoolRepr))) $
+                \ (Posd eloc cond) ->
+                  cons normalLabel (cons normalLabel emptyList) >>=
+                  \(l1, (l2, ())) -> do
+                    c <- eval eloc cond
+                    return (Br c l1 l2))
+
+    maybeBranch :: m (TermStmt s ret)
+    maybeBranch =
+      followedBy (kw MaybeBranch_) $
+      describe "valid arguments to maybe-branch" $
+      depCons (located (reading synth)) $
+        \(Posd sloc (Pair ty scrut)) ->
+          case ty of
+            MaybeRepr ty' ->
+              depCons (typedLambdaLabel ty') $
+                \lbl1 ->
+                  depCons normalLabel $
+                    \ lbl2 ->
+                      do s <- eval sloc scrut
+                         return $ MaybeBranch ty' s lbl1 lbl2
+            _ -> empty
+
+    cases :: m (TermStmt s ret)
+    cases =
+      followedBy (kw Case) $
+      depCons (located (reading synth)) $
+        \(Posd tgtloc (Pair ty tgt)) ->
+          describe ("cases for variant type " <> T.pack (show ty)) $
+          case ty of
+            VariantRepr ctx ->
+              do t <- eval tgtloc tgt
+                 VariantElim ctx t <$> backwards (go (Ctx.viewAssign ctx))
+            _ -> empty
+      where
+        go :: forall cases
+            . Ctx.AssignView TypeRepr cases
+           -> m (Ctx.Assignment (LambdaLabel s) cases)
+        go Ctx.AssignEmpty = emptyList $> Ctx.empty
+        go (Ctx.AssignExtend ctx' t) =
+          depCons (typedLambdaLabel t) $
+            \ lbl -> Ctx.extend <$>
+                       go (Ctx.viewAssign ctx') <*>
+                       pure lbl
+
+    ret :: m (TermStmt s ret)
+    ret =
+        do Posd loc e <- unary Return_ (located (reading (check retTy)))
+           Return <$> eval loc e
+
+    tailCall :: m (TermStmt s ret)
+    tailCall =
+      followedBy (kw TailCall_) $
+        describe "function atom and arguments" $
+          do -- commit
+             depCons (located (reading synth)) $
+               \case
+                 Posd loc (Pair (FunctionHandleRepr argumentTypes retTy') funExpr) ->
+                   case testEquality retTy retTy' of
+                       Nothing -> empty
+                       Just Refl ->
+                         do funAtom <- eval loc funExpr
+                            describe ("arguments with types " <> T.pack (show argumentTypes)) $
+                              TailCall funAtom argumentTypes <$> backwards (go (Ctx.viewAssign argumentTypes))
+                 _ -> empty
+      where
+        go :: forall argTypes
+            . Ctx.AssignView TypeRepr argTypes
+           -> m (Ctx.Assignment (Atom s) argTypes)
+        go Ctx.AssignEmpty = emptyList *> pure Ctx.empty
+        go (Ctx.AssignExtend tys ty) =
+          depCons (located (reading (check ty))) $
+            \(Posd loc arg) ->
+               Ctx.extend <$> go (Ctx.viewAssign tys) <*> eval loc arg
+
+    err :: m (TermStmt s ret)
+    err =
+      do Posd loc e <- unary Error_ (located (reading (check (StringRepr UnicodeRepr))))
+         ErrorStmt <$> eval loc e
+
+    out :: m (TermStmt s ret)
+    out = followedBy (kw Output_) $
+          do -- commit
+             depCons lambdaLabel $
+               \(Some lbl) ->
+                 depCons (located (reading (check (typeOfAtom (lambdaAtom lbl))))) $
+                   \(Posd loc arg) ->
+                     emptyList *>
+                       (Output lbl <$> eval loc arg)
+
+
+
+data Rand ext s t = Rand (AST s) (E ext s t)
+
+
+
+
+--------------------------------------------------------------------------
+
+data Arg t = Arg AtomName Position (TypeRepr t)
+
+someAssign ::
+  forall m ext a.
+  ( MonadSyntax Atomic m
+  , ?parserHooks :: ParserHooks ext
+  ) =>
+  Text ->
+  m (Some a) ->
+  m (Some (Ctx.Assignment a))
+someAssign desc sub = call (go (Some Ctx.empty))
+  where
+    go :: Some (Ctx.Assignment a) -> m (Some (Ctx.Assignment a))
+    go args@(Some prev) =
+      describe desc $
+        (emptyList *> pure args) <|>
+        (depCons sub $
+           \(Some a) ->
+             go (Some $ Ctx.extend prev a))
+
+arguments' :: forall m ext
+            . ( MonadSyntax Atomic m, ?parserHooks :: ParserHooks ext )
+           => m (Some (Ctx.Assignment Arg))
+arguments' = someAssign "argument list" oneArg
+  where oneArg =
+          (describe "argument" $
+           located $
+           cons atomName (cons isType emptyList)) <&>
+          \(Posd loc (x, (Some t, ()))) -> Some (Arg x loc t)
+
+
+saveArgs :: (MonadState (SyntaxState s) m, MonadError (ExprErr s) m)
+         => Ctx.Assignment Arg init
+         -> Ctx.Assignment (Atom s) init
+         -> m ()
+saveArgs ctx1 ctx2 =
+  let combined = Ctx.zipWith
+                   (\(Arg x p _) argAtom ->
+                      (Const (Some (Functor.Pair (Const x) (Functor.Pair (Const p) argAtom)))))
+                   ctx1 ctx2
+  in forFC_ combined $
+       \(Const (Some (Functor.Pair (Const x) (Functor.Pair (Const argPos) y)))) ->
+         with (stxAtoms . at x) $
+           \case
+             Just _ -> throwError $ DuplicateAtom argPos x
+             Nothing ->
+               do stxAtoms %= Map.insert x (Some y)
+
+data FunctionHeader =
+  forall args ret .
+  FunctionHeader { _headerName :: FunctionName
+                 , _headerArgs :: Ctx.Assignment Arg args
+                 , _headerReturnType :: TypeRepr ret
+                 , _headerHandle :: FnHandle args ret
+                 , _headerLoc :: Position
+                 }
+
+data FunctionSource s =
+  FunctionSource { _functionRegisters :: [AST s]
+                 , _functionBody :: AST s
+                 }
+
+functionHeader' :: ( MonadSyntax Atomic m, ?parserHooks :: ParserHooks ext )
+                => m ( (FunctionName, Some (Ctx.Assignment Arg), Some TypeRepr, Position)
+                     , FunctionSource s
+                     )
+functionHeader' =
+  do (fnName, (Some theArgs, (Some ret, (regs, body)))) <-
+       followedBy (kw Defun) $
+       cons funName $
+       cons arguments' $
+       cons isType $
+       cons registers anything <|> ([], ) <$> anything
+     loc <- position
+     return ((fnName, Some theArgs, Some ret, loc), FunctionSource regs body)
+  where
+    registers = call $ kw Registers `followedBy` anyList
+
+functionHeader :: (?parserHooks :: ParserHooks ext)
+               => AST s
+               -> TopParser s (FunctionHeader, FunctionSource s)
+functionHeader defun =
+  do ((fnName, Some theArgs, Some ret, loc), src) <- liftSyntaxParse functionHeader' defun
+     ha <- use $ stxProgState  . progHandleAlloc
+     handle <- liftIO $ mkHandle' ha fnName (argTypes theArgs) ret
+     let header = FunctionHeader fnName theArgs ret handle loc
+
+     saveHeader fnName header
+     return $ (header, src)
+  where
+    saveHeader n h =
+      stxFunctions %= Map.insert n h
+
+
+
+
+global :: (?parserHooks :: ParserHooks ext)
+       => AST s
+       -> TopParser s (Some GlobalVar)
+global stx =
+  do (var@(GlobalName varName), Some t) <- liftSyntaxParse (call (binary DefGlobal globalName isType)) stx
+     ha <- use $ stxProgState  . progHandleAlloc
+     v <- liftIO $ freshGlobalVar ha varName t
+     let sv = Some v
+     stxGlobals %= Map.insert var sv
+     return sv
+
+-- | Parse a forward declaration.
+declare :: (?parserHooks :: ParserHooks ext)
+        => AST t
+        -> TopParser s FunctionHeader
+declare stx =
+  do ((fnName, (Some theArgs, (Some ret, ()))), loc) <-
+       liftSyntaxParse (do r <- followedBy (kw Declare) $
+                                cons funName $
+                                cons arguments' $
+                                cons isType emptyList
+                           loc <- position
+                           pure (r, loc))
+                       stx
+     ha <- use $ stxProgState . progHandleAlloc
+     handle <- liftIO $ mkHandle' ha fnName (argTypes theArgs) ret
+
+     let header = FunctionHeader fnName theArgs ret handle loc
+     stxForwardDecs %= Map.insert fnName header
+     pure header
+
+-- | Parse an extern.
+extern :: (?parserHooks :: ParserHooks ext)
+       => AST s
+       -> TopParser s (Some GlobalVar)
+extern stx =
+  do (var@(GlobalName varName), Some t) <- liftSyntaxParse (call (binary Extern globalName isType)) stx
+     ha <- use $ stxProgState  . progHandleAlloc
+     v <- liftIO $ freshGlobalVar ha varName t
+     let sv = Some v
+     stxExterns %= Map.insert var sv
+     return sv
+
+topLevel :: (?parserHooks :: ParserHooks ext)
+         => AST s
+         -> TopParser s (Maybe (FunctionHeader, FunctionSource s))
+topLevel ast =
+  (Just <$> functionHeader ast) `catchError` \e ->
+  (global ast $> Nothing)       `catchError` \_ ->
+  (declare ast $> Nothing)      `catchError` \_ ->
+  (extern ast $> Nothing)       `catchError` \_ ->
+  throwError e
+
+argTypes :: Ctx.Assignment Arg init -> Ctx.Assignment TypeRepr init
+argTypes  = fmapFC (\(Arg _ _ t) -> t)
+
+
+type BlockTodo s ret =
+  (LabelName, BlockID s, Progress, AST s)
+
+blocks :: forall s ret m ext
+        . ( MonadState (SyntaxState s) m
+          , MonadSyntax Atomic m
+          , MonadIO m
+          , TraverseExt ext
+          , IsSyntaxExtension ext
+          , ?parserHooks :: ParserHooks ext )
+        => TypeRepr ret
+        -> m [Block ext s ret]
+blocks ret =
+      depCons startBlock' $
+      \ startContents ->
+        do todo <- rep blockLabel'
+           forM (startContents : todo) $ \(_, bid, pr, stmts) ->
+             do (term, stmts') <- withProgress (const pr) $ parse stmts (call (blockBody' ret))
+                pure $ mkBlock bid mempty (Seq.fromList stmts') term
+
+
+  where
+
+    startBlock' :: (MonadState (SyntaxState s) m, MonadSyntax Atomic m, MonadIO m) => m (BlockTodo s ret)
+    startBlock' =
+      call $
+      describe "starting block" $
+      followedBy (kw Start) $
+      depCons labelName $
+      \l ->
+        do lbl <- newLabel l
+           pr <- progress
+           rest <- anything
+           return (l, LabelID lbl, pr, rest)
+
+    blockLabel' :: m (BlockTodo s ret)
+    blockLabel' =
+      call $
+      followedBy (kw DefBlock) $
+      simpleBlock <|> argBlock
+      where
+        simpleBlock, argBlock :: m (BlockTodo s ret)
+        simpleBlock =
+          depConsCond labelName $
+          \ l ->
+            do lbls <- use stxLabels
+               pr <- progress
+               body <- anything
+               case Map.lookup l lbls of
+                 Just _ -> return $ Left "unique label"
+                 Nothing ->
+                   do theLbl <- newLabel l
+                      return $ Right (l, LabelID theLbl, pr, body)
+        argBlock =
+          call $
+          depConsCond lambdaLabelBinding $
+          \ (l, (Some lbl)) ->
+            do pr <- progress
+               body <- anything
+               return $ Right (l, LambdaID lbl, pr, body)
+
+eval :: (MonadWriter [Posd (Stmt ext s)] m, MonadState (SyntaxState s) m, MonadIO m, IsSyntaxExtension ext)
+     => Position -> E ext s t -> m (Atom s t)
+eval _   (EAtom theAtom)  = pure theAtom -- The expression is already evaluated
+eval loc (EApp e)         = freshAtom loc . EvalApp =<< traverseFC (eval loc) e
+eval _   (EReg loc reg)   = freshAtom loc (ReadReg reg)
+eval _   (EGlob loc glob) = freshAtom loc (ReadGlobal glob)
+eval loc (EDeref eloc e)  = freshAtom loc . ReadRef =<< eval eloc e
+
+newtype TopParser s a =
+  TopParser { runTopParser :: ExceptT (ExprErr s)
+                                (StateT (SyntaxState s) IO)
+                                a
+            }
+  deriving (Functor)
+
+top :: NonceGenerator IO s -> HandleAllocator -> [(SomeHandle,Position)] -> TopParser s a -> IO (Either (ExprErr s) a)
+top ng ha builtIns (TopParser (ExceptT (StateT act))) =
+  fst <$> act (initSyntaxState ng (initProgState builtIns ha))
+
+instance Applicative (TopParser s) where
+  pure x = TopParser (pure x)
+  (TopParser f) <*> (TopParser x) = TopParser (f <*> x)
+
+instance Alternative (TopParser s) where
+  empty = TopParser $ throwError (TrivialErr InternalPos)
+  (TopParser x) <|> (TopParser y) = TopParser (x <|> y)
+
+instance MonadPlus (TopParser s) where
+  mzero = empty
+  mplus = (<|>)
+
+instance Semigroup (TopParser s a) where
+  (<>) = (<|>)
+
+instance Monoid (TopParser s a) where
+  mempty = empty
+
+instance Monad (TopParser s) where
+  (TopParser m) >>= f = TopParser $ m >>= runTopParser . f
+
+instance MonadError (ExprErr s) (TopParser s) where
+  throwError = TopParser . throwError
+  catchError m h = TopParser $ catchError (runTopParser m) (runTopParser . h)
+
+instance MonadState (SyntaxState s) (TopParser s) where
+  get = TopParser get
+  put = TopParser . put
+
+instance MonadIO (TopParser s) where
+  liftIO = TopParser . lift . lift
+
+
+initParser :: forall s m ext
+            . ( MonadState (SyntaxState s) m
+              , MonadError (ExprErr s) m
+              , MonadIO m
+              , ?parserHooks :: ParserHooks ext )
+           => FunctionHeader
+           -> FunctionSource s
+           -> m ()
+initParser (FunctionHeader _ (funArgs :: Ctx.Assignment Arg init) _ _ _) (FunctionSource regs _) =
+  do ng <- use stxNonceGen
+     progState <- use stxProgState
+     put $ initSyntaxState ng progState
+     let types = argTypes funArgs
+     inputAtoms <- liftIO $ mkInputAtoms ng (OtherPos "args") types
+     saveArgs funArgs inputAtoms
+     forM_ regs saveRegister
+
+  where
+    saveRegister :: Syntax Atomic -> m ()
+    saveRegister (L [A (Rg x), t]) =
+      do Some ty <- liftSyntaxParse isType t
+         r <- newUnassignedReg ty
+         stxRegisters %= Map.insert x (Some r)
+    saveRegister other = throwError $ InvalidRegister (syntaxPos other) other
+
+cfgs :: ( IsSyntaxExtension ext
+        , ?parserHooks :: ParserHooks ext )
+     => [AST s]
+     -> TopParser s [AnyCFG ext]
+cfgs = fmap parsedProgCFGs <$> prog
+
+prog :: ( TraverseExt ext
+        , IsSyntaxExtension ext
+        , ?parserHooks :: ParserHooks ext )
+     => [AST s]
+     -> TopParser s (ParsedProgram ext)
+prog defuns =
+  do headers <- catMaybes <$> traverse topLevel defuns
+     cs <- forM headers $
+       \(hdr@(FunctionHeader _ _ ret handle _), src@(FunctionSource _ body)) ->
+         do initParser hdr src
+            args <- toList <$> use stxAtoms
+            let ?returnType = ret
+            st <- get
+            (theBlocks, st') <- liftSyntaxParse (runStateT (blocks ret) st) body
+            put st'
+            let vs = Set.fromList [ Some (AtomValue a) | Some a <- args ]
+            case theBlocks of
+              []       -> error "found no blocks"
+              (e:rest) ->
+                do let entry = case blockID e of
+                                 LabelID lbl -> lbl
+                                 LambdaID {} -> error "initial block is lambda"
+                       e' = mkBlock (blockID e) vs (blockStmts e) (blockTerm e)
+                   return $ AnyCFG (CFG handle entry (e' : rest))
+     gs <- use stxGlobals
+     externs <- use stxExterns
+     fds <- uses stxForwardDecs $ fmap $
+              \(FunctionHeader _ _ _ handle _) -> SomeHandle handle
+     return $ ParsedProgram
+       { parsedProgGlobals = gs
+       , parsedProgExterns = externs
+       , parsedProgCFGs = cs
+       , parsedProgForwardDecs = fds
+       }
diff --git a/src/Lang/Crucible/Syntax/ExprParse.hs b/src/Lang/Crucible/Syntax/ExprParse.hs
new file mode 100644
--- /dev/null
+++ b/src/Lang/Crucible/Syntax/ExprParse.hs
@@ -0,0 +1,282 @@
+{-# 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.ExprParse
+  ( SyntaxParse
+  , syntaxParseIO
+
+  -- * Errors
+  , SyntaxError(..)
+  , printSyntaxError
+
+  -- * Testing utilities
+  , TrivialAtom(..)
+  , test
+  ) where
+
+import Control.Applicative
+import Control.Lens hiding (List, cons, backwards)
+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 Data.Foldable as Foldable
+import Data.List
+import qualified Data.List.NonEmpty as NE
+import Data.List.NonEmpty (NonEmpty(..))
+import Data.String
+import Data.Text (Text)
+import qualified Data.Text as T
+import qualified Data.Text.IO as T
+
+import GHC.Stack
+
+import Lang.Crucible.Syntax.SExpr
+
+import qualified Text.Megaparsec as MP
+
+import Lang.Crucible.Syntax.Monad
+
+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
+
+delimitSearch :: Search a -> Search a
+delimitSearch (Try first rest) = Try first $ delimitSearch rest
+delimitSearch Fail = Fail
+delimitSearch Cut = Fail
+
+cutSearch :: Search a
+cutSearch = Cut
+
+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
+
+instance Semigroup (P atom a) where
+  P s1 f1 <> P s2 f2 = P (s1 <> s2) (f1 <> f2)
+
+instance Monoid (P atom a) where
+  mempty = P mempty mempty
+
+instance Applicative (P atom) where
+  pure x = P (pure x) mempty
+  f <*> x = ap f x
+
+instance Alternative (P atom) where
+  empty = mempty
+  (<|>) = mappend
+
+instance Monad (P atom) where
+  (P xs e) >>= f = mappend (foldMap f xs) (P empty e)
+
+instance MonadPlus (P atom) where
+  mzero = empty
+  mplus = (<|>)
+
+newtype STP atom a = STP { runSTP :: IO (P atom a) }
+  deriving (Functor, Semigroup, Monoid)
+
+instance Applicative (STP atom) where
+  pure = STP . pure . pure
+  (<*>) = ap
+
+instance Monad (STP atom) where
+  STP m >>= f = STP $ do
+    P xs e <- m
+    mappend (runSTP (foldMap f xs)) (return $ P empty e)
+
+instance MonadIO (STP atom) where
+  liftIO m = STP $ return <$> m
+
+data SyntaxParseCtx atom =
+  SyntaxParseCtx { _parseProgress :: Progress
+                 , _parseReason :: Reason atom
+                 , _parseFocus :: Syntax atom
+                 }
+  deriving Show
+
+parseProgress :: Simple Lens (SyntaxParseCtx atom) Progress
+parseProgress = lens _parseProgress (\s v -> s { _parseProgress = v })
+
+parseReason :: Simple Lens (SyntaxParseCtx atom) (Reason atom)
+parseReason = lens _parseReason (\s v -> s { _parseReason = v })
+
+parseFocus :: Simple Lens (SyntaxParseCtx atom) (Syntax atom)
+parseFocus = lens _parseFocus (\s v -> s { _parseFocus = v })
+
+-- | The default parsing monad. Use its 'MonadSyntax' instance to write parsers.
+newtype SyntaxParse atom a =
+  SyntaxParse { runSyntaxParse :: ReaderT (SyntaxParseCtx atom)
+                                          (STP atom)
+                                          a }
+  deriving ( Functor, Applicative, Monad
+           , MonadReader (SyntaxParseCtx atom), MonadIO
+           )
+
+instance Alternative (SyntaxParse atom) where
+  empty =
+    SyntaxParse $ ReaderT $ \(SyntaxParseCtx p r _) ->
+      STP $ return $ P empty (Oops p (pure r))
+  (SyntaxParse (ReaderT x)) <|> (SyntaxParse (ReaderT y)) =
+    SyntaxParse $ ReaderT $ \ctx -> STP $ do
+      a <- runSTP $ x ctx
+      b <- runSTP $ y ctx
+      return $ a <|> b
+
+instance MonadPlus (SyntaxParse atom) where
+  mzero = empty
+  mplus = (<|>)
+
+instance MonadSyntax atom (SyntaxParse atom) where
+  anything = view parseFocus
+  progress = view parseProgress
+  withFocus stx = local $ set parseFocus stx
+  withProgress f = local $ over parseProgress f
+  withReason r = local $ set parseReason r
+  cut =
+    SyntaxParse $
+    ReaderT $
+    \(SyntaxParseCtx p r _) ->
+      STP $ return $
+      P cutSearch (Oops p (pure r))
+  delimit (SyntaxParse (ReaderT f)) =
+    SyntaxParse $
+    ReaderT $
+    \r -> STP $ do
+      P s e <- runSTP $ f r
+      return $ P (delimitSearch s) e
+  call (SyntaxParse (ReaderT p)) =
+    SyntaxParse $
+    ReaderT $
+    \r -> STP $ do
+      P s e <- runSTP $ p r
+      return $ case s of
+        Try x _ -> P (Try x Fail) Ok
+        Cut -> P Cut e
+        Fail -> P Fail e
+
+-- | Syntax errors explain why the error occurred.
+data SyntaxError atom = SyntaxError (NonEmpty (Reason atom))
+  deriving (Show, Eq)
+
+-- | Convert an internal error structure into a form suitable for
+-- humans to read.
+printSyntaxError :: IsAtom atom => SyntaxError atom -> Text
+printSyntaxError (SyntaxError rs) =
+  T.intercalate "\n\tor\n" $ nub $ map printGroup $ groupReasons rs
+ where
+    reasonPos (Reason found _) = syntaxPos found
+    groupReasons reasons =
+      [ (reasonPos repr, g)
+      | g@(repr :| _) <- NE.groupBy (\x y -> reasonPos x == reasonPos y) (NE.toList reasons)
+      ]
+    printGroup (p, r@(Reason found _) :| more) =
+      T.concat
+      [ "At ", T.pack (show p)
+      , ", expected ", T.intercalate " or " (nub $ sort [ wanted | Reason _ wanted <- r:more ])
+      , " but got ", toText mempty found]
+
+-- | Attempt to parse the given piece of syntax, returning the first success found,
+--   or the error(s) with the greatest progress otherwise.
+syntaxParseIO :: IsAtom atom => SyntaxParse atom a -> Syntax atom -> IO (Either (SyntaxError atom) a)
+syntaxParseIO p stx = do
+  (P yes no) <-
+        runSTP $ runReaderT (runSyntaxParse p) $
+          SyntaxParseCtx emptyProgress (Reason stx (T.pack "bad syntax")) stx
+  case Foldable.toList yes of
+    [] ->
+      return $ Left $ SyntaxError $
+        case no of
+          Ok        -> error "Internal error: no reason provided, yet no successful parse found."
+          Oops _ rs -> rs
+    (r:_) -> return $ Right r
+
+-- | A trivial atom, which is a wrapper around 'Text', for use when testing the library.
+newtype TrivialAtom = TrivialAtom Text deriving (Show, Eq)
+
+instance IsAtom TrivialAtom where
+  showAtom (TrivialAtom x) = x
+
+instance IsString TrivialAtom where
+  fromString x = TrivialAtom (fromString x)
+
+-- | Test a parser on some input, displaying the result.
+test :: (HasCallStack, Show a) => Text -> SyntaxParse TrivialAtom a -> IO ()
+test txt p =
+  case MP.parse (skipWhitespace *> sexp (TrivialAtom <$> identifier) <* MP.eof) "input" txt of
+     Left err -> putStrLn "Reader error: " >> putStrLn (MP.errorBundlePretty err)
+     Right sexpr ->
+       syntaxParseIO p sexpr >>= \case
+         Left e -> T.putStrLn (printSyntaxError e)
+         Right ok -> print ok
diff --git a/src/Lang/Crucible/Syntax/Monad.hs b/src/Lang/Crucible/Syntax/Monad.hs
new file mode 100644
--- /dev/null
+++ b/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/src/Lang/Crucible/Syntax/Overrides.hs b/src/Lang/Crucible/Syntax/Overrides.hs
new file mode 100644
--- /dev/null
+++ b/src/Lang/Crucible/Syntax/Overrides.hs
@@ -0,0 +1,68 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Lang.Crucible.Syntax.Overrides
+  ( setupOverrides
+  ) where
+
+import Control.Lens hiding ((:>), Empty)
+import Control.Monad.Except (runExceptT)
+import Control.Monad.IO.Class
+import System.IO
+
+import Data.Parameterized.Context hiding (view)
+
+import What4.Expr.Builder
+import What4.ProgramLoc
+import What4.Solver (LogData(..), defaultLogData)
+import What4.Solver.Z3 (z3Adapter)
+
+import Lang.Crucible.Backend
+import qualified Lang.Crucible.Backend.Prove as CB
+import Lang.Crucible.Types
+import Lang.Crucible.FunctionHandle
+import Lang.Crucible.Simulator
+import qualified Lang.Crucible.Utils.Seconds as Sec
+import qualified Lang.Crucible.Utils.Timeout as CTO
+
+
+setupOverrides ::
+  (IsSymInterface sym, sym ~ (ExprBuilder t st fs)) =>
+  sym -> HandleAllocator -> IO [(FnBinding p sym ext, Position)]
+setupOverrides _ ha =
+  do f1 <- FnBinding <$> mkHandle ha "proveObligations"
+                     <*> pure (UseOverride (mkOverride "proveObligations" proveObligations))
+
+     return [(f1, InternalPos)]
+
+
+proveObligations :: (IsSymInterface sym, sym ~ (ExprBuilder t st fs)) =>
+  OverrideSim p sym ext r EmptyCtx UnitType (RegValue sym UnitType)
+proveObligations =
+  ovrWithBackend $ \bak ->
+  do let sym = backendGetSym bak
+     h <- printHandle <$> getContext
+     liftIO $ do
+       hPutStrLn h "Attempting to prove all outstanding obligations!\n"
+
+       let logData = defaultLogData { logCallbackVerbose = \_ -> hPutStrLn h
+                                    , logReason = "assertion proof" }
+       let timeout = CTO.Timeout (Sec.secondsFromInt 5)
+       let prover = CB.offlineProver timeout sym logData z3Adapter
+       let strat = CB.ProofStrategy prover CB.keepGoing
+       let ppResult o =
+             \case
+               CB.Proved {}  -> unlines ["Proof Succeeded!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
+               CB.Disproved {} -> unlines ["Proof failed!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
+               CB.Unknown {} -> unlines ["Proof inconclusive!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
+       let printer = CB.ProofConsumer $ \o r -> hPutStrLn h (ppResult o r)
+       runExceptT (CB.proveCurrentObligations bak strat printer) >>=
+         \case
+           Left CTO.TimedOut -> hPutStrLn h "Proof timed out!"
+           Right () -> pure ()
+
+       clearProofObligations bak
diff --git a/src/Lang/Crucible/Syntax/Prog.hs b/src/Lang/Crucible/Syntax/Prog.hs
new file mode 100644
--- /dev/null
+++ b/src/Lang/Crucible/Syntax/Prog.hs
@@ -0,0 +1,87 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Lang.Crucible.Syntax.Prog
+  ( assertNoExterns
+  , assertNoForwardDecs
+  , doParseCheck
+  ) where
+
+import Control.Monad
+
+import qualified Data.Map as Map
+import Data.Map (Map)
+import Data.Text (Text)
+import qualified Data.Text.IO as T
+import qualified Prettyprinter as PP
+import System.IO
+import System.Exit
+import Text.Megaparsec as MP
+
+import Data.Parameterized.Nonce
+import Data.Parameterized.Some (Some(Some))
+
+import qualified Lang.Crucible.CFG.Core as C
+import Lang.Crucible.CFG.Extension (IsSyntaxExtension)
+import Lang.Crucible.CFG.Reg
+import Lang.Crucible.CFG.SSAConversion
+
+import Lang.Crucible.Syntax.Concrete
+import Lang.Crucible.Syntax.SExpr
+import Lang.Crucible.Syntax.Atoms
+
+import Lang.Crucible.Analysis.Postdom
+import Lang.Crucible.FunctionHandle
+
+import What4.FunctionName
+
+assertNoExterns :: Map GlobalName (Some GlobalVar) -> IO ()
+assertNoExterns externs =
+  unless (Map.null externs) $
+  do putStrLn "Externs not currently supported"
+     exitFailure
+
+assertNoForwardDecs :: Map FunctionName SomeHandle -> IO ()
+assertNoForwardDecs fds =
+  unless (Map.null fds) $
+  do putStrLn "Forward declarations not currently supported"
+     exitFailure
+
+-- | The main loop body, useful for both the program and for testing.
+doParseCheck
+   :: (IsSyntaxExtension ext, ?parserHooks :: ParserHooks ext)
+   => FilePath -- ^ The name of the input (appears in source locations)
+   -> Text     -- ^ The contents of the input
+   -> Bool     -- ^ Whether to pretty-print the input data as well
+   -> Handle   -- ^ A handle that will receive the output
+   -> IO ()
+doParseCheck fn theInput pprint outh =
+  do Some ng <- newIONonceGenerator
+     ha <- newHandleAllocator
+     case MP.parse (skipWhitespace *> many (sexp atom) <* eof) fn theInput of
+       Left err ->
+         do putStrLn $ errorBundlePretty err
+            exitFailure
+       Right v ->
+         do when pprint $
+              forM_ v $
+                \e -> T.hPutStrLn outh (printExpr e) >> hPutStrLn outh ""
+            cs <- top ng ha [] $ prog v
+            case cs of
+              Left err -> hPutStrLn outh (show (PP.pretty err))
+              Right (ParsedProgram{ parsedProgCFGs = ok
+                                  , parsedProgExterns = externs
+                                  , parsedProgForwardDecs = fds
+                                  }) -> do
+                assertNoExterns externs
+                assertNoForwardDecs fds
+                forM_ ok $
+                 \(AnyCFG theCfg) ->
+                   do C.SomeCFG ssa <- return $ toSSA theCfg
+                      hPutStrLn outh $ show $ cfgHandle theCfg
+                      hPutStrLn outh $ show $ C.ppCFG' True (postdomInfo ssa) ssa
+
diff --git a/src/Lang/Crucible/Syntax/SExpr.hs b/src/Lang/Crucible/Syntax/SExpr.hs
new file mode 100644
--- /dev/null
+++ b/src/Lang/Crucible/Syntax/SExpr.hs
@@ -0,0 +1,192 @@
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ViewPatterns #-}
+module Lang.Crucible.Syntax.SExpr
+  ( pattern A
+  , pattern L
+  , pattern (:::)
+  , Syntax(..)
+  , Datum(..)
+  , Syntactic(..)
+  ,  Parser
+  , syntaxPos
+  , withPosFrom
+  , sexp
+  , identifier
+  , toText
+  , datumToText
+  , skipWhitespace
+  , PrintRules(..)
+  , PrintStyle(..)
+  , Layer(..)
+  , IsAtom(..)
+  ) where
+
+import Data.Char (isDigit, isLetter)
+import Data.Text (Text)
+import qualified Data.Text as T
+import Data.Void
+import What4.ProgramLoc as C
+
+import Text.Megaparsec as MP
+import Text.Megaparsec.Char
+import qualified Text.Megaparsec.Char.Lexer as L
+import qualified Prettyprinter as PP
+import qualified Prettyprinter.Render.Text as PP (renderStrict)
+
+
+-- | Syntax objects, in which each layer is annotated with a source position.
+newtype Syntax a = Syntax { unSyntax :: Posd (Layer Syntax a) }
+  deriving (Show, Functor, Eq)
+
+-- | Syntax objects divorced of their source-code context, without source positions.
+newtype Datum a = Datum { unDatum :: Layer Datum a}
+  deriving (Show, Functor, Eq)
+
+-- | Extract the source position from a 'Syntax' object.
+syntaxPos :: Syntax a -> Position
+syntaxPos (Syntax (Posd p _)) = p
+
+-- | Use the position from a syntax object around something else.
+withPosFrom :: Syntax a -> b -> Posd b
+withPosFrom stx x = Posd (syntaxPos stx) x
+
+-- | Instances of 'Syntactic' support observations using the 'L' and 'A' patterns.
+class Syntactic a b | a -> b where
+  syntaxE :: a -> Layer Syntax b
+
+instance Syntactic (Layer Syntax a) a where
+  syntaxE = id
+
+
+instance Syntactic (Syntax a) a where
+  syntaxE (Syntax (Posd _ e)) = e
+
+-- | Match an atom from a syntactic structure
+pattern A :: Syntactic a b => b -> a
+pattern A x <- (syntaxE -> Atom x)
+
+-- | Match a list from a syntactic structure
+pattern L :: Syntactic a b => [Syntax b] -> a
+pattern L xs <- (syntaxE -> List xs)
+
+-- | Match the head and tail of a list-like structure
+pattern (:::) :: Syntactic a b => Syntax b -> [Syntax b] -> a
+pattern x ::: xs <- (syntaxE -> List (x : xs))
+
+-- | The pattern functor for syntax, used both for 'Syntax' and
+-- 'Datum'. In 'Syntax', it is composed with another structure that
+-- adds source positions.
+data Layer f a = List [f a] | Atom a
+  deriving (Show, Functor, Eq)
+
+-- | Convert any syntactic structure to its simplest description.
+syntaxToDatum :: Syntactic expr atom => expr -> Datum atom
+syntaxToDatum (A x) = Datum (Atom x)
+syntaxToDatum (L xs) = Datum (List (map syntaxToDatum xs))
+syntaxToDatum _ = error "impossible - bad Syntactic instance"
+
+-- | A parser for s-expressions.
+type Parser = Parsec Void Text
+
+-- | Skip whitespace.
+skipWhitespace :: Parser ()
+skipWhitespace = L.space space1 lineComment blockComment
+  where lineComment = L.skipLineComment ";"
+        blockComment = L.skipBlockComment "#|" "|#"
+
+-- | Skip the whitespace after a token.
+lexeme :: Parser a -> Parser a
+lexeme = L.lexeme skipWhitespace
+
+-- | Parse something with its location.
+withPos :: Parser a -> Parser (Posd a)
+withPos p =
+  do MP.SourcePos file line col <- getSourcePos
+     let loc = C.SourcePos (T.pack file) (unPos line) (unPos col)
+     res <- p
+     return $ Posd loc res
+
+-- | Parse a particular string.
+symbol :: Text -> Parser Text
+symbol = L.symbol skipWhitespace
+
+-- | Parse a parenthesized list.
+list :: Parser (Syntax a) -> Parser (Syntax a)
+list p =
+  do Posd loc _ <- withPos (symbol "(")
+     xs <- many p
+     _ <- lexeme $ symbol ")"
+     return $ Syntax (Posd loc (List xs))
+
+-- | Given a parser for atoms, parse an s-expression that contains them.
+sexp :: Parser a -> Parser (Syntax a)
+sexp atom =
+  (Syntax . fmap Atom <$> lexeme (withPos atom)) <|>
+  list (sexp atom)
+
+-- | Parse an identifier.
+identifier :: Parser Text
+identifier = T.pack <$> identString
+  where letterLike x = isLetter x || elem x ("<>=+-*/!_\\?" :: [Char])
+        nameChar x = letterLike x || isDigit x || elem x ("$" :: [Char])
+        identString = (:) <$> satisfy letterLike <*> many (satisfy nameChar)
+
+-- | Styles of printing
+data PrintStyle =
+  -- | Special forms should treat the first n subforms as special, and
+  -- the remaining as a body. For instance, for a Lisp-like
+  -- let-expression, use 'Special 1' for indentation.
+  Special Int
+
+-- | Printing rules describe how to specially format expressions that
+-- begin with particular atoms.
+newtype PrintRules a = PrintRules (a -> Maybe PrintStyle)
+
+instance Semigroup (PrintRules a) where
+  PrintRules f <> PrintRules g = PrintRules $ \z -> f z <|> g z
+
+instance Monoid (PrintRules a) where
+  mempty = PrintRules $ const Nothing
+
+
+class IsAtom a where
+  showAtom :: a -> Text
+
+pprint :: (Syntactic expr a, IsAtom a) => PrintRules a -> expr -> PP.Doc ann
+pprint rules expr = pprintDatum rules (syntaxToDatum expr)
+
+pprintDatum :: IsAtom a => PrintRules a -> Datum a -> PP.Doc ann
+pprintDatum rules@(PrintRules getLayout) stx =
+  case unDatum stx of
+    Atom at -> ppAtom at
+    List lst ->
+      PP.parens . PP.group $
+      case lst of
+        [] -> mempty
+        [x] -> pprintDatum rules x
+        ((unDatum -> Atom car) : xs) ->
+          case getLayout car of
+            Nothing -> ppAtom car <> PP.space <> PP.align (PP.vsep $ pprintDatum rules <$> xs)
+            Just (Special i) ->
+              let (special, rest) = splitAt i xs
+              in PP.hang 2 $ PP.vsep $
+                 PP.group (PP.hang 2 $ PP.vsep $ ppAtom car : (map (pprintDatum rules) special)) :
+                 map (pprintDatum rules) rest
+        xs -> PP.vsep $ pprintDatum rules <$> xs
+
+  where ppAtom = PP.pretty . showAtom
+
+-- | Render a syntactic structure to text, according to rules.
+toText :: (Syntactic expr a, IsAtom a) => PrintRules a -> expr -> Text
+toText rules stx = PP.renderStrict (PP.layoutSmart opts $ pprint rules stx)
+  where opts = PP.LayoutOptions (PP.AvailablePerLine 80 0.8)
+
+-- | Render a datum to text according to rules.
+datumToText :: IsAtom a => PrintRules a -> Datum a -> Text
+datumToText rules dat = PP.renderStrict (PP.layoutSmart opts $ pprintDatum rules dat)
+  where opts = PP.LayoutOptions (PP.AvailablePerLine 80 0.8)
diff --git a/test/Tests.hs b/test/Tests.hs
new file mode 100644
--- /dev/null
+++ b/test/Tests.hs
@@ -0,0 +1,199 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE RankNTypes #-}
+module Main (main) where
+
+import qualified Data.List as List
+import Data.Text (Text)
+import qualified Data.Text as T
+import qualified Data.Text.IO as T
+
+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
+
+import Test.Tasty (defaultMain, TestTree, testGroup)
+import Test.Tasty.Golden
+import Test.Tasty.HUnit
+import qualified Text.Megaparsec as MP
+import System.FilePath
+import System.Directory
+
+import What4.ProgramLoc (Position(SourcePos), Posd(..))
+
+main :: IO ()
+main = do wd <- getCurrentDirectory
+          putStrLn $ "Looking for tests in " ++ wd
+          parseTests <- findTests "Parsing round-trips" "test-data" testParser
+          let allTests = testGroup "Tests" [syntaxParsing, parseTests]
+          defaultMain allTests
+
+findTests :: String -> FilePath -> (FilePath -> FilePath -> IO ()) -> IO TestTree
+findTests group_name test_dir test_action =
+  do inputs <- findByExtension [".cbl"] test_dir
+     return $ testGroup group_name
+       [ goldenFileTestCase input test_action
+       | input <- List.sort inputs
+       ]
+
+goldenFileTestCase :: FilePath -> (FilePath -> FilePath -> IO ()) -> TestTree
+goldenFileTestCase input test_action =
+  goldenVsFileDiff
+   (takeBaseName input) -- test name
+   (\x y -> ["diff", "-u", x, y])
+   goodFile -- golden file path
+   outFile
+   (test_action input outFile) -- action whose result is tested
+  where
+    outFile = replaceExtension input ".out"
+    goodFile = replaceExtension input ".out.good"
+
+testParser :: FilePath -> FilePath -> IO ()
+testParser inFile outFile =
+  do contents <- T.readFile inFile
+     let ?parserHooks = defaultParserHooks
+     withFile outFile WriteMode $ doParseCheck inFile contents True
+
+data Lam = Lam [Text] (Datum TrivialAtom) deriving (Eq, Show)
+
+syntaxParsing :: TestTree
+syntaxParsing =
+  let
+    anyUnit :: SyntaxParse TrivialAtom ()
+    anyUnit = anything *> pure ()
+    vars :: SyntaxParse TrivialAtom [TrivialAtom]
+    vars = describe "sequence of variable bindings" $ rep atomic
+    distinctVars :: SyntaxParse TrivialAtom [TrivialAtom]
+    distinctVars = sideCondition' "sequence of distinct variable bindings" (\xs -> List.nub xs == xs) vars
+    lambda =
+      fmap (\(_, (xs, (body, ()))) -> Lam [x | TrivialAtom x <- xs] (syntaxToDatum body))
+      (cons (atom "lambda") $
+       cons distinctVars $
+       cons anything $ emptyList)
+  in testGroup "Syntax parsing lib"
+       [ testCase "Empty list is empty list" $
+         do x <- syntaxTest "()" emptyList
+            x @?= Right ()
+       , testCase "Empty list is not atom" $
+         do x <- syntaxTest "()" (atom ("foo" :: TrivialAtom))
+            x @?= Left
+             (SyntaxError $ pure $
+               Reason { expr = Syntax {unSyntax = Posd {pos = fakeFilePos 1 1, pos_val = List []}}
+                        , message = "foo"
+                        })
+       , testCase "Atom is not empty list" $
+          do x <- syntaxTest "foo" emptyList
+             x @?= Left
+               (SyntaxError $ pure $
+                 Reason { expr = Syntax {unSyntax = Posd {pos = fakeFilePos 1 1, pos_val = Atom (TrivialAtom "foo")}}
+                          , message = "empty expression ()"
+                          })
+       , testCase "Three element list of whatever" $
+         do x <- syntaxTest "(delicious avocado toast)" (list [anyUnit, anyUnit, anyUnit])
+            x @?= Right [(), (), ()]
+       , testCase "Three element list of whatever, again" $
+         do x <- syntaxTest "(delicious (avocado and tomato) toast)" (list [anyUnit, anyUnit, anyUnit])
+            x @?= Right [(), (), ()]
+       , testCase "Three element list of atoms" $
+         do x <- syntaxTest "(delicious avocado toast)" (list [atomic, atomic, atomic])
+            x @?= Right [TrivialAtom "delicious", TrivialAtom "avocado", TrivialAtom "toast"]
+       , testCase "Three element list of non-atoms isn't atoms" $
+         do x <- syntaxTest "((delicious) avocado toast)" (list [atomic, atomic, atomic])
+            x @?= Left
+               (SyntaxError $ pure $
+                 Reason { expr =
+                            Syntax $
+                            Posd { pos = fakeFilePos 1 2
+                                 , pos_val =
+                                     List [ Syntax (Posd (fakeFilePos 1 3)
+                                                     (Atom (TrivialAtom "delicious")))
+                                          ]
+                                 }
+                        , message = "an atom"
+                        })
+       , testCase "Three element list of non-atoms still isn't atoms" $
+         do x <- syntaxTest "(delicious (avocado) toast)" (list [atomic, atomic, atomic])
+            x @?= Left
+               (SyntaxError $ pure $
+                 Reason { expr =
+                            Syntax $
+                              Posd { pos = fakeFilePos 1 12
+                                   , pos_val =
+                                       List [ Syntax (Posd (fakeFilePos 1 13)
+                                                        (Atom (TrivialAtom "avocado")))
+                                            ]
+                                   }
+                          , message = "an atom"
+                          })
+       , testCase "Many three-element lists of whatever (1)" $
+         do x <- syntaxTest "((delicious avocado toast))" (rep $ list [anything, anything, anything] *> pure ())
+            x @?= Right [()]
+       , testCase "Many three-element lists of whatever (0)" $
+         do x <- syntaxTest "()" (rep $ list [anything, anything, anything] *> pure ())
+            x @?= Right []
+       , testCase "Many three-element lists of whatever (4)" $
+         do x <- syntaxTest "((programming is fun) (a b c) (x y z) (hello (more stuff) fits))" (rep $ list [anything, anything, anything] *> pure ())
+            x @?= Right [(), (), (), ()]
+       , testCase "Many three-element lists of whatever failing on third sublist" $
+         do x <- syntaxTest "((programming is fun) (a b c) (x y) (hello (more stuff) fits))" (rep $ list [anything, anything, anything] *> pure ())
+            x @?= Left
+               (SyntaxError $ pure $
+                Reason { expr = Syntax (Posd (fakeFilePos 1 31)
+                                         (List [ Syntax (Posd (fakeFilePos 1 32)
+                                                          (Atom (TrivialAtom "x")))
+                                               , Syntax (Posd (fakeFilePos 1 34)
+                                                          (Atom (TrivialAtom "y")))]))
+                       , message = "3 expressions"
+                       })
+       , testCase "Realistic example 1" $
+         do x <- syntaxTest "(lambda (x y z) y)" lambda
+            x @?= Right (Lam ["x", "y", "z"] (Datum (Atom "y")))
+       , testCase "Realistic example 2" $
+         do x <- syntaxTest "(lambda (x y (z)) y)" lambda
+            x @?= Left
+                (SyntaxError $ pure $
+                 Reason { expr = Syntax (Posd (fakeFilePos 1 14)
+                                            (List [Syntax {unSyntax = Posd {pos = fakeFilePos 1 15, pos_val = Atom (TrivialAtom "z")}}]))
+                          , message = "an atom"
+                          })
+       , testCase "Realistic example 3" $
+         do x <- syntaxTest "(lambda x x)" lambda
+            x @?= Left
+                (SyntaxError $ pure $
+                 Reason { expr = Syntax (Posd (fakeFilePos 1 9)
+                                            (Atom "x"))
+                          , message = "sequence of variable bindings"
+                          })
+       , testCase "Realistic example 4" $
+         do x <- syntaxTest "(lambda (x y x) y)" lambda
+            x @?= Left
+                (SyntaxError $ pure $
+                 Reason { expr =
+                            Syntax (Posd (fakeFilePos 1 9)
+                                     (List [ Syntax {unSyntax = Posd {pos = fakeFilePos 1 10, pos_val = Atom (TrivialAtom "x")}}
+                                           , Syntax {unSyntax = Posd {pos = fakeFilePos 1 12, pos_val = Atom (TrivialAtom "y")}}
+                                           , Syntax {unSyntax = Posd {pos = fakeFilePos 1 14, pos_val = Atom (TrivialAtom "x")}}
+                                           ]))
+                          , message = "sequence of distinct variable bindings"
+                          })
+       ]
+
+fakeFile :: Text
+fakeFile = "test input"
+
+fakeFilePos :: Int -> Int -> Position
+fakeFilePos = SourcePos fakeFile
+
+syntaxTest :: Text -> SyntaxParse TrivialAtom a -> IO (Either (SyntaxError TrivialAtom) a)
+syntaxTest txt p =
+  case MP.parse (skipWhitespace *> sexp (TrivialAtom <$> identifier) <* MP.eof) (T.unpack fakeFile) txt of
+     Left err -> error $ "Reader error: " ++ MP.errorBundlePretty err
+     Right sexpr -> syntaxParseIO p sexpr
+