Migrate to `Felix` namespaceHEADhotg

1 files changed, 0 insertions, 928 deletions

diff --git a/source/Syntax/Adapt.hs b/source/Syntax/Adapt.hs
deleted file mode 100644
index f496ead..0000000
--- a/source/Syntax/Adapt.hs
+++ /dev/null
@@ -1,928 +0,0 @@
-{-# LANGUAGE NoImplicitPrelude #-}
-{-# LANGUAGE ApplicativeDo #-}
-{-# LANGUAGE RecordWildCards #-}
-
-module Syntax.Adapt
-    ( FunctionPatternError(..)
-    , LexicalScanError(..)
-    , ScannedLexicalItem(..)
-    , scannedItemMarker
-    , canonicalScannedItem
-    , SyntaxMaterializationError(..)
-    , materializeSyntaxDelta
-    , scanChunk
-    ) where
-
-import Base
-import Syntax.Abstract
-import Syntax.Interface
-import Syntax.Lexicon
-import 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)