diff options
Diffstat (limited to 'source/Syntax/Adapt.hs')
| -rw-r--r-- | source/Syntax/Adapt.hs | 928 |
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) |