Migrate to `Felix` namespaceHEADhotg

1 files changed, 928 insertions, 0 deletions

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)