Migrate to `Felix` namespaceHEADhotg

11 files changed, 6215 insertions, 0 deletions

diff --git a/source/Felix/Syntax/Abstract.hs b/source/Felix/Syntax/Abstract.hs
new file mode 100644
index 0000000..b18612a
--- /dev/null
+++ b/source/Felix/Syntax/Abstract.hs
@@ -0,0 +1,863 @@
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE OverloadedRecordDot #-}
+{-# LANGUAGE DuplicateRecordFields #-}
+
+-- | Data types for the abstract syntax tree and helper functions
+-- for constructing the lexicon.
+--
+module Felix.Syntax.Abstract
+    ( module Felix.Syntax.Abstract
+    , module Felix.Syntax.LexicalPhrase
+    , module Felix.Syntax.Token
+    ) where
+
+
+import Base
+import Felix.Syntax.LexicalPhrase (LexicalPhrase, SgPl(..), unsafeReadPhraseSgPl, unsafeReadPhrase)
+import Felix.Syntax.Token (Token(..), Located(..))
+import Felix.Report.Location
+
+import Control.DeepSeq (NFData)
+import Text.Earley.Mixfix (Holey)
+import Data.Text qualified as Text
+import Numeric.Natural (Natural)
+
+-- | Local "variable-like" symbols that can be captured by binders.
+data VarSymbol
+    = NamedVarAt Location Text -- ^ A named variable.
+    | FreshVarAt Location Int -- ^ A nameless (implicit) variable. Should only come from desugaring.
+    deriving (Generic, NFData)
+
+pattern NamedVar :: Text -> VarSymbol
+pattern NamedVar x <- NamedVarAt _ x where
+    NamedVar x = NamedVarAt Nowhere x
+
+pattern FreshVar :: Int -> VarSymbol
+pattern FreshVar n <- FreshVarAt _ n where
+    FreshVar n = FreshVarAt Nowhere n
+
+{-# COMPLETE NamedVarAt, FreshVarAt #-}
+{-# COMPLETE NamedVar, FreshVar #-}
+
+instance Show VarSymbol where
+    showsPrec d = \case
+        NamedVarAt _ x ->
+            showParen (d > 10) (showString "NamedVar " . showsPrec 11 x)
+        FreshVarAt _ n ->
+            showParen (d > 10) (showString "FreshVar " . showsPrec 11 n)
+
+instance Eq VarSymbol where
+    NamedVarAt _ x == NamedVarAt _ y = x == y
+    FreshVarAt _ n == FreshVarAt _ m = n == m
+    _ == _ = False
+
+instance Ord VarSymbol where
+    compare (NamedVarAt _ x) (NamedVarAt _ y) = compare x y
+    compare NamedVarAt{} FreshVarAt{} = LT
+    compare FreshVarAt{} NamedVarAt{} = GT
+    compare (FreshVarAt _ n) (FreshVarAt _ m) = compare n m
+
+instance Hashable VarSymbol where
+    hashWithSalt s = \case
+        NamedVarAt _ x -> hashWithSalt s (0 :: Int, x)
+        FreshVarAt _ n -> hashWithSalt s (1 :: Int, n)
+
+instance IsString VarSymbol where
+    fromString v = NamedVar $ Text.pack v
+
+instance Locatable VarSymbol where
+    locate = \case
+        NamedVarAt l _ -> l
+        FreshVarAt l _ -> l
+
+data Expr
+    = ExprVar VarSymbol
+    | ExprInteger Location Int
+    | ExprOp Location MixfixItem [Expr]
+    | ExprStructOp Location StructSymbol (Maybe Expr)
+    | ExprFiniteSet Location (NonEmpty Expr)
+    | ExprSep Location VarSymbol Expr Stmt
+    -- ^ Of the form /@{x ∈ X | P(x)}@/.
+    | ExprReplace Location Expr (NonEmpty (VarSymbol,Expr)) (Maybe Stmt)
+    -- ^ E.g.: /@{ f(x, y) | x ∈ X, y ∈ Y | P(x, y) }@/.
+    | ExprReplacePred Location VarSymbol VarSymbol Expr Stmt
+    -- ^ E.g.: /@{ y | \\exists x\\in X. P(x, y) }@/.
+    deriving (Show, Eq, Ord, Generic, NFData)
+
+instance Locatable Expr where
+    locate = \case
+        ExprVar x -> locate x
+        ExprInteger l _ -> l
+        ExprOp l _ _ -> l
+        ExprStructOp l _ _ -> l
+        ExprFiniteSet l _ -> l
+        ExprSep l _ _ _ -> l
+        ExprReplace l _ _ _ -> l
+        ExprReplacePred l _ _ _ _ -> l
+
+
+data LexicalItem = LexicalItem Pattern Marker deriving (Show, Generic, NFData)
+
+instance Eq LexicalItem where
+    LexicalItem p _ == LexicalItem p' _ = p == p'
+
+instance Ord LexicalItem where
+    compare (LexicalItem p _) (LexicalItem p' _) = compare p p'
+
+instance Hashable LexicalItem where
+    hashWithSalt s (LexicalItem p _) = hashWithSalt s p
+
+data LexicalItemSgPl = LexicalItemSgPl (SgPl Pattern) Marker deriving (Show, Generic, NFData)
+
+instance Eq LexicalItemSgPl where
+    LexicalItemSgPl p _ == LexicalItemSgPl p' _ = sg p == sg p'
+
+instance Ord LexicalItemSgPl where
+    compare (LexicalItemSgPl p _) (LexicalItemSgPl p' _) = compare (sg p) (sg p')
+
+instance Hashable LexicalItemSgPl where
+    hashWithSalt s (LexicalItemSgPl p _) = hashWithSalt s (sg p)
+
+data Associativity
+  = LeftAssoc
+  | NonAssoc
+  | RightAssoc
+  deriving (Eq, Show, Ord, Generic, Hashable, NFData)
+
+data MixfixItem = MixfixItem Pattern Marker Associativity deriving (Eq, Show, Ord, Generic, Hashable, NFData)
+
+data Pattern = End | HoleCons Pattern | TokenCons Token Pattern deriving (Eq, Show, Ord, Generic, Hashable, NFData)
+
+type FunctionSymbol = MixfixItem
+
+newtype ParameterArity = ParameterArity Natural
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving newtype (Hashable, NFData)
+
+zeroParameterArity :: ParameterArity
+zeroParameterArity = ParameterArity 0
+
+parameterArityOf :: Foldable f => f a -> ParameterArity
+parameterArityOf = ParameterArity . fromIntegral . length
+
+parameterArityValue :: ParameterArity -> Natural
+parameterArityValue (ParameterArity arity) = arity
+
+data RelationSymbol
+    = RelationSymbol Token ParameterArity Marker
+    deriving (Show, Eq, Ord, Generic, Hashable, NFData)
+
+newtype StructSymbol = StructSymbol { unStructSymbol :: Text }
+    deriving newtype (Show, Eq, Ord, Hashable, NFData)
+
+pattern ElementSymbol, NotElementSymbol :: RelationSymbol
+pattern ElementSymbol =
+    RelationSymbol (Command "in") (ParameterArity 0) "elem"
+pattern NotElementSymbol =
+    RelationSymbol (Command "notin") (ParameterArity 0) "notelem"
+
+pattern EqSymbol, NeqSymbol, SubseteqSymbol :: RelationSymbol
+pattern EqSymbol =
+    RelationSymbol (Symbol "=") (ParameterArity 0) "eq"
+pattern NeqSymbol =
+    RelationSymbol (Command "neq") (ParameterArity 0) "neq"
+pattern SubseteqSymbol =
+    RelationSymbol (Command "subseteq") (ParameterArity 0) "subseteq"
+
+-- | The ordinary source-level @cons@ function symbol.
+--
+-- Finite-set notation is intrinsic and does not desugar through this symbol.
+pattern ConsSymbol :: FunctionSymbol
+pattern ConsSymbol =
+    MixfixItem
+        (TokenCons (Command "cons")
+            (TokenCons InvisibleBraceL
+                (HoleCons
+                    (TokenCons InvisibleBraceR
+                        (TokenCons InvisibleBraceL
+                            (HoleCons
+                                (TokenCons InvisibleBraceR End)))))))
+        "cons"
+        NonAssoc
+
+-- | The predefined @pair@ function symbol used for desugaring tuple notation..
+pattern PairSymbol :: FunctionSymbol
+pattern PairSymbol =
+    MixfixItem
+        (TokenCons (Command "pair")
+            (TokenCons InvisibleBraceL
+                (HoleCons
+                    (TokenCons InvisibleBraceR
+                        (TokenCons InvisibleBraceL
+                            (HoleCons
+                                (TokenCons InvisibleBraceR End)))))))
+        "pair"
+        NonAssoc
+
+-- | The concrete binary-tuple surface recognized by the dedicated tuple
+-- grammar. It lowers to 'PairSymbol'.
+tupleSurfacePattern :: Pattern
+tupleSurfacePattern =
+    TokenCons ParenL
+        (HoleCons
+            (TokenCons (Symbol ",")
+                (HoleCons
+                    (TokenCons ParenR End))))
+
+-- | The predefined unordered-pair function symbol.
+pattern UpairSymbol :: FunctionSymbol
+pattern UpairSymbol =
+    MixfixItem
+        (TokenCons (Command "upair")
+            (TokenCons InvisibleBraceL
+                (HoleCons
+                    (TokenCons InvisibleBraceR
+                        (TokenCons InvisibleBraceL
+                            (HoleCons
+                                (TokenCons InvisibleBraceR End)))))))
+        "upair"
+        NonAssoc
+
+-- | The fixed family-union function symbol.
+pattern UnionsSymbol :: FunctionSymbol
+pattern UnionsSymbol =
+    MixfixItem
+        (TokenCons (Command "unions")
+            (TokenCons InvisibleBraceL
+                (HoleCons
+                    (TokenCons InvisibleBraceR End))))
+        "unions"
+        NonAssoc
+
+-- | Function application /@f(x)@/ desugars to /@\apply{f}{x}@/.
+pattern ApplySymbol :: FunctionSymbol
+pattern ApplySymbol =
+    MixfixItem
+        (TokenCons (Command "apply")
+            (TokenCons InvisibleBraceL
+                (HoleCons
+                    (TokenCons InvisibleBraceR
+                        (TokenCons InvisibleBraceL
+                            (HoleCons
+                                (TokenCons InvisibleBraceR End)))))))
+        "apply"
+        NonAssoc
+
+pattern DomSymbol :: FunctionSymbol
+pattern DomSymbol =
+    MixfixItem
+        (TokenCons (Command "dom")
+            (TokenCons InvisibleBraceL
+                (HoleCons
+                    (TokenCons InvisibleBraceR End))))
+        "dom"
+        NonAssoc
+
+pattern CarrierSymbol :: StructSymbol
+pattern CarrierSymbol = StructSymbol "carrier"
+
+patternFromHoley :: Holey Token -> Pattern
+patternFromHoley = foldr step End
+    where
+        step = \case
+            Nothing -> HoleCons
+            Just tok -> TokenCons tok
+
+patternToHoley :: Pattern -> Holey Token
+patternToHoley = \case
+    End -> []
+    HoleCons pat -> Nothing : patternToHoley pat
+    TokenCons tok pat -> Just tok : patternToHoley pat
+
+mixfixPattern :: MixfixItem -> Pattern
+mixfixPattern (MixfixItem pat _ _) = pat
+
+mixfixMarker :: MixfixItem -> Marker
+mixfixMarker (MixfixItem _ m _) = m
+
+mixfixAssoc :: MixfixItem -> Associativity
+mixfixAssoc (MixfixItem _ _ assoc) = assoc
+
+mkMixfixItem :: Holey Token -> Marker -> Associativity -> MixfixItem
+mkMixfixItem pat m assoc = MixfixItem (patternFromHoley pat) m assoc
+
+lexicalItemPattern :: LexicalItem -> Pattern
+lexicalItemPattern (LexicalItem pat _) = pat
+
+lexicalItemMarker :: LexicalItem -> Marker
+lexicalItemMarker (LexicalItem _ m) = m
+
+lexicalItemPhrase :: LexicalItem -> LexicalPhrase
+lexicalItemPhrase = patternToHoley . lexicalItemPattern
+
+lexicalItemSgPlPattern :: LexicalItemSgPl -> SgPl Pattern
+lexicalItemSgPlPattern (LexicalItemSgPl pat _) = pat
+
+lexicalItemSgPlMarker :: LexicalItemSgPl -> Marker
+lexicalItemSgPlMarker (LexicalItemSgPl _ m) = m
+
+lexicalItemSgPlPhrase :: LexicalItemSgPl -> SgPl LexicalPhrase
+lexicalItemSgPlPhrase = fmap patternToHoley . lexicalItemSgPlPattern
+
+mkLexicalItem :: LexicalPhrase -> Marker -> LexicalItem
+mkLexicalItem pat m = LexicalItem (patternFromHoley pat) m
+
+mkLexicalItemSgPl :: SgPl LexicalPhrase -> Marker -> LexicalItemSgPl
+mkLexicalItemSgPl pat m = LexicalItemSgPl (patternFromHoley <$> pat) m
+
+relationSymbolToken :: RelationSymbol -> Token
+relationSymbolToken (RelationSymbol tok _ _) = tok
+
+relationSymbolParameterArity :: RelationSymbol -> ParameterArity
+relationSymbolParameterArity (RelationSymbol _ arity _) = arity
+
+relationSymbolMarker :: RelationSymbol -> Marker
+relationSymbolMarker (RelationSymbol _ _ m) = m
+
+relationSymbolPattern :: RelationSymbol -> Pattern
+relationSymbolPattern rel =
+    HoleCons (TokenCons (relationSymbolToken rel) (HoleCons End))
+
+structSymbolPattern :: StructSymbol -> Pattern
+structSymbolPattern (StructSymbol c) = TokenCons (Command c) End
+
+patternToken :: Pattern -> Maybe Token
+patternToken = \case
+    TokenCons tok End -> Just tok
+    _ -> Nothing
+
+markerFromToken :: Token -> Marker
+markerFromToken = \case
+    Word w -> Marker w
+    Symbol s -> Marker s
+    Command c -> Marker c
+    Integer n -> Marker (Text.pack (show n))
+    tok -> error ("markerFromToken: unsupported token " <> show tok)
+
+pattern ExprConst :: Location -> Token -> Expr
+pattern ExprConst l c <- ExprOp l (MixfixItem (TokenCons c End) _ NonAssoc) []
+    where
+        ExprConst l c = ExprOp l (MixfixItem (TokenCons c End) (markerFromToken c) NonAssoc) []
+
+pattern ExprApp :: Location -> Expr -> Expr -> Expr
+pattern ExprApp loc e1 e2 = ExprOp loc ApplySymbol [e1, e2]
+
+pattern ExprPair :: Location -> Expr -> Expr -> Expr
+pattern ExprPair loc e1 e2 = ExprOp loc PairSymbol [e1, e2]
+
+-- | Tuples are interpreted as nested pairs:
+-- the triple /@(a, b, c)@/ is interpreted as
+-- /@(a, (b, c))@/.
+-- This means that the product operation should also
+-- be right associative, so that /@(a, b, c)@/ can
+-- form elements of /@A\times B\times C@/.
+makeTuple :: Location -> NonEmpty Expr -> Expr
+makeTuple l = \case
+    e :| [] -> e
+    e :| (e' : es) -> ExprPair l e (makeTuple l (e' :| es))
+
+
+data Chain
+    = ChainBase (NonEmpty Expr) Sign Relation (NonEmpty Expr) -- left arguments, possibly empty list of parameters, right arguments
+    | ChainCons (NonEmpty Expr) Sign Relation Chain
+    deriving (Show, Eq, Ord, Generic, NFData)
+
+instance Locatable Chain where
+    locate (ChainBase lhs _ _ _) = locate lhs
+    locate (ChainCons lhs _ _ _) = locate lhs
+
+data Relation
+    = Relation Location RelationSymbol [Expr] -- ^  E.g.: /@x \in X@/, potentially with parameters in braces
+    | RelationExpr Location Expr   -- ^  E.g.: /@x \mathrel{R} y@/
+    deriving (Show, Eq, Ord, Generic, NFData)
+
+instance Locatable Relation where
+    locate = \case
+        Relation l _ _ -> l
+        RelationExpr l _ -> l
+
+data Sign = Positive | Negative deriving (Show, Eq, Ord, Generic, NFData)
+
+data Formula
+    = FormulaChain Chain
+    | FormulaPredicate Location PrefixPredicate Marker (NonEmpty Expr)
+    | Connected Location Connective Formula Formula
+    | FormulaNeg Location Formula
+    | FormulaQuantified Location Quantifier (NonEmpty VarSymbol) Bound Formula
+    | PropositionalConstant Location PropositionalConstant
+    deriving (Show, Eq, Ord, Generic, NFData)
+
+instance Locatable Formula where
+    locate = \case
+        FormulaChain chain -> locate chain
+        FormulaPredicate l _ _ _ -> l
+        Connected l _ _ _ -> l
+        FormulaNeg l _ -> l
+        FormulaQuantified l _ _ _ _ -> l
+        PropositionalConstant l _ -> l
+
+data PropositionalConstant = IsBottom | IsTop
+    deriving (Show, Eq, Ord, Generic, Hashable, NFData)
+
+data PrefixPredicate
+    = PrefixPredicate Text Int
+    deriving (Show, Eq, Ord, Generic, Hashable, NFData)
+
+
+data Connective
+    = Conjunction
+    | Disjunction
+    | Implication
+    | Equivalence
+    | ExclusiveOr
+    | NegatedDisjunction
+    deriving (Show, Eq, Ord, Generic, Hashable, NFData)
+
+
+
+mixfixLoc :: Locatable a => Holey (Located Token) -> [a] -> Location
+mixfixLoc parts args0 = go parts args0
+    where
+        go [] _ = Nowhere
+        go (Just ltok : _parts') _args' = startPos ltok
+        go (Nothing : parts') (a : args')
+            | locate a == Nowhere = go parts' args'
+            | otherwise = locate a
+        go (Nothing : parts') [] = go parts' []
+
+makeConnective :: Holey (Located Token) -> [Formula] -> Formula
+makeConnective parts@[Nothing, Just Located{unLocated = Command "implies"}, Nothing] [f1, f2] = Connected (mixfixLoc parts [f1, f2]) Implication  f1 f2
+makeConnective parts@[Nothing, Just Located{unLocated = Command "land"}, Nothing] [f1, f2] = Connected (mixfixLoc parts [f1, f2]) Conjunction f1 f2
+makeConnective parts@[Nothing, Just Located{unLocated = Command "lor"}, Nothing] [f1, f2] = Connected (mixfixLoc parts [f1, f2]) Disjunction f1 f2
+makeConnective parts@[Nothing, Just Located{unLocated = Command "iff"}, Nothing] [f1, f2] = Connected (mixfixLoc parts [f1, f2]) Equivalence f1 f2
+makeConnective parts@[Just Located{unLocated = Command "lnot"}, Nothing] [f1] = FormulaNeg (mixfixLoc parts [f1]) f1
+makeConnective pat _ = error ("makeConnective does not handle the following connective correctly: " <> show pat)
+
+
+
+type StructPhrase = LexicalItemSgPl
+
+-- | For example 'an integer' would be
+-- > Noun (unsafeReadPhrase "integer[/s]") []
+type Noun = NounOf Term
+data NounOf a
+    = Noun Location LexicalItemSgPl [a]
+    deriving (Show, Eq, Ord, Generic, NFData)
+
+instance Locatable (NounOf a) where
+    locate (Noun l _ _) = l
+
+
+
+
+type NounPhrase t = NounPhraseOf t Term
+-- NOTE: 'NounPhraseOf' is only used with arguments of type 'Term',
+-- but keeping the argument parameter @a@ allows the 'Show' and 'Eq'
+-- instances to remain decidable.
+data NounPhraseOf t a
+    = NounPhrase [AdjLOf a] (NounOf a) (t VarSymbol) [AdjROf a] (Maybe Stmt)
+    deriving (Generic)
+
+instance (Show a, Show (t VarSymbol)) => Show (NounPhraseOf t a) where
+    show (NounPhrase ls n vs rs ms) =
+        "NounPhrase ("
+            <> show ls <> ") ("
+            <> show n <> ") ("
+            <> show vs <> ") ("
+            <> show rs <> ") ("
+            <> show ms <> ")"
+
+instance (Eq a, Eq (t VarSymbol)) => Eq (NounPhraseOf t a) where
+    NounPhrase ls n vs rs ms == NounPhrase ls' n' vs' rs' ms' =
+        ls == ls' && n == n' && vs == vs' && rs == rs' && ms == ms'
+
+-- Raw syntax uses this lexicographic order for deterministic deduplication.
+instance (Ord a, Ord (t VarSymbol)) => Ord (NounPhraseOf t a) where
+    NounPhrase ls n vs rs ms `compare` NounPhrase ls' n' vs' rs' ms' =
+        compare
+            (ls, n, vs, rs, ms)
+            (ls', n', vs', rs', ms')
+
+instance
+    (NFData a, NFData (t VarSymbol))
+    => NFData (NounPhraseOf t a)
+
+-- | @Nameless a@ is quivalent to @Const () a@ (from "Data.Functor.Const").
+-- It describes a container that is unwilling to actually contain something.
+-- @Nameless@ lets us treat nouns with no names, one name, or many names uniformly.
+-- Thus @NounPhraseOf Nameless a@ is a noun phrase without a name and with arguments
+-- of type @a@.
+data Nameless a = Nameless deriving (Show, Eq, Ord, Generic, NFData)
+
+
+-- | Left adjectives modify nouns from the left side,
+-- e.g. /@even@/, /@continuous@/, and /@σ-finite@/.
+type AdjL = AdjLOf Term
+data AdjLOf a
+    = AdjL Location LexicalItem [a]
+    deriving (Show, Eq, Ord, Generic, NFData)
+
+instance Locatable (AdjLOf a) where
+    locate (AdjL l _ _) = l
+
+
+-- | Right attributes consist of basic right adjectives, e.g.
+-- /@divisible by ?@/, or /@of finite type@/ and verb phrases
+-- marked with /@that@/, such as /@integer that divides n@/.
+-- In some cases these right attributes may be followed
+-- by an additional such-that phrase.
+type AdjR = AdjROf Term
+data AdjROf a
+    = AdjR Location LexicalItem [a]
+    | AttrRThat VerbPhrase
+    deriving (Show, Eq, Ord, Generic, NFData)
+
+instance Locatable (AdjROf a) where
+    locate (AdjR l _ _) = l
+    locate (AttrRThat vp) = locate vp
+
+-- | Adjectives for parts of the AST where adjectives are not used
+-- to modify nouns and the L/R distinction does not matter, such as
+-- when then are used together with a copula (like /@n is even@/).
+type Adj = AdjOf Term
+data AdjOf a
+    = Adj Location LexicalItem [a]
+    deriving (Show, Eq, Ord, Generic, NFData)
+
+instance Locatable (AdjOf a) where
+    locate (Adj l _ _) = l
+
+
+type Verb = VerbOf Term
+data VerbOf a
+    = Verb Location LexicalItemSgPl [a]
+    deriving (Show, Eq, Ord, Generic, NFData)
+
+instance Locatable (VerbOf a) where
+    locate (Verb l _ _) = l
+
+
+type Fun = FunOf Term
+data FunOf a
+    = Fun {loc :: Location, phrase :: LexicalItemSgPl, funArgs :: [a]}
+    deriving (Show, Eq, Ord, Generic, NFData)
+
+instance Locatable (FunOf a) where
+    locate = (.loc)
+
+
+type VerbPhrase = VerbPhraseOf Term
+data VerbPhraseOf a
+    = VPVerb (VerbOf a)
+    | VPAdj (NonEmpty (AdjOf a)) -- ^ @x is foo@ / @x is foo and bar@
+    | VPVerbNot (VerbOf a)
+    | VPAdjNot (NonEmpty (AdjOf a)) -- ^ @x is not foo@ / @x is neither foo nor bar@
+    deriving (Show, Eq, Ord, Generic, NFData)
+
+instance Locatable (VerbPhraseOf a) where
+    locate = \case
+        VPVerb v -> locate v
+        VPAdj adjs -> locate adjs
+        VPVerbNot v -> locate v
+        VPAdjNot adjs -> locate adjs
+
+
+data Quantifier
+    = Universally
+    | Existentially
+    | Nonexistentially
+    deriving (Show, Eq, Ord, Generic, NFData)
+
+data QuantPhrase = QuantPhrase Quantifier (NounPhrase []) deriving (Show, Eq, Ord, Generic, NFData)
+
+
+data Term
+    = TermExpr Expr
+    -- ^ A symbolic expression.
+    | TermFun Fun
+    -- ^ Definite noun phrase, e.g. /@the derivative of $f$@/.
+    | TermIota Location VarSymbol Stmt
+    -- ^ Definite descriptor, e.g. /@an $x$ such that ...@//
+    | TermQuantified Quantifier Location (NounPhrase Maybe)
+    -- ^ Indefinite quantified notion, e.g. /@every even integer that divides $k$ ...@/.
+    deriving (Show, Eq, Ord, Generic, NFData)
+
+instance Locatable Term where
+    locate :: Term -> Location
+    locate (TermExpr e) = locate e
+    locate (TermFun f) = f.loc
+    locate (TermIota l _ _) = l
+    locate (TermQuantified _ l _) = l
+
+
+data Stmt
+    = StmtFormula {formula :: Formula} -- ^ E.g.: /@We have \<Formula\>@/.
+    | StmtVerbPhrase {args :: NonEmpty Term, verb :: VerbPhrase} -- ^ E.g.: /@\<Term\> and \<Term\> \<verb\>@/.
+    | StmtNoun {args :: NonEmpty Term, noun :: (NounPhrase Maybe)} -- ^ E.g.: /@\<Term\> is a(n) \<NP\>@/.
+    | StmtStruct {arg :: Term, struct :: StructPhrase}
+    | StmtNeg {loc :: Location, stmt :: Stmt} -- ^ E.g.: /@It is not the case that \<Stmt\>@/.
+    | StmtExists {loc :: Location, np :: NounPhrase []} -- ^ E.g.: /@There exists a(n) \<NP\>@/.
+    | StmtConnected {conn :: Connective, mloc :: Maybe Location, stmt1 :: Stmt, stmt2 :: Stmt}
+    | StmtQuantPhrase {loc :: Location, qp :: QuantPhrase, stmt :: Stmt}
+    | SymbolicQuantified {loc :: Location, quant :: Quantifier, vars :: NonEmpty VarSymbol, b :: Bound, suchThat :: Maybe Stmt, stmt :: Stmt}
+    deriving (Show, Eq, Ord, Generic, NFData)
+
+instance Locatable Stmt where
+    locate :: Stmt -> Location
+    locate StmtFormula{formula = phi} = locate phi
+    locate StmtConnected{mloc = Just p} = p
+    locate StmtConnected{mloc = Nothing, stmt1 = s} = locate s
+    locate StmtVerbPhrase{args = a :| _} = locate a
+    locate StmtNoun{args = a :| _} = locate a
+    locate StmtStruct{arg = a} = locate a
+    locate StmtNeg{loc = p} = p
+    locate StmtExists{loc = p} = p
+    locate StmtQuantPhrase{loc = p} = p
+    locate SymbolicQuantified{loc = p} = p
+
+data Bound = Unbounded | Bounded Location Sign Relation Expr deriving (Show, Eq, Ord, Generic, NFData)
+
+instance Locatable Bound where
+    locate = \case
+        Unbounded -> Nowhere
+        Bounded l _ _ _ -> l
+
+pattern SymbolicForall :: Location -> NonEmpty VarSymbol -> Bound -> Maybe Stmt -> Stmt -> Stmt
+pattern SymbolicForall loc vs bound suchThat have = SymbolicQuantified loc Universally vs bound suchThat have
+
+pattern SymbolicExists :: Location -> NonEmpty VarSymbol -> Bound -> Stmt -> Stmt
+pattern SymbolicExists loc vs bound suchThat = SymbolicQuantified loc Existentially vs bound Nothing suchThat
+
+makeSymbolicNotExists :: Location -> NonEmpty VarSymbol -> Bound -> Stmt -> Stmt
+makeSymbolicNotExists p vs bound st = StmtNeg p (SymbolicExists p vs bound st)
+
+data Asm
+    = AsmSuppose Stmt
+    | AsmLetNoun (NonEmpty VarSymbol) (NounPhrase Maybe) -- ^ E.g.: /@let k be an integer@/
+    | AsmLetIn (NonEmpty VarSymbol) Expr -- ^ E.g.: /@let $k\in\integers$@/
+    | AsmLetThe VarSymbol Fun -- ^ E.g.: /@let $g$ be the derivative of $f$@/
+    | AsmLetEq VarSymbol Expr -- ^ E.g.: /@let $m = n + k$@/
+    | AsmLetStruct VarSymbol StructPhrase -- ^ E.g.: /@let $A$ be a monoid@/
+    deriving (Show, Eq, Ord, Generic, NFData)
+
+data Axiom = Axiom [Asm] Stmt
+    deriving (Show, Eq, Ord, Generic, NFData)
+
+data Claim = Claim [Asm] Stmt
+    deriving (Show, Eq, Ord, Generic, NFData)
+
+-- | The head of the definition describes the part before the /@iff@/,
+-- i.e. the definiendum. An optional noun-phrase corresponds to an optional
+-- type annotation for the 'Term' of the head. The last part of the head
+-- is the lexical phrase that is defined.
+--
+-- > "A natural number   $n$        divides $m$   iff   ..."
+-- >  ^^^^^^^^^^^^^^^^   ^^^        ^^^^^^^^^^^         ^^^
+-- >  type annotation    variable   verb                definiens
+-- >  (a noun phrase)               (all args are vars) (a statement)
+--
+data DefnHead
+    = DefnAdj (Maybe (NounPhrase Maybe)) VarSymbol (AdjOf VarSymbol)
+    | DefnVerb (Maybe (NounPhrase Maybe)) VarSymbol (VerbOf VarSymbol)
+    | DefnNoun VarSymbol (NounOf VarSymbol)
+    | DefnSymbolicPredicate PrefixPredicate Marker (NonEmpty VarSymbol)
+    | DefnRel VarSymbol RelationSymbol [VarSymbol] VarSymbol
+    -- ^ E.g.: /@$x \subseteq y$ iff [...@/
+    deriving (Show, Eq, Ord, Generic, NFData)
+
+data Defn
+    = Defn [Asm] DefnHead Stmt
+    | DefnFun [Asm] (FunOf VarSymbol) (Maybe Term) Term
+    -- ^ A 'DefnFun' consists of the functional noun (which must start with /@the@/)
+    -- and an optional specification of a symbolic equivalent. The symbolic equivalent
+    -- does not need to have the same variables as the full functional noun pattern.
+    --
+    -- > "The tensor product of $U$ and $V$ over $K$, $U\tensor V$, is ..."
+    -- >  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^  ^^^^^^^^^^^^     ^^^
+    -- >  definiendum                                 symbolic eqv.    definiens
+    -- >  (a functional noun)                         (an exression)   (a term)
+    --
+    | DefnOp SymbolPattern Expr
+    deriving (Show, Eq, Ord, Generic, NFData)
+
+data CalcQuantifier
+    = CalcQuantifier (NonEmpty VarSymbol) Bound (Maybe Stmt)
+    deriving (Show, Eq, Ord, Generic, NFData)
+
+data Proof
+    = Omitted Location
+    | Qed (Maybe Location) Justification
+    -- ^ Ends of a proof, leaving automation to discharge the current goal using the given justification.
+    | Contradiction Location Justification
+    -- ^ Ends a proof by deriving absurdity using the given justification.
+    | ByCase Location [Case]
+    | ByContradiction Location Proof
+    | BySetInduction Location (Maybe Term) Proof
+    -- ^ ∈-induction.
+    | ByOrdInduction Location Proof
+    -- ^ Transfinite induction for ordinals.
+    | Assume Location Stmt Proof
+    | FixSymbolic Location (NonEmpty VarSymbol) Bound Proof
+    | FixSuchThat Location (NonEmpty VarSymbol) Stmt Proof
+    | Calc Location (Maybe CalcQuantifier) Calc Proof
+    -- ^ Simplify goals that are implications or disjunctions.
+    | TakeVar Location (NonEmpty VarSymbol) Bound Stmt Justification Proof
+    | TakeNoun Location (NounPhrase []) Justification Proof
+    | Have Location (Maybe Stmt) Stmt Justification Proof
+    -- ^ /@Since \<stmt\>, we have \<stmt\> by \<ref\>.@/
+    | Suffices Location Stmt Justification Proof
+    -- ^ /@It suffices to show that [...]. [...]@/
+    | Subclaim Location Stmt Proof Proof
+    -- ^ A claim is a sublemma with its own proof:
+    --  /@Show \<goal stmt\>. \<steps\>. \<continue other proof\>.@/
+    | Define Location VarSymbol Expr Proof
+    -- ^ Local definition.
+    --
+    | DefineFunction Location VarSymbol VarSymbol Expr VarSymbol Expr Proof
+    -- ^ Local function definition, e.g. /@Let $f(x) = e$ for $x\\in d$@/.
+    -- The first 'VarSymbol' is the newly defined symbol, the second one is the argument.
+    -- The first 'Expr' is the value, the final variable and expr specify a bound (the domain of the function).
+
+
+
+
+    | DefineFunctionLocal Location VarSymbol VarSymbol Expr VarSymbol VarSymbol (NonEmpty (Expr, Formula)) Proof
+    -- ^ Local function definition, but in this case we give the domain and target an the rules for $xs$ in some sub domains.
+    --
+    deriving (Show, Eq, Ord, Generic, NFData)
+
+-- | An inline justification.
+data Justification
+    = JustificationRef (NonEmpty Marker)
+    | JustificationSetExt
+    | JustificationEmpty
+    | JustificationLocal -- ^ Use only local assumptions
+    deriving (Show, Eq, Ord, Generic, NFData)
+
+
+-- | A case of a case split.
+data Case = Case
+    { caseOf :: Stmt
+    , caseProof :: Proof
+    } deriving (Show, Eq, Ord, Generic, NFData)
+
+data Calc
+    = Equation Expr (NonEmpty (Expr, Justification))
+    -- ^ A chain of equalities. Each claimed equality has a (potentially empty) justification.
+    -- For example: @a &= b \\explanation{by \\cref{a_eq_b}} &= c@
+    -- would be (modulo expr constructors)
+    -- @Equation "a" [("b", JustificationRef "a_eq_b"), ("c", JustificationEmpty)]@.
+    | Biconditionals Formula (NonEmpty (Formula, Justification))
+    deriving (Show, Eq, Ord, Generic, NFData)
+
+
+data Abbreviation
+    = AbbreviationAdj VarSymbol (AdjOf VarSymbol) Stmt
+    | AbbreviationVerb VarSymbol (VerbOf VarSymbol) Stmt
+    | AbbreviationNoun VarSymbol (NounOf VarSymbol) Stmt
+    | AbbreviationRel VarSymbol RelationSymbol [VarSymbol] VarSymbol Stmt
+    | AbbreviationFun (FunOf VarSymbol) Term
+    | AbbreviationEq SymbolPattern Expr
+    deriving (Show, Eq, Ord, Generic, NFData)
+
+data Datatype
+    = Datatype
+        { datatypeHeadExpr :: Expr
+        , datatypeClauses :: NonEmpty DatatypeClause
+        }
+    deriving (Show, Eq, Ord, Generic, NFData)
+
+data DatatypeClause = DatatypeClause
+    { datatypeClauseConstructorExpr :: Expr
+    , datatypeClauseTargetExpr :: Expr
+    , datatypeClausePremises :: [(VarSymbol, Expr)]
+    }
+    deriving (Show, Eq, Ord, Generic, NFData)
+
+data Inductive = Inductive
+    { inductiveSymbolPattern :: SymbolPattern
+    , inductiveDomain :: Expr
+    , inductiveIntros :: NonEmpty IntroRule
+    }
+    deriving (Show, Eq, Ord, Generic, NFData)
+
+data IntroRule = IntroRule
+    { introConditions :: [Formula] -- The inductively defined set may only appear as an argument of monotone operations on the rhs.
+    , introResult :: Formula -- TODO Refine.
+    }
+    deriving (Show, Eq, Ord, Generic, NFData)
+
+
+data SymbolPattern = SymbolPattern FunctionSymbol [VarSymbol]
+    deriving (Show, Eq, Ord, Generic, NFData)
+
+data Signature
+    = SignatureAdj  VarSymbol (AdjOf  VarSymbol)
+    -- The verb and noun forms are available to programmatic AST consumers but
+    -- have no concrete source syntax.
+    | SignatureVerb VarSymbol (VerbOf VarSymbol)
+    | SignatureNoun VarSymbol (NounOf VarSymbol)
+    | SignatureSymbolic SymbolPattern (NounPhrase Maybe)
+    -- ^ /@$\<symbol\>(\<vars\>)$ is a \<noun\>@/
+    deriving (Show, Eq, Ord, Generic, NFData)
+
+
+data StructDefn = StructDefn
+    { structPhrase :: StructPhrase
+    -- ^ E.g.: @partial order@ or @abelian group@.\
+    , structParents :: [StructPhrase]
+    -- ^ Structural parents
+    , structLabel :: VarSymbol
+    , structFixes :: [StructSymbol]
+    -- ^ List of text for commands representing constants not inherited from its parents,
+    -- e.g.: @\sqsubseteq@ or @\inv@.
+    , structAssumes :: [(Marker, Stmt)]
+    }
+    deriving (Show, Eq, Ord, Generic, NFData)
+
+newtype Marker = Marker Text
+    deriving stock (Show, Eq, Ord, Generic)
+
+deriving newtype instance Hashable Marker
+deriving newtype instance NFData Marker
+
+instance IsString Marker where
+    fromString str = Marker (Text.pack str)
+
+type BlockTitle = [Token]
+
+data ClaimKind
+    = Proposition
+    | Theorem
+    | Lemma
+    | Corollary
+    | PlainClaim
+    deriving (Show, Eq, Ord, Generic, NFData)
+
+data Block
+    = BlockAxiom Location (Maybe BlockTitle) Marker Axiom
+    | BlockClaim ClaimKind Location (Maybe BlockTitle) Marker Claim
+    | BlockProof Location Proof Location -- ^ Proof start and ending location.
+    | BlockDefn Location (Maybe BlockTitle) Marker Defn
+    | BlockAbbr Location (Maybe BlockTitle) Marker Abbreviation
+    | BlockData Location (Maybe BlockTitle) Marker Datatype
+    | BlockInductive Location (Maybe BlockTitle) Marker Inductive
+    | BlockSig Location (Maybe BlockTitle) Marker [Asm] Signature
+    | BlockStruct Location (Maybe BlockTitle) Marker StructDefn
+    deriving (Show, Eq, Ord, Generic, NFData)
+
+instance Locatable Block where
+    locate = \case
+        BlockAxiom location _title _marker _axiom -> location
+        BlockClaim _kind location _title _marker _claim -> location
+        BlockProof location _proof _end -> location
+        BlockDefn location _title _marker _definition -> location
+        BlockAbbr location _title _marker _abbreviation -> location
+        BlockData location _title _marker _datatype -> location
+        BlockInductive location _title _marker _inductive -> location
+        BlockSig location _title _marker _assumptions _signature -> location
+        BlockStruct location _title _marker _structure -> location
diff --git a/source/Felix/Syntax/Adapt.hs b/source/Felix/Syntax/Adapt.hs
new file mode 100644
index 0000000..eb0cb6c
--- /dev/null
+++ b/source/Felix/Syntax/Adapt.hs
@@ -0,0 +1,928 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE ApplicativeDo #-}
+{-# LANGUAGE RecordWildCards #-}
+
+module Felix.Syntax.Adapt
+    ( FunctionPatternError(..)
+    , LexicalScanError(..)
+    , ScannedLexicalItem(..)
+    , scannedItemMarker
+    , canonicalScannedItem
+    , SyntaxMaterializationError(..)
+    , materializeSyntaxDelta
+    , scanChunk
+    ) where
+
+import Base
+import Felix.Syntax.Abstract
+import Felix.Syntax.Interface
+import Felix.Syntax.Lexicon
+import Felix.Report.Location
+
+import Control.Monad (foldM)
+import Data.Bifunctor qualified as Bifunctor
+import Data.Map.Strict qualified as Map
+import Data.Maybe (catMaybes)
+import Data.Set qualified as Set
+import Data.Sequence qualified as Seq
+import Data.Text qualified as Text
+import Numeric.Natural (Natural)
+import Text.Regex.Applicative qualified as RE
+import Text.Regex.Applicative (RE)
+
+data FunctionPatternError
+    = FunctionPatternEmpty
+    | FunctionPatternBareVariable
+    | FunctionPatternReservedApplication
+    deriving (Show, Eq)
+
+data LexicalScanError
+    = MalformedLexicalEnvironment !Location !Text
+    | InvalidFunctionPattern !Location !FunctionPatternError
+    | MalformedDatatype !Location !Text
+    deriving (Eq)
+
+instance Show LexicalScanError where
+    show = \case
+        MalformedLexicalEnvironment location environment ->
+            "could not find a lexical pattern in "
+                <> Text.unpack environment
+                <> " at "
+                <> prettyLocation location
+        InvalidFunctionPattern location problem ->
+            functionPatternErrorMessage problem
+                <> " at "
+                <> prettyLocation location
+        MalformedDatatype location problem ->
+            "malformed datatype declaration at "
+                <> prettyLocation location
+                <> ": "
+                <> Text.unpack problem
+
+scanChunk
+    :: [Located Token]
+    -> Either LexicalScanError [Located ScannedLexicalItem]
+scanChunk ltoks =
+    case ltoks of
+        first@Located{startPos = pos, unLocated = BeginEnv "definition"} : _ ->
+            locateAt first
+                <$> (matchOrErr (definition pos) "definition" pos >>= id)
+        first@Located{startPos = pos, unLocated = BeginEnv "signature"} : _ ->
+            locateAt first
+                <$> (matchOrErr (signatureExtension pos) "signature" pos >>= id)
+        first@Located{startPos = pos, unLocated = BeginEnv "abbreviation"} : _ ->
+            locateAt first
+                <$> (matchOrErr (abbreviation pos) "abbreviation" pos >>= id)
+        first@Located{startPos = pos, unLocated = BeginEnv "struct"} : _ ->
+            locateStructItems first ltoks
+                <$> matchOrErr structRE "struct definition" pos
+        first@Located{startPos = pos, unLocated = BeginEnv "inductive"} : _ ->
+            locateAt first
+                <$> (matchOrErr (inductive pos) "inductive definition" pos >>= id)
+        Located{startPos = pos, unLocated = BeginEnv "datatype"} : _ ->
+            scanDatatypeChunk pos ltoks
+        _ ->
+            Right []
+  where
+    toks = unLocated <$> ltoks
+
+    matchOrErr
+        :: RE Token a
+        -> Text
+        -> Location
+        -> Either LexicalScanError a
+    matchOrErr re environment location =
+        case RE.match re toks of
+            Nothing ->
+                Left
+                    (MalformedLexicalEnvironment
+                        location
+                        environment)
+            Just result ->
+                Right result
+
+    locateAt first items =
+        [item <$ first | item <- items]
+
+data ScannedLexicalItem
+    = ScanAdj LexicalPhrase Marker
+    | ScanFun LexicalPhrase Marker
+    | ScanNoun LexicalPhrase Marker
+    | ScanStructNoun LexicalPhrase Marker
+    | ScanVerb LexicalPhrase Marker
+    | ScanRelationSymbol Token ParameterArity Marker
+    | ScanFunctionSymbol Pattern Marker
+    | ScanPrefixPredicate PrefixPredicate Marker
+    | ScanStructOp Text -- we an use the command text as export name.
+    deriving (Show, Eq, Ord)
+
+scannedItemMarker :: ScannedLexicalItem -> Marker
+scannedItemMarker = \case
+    ScanAdj _item marker ->
+        marker
+    ScanFun _item marker ->
+        marker
+    ScanNoun _item marker ->
+        marker
+    ScanStructNoun _item marker ->
+        marker
+    ScanVerb _item marker ->
+        marker
+    ScanRelationSymbol _token _arity marker ->
+        marker
+    ScanFunctionSymbol _pattern marker ->
+        marker
+    ScanPrefixPredicate _predicate marker ->
+        marker
+    ScanStructOp commandText ->
+        Marker commandText
+
+canonicalScannedItem
+    :: Fixity
+    -> ScannedLexicalItem
+    -> CanonicalLexicalEntry
+canonicalScannedItem fixity = \case
+    ScanAdj phrase marker
+        | isAdjR phrase ->
+            CanonicalRightAdjective
+                (patternFromHoley phrase)
+                marker
+        | otherwise ->
+            CanonicalLeftAdjective
+                (patternFromHoley phrase)
+                marker
+    ScanFun phrase marker ->
+        canonicalSgPl
+            CanonicalFunctionPhrase
+            (guessNounPlural phrase)
+            marker
+    ScanNoun phrase marker ->
+        canonicalSgPl
+            CanonicalNoun
+            (guessNounPlural phrase)
+            marker
+    ScanStructNoun phrase marker ->
+        canonicalSgPl
+            CanonicalStructureNoun
+            (guessNounPlural phrase)
+            marker
+    ScanVerb phrase marker ->
+        canonicalSgPl
+            CanonicalVerb
+            (guessVerbPlural phrase)
+            marker
+    ScanRelationSymbol token arity marker ->
+        CanonicalRelation token arity marker
+    ScanFunctionSymbol pat marker ->
+        CanonicalExpressionFunction
+            (if pat == tupleSurfacePattern
+                then mixfixPattern PairSymbol
+                else pat)
+            marker
+            fixity
+    ScanPrefixPredicate
+            (PrefixPredicate commandText arity)
+            marker ->
+        CanonicalPrefixPredicate
+            commandText
+            (fromIntegral arity)
+            marker
+    ScanStructOp commandText ->
+        CanonicalStructureOperation commandText
+  where
+    canonicalSgPl constructor phrases marker =
+        constructor
+            (patternFromHoley (sg phrases))
+            (patternFromHoley (pl phrases))
+            marker
+
+data SyntaxMaterializationError
+    = MaterializedSyntaxCollision !CanonicalSyntaxCollision
+    | PrefixPredicateArityOutOfRange !Natural
+    deriving (Show, Eq)
+
+materializeSyntaxDelta
+    :: CanonicalSyntaxDelta
+    -> Either SyntaxMaterializationError Lexicon
+materializeSyntaxDelta delta = do
+    combined <-
+        Bifunctor.first MaterializedSyntaxCollision
+            (canonicalSyntaxDelta
+                (fixedBaseSyntaxEntries
+                    <> canonicalSyntaxDeltaEntries delta))
+    foldM
+        insertCanonicalEntry
+        builtins
+        [ entry
+        | entry <- canonicalSyntaxDeltaEntries combined
+        , entry `Set.notMember` fixedEntries
+        ]
+  where
+    fixedEntries =
+        Set.fromList fixedBaseSyntaxEntries
+
+insertCanonicalEntry
+    :: Lexicon
+    -> CanonicalLexicalEntry
+    -> Either SyntaxMaterializationError Lexicon
+insertCanonicalEntry lexicon@Lexicon{..} entry = do
+    extended <- case entry of
+        CanonicalLeftAdjective pat marker ->
+            pure
+                lexicon
+                    { lexiconAdjLs =
+                        lexicalItem pat marker : lexiconAdjLs
+                    }
+        CanonicalRightAdjective pat marker ->
+            pure
+                lexicon
+                    { lexiconAdjRs =
+                        lexicalItem pat marker : lexiconAdjRs
+                    }
+        CanonicalFunctionPhrase singular plural marker ->
+            pure
+                lexicon
+                    { lexiconFuns =
+                        lexicalItemSgPl singular plural marker
+                            : lexiconFuns
+                    }
+        CanonicalNoun singular plural marker ->
+            pure
+                lexicon
+                    { lexiconNouns =
+                        lexicalItemSgPl singular plural marker
+                            : lexiconNouns
+                    }
+        CanonicalStructureNoun singular plural marker ->
+            pure
+                lexicon
+                    { lexiconStructNouns =
+                        lexicalItemSgPl singular plural marker
+                            : lexiconStructNouns
+                    }
+        CanonicalVerb singular plural marker ->
+            pure
+                lexicon
+                    { lexiconVerbs =
+                        lexicalItemSgPl singular plural marker
+                            : lexiconVerbs
+                    }
+        CanonicalRelation token arity marker ->
+            pure
+                lexicon
+                    { lexiconRelationSymbols =
+                        RelationSymbol token arity marker
+                            : lexiconRelationSymbols
+                    }
+        CanonicalExpressionFunction
+                pat
+                marker
+                (Fixity associativity level) ->
+            pure
+                lexicon
+                    { lexiconMixfixTable =
+                        Seq.adjust
+                            (Map.insert
+                                pat
+                                (MixfixItem
+                                    pat
+                                    marker
+                                    associativity))
+                            (fromIntegral
+                                (mixfixLevelValue level))
+                            lexiconMixfixTable
+                    }
+        CanonicalPrefixPredicate commandText arity marker -> do
+            runtimeArity <-
+                if arity <= fromIntegral (maxBound :: Int)
+                    then pure (fromIntegral arity)
+                    else
+                        Left
+                            (PrefixPredicateArityOutOfRange arity)
+            pure
+                lexicon
+                    { lexiconPrefixPredicates =
+                        (PrefixPredicate commandText runtimeArity, marker)
+                            : lexiconPrefixPredicates
+                    }
+        CanonicalStructureOperation commandText ->
+            pure
+                lexicon
+                    { lexiconStructFun =
+                        StructSymbol commandText : lexiconStructFun
+                    }
+    pure extended
+  where
+    lexicalItem pat marker =
+        mkLexicalItem (patternToHoley pat) marker
+
+    lexicalItemSgPl singular plural marker =
+        mkLexicalItemSgPl
+            (SgPl
+                (patternToHoley singular)
+                (patternToHoley plural))
+            marker
+
+skipUntilNextLexicalEnv :: RE Token [Token]
+skipUntilNextLexicalEnv = many (RE.psym otherToken)
+    where
+        otherToken tok = tok /= BeginEnv "definition" && tok /= BeginEnv "struct" && tok /= BeginEnv "abbreviation"
+
+notEndOfLexicalEnvToken :: RE Token Token
+notEndOfLexicalEnvToken = RE.psym innerToken
+    where
+        innerToken tok = tok /= EndEnv "definition" && tok /= EndEnv "struct" && tok /= EndEnv "abbreviation"
+
+notEndOfSignatureSentenceToken :: RE Token Token
+notEndOfSignatureSentenceToken = RE.psym \case
+    Symbol "." -> False
+    EndEnv "signature" -> False
+    _ -> True
+
+definition
+    :: Location
+    -> RE Token (Either LexicalScanError [ScannedLexicalItem])
+definition location = do
+    RE.sym (BeginEnv "definition")
+    RE.few notEndOfLexicalEnvToken
+    m <- labelRE
+    RE.few RE.anySym
+    lexicalItem <- headRE location
+    RE.few RE.anySym
+    RE.sym (EndEnv "definition")
+    skipUntilNextLexicalEnv
+    pure ((: []) <$> lexicalItem m)
+
+abbreviation
+    :: Location
+    -> RE Token (Either LexicalScanError [ScannedLexicalItem])
+abbreviation location = do
+    RE.sym (BeginEnv "abbreviation")
+    RE.few RE.anySym
+    m <- labelRE
+    RE.few RE.anySym
+    lexicalItem <- headRE location
+    RE.few RE.anySym
+    RE.sym (EndEnv "abbreviation")
+    skipUntilNextLexicalEnv
+    pure ((: []) <$> lexicalItem m)
+
+signatureExtension
+    :: Location
+    -> RE Token (Either LexicalScanError [ScannedLexicalItem])
+signatureExtension location = do
+    RE.sym (BeginEnv "signature")
+    RE.few notEndOfLexicalEnvToken
+    m <- labelRE
+    RE.few RE.anySym
+    lexicalItem <- sigHeadRE location
+    RE.few notEndOfSignatureSentenceToken
+    RE.sym (Symbol ".")
+    RE.sym (EndEnv "signature")
+    skipUntilNextLexicalEnv
+    pure ((: []) <$> lexicalItem m)
+
+labelRE :: RE Token Marker
+labelRE = RE.msym \case
+    Label m -> Just (Marker m)
+    _ -> Nothing
+
+-- | 'RE' that matches the head of a definition.
+headRE
+    :: Location
+    -> RE Token (Marker -> Either LexicalScanError ScannedLexicalItem)
+-- Note that @<|>@ is left biased for 'RE', so we can just
+-- place 'adj' before 'verb' and do not have to worry about
+-- overlapping patterns.
+headRE location =
+        pureScan ScanNoun <$> nounRE
+    <|> pureScan ScanAdj <$> adjRE
+    <|> pureScan ScanVerb <$> verbRE
+    <|> pureScan ScanFun <$> funRE
+    <|> relationScan <$> relationSymbolRE
+    <|> functionScan <$> functionSymbolRE location
+    <|> pureScan ScanPrefixPredicate <$> prefixPredicate
+  where
+    pureScan constructor value marker =
+        Right (constructor value marker)
+
+    relationScan (token, arity) marker =
+        Right (ScanRelationSymbol token arity marker)
+
+    functionScan patternResult marker =
+        (`ScanFunctionSymbol` marker) <$> patternResult
+
+sigHeadRE
+    :: Location
+    -> RE Token (Marker -> Either LexicalScanError ScannedLexicalItem)
+sigHeadRE location =
+    asum
+        [ signatureHeadRE form
+        | form <- concreteSignatureHeadForms
+        ]
+  where
+    signatureHeadRE = \case
+        AdjectiveSignatureHead ->
+            pureScan ScanAdj <$> sigAdjectiveRE
+        SymbolicSignatureHead ->
+            functionScan <$> sigFunctionSymbolRE location
+
+    pureScan constructor value marker =
+        Right (constructor value marker)
+
+    functionScan patternResult marker =
+        (`ScanFunctionSymbol` marker) <$> patternResult
+
+sigAdjectiveRE :: RE Token LexicalPhrase
+sigAdjectiveRE =
+    toLexicalPhrase
+        <$> ( math var
+                *> RE.sym (Word "can")
+                *> RE.sym (Word "be")
+                *> RE.some
+                    (RE.psym isLexicalPhraseToken <|> math var)
+            )
+
+sigFunctionSymbolRE :: Location -> RE Token (Either LexicalScanError Pattern)
+sigFunctionSymbolRE location = do
+    RE.sym (BeginEnv "math")
+    toks <- RE.few nonDefinitionKeyword
+    RE.sym (EndEnv "math")
+    pure (makeFunctionSymbol location toks)
+
+inductive
+    :: Location
+    -> RE Token (Either LexicalScanError [ScannedLexicalItem])
+inductive location = do
+    RE.sym (BeginEnv "inductive")
+    RE.few notEndOfLexicalEnvToken
+    m <- labelRE
+    RE.few RE.anySym
+    lexicalItem <- functionSymbolInductive location
+    RE.few RE.anySym
+    RE.sym (EndEnv "inductive")
+    skipUntilNextLexicalEnv
+    pure (((: []) . (`ScanFunctionSymbol` m)) <$> lexicalItem)
+
+scanDatatypeChunk
+    :: Location
+    -> [Located Token]
+    -> Either LexicalScanError [Located ScannedLexicalItem]
+scanDatatypeChunk = datatypeLexicalItems
+
+datatypeLexicalItems
+    :: Location
+    -> [Located Token]
+    -> Either LexicalScanError [Located ScannedLexicalItem]
+datatypeLexicalItems environmentLocation toks = do
+    marker <- requireDatatype
+        environmentLocation
+        "missing declaration label"
+        (findDatatypeLabel toks)
+    datatypeHeadToks <- requireDatatype
+        environmentLocation
+        "missing datatype head"
+        (findDatatypeHead toks)
+    constructorToks <- requireDatatype
+        environmentLocation
+        "missing constructor enumeration"
+        (findDatatypeConstructors toks)
+    let datatypeLocation =
+            maybe environmentLocation startPos (listToMaybe datatypeHeadToks)
+    datatypePattern <- makeFunctionSymbol
+        datatypeLocation
+        (unLocated <$> datatypeHeadToks)
+    constructorItems <- traverse makeConstructor constructorToks
+    pure
+        ((ScanFunctionSymbol datatypePattern marker
+            <$ locationTemplate datatypeLocation toks)
+            : constructorItems)
+  where
+    makeConstructor (itemLocation, raw) = do
+        constructorToks <- requireDatatype
+            itemLocation
+            "constructor item has no symbolic declaration"
+            (itemConstructorToks raw)
+        let stripped = stripOuterParens constructorToks
+        markerToken <- constructorMarker itemLocation stripped
+        constructorPattern <- makeFunctionSymbol
+            (startPos markerToken)
+            (unLocated <$> stripped)
+        pure
+            (ScanFunctionSymbol
+                constructorPattern
+                (markerFromToken (unLocated markerToken))
+                <$ markerToken)
+
+requireDatatype
+    :: Location
+    -> Text
+    -> Maybe a
+    -> Either LexicalScanError a
+requireDatatype location problem =
+    maybe (Left (MalformedDatatype location problem)) Right
+
+locationTemplate :: Location -> [Located Token] -> Located Token
+locationTemplate location = \case
+    token : _ ->
+        token{startPos = location}
+    [] ->
+        impossible "datatype scanner has no environment token"
+
+findDatatypeLabel :: [Located Token] -> Maybe Marker
+findDatatypeLabel = \case
+    [] -> Nothing
+    Located{unLocated = Label m} : _ -> Just (Marker m)
+    _ : toks -> findDatatypeLabel toks
+
+findDatatypeHead :: [Located Token] -> Maybe [Located Token]
+findDatatypeHead toks = do
+    afterLabel <- tailMay =<< dropUntil (isLabel . unLocated) toks
+    defineToks <- dropUntil ((== Word "define") . unLocated) afterLabel
+    case defineToks of
+        _define : Located{unLocated = BeginEnv "math"} : rest ->
+            takeUntilToken (EndEnv "math") rest
+        _ -> Nothing
+
+findDatatypeConstructors
+    :: [Located Token]
+    -> Maybe [(Location, [Located Token])]
+findDatatypeConstructors toks = do
+    afterEnumerate <- tailMay
+        =<< dropUntil ((== BeginEnv "enumerate") . unLocated) toks
+    enumerateBody <- takeUntilToken (EndEnv "enumerate") afterEnumerate
+    let items = splitDatatypeItems enumerateBody
+    guard (not (null items))
+    pure items
+
+splitDatatypeItems
+    :: [Located Token]
+    -> [(Location, [Located Token])]
+splitDatatypeItems = \case
+    [] ->
+        []
+    Located{startPos = itemLocation, unLocated = Command "item"} : rest ->
+        let (item, remaining) =
+                break ((== Command "item") . unLocated) rest
+        in (itemLocation, item) : splitDatatypeItems remaining
+    _ : rest ->
+        splitDatatypeItems rest
+
+itemConstructorToks :: [Located Token] -> Maybe [Located Token]
+itemConstructorToks toks = do
+    afterMath <- tailMay =<< dropUntil ((== BeginEnv "math") . unLocated) toks
+    mathBody <- takeUntilToken (EndEnv "math") afterMath
+    takeUntilToken (Command "in") mathBody
+
+constructorMarker
+    :: Location
+    -> [Located Token]
+    -> Either LexicalScanError (Located Token)
+constructorMarker fallback =
+    maybe
+        (Left
+            (MalformedDatatype
+                fallback
+                "constructor has no marker-bearing head token"))
+        Right
+        . find (isConstructorMarkerToken . unLocated)
+
+isConstructorMarkerToken :: Token -> Bool
+isConstructorMarkerToken = \case
+    Word _ -> True
+    Symbol _ -> True
+    Command _ -> True
+    Integer _ -> True
+    _ -> False
+
+stripOuterParens :: [Located Token] -> [Located Token]
+stripOuterParens toks
+    | hasOuterParens toks = case toks of
+        Located{unLocated = ParenL} : rest -> case reverse rest of
+            Located{unLocated = ParenR} : innerRev -> reverse innerRev
+            _ -> toks
+        _ -> toks
+    | otherwise = toks
+
+hasOuterParens :: [Located Token] -> Bool
+hasOuterParens = \case
+    Located{unLocated = ParenL} : rest -> go (1 :: Int) rest
+    _ -> False
+    where
+        go _ [] = False
+        go depth [Located{unLocated = ParenR}] = depth == 1
+        go depth (Located{unLocated = ParenL} : rest) =
+            go (depth + 1) rest
+        go depth (Located{unLocated = ParenR} : rest)
+            | depth <= 0 = False
+            | otherwise = go (depth - 1) rest
+        go depth (_ : rest) = go depth rest
+
+isLabel :: Token -> Bool
+isLabel = \case
+    Label _ -> True
+    _ -> False
+
+dropUntil :: (a -> Bool) -> [a] -> Maybe [a]
+dropUntil predicate = \case
+    [] -> Nothing
+    xs@(x : rest)
+        | predicate x -> Just xs
+        | otherwise -> dropUntil predicate rest
+
+takeUntilToken :: Token -> [Located Token] -> Maybe [Located Token]
+takeUntilToken stop = \case
+    [] -> Nothing
+    x : xs
+        | unLocated x == stop -> Just []
+        | otherwise -> (x :) <$> takeUntilToken stop xs
+
+tailMay :: [a] -> Maybe [a]
+tailMay = \case
+    [] -> Nothing
+    _ : xs -> Just xs
+
+structRE :: RE Token [ScannedLexicalItem]
+structRE = do
+    RE.sym (BeginEnv "struct")
+    RE.few RE.anySym
+    m <- labelRE
+    RE.few RE.anySym
+    lexicalItem <- ScanStructNoun . toLexicalPhrase <$> (an *> structPat <* math var)
+    RE.few RE.anySym
+    lexicalItems <- structOps <|> pure []
+    RE.sym (EndEnv "struct")
+    skipUntilNextLexicalEnv
+    pure (lexicalItem m : lexicalItems)
+
+structOps :: RE Token [ScannedLexicalItem]
+structOps = do
+    RE.sym (BeginEnv "enumerate")
+    lexicalItems <- many structOp
+    RE.sym (EndEnv "enumerate")
+    RE.few RE.anySym
+    pure lexicalItems
+
+structOp :: RE Token ScannedLexicalItem
+structOp = do
+    RE.sym (Command "item")
+    op <- math command
+    pure (ScanStructOp op)
+
+locateStructItems
+    :: Located Token
+    -> [Located Token]
+    -> [ScannedLexicalItem]
+    -> [Located ScannedLexicalItem]
+locateStructItems environmentToken toks = \case
+    [] ->
+        []
+    structureNoun : operations ->
+        (structureNoun <$ environmentToken)
+            : zipWith locateOperation operations operationTokens
+  where
+    operationTokens =
+        structOperationTokens toks
+            <> repeat environmentToken
+
+    locateOperation operation token =
+        operation <$ token
+
+structOperationTokens :: [Located Token] -> [Located Token]
+structOperationTokens = \case
+    Located{unLocated = Command "item"}
+        : Located{unLocated = BeginEnv "math"}
+        : commandToken@Located{unLocated = Command _}
+        : Located{unLocated = EndEnv "math"}
+        : rest ->
+            commandToken : structOperationTokens rest
+    _ : rest ->
+        structOperationTokens rest
+    [] ->
+        []
+
+nounRE :: RE Token LexicalPhrase
+nounRE = toLexicalPhrase <$> (math var *> is *> an *> patRE <* iff)
+
+adjRE :: RE Token LexicalPhrase
+adjRE = toLexicalPhrase <$> (math var *> is *> patRE <* iff)
+
+verbRE :: RE Token LexicalPhrase
+verbRE = toLexicalPhrase <$> (math var *> patRE <* iff)
+
+funRE :: RE Token LexicalPhrase
+funRE = toLexicalPhrase <$> (the *> patRE <* (is <|> comma))
+
+relationSymbolRE :: RE Token (Token, ParameterArity)
+relationSymbolRE = do
+    beginMath
+    var
+    rel <- symbol
+    k <- params
+    var
+    endMath
+    iff
+    pure (rel, k)
+        where
+        params :: RE Token ParameterArity
+        params = do
+            vars <- many (RE.sym InvisibleBraceL *> var <* RE.sym InvisibleBraceR)
+            pure (parameterArityOf vars)
+
+functionSymbolRE
+    :: Location
+    -> RE Token (Either LexicalScanError Pattern)
+functionSymbolRE location = do
+    RE.sym (BeginEnv "math")
+    toks <- RE.few nonDefinitionKeyword
+    RE.sym (Symbol "=")
+    pure (makeFunctionSymbol location toks)
+
+makeFunctionSymbol
+    :: Location
+    -> [Token]
+    -> Either LexicalScanError Pattern
+makeFunctionSymbol location = \case
+    [] ->
+        Left (InvalidFunctionPattern location FunctionPatternEmpty)
+    [Variable _] ->
+        Left (InvalidFunctionPattern location FunctionPatternBareVariable)
+    [Variable _, ParenL, Variable _, ParenR] ->
+        Left
+            (InvalidFunctionPattern
+                location
+                FunctionPatternReservedApplication)
+    toks ->
+        Right (patternFromHoley (fromToken <$> toks))
+    where
+        fromToken = \case
+            Variable _ -> Nothing -- Variables become slots.
+            tok -> Just tok -- Everything else is part of the pattern.
+
+functionPatternErrorMessage :: FunctionPatternError -> String
+functionPatternErrorMessage = \case
+    FunctionPatternEmpty ->
+        "malformed function pattern: no pattern"
+    FunctionPatternBareVariable ->
+        "malformed function pattern: a bare variable would cause infinite left recursion"
+    FunctionPatternReservedApplication ->
+        "malformed function pattern: _(_) is reserved for set-theoretic function application"
+
+functionSymbolInductive
+    :: Location
+    -> RE Token (Either LexicalScanError Pattern)
+functionSymbolInductive location = do
+    RE.sym (BeginEnv "math")
+    toks <- RE.few nonDefinitionKeyword
+    RE.sym (Command "subseteq")
+    pure (makeFunctionSymbol location toks)
+
+prefixPredicate :: RE Token PrefixPredicate
+prefixPredicate = math prfx <* iff
+    where
+        prfx = do
+            r <- command
+            args <- many (RE.sym InvisibleBraceL *> var <* RE.sym InvisibleBraceR)
+            pure (PrefixPredicate r (length args))
+
+
+command :: RE Token Text
+command = RE.msym \case
+    Command cmd -> Just cmd
+    _ -> Nothing
+
+var :: RE Token Token
+var = RE.psym isVar
+
+
+nonDefinitionKeyword :: RE Token Token
+nonDefinitionKeyword = RE.psym (`notElem` keywords)
+    where
+        keywords =
+            [ Word "if"
+            , Word "iff"
+            , Symbol "="
+            , Command "iff"
+            , BeginEnv "math"
+            , EndEnv "math"
+            ]
+
+
+patRE :: RE Token [Token]
+patRE = many (RE.psym isLexicalPhraseToken <|> math var)
+
+structPat :: RE Token [Token]
+structPat = many (RE.psym isLexicalPhraseToken)
+
+beginMath, endMath :: RE Token ()
+beginMath = void (RE.sym (BeginEnv "math"))
+endMath = void (RE.sym (EndEnv "math"))
+
+math :: RE Token a -> RE Token a
+math re = beginMath *> re <* endMath
+
+-- | We allow /conditional perfection/: the first /@if@/ in a definition is interpreted as /@iff@/.
+iff :: RE Token ()
+iff = void (RE.sym (Word "if")) -- Using @void@ is faster (only requires recognition).
+    <|> void (RE.sym (Word "iff"))
+    <|> void (RE.string [Word "if", Word "and", Word "only", Word "if"])
+    <|> void (RE.sym (Word "denote"))
+    <|> void (RE.sym (Word "stand") *> RE.sym (Word "for"))
+{-# INLINE iff #-}
+
+an :: RE Token ()
+an = void (RE.sym (Word "a"))
+    <|> void (RE.sym (Word "an"))
+{-# INLINE an #-}
+
+is :: RE Token ()
+is = void (RE.sym (Word "is") <|> RE.sym (Word "denotes"))
+{-# INLINE is #-}
+
+the :: RE Token ()
+the = void (RE.sym (Word "the"))
+{-# INLINE the #-}
+
+comma :: RE Token ()
+comma = void (RE.sym (Symbol ","))
+{-# INLINE comma #-}
+
+
+isVar :: Token -> Bool
+isVar = \case
+    Variable _ -> True
+    _token -> False
+
+isLexicalPhraseToken :: Token -> Bool
+isLexicalPhraseToken = \case
+    Word w -> w `Set.notMember` keywords
+    --
+    -- Simple commands (outside of math-mode) are allowed. This is useful
+    -- for defining lexical phrases containing symbolic expressions such as
+    -- `X is \Ttwo{}`, where `\Ttwo` is a macro that expands to `T_2`.
+    -- We also allow these macros to take arguments, hence the need to
+    -- allow grouping delimiters. They can also be used to escape the end
+    -- of the command for correct spacing, as in the above example.
+    --
+    Command _cmd -> True
+    InvisibleBraceL -> True
+    InvisibleBraceR -> True
+    --
+    -- No other tokens may occur in lexical phrases. In particular, no `_dot`
+    -- token may occur, limiting the lexical phrase to a single sentence.
+    -- Commas occurring in variable lists should be placed
+    -- within the math environment. Thus `$a,b$ are coprime iff`,
+    -- not `$a$,`$b$` are coprime iff`.
+    --
+    _token -> False
+    where
+        keywords = Set.fromList ["a", "an", "is", "are", "if", "iff", "denote", "stand", "let"]
+
+
+toLexicalPhrase :: [Token] -> LexicalPhrase
+toLexicalPhrase toks = component <$> toks
+    where
+        component = \case
+            Variable _ -> Nothing
+            tok        -> Just tok
+
+
+symbol :: RE Token Token
+symbol = RE.msym $ \tok -> case tok of
+    Command _ -> Just tok
+    Symbol _ -> Just tok
+    _tok -> Nothing
+
+
+-- | Basic paradigms for pluralizations of nominals.
+guessNounPlural :: LexicalPhrase -> SgPl LexicalPhrase
+guessNounPlural item = SgPl item (pluralize item)
+    where
+        pluralize :: LexicalPhrase -> LexicalPhrase
+        pluralize = \case
+            Just (Word w) : pat'@(Just w' : _) | isPreposition w' -> Just (Word (Text.snoc w 's')) : pat'
+            tok : Just (Word w) : pat'@(Just w' : _) | isPreposition w' -> tok : Just (Word (Text.snoc w 's')) : pat'
+            tok1 : tok2 : Just (Word w) : pat'@(Just w' : _) | isPreposition w' -> tok1 : tok2 : Just (Word (Text.snoc w 's')) : pat'
+            [Just (Word w)] -> [Just (Word (Text.snoc w 's'))]
+            [tok, Just (Word w)] -> [tok, Just (Word (Text.snoc w 's'))]
+            [tok, tok', Just (Word w)] -> [tok, tok', Just (Word (Text.snoc w 's'))]
+            pat' -> pat'
+
+guessVerbPlural :: LexicalPhrase -> SgPl LexicalPhrase
+guessVerbPlural item = SgPl item itemPl
+    where
+        itemPl = case item of
+            Just (Word v) : rest -> case Text.unsnoc v of
+                Just (v', 's') -> Just (Word v') : rest
+                _ -> item
+            _ -> item
+
+isAdjR :: LexicalPhrase -> Bool
+isAdjR item = containsPreposition item || containsSlot item
+    where
+        containsPreposition, containsSlot :: LexicalPhrase -> Bool
+        containsPreposition = any isPreposition . catMaybes
+        containsSlot = (Nothing `elem`)
+
+isPreposition :: Token -> Bool
+isPreposition w = Set.member w (Set.map Word prepositions)
diff --git a/source/Felix/Syntax/Concrete.hs b/source/Felix/Syntax/Concrete.hs
new file mode 100644
index 0000000..8be8ab6
--- /dev/null
+++ b/source/Felix/Syntax/Concrete.hs
@@ -0,0 +1,1032 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE RecursiveDo #-}
+
+-- | Concrete syntax of the surface language.
+module Felix.Syntax.Concrete where
+
+import Base
+import Felix.Syntax.Abstract
+import Felix.Syntax.Concrete.Keywords
+import Felix.Syntax.Lexicon
+    ( Lexicon(..)
+    , SignatureHeadForm(..)
+    , concreteSignatureHeadForms
+    , lexiconAdjs
+    , splitOnVariableSlot
+    )
+import Felix.Syntax.Token
+import Felix.Report.Location
+
+import Data.List.NonEmpty qualified as NonEmpty
+import Data.Map.Strict qualified as Map
+import Text.Earley (Grammar, Prod, (<?>), rule, satisfy, terminal)
+import Felix.Syntax.Mixfix
+
+
+grammar :: Lexicon -> Grammar r (Prod r Text (Located Token) Block)
+grammar lexicon@Lexicon{..} = mdo
+    let patternToProd :: Pattern -> Holey (Prod r Text (Located Token) (Located Token))
+        patternToProd pat = map (fmap tokenLocated) (patternToHoley pat)
+        makeMixfixOp item = (patternToProd (mixfixPattern item), mixfixAssoc item, \parts args -> ExprOp (mixfixLoc parts args) item args)
+        mixfixItems = toList (Map.elems <$> lexiconMixfixTable)
+        mixfixOps = map (map makeMixfixOp) mixfixItems
+        makeConn (pat, assoc) = (map (fmap tokenLocated) pat, assoc)
+        conns = map (map makeConn) lexiconConnectives
+
+    integerWithLoc <- rule (terminal maybeIntTokenWithLoc <?> "integer")
+    relatorWithLoc <- rule $ asum
+        [ (,) <$> tokenPos (relationSymbolToken item) <*> pure item
+        | item <- lexiconRelationSymbols
+        ] <?> "relator"
+    relator <- rule (snd <$> relatorWithLoc)
+    varSymbol  <- rule (terminal maybeVarToken <?> "variable")
+    varSymbols <- rule (commaList varSymbol)
+    cmd        <- rule (terminal maybeCmdToken <?> "TEX command")
+--
+-- Formulas have three levels:
+--
+-- + Expressions: atoms or operators applied to atoms.
+-- + Chains:      comma-lists of expressions, separated by relators.
+-- + Formulas:    chains or connectives applied to chains.
+--
+-- For example, the formula @x, y < z \implies x, y < z + 1@ consist of the
+-- connective @\implies@ applied to two chains @x, y < z@ and @x, y < z + 1@.
+-- In turn, the chain @x, y < z + 1@ consist of three expressions,
+-- @x@, @y@, and @z + 1@. Finally, @z + 1@ consist the operator @+@
+-- applied to two atoms, the variable @z@ and the number literal @1@.
+--
+-- This split is due to the different behaviour of relators compared to
+-- operators and connectives. Relators can chain (@x < y < z@) and allow
+-- lists as arguments, as in the above example. Operators and connectives
+-- instead have precedence and fixity. The only syntactic difference between
+-- an operator and a connective is the relative precedence compared to relators.
+--
+    replaceBound  <- rule $ (,) <$> varSymbol <* _in <*> expr
+    replaceBounds <- rule $ commaList replaceBound
+    comprStmt <- rule $ (StmtFormula <$> formula) <|> text stmt
+
+    let replaceFun = (\e bounds mstmt loc -> ExprReplace loc e bounds mstmt) <$> expr <* _pipe <*> replaceBounds <*> optional (_pipe *> comprStmt)
+        replacePredSymbolic = (\y x xBound st loc -> ExprReplacePred loc y x xBound st) <$> varSymbol <* _pipe <*> (command "exists" *> varSymbol) <* _in <*> expr <* _dot <*> (StmtFormula <$> formula)
+        replacePredText = (\y x xBound st loc -> ExprReplacePred loc y x xBound st) <$> varSymbol <* _pipe <*> (begin "text" *> _exists *> beginMath *> varSymbol <* _in) <*> expr <* endMath <* _suchThat <*> stmt <* end "text"
+        replacePred = replacePredSymbolic <|> replacePredText
+
+    let exprStructOpOf ann = foldr alg empty lexiconStructFun
+            where
+                alg s prod = prod <|> (uncurry ExprStructOp <$> structSymbolPos s <*> ann)
+
+    exprStructOp <- rule (exprStructOpOf (optional (bracket expr)))
+
+    let bracedArgs1 ar arg = count1 ar $ group arg
+    let prefixPredicateOf f arg symb@(PrefixPredicate c ar) = f <$> pure symb <* command c <*> bracedArgs1 ar arg
+
+
+    exprParen <- rule $ paren expr
+    exprInteger <- rule $ uncurry ExprInteger <$> integerWithLoc
+    exprVar <- rule $ ExprVar <$> varSymbol
+    exprTuple <- rule do
+        loc <- tokenPos ParenL
+        es <- commaList2 expr <* token ParenR
+        pure (makeTuple loc es)
+    exprSep <- rule do
+        loc <- tokenPos VisibleBraceL
+        x <- varSymbol <* _in
+        bound <- expr <* _pipe
+        phi <- comprStmt <* token VisibleBraceR
+        pure (ExprSep loc x bound phi)
+    exprReplace <- rule do
+        (\loc mk -> mk loc) <$> tokenPos VisibleBraceL <*> (replaceFun <|> replacePred) <* token VisibleBraceR
+    exprFinSet <- rule do
+        loc <- tokenPos VisibleBraceL
+        es <- exprs <* token VisibleBraceR
+        pure (ExprFiniteSet loc es)
+    exprBase    <- rule $ asum [exprVar, exprInteger, exprStructOp, exprParen, exprTuple, exprSep, exprReplace, exprFinSet]
+    exprApp <- rule $ (\e1 e2 -> ExprApp (locate e1) e1 e2) <$> exprBase <*> (paren expr <|> exprTuple)
+    expr        <- mixfixExpressionSeparate mixfixOps (exprBase <|> exprApp)
+    exprs       <- rule $ commaList expr
+
+    relationSign   <- rule $ pure Positive <|> (Negative <$ command "not")
+    relationExpr <- rule $ RelationExpr <$> command "mathrel" <*> group expr
+    relation <- rule $ (uncurry Relation <$> relatorWithLoc <*> many (group expr)) <|> relationExpr
+    chainBase <- rule $ (\es sign rel es' -> ChainBase es sign rel es') <$> exprs <*> relationSign <*> relation <*> exprs
+    chainCons <- rule $ (\es sign rel ch -> ChainCons es sign rel ch) <$> exprs <*> relationSign <*> relation <*> chain
+    chain          <- rule $ chainCons <|> chainBase
+
+    formulaPredicate <- rule $ asum
+        [ (\loc es -> FormulaPredicate loc symb marker es) <$> command c <*> bracedArgs1 ar expr
+        | (symb@(PrefixPredicate c ar), marker) <- lexiconPrefixPredicates
+        ]
+    formulaChain <- rule $ FormulaChain <$> chain
+    formulaBottom <- rule $ PropositionalConstant <$> command "bot" <*> pure IsBottom <?> "\"\\bot\""
+    formulaTop <- rule $ PropositionalConstant <$> command "top" <*> pure IsTop <?> "\"\\top\""
+    formulaExists <- rule $ FormulaQuantified <$> command "exists" <*> pure Existentially <*> varSymbols <*> maybeBounded <* _dot <*> formula
+    formulaAll <- rule $ FormulaQuantified <$> command "forall" <*> pure Universally <*> varSymbols <*> maybeBounded <* _dot <*> formula
+    formulaQuantified <- rule $ formulaExists <|> formulaAll
+    formulaBase       <- rule $ asum [formulaChain, formulaPredicate, formulaBottom, formulaTop, paren formula]
+    formulaConn       <- mixfixExpression conns formulaBase makeConnective
+    formula           <- rule $ formulaQuantified <|> formulaConn
+
+-- These are asymmetric formulas (only variables are allowed on one side).
+-- They express judgements.
+--
+    assignment  <- rule $ (,) <$> varSymbol <* (_eq <|> _defeq) <*> expr
+    typing      <- rule $ (,) <$> varSymbols <* (_in <|> _colon) <*> expr
+
+    adjL     <- rule $ adjLOf lexicon term
+    adjR     <- rule $ adjROf lexicon term
+    adj      <- rule $ adjOf lexicon term
+    adjVar   <- rule $ adjOf lexicon var
+
+    var  <- rule $ math varSymbol
+    vars <- rule $ math varSymbols
+
+    verb     <- rule $ verbOf lexicon sg term
+    verbPl   <- rule $ verbOf lexicon pl term
+    verbVar  <- rule $ verbOf lexicon sg var
+
+    let nounTrieSg = nounTrieOf sg lexiconNouns
+        nounTriePl = nounTrieOf pl lexiconNouns
+        structNounTrieSg = nounTrieOf sg lexiconStructNouns
+
+    noun      <- rule $ nounOfTrie nounTrieSg term nounName -- Noun with optional variable name.
+    nounList  <- rule $ nounOfTrie nounTrieSg term nounNames -- Noun with a list of names.
+    nounVar   <- rule $ fst <$> nounOfTrie nounTrieSg var (pure Nameless) -- No names in defined nouns.
+    nounPl    <- rule $ nounOfTrie nounTriePl term nounNames
+    nounPlMay <- rule $ nounOfTrie nounTriePl term nounName
+
+
+    structNoun <- rule $ structNounOfTrie structNounTrieSg var var
+    structNounNameless <- rule $ fst <$> structNounOfTrie structNounTrieSg var (pure Nameless)
+
+
+    fun      <- rule $ funOf lexicon sg term
+    funVar   <- rule $ funOf lexicon sg var
+
+    attrRThat   <- rule $ AttrRThat <$> thatVerbPhrase
+    attrRThats  <- rule $ ((:[]) <$> attrRThat) <|> ((\a a' -> [a,a']) <$> attrRThat <* _and <*> attrRThat) <|> pure []
+    attrRs      <- rule $ ((:[]) <$> adjR)      <|> ((\a a' -> [a,a']) <$> adjR <* _and <*> adjR)           <|> pure []
+    attrRight   <- rule $ (<>) <$> attrRs <*> attrRThats
+
+    verbPhraseVerbSg    <- rule $ VPVerb <$> verb
+    verbPhraseVerbNotSg <- rule $ VPVerbNot <$> (_does *> _not *> verbPl)
+    verbPhraseAdjSg     <- rule $ VPAdj . (:|[]) <$> (_is *> adj)
+    verbPhraseAdjAnd    <- rule do {_is; a1 <- adj; _and; a2 <- adj; pure (VPAdj (a1 :| [a2]))}
+    verbPhraseAdjNotSg  <- rule $ VPAdjNot . (:|[]) <$> (_is *> _not *> adj)
+    verbPhraseNotSg     <- rule $ verbPhraseVerbNotSg <|> verbPhraseAdjNotSg
+    verbPhraseSg        <- rule $ verbPhraseVerbSg <|> verbPhraseAdjSg <|> verbPhraseAdjAnd <|> verbPhraseNotSg
+
+    -- LATER can cause technical ambiguities? verbPhraseVerbPl    <- rule $ VPVerb <$> verbPl
+    verbPhraseVerbNotPl <- rule $ VPVerbNot <$> (_do *> _not *> verbPl)
+    verbPhraseAdjPl     <- rule $ VPAdj . (:|[]) <$> (_are *> adj)
+    verbPhraseAdjNotPl  <- rule $ VPAdjNot . (:|[]) <$> (_are *> _not *> adj)
+    verbPhraseNotPl     <- rule $ verbPhraseVerbNotPl <|> verbPhraseAdjNotPl
+    verbPhrasePl        <- rule $ verbPhraseAdjPl <|> verbPhraseNotPl -- LATER <|> verbPhraseVerbPl
+
+
+
+    thatVerbPhrase    <- rule $ _that *> verbPhraseSg
+
+    nounName        <- rule $ optional (math varSymbol)
+    nounNames       <- rule $ math (commaList_ varSymbol) <|> pure []
+    nounPhrase      <- rule $ makeNounPhrase <$> many adjL <*> noun  <*> attrRight <*> optional suchStmt
+    nounPhrase'     <- rule $ makeNounPhrase <$> many adjL <*> nounList <*> attrRight <*> optional suchStmt
+    nounPhrasePl    <- rule $ makeNounPhrase <$> many adjL <*> nounPl <*> attrRight <*> optional suchStmt
+    nounPhrasePlMay <- rule $ makeNounPhrase <$> many adjL <*> nounPlMay <*> attrRight <*> optional suchStmt
+    nounPhraseMay   <- rule $ makeNounPhrase <$> many adjL <*> noun <*> attrRight <*> optional suchStmt
+
+    -- Quantification phrases for quantification and indfinite terms.
+    quantAll   <- rule $ QuantPhrase Universally <$> (_forEvery *> nounPhrase' <|> _forAll *> nounPhrasePl)
+    quantSome  <- rule $ QuantPhrase Existentially <$> (_some *> (nounPhrase' <|> nounPhrasePl))
+    quantNone  <- rule $ QuantPhrase Nonexistentially <$> (_no *> (nounPhrase' <|> nounPhrasePl))
+    quant      <- rule $ quantAll <|> quantSome <|> quantNone -- <|> quantUniq
+
+
+    termExpr <- rule $ math do
+        e <- expr
+        pure (TermExpr e)
+    termFun        <- rule $ TermFun <$> (optional _the *> fun)
+    termIota       <- rule $ TermIota <$> _the <*> var <* _suchThat <*> stmt
+    termAll        <- rule $ TermQuantified Universally <$> _every <*> nounPhraseMay
+    termSome       <- rule $ TermQuantified Existentially <$> _some <*> nounPhraseMay
+    termNo         <- rule $ TermQuantified Nonexistentially <$> _no <*> nounPhraseMay
+    termQuantified <- rule $ termAll <|> termSome <|> termNo
+    term           <- rule $ termExpr <|> termFun <|> termQuantified <|> termIota
+
+-- Basic statements @stmt'@ are statements without any conjunctions or quantifiers.
+--
+    let singletonTerm = (:| []) <$> term
+        nonemptyTerms = andList1 term
+    stmtVerbSg    <- rule $ StmtVerbPhrase <$> singletonTerm <*> verbPhraseSg
+    stmtVerbPl    <-rule $ StmtVerbPhrase <$> andList1 term <*> verbPhrasePl
+    stmtVerb      <- rule $ stmtVerbSg <|> stmtVerbPl
+    stmtNounIs    <- rule do
+        ts <- singletonTerm
+        np <- _is *> _an *> nounPhrase
+        pure (StmtNoun ts np)
+    stmtNounAre   <- rule do
+        ts <- nonemptyTerms <* _are
+        np <- nounPhrasePlMay
+        pure (StmtNoun ts np)
+    stmtNounIsNot <- rule do
+        ts <- singletonTerm
+        np <- _is *> _not *> _an *> nounPhrase
+        pure let t :| _ = ts in (StmtNeg (locate t) (StmtNoun ts np))
+    stmtNounAreNot <- rule do
+        ts <- nonemptyTerms
+        np <- _are *> _not *> nounPhrasePlMay
+        pure let t :| _ = ts in (StmtNeg (locate t) (StmtNoun ts np))
+    stmtNoun      <- rule $ stmtNounIs <|> stmtNounIsNot <|> stmtNounAre <|> stmtNounAreNot
+    stmtStruct    <- rule do
+        t <- term
+        s <- _is *> _an *> structNounNameless
+        pure (StmtStruct t s)
+    stmtExists    <- rule $ StmtExists <$> _exists <*> (_an *> nounPhrase')
+    stmtExist     <- rule $ StmtExists <$> _exist <*> nounPhrasePl
+    stmtExistsNot <- rule do
+        p <- _exists *> _no
+        np <- nounPhrase'
+        pure (StmtNeg p (StmtExists p np))
+    stmtFormula <- rule $ math do
+        phi <- formula
+        pure (StmtFormula phi)
+    stmtFormualNeg <- rule do
+        loc <- _not
+        phi <- math formula
+        pure (StmtNeg loc (StmtFormula phi))
+    stmtAtom <- rule $
+        stmtVerb
+            <|> stmtNoun
+            <|> stmtStruct
+            <|> stmtFormula
+            <|> stmtFormualNeg
+            <|> paren stmt
+
+    -- Textual connectives use the same precedence and associativity as
+    -- symbolic connectives. Prefix negation and quantifiers scope over the
+    -- complete statement that follows them.
+    let connect conn lhs rhs =
+            StmtConnected conn Nothing lhs rhs
+        appendScoped conn lhs rhs scoped =
+            let connected = foldl' (connect conn) lhs rhs
+            in maybe connected (connect conn connected) scoped
+    stmtAnd <- rule do
+        lhs <- stmtAtom
+        rhs <- many (_and *> stmtAtom)
+        scoped <- optional (_and *> stmtScoped)
+        pure (appendScoped Conjunction lhs rhs scoped)
+    stmtXor <- rule $
+        StmtConnected ExclusiveOr
+            <$> (Just <$> _either)
+            <*> stmtAnd
+            <* _or
+            <*> stmtAnd
+    stmtNor <- rule $
+        StmtConnected NegatedDisjunction
+            <$> (Just <$> _neither)
+            <*> stmtAnd
+            <* _nor
+            <*> stmtAnd
+    stmtOrBase <- rule $ stmtXor <|> stmtNor <|> stmtAnd
+    stmtOr <- rule do
+        lhs <- stmtOrBase
+        rhs <- many (_or *> stmtOrBase)
+        scoped <- optional (_or *> stmtScoped)
+        pure (appendScoped Disjunction lhs rhs scoped)
+    stmtIf <- rule $
+        StmtConnected Implication
+            <$> (Just <$> _if)
+            <*> stmtIfAntecedent
+            <* optional _comma
+            <* _then
+            <*> stmtImpRhs
+    stmtImp <- rule $ stmtIf <|> stmtOr
+    stmtIff <- rule do
+        lhs <- stmtImp
+        rhs <- optional (_iff *> stmtImpRhs)
+        pure case rhs of
+            Nothing -> lhs
+            Just rhs' -> connect Equivalence lhs rhs'
+    stmtNeg <- rule $ StmtNeg <$> _itIsWrong <*> stmt
+
+    stmtQuantPhrase <- rule $ StmtQuantPhrase <$> _for <*> quant <* optional _comma <* optional _have <*> stmt
+
+    suchStmt <- rule $ _suchThat *> stmt <* optional _comma
+
+   -- Symbolic quantifications with or without generalized bounds.
+    symbolicForall <- rule do
+        p <- _forAll <|> _forEvery
+        xs <- beginMath *> varSymbols
+        b <- maybeBounded <* endMath
+        ms <- optional suchStmt
+        s <- optional _have *> stmt
+        pure (SymbolicForall p xs b ms s)
+    symbolicExists <- rule do
+        loc1 <- _exists <|> _exist
+        xs <- beginMath *> varSymbols
+        b <- maybeBounded
+        loc2 <- endMath
+        ms <- optional (_suchThat *> stmt)
+        pure (SymbolicExists loc1 xs b (ms ?? StmtFormula (PropositionalConstant loc2 IsTop)))
+    symbolicNotExists <- rule do
+        p <- _exists *> _no
+        xs <- beginMath *> varSymbols
+        b <- maybeBounded <* endMath
+        s <- _suchThat *> stmt
+        pure (makeSymbolicNotExists p xs b s)
+    symbolicBound <- rule $ (\sign rel e -> Bounded (locate rel) sign rel e) <$> relationSign <*> relation <*> expr
+    maybeBounded <- rule (pure Unbounded <|> symbolicBound)
+
+    symbolicQuantified <- rule $ symbolicForall <|> symbolicExists <|> symbolicNotExists
+
+    stmtScoped <- rule $
+        asum
+            [ stmtNeg
+            , stmtExists
+            , stmtExist
+            , stmtExistsNot
+            , stmtQuantPhrase
+            , symbolicQuantified
+            ]
+    stmtIfAntecedent <- rule $ stmtScoped <|> stmtOr
+    stmtImpRhs <- rule $ stmtScoped <|> stmtImp
+    stmt :: Prod r Text (Located Token) Stmt <- rule $
+        (stmtScoped <|> stmtIff) <?> "a statement"
+
+
+    asmLetIn        <- rule $ uncurry AsmLetIn <$> (_let *> math typing)
+    asmLetNoun      <- rule $ AsmLetNoun <$> (_let *> fmap pure var <* (_be <|> _denote) <* _an) <*> nounPhrase
+    asmLetNouns     <- rule $ AsmLetNoun <$> (_let *> vars <* (_be <|> _denote)) <*> nounPhrasePlMay
+    asmLetEq        <- rule $ uncurry AsmLetEq <$> (_let *> math assignment)
+    asmLetThe       <- rule $ AsmLetThe <$> (_let *> var <* _be <* _the) <*> fun
+    asmLetStruct    <- rule $ AsmLetStruct <$> (_let *> var <* _be <* _an) <*> structNounNameless
+    asmLet          <- rule $ asmLetNoun <|> asmLetNouns <|> asmLetIn <|> asmLetEq <|> asmLetThe <|> asmLetStruct
+    asmSuppose      <- rule $ AsmSuppose <$> (_suppose *> stmt)
+    asm             <- rule $ andList1_ (asmLet <|> asmSuppose) <* _dot
+    asms            <- rule $ concat <$> many asm
+
+    axiom <- rule $ Axiom <$> asms <* optional _then <*> stmt <* _dot
+
+    claim <- rule $ (,) <$> asms <* optional _then <*> stmt <* _dot
+
+    defnAdj <- rule $ DefnAdj <$> optional (_an *> nounPhrase) <*> var <* _is <*> adjVar
+    defnVerb <- rule $ DefnVerb <$> optional (_an *> nounPhrase) <*> var <*> verbVar
+    defnNoun <- rule $ DefnNoun <$> var <* _is <* _an <*> nounVar
+    defnRel <- rule $ DefnRel <$> (beginMath *> varSymbol) <*> relator <*> many (group varSymbol) <*> varSymbol <* endMath
+    defnSymbolicPredicate <- rule $ math $ asum $ do
+        (predi, marker) <- lexiconPrefixPredicates
+        pure (prefixPredicateOf (\predi' args -> DefnSymbolicPredicate predi' marker args) varSymbol predi)
+    defnHead <- rule $ optional _write *> asum [defnAdj, defnVerb, defnNoun, defnRel, defnSymbolicPredicate]
+
+    defnIf <- rule $ Defn <$> asms <*> defnHead <* (_iff <|> _if) <*> stmt <* _dot
+    defnFunSymb <- rule $ _comma *> termExpr <* _comma --  Optional symbolic equivalent.
+    defnFun <- rule $ DefnFun <$> asms <*> (optional _the *> funVar) <*> optional defnFunSymb <* _is <*> term <* _dot
+
+    symbolicPatternEqTerm <- rule do
+        pat <- beginMath *> symbolicPattern <* _eq
+        e <- expr <* endMath <* _dot
+        pure (pat, e)
+    defnOp <- rule $ uncurry DefnOp <$> symbolicPatternEqTerm
+
+    defn <- rule $ defnIf <|> defnFun <|> defnOp
+
+    abbreviationVerb  <- rule $ AbbreviationVerb <$> var <*> verbVar <* (_iff <|> _if) <*> stmt <* _dot
+    abbreviationAdj   <- rule $ AbbreviationAdj <$> var <* _is <*> adjVar <* (_iff <|> _if) <*> stmt <* _dot
+    abbreviationNoun  <- rule $ AbbreviationNoun <$>  var <* _is <* _an <*> nounVar <* (_iff <|> _if) <*> stmt <* _dot
+    abbreviationRel   <- rule $ AbbreviationRel <$> (beginMath *> varSymbol) <*> relator <*> many (group varSymbol) <*> varSymbol <* endMath <* (_iff <|> _if) <*> stmt <* _dot
+    abbreviationFun   <- rule $ AbbreviationFun <$> (_the *> funVar) <* (_is <|> _denotes) <*> term <* _dot
+    abbreviationEq    <- rule $ uncurry AbbreviationEq <$> symbolicPatternEqTerm
+    abbreviation      <- rule $ (abbreviationVerb <|> abbreviationAdj <|> abbreviationNoun <|> abbreviationRel <|> abbreviationFun <|> abbreviationEq)
+
+    datatypePremise <- rule $ math $ (,) <$> varSymbol <* _in <*> expr
+    datatypeClause <- rule $
+        (\(constructorExpr, targetExpr) premises -> DatatypeClause
+            { datatypeClauseConstructorExpr = constructorExpr
+            , datatypeClauseTargetExpr = targetExpr
+            , datatypeClausePremises = premises ?? []
+            }) <$> math ((,) <$> expr <* _in <*> expr)
+               <*> optional (_for *> andList1_ datatypePremise)
+               <* _dot
+    datatypeHead <- rule $ _define *> math expr <* optional _inductively <* optional _asFollows <* _dot
+    datatype     <- rule $ Datatype <$> datatypeHead <*> enumerated1 datatypeClause
+
+    unconditionalIntro <- rule $ IntroRule [] <$> math formula
+    conditionalIntro   <- rule $ IntroRule <$> (_if *> andList1_ (math formula)) <* _comma <* _then <*> math formula
+    inductiveIntro     <- rule $ (unconditionalIntro <|> conditionalIntro) <* _dot
+    inductiveDomain    <- rule $ math $ (,) <$> symbolicPattern <* _subseteq <*> expr
+    inductiveHead      <- rule $ _define *> inductiveDomain <* optional _inductively <* optional _asFollows <* _dot
+    inductive          <- rule $ uncurry Inductive <$> inductiveHead <*> enumerated1 inductiveIntro
+
+    signatureAdj      <- rule $ SignatureAdj <$> var <* _can <* _be <*> adjOf lexicon var
+    symbolicPattern   <- symbolicPatternOf mixfixItems varSymbol
+    signatureSymbolic <- rule $ SignatureSymbolic <$> math symbolicPattern <* _is <* _an <*> nounPhrase
+    signatureHead <- rule $ asum
+        [ case form of
+            AdjectiveSignatureHead -> signatureAdj
+            SymbolicSignatureHead -> signatureSymbolic
+        | form <- concreteSignatureHeadForms
+        ]
+    signature <- rule $
+        (,) <$> asms <* optional _then <*> signatureHead <* _dot
+
+    structFix <- rule do
+        beginMath
+        rawCmd <- cmd
+        endMath
+        pure (StructSymbol rawCmd)
+    structDefn <- rule $ do
+        _an
+        ~(structPhrase, structLabel) <- structNoun
+        _extends
+        structParents <- andList1_ (_an *> structNounNameless)
+        maybeFixes <- optional (_equipped *> enumerated structFix)
+        structAssumes <- (_suchThat *> enumeratedMarked (stmt <* _dot)) <|> ([] <$ _dot)
+        pure StructDefn
+            { structPhrase = structPhrase
+            , structLabel = structLabel
+            , structParents = structParents
+            , structFixes = maybeFixes ?? []
+            , structAssumes = structAssumes
+            }
+
+    justificationSet <- rule $ JustificationSetExt <$ _bySetExt
+    justificationRef <- rule $ JustificationRef <$> (_by *> ref)
+    justificationLocal <- rule $ JustificationLocal <$ (_by *> (_assumption <|> _definition))
+    justification <- rule (justificationSet <|> justificationRef <|> justificationLocal <|> pure JustificationEmpty)
+
+    trivial          <- rule $ Qed . Just <$> _trivial <* _dot <*> pure JustificationEmpty
+    omitted          <- rule $ Omitted <$> _omitted <* _dot
+    qedJustified     <- rule $ Qed . Just <$> _follows <*> (justification <* _dot)
+    qed              <- rule $ qedJustified <|> trivial <|> omitted <|> pure (Qed Nothing JustificationEmpty)
+    contradiction    <- rule $ Contradiction <$> _contradiction <*> justification <* _dot
+
+    let alignedEq = symbol "&=" <?> "\"&=\""
+    explanation <- rule $ (text justification) <|> pure JustificationEmpty
+    equationItem <- rule $ (,) <$> (alignedEq *> expr) <*> explanation
+    equations <- rule $ Equation <$> expr <*> (many1 equationItem)
+
+    let alignedIff = symbol "&" *> command "iff" <?> "\"&\\iff\""
+    biconditionalItem <- rule $ (,) <$> (alignedIff *> formula) <*> explanation
+    biconditionals <- rule $ Biconditionals <$> formula <*> (many1 biconditionalItem) <* optional _dot
+
+
+    calcQuantifier <- rule do
+        loc <- _forAll <|> _forEvery
+        xs <- beginMath *> varSymbols
+        mb <- maybeBounded <* endMath
+        st <- optional suchStmt
+        optional _have
+        pure (loc, CalcQuantifier xs mb st)
+
+    calc <- rule do
+        mquant <- optional calcQuantifier
+        psteps <- align (equations <|> biconditionals)
+        pf <- proof
+        pure let (loc2, steps) = psteps in case mquant of
+            Nothing -> Calc loc2 Nothing steps pf
+            Just (loc, q) -> Calc loc (Just q) steps pf
+
+    caseOf           <- rule $ command "caseOf" *> token InvisibleBraceL *> stmt <* _dot <* token InvisibleBraceR
+    byCases          <- rule $ uncurry ByCase <$> envPos_ "byCase" (many1_ (Case <$> caseOf <*> proof))
+    byContradiction  <- rule $ ByContradiction <$> _suppose <* _not <* _dot <*> proof
+    bySetInduction   <- rule $ uncurry BySetInduction <$> proofBy (_in *> word "-induction" *> optional (word "on" *> term)) <*> proof
+    byOrdInduction   <- rule $ ByOrdInduction . fst <$> proofBy (word "transfinite" *> word "induction") <*> proof
+    assume           <- rule $ Assume <$> _suppose <*> (stmt <* _dot) <*> proof
+
+    fixSymbolic      <- rule $ FixSymbolic <$> _fix <*> (beginMath *> varSymbols) <*> maybeBounded <* endMath <* _dot <*> proof
+    fixSuchThat      <- rule $ FixSuchThat <$> _fix <*> math varSymbols <* _suchThat <*> stmt <* _dot <*> proof
+    fix              <- rule $ fixSymbolic <|> fixSuchThat
+
+    takeVar          <- rule $ TakeVar <$> _take <*> (beginMath *> varSymbols) <*> maybeBounded <* endMath <* _suchThat <*> stmt <*> justification <* _dot <*> proof
+    takeNoun         <- rule $ TakeNoun <$> _take <*> (_an *> (nounPhrase' <|> nounPhrasePl)) <*> justification <* _dot <*> proof
+    take             <- rule $ takeVar <|> takeNoun
+    suffices         <- rule $ Suffices <$> _sufficesThat <*> stmt <*> (justification <* _dot) <*> proof
+    subclaim         <- rule $ Subclaim <$> _show <*> (stmt <* _dot) <*> env_ "subproof" proof <*> proof
+    have             <- rule do
+        msince <- optional ((,) <$> _since <*> stmt <* _comma <* _have)
+        mpos <- optional _haveIntro
+        s <- stmt
+        j <- justification <* _dot
+        pf <- proof
+        pure
+            let pos = case (msince, mpos) of
+                    (Just (p, _), _) -> p
+                    (_, Just p) -> p
+                    _ -> locate s
+            in (Have pos (snd <$> msince) s j pf)
+
+
+    define           <- rule $ Define <$> _let <*> (beginMath *> varSymbol <* _eq) <*> expr <* endMath <* _dot <*> proof
+    defineFunction   <- rule $ DefineFunction <$> _let <*> (beginMath *> varSymbol) <*> paren varSymbol <* _eq <*>  expr <* endMath <* _for <* beginMath <*> varSymbol <* _in <*> expr <* endMath <* _dot <*> proof
+
+    proof            <- rule $ asum [byContradiction, byCases, bySetInduction, byOrdInduction, calc, subclaim, assume, fix, take, have, suffices, define, defineFunction, contradiction, qed]
+
+
+    blockAxiom  <- rule $ (\(p, title, m, a) -> BlockAxiom p title m a) <$> envPos  "axiom" axiom
+    blockClaim  <- rule $ claimEnv claim
+    blockProof  <- rule $ uncurry3 BlockProof     <$> envStartEndLocation "proof" proof
+    blockDefn   <- rule $ (\(p, title, m, d) -> BlockDefn p title m d) <$> envPos "definition" defn
+    blockAbbr   <- rule $ (\(p, title, m, a) -> BlockAbbr p title m a) <$> envPos "abbreviation" abbreviation
+    blockData   <- rule $ (\(p, title, m, d) -> BlockData p title m d) <$> envPos "datatype" datatype
+    blockInd    <- rule $ (\(p, title, m, i) -> BlockInductive p title m i) <$> envPos "inductive" inductive
+    blockSig    <- rule $ (\(p, title, m, (a, s)) -> BlockSig p title m a s) <$> envPos "signature" signature
+    blockStruct <- rule $ (\(p, title, m, s) -> BlockStruct p title m s) <$> envPos "struct" structDefn
+    block       <- rule $ asum [blockAxiom, blockClaim, blockDefn, blockAbbr, blockData, blockInd, blockSig, blockStruct, blockProof]
+
+    -- Starting category.
+    pure block
+
+
+proofBy :: Prod r Text (Located Token) a -> Prod r Text (Located Token) (Location, a)
+proofBy method = bracket do
+    pos <- word "proof" *> word "by"
+    a <- method
+    pure (pos, a)
+
+claimEnv :: Prod r Text (Located Token) (([Asm], Stmt)) -> Prod r Text (Located Token) Block
+claimEnv content = asum
+    [ make Theorem <$> envPos "theorem" content
+    , make Lemma <$> envPos "lemma" content
+    , make Corollary <$> envPos "corollary"  content
+    , make PlainClaim <$> envPos "claim" content
+    , make Proposition <$> envPos "proposition" content
+    ]
+    where
+        make kind = (\ (loc, title, m, (asms, stmt)) -> BlockClaim kind loc title m (Claim asms stmt))
+
+-- | A disjunctive list with at least two items:
+-- * 'a or b'
+-- * 'a, b, or c'
+-- * 'a, b, c, or d'
+--
+orList2 :: Prod r Text (Located Token) a -> Prod r Text (Located Token) (NonEmpty a)
+orList2 item = ((:|) <$> item <*> many (_commaOr *> item))
+    <|> ((\i j -> i:|[j]) <$> item <* _or <*> item)
+
+
+-- | Nonempty textual lists of the form "a, b, c, and d".
+-- The final comma is mandatory, 'and' is not.
+-- Also allows "a and b". Should therefore be avoided in contexts where
+-- a logical conjunction would also be possible.
+-- Currently also allows additional 'and's after each comma...
+--
+andList1 :: Prod r Text (Located Token) a -> Prod r Text (Located Token) (NonEmpty a)
+andList1 item = ((:|) <$> item <*> many (_commaAnd *> item))
+    <|> ((\i j -> i:|[j]) <$> item <* _and <*> item)
+
+-- | Like 'andList1', but drops the information about nonemptiness.
+andList1_ :: Prod r Text (Located Token) a -> Prod r Text (Located Token) [a]
+andList1_ item = NonEmpty.toList <$> andList1 item
+
+
+commaList :: Prod r Text (Located Token) a -> Prod r Text (Located Token) (NonEmpty a)
+commaList item = (:|) <$> item <*> many (_comma *> item)
+
+-- | Like 'commaList', but drops the information about nonemptiness.
+commaList_ :: Prod r Text (Located Token) a -> Prod r Text (Located Token) [a]
+commaList_ item = NonEmpty.toList <$> commaList item
+
+-- | Like 'commaList', but requires at least two items (and hence at least one comma).
+commaList2 :: Prod r Text (Located Token) a -> Prod r Text (Located Token) (NonEmpty a)
+commaList2 item = (:|) <$> item <* _comma <*> commaList_ item
+
+
+enumerated :: Prod r Text (Located Token) a -> Prod r Text (Located Token) [a]
+enumerated p = NonEmpty.toList <$> enumerated1 p
+
+enumerated1 :: Prod r Text (Located Token) a -> Prod r Text (Located Token) (NonEmpty a)
+enumerated1 p = begin "enumerate" *> many1 (command "item" *> p) <* end "enumerate" <?> "\"\\begin{enumerate} ...\""
+
+
+enumeratedMarked :: Prod r Text (Located Token) a -> Prod r Text (Located Token) [(Marker, a)]
+enumeratedMarked p = NonEmpty.toList <$> enumeratedMarked1 p
+
+enumeratedMarked1 :: Prod r Text (Located Token) a -> Prod r Text (Located Token) (NonEmpty (Marker, a))
+enumeratedMarked1 p = begin "enumerate" *> many1 ((,) <$> (command "item" *> label) <*> p) <* end "enumerate" <?> "\"\\begin{enumerate}\\item\\label{...}...\""
+
+
+
+-- This function could be rewritten, so that it can be used directly in the grammar,
+-- instead of with specialized variants.
+--
+phraseOf
+    :: forall pat a b r. Locatable a
+    => (Location -> pat -> [a] -> b)
+    -> Lexicon
+    -> (Lexicon -> [pat])
+    -> (pat -> LexicalPhrase)
+    -> Prod r Text (Located Token) a
+    -> Prod r Text (Located Token) b
+phraseOf constr lexicon selector proj arg =
+    uncurry3 constr <$> buildPhraseTrie arg trie
+    where
+        pats :: [pat]
+        pats = selector lexicon
+
+        trie :: Trie PhraseStep pat
+        trie = trieFromList
+            [ (phraseSteps (proj pat), pat)
+            | pat <- pats
+            ]
+
+adjLOf :: Locatable arg => Lexicon -> Prod r Text (Located Token) arg -> Prod r Text (Located Token) (AdjLOf arg)
+adjLOf lexicon arg = phraseOf AdjL lexicon lexiconAdjLs lexicalItemPhrase arg <?> "a left adjective"
+
+adjROf :: Locatable arg =>Lexicon -> Prod r Text (Located Token) arg -> Prod r Text (Located Token) (AdjROf arg)
+adjROf lexicon arg = phraseOf AdjR lexicon lexiconAdjRs lexicalItemPhrase arg <?> "a right adjective"
+
+adjOf :: Locatable arg =>Lexicon -> Prod r Text (Located Token) arg -> Prod r Text (Located Token) (AdjOf arg)
+adjOf lexicon arg = phraseOf Adj lexicon lexiconAdjs lexicalItemPhrase arg <?> "an adjective"
+
+verbOf
+    :: Locatable a => Lexicon
+    -> (SgPl LexicalPhrase -> LexicalPhrase)
+    -> Prod r Text (Located Token) a
+    -> Prod r Text (Located Token) (VerbOf a)
+verbOf lexicon proj arg = phraseOf Verb lexicon lexiconVerbs (proj . lexicalItemSgPlPhrase) arg
+
+funOf
+    :: Locatable a => Lexicon
+    -> (SgPl LexicalPhrase -> LexicalPhrase)
+    -> Prod r Text (Located Token) a
+    -> Prod r Text (Located Token) (FunOf a)
+funOf lexicon proj arg = phraseOf Fun lexicon lexiconFuns (proj . lexicalItemSgPlPhrase) arg <?> "functional phrase"
+
+
+-- | A noun with a @t VarSymbol@ as name(s).
+nounOf
+    :: Locatable arg => Lexicon
+    -> (SgPl LexicalPhrase -> LexicalPhrase)
+    -> Prod r Text (Located Token) arg
+    -> Prod r Text (Located Token) (t VarSymbol)
+    -> Prod r Text (Located Token) (NounOf arg, t VarSymbol)
+nounOf lexicon proj arg vars =
+    nounOfTrie (nounTrieOf proj (lexiconNouns lexicon)) arg vars
+
+nounOfTrie
+    :: Locatable arg => Trie NounStep LexicalItemSgPl
+    -> Prod r Text (Located Token) arg
+    -> Prod r Text (Located Token) (t VarSymbol)
+    -> Prod r Text (Located Token) (NounOf arg, t VarSymbol)
+nounOfTrie trie arg vars =
+    (\(loc, pat, args, xs) -> (Noun loc pat args, xs))
+        <$> buildNounTrie arg vars trie
+        <?> "a noun"
+
+nounTrieOf
+    :: (SgPl LexicalPhrase -> LexicalPhrase)
+    -> [LexicalItemSgPl]
+    -> Trie NounStep LexicalItemSgPl
+nounTrieOf proj pats = trieFromList
+    [ (nounStepsWithSlot (proj (lexicalItemSgPlPhrase pat)), pat)
+    | pat <- pats
+    ]
+
+structNounOfTrie
+    :: Locatable arg => Trie NounStep LexicalItemSgPl
+    -> Prod r Text (Located Token) arg
+    -> Prod r Text (Located Token) name
+    -> Prod r Text (Located Token) (StructPhrase, name)
+structNounOfTrie trie arg name =
+    (\(_loc, pat, _args, xs) -> (pat, xs))
+        <$> buildNounTrie arg name trie
+        <?> "a structure noun"
+
+structNounOf
+    :: Locatable arg => Lexicon
+    -> (SgPl LexicalPhrase -> LexicalPhrase)
+    -> Prod r Text (Located Token) arg
+    -> Prod r Text (Located Token) name
+    -> Prod r Text (Located Token) (StructPhrase, name)
+structNounOf lexicon proj arg name =
+    structNounOfTrie (nounTrieOf proj (lexiconStructNouns lexicon)) arg name
+
+-- Trie helpers for lexically-defined phrases.
+
+data PhraseStep
+    = PhraseTok Token
+    | PhraseHole
+    deriving (Eq, Ord)
+
+data NounStep
+    = NounTok Token
+    | NounHole
+    | NounVar
+    deriving (Eq, Ord)
+
+data Trie k v = Trie
+    { trieValues :: [v]
+    , trieEdges  :: [(k, Trie k v)]
+    }
+
+emptyTrie :: Trie k v
+emptyTrie = Trie [] []
+
+insertTrie :: Eq k => [k] -> v -> Trie k v -> Trie k v
+insertTrie [] v Trie{trieValues = vs, trieEdges = es} =
+    Trie (vs <> [v]) es
+insertTrie (k:ks) v Trie{trieValues = vs, trieEdges = es} =
+    Trie vs (go es)
+    where
+        go = \case
+            [] -> [(k, insertTrie ks v emptyTrie)]
+            (k', child) : rest
+                | k == k'   -> (k', insertTrie ks v child) : rest
+                | otherwise -> (k', child) : go rest
+
+trieFromList :: Eq k => [([k], v)] -> Trie k v
+trieFromList = foldl' (\tr (k, v) -> insertTrie k v tr) emptyTrie
+
+phraseSteps :: LexicalPhrase -> [PhraseStep]
+phraseSteps = map \case
+    Just tok -> PhraseTok tok
+    Nothing  -> PhraseHole
+
+nounSteps :: LexicalPhrase -> [NounStep]
+nounSteps = map \case
+    Just tok -> NounTok tok
+    Nothing  -> NounHole
+
+nounStepsWithSlot :: LexicalPhrase -> [NounStep]
+nounStepsWithSlot pat =
+    let (pat1, pat2) = splitOnVariableSlot pat
+    in nounSteps pat1 <> [NounVar] <> nounSteps pat2
+
+data PhraseAcc a = PhraseAcc
+    { phraseLoc  :: Maybe Location
+    , phraseArgs :: [a] -> [a]
+    }
+
+emptyPhraseAcc :: PhraseAcc a
+emptyPhraseAcc = PhraseAcc Nothing id
+
+setPhraseLoc :: Location -> PhraseAcc a -> PhraseAcc a
+setPhraseLoc Nowhere acc = acc
+setPhraseLoc _loc acc@PhraseAcc{phraseLoc = Just _} = acc
+setPhraseLoc loc PhraseAcc{phraseLoc = Nothing, phraseArgs = args} =
+    PhraseAcc (Just loc) args
+
+addPhraseArg :: Locatable a => a -> PhraseAcc a -> PhraseAcc a
+addPhraseArg a acc@PhraseAcc{phraseLoc = loc, phraseArgs = args}
+    | locate a == Nowhere = acc{phraseArgs = args . (a :)}
+    | otherwise = PhraseAcc (loc <|> Just (locate a)) (args . (a :))
+
+finalizePhraseAcc :: PhraseAcc a -> (Location, [a])
+finalizePhraseAcc PhraseAcc{phraseLoc = Just loc, phraseArgs = args} =
+    (loc, args [])
+finalizePhraseAcc PhraseAcc{phraseLoc = Nothing} =
+    impossible "phraseOf: empty phrase"
+
+data NounAcc a name = NounAcc
+    { nounLoc :: Maybe Location
+    , nounArgs :: [a] -> [a]
+    , nounName :: Maybe name
+    }
+
+emptyNounAcc :: NounAcc a name
+emptyNounAcc = NounAcc Nothing id Nothing
+
+setNounLoc :: Location -> NounAcc a name -> NounAcc a name
+setNounLoc Nowhere acc = acc
+setNounLoc _loc acc@NounAcc{nounLoc = Just _} = acc
+setNounLoc loc NounAcc{nounLoc = Nothing, nounArgs = args, nounName = name} =
+    NounAcc (Just loc) args name
+
+addNounArg :: Locatable a => a -> NounAcc a name -> NounAcc a name
+addNounArg a acc@NounAcc{nounLoc = loc, nounArgs = args, nounName = name}
+    | locate a == Nowhere = acc{nounArgs = args . (a :)}
+    | otherwise = NounAcc (loc <|> Just (locate a)) (args . (a :)) name
+
+setNounName :: name -> NounAcc a name -> NounAcc a name
+setNounName name NounAcc{nounLoc = loc, nounArgs = args, nounName = Nothing} =
+    NounAcc loc args (Just name)
+setNounName _ acc@NounAcc{nounName = Just _} = acc
+
+finalizeNounAcc :: NounAcc a name -> (Location, [a], name)
+finalizeNounAcc NounAcc{nounLoc = Just loc, nounArgs = args, nounName = Just name} =
+    (loc, args [], name)
+finalizeNounAcc NounAcc{nounName = Nothing} =
+    impossible "nounOf: missing variable slot"
+finalizeNounAcc NounAcc{nounLoc = Nothing} =
+    impossible "nounOf: empty noun phrase"
+
+buildPhraseTrie
+    :: Locatable a
+    => Prod r Text (Located Token) a
+    -> Trie PhraseStep pat
+    -> Prod r Text (Located Token) (Location, pat, [a])
+buildPhraseTrie arg trie =
+    let stepParser = \case
+            PhraseTok tok -> setPhraseLoc <$> tokenPos tok
+            PhraseHole    -> addPhraseArg <$> arg
+        finish f =
+            let (acc, pat) = f emptyPhraseAcc
+                (loc, args) = finalizePhraseAcc acc
+            in (loc, pat, args)
+    in finish <$> buildTrieProd stepParser trie
+
+buildTrieProd
+    :: (step -> Prod r Text (Located Token) (acc -> acc))
+    -> Trie step pat
+    -> Prod r Text (Located Token) (acc -> (acc, pat))
+buildTrieProd stepParser = go
+    where
+        go Trie{trieValues = pats, trieEdges = edges} =
+            let leafs = asum [pure (\acc -> (acc, pat)) | pat <- pats]
+                edgesProds = asum
+                    [ liftA2 (\f g -> g . f) (stepParser step) (go sub)
+                    | (step, sub) <- edges
+                    ]
+            in leafs <|> edgesProds
+
+buildNounTrie
+    :: Locatable a
+    => Prod r Text (Located Token) a
+    -> Prod r Text (Located Token) name
+    -> Trie NounStep pat
+    -> Prod r Text (Located Token) (Location, pat, [a], name)
+buildNounTrie arg vars trie =
+    let stepParser = \case
+            NounTok tok -> setNounLoc <$> tokenPos tok
+            NounHole    -> addNounArg <$> arg
+            NounVar     -> setNounName <$> vars
+        finish f =
+            let (acc, pat) = f emptyNounAcc
+                (loc, args, name) = finalizeNounAcc acc
+            in (loc, pat, args, name)
+    in finish <$> buildTrieProd stepParser trie
+
+
+symbolicPatternOf
+    :: forall r. [[MixfixItem]]
+    -> Prod r Text (Located Token) VarSymbol
+    -> Grammar r (Prod r Text (Located Token) SymbolPattern)
+symbolicPatternOf ops varSymbol = rule $
+    (tuplePattern <|> asum
+        [ go item
+        | ops' <- ops
+        , item <- ops'
+        ]) <?> "a symbolic pattern"
+    where
+        tuplePattern = do
+            token ParenL
+            first <- varSymbol <* token (Symbol ",")
+            second <- varSymbol <* token ParenR
+            pure (SymbolPattern PairSymbol [first, second])
+
+        go :: MixfixItem -> Prod r Text (Located Token) SymbolPattern
+        go item = SymbolPattern item <$> parseVars (mixfixPattern item)
+
+        parseVars :: Pattern -> Prod r Text (Located Token) [VarSymbol]
+        parseVars = \case
+            End -> pure []
+            TokenCons tok pat -> token tok *> parseVars pat
+            HoleCons pat -> (:) <$> varSymbol <*> parseVars pat
+
+
+makeNounPhrase
+    :: [AdjL]
+    -> (Noun, t VarSymbol)
+    -> [AdjR]
+    -> Maybe Stmt
+    -> NounPhrase t
+makeNounPhrase ls (n, vs) rs ms = NounPhrase ls n vs rs ms
+
+
+
+
+begin, end :: Text -> Prod r Text (Located Token) Location
+begin kind = tokenPos (BeginEnv kind) <?> ("\"\\begin{" <> kind <> "}\"")
+end kind   = tokenPos (EndEnv kind) <?> ("\"\\end{" <> kind <> "}\"")
+
+-- | Surround a production rule @body@ with an environment of a certain @kind@ requiring a marker specified in a @\\label@.
+envPos :: Text -> Prod r Text (Located Token) a -> Prod r Text (Located Token) (Location, Maybe [Token], Marker, a)
+envPos kind body = do
+    p <- begin kind <?> ("start of a \"" <> kind <> "\" environment")
+    mt <- optional title
+    m <- label
+    a <- body <* end kind
+    pure (p, mt, m, a)
+    where
+        title :: Prod r Text (Located Token) [Token]
+        title = bracket (many (unLocated <$> satisfy (\ltok -> unLocated ltok /= BracketR)))
+
+-- 'env_' is like 'env', but without allowing titles.
+--
+envPos_ :: Text -> Prod r Text (Located Token) a -> Prod r Text (Located Token) (Location, a)
+envPos_ kind body = (,) <$> begin kind <*> (optional label *> body) <* end kind
+
+envStartEndLocation :: Text -> Prod r Text (Located Token) a -> Prod r Text (Located Token) (Location, a, Location)
+envStartEndLocation kind body = (,,) <$> begin kind <*> (optional label *> body) <*> end kind
+
+env_ :: Text -> Prod r Text (Located Token) a -> Prod r Text (Located Token) a
+env_ kind body = begin kind *> optional label *> body <* end kind
+
+-- | A label specifying a marker for referencing via /@\\label{...}@/. Returns the marker text.
+label :: Prod r Text (Located Token) Marker
+label = label_ <?> "\"\\label{...}\""
+    where
+        label_ = terminal \ltok -> case unLocated ltok of
+            Label m -> Just (Marker m)
+            _tok -> Nothing
+
+-- | A reference via /@\\ref{...}@/. Returns the markers as text.
+ref :: Prod r Text (Located Token) (NonEmpty Marker)
+ref = terminal \ltok -> case unLocated ltok of
+    Ref ms -> Just (Marker <$> ms)
+    _tok -> Nothing
+
+math :: Prod r Text (Located Token) a -> Prod r Text (Located Token) a
+math body = beginMath *> body <* endMath
+
+mathPos :: Prod r Text (Located Token) a -> Prod r Text (Located Token) (Location, a)
+mathPos body = (,) <$> beginMath <*> body <* endMath
+
+text :: Prod r Text (Located Token) a -> Prod r Text (Located Token) a
+text body = begin "text" *> body <* end "text" <?> "\"\\text{...}\""
+
+beginMath, endMath :: Prod r Text (Located Token) Location
+beginMath = begin "math" <?> "start of a formula, e.g. \"$\""
+endMath = end "math" <?> "end of a formula, e.g. \"$\""
+
+paren :: Prod r Text (Located Token) a -> Prod r Text (Located Token) a
+paren body = token ParenL *> body <* token ParenR <?> "\"(...)\""
+
+bracket :: Prod r Text (Located Token) a -> Prod r Text (Located Token) a
+bracket body = token BracketL *> body <* token BracketR <?> "\"[...]\""
+
+brace :: Prod r Text (Located Token) a -> Prod r Text (Located Token) a
+brace body = token VisibleBraceL  *> body <* token VisibleBraceR <?> "\"\\{...\\}\""
+
+group :: Prod r Text (Located Token) a -> Prod r Text (Located Token) a
+group body = token InvisibleBraceL *> body <* token InvisibleBraceR <?> "\"{...}\""
+
+align :: Prod r Text (Located Token) a -> Prod r Text (Located Token) (Location, a)
+align body = (,) <$> begin "align*" <*> body <* end "align*"
+
+cases :: Prod r Text (Located Token) a -> Prod r Text (Located Token) a
+cases body = begin "cases" *> body <* end "cases"
+
+
+maybeVarToken :: Located Token -> Maybe VarSymbol
+maybeVarToken ltok = case unLocated ltok of
+    Variable x -> Just (NamedVarAt (startPos ltok) x)
+    _tok -> Nothing
+
+maybeWordToken :: Located Token -> Maybe Text
+maybeWordToken ltok = case unLocated ltok of
+    Word n -> Just n
+    _tok -> Nothing
+
+maybeIntToken :: Located Token -> Maybe Int
+maybeIntToken ltok = case unLocated ltok of
+    Integer n -> Just n
+    _tok -> Nothing
+
+maybeIntTokenWithLoc :: Located Token -> Maybe (Location, Int)
+maybeIntTokenWithLoc ltok = case unLocated ltok of
+    Integer n -> Just (startPos ltok, n)
+    _tok -> Nothing
+
+maybeCmdToken :: Located Token -> Maybe Text
+maybeCmdToken ltok = case unLocated ltok of
+    Command n -> Just n
+    _tok -> Nothing
+
+structSymbol :: StructSymbol -> Prod r Text (Located Token) StructSymbol
+structSymbol s@(StructSymbol c) = terminal \ltok -> case unLocated ltok of
+    Command c' | c == c' -> Just s
+    _ -> Nothing
+
+structSymbolPos :: StructSymbol -> Prod r Text (Located Token) (Location, StructSymbol)
+structSymbolPos s@(StructSymbol c) = terminal \ltok -> case unLocated ltok of
+    Command c' | c == c' -> Just (startPos ltok, s)
+    _ -> Nothing
+
+-- | Tokens that are allowed to appear in labels of environments.
+maybeTagToken :: Located Token -> Maybe Text
+maybeTagToken ltok = case unLocated ltok of
+    Symbol "'" ->Just "'"
+    Symbol "-" -> Just ""
+    _ -> maybeWordToken ltok
+
+
+token :: Token -> Prod r Text (Located Token) Token
+token tok = terminal maybeToken <?> tokToText tok
+    where
+        maybeToken ltok = case unLocated ltok of
+            tok' | tok == tok' -> Just tok
+            _ -> Nothing
+
+tokenLocated :: Token -> Prod r Text (Located Token) (Located Token)
+tokenLocated tok = terminal maybeToken <?> tokToText tok
+    where
+        maybeToken ltok = case unLocated ltok of
+            tok' | tok == tok' -> Just ltok
+            _ -> Nothing
+
+tokenPos :: Token -> Prod r Text (Located Token) Location
+tokenPos tok = terminal maybeToken <?> tokToText tok
+    where
+        maybeToken ltok = case unLocated ltok of
+            tok' | tok == tok' -> Just (startPos ltok)
+            _ -> Nothing
diff --git a/source/Felix/Syntax/Concrete/Keywords.hs b/source/Felix/Syntax/Concrete/Keywords.hs
new file mode 100644
index 0000000..eb6d09c
--- /dev/null
+++ b/source/Felix/Syntax/Concrete/Keywords.hs
@@ -0,0 +1,228 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+{-|
+This module defines lots of keywords and various filler
+phrases. The prefix underscore indicates that we do not
+care about the parse result (analogous to  discarding
+like @...; _ <- action; ...@ in do-notation). Moreover,
+this convention allows the use of short names that would
+otherwise be Haskell keywords or clash with other definitions.
+Care should be taken with introducing too many variants of
+a keyword, lest the grammar becomes needlessly ambiguous!
+
+The names are chosen using the following criteria:
+
+   * As short as possible (e.g.: @_since@ over @_because@).
+
+   * Sound like a keyword (e.g.: @_show@).
+
+This module also defines symbols that have special uses
+(such as @_colon@ for its use in type signatures).
+-}
+module Felix.Syntax.Concrete.Keywords where
+
+
+import Base
+import Felix.Syntax.Token
+import Felix.Report.Location
+
+import Text.Earley (Prod, (<?>), terminal)
+
+infixr 0 ?
+-- | Variant of '<?>' for annotating literal tokens.
+(?) :: Prod r Text t a -> Text -> Prod r Text t a
+p ? e = p <?> ("\"" <> e <> "\"")
+
+word :: Text -> Prod r Text (Located Token) Location
+word w = terminal maybeToken
+   where
+      maybeToken ltok = case unLocated ltok of
+         Word w' | w == w' -> Just (startPos ltok)
+         _ -> Nothing
+
+symbol :: Text -> Prod r Text (Located Token) Location
+symbol s = terminal maybeToken
+   where
+      maybeToken ltok = case unLocated ltok of
+         Symbol s' | s == s' -> Just (startPos ltok)
+         _ -> Nothing
+
+command :: Text -> Prod r Text (Located Token) Location
+command cmd = terminal maybeToken
+   where
+      maybeToken ltok = case unLocated ltok of
+         Command cmd' | cmd == cmd' -> Just (startPos ltok)
+         _ -> Nothing
+
+_arity :: Prod r Text (Located Token) Int
+_arity = asum
+   [ 1  <$ word "unary"
+   , 2  <$ word "binary"
+   , 3  <$ word "ternary"
+   , 4  <$ word "quaternary"
+   , 5  <$ word "quinary"
+   , 6  <$ word "senary"
+   , 7  <$ word "septenary"
+   , 8  <$ word "octonary"
+   , 9  <$ word "nonary"
+   , 10 <$ word "denary"
+   ] <?> "\"unary\", \"binary\', ..."
+
+-- * Keywords
+
+_an :: Prod r Text (Located Token) Location
+_an = word "a" <|> word "an" <?> "indefinite article"
+_and :: Prod r Text (Located Token) Location
+_and = word "and" ? "and"
+_are :: Prod r Text (Located Token) Location
+_are = word "are" ? "are"
+_asFollows :: Prod r Text (Located Token) Location
+_asFollows = word "as" <* word "follows" ? "as follows"
+_assumption :: Prod r Text (Located Token) Location
+_assumption = word "assumption" ? "assumption"
+_be :: Prod r Text (Located Token) Location
+_be = word "be" ? "be"
+_by :: Prod r Text (Located Token) Location
+_by = word "by" ? "by"
+_bySetExt :: Prod r Text (Located Token) Location
+_bySetExt = word "by" <* ((word "set" ? "set") <* word "extensionality") ? "by set extensionality"
+_can :: Prod r Text (Located Token) Location
+_can = word "can" ? "can"
+_consistsOf :: Prod r Text (Located Token) Location
+_consistsOf = word "consists" <* word "of" ? "consists of"
+_contradiction :: Prod r Text (Located Token) Location
+_contradiction = optional (word "a") *> word "contradiction" ? "a contradiction"
+_define :: Prod r Text (Located Token) Location
+_define = word "define" ? "define"
+_definition :: Prod r Text (Located Token) Location
+_definition = word "definition" ? "definition"
+_denote :: Prod r Text (Located Token) Location
+_denote = word "denote" <|> (word "stand" <* word "for") ? "denote"
+_denotes :: Prod r Text (Located Token) Location
+_denotes = word "denotes" ? "denotes"
+_do :: Prod r Text (Located Token) Location
+_do = word "do" ? "do"
+_does :: Prod r Text (Located Token) Location
+_does = word "does" ? "does"
+_either :: Prod r Text (Located Token) Location
+_either = word "either" ? "either"
+_equipped :: Prod r Text (Located Token) Location
+_equipped = (word "equipped" <|> word "together") <* word "with" ? "equipped with"
+_every :: Prod r Text (Located Token) Location
+_every = word "every" ? "every"
+_exist :: Prod r Text (Located Token) Location
+_exist = word "there" <* word "exist" ? "there exist"
+_exists :: Prod r Text (Located Token) Location
+_exists = word "there" <* word "exists" ? "there exists"
+_extends :: Prod r Text (Located Token) Location
+_extends = (_is) <|> (word "consists" <* word "of") ? "consists of"
+_fix :: Prod r Text (Located Token) Location
+_fix = word "fix" ? "fix"
+_follows :: Prod r Text (Located Token) Location
+_follows = word "follows" ? "follows"
+_for :: Prod r Text (Located Token) Location
+_for = word "for" ? "for"
+_forAll :: Prod r Text (Located Token) Location
+_forAll = (word "for" <* word "all") <|> word "all" ? "all"
+_forEvery :: Prod r Text (Located Token) Location
+_forEvery = (word "for" <* word "every") <|> word "every" ? "for every"
+_have :: Prod r Text (Located Token) Location
+_have = word "we" <* word "have" <* optional (word "that") ? "we have"
+_if :: Prod r Text (Located Token) Location
+_if = word "if" ? "if"
+_iff :: Prod r Text (Located Token) Location
+_iff = word "iff" <|> (word "if" <* word "and" <* word "only" <* word "if") ? "iff"
+_inductively :: Prod r Text (Located Token) Location
+_inductively = word "inductively" ? "inductively"
+_is :: Prod r Text (Located Token) Location
+_is = word "is" ? "is"
+_itIsWrong :: Prod r Text (Located Token) Location
+_itIsWrong = word "it" <* word "is" <* (word "not" <* word "the" <* word "case" <|> word "wrong") <* word "that" ? "it is wrong that"
+_let :: Prod r Text (Located Token) Location
+_let = word "let" ? "let"
+_neither :: Prod r Text (Located Token) Location
+_neither = word "neither" ? "neither"
+_no :: Prod r Text (Located Token) Location
+_no = word "no" ? "no"
+_nor :: Prod r Text (Located Token) Location
+_nor = word "nor" ? "nor"
+_not :: Prod r Text (Located Token) Location
+_not = word "not" ? "not"
+_omitted :: Prod r Text (Located Token) Location
+_omitted = word "omitted" ? "omitted"
+_on :: Prod r Text (Located Token) Location
+_on = word "on" ? "on"
+_oneOf :: Prod r Text (Located Token) Location
+_oneOf = word "one" <* word "of" ? "one of"
+_or :: Prod r Text (Located Token) Location
+_or = word "or" ? "or"
+_particularly :: Prod r Text (Located Token) Location
+_particularly = (word "particularly" <|> (word "in" *> word "particular")) <* _comma ? "particularly"
+_relation :: Prod r Text (Located Token) Location
+_relation = word "relation" ? "relation"
+_satisfying :: Prod r Text (Located Token) Location
+_satisfying = _suchThat <|> word "satisfying" ? "satisfying"
+_setOf :: Prod r Text (Located Token) Location
+_setOf = word "set" <* word "of" ? "set of"
+_now :: Prod r Text (Located Token) Location
+_now = (word "then" <|> word "next" <|> word "now" <|> word "first" <|> word "finally" <|> word "subsequently" <|> word "ultimately")
+_show :: Prod r Text (Located Token) Location
+_show = optional _now *> optional (word "we") *> word "show" <* optional (word "that")
+_since :: Prod r Text (Located Token) Location
+_since = word "since" <|> word "because" ? "since"
+_some :: Prod r Text (Located Token) Location
+_some = word "some" ? "some"
+_suchThat :: Prod r Text (Located Token) Location
+_suchThat = ((word "such" <* word "that") <|> (word "s" <* _dot <* word "t" <* _dot)) ? "such that"
+_sufficesThat :: Prod r Text (Located Token) Location
+_sufficesThat = word "it" <* word "suffices" <* word "to" <* word "show" <* word "that" ? "it suffices to show"
+_suppose :: Prod r Text (Located Token) Location
+_suppose = (word "suppose" <|> word "assume") <* optional (word "that") ? "assume"
+_take :: Prod r Text (Located Token) Location
+_take = optional _now *> (word "take" <|> word "consider") ? "take"
+_that :: Prod r Text (Located Token) Location
+_that = word "that" ? "that"
+_the :: Prod r Text (Located Token) Location
+_the = word "the" ? "the"
+_then :: Prod r Text (Located Token) Location
+_then = word "then" ? "then"
+_thus :: Prod r Text (Located Token) Location
+_thus = word "thus" <|> word "hence" <|> _now <|> word "therefore" ? "thus"
+_trivial :: Prod r Text (Located Token) Location
+_trivial = word "straightforward" <|> word "trivial" ? "trivial"
+_unique :: Prod r Text (Located Token) Location
+_unique = word "unique" ? "unique"
+_write :: Prod r Text (Located Token) Location
+_write = (optional (word "we") *> word "say" <* optional (word "that")) <|> (optional (word "we") *> word "write") ? "write"
+
+-- | Introducing plain claims in proofs.
+_haveIntro :: Prod r Text (Located Token) Location
+_haveIntro = _thus <|> _particularly <|> _have
+
+-- * Symbols
+
+_colon :: Prod r Text (Located Token) Location
+_colon = symbol ":" ? ":"
+_pipe :: Prod r Text (Located Token) Location
+_pipe = (optional (command "middle") *> symbol "|") <|> command "mid" ? "\\mid"
+_comma :: Prod r Text (Located Token) Location
+_comma = symbol "," ? ","
+_commaAnd :: Prod r Text (Located Token) Location
+_commaAnd = symbol "," <* optional (word "and") ? ", and"
+_commaOr :: Prod r Text (Located Token) Location
+_commaOr = symbol "," <* optional (word "or") ? ", or"
+_defeq :: Prod r Text (Located Token) Location
+_defeq = symbol ":=" ? ":=" -- Should use `\coloneq` from unicode-math as display.
+_dot :: Prod r Text (Located Token) Location
+_dot = symbol "." ? "."
+_eq :: Prod r Text (Located Token) Location
+_eq = symbol "=" ? "="
+_in :: Prod r Text (Located Token) Location
+_in = command "in" ? "\\in"
+_subseteq :: Prod r Text (Located Token) Location
+_subseteq = command "subseteq" ? "\\subseteq"
+_to :: Prod r Text (Located Token) Location
+_to = command "to" ? "\\to"
+_mapsto :: Prod r Text (Located Token) Location
+_mapsto = command "mapsto" ? "\\mapsto"
+_ampersand :: Prod r Text (Located Token) Location
+_ampersand = symbol "&" ? "&"
diff --git a/source/Felix/Syntax/Interface.hs b/source/Felix/Syntax/Interface.hs
new file mode 100644
index 0000000..1820705
--- /dev/null
+++ b/source/Felix/Syntax/Interface.hs
@@ -0,0 +1,887 @@
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+
+module Felix.Syntax.Interface
+    ( MixfixLevel
+    , mixfixLevel
+    , mixfixLevelValue
+    , MixfixLevelError(..)
+    , Fixity(..)
+    , sourcePragmaFixity
+    , CanonicalLexicalEntry(..)
+    , canonicalLexicalSurfacePatterns
+    , eligibleExpressionPattern
+    , CanonicalSyntaxDelta
+    , canonicalSyntaxDelta
+    , canonicalSyntaxDeltaEntries
+    , canonicalSyntaxDeltaSize
+    , CanonicalSyntaxCollision
+    , canonicalCollisionPattern
+    , canonicalCollisionEntries
+    , CanonicalSyntaxDeltaId
+    , canonicalSyntaxDeltaId
+    , canonicalSyntaxDeltaIdDigest
+    , BaseSyntaxInterfaceId
+    , baseSyntaxInterfaceId
+    , baseSyntaxInterfaceIdDigest
+    , baseSyntaxManifest
+    , fixedBaseSyntaxEntries
+    , SyntaxInterfaceId
+    , syntaxInterfaceIdDigest
+    , ModuleSyntaxInterface
+    , moduleSyntaxInterface
+    , moduleSyntaxBase
+    , moduleSyntaxDirectInputs
+    , moduleSyntaxLocalDelta
+    , moduleSyntaxAssertedId
+    , SyntaxInterfaceError(..)
+    , validateModuleSyntaxInterface
+    , putCanonicalLexicalEntryCache
+    , getCanonicalLexicalEntryCache
+    , putPatternCache
+    , getPatternCache
+    , putTokenCache
+    , getTokenCache
+    , putCanonicalSyntaxDeltaCache
+    , getCanonicalSyntaxDeltaCache
+    , putModuleSyntaxInterfaceCache
+    , getModuleSyntaxInterfaceCache
+    , putBaseSyntaxInterfaceIdCache
+    , getBaseSyntaxInterfaceIdCache
+    , putSyntaxInterfaceIdCache
+    , getSyntaxInterfaceIdCache
+    ) where
+
+import Base
+
+import Felix.Cache.Codec
+import Felix.Syntax.Abstract
+import Felix.Syntax.Lexicon
+import Felix.Syntax.Pragma
+
+import Control.DeepSeq (NFData)
+import Control.Monad (unless)
+import Data.List qualified as List
+import Data.List.NonEmpty qualified as NonEmpty
+import Data.Map.Strict qualified as Map
+import Data.Set qualified as Set
+import Data.Word (Word8)
+import Numeric.Natural (Natural)
+
+
+newtype MixfixLevel = MixfixLevel Word8
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving newtype (Hashable, NFData)
+
+data MixfixLevelError
+    = MixfixLevelOutOfRange !Word8
+    deriving stock (Show, Eq)
+
+mixfixLevel :: Word8 -> Either MixfixLevelError MixfixLevel
+mixfixLevel supplied
+    | supplied <= 9 =
+        Right (MixfixLevel supplied)
+    | otherwise =
+        Left (MixfixLevelOutOfRange supplied)
+
+mixfixLevelValue :: MixfixLevel -> Word8
+mixfixLevelValue (MixfixLevel level) =
+    level
+
+data Fixity = Fixity
+    { fixityAssociativity :: !Associativity
+    , fixityLevel :: !MixfixLevel
+    } deriving stock (Show, Eq, Ord, Generic)
+      deriving anyclass (NFData)
+
+sourcePragmaFixity :: SyntaxPragma -> Fixity
+sourcePragmaFixity pragma =
+    Fixity
+        (syntaxPragmaAssociativity pragma)
+        (MixfixLevel
+            (sourceMixfixLevelValue
+                (syntaxPragmaLevel pragma)))
+
+-- | Complete origin-free lexical semantics produced by scanning.
+data CanonicalLexicalEntry
+    = CanonicalLeftAdjective !Pattern !Marker
+    | CanonicalRightAdjective !Pattern !Marker
+    | CanonicalFunctionPhrase !Pattern !Pattern !Marker
+    | CanonicalNoun !Pattern !Pattern !Marker
+    | CanonicalStructureNoun !Pattern !Pattern !Marker
+    | CanonicalVerb !Pattern !Pattern !Marker
+    | CanonicalRelation !Token !ParameterArity !Marker
+    | CanonicalExpressionFunction !Pattern !Marker !Fixity
+    | CanonicalPrefixPredicate !Text !Natural !Marker
+    | CanonicalStructureOperation !Text
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving anyclass (NFData)
+
+-- | Every surface pattern through which the concrete parser can select an
+-- entry. Equal singular and plural surfaces are returned only once.
+canonicalLexicalSurfacePatterns
+    :: CanonicalLexicalEntry
+    -> NonEmpty Pattern
+canonicalLexicalSurfacePatterns =
+    deduplicatePatterns . \case
+    CanonicalLeftAdjective pat _marker ->
+        [pat]
+    CanonicalRightAdjective pat _marker ->
+        [pat]
+    CanonicalFunctionPhrase singular _plural _marker ->
+        [singular]
+    CanonicalNoun singular plural _marker ->
+        [singular, plural]
+    CanonicalStructureNoun singular _plural _marker ->
+        [singular]
+    CanonicalVerb singular plural _marker ->
+        [singular, plural]
+    CanonicalRelation token arity marker ->
+        [ relationSymbolPattern
+            (RelationSymbol token arity marker)
+        ]
+    CanonicalExpressionFunction pat _marker _fixity ->
+        [pat]
+    CanonicalPrefixPredicate command _arity _marker ->
+        [ prefixPredicatePattern
+            (PrefixPredicate command 0)
+        ]
+    CanonicalStructureOperation command ->
+        [structSymbolPattern (StructSymbol command)]
+  where
+    deduplicatePatterns patterns =
+        case NonEmpty.nonEmpty
+                (Set.toList (Set.fromList patterns)) of
+            Just nonempty ->
+                nonempty
+            Nothing ->
+                impossible
+                    "canonical lexical entry has no parser surface"
+
+eligibleExpressionPattern :: Pattern -> Bool
+eligibleExpressionPattern pat =
+    case patternToHoley pat of
+        Nothing : rest ->
+            case reverse rest of
+                Nothing : middleReversed ->
+                    let middle =
+                            reverse middleReversed
+                    in
+                        countHoles middle == 0
+                            && any isJust middle
+                _ ->
+                    False
+        _ ->
+            False
+  where
+    countHoles =
+        length . List.filter isNothing
+
+newtype CanonicalSyntaxDelta =
+    CanonicalSyntaxDelta
+        [CanonicalLexicalEntry]
+    deriving stock (Show, Eq, Generic)
+    deriving anyclass (NFData)
+
+data CanonicalSyntaxCollision = CanonicalSyntaxCollision
+    { canonicalCollisionPattern :: !Pattern
+    , canonicalCollisionEntries
+        :: !(NonEmpty CanonicalLexicalEntry)
+    } deriving stock (Show, Eq)
+
+canonicalSyntaxDelta
+    :: [CanonicalLexicalEntry]
+    -> Either CanonicalSyntaxCollision CanonicalSyntaxDelta
+canonicalSyntaxDelta supplied =
+    case orderedCollisions of
+        [] ->
+            Right (CanonicalSyntaxDelta orderedEntries)
+        (_encodedPattern, pat, entries) : _ ->
+            Left
+                (CanonicalSyntaxCollision
+                    pat
+                    (case NonEmpty.nonEmpty
+                        (canonicalEntryOrder
+                            (Set.toList entries)) of
+                        Just collisionEntries ->
+                            collisionEntries
+                        Nothing ->
+                            impossible
+                                "canonical syntax collision has no entries"))
+  where
+    orderedEntries =
+        canonicalEntryOrder
+            (Set.toList (Set.fromList supplied))
+
+    grouped =
+        foldl'
+            (\entries entry ->
+                foldl'
+                    (\indexed pat ->
+                        Map.insertWith
+                            Set.union
+                            pat
+                            (Set.singleton entry)
+                            indexed)
+                    entries
+                    (canonicalLexicalSurfacePatterns entry))
+            mempty
+            orderedEntries
+
+    orderedCollisions =
+        List.sortOn
+            (\(encodedPattern, _pattern, _entries) ->
+                encodedPattern)
+            [ ( encodeCache (putPatternCache pat)
+              , pat
+              , entries
+              )
+            | (pat, entries) <- Map.toList grouped
+            , Set.size entries > 1
+            ]
+
+canonicalSyntaxDeltaEntries
+    :: CanonicalSyntaxDelta
+    -> [CanonicalLexicalEntry]
+canonicalSyntaxDeltaEntries
+        (CanonicalSyntaxDelta entries) =
+    entries
+
+canonicalSyntaxDeltaSize :: CanonicalSyntaxDelta -> Int
+canonicalSyntaxDeltaSize
+        (CanonicalSyntaxDelta entries) =
+    length entries
+
+canonicalEntryOrder
+    :: [CanonicalLexicalEntry]
+    -> [CanonicalLexicalEntry]
+canonicalEntryOrder =
+    List.sortOn
+        (encodeCache . putCanonicalLexicalEntryCache)
+
+newtype CanonicalSyntaxDeltaId =
+    CanonicalSyntaxDeltaId CacheDigest
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving newtype (Hashable, NFData)
+
+canonicalSyntaxDeltaId
+    :: CanonicalSyntaxDelta
+    -> CanonicalSyntaxDeltaId
+canonicalSyntaxDeltaId delta =
+    CanonicalSyntaxDeltaId
+        (hashCacheFields
+            "felix-syntax-delta-v1"
+            [encodeCache
+                (putCanonicalSyntaxDeltaCache delta)])
+
+canonicalSyntaxDeltaIdDigest
+    :: CanonicalSyntaxDeltaId
+    -> CacheDigest
+canonicalSyntaxDeltaIdDigest
+        (CanonicalSyntaxDeltaId digest) =
+    digest
+
+newtype BaseSyntaxInterfaceId =
+    BaseSyntaxInterfaceId CacheDigest
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving newtype (Hashable, NFData)
+
+baseSyntaxInterfaceId :: BaseSyntaxInterfaceId
+baseSyntaxInterfaceId =
+    BaseSyntaxInterfaceId
+        (hashCacheFields
+            "felix-base-syntax-interface-v1"
+            [encodeCache
+                (putCacheList
+                    putManifestRow
+                    baseSyntaxManifest)])
+  where
+    putManifestRow =
+        putCacheList putCanonicalLexicalEntryCache
+            . canonicalEntryOrder
+
+baseSyntaxInterfaceIdDigest
+    :: BaseSyntaxInterfaceId
+    -> CacheDigest
+baseSyntaxInterfaceIdDigest
+        (BaseSyntaxInterfaceId digest) =
+    digest
+
+baseSyntaxManifest :: [[CanonicalLexicalEntry]]
+baseSyntaxManifest =
+    case traverse makeRow
+            (zip [0 :: Word8 ..] builtinMixfixLevels) of
+        Right rows
+            | length rows == 10 ->
+                rows
+        _ ->
+            impossible
+                "the fixed mixfix manifest does not have ten valid rows"
+  where
+    makeRow (row, entries) = do
+        level <- mixfixLevel row
+        pure
+            [ CanonicalExpressionFunction
+                pat
+                marker
+                (Fixity associativity level)
+            | MixfixItem pat marker associativity <-
+                entries
+            ]
+
+-- | Every fixed lexical entry consulted by the concrete parser. The base
+-- syntax identity above commits to the ten expression rows; the remaining
+-- fixed categories are compiler input covered by the cache epoch.
+fixedBaseSyntaxEntries :: [CanonicalLexicalEntry]
+fixedBaseSyntaxEntries =
+    case canonicalSyntaxDelta rawEntries of
+        Right delta ->
+            canonicalSyntaxDeltaEntries delta
+        Left collision ->
+            impossible
+                ("fixed base syntax contains a collision: "
+                    <> show collision)
+  where
+    rawEntries =
+        concat baseSyntaxManifest
+            <> (canonicalAdjective CanonicalLeftAdjective
+                    <$> lexiconAdjLs builtins)
+            <> (canonicalAdjective CanonicalRightAdjective
+                    <$> lexiconAdjRs builtins)
+            <> (canonicalSgPl CanonicalFunctionPhrase
+                    <$> lexiconFuns builtins)
+            <> (canonicalSgPl CanonicalNoun
+                    <$> lexiconNouns builtins)
+            <> (canonicalSgPl CanonicalStructureNoun
+                    <$> lexiconStructNouns builtins)
+            <> (canonicalSgPl CanonicalVerb
+                    <$> lexiconVerbs builtins)
+            <> (canonicalRelation
+                    <$> lexiconRelationSymbols builtins)
+            <> (canonicalPrefix
+                    <$> lexiconPrefixPredicates builtins)
+            <> (canonicalStructure
+                    <$> lexiconStructFun builtins)
+
+    canonicalAdjective constructor item =
+        constructor
+            (lexicalItemPattern item)
+            (lexicalItemMarker item)
+
+    canonicalSgPl constructor item =
+        let patterns =
+                lexicalItemSgPlPattern item
+        in
+            constructor
+                (sg patterns)
+                (pl patterns)
+                (lexicalItemSgPlMarker item)
+
+    canonicalRelation relation =
+        CanonicalRelation
+            (relationSymbolToken relation)
+            (relationSymbolParameterArity relation)
+            (relationSymbolMarker relation)
+
+    canonicalPrefix
+            (PrefixPredicate command arity, marker) =
+        CanonicalPrefixPredicate
+            command
+            (fromIntegral arity)
+            marker
+
+    canonicalStructure (StructSymbol command) =
+        CanonicalStructureOperation command
+
+newtype SyntaxInterfaceId =
+    SyntaxInterfaceId CacheDigest
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving newtype (Hashable, NFData)
+
+syntaxInterfaceIdDigest :: SyntaxInterfaceId -> CacheDigest
+syntaxInterfaceIdDigest (SyntaxInterfaceId digest) =
+    digest
+
+data ModuleSyntaxInterface = ModuleSyntaxInterface
+    !BaseSyntaxInterfaceId
+    ![SyntaxInterfaceId]
+    !CanonicalSyntaxDelta
+    !SyntaxInterfaceId
+    deriving stock (Show, Eq, Generic)
+    deriving anyclass (NFData)
+
+moduleSyntaxBase
+    :: ModuleSyntaxInterface
+    -> BaseSyntaxInterfaceId
+moduleSyntaxBase
+        (ModuleSyntaxInterface base _direct _delta _asserted) =
+    base
+
+moduleSyntaxDirectInputs
+    :: ModuleSyntaxInterface
+    -> [SyntaxInterfaceId]
+moduleSyntaxDirectInputs
+        (ModuleSyntaxInterface _base direct _delta _asserted) =
+    direct
+
+moduleSyntaxLocalDelta
+    :: ModuleSyntaxInterface
+    -> CanonicalSyntaxDelta
+moduleSyntaxLocalDelta
+        (ModuleSyntaxInterface _base _direct delta _asserted) =
+    delta
+
+moduleSyntaxAssertedId
+    :: ModuleSyntaxInterface
+    -> SyntaxInterfaceId
+moduleSyntaxAssertedId
+        (ModuleSyntaxInterface _base _direct _delta asserted) =
+    asserted
+
+data SyntaxInterfaceError
+    = DuplicateDirectSyntaxInterface !SyntaxInterfaceId
+    | UnexpectedBaseSyntaxInterface
+        !BaseSyntaxInterfaceId
+        !BaseSyntaxInterfaceId
+    | SyntaxInterfaceIdMismatch
+        !SyntaxInterfaceId
+        !SyntaxInterfaceId
+    deriving stock (Show, Eq)
+
+moduleSyntaxInterface
+    :: [SyntaxInterfaceId]
+    -> CanonicalSyntaxDelta
+    -> Either SyntaxInterfaceError ModuleSyntaxInterface
+moduleSyntaxInterface direct delta =
+    validateModuleSyntaxInterface
+        baseSyntaxInterfaceId
+        direct
+        delta
+        (computeSyntaxInterfaceId
+            baseSyntaxInterfaceId
+            direct
+            delta)
+
+validateModuleSyntaxInterface
+    :: BaseSyntaxInterfaceId
+    -> [SyntaxInterfaceId]
+    -> CanonicalSyntaxDelta
+    -> SyntaxInterfaceId
+    -> Either SyntaxInterfaceError ModuleSyntaxInterface
+validateModuleSyntaxInterface base direct delta asserted = do
+    unless
+        (base == baseSyntaxInterfaceId)
+        (Left
+            (UnexpectedBaseSyntaxInterface
+                base
+                baseSyntaxInterfaceId))
+    case firstDuplicate direct of
+        Just duplicate ->
+            Left
+                (DuplicateDirectSyntaxInterface duplicate)
+        Nothing ->
+            pure ()
+    let computed =
+            computeSyntaxInterfaceId base direct delta
+    unless
+        (asserted == computed)
+        (Left
+            (SyntaxInterfaceIdMismatch
+                asserted
+                computed))
+    Right
+        (ModuleSyntaxInterface
+            base
+            direct
+            delta
+            asserted)
+
+computeSyntaxInterfaceId
+    :: BaseSyntaxInterfaceId
+    -> [SyntaxInterfaceId]
+    -> CanonicalSyntaxDelta
+    -> SyntaxInterfaceId
+computeSyntaxInterfaceId base direct delta =
+    SyntaxInterfaceId
+        (hashCacheFields
+            "felix-syntax-interface-v1"
+            [ cacheDigestBytes
+                (baseSyntaxInterfaceIdDigest base)
+            , encodeCache
+                (putCacheList
+                    putSyntaxInterfaceIdCache
+                    direct)
+            , cacheDigestBytes
+                (canonicalSyntaxDeltaIdDigest
+                    (canonicalSyntaxDeltaId delta))
+            ])
+
+firstDuplicate :: Ord value => [value] -> Maybe value
+firstDuplicate =
+    go mempty
+  where
+    go _seen [] =
+        Nothing
+    go seen (value : rest)
+        | value `Set.member` seen =
+            Just value
+        | otherwise =
+            go (Set.insert value seen) rest
+
+putCanonicalLexicalEntryCache
+    :: CanonicalLexicalEntry
+    -> CachePut
+putCanonicalLexicalEntryCache = \case
+    CanonicalLeftAdjective pat marker -> do
+        putCacheTag 0x00
+        putPatternCache pat
+        putMarkerCache marker
+    CanonicalRightAdjective pat marker -> do
+        putCacheTag 0x01
+        putPatternCache pat
+        putMarkerCache marker
+    CanonicalFunctionPhrase singular plural marker -> do
+        putCacheTag 0x02
+        putPatternCache singular
+        putPatternCache plural
+        putMarkerCache marker
+    CanonicalNoun singular plural marker -> do
+        putCacheTag 0x03
+        putPatternCache singular
+        putPatternCache plural
+        putMarkerCache marker
+    CanonicalStructureNoun singular plural marker -> do
+        putCacheTag 0x04
+        putPatternCache singular
+        putPatternCache plural
+        putMarkerCache marker
+    CanonicalVerb singular plural marker -> do
+        putCacheTag 0x05
+        putPatternCache singular
+        putPatternCache plural
+        putMarkerCache marker
+    CanonicalRelation token arity marker -> do
+        putCacheTag 0x06
+        putTokenCache token
+        putCacheNatural (parameterArityValue arity)
+        putMarkerCache marker
+    CanonicalExpressionFunction pat marker fixity -> do
+        putCacheTag 0x07
+        putPatternCache pat
+        putMarkerCache marker
+        putFixityCache fixity
+    CanonicalPrefixPredicate command arity marker -> do
+        putCacheTag 0x08
+        putCacheText command
+        putCacheNatural arity
+        putMarkerCache marker
+    CanonicalStructureOperation command -> do
+        putCacheTag 0x09
+        putCacheText command
+
+getCanonicalLexicalEntryCache
+    :: CacheGet CanonicalLexicalEntry
+getCanonicalLexicalEntryCache =
+    getCacheTag >>= \case
+        0x00 ->
+            CanonicalLeftAdjective
+                <$> getPatternCache
+                <*> getMarkerCache
+        0x01 ->
+            CanonicalRightAdjective
+                <$> getPatternCache
+                <*> getMarkerCache
+        0x02 ->
+            CanonicalFunctionPhrase
+                <$> getPatternCache
+                <*> getPatternCache
+                <*> getMarkerCache
+        0x03 ->
+            CanonicalNoun
+                <$> getPatternCache
+                <*> getPatternCache
+                <*> getMarkerCache
+        0x04 ->
+            CanonicalStructureNoun
+                <$> getPatternCache
+                <*> getPatternCache
+                <*> getMarkerCache
+        0x05 ->
+            CanonicalVerb
+                <$> getPatternCache
+                <*> getPatternCache
+                <*> getMarkerCache
+        0x06 ->
+            CanonicalRelation
+                <$> getTokenCache
+                <*> (ParameterArity <$> getCacheNatural)
+                <*> getMarkerCache
+        0x07 ->
+            CanonicalExpressionFunction
+                <$> getPatternCache
+                <*> getMarkerCache
+                <*> getFixityCache
+        0x08 ->
+            CanonicalPrefixPredicate
+                <$> getCacheText
+                <*> getCacheNatural
+                <*> getMarkerCache
+        0x09 ->
+            CanonicalStructureOperation
+                <$> getCacheText
+        tag ->
+            fail
+                ("unknown canonical lexical entry tag "
+                    <> show tag)
+
+putCanonicalSyntaxDeltaCache
+    :: CanonicalSyntaxDelta
+    -> CachePut
+putCanonicalSyntaxDeltaCache
+        (CanonicalSyntaxDelta entries) =
+    putCacheList putCanonicalLexicalEntryCache entries
+
+getCanonicalSyntaxDeltaCache
+    :: CacheGet CanonicalSyntaxDelta
+getCanonicalSyntaxDeltaCache = do
+    supplied <- getCacheList getCanonicalLexicalEntryCache
+    case canonicalSyntaxDelta supplied of
+        Left collision ->
+            fail
+                ("colliding cached canonical syntax entries: "
+                    <> show collision)
+        Right delta
+            | canonicalSyntaxDeltaEntries delta == supplied ->
+                pure delta
+            | otherwise ->
+                fail
+                    "cached canonical syntax entries are not in canonical order"
+
+putModuleSyntaxInterfaceCache
+    :: ModuleSyntaxInterface
+    -> CachePut
+putModuleSyntaxInterfaceCache
+        (ModuleSyntaxInterface base direct delta asserted) = do
+    putBaseSyntaxInterfaceIdCache base
+    putCacheList putSyntaxInterfaceIdCache direct
+    putCanonicalSyntaxDeltaCache delta
+    putSyntaxInterfaceIdCache asserted
+
+getModuleSyntaxInterfaceCache
+    :: CacheGet ModuleSyntaxInterface
+getModuleSyntaxInterfaceCache = do
+    base <- getBaseSyntaxInterfaceIdCache
+    direct <- getCacheList getSyntaxInterfaceIdCache
+    delta <- getCanonicalSyntaxDeltaCache
+    asserted <- getSyntaxInterfaceIdCache
+    case
+        validateModuleSyntaxInterface
+            base
+            direct
+            delta
+            asserted of
+        Left err ->
+            fail
+                ("invalid module syntax interface: "
+                    <> show err)
+        Right interface ->
+            pure interface
+
+putBaseSyntaxInterfaceIdCache
+    :: BaseSyntaxInterfaceId
+    -> CachePut
+putBaseSyntaxInterfaceIdCache
+        (BaseSyntaxInterfaceId digest) =
+    putCacheDigest digest
+
+getBaseSyntaxInterfaceIdCache
+    :: CacheGet BaseSyntaxInterfaceId
+getBaseSyntaxInterfaceIdCache =
+    BaseSyntaxInterfaceId <$> getCacheDigest
+
+putSyntaxInterfaceIdCache
+    :: SyntaxInterfaceId
+    -> CachePut
+putSyntaxInterfaceIdCache
+        (SyntaxInterfaceId digest) =
+    putCacheDigest digest
+
+getSyntaxInterfaceIdCache
+    :: CacheGet SyntaxInterfaceId
+getSyntaxInterfaceIdCache =
+    SyntaxInterfaceId <$> getCacheDigest
+
+putFixityCache :: Fixity -> CachePut
+putFixityCache (Fixity associativity level) = do
+    putAssociativityCache associativity
+    putCacheTag (mixfixLevelValue level)
+
+getFixityCache :: CacheGet Fixity
+getFixityCache = do
+    associativity <- getAssociativityCache
+    suppliedLevel <- getCacheTag
+    case mixfixLevel suppliedLevel of
+        Left err ->
+            fail ("invalid cached mixfix level: " <> show err)
+        Right level ->
+            pure (Fixity associativity level)
+
+putAssociativityCache :: Associativity -> CachePut
+putAssociativityCache =
+    putCacheTag . \case
+        LeftAssoc ->
+            0x00
+        RightAssoc ->
+            0x01
+        NonAssoc ->
+            0x02
+
+getAssociativityCache :: CacheGet Associativity
+getAssociativityCache =
+    getCacheTag >>= \case
+        0x00 ->
+            pure LeftAssoc
+        0x01 ->
+            pure RightAssoc
+        0x02 ->
+            pure NonAssoc
+        tag ->
+            fail
+                ("unknown associativity tag " <> show tag)
+
+putMarkerCache :: Marker -> CachePut
+putMarkerCache (Marker marker) =
+    putCacheText marker
+
+getMarkerCache :: CacheGet Marker
+getMarkerCache =
+    Marker <$> getCacheText
+
+putPatternCache :: Pattern -> CachePut
+putPatternCache = \case
+    End ->
+        putCacheTag 0x00
+    HoleCons rest -> do
+        putCacheTag 0x01
+        putPatternCache rest
+    TokenCons token rest -> do
+        putCacheTag 0x02
+        putTokenCache token
+        putPatternCache rest
+
+getPatternCache :: CacheGet Pattern
+getPatternCache =
+    getCacheTag >>= \case
+        0x00 ->
+            pure End
+        0x01 ->
+            HoleCons <$> getPatternCache
+        0x02 ->
+            TokenCons
+                <$> getTokenCache
+                <*> getPatternCache
+        tag ->
+            fail
+                ("unknown lexical pattern tag " <> show tag)
+
+putTokenCache :: Token -> CachePut
+putTokenCache = \case
+    Word text -> do
+        putCacheTag 0x00
+        putCacheText text
+    Variable text -> do
+        putCacheTag 0x01
+        putCacheText text
+    Symbol text -> do
+        putCacheTag 0x02
+        putCacheText text
+    Integer integer -> do
+        putCacheTag 0x03
+        putCacheInteger (toInteger integer)
+    Command text -> do
+        putCacheTag 0x04
+        putCacheText text
+    Label text -> do
+        putCacheTag 0x05
+        putCacheText text
+    Ref references -> do
+        putCacheTag 0x06
+        putCacheList putCacheText (toList references)
+    BeginEnv text -> do
+        putCacheTag 0x07
+        putCacheText text
+    EndEnv text -> do
+        putCacheTag 0x08
+        putCacheText text
+    ParenL ->
+        putCacheTag 0x09
+    ParenR ->
+        putCacheTag 0x0a
+    BracketL ->
+        putCacheTag 0x0b
+    BracketR ->
+        putCacheTag 0x0c
+    VisibleBraceL ->
+        putCacheTag 0x0d
+    VisibleBraceR ->
+        putCacheTag 0x0e
+    InvisibleBraceL ->
+        putCacheTag 0x0f
+    InvisibleBraceR ->
+        putCacheTag 0x10
+
+getTokenCache :: CacheGet Token
+getTokenCache =
+    getCacheTag >>= \case
+        0x00 ->
+            Word <$> getCacheText
+        0x01 ->
+            Variable <$> getCacheText
+        0x02 ->
+            Symbol <$> getCacheText
+        0x03 ->
+            Integer <$> getCacheInt
+        0x04 ->
+            Command <$> getCacheText
+        0x05 ->
+            Label <$> getCacheText
+        0x06 -> do
+            references <- getCacheList getCacheText
+            case NonEmpty.nonEmpty references of
+                Nothing ->
+                    fail "cached reference token has no marker"
+                Just nonempty ->
+                    pure (Ref nonempty)
+        0x07 ->
+            BeginEnv <$> getCacheText
+        0x08 ->
+            EndEnv <$> getCacheText
+        0x09 ->
+            pure ParenL
+        0x0a ->
+            pure ParenR
+        0x0b ->
+            pure BracketL
+        0x0c ->
+            pure BracketR
+        0x0d ->
+            pure VisibleBraceL
+        0x0e ->
+            pure VisibleBraceR
+        0x0f ->
+            pure InvisibleBraceL
+        0x10 ->
+            pure InvisibleBraceR
+        tag ->
+            fail ("unknown lexical token tag " <> show tag)
+
+getCacheInt :: CacheGet Int
+getCacheInt = do
+    integer <- getCacheInteger
+    if integer < toInteger (minBound :: Int)
+        || integer > toInteger (maxBound :: Int)
+        then
+            fail "cached integer token exceeds Int"
+        else
+            pure (fromInteger integer)
diff --git a/source/Felix/Syntax/Internal.hs b/source/Felix/Syntax/Internal.hs
new file mode 100644
index 0000000..d129947
--- /dev/null
+++ b/source/Felix/Syntax/Internal.hs
@@ -0,0 +1,830 @@
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE ViewPatterns #-}
+
+-- | Data types for the internal (semantic) syntax tree.
+module Felix.Syntax.Internal
+    ( module Felix.Syntax.Internal
+    , module Felix.Syntax.Abstract
+    , module Felix.Syntax.LexicalPhrase
+    , module Felix.Syntax.Token
+    ) where
+
+
+import Base
+import Felix.Syntax.Lexicon
+    ( pattern PairSymbol
+    , pattern UnionsSymbol
+    , pattern UpairSymbol
+    )
+import Felix.Syntax.LexicalPhrase (unsafeReadPhrase, unsafeReadPhraseSgPl)
+import Felix.Syntax.Token (Token(..))
+import Felix.Report.Location
+
+import Felix.Syntax.Abstract
+    ( Chain(..)
+    , Associativity(..)
+    , Connective(..)
+    , VarSymbol(..)
+    , pattern NamedVar
+    , pattern FreshVar
+    , FunctionSymbol
+    , SymbolPattern(..)
+    , MixfixItem(..)
+    , Pattern(..)
+    , LexicalItem
+    , LexicalItemSgPl
+    , RelationSymbol(..)
+    , ParameterArity(..)
+    , PrefixPredicate(..)
+    , StructSymbol (..)
+    , Relation
+    , PropositionalConstant(..)
+    , StructPhrase
+    , Justification(..)
+    , Marker(..)
+    , markerFromToken
+    , lexicalItemMarker
+    , lexicalItemSgPlMarker
+    , mkLexicalItem
+    , mkLexicalItemSgPl
+    , relationSymbolMarker
+    , relationSymbolParameterArity
+    , relationSymbolToken
+    , parameterArityOf
+    , parameterArityValue
+    , zeroParameterArity
+    , mixfixMarker
+    , mkMixfixItem
+    , pattern CarrierSymbol, pattern ConsSymbol, pattern ElementSymbol
+    , pattern NotElementSymbol, pattern EqSymbol, pattern NeqSymbol, pattern SubseteqSymbol
+    )
+
+import Bound
+import Bound.Scope
+import Data.Deriving (deriveShow1, deriveEq1, deriveOrd1)
+import Data.Hashable.Lifted
+import Data.HashMap.Strict qualified as HM
+import Data.List qualified as List
+import Data.List.NonEmpty qualified as NonEmpty
+import Data.Set qualified as Set
+
+-- | 'Symbol's can be used as function and relation symbols.
+data Symbol
+    = SymbolMixfix FunctionSymbol
+    | SymbolFun LexicalItemSgPl
+    | SymbolInteger Int
+    | SymbolPredicate Predicate
+    deriving (Show, Eq, Ord, Generic, Hashable)
+
+
+data Predicate
+    = PredicateAdj LexicalItem
+    | PredicateVerb LexicalItemSgPl
+    | PredicateNoun LexicalItemSgPl -- ^ /@\<...\> is a \<...\>@/.
+    | PredicateRelation RelationSymbol
+    | PredicateSymbol Text
+    | PredicateNounStruct LexicalItemSgPl -- ^ /@\<...\> is a \<...\>@/.
+    deriving (Show, Eq, Ord, Generic, Hashable)
+
+
+-- | The object-language marker of an ownable symbol.
+objectSymbolMarker :: Symbol -> Maybe Marker
+objectSymbolMarker = \case
+    SymbolMixfix symbol ->
+        Just (mixfixMarker symbol)
+    SymbolFun symbol ->
+        Just (lexicalItemSgPlMarker symbol)
+    SymbolInteger{} ->
+        Nothing
+    SymbolPredicate predicate ->
+        Just (predicateObjectMarker predicate)
+
+-- | The object-language marker of a predicate.
+predicateObjectMarker :: Predicate -> Marker
+predicateObjectMarker = \case
+    PredicateAdj item ->
+        lexicalItemMarker item
+    PredicateVerb item ->
+        lexicalItemSgPlMarker item
+    PredicateNoun item ->
+        lexicalItemSgPlMarker item
+    PredicateRelation relation ->
+        relationSymbolMarker relation
+    PredicateSymbol text ->
+        Marker text
+    PredicateNounStruct item ->
+        lexicalItemSgPlMarker item
+
+
+data Quantifier
+    = Universally
+    | Existentially
+    deriving (Show, Eq, Ord, Generic, Hashable)
+
+type Formula = Term
+type Term = Expr
+type Expr = ExprOf VarSymbol
+
+
+-- | Internal higher-order expressions.
+data ExprOf a
+    = TermVar a
+    -- ^ Fresh constants disjoint from all user-named identifiers.
+    -- These can be used to eliminate higher-order constructs.
+    --
+    | TermSymbol Location Symbol [ExprOf a]
+    -- ^ Application of a symbol (including function and predicate symbols).
+    | TermSymbolStruct StructSymbol (Maybe (ExprOf a))
+    --
+    | Apply (ExprOf a) (NonEmpty (ExprOf a))
+    -- ^ Higher-order application.
+    --
+    | TermSep VarSymbol (ExprOf a) (Scope () ExprOf a)
+    -- ^ Set comprehension using seperation, e.g.: /@{ x ∈ X | P(x) }@/.
+    --
+    | ReplacePred VarSymbol VarSymbol (ExprOf a) (Scope ReplacementVar ExprOf a)
+    -- ^ Replacement for single-valued predicates. The concrete syntax for these
+    -- syntactically requires a bounded existential quantifier in the condition:
+    --
+    -- /@$\\{ y | \\exists x\\in A. P(x,y) \\}$@/
+    --
+    -- In definitions the single-valuedness of @P@ becomes a proof obligation.
+    -- In other cases we could instead add it as constraint
+    --
+    -- /@$b\\in \\{ y | \\exists x\\in A. P(x,y) \\}$@/
+    -- /@iff@/
+    -- /@$\\exists x\\in A. P(x,y)$ and $P$ is single valued@/
+    --
+    --
+    | ReplaceFun (NonEmpty (VarSymbol, ExprOf a)) (Scope VarSymbol ExprOf a) (Scope VarSymbol ExprOf a)
+    -- ^ Set comprehension using functional replacement,
+    -- e.g.: /@{ f(x, y) | x ∈ X; y ∈ Y; P(x, y) }@/.
+    -- The list of pairs gives the domains, the integers in the scope point to list indices.
+    -- The first scope is the lhs, the optional scope can be used for additional constraints
+    -- on the variables (i.e. implicit separation over the product of the domains).
+    -- An out-of-bound index is an error, since otherwise replacement becomes unsound.
+    --
+    | Connected Connective (ExprOf a) (ExprOf a)
+    | Lambda (Scope VarSymbol ExprOf a)
+    | Quantified Quantifier (Scope VarSymbol ExprOf a)
+    | PropositionalConstant PropositionalConstant
+    | Not Location (ExprOf a)
+    deriving (Functor, Foldable, Traversable)
+
+-- | Best source location carried by an elaborated expression.
+exprLocation :: Expr -> Location
+exprLocation = \case
+    TermVar variable -> locate variable
+    TermSymbol location _symbol _arguments -> location
+    TermSymbolStruct _symbol expression ->
+        maybe Nowhere exprLocation expression
+    Apply function _arguments -> exprLocation function
+    TermSep variable _bound _predicate -> locate variable
+    ReplacePred value _domain _bound _predicate -> locate value
+    ReplaceFun ((variable, _domain) :| _remaining) _value _condition ->
+        locate variable
+    Connected _connective left _right -> exprLocation left
+    Lambda{} -> Nowhere
+    Quantified{} -> Nowhere
+    PropositionalConstant{} -> Nowhere
+    Not location _term -> location
+
+data ReplacementVar = ReplacementDomVar | ReplacementRangeVar deriving (Show, Eq, Ord, Generic, Hashable)
+
+makeBound ''ExprOf
+
+deriveShow1 ''ExprOf
+deriveEq1   ''ExprOf
+deriveOrd1  ''ExprOf
+
+deriving instance Show a => Show (ExprOf a)
+deriving instance Eq   a => Eq   (ExprOf a)
+deriving instance Ord  a => Ord  (ExprOf a)
+
+deriving instance Generic (ExprOf a)
+deriving instance Generic1 ExprOf
+
+deriving instance Hashable1 ExprOf
+
+deriving instance Hashable a =>  Hashable (ExprOf a)
+
+mentionedSymbols :: ExprOf a -> Set Symbol
+mentionedSymbols = \case
+    TermVar{} ->
+        mempty
+    TermSymbol _loc symbol args ->
+        Set.insert symbol (Set.unions (mentionedSymbols <$> args))
+    TermSymbolStruct _symbol expr ->
+        maybe mempty mentionedSymbols expr
+    Apply expr args ->
+        mentionedSymbols expr <> Set.unions (mentionedSymbols <$> toList args)
+    TermSep _x bound scope ->
+        mentionedSymbols bound <> mentionedSymbols (fromScope scope)
+    ReplacePred _y _x bound scope ->
+        mentionedSymbols bound <> mentionedSymbols (fromScope scope)
+    ReplaceFun bounds lhs cond ->
+        Set.unions (mentionedSymbols . snd <$> toList bounds)
+            <> mentionedSymbols (fromScope lhs)
+            <> mentionedSymbols (fromScope cond)
+    Connected _conn left right ->
+        mentionedSymbols left <> mentionedSymbols right
+    Lambda scope ->
+        mentionedSymbols (fromScope scope)
+    Quantified _quant scope ->
+        mentionedSymbols (fromScope scope)
+    PropositionalConstant{} ->
+        mempty
+    Not _loc expr ->
+        mentionedSymbols expr
+
+abstractVarSymbol :: VarSymbol -> ExprOf VarSymbol -> Scope VarSymbol ExprOf VarSymbol
+abstractVarSymbol x = abstract (\y -> if x == y then Just x else Nothing)
+
+abstractVarSymbols :: Foldable t => t VarSymbol -> ExprOf VarSymbol -> Scope VarSymbol ExprOf VarSymbol
+abstractVarSymbols xs = abstract (\y -> if y `elem` xs then Just y else Nothing)
+
+
+forgetLocation :: forall a. ExprOf a -> ExprOf a
+forgetLocation = \case
+      TermVar a ->
+        TermVar a
+
+      TermSymbol _loc symb args ->
+        TermSymbol Nowhere symb (map forgetLocation args)
+
+      TermSymbolStruct ss me ->
+        TermSymbolStruct ss (forgetLocation <$> me)
+
+      Apply f args ->
+        Apply (forgetLocation f) (forgetLocation <$> args)
+
+      TermSep v dom sc ->
+        TermSep v (forgetLocation dom) (hoistScope forgetLocation sc)
+
+      ReplacePred v1 v2 dom sc ->
+        ReplacePred v1 v2 (forgetLocation dom) (hoistScope forgetLocation sc)
+
+      ReplaceFun doms lhs rhs ->
+        ReplaceFun
+          (fmap (fmap forgetLocation) doms)
+          (hoistScope forgetLocation lhs)
+          (hoistScope forgetLocation rhs)
+
+      Connected c e1 e2 ->
+        Connected c (forgetLocation e1) (forgetLocation e2)
+
+      Lambda sc ->
+        Lambda (hoistScope forgetLocation sc)
+
+      Quantified q sc ->
+        Quantified q (hoistScope forgetLocation sc)
+
+      PropositionalConstant pc ->
+        PropositionalConstant pc
+
+      Not _loc e ->
+        Not Nowhere (forgetLocation e)
+
+
+equivalent :: Eq a => ExprOf a -> ExprOf a -> Bool
+equivalent e1 e2 = forgetLocation e1 == forgetLocation e2
+
+-- | Use the given set of in scope structures to cast them to their carriers
+-- when occurring on the rhs of the element relation.
+-- Use the given 'Map' to annotate (unannotated) structure operations
+-- with the most recent inscope appropriate label.
+annotateWith :: Set VarSymbol -> HashMap StructSymbol VarSymbol -> Formula -> Formula
+annotateWith = go
+    where
+        go :: (Ord a) => Set a -> HashMap StructSymbol a -> ExprOf a -> ExprOf a
+        go labels ops = \case
+            TermSymbolStruct symb Nothing ->
+                -- TODO error if symbol is not instantiated, but only in theorems?
+                TermSymbolStruct symb (TermVar <$> HM.lookup symb ops)
+            TermSymbolStruct symb (Just e) ->
+                TermSymbolStruct symb (Just (go labels ops e))
+            IsElementOf loc1 a (TermVar x) | x `Set.member` labels ->
+                IsElementOf loc1 (go labels ops a) (TermSymbolStruct CarrierSymbol (Just (TermVar x)))
+            Not loc a ->
+                Not loc (go labels ops a)
+            Connected conn a b ->
+                Connected conn (go labels ops a) (go labels ops b)
+            Quantified quant body ->
+                Quantified quant (toScope (go (Set.map F labels) (F <$> ops) (fromScope body)))
+            e@TermVar{} -> e
+            TermSymbol loc symb args ->
+                TermSymbol loc symb (go labels ops <$> args)
+            Apply e1 args ->
+                Apply (go labels ops e1) (go labels ops <$> args)
+            TermSep vs e scope ->
+                TermSep vs (go labels ops e) (toScope (go (Set.map F labels) (F <$> ops) (fromScope scope)))
+            ReplacePred y x xB scope ->
+                ReplacePred y x (go labels ops xB) (toScope (go (Set.map F labels) (F <$> ops) (fromScope scope)))
+            ReplaceFun bounds ap cond ->
+                ReplaceFun
+                    (fmap (\(x, e) -> (x, go labels ops e)) bounds)
+                    (toScope (go (Set.map F labels) (F <$> ops) (fromScope ap)))
+                    (toScope (go (Set.map F labels) (F <$> ops) (fromScope cond)))
+            Lambda body ->
+                Lambda (toScope (go (Set.map F labels) (F <$> ops) (fromScope body)))
+            e@PropositionalConstant{} -> e
+
+containsHigherOrderConstructs :: ExprOf a -> Bool
+containsHigherOrderConstructs = \case
+    TermSep {} -> True
+    ReplacePred{}-> True
+    ReplaceFun{}-> True
+    Lambda{} -> True
+    Apply{} -> False -- FIXME: this is a lie in general; we need to add sortchecking to determine this.
+    TermVar{} -> False
+    PropositionalConstant{} -> False
+    TermSymbol _loc _s es -> any containsHigherOrderConstructs es
+    Not _loc e -> containsHigherOrderConstructs e
+    Connected _ e1 e2 -> containsHigherOrderConstructs e1 || containsHigherOrderConstructs e2
+    Quantified _ scope -> containsHigherOrderConstructs (fromScope scope)
+    TermSymbolStruct _ _ -> False
+
+pattern TermOp :: Location -> FunctionSymbol -> [ExprOf a] -> ExprOf a
+pattern TermOp loc op es = TermSymbol loc (SymbolMixfix op) es
+
+pattern TermConst :: Location -> Token -> ExprOf a
+pattern TermConst loc c <- TermOp loc (MixfixItem (TokenCons c End) _ NonAssoc) []
+    where
+        TermConst loc c =
+            TermOp loc (MixfixItem (TokenCons c End) (markerFromToken c) NonAssoc) []
+
+pattern TermPair :: Location -> ExprOf a -> ExprOf a -> ExprOf a
+pattern TermPair loc e1 e2 = TermOp loc PairSymbol [e1, e2]
+
+pattern Atomic :: Location -> Predicate -> [ExprOf a] -> ExprOf a
+pattern Atomic loc symbol args = TermSymbol loc (SymbolPredicate symbol) args
+
+
+pattern FormulaAdj :: Location -> ExprOf a -> LexicalItem -> [ExprOf a] -> ExprOf a
+pattern FormulaAdj loc e adj es = Atomic loc (PredicateAdj adj) (e:es)
+
+pattern FormulaVerb :: Location -> ExprOf a -> LexicalItemSgPl -> [ExprOf a] -> ExprOf a
+pattern FormulaVerb loc e verb es = Atomic loc (PredicateVerb verb) (e:es)
+
+pattern FormulaNoun :: Location -> ExprOf a -> LexicalItemSgPl -> [ExprOf a] -> ExprOf a
+pattern FormulaNoun loc e noun es = Atomic loc (PredicateNoun noun) (e:es)
+
+relationNoun :: Location -> Expr -> Formula
+relationNoun loc arg = FormulaNoun loc arg (mkLexicalItemSgPl (unsafeReadPhraseSgPl "relation[/s]") "relation") []
+
+rightUniqueAdj :: Location -> Expr -> Formula
+rightUniqueAdj loc arg = FormulaAdj loc arg (mkLexicalItem (unsafeReadPhrase "right-unique") "rightunique") []
+
+-- | Untyped quantification.
+pattern Forall, Exists :: Scope VarSymbol ExprOf a -> ExprOf a
+pattern Forall scope = Quantified Universally  scope
+pattern Exists scope = Quantified Existentially scope
+
+makeForall, makeExists :: Foldable t => t VarSymbol -> Formula -> Formula
+makeForall xs e = Quantified Universally (abstractVarSymbols xs e)
+makeExists xs e = Quantified Existentially (abstractVarSymbols xs e)
+
+instantiateSome :: NonEmpty VarSymbol -> Scope VarSymbol ExprOf VarSymbol -> Scope VarSymbol ExprOf VarSymbol
+instantiateSome xs scope = toScope (instantiateEither inst scope)
+    where
+        inst (Left x) | x `elem` xs = TermVar (F x)
+        inst (Left b) = TermVar (B b)
+        inst (Right fv) = TermVar (F fv)
+
+-- | Bind all free variables not occuring in the given set universally
+forallClosure :: Set VarSymbol -> Formula -> Formula
+forallClosure xs phi = if isClosed phi
+    then phi
+    else Quantified Universally (abstract isNamedVar phi)
+        where
+            isNamedVar :: VarSymbol -> Maybe VarSymbol
+            isNamedVar x = if x `Set.member` xs then Nothing else Just x
+
+freeVars :: ExprOf VarSymbol -> Set VarSymbol
+freeVars = Set.fromList . toList
+
+pattern And :: ExprOf a -> ExprOf a -> ExprOf a
+pattern And e1 e2 = Connected Conjunction e1 e2
+
+pattern Or :: ExprOf a -> ExprOf a -> ExprOf a
+pattern Or e1 e2 = Connected Disjunction e1 e2
+
+pattern Implies :: ExprOf a -> ExprOf a -> ExprOf a
+pattern Implies e1 e2 = Connected Implication e1 e2
+
+pattern Iff :: ExprOf a -> ExprOf a -> ExprOf a
+pattern Iff e1 e2 = Connected Equivalence e1 e2
+
+pattern Xor :: ExprOf a -> ExprOf a -> ExprOf a
+pattern Xor e1 e2 = Connected ExclusiveOr e1 e2
+
+
+pattern Bottom :: ExprOf a
+pattern Bottom = PropositionalConstant IsBottom
+
+pattern Top :: ExprOf a
+pattern Top = PropositionalConstant IsTop
+
+
+data RelationApplicationError
+    = RelationParameterArityMismatch
+        { relationApplicationLocation :: Location
+        , relationApplicationSymbol :: RelationSymbol
+        , relationApplicationExpectedParameters :: ParameterArity
+        , relationApplicationActualParameters :: ParameterArity
+        }
+    deriving (Show, Eq, Ord)
+
+checkRelationParameterArity
+    :: Foldable f
+    => Location
+    -> RelationSymbol
+    -> f a
+    -> Either RelationApplicationError ()
+checkRelationParameterArity loc relation parameters
+    | expected == actual =
+        Right ()
+    | otherwise =
+        Left RelationParameterArityMismatch
+            { relationApplicationLocation = loc
+            , relationApplicationSymbol = relation
+            , relationApplicationExpectedParameters = expected
+            , relationApplicationActualParameters = actual
+            }
+  where
+    expected = relationSymbolParameterArity relation
+    actual = parameterArityOf parameters
+
+makeRelationApplication
+    :: Location
+    -> RelationSymbol
+    -> [ExprOf a]
+    -> Either
+        RelationApplicationError
+        (ExprOf a -> ExprOf a -> ExprOf a)
+makeRelationApplication loc relation parameters = do
+    checkRelationParameterArity loc relation parameters
+    pure \left right ->
+        Atomic loc (PredicateRelation relation) (parameters <> [left, right])
+
+pattern Relation :: Location -> RelationSymbol -> [ExprOf a] -> ExprOf a
+pattern Relation loc rel es <- Atomic loc (PredicateRelation rel) es
+
+-- | Membership.
+pattern IsElementOf :: Location -> ExprOf a -> ExprOf a -> ExprOf a
+pattern IsElementOf loc e1 e2 =
+    Atomic loc (PredicateRelation ElementSymbol) [e1, e2]
+
+isElementOf :: ExprOf a -> ExprOf a -> ExprOf a
+isElementOf e1 e2 =
+    Atomic Nowhere (PredicateRelation ElementSymbol) [e1, e2]
+
+-- | Membership.
+isNotElementOf :: Location -> ExprOf a -> ExprOf a -> ExprOf a
+isNotElementOf loc e1 e2 = Not loc (IsElementOf loc e1 e2)
+
+-- | Subset relation (non-strict).
+pattern IsSubsetOf :: Location -> ExprOf a -> ExprOf a -> ExprOf a
+pattern IsSubsetOf loc e1 e2 = Atomic loc (PredicateRelation SubseteqSymbol) (e1 : [e2])
+
+ordinalNoun :: LexicalItemSgPl
+ordinalNoun = mkLexicalItemSgPl (unsafeReadPhraseSgPl "ordinal[/s]") "ordinal"
+
+isOrdinalNoun :: LexicalItemSgPl -> Bool
+isOrdinalNoun noun = noun == ordinalNoun
+
+-- | Ordinal predicate.
+pattern IsOrd :: Location -> ExprOf a -> ExprOf a
+pattern IsOrd loc e1 <- Atomic loc (PredicateNoun (isOrdinalNoun -> True)) [e1]
+    where
+        IsOrd loc e1 = Atomic loc (PredicateNoun ordinalNoun) [e1]
+
+-- | Equality.
+pattern Equals :: Location -> ExprOf a -> ExprOf a -> ExprOf a
+pattern Equals loc e1 e2 = Atomic loc (PredicateRelation EqSymbol) (e1 : [e2])
+
+equals :: ExprOf a -> ExprOf a -> ExprOf a
+equals e1 e2 = Atomic Nowhere (PredicateRelation EqSymbol) (e1 : [e2])
+
+-- | Disequality.
+pattern NotEquals :: Location -> ExprOf a -> ExprOf a -> ExprOf a
+pattern NotEquals loc e1 e2 = Atomic loc (PredicateRelation NeqSymbol) (e1 : [e2])
+
+pattern EmptySet :: Location -> ExprOf a
+pattern EmptySet loc =
+    TermSymbol loc
+        (SymbolMixfix (MixfixItem (TokenCons (Command "emptyset") End) "emptyset" NonAssoc))
+        []
+
+makeConjunction :: [ExprOf a] -> ExprOf a
+makeConjunction = \case
+    [] -> Top
+    es -> List.foldl1' And es
+
+makeDisjunction :: [ExprOf a] -> ExprOf a
+makeDisjunction = \case
+    [] -> Bottom
+    es -> List.foldl1' Or es
+
+makeIff :: [ExprOf a] -> ExprOf a
+makeIff = \case
+    [] -> Bottom
+    es -> List.foldl1' Iff es
+
+makeXor :: [ExprOf a] -> ExprOf a
+makeXor = \case
+    [] -> Bottom
+    es -> List.foldl1' Xor es
+
+-- | Source-ordered HOTG finite-set adjunction.
+--
+-- This deliberately uses only fixed operations.  In particular, finite-set
+-- notation is independent of the ordinary source-owned 'ConsSymbol'.
+finiteSet :: Location -> NonEmpty (ExprOf a) -> ExprOf a
+finiteSet location = foldr insert (EmptySet location)
+    where
+        insert element set =
+            TermSymbol location (SymbolMixfix UnionsSymbol)
+                [ TermSymbol location (SymbolMixfix UpairSymbol)
+                    [ TermSymbol location (SymbolMixfix UpairSymbol)
+                        [element, element]
+                    , set
+                    ]
+                ]
+
+isPositive :: ExprOf a -> Bool
+isPositive = \case
+    Not _ _ -> False
+    _ -> True
+
+dual :: ExprOf a -> ExprOf a
+dual = \case
+    Not _loc f -> f
+    f -> Not Nowhere f
+
+
+
+-- | Local assumptions.
+data Asm
+    = Asm Formula
+    | AsmStruct VarSymbol StructPhrase
+
+
+deriving instance Show Asm
+deriving instance Eq   Asm
+deriving instance Ord  Asm
+
+data StructAsm
+    = StructAsm VarSymbol StructPhrase
+
+
+
+data Axiom = Axiom [Asm] Formula
+
+deriving instance Show Axiom
+deriving instance Eq   Axiom
+deriving instance Ord  Axiom
+
+
+data Lemma = Lemma [Asm] Formula
+
+deriving instance Show Lemma
+deriving instance Eq   Lemma
+deriving instance Ord  Lemma
+
+
+data Defn
+    = DefnPredicate [Asm] Predicate (NonEmpty VarSymbol) Formula
+    | DefnFun [Asm] LexicalItemSgPl [VarSymbol] Term
+    | DefnOp FunctionSymbol [VarSymbol] Term
+
+deriving instance Show Defn
+deriving instance Eq   Defn
+deriving instance Ord  Defn
+
+data Inductive = Inductive
+    { inductiveSymbol :: FunctionSymbol
+    , inductiveParams :: [VarSymbol]
+    , inductiveDomain :: Expr
+    , inductiveIntros :: NonEmpty IntroRule
+    }
+    deriving (Show, Eq, Ord)
+
+data IntroRule = IntroRule
+    { introConditions :: [Formula] -- The inductively defined set may only appear as an argument of monotone operations on the rhs.
+    , introResult :: Formula -- TODO Refine.
+    }
+    deriving (Show, Eq, Ord)
+
+data CalcQuantifier
+    = CalcForall (NonEmpty VarSymbol) (Maybe Formula)
+    | CalcUnquantified
+    deriving (Show, Eq, Ord)
+
+data Proof
+    = Omitted Location
+    -- ^ Ends a proof without further verification.
+    -- This results in a “gap” in the formalization.
+    | Qed {mloc :: Maybe Location, by :: Justification}
+    -- ^ Ends of a proof, leaving automation to discharge the current goal using the given justification.
+    | Contradiction Location Justification
+    -- ^ Ends a proof by deriving absurdity using the given justification.
+    | ByContradiction Location Proof
+    -- ^ Take the dual of the current goal as an assumption and
+    -- set the goal to absurdity.
+    | BySetInduction Location (Maybe Term) Proof
+    -- ^ ∈-induction.
+    | ByOrdInduction Location Proof
+    -- ^ Transfinite induction for ordinals.
+    | Assume Location Formula Proof
+    -- ^ Simplify goals that are implications or disjunctions.
+    | Fix Location (NonEmpty VarSymbol) Formula Proof
+    -- ^ Simplify universal goals (with an optional bound or such that statement)
+    | Take Location (NonEmpty VarSymbol) Formula Justification Proof
+    -- ^ Use existential assumptions.
+    | Suffices Location Formula Justification Proof
+    | ByCase Location [Case]
+    -- ^ Proof by case. Disjunction of the case hypotheses 'Case'
+    -- must hold for this step to succeed. Each case starts a subproof,
+    -- keeping the same goal but adding the case hypothesis as an assumption.
+    -- Often this will be a classical split between /@P@/ and /@not P@/, in
+    -- which case the proof that /@P or not P@/ holds is easy.
+    --
+    | Have Location Formula Justification Proof
+    -- ^ An affirmation, e.g.: /@We have \<stmt\> by \<ref\>@/.
+    --
+    | Calc Location CalcQuantifier Calc Proof
+    | Subclaim Location Formula Proof Proof
+    -- ^ A claim is a sublemma with its own proof:
+    --
+    -- /@Show \<goal stmt\>. \<steps\>. \<continue other proof\>.@/
+    --
+    -- A successful first proof adds the claimed formula as an assumption
+    -- for the remaining proof.
+    --
+    | Define Location VarSymbol Term Proof
+    | DefineFunction Location VarSymbol VarSymbol Term Term Proof
+
+    | DefineFunctionLocal Location VarSymbol VarSymbol VarSymbol Term (NonEmpty (Term, Formula)) Proof
+
+deriving instance Show Proof
+deriving instance Eq   Proof
+deriving instance Ord  Proof
+
+
+
+-- | A case of a case split.
+data Case = Case
+    { caseOf :: Formula
+    , caseProof :: Proof
+    }
+
+deriving instance Show Case
+deriving instance Eq   Case
+deriving instance Ord  Case
+
+-- | See 'Syntax.Abstract.Calc'.
+data Calc
+    = Equation Term (NonEmpty (Term, Justification))
+    | Biconditionals Term (NonEmpty (Term, Justification))
+
+deriving instance Show Calc
+deriving instance Eq   Calc
+deriving instance Ord  Calc
+
+calcQuant :: CalcQuantifier -> (Formula -> Formula)
+calcQuant = \case
+    CalcUnquantified -> id
+    CalcForall xs maySuchThat -> case maySuchThat of
+        Nothing -> makeForall xs
+        Just suchThat -> \phi -> makeForall xs (suchThat `Implies` phi)
+
+calcResult :: CalcQuantifier -> Calc -> ExprOf VarSymbol
+calcResult quant = \case
+    Equation e eqns -> calcQuant quant (Equals Nowhere e (fst (NonEmpty.last eqns)))
+    Biconditionals phi phis -> calcQuant quant (phi `Iff` fst (NonEmpty.last phis))
+
+calculation :: CalcQuantifier -> Calc -> [(ExprOf VarSymbol, Justification)]
+calculation quant = \case
+    Equation e1 eqns@((e2, jst) :| _) -> (calcQuant quant (Equals Nowhere e1 e2), jst) : collectEquations quant (toList eqns)
+    Biconditionals p1 ps@((p2, jst) :| _) -> (calcQuant quant (p1 `Iff` p2), jst) : collectBiconditionals quant (toList ps)
+
+
+collectEquations :: CalcQuantifier -> [(Formula, j)] -> [(Formula, j)]
+collectEquations quant = \case
+    (e1, _) : eqns'@((e2, jst) : _) -> (calcQuant quant (Equals Nowhere e1 e2), jst) : collectEquations quant eqns'
+    _ -> []
+
+collectBiconditionals :: CalcQuantifier -> [(Formula, j)] -> [(Formula, j)]
+collectBiconditionals quant = \case
+    (p1, _) : ps@((p2, jst) : _) -> (calcQuant quant (p1 `Iff` p2), jst) : collectBiconditionals quant ps
+    _ -> []
+
+
+data Datatype
+    = Datatype
+        { datatypeHead :: SymbolPattern
+        , datatypeClauses :: NonEmpty DatatypeClause
+        }
+    deriving (Show, Eq, Ord)
+
+data DatatypeClause = DatatypeClause
+    { datatypeClauseConstructor :: SymbolPattern
+    , datatypeClausePremises :: [(VarSymbol, Expr)]
+    }
+    deriving (Show, Eq, Ord)
+
+
+data Signature
+    = SignaturePredicate Predicate (NonEmpty VarSymbol)
+    | SignatureFormula Formula
+    -- TODO: This is a lossy encoding of a symbolic signature declaration.
+    -- The checker currently recovers the declared mixfix symbol heuristically
+    -- from the generated formula in order to assign ownership. Replace this
+    -- with a precise signature representation that carries the declared symbol
+    -- directly.
+
+deriving instance Show Signature
+deriving instance Eq   Signature
+deriving instance Ord  Signature
+
+data StructDefn = StructDefn
+    { structPhrase :: StructPhrase
+    -- ^ The noun phrase naming the structure, e.g.: @partial order@ or @abelian group@.
+    , structParents :: Set StructPhrase
+    , structDefnLabel :: VarSymbol
+    , structDefnFixes :: Set StructSymbol
+    -- ^ List of commands representing operations,
+    -- e.g.: @\\contained@ or @\\inv@. These are used as default operation names
+    -- in instantiations such as @Let $G$ be a group@.
+    -- The commands should be set up to handle an optional struct label
+    -- which would typically be rendered as a sub- or superscript, e.g.:
+    -- @\\contained[A]@ could render as ”⊑ᴬ“.
+    --    --
+    , structDefnAssumes :: [(Marker, Formula)]
+    -- ^ The assumption or axioms of the structure.
+    -- To be instantiate with the @structFixes@ of a given structure.
+    }
+
+deriving instance Show StructDefn
+deriving instance Eq   StructDefn
+deriving instance Ord  StructDefn
+
+
+data Abbreviation
+    = Abbreviation Symbol (Scope Int ExprOf Void)
+    deriving (Show, Eq, Ord)
+
+data Block
+    = BlockAxiom Location Marker Axiom
+    | BlockLemma Location Marker Lemma
+    | BlockProof Location Location Proof
+    | BlockDefn Location Marker Defn
+    | BlockAbbr Location Marker Abbreviation
+    | BlockStruct Location Marker StructDefn
+    | BlockInductive Location Marker Inductive
+    | BlockSig Location Marker [Asm] Signature
+    | BlockData Location Marker Datatype
+    deriving (Show, Eq, Ord)
+
+
+-- | Full boolean contraction.
+contraction :: ExprOf a -> ExprOf a
+contraction = \case
+    Connected conn f1 f2  -> atomicContraction (Connected conn (contraction f1) (contraction f2))
+    Quantified quant scope -> atomicContraction (Quantified quant (hoistScope contraction scope))
+    Not loc f -> Not loc (contraction f)
+    f -> f
+
+
+-- | Atomic boolean contraction.
+atomicContraction :: ExprOf a -> ExprOf a
+atomicContraction = \case
+    Top    `Iff` f      -> f
+    Bottom `Iff` f      -> Not Nowhere f
+    f      `Iff` Top    -> f
+    f      `Iff` Bottom -> Not Nowhere f
+
+    Top    `Implies` f      -> f
+    Bottom `Implies` _      -> Top
+    _      `Implies` Top    -> Top
+    f      `Implies` Bottom -> Not Nowhere f
+
+    Top    `And` f      -> f
+    Bottom `And` _      -> Bottom
+    f      `And` Top    -> f
+    _      `And` Bottom -> Bottom
+
+    phi@(Quantified _quant scope) -> case unscope scope of
+        Top -> Top
+        Bottom -> Bottom
+        _ -> phi
+
+    Not _ Top    -> Bottom
+    Not _ Bottom -> Top
+
+    f -> f
diff --git a/source/Felix/Syntax/LexicalPhrase.hs b/source/Felix/Syntax/LexicalPhrase.hs
new file mode 100644
index 0000000..5eb5b18
--- /dev/null
+++ b/source/Felix/Syntax/LexicalPhrase.hs
@@ -0,0 +1,95 @@
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+
+module Felix.Syntax.LexicalPhrase where
+
+
+import Base
+import Felix.Syntax.Token (Token(..))
+
+import Control.DeepSeq (NFData)
+import Data.Char (isAlpha)
+import Data.Text qualified as Text
+import Text.Earley.Mixfix (Holey)
+import Text.Earley (Grammar, Prod, (<?>), fullParses, parser, rule, token, satisfy)
+
+
+
+-- | 'LexicalPhrase's should be nonempty lists with at least one proper word token.
+-- Hyphens and quotes in words are treated as letters.
+-- Thus /@manifold-with-boundary@/ is a singleton lexical phrase (one word).
+--
+type LexicalPhrase = Holey Token
+
+-- MAYBE Add this instance by making LexicalPhrase a proper Type?
+-- Until then we can use the default instance for lists of prettyprintable things.
+--
+-- instance Pretty LexicalPhrase where
+--    pretty components = hsep (prettyComponent <$> components)
+--       where
+--          prettyComponent = \case
+--             Nothing -> "_"
+--             Just tok -> pretty tok
+
+
+
+-- | Split data by grammatical number (singular/plural).
+-- The 'Eq' and 'Ord' instances only consider the singular
+-- form so that we can prefer known irregular plurals over
+-- guessed irregular plurals when inserting items into
+-- the 'Lexicon'.
+data SgPl a
+    = SgPl {sg :: a, pl :: a}
+    deriving (Show, Functor, Generic, Hashable, NFData)
+
+instance Eq a => Eq (SgPl a) where (==) = (==) `on` sg
+instance Ord a => Ord (SgPl a) where compare = compare `on` sg
+
+
+-- These readers parse only Felix-owned lexical literals.
+unsafeReadPhrase :: String -> LexicalPhrase
+unsafeReadPhrase spec = case fst (fullParses (parser lexicalPhraseSpec) spec) of
+    pat : _ -> pat
+    _ -> error "unsafeReadPhrase failed"
+
+unsafeReadPhraseSgPl :: String -> SgPl LexicalPhrase
+unsafeReadPhraseSgPl spec = case fst (fullParses (parser lexicalPhraseSpecSgPl) spec) of
+    pat : _ -> pat
+    _ -> error "unsafeReadPhraseSgPl failed"
+
+
+lexicalPhraseSpec :: Grammar r (Prod r String Char LexicalPhrase)
+lexicalPhraseSpec = do
+    hole     <- rule $ Nothing <$ token '?' <?> "hole"
+    word     <- rule $ Just <$> many (satisfy (\c -> isAlpha c || c == '-'))
+    space    <- rule $ Just . (:[]) <$> token ' '
+    segment  <- rule $ hole <|> word
+    rule $ (\s ss -> makePhrase (s:ss)) <$> segment <*> many (space *> segment)
+    where
+        makePhrase :: [Maybe String] -> LexicalPhrase
+        makePhrase pat = fmap makeWord pat
+
+
+lexicalPhraseSpecSgPl :: Grammar r (Prod r String Char (SgPl LexicalPhrase))
+lexicalPhraseSpecSgPl = do
+    space <- rule $ Just . (:[]) <$> token ' '
+    hole  <- rule $ (Nothing, Nothing) <$ token '?'<?> "hole"
+
+    word <- rule (many (satisfy isAlpha) <?> "word")
+    wordSgPl <- rule $ (,) <$> (token '[' *> word) <* token '/' <*> word <* token ']'
+    complexWord <- rule $ (\(a,b) -> (Just a, Just b)) . fuse <$>
+        many ((<>) <$> (dup <$> word) <*> wordSgPl) <?> "word"
+    segment  <- rule (hole <|> (dup . Just <$> word) <|> complexWord )
+    rule $ (\s ss -> makePhrase (s:ss)) <$> segment <*> many (space *> segment)
+    where
+        dup x = (x,x)
+        fuse = \case
+            (a, b) : (c, d) : rest -> fuse ((a <> c, b <> d) : rest)
+            [(a, b)] -> (a, b)
+            _ -> error "Syntax.Abstract.fuse"
+
+        makePhrase :: [(Maybe String, Maybe String)] -> SgPl LexicalPhrase
+        makePhrase = (\(patSg, patPl) -> SgPl (fmap makeWord patSg) (fmap makeWord patPl)) . unzip
+
+makeWord :: Maybe String -> Maybe Token
+makeWord = fmap (Word . Text.pack)
diff --git a/source/Felix/Syntax/Lexicon.hs b/source/Felix/Syntax/Lexicon.hs
new file mode 100644
index 0000000..c3332c7
--- /dev/null
+++ b/source/Felix/Syntax/Lexicon.hs
@@ -0,0 +1,330 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | The 'Lexicon' describes the part of the grammar that extensible/dynamic.
+--
+-- The items of the 'Lexicon' are organized by their meaning and their
+-- syntactic behaviour. They are typically represented as some kind of
+-- pattern data which is then used to generate various production rules
+-- for the concrete grammar. This representation makes inspection and
+-- extension easier.
+--
+
+module Felix.Syntax.Lexicon
+    ( module Felix.Syntax.Lexicon
+    , pattern ConsSymbol
+    , pattern PairSymbol
+    , pattern UpairSymbol
+    , pattern UnionsSymbol
+    , pattern CarrierSymbol
+    , pattern ApplySymbol
+    , pattern DomSymbol
+    ) where
+
+
+import Base
+import Felix.Syntax.Abstract
+
+import Data.List qualified as List
+import Data.Sequence qualified as Seq
+import Data.Set qualified as Set
+import Data.Map.Strict qualified as Map
+import Data.Text qualified as Text
+import Felix.Syntax.Mixfix (Holey)
+
+
+data SignatureHeadForm
+    = AdjectiveSignatureHead
+    | SymbolicSignatureHead
+    deriving (Show, Eq, Ord)
+
+-- Adjective heads must precede symbolic heads because both start with a math
+-- variable.
+concreteSignatureHeadForms :: [SignatureHeadForm]
+concreteSignatureHeadForms =
+    [ AdjectiveSignatureHead
+    , SymbolicSignatureHead
+    ]
+
+data Lexicon = Lexicon
+    { lexiconMixfixTable        :: Seq (Map Pattern MixfixItem)
+    , lexiconConnectives        :: [[(Holey Token, Associativity)]]
+    , lexiconPrefixPredicates   :: [(PrefixPredicate, Marker)]
+    , lexiconStructFun          :: [StructSymbol]
+    , lexiconRelationSymbols    :: [RelationSymbol]
+    , lexiconVerbs              :: [LexicalItemSgPl]
+    , lexiconAdjLs              :: [LexicalItem]
+    , lexiconAdjRs              :: [LexicalItem]
+    , lexiconNouns              :: [LexicalItemSgPl]
+    , lexiconStructNouns        :: [LexicalItemSgPl]
+    , lexiconFuns               :: [LexicalItemSgPl]
+    } deriving (Show, Eq)
+
+-- Projection returning the union of both left and right attributes.
+--
+lexiconAdjs :: Lexicon -> [LexicalItem]
+lexiconAdjs lexicon = lexiconAdjLs lexicon <> lexiconAdjRs lexicon
+
+
+builtins :: Lexicon
+builtins =
+    Lexicon
+        { lexiconMixfixTable        = builtinMixfixTable
+        , lexiconPrefixPredicates   = builtinPrefixPredicates
+        , lexiconStructFun          = builtinStructOps
+        , lexiconConnectives        = builtinConnectives
+        , lexiconRelationSymbols    = builtinRelationSymbols
+        , lexiconAdjLs              = []
+        , lexiconAdjRs              = builtinAdjRs
+        , lexiconVerbs              = builtinVerbs
+        , lexiconNouns              = builtinNouns
+        , lexiconStructNouns        = builtinStructNouns
+        , lexiconFuns               = []
+        }
+
+prefixPredicatePattern :: PrefixPredicate -> Pattern
+prefixPredicatePattern (PrefixPredicate command _arity) =
+    TokenCons (Command command) End
+
+builtinMixfixTable :: Seq (Map Pattern MixfixItem)
+builtinMixfixTable = Seq.fromList $ Map.fromList . fmap toEntry <$> builtinMixfixLevels
+    where
+        toEntry item@(MixfixItem pat _ _) = (pat, item)
+
+-- INVARIANT: 10 precedence levels for now.
+builtinMixfixLevels :: [[MixfixItem]]
+builtinMixfixLevels =
+    [ []
+    , [binOp (Symbol "+") LeftAssoc "add", binOp (Command "union") LeftAssoc "union", binOp (Symbol "-") LeftAssoc "minus", binOp (Command "rminus") LeftAssoc "rminus", binOp (Command "monus") LeftAssoc "monus"]
+    , [binOp (Command "relcomp") LeftAssoc "relcomp"]
+    , [binOp (Command "circ") LeftAssoc "circ"]
+    , [binOp (Command "mul") LeftAssoc "mul", binOp (Command "inter") LeftAssoc "inter", binOp (Command "rmul") LeftAssoc "rmul"]
+    , [binOp (Command "setminus") LeftAssoc "setminus"]
+    , [binOp (Command "times") RightAssoc "times"]
+    , []
+    , prefixOps
+    , builtinIdentifiers
+    ]
+    where
+        builtinIdentifiers :: [MixfixItem]
+        builtinIdentifiers = identifier <$>
+            [ "emptyset"
+            , "naturals"
+            , "naturalsPlus"
+            , "integers"
+            , "rationals"
+            , "reals"
+            , "unit"
+            , "zero"
+            ]
+
+
+prefixOps :: [MixfixItem]
+prefixOps =
+    [ mkMixfixItem [Just (Command "rfrac"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR, Just InvisibleBraceL, Nothing, Just InvisibleBraceR] "rfrac" NonAssoc
+    , mkMixfixItem [Just (Command "exp"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR, Just InvisibleBraceL, Nothing, Just InvisibleBraceR] "exp" NonAssoc
+    , UnionsSymbol
+    , mkMixfixItem [Just (Command "cumul"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR] "cumul" NonAssoc
+    , mkMixfixItem [Just (Command "fst"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR] "fst" NonAssoc
+    , mkMixfixItem [Just (Command "snd"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR] "snd" NonAssoc
+    , mkMixfixItem [Just (Command "pow"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR] "pow" NonAssoc
+    , mkMixfixItem [Just (Command "neg"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR] "neg" NonAssoc
+    , mkMixfixItem [Just (Command "inv"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR] "inv" NonAssoc
+    , mkMixfixItem [Just (Command "abs"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR] "abs" NonAssoc
+    , ConsSymbol
+    , PairSymbol
+    , UpairSymbol
+    -- NOTE Is now defined and hence no longer necessary , ApplySymbol
+    ]
+
+
+builtinStructOps :: [StructSymbol]
+builtinStructOps =
+    [ CarrierSymbol
+    ]
+
+identifier :: Text -> MixfixItem
+identifier cmd = mkMixfixItem [Just (Command cmd)] (Marker cmd) NonAssoc
+
+
+builtinRelationSymbols :: [RelationSymbol]
+builtinRelationSymbols =
+    [ RelationSymbol (Symbol "=") zeroParameterArity "eq"
+    , RelationSymbol (Command "rless") zeroParameterArity "rless"
+    , RelationSymbol (Command "neq") zeroParameterArity "neq"
+    , ElementSymbol
+    , NotElementSymbol -- Alternative to @\not\in@.
+    ]
+
+builtinPrefixPredicates :: [(PrefixPredicate, Marker)]
+builtinPrefixPredicates =
+    [ (PrefixPredicate "Cong" 4, "cong")
+    , (PrefixPredicate "Betw" 3, "betw")
+    ]
+
+
+builtinConnectives :: [[(Holey Token, Associativity)]]
+builtinConnectives =
+    [ [binOp' (Command "iff") NonAssoc]
+    , [binOp' (Command "implies") RightAssoc]
+    , [binOp' (Command "lor") LeftAssoc]
+    , [binOp' (Command "land") LeftAssoc]
+    , [([Just (Command "lnot"), Nothing], NonAssoc)]
+    ]
+
+
+binOp :: Token -> Associativity -> Marker -> MixfixItem
+binOp tok assoc m = mkMixfixItem [Nothing, Just tok, Nothing] m assoc
+
+binOp' :: Token -> Associativity -> (Holey Token, Associativity)
+binOp' tok assoc = ([Nothing, Just tok, Nothing], assoc)
+
+builtinAdjRs :: [LexicalItem]
+builtinAdjRs =
+    [ builtinEqualityRightAdjective
+    ]
+
+builtinEqualityRightAdjective :: LexicalItem
+builtinEqualityRightAdjective =
+    mkLexicalItem (unsafeReadPhrase "equal to ?") "eq"
+
+builtinVerbs :: [LexicalItemSgPl]
+builtinVerbs =
+    [ builtinEqualityVerb
+    ]
+
+builtinEqualityVerb :: LexicalItemSgPl
+builtinEqualityVerb =
+    mkLexicalItemSgPl (unsafeReadPhraseSgPl "equal[s/] ?") "eq"
+
+
+-- Some of these do/should correspond to mathlib structures,
+-- e.g.: lattice, complete lattice, ring, etc.
+--
+builtinNouns :: [LexicalItemSgPl]
+builtinNouns =
+    [ builtinSetNoun
+    , mkLexicalItemSgPl (unsafeReadPhraseSgPl "point[/s]") "point"
+    , builtinElementNoun
+    ]
+
+builtinSetNoun :: LexicalItemSgPl
+builtinSetNoun =
+    mkLexicalItemSgPl
+        (unsafeReadPhraseSgPl "set[/s]")
+        "set"
+
+builtinElementNoun :: LexicalItemSgPl
+builtinElementNoun =
+    mkLexicalItemSgPl
+        (unsafeReadPhraseSgPl "element[/s] of ?")
+        "elem"
+
+-- | Match the complete fixed-base identity, including the plural surface and
+-- authoritative marker. The ordinary 'Eq' instance intentionally compares
+-- only singular patterns.
+isBuiltinSetNoun :: LexicalItemSgPl -> Bool
+isBuiltinSetNoun item =
+    let actual = lexicalItemSgPlPattern item
+        expected = lexicalItemSgPlPattern builtinSetNoun
+    in sg actual == sg expected
+        && pl actual == pl expected
+        && lexicalItemSgPlMarker item
+            == lexicalItemSgPlMarker builtinSetNoun
+
+_Onesorted :: LexicalItemSgPl
+_Onesorted = mkLexicalItemSgPl (unsafeReadPhraseSgPl "onesorted structure[/s]") "onesorted_structure"
+
+builtinStructNouns :: [LexicalItemSgPl]
+builtinStructNouns = [_Onesorted]
+
+
+-- | Naïve splitting of lexical phrases to insert a variable slot for names in noun phrases,
+-- as in /@there exists a linear form $h$ on $E$@/, where the underlying pattern is
+-- /@linear form on ?@/. In this case we would get:
+--
+-- > splitOnVariableSlot (sg (unsafeReadPhraseSgPl "linear form[/s] on ?"))
+-- > ==
+-- > (unsafeReadPhrase "linear form", unsafeReadPhrase "on ?")
+--
+splitOnVariableSlot :: LexicalPhrase -> (LexicalPhrase, LexicalPhrase)
+splitOnVariableSlot pat = case prepositionIndices <> nonhyphenatedSlotIndices of
+    [] -> (pat, []) -- Place variable slot at the end.
+    is -> List.splitAt (minimum is) pat
+    where
+        prepositionIndices, slotIndices, nonhyphenatedSlotIndices :: [Int] -- Ascending.
+        prepositionIndices = List.findIndices isPreposition pat
+        slotIndices = List.findIndices isNothing pat
+        nonhyphenatedSlotIndices = [i | i <- slotIndices, noHyphen (nth (i + 1) pat)]
+
+        isPreposition :: Maybe Token -> Bool
+        isPreposition = \case
+            Just (Word w) -> w `Set.member` prepositions
+            _ -> False
+
+        noHyphen :: Maybe (Maybe Token) -> Bool
+        noHyphen = \case
+            Just (Just (Word w)) -> Text.head w /= '-'
+            -- If we arrive here, either the pattern is over (`Nothing`) or the next
+            -- part of the pattern is not a word that starts with a hyphen.
+            _ -> True
+
+
+-- Preposition are a closed class, but this list is not yet exhaustive.
+-- It can and should be extended when needed. The following list is a
+-- selection of the prepositions found at
+-- https://en.wikipedia.org/wiki/List_of_English_prepositions.
+--
+prepositions :: Set Text
+prepositions = Set.fromList
+    [ "about"
+    , "above"
+    , "across"
+    , "after"
+    , "against"
+    , "along", "alongside"
+    , "amid", "amidst"
+    , "among"
+    , "around"
+    , "as"
+    , "at"
+    , "atop"
+    , "before"
+    , "behind"
+    , "below"
+    , "beneath"
+    , "beside", "besides"
+    , "between"
+    , "beyond"
+    , "but"
+    , "by"
+    , "except"
+    , "for"
+    , "from"
+    , "in", "inside", "into"
+    , "like"
+    , "modulo", "mod"
+    , "near"
+    , "next"
+    , "of"
+    , "off"
+    , "on"
+    , "onto"
+    , "opposite"
+    , "out"
+    , "over"
+    , "past"
+    , "per"
+    , "sans"
+    , "till"
+    , "to"
+    , "under"
+    , "underneath"
+    , "unlike"
+    , "unto"
+    , "up", "upon"
+    , "versus"
+    , "via"
+    , "with"
+    , "within"
+    , "without"
+    ]
diff --git a/source/Felix/Syntax/Mixfix.hs b/source/Felix/Syntax/Mixfix.hs
new file mode 100644
index 0000000..a3ce4bb
--- /dev/null
+++ b/source/Felix/Syntax/Mixfix.hs
@@ -0,0 +1,139 @@
+{-# LANGUAGE RecursiveDo #-}
+
+module Felix.Syntax.Mixfix where
+
+{-
+Original code Copyright (c) 2014-2019, Olle Fredriksson
+
+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 Olle Fredriksson nor the names of other
+      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.
+-}
+
+
+import Base
+import Text.Earley
+import Data.Either
+import Felix.Syntax.Abstract
+
+
+replicateA :: Applicative f => Int -> f a -> f [a]
+replicateA n = sequenceA . replicate n
+
+consA :: Applicative f => f a -> f [a] -> f [a]
+consA p q = (:) <$> p <*> q
+
+
+-- | An identifier with identifier parts ('Just's), and holes ('Nothing's)
+-- representing the positions of its arguments.
+--
+-- Example (commonly written "if_then_else_"):
+-- @['Just' "if", 'Nothing', 'Just' "then", 'Nothing', 'Just' "else", 'Nothing'] :: 'Holey' 'String'@
+type Holey a = [Maybe a]
+
+
+-- | Create a grammar for parsing mixfix expressions.
+mixfixExpression
+  :: [[(Holey (Prod r e t ident), Associativity)]]
+  -- ^ A table of holey identifier parsers, with associativity information.
+  -- The identifiers should be in groups of precedence levels listed from
+  -- binding the least to the most tightly.
+  --
+  -- The associativity is taken into account when an identifier starts or ends
+  -- with holes, or both. Internal holes (e.g. after "if" in "if_then_else_")
+  -- start from the beginning of the table.
+  --
+  -- Note that this rule also applies to identifiers with multiple consecutive
+  -- holes, e.g. "if__" --- the associativity then applies to both holes.
+  -> Prod r e t expr
+  -- ^ An atom, i.e. what is parsed at the lowest level. This will
+  -- commonly be a (non-mixfix) identifier or a parenthesised expression.
+  -> (Holey ident -> [expr] -> expr)
+  -- ^ How to combine the successful application of a holey identifier to its
+  -- arguments into an expression.
+  -> Grammar r (Prod r e t expr)
+mixfixExpression table atom app = mixfixExpressionSeparate table' atom
+  where
+    table' = [[(holey, assoc, app) | (holey, assoc) <- row] | row <- table]
+
+-- | A version of 'mixfixExpression' with a separate semantic action for each
+-- individual 'Holey' identifier.
+mixfixExpressionSeparate
+  :: [[(Holey (Prod r e t ident), Associativity, Holey ident -> [expr] -> expr)]]
+  -- ^ A table of holey identifier parsers, with associativity information and
+  -- semantic actions.  The identifiers should be in groups of precedence
+  -- levels listed from binding the least to the most tightly.
+  --
+  -- The associativity is taken into account when an identifier starts or ends
+  -- with holes, or both. Internal holes (e.g. after "if" in "if_then_else_")
+  -- start from the beginning of the table.
+  --
+  -- Note that this rule also applies to identifiers with multiple consecutive
+  -- holes, e.g. "if__" --- the associativity then applies to both holes.
+  -> Prod r e t expr
+  -- ^ An atom, i.e. what is parsed at the lowest level. This will
+  -- commonly be a (non-mixfix) identifier or a parenthesised expression.
+  -> Grammar r (Prod r e t expr)
+mixfixExpressionSeparate table atom = mdo
+  expr <- foldrM ($) atom $ map (level expr) table
+  return expr
+  where
+    level expr idents next = mdo
+      same <- rule $ asum $ next : map (mixfixIdent same) idents
+      return same
+      where
+        -- Group consecutive holes and ident parts.
+        grp [] = []
+        grp (Nothing:ps) = case grp ps of
+          Left n:rest -> (Left $! (n + 1)) : rest
+          rest        -> Left 1            : rest
+        grp (Just p:ps) = case grp ps of
+          Right ps':rest -> Right (consA p ps')       : rest
+          rest           -> Right (consA p $ pure []) : rest
+
+        mixfixIdent same (ps, a, f) = f' <$> go (grp ps)
+          where
+            f' xs = f (concatMap (either (map $ const Nothing) $ map Just) xs)
+                   $ concat $ lefts xs
+            go ps' = case ps' of
+              [] -> pure []
+              [Right p] -> pure . Right <$> p
+              Left n:rest -> consA
+                (Left <$> replicateA n (if a == RightAssoc then next
+                                                           else same))
+                $ go rest
+              [Right p, Left n] -> consA
+                (Right <$> p)
+                $ pure . Left <$> replicateA n (if a == LeftAssoc then next
+                                                                  else same)
+              Right p:Left n:rest -> consA (Right <$> p)
+                $ consA (Left <$> replicateA n expr)
+                $ go rest
+              Right _:Right _:_ -> error
+                $  "Earley.mixfixExpression: The impossible happened. "
+                ++ "Please report this as a bug."
diff --git a/source/Felix/Syntax/Pragma.hs b/source/Felix/Syntax/Pragma.hs
new file mode 100644
index 0000000..97d1482
--- /dev/null
+++ b/source/Felix/Syntax/Pragma.hs
@@ -0,0 +1,250 @@
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+
+module Felix.Syntax.Pragma
+    ( SourceMixfixLevel
+    , sourceMixfixLevelValue
+    , SyntaxPragma(..)
+    , SyntaxPragmaProblem(..)
+    , SyntaxPragmaError(..)
+    , renderSyntaxPragmaError
+    , extractSyntaxPragmas
+    ) where
+
+import Base
+
+import Felix.Report.Location
+import Felix.Syntax.Abstract (Associativity(..))
+
+import Control.DeepSeq (NFData)
+import Control.Monad (unless, when)
+import Data.Bifunctor (first)
+import Data.Char (ord)
+import Data.Text qualified as Text
+import Data.Word (Word8)
+
+
+newtype SourceMixfixLevel = SourceMixfixLevel Word8
+    deriving stock (Show, Eq, Ord, Generic)
+    deriving anyclass (NFData)
+
+sourceMixfixLevelValue :: SourceMixfixLevel -> Word8
+sourceMixfixLevelValue (SourceMixfixLevel level) =
+    level
+
+data SyntaxPragma = LocatedFixityPragma
+    { syntaxPragmaLocation :: !Location
+    , syntaxPragmaAssociativity :: !Associativity
+    , syntaxPragmaLevel :: !SourceMixfixLevel
+    } deriving stock (Show, Eq)
+
+instance Locatable SyntaxPragma where
+    locate = syntaxPragmaLocation
+
+data SyntaxPragmaProblem
+    = SyntaxPragmaMissingSpaceAfterPrefix
+    | SyntaxPragmaMissingKeyword
+    | SyntaxPragmaUnknownKeyword !Text
+    | SyntaxPragmaMissingLevel
+    | SyntaxPragmaInvalidLevel
+    | SyntaxPragmaLevelOutOfRange
+    | SyntaxPragmaTrailingContent
+    | SyntaxPragmaLoneCarriageReturn
+    deriving stock (Show, Eq)
+
+data SyntaxPragmaError
+    = InvalidSyntaxPragma !Location !SyntaxPragmaProblem
+    | SyntaxPragmaLocationOutOfRange !FilePath !Int !Int
+    deriving stock (Show, Eq)
+
+renderSyntaxPragmaError :: SyntaxPragmaError -> Text
+renderSyntaxPragmaError = \case
+    InvalidSyntaxPragma location problem ->
+        locationToText location
+            <> ": "
+            <> renderSyntaxPragmaProblem problem
+    SyntaxPragmaLocationOutOfRange file line column ->
+        Text.pack file
+            <> ": syntax pragma location is out of range at "
+            <> Text.pack (show line)
+            <> ":"
+            <> Text.pack (show column)
+
+renderSyntaxPragmaProblem :: SyntaxPragmaProblem -> Text
+renderSyntaxPragmaProblem = \case
+    SyntaxPragmaMissingSpaceAfterPrefix ->
+        "expected horizontal space after %!"
+    SyntaxPragmaMissingKeyword ->
+        "missing syntax pragma keyword"
+    SyntaxPragmaUnknownKeyword keyword ->
+        "unknown syntax pragma keyword " <> Text.pack (show keyword)
+    SyntaxPragmaMissingLevel ->
+        "missing syntax pragma level"
+    SyntaxPragmaInvalidLevel ->
+        "syntax pragma level must use ASCII decimal digits"
+    SyntaxPragmaLevelOutOfRange ->
+        "syntax pragma level must be between 0 and 7"
+    SyntaxPragmaTrailingContent ->
+        "unexpected trailing syntax pragma content"
+    SyntaxPragmaLoneCarriageReturn ->
+        "a syntax pragma line must end with LF, CRLF, or end of file"
+
+extractSyntaxPragmas
+    :: FileId
+    -> FilePath
+    -> Text
+    -> Either SyntaxPragmaError [SyntaxPragma]
+extractSyntaxPragmas fileId file =
+    go 1
+  where
+    go lineNumber source
+        | Text.null source =
+            Right []
+        | otherwise = do
+            let (rawLine, suffix) =
+                    Text.break (== '\n') source
+                hasLineFeed =
+                    not (Text.null suffix)
+                (line, lineEnding) =
+                    if hasLineFeed && Text.isSuffixOf "\r" rawLine
+                        then
+                            (Text.dropEnd 1 rawLine, CrLf)
+                        else if hasLineFeed
+                            then
+                                (rawLine, LineFeed)
+                            else
+                                (rawLine, EndOfFile)
+                remaining =
+                    if hasLineFeed
+                        then Text.drop 1 suffix
+                        else ""
+                reserved =
+                    Text.isPrefixOf "%!"
+                        (Text.dropWhile isHorizontalSpace line)
+            pragma <-
+                if reserved
+                    then Just <$> parsePragmaLine
+                        fileId
+                        file
+                        lineNumber
+                        lineEnding
+                        line
+                    else
+                        Right Nothing
+            rest <- go (lineNumber + 1) remaining
+            pure (maybe rest (: rest) pragma)
+
+data LineEnding
+    = LineFeed
+    | CrLf
+    | EndOfFile
+    deriving stock (Show, Eq)
+
+parsePragmaLine
+    :: FileId
+    -> FilePath
+    -> Int
+    -> LineEnding
+    -> Text
+    -> Either SyntaxPragmaError SyntaxPragma
+parsePragmaLine fileId file lineNumber lineEnding rawLine = do
+    let horizontalPrefix =
+            Text.takeWhile isHorizontalSpace rawLine
+        column =
+            Text.length horizontalPrefix + 1
+    location <-
+        first
+            (const
+                (SyntaxPragmaLocationOutOfRange
+                    file
+                    lineNumber
+                    column))
+            (mkLocationChecked fileId lineNumber column)
+    let invalid
+            :: SyntaxPragmaProblem
+            -> Either SyntaxPragmaError a
+        invalid =
+            Left . InvalidSyntaxPragma location
+        afterPrefix =
+            Text.drop 2
+                (Text.dropWhile isHorizontalSpace rawLine)
+    when
+        (lineEnding == EndOfFile
+            && Text.isSuffixOf "\r" rawLine)
+        (invalid SyntaxPragmaLoneCarriageReturn)
+    afterPrefixSpace <-
+        case Text.uncons afterPrefix of
+            Nothing ->
+                invalid SyntaxPragmaMissingKeyword
+            Just (char, _)
+                | not (isHorizontalSpace char) ->
+                    invalid SyntaxPragmaMissingSpaceAfterPrefix
+            Just{} ->
+                Right (Text.dropWhile isHorizontalSpace afterPrefix)
+    when
+        (Text.null afterPrefixSpace)
+        (invalid SyntaxPragmaMissingKeyword)
+    let (keyword, afterKeyword) =
+            Text.break isHorizontalSpace afterPrefixSpace
+    associativity <-
+        case keyword of
+            "infixl" ->
+                Right LeftAssoc
+            "infixr" ->
+                Right RightAssoc
+            "infix" ->
+                Right NonAssoc
+            _ ->
+                invalid (SyntaxPragmaUnknownKeyword keyword)
+    afterKeywordSpace <-
+        case Text.uncons afterKeyword of
+            Nothing ->
+                invalid SyntaxPragmaMissingLevel
+            Just{} ->
+                Right (Text.dropWhile isHorizontalSpace afterKeyword)
+    when
+        (Text.null afterKeywordSpace)
+        (invalid SyntaxPragmaMissingLevel)
+    let (digits, trailing) =
+            Text.span isAsciiDigit afterKeywordSpace
+    when
+        (Text.null digits)
+        (invalid SyntaxPragmaInvalidLevel)
+    level <-
+        maybe
+            (invalid SyntaxPragmaLevelOutOfRange)
+            (Right . SourceMixfixLevel)
+            (sourceLevel digits)
+    unless
+        (Text.null (Text.dropWhile isHorizontalSpace trailing))
+        (invalid SyntaxPragmaTrailingContent)
+    pure
+        LocatedFixityPragma
+            { syntaxPragmaLocation = location
+            , syntaxPragmaAssociativity = associativity
+            , syntaxPragmaLevel = level
+            }
+
+isHorizontalSpace :: Char -> Bool
+isHorizontalSpace char =
+    char == ' ' || char == '\t'
+
+isAsciiDigit :: Char -> Bool
+isAsciiDigit char =
+    '0' <= char && char <= '9'
+
+sourceLevel :: Text -> Maybe Word8
+sourceLevel =
+    Text.foldl' step (Just 0)
+  where
+    step Nothing _ =
+        Nothing
+    step (Just current) char =
+        let next =
+                current * 10
+                    + fromIntegral (ord char - ord '0')
+        in
+            if next <= 7
+                then Just next
+                else Nothing
diff --git a/source/Felix/Syntax/Token.hs b/source/Felix/Syntax/Token.hs
new file mode 100644
index 0000000..31d1d19
--- /dev/null
+++ b/source/Felix/Syntax/Token.hs
@@ -0,0 +1,633 @@
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- |
+-- This module defines the lexer and its associated data types.
+-- The lexer takes `Text` as input and produces a stream of tokens
+-- annotated with positional information. This information is bundled
+-- together with the original raw input for producing error messages.
+--
+-- The lexer perfoms some normalizations to make describing the grammar easier.
+-- Words outside of math environments are case-folded. Some commands are analysed
+-- as variable tokens and are equivalent to their respective unicode variants
+-- (α, β, γ, ..., 𝔸, 𝔹, ℂ, ...). Similarly, @\\begin{...}@ and @\\end{...}@ commands
+-- are each parsed as single tokens.
+--
+module Felix.Syntax.Token
+    ( Token(..)
+    , VariableDisplay(..)
+    , VariableSuffix(..)
+    , displayVariable
+    , renderVariableText
+    , tokToString
+    , tokToText
+    , TokStream(..)
+    , Located(..)
+    , runLexer
+    , gatherImports
+    ) where
+
+
+import Base hiding (many)
+
+import Felix.Report.Location
+
+import Control.DeepSeq (NFData)
+import Control.Monad.Combinators
+import Control.Monad.State.Strict
+import Data.List.NonEmpty qualified as NonEmpty
+import Data.Text qualified as Text
+import Prettyprinter (Pretty(..))
+import Text.Megaparsec hiding (Token, Label, label)
+import Text.Megaparsec.Char qualified as Char
+import Text.Megaparsec.Char.Lexer qualified as Lexer
+import Tptp.UnsortedFirstOrder (isAsciiLetter, isAsciiAlphaNumOrUnderscore)
+
+
+runLexer :: FileId -> String -> Text -> Either (ParseErrorBundle Text Void) ([FilePath], [[Located Token]])
+runLexer fileId file raw = runParser (evalStateT document (initLexerState fileId)) file raw
+
+
+type Lexer = StateT LexerState (Parsec Void Text)
+
+
+data LexerState = LexerState
+    { frames :: !(NonEmpty Frame)
+    , currentFileId :: !FileId
+    } deriving (Show, Eq)
+
+data Frame
+    = TopText
+    | MathFrame !Text
+    | TextFrame !Int
+    deriving (Show, Eq)
+
+initLexerState :: FileId -> LexerState
+initLexerState fileId = LexerState (TopText :| []) fileId
+
+topFrameOf :: LexerState -> Frame
+topFrameOf LexerState{frames = frame :| _} = frame
+
+topFrame :: Lexer Frame
+topFrame = gets topFrameOf
+
+pushFrame :: Frame -> LexerState -> LexerState
+pushFrame frame st@LexerState{frames = top :| rest} =
+    st{frames = frame :| (top : rest)}
+
+popFrame :: LexerState -> LexerState
+popFrame st@LexerState{frames = _ :| []} = st
+popFrame st@LexerState{frames = _ :| (top : rest)} =
+    st{frames = top :| rest}
+
+modifyTopFrame :: (Frame -> Frame) -> LexerState -> LexerState
+modifyTopFrame f st@LexerState{frames = top :| rest} =
+    st{frames = f top :| rest}
+
+-- Token recognizers only emit tokens; this is the single place that changes
+-- lexical context.
+advance :: Token -> LexerState -> LexerState
+advance tok st =
+    case (topFrameOf st, tok) of
+        (TopText, BeginEnv "math") ->
+            pushFrame (MathFrame "math") st
+        (TextFrame{}, BeginEnv "math") ->
+            pushFrame (MathFrame "math") st
+        (TopText, BeginEnv "align*") ->
+            pushFrame (MathFrame "align*") st
+        (TextFrame{}, BeginEnv "align*") ->
+            pushFrame (MathFrame "align*") st
+        (MathFrame env, EndEnv env')
+            | env == env' ->
+                popFrame st
+        (MathFrame{}, BeginEnv "text") ->
+            pushFrame (TextFrame 1) st
+        (TextFrame n, InvisibleBraceL) ->
+            modifyTopFrame (const (TextFrame (n + 1))) st
+        (TextFrame n, InvisibleBraceR)
+            | n > 1 ->
+                modifyTopFrame (const (TextFrame (n - 1))) st
+        (TextFrame 1, EndEnv "text") ->
+            popFrame st
+        _ ->
+            st
+
+-- |
+-- A token stream as input stream for a parser. Contains the raw input
+-- before tokenization as 'Text' for showing error messages.
+--
+data TokStream = TokStream
+    { rawInput :: !Text
+    , unTokStream :: ![[Located Token]]
+    } deriving (Show, Eq)
+
+instance Semigroup TokStream where
+    TokStream raw1 toks1 <> TokStream raw2 toks2 = TokStream (raw1 <> raw2) (toks1 <> toks2)
+
+instance Monoid TokStream where
+    mempty = TokStream mempty mempty
+
+-- | A LaTeX token.
+-- Invisible delimiters 'InvisibleBraceL' and 'InvisibleBraceR' are
+-- unescaped braces used for grouping in TEX (@{@),
+-- visibles braces are escaped braces (@\\{@).
+data Token
+    = Word !Text
+    | Variable !Text
+    | Symbol !Text
+    | Integer !Int
+    | Command !Text
+    | Label Text -- ^ A /@\\label{...}@/ command (case-sensitive).
+    | Ref (NonEmpty Text) -- ^ A /@\\ref{...}@/ command (case-sensitive).
+    | BeginEnv !Text
+    | EndEnv !Text
+    | ParenL | ParenR
+    | BracketL | BracketR
+    | VisibleBraceL | VisibleBraceR
+    | InvisibleBraceL | InvisibleBraceR
+    deriving (Show, Eq, Ord, Generic, Hashable, NFData)
+
+instance IsString Token where
+    fromString w = Word (Text.pack w)
+
+data VariableDisplay = VariableDisplay
+    { variableBaseText :: !Text
+    , variableSuffix :: !(Maybe VariableSuffix)
+    } deriving (Show, Eq, Ord)
+
+data VariableSuffix
+    = VariableSubscript !Text
+    | VariableTicks !Int
+    deriving (Show, Eq, Ord)
+
+displayVariable :: Text -> VariableDisplay
+displayVariable rawName =
+    case splitVariableBase rawName of
+        Nothing ->
+            VariableDisplay rawName Nothing
+        Just (baseText, suffixText) ->
+            VariableDisplay baseText (displayVariableSuffix suffixText)
+
+renderVariableText :: Text -> Text
+renderVariableText rawName =
+    case displayVariable rawName of
+        VariableDisplay baseText Nothing ->
+            baseText
+        VariableDisplay baseText (Just (VariableTicks n)) ->
+            baseText <> Text.replicate n "'"
+        VariableDisplay baseText (Just (VariableSubscript subscriptText)) ->
+            baseText <> renderSubscriptText subscriptText
+
+splitVariableBase :: Text -> Maybe (Text, Text)
+splitVariableBase rawName =
+    matchBlackboardBase rawName <|> matchGreekBase rawName <|> matchSingleLetterBase rawName
+
+matchBlackboardBase :: Text -> Maybe (Text, Text)
+matchBlackboardBase rawName = do
+    suffixText <- Text.stripPrefix "bb" rawName
+    case Text.uncons suffixText of
+        Just (upper, rest)
+            | 'A' <= upper && upper <= 'Z' ->
+                Just ("bb" <> Text.singleton upper, rest)
+        _ ->
+            Nothing
+
+matchGreekBase :: Text -> Maybe (Text, Text)
+matchGreekBase rawName =
+    asum
+        [ (\suffixText -> (rendered, suffixText)) <$> Text.stripPrefix prefix rawName
+        | (prefix, rendered) <- greekVariables
+        ]
+
+matchSingleLetterBase :: Text -> Maybe (Text, Text)
+matchSingleLetterBase rawName = do
+    (baseChar, suffixText) <- Text.uncons rawName
+    pure (Text.singleton baseChar, suffixText)
+
+displayVariableSuffix :: Text -> Maybe VariableSuffix
+displayVariableSuffix suffixText
+    | Text.null suffixText =
+        Nothing
+    | Text.all (== '_') suffixText =
+        Just (VariableTicks (Text.length suffixText))
+    | otherwise =
+        Just (VariableSubscript (Text.replace "_" "'" suffixText))
+
+renderSubscriptText :: Text -> Text
+renderSubscriptText subscriptText
+    | Text.length subscriptText == 1 =
+        "_" <> subscriptText
+    | otherwise =
+        "_{" <> subscriptText <> "}"
+
+greekVariables :: [(Text, Text)]
+greekVariables =
+    [ ("alpha", "α"), ("beta", "β"), ("gamma", "γ"), ("delta", "δ")
+    , ("epsilon", "ε"), ("zeta", "ζ"), ("eta", "η"), ("theta", "θ")
+    , ("iota", "ι"), ("kappa", "κ"), ("lambda", "λ"), ("mu", "μ")
+    , ("nu", "ν"), ("xi", "ξ"), ("pi", "π"), ("rho", "ρ"), ("sigma", "σ")
+    , ("tau", "τ"), ("upsilon", "υ"), ("phi", "φ"), ("chi", "χ")
+    , ("psi", "ψ"), ("omega", "ω")
+    , ("Gamma", "Γ"), ("Delta", "Δ"), ("Theta", "Θ"), ("Lambda", "Λ")
+    , ("Xi", "Ξ"), ("Pi", "Π"), ("Sigma", "Σ"), ("Upsilon", "Υ")
+    , ("Phi", "Φ"), ("Psi", "Ψ"), ("Omega", "Ω")
+    ]
+
+tokToText :: Token -> Text
+tokToText = \case
+    Word w -> w
+    Variable v -> renderVariableText v
+    Symbol s -> s
+    Integer n -> Text.pack (show n)
+    Command cmd -> Text.cons '\\' cmd
+    Label m -> "\\label{" <> m <> "}"
+    Ref ms -> "\\ref{" <> Text.intercalate ", " (toList ms) <> "}"
+    BeginEnv "math" -> "$"
+    EndEnv "math" -> "$"
+    BeginEnv env -> "\\begin{" <> env <> "}"
+    EndEnv env -> "\\end{" <> env <> "}"
+    ParenL -> "("
+    ParenR -> ")"
+    BracketL -> "["
+    BracketR -> "]"
+    VisibleBraceL -> "\\{"
+    VisibleBraceR -> "\\}"
+    InvisibleBraceL -> "{"
+    InvisibleBraceR -> "}"
+
+tokToString :: Token -> String
+tokToString = Text.unpack . tokToText
+
+instance Pretty Token where
+    pretty = \case
+        Word w -> pretty w
+        Variable v -> pretty (renderVariableText v)
+        Symbol s -> pretty s
+        Integer n -> pretty n
+        Command cmd -> "\\" <> pretty cmd
+        Label m -> "\\label{" <> pretty m <> "}"
+        Ref m -> "\\ref{" <> pretty m <> "}"
+        BeginEnv env -> "\\begin{" <> pretty env <> "}"
+        EndEnv env -> "\\end{" <> pretty env <> "}"
+        ParenL -> "("
+        ParenR -> ")"
+        BracketL -> "["
+        BracketR -> "]"
+        VisibleBraceL -> "\\{"
+        VisibleBraceR -> "\\}"
+        InvisibleBraceL -> "{"
+        InvisibleBraceR -> "}"
+
+
+data Located a = Located
+    { startPos :: !Location
+    , unLocated :: !a
+    , postWhitespace :: Whitespace
+    } deriving (Show, Functor)
+
+data Whitespace = NoSpace | Space deriving (Show)
+
+collapseWhitespace :: [Whitespace] -> Whitespace
+collapseWhitespace = \case
+    Space : _ -> Space
+    NoSpace : ws -> collapseWhitespace ws
+    [] -> NoSpace
+
+instance Eq a  => Eq  (Located a) where (==) = (==) `on` unLocated
+instance Ord a => Ord (Located a) where compare = compare `on` unLocated
+
+
+document :: Lexer ([FilePath], [[Located Token]])
+document = do
+    is <- importBlock
+    es <- many environment
+    eof
+    return (unLocated <$> is, es)
+
+
+importBlock :: Lexer [Located FilePath]
+importBlock = do
+    void (skipManyTill skipChar importLineOrBeginEnvOrEof)
+    many importLine
+    where
+        -- When skipping to the import block, we first need to try parsing whitespace to properly handle comments and avoid picking up a commented import line at the start of the import block.
+        skipChar, importLineOrBeginEnvOrEof :: Lexer ()
+        skipChar = comment <|> void anySingle
+        importLineOrBeginEnvOrEof =
+            lookAhead
+                (void (Char.string "\\import{")
+                    <|> void beginToplevelEnvironment)
+                <|> eof
+
+        importLine :: Lexer (Located FilePath) = lexeme do
+            Char.string "\\import{"
+            path <- some (satisfy isTheoryNameChar)
+            Char.char '}'
+            pure path
+
+        isTheoryNameChar :: Char -> Bool
+        isTheoryNameChar c =
+            c /= '}' && c /= '\n' && c /= '\r' && c /= '\0'
+
+-- | Scan only the leading import block. Source-graph construction uses this
+-- authority-free pass before parsing modules under their composed syntax.
+gatherImports
+    :: FileId
+    -> String
+    -> Text
+    -> Either (ParseErrorBundle Text Void) [Located FilePath]
+gatherImports fileId file =
+    runParser (evalStateT importBlock (initLexerState fileId)) file
+
+
+beginToplevelEnvironment :: Lexer (Located Text)
+beginToplevelEnvironment = lexeme do
+    Char.string "\\begin{"
+    env :: Text <- asum (Char.string <$> ["definition", "theorem", "lemma", "axiom", "proof", "corollary", "proposition", "claim", "abbreviation", "datatype", "inductive", "signature", "struct"])
+    Char.char '}'
+    pure env
+
+-- | Parses tokens, switching tokenizing frames when encountering math and text environments.
+environment :: Lexer [Located Token]
+environment = do
+    env <- skipManyTill (comment <|> void anySingle) beginToplevelEnvironment
+    lts <- go (unLocated env) id
+    pure ((BeginEnv <$> env) : lts)
+    where
+        go env f = do
+            frame <- topFrame
+            r <- optional (nextTokenFor frame)
+            case r of
+                Nothing ->
+                    pure (f [])
+                Just t@Located{unLocated = EndEnv env'}
+                    | frame == TopText && env == env' ->
+                        pure (f [t])
+                Just t -> do
+                    modify' (advance (unLocated t))
+                    go env (f . (t:))
+{-# INLINE environment #-}
+
+nextTokenFor :: Frame -> Lexer (Located Token)
+nextTokenFor = \case
+    TopText -> normalToken
+    MathFrame{} -> mathToken
+    TextFrame n -> textToken n
+
+-- | Parses a single normal-mode token.
+normalToken :: Lexer (Located Token)
+normalToken =
+    word <|> symbol <|> beginMath <|> beginAlign <|> subEnvironment <|> opening <|> closing <|> label <|> ref <|> end <|> command
+
+-- | Parses a single math mode token.
+mathToken :: Lexer (Located Token)
+mathToken =
+    var <|> symbol <|> number <|> beginCases <|> endAlign <|> endCases <|> opening <|> closing <|> beginText <|> beginExplanation <|> endMath <|> command
+
+beginText :: Lexer (Located Token)
+beginText = lexeme do
+    Char.string "\\text{" <|> Char.string "\\textbox{"
+    pure (BeginEnv "text")
+
+-- | Same as text modulo spacing, so we treat it synonymously
+beginExplanation :: Lexer (Located Token)
+beginExplanation = lexeme do
+    Char.string "\\explanation{"
+    pure (BeginEnv "text")
+
+subEnvironment :: Lexer (Located Token)
+subEnvironment = beginOrEnd ["enumerate", "subproof", "byCase"]
+    where
+        beginOrEnd envs = asum [beginEnv env <|> endEnv env | env <- envs]
+        beginEnv env = lexeme do
+            Char.string ("\\begin{" <> env <> "}")
+            pure (BeginEnv env)
+        endEnv env = lexeme do
+            Char.string ("\\end{" <> env <> "}")
+            pure (EndEnv env)
+
+-- | Normal mode embedded into math mode via @\text{...}@.
+textToken :: Int -> Lexer (Located Token)
+textToken n = word <|> symbol <|> textEnd <|> beginMath <|> beginAlign <|> opening' <|> closing' <|> ref <|> command
+    where
+        textEnd = lexeme do
+            guard (n == 1)
+            Char.char '}'
+            pure (EndEnv "text")
+
+        opening' = lexeme (group <|> optional (Char.string "\\left") *> (brace <|> paren <|> bracket))
+            where
+                brace = VisibleBraceL <$ lexeme (Char.string "\\{")
+                group = InvisibleBraceL <$ lexeme (Char.char '{')
+                paren = ParenL <$ lexeme (Char.char '(')
+                bracket = BracketL <$ lexeme (Char.char '[')
+
+        closing' = lexeme (group <|> optional (Char.string "\\right") *> (brace <|> paren <|> bracket))
+            where
+                brace = VisibleBraceR <$ lexeme (Char.string "\\}")
+                group = InvisibleBraceR <$ lexeme (Char.char '}')
+                paren = ParenR <$ lexeme (Char.char ')')
+                bracket = BracketR <$ lexeme (Char.char ']')
+
+
+-- | Parses a single begin math token.
+beginMath :: Lexer (Located Token)
+beginMath = lexeme do
+    Char.string "\\(" <|> Char.string "\\[" <|> Char.string "$"
+    pure (BeginEnv "math")
+
+beginAlign :: Lexer (Located Token)
+beginAlign = lexeme do
+    Char.string "\\begin{align*}"
+    pure (BeginEnv "align*")
+
+beginCases :: Lexer (Located Token)
+beginCases = lexeme do
+    Char.string "\\begin{cases}"
+    pure (BeginEnv "cases")
+
+-- | Parses a single end math token.
+endMath :: Lexer (Located Token)
+endMath = lexeme do
+    Char.string "\\)" <|> Char.string "\\]" <|> Char.string "$"
+    pure (EndEnv "math")
+
+endAlign :: Lexer (Located Token)
+endAlign = lexeme do
+    Char.string "\\end{align*}"
+    pure (EndEnv "align*")
+
+endCases :: Lexer (Located Token)
+endCases = lexeme do
+    Char.string "\\end{cases}"
+    pure (EndEnv "cases")
+
+
+-- | Parses the end of an environment.
+-- Commits only after having seen "\end{".
+end :: Lexer (Located Token)
+end = lexeme do
+    notFollowedBy (Char.string "\\end{cases}")
+    Char.string "\\end{"
+    env <- some (Char.letterChar <|> Char.char '*')
+    Char.char '}'
+    pure (EndEnv (Text.pack env))
+
+
+
+-- | Parses a word. Words are returned casefolded, since we want to ignore their case later on.
+word :: Lexer (Located Token)
+word = lexeme do
+    w <- some (Char.letterChar <|> Char.char '\'' <|> Char.char '-')
+    let t = Word (Text.toCaseFold (Text.pack w))
+    pure t
+
+number :: Lexer (Located Token)
+number = lexeme $ Integer <$> Lexer.decimal
+
+
+var :: Lexer (Located Token)
+var = lexeme (fmap Variable var')
+    where
+    var' = do
+        alphabeticPart <- letter <|> bb <|> greek
+        variationPart  <- subscript <|> ticked <|> pure ""
+        pure (alphabeticPart <> variationPart)
+
+    subscript :: Lexer Text
+    subscript = do
+        Char.char '_'
+        unbraced <|> braced <|> text
+        where
+            unbraced = Text.singleton <$> Char.alphaNumChar
+            braced = Text.pack <$> (Char.char '{' *> some (Char.alphaNumChar <|> tick) <* Char.char '}')
+            text = Char.string "\\text" *> braced -- for rendering the subscript in roman type
+
+    -- A bit of a hack to fit the TPTP format.
+    tick :: Lexer Char
+    tick = '_' <$ Char.char '\''
+
+    ticked :: Lexer Text
+    ticked = do
+        ticks <- some tick
+        pure (Text.pack ticks)
+
+    letter :: Lexer Text
+    letter = fmap Text.singleton Char.letterChar
+
+    greek :: Lexer Text
+    greek = try do
+        Char.char '\\'
+        l <- symbolParser greeks
+        notFollowedBy Char.letterChar
+        pure l
+
+    greeks :: [Text]
+    greeks =
+        [ "alpha", "beta", "gamma", "delta", "epsilon", "zeta", "eta", "theta"
+        , "iota", "kappa", "lambda", "mu", "nu", "xi", "pi", "rho", "sigma"
+        , "tau", "upsilon", "phi", "chi", "psi", "omega"
+        , "Gamma", "Delta", "Theta", "Lambda", "Xi", "Pi", "Sigma", "Upsilon"
+        , "Phi", "Psi", "Omega"
+        ]
+
+    bb :: Lexer Text
+    bb = do
+        Char.string "\\mathbb{"
+        l <-  symbolParser bbs
+        Char.char '}'
+        pure $ "bb" <> l
+
+    bbs :: [Text]
+    bbs = Text.singleton <$> ['A'..'Z']
+
+
+    symbolParser :: [Text] -> Lexer Text
+    symbolParser symbols = asum (fmap Char.string symbols)
+
+
+symbol :: Lexer (Located Token)
+symbol = lexeme do
+    symb <- some (satisfy (`elem` symbols))
+    pure (Symbol (Text.pack symb))
+        where
+        symbols :: [Char]
+        symbols = ".,:;!?@=≠+-/|^><≤≥*&≈⊂⊃⊆⊇∈“”‘’"
+
+-- | Parses a TEX-style command.
+command :: Lexer (Located Token)
+command = lexeme do
+    Char.char '\\'
+    cmd <- some Char.letterChar
+    pure (Command (Text.pack cmd))
+
+-- | Parses a label command and extracts its marker.
+label :: Lexer (Located Token)
+label = lexeme do
+    Char.string "\\label{"
+    m <- marker
+    Char.char '}'
+    pure (Label m)
+
+-- | Parses a label command and extracts its marker.
+ref :: Lexer (Located Token)
+ref = lexeme do
+    -- @\\cref@ is from @cleveref@ and @\\hyperref@ is from @hyperref@
+    cmd <- Char.string "\\ref{" <|> Char.string "\\cref{" <|> Char.string "\\hyperref["
+    ms <- NonEmpty.fromList <$> marker `sepBy1` Char.char ','
+    case cmd of
+        "\\hyperref[" -> Char.string "]{" *> some (satisfy (/= '}')) *> Char.char '}' *> pure (Ref ms)
+        _ -> Char.char '}' *> pure (Ref ms)
+
+marker :: Lexer Text
+marker = do
+    c <- satisfy isAsciiLetter
+    cs <- takeWhileP Nothing isAsciiAlphaNumOrUnderscore
+    pure (Text.cons c cs)
+
+-- | Parses an opening delimiter.
+opening :: Lexer (Located Token)
+opening = lexeme (group <|> optional (Char.string "\\left") *> (paren <|> brace <|> bracket))
+    where
+        brace = VisibleBraceL <$ lexeme (Char.string "\\{")
+        group = InvisibleBraceL <$ lexeme (Char.char '{')
+        paren = ParenL <$ lexeme (Char.char '(')
+        bracket = BracketL <$ lexeme (Char.char '[')
+
+-- | Parses a closing delimiter.
+closing :: Lexer (Located Token)
+closing = lexeme (group <|> optional (Char.string "\\right") *> (paren <|> brace <|> bracket))
+    where
+        brace = VisibleBraceR <$ lexeme (Char.string "\\}")
+        group = InvisibleBraceR <$ lexeme (Char.char '}')
+        paren = ParenR <$ lexeme (Char.char ')')
+        bracket = BracketR <$ lexeme (Char.char ']')
+
+-- | Turns a Lexer into one that tracks the source position of the token
+-- and consumes trailing whitespace.
+lexeme :: Lexer a -> Lexer (Located a)
+lexeme p = do
+    fileId <- gets currentFileId
+    start <- getSourcePos
+    location <-
+        either
+            (fail . show)
+            pure
+            (fromSourcePosChecked fileId start)
+    t <- p
+    w <- whitespace
+    pure (Located location t w)
+
+space :: Lexer Whitespace
+space = Space <$ (Char.char ' ' <|> Char.char '\n' <|> Char.char '\r')
+    <|> Space <$ (Char.string "\\ " <|> Char.string "\\\\" <|> Char.string "\\!" <|> Char.string "\\," <|> Char.string "\\:" <|> Char.string "\\;" <|> Char.string "\\;")
+
+whitespace :: Lexer Whitespace
+whitespace = do
+    ws <- many (spaces <|> NoSpace <$ comment)
+    pure (collapseWhitespace ws)
+    where
+        spaces = collapseWhitespace <$> some space
+
+comment :: Lexer ()
+comment = Lexer.skipLineComment "%"