path: root/source/Felix/Syntax/Adapt.hs

{-# 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)