summaryrefslogtreecommitdiff
path: root/source/Felix/Syntax/Lexicon.hs
diff options
context:
space:
mode:
Diffstat (limited to 'source/Felix/Syntax/Lexicon.hs')
-rw-r--r--source/Felix/Syntax/Lexicon.hs330
1 files changed, 330 insertions, 0 deletions
diff --git a/source/Felix/Syntax/Lexicon.hs b/source/Felix/Syntax/Lexicon.hs
new file mode 100644
index 0000000..c3332c7
--- /dev/null
+++ b/source/Felix/Syntax/Lexicon.hs
@@ -0,0 +1,330 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | The 'Lexicon' describes the part of the grammar that extensible/dynamic.
+--
+-- The items of the 'Lexicon' are organized by their meaning and their
+-- syntactic behaviour. They are typically represented as some kind of
+-- pattern data which is then used to generate various production rules
+-- for the concrete grammar. This representation makes inspection and
+-- extension easier.
+--
+
+module Felix.Syntax.Lexicon
+ ( module Felix.Syntax.Lexicon
+ , pattern ConsSymbol
+ , pattern PairSymbol
+ , pattern UpairSymbol
+ , pattern UnionsSymbol
+ , pattern CarrierSymbol
+ , pattern ApplySymbol
+ , pattern DomSymbol
+ ) where
+
+
+import Base
+import Felix.Syntax.Abstract
+
+import Data.List qualified as List
+import Data.Sequence qualified as Seq
+import Data.Set qualified as Set
+import Data.Map.Strict qualified as Map
+import Data.Text qualified as Text
+import Felix.Syntax.Mixfix (Holey)
+
+
+data SignatureHeadForm
+ = AdjectiveSignatureHead
+ | SymbolicSignatureHead
+ deriving (Show, Eq, Ord)
+
+-- Adjective heads must precede symbolic heads because both start with a math
+-- variable.
+concreteSignatureHeadForms :: [SignatureHeadForm]
+concreteSignatureHeadForms =
+ [ AdjectiveSignatureHead
+ , SymbolicSignatureHead
+ ]
+
+data Lexicon = Lexicon
+ { lexiconMixfixTable :: Seq (Map Pattern MixfixItem)
+ , lexiconConnectives :: [[(Holey Token, Associativity)]]
+ , lexiconPrefixPredicates :: [(PrefixPredicate, Marker)]
+ , lexiconStructFun :: [StructSymbol]
+ , lexiconRelationSymbols :: [RelationSymbol]
+ , lexiconVerbs :: [LexicalItemSgPl]
+ , lexiconAdjLs :: [LexicalItem]
+ , lexiconAdjRs :: [LexicalItem]
+ , lexiconNouns :: [LexicalItemSgPl]
+ , lexiconStructNouns :: [LexicalItemSgPl]
+ , lexiconFuns :: [LexicalItemSgPl]
+ } deriving (Show, Eq)
+
+-- Projection returning the union of both left and right attributes.
+--
+lexiconAdjs :: Lexicon -> [LexicalItem]
+lexiconAdjs lexicon = lexiconAdjLs lexicon <> lexiconAdjRs lexicon
+
+
+builtins :: Lexicon
+builtins =
+ Lexicon
+ { lexiconMixfixTable = builtinMixfixTable
+ , lexiconPrefixPredicates = builtinPrefixPredicates
+ , lexiconStructFun = builtinStructOps
+ , lexiconConnectives = builtinConnectives
+ , lexiconRelationSymbols = builtinRelationSymbols
+ , lexiconAdjLs = []
+ , lexiconAdjRs = builtinAdjRs
+ , lexiconVerbs = builtinVerbs
+ , lexiconNouns = builtinNouns
+ , lexiconStructNouns = builtinStructNouns
+ , lexiconFuns = []
+ }
+
+prefixPredicatePattern :: PrefixPredicate -> Pattern
+prefixPredicatePattern (PrefixPredicate command _arity) =
+ TokenCons (Command command) End
+
+builtinMixfixTable :: Seq (Map Pattern MixfixItem)
+builtinMixfixTable = Seq.fromList $ Map.fromList . fmap toEntry <$> builtinMixfixLevels
+ where
+ toEntry item@(MixfixItem pat _ _) = (pat, item)
+
+-- INVARIANT: 10 precedence levels for now.
+builtinMixfixLevels :: [[MixfixItem]]
+builtinMixfixLevels =
+ [ []
+ , [binOp (Symbol "+") LeftAssoc "add", binOp (Command "union") LeftAssoc "union", binOp (Symbol "-") LeftAssoc "minus", binOp (Command "rminus") LeftAssoc "rminus", binOp (Command "monus") LeftAssoc "monus"]
+ , [binOp (Command "relcomp") LeftAssoc "relcomp"]
+ , [binOp (Command "circ") LeftAssoc "circ"]
+ , [binOp (Command "mul") LeftAssoc "mul", binOp (Command "inter") LeftAssoc "inter", binOp (Command "rmul") LeftAssoc "rmul"]
+ , [binOp (Command "setminus") LeftAssoc "setminus"]
+ , [binOp (Command "times") RightAssoc "times"]
+ , []
+ , prefixOps
+ , builtinIdentifiers
+ ]
+ where
+ builtinIdentifiers :: [MixfixItem]
+ builtinIdentifiers = identifier <$>
+ [ "emptyset"
+ , "naturals"
+ , "naturalsPlus"
+ , "integers"
+ , "rationals"
+ , "reals"
+ , "unit"
+ , "zero"
+ ]
+
+
+prefixOps :: [MixfixItem]
+prefixOps =
+ [ mkMixfixItem [Just (Command "rfrac"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR, Just InvisibleBraceL, Nothing, Just InvisibleBraceR] "rfrac" NonAssoc
+ , mkMixfixItem [Just (Command "exp"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR, Just InvisibleBraceL, Nothing, Just InvisibleBraceR] "exp" NonAssoc
+ , UnionsSymbol
+ , mkMixfixItem [Just (Command "cumul"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR] "cumul" NonAssoc
+ , mkMixfixItem [Just (Command "fst"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR] "fst" NonAssoc
+ , mkMixfixItem [Just (Command "snd"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR] "snd" NonAssoc
+ , mkMixfixItem [Just (Command "pow"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR] "pow" NonAssoc
+ , mkMixfixItem [Just (Command "neg"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR] "neg" NonAssoc
+ , mkMixfixItem [Just (Command "inv"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR] "inv" NonAssoc
+ , mkMixfixItem [Just (Command "abs"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR] "abs" NonAssoc
+ , ConsSymbol
+ , PairSymbol
+ , UpairSymbol
+ -- NOTE Is now defined and hence no longer necessary , ApplySymbol
+ ]
+
+
+builtinStructOps :: [StructSymbol]
+builtinStructOps =
+ [ CarrierSymbol
+ ]
+
+identifier :: Text -> MixfixItem
+identifier cmd = mkMixfixItem [Just (Command cmd)] (Marker cmd) NonAssoc
+
+
+builtinRelationSymbols :: [RelationSymbol]
+builtinRelationSymbols =
+ [ RelationSymbol (Symbol "=") zeroParameterArity "eq"
+ , RelationSymbol (Command "rless") zeroParameterArity "rless"
+ , RelationSymbol (Command "neq") zeroParameterArity "neq"
+ , ElementSymbol
+ , NotElementSymbol -- Alternative to @\not\in@.
+ ]
+
+builtinPrefixPredicates :: [(PrefixPredicate, Marker)]
+builtinPrefixPredicates =
+ [ (PrefixPredicate "Cong" 4, "cong")
+ , (PrefixPredicate "Betw" 3, "betw")
+ ]
+
+
+builtinConnectives :: [[(Holey Token, Associativity)]]
+builtinConnectives =
+ [ [binOp' (Command "iff") NonAssoc]
+ , [binOp' (Command "implies") RightAssoc]
+ , [binOp' (Command "lor") LeftAssoc]
+ , [binOp' (Command "land") LeftAssoc]
+ , [([Just (Command "lnot"), Nothing], NonAssoc)]
+ ]
+
+
+binOp :: Token -> Associativity -> Marker -> MixfixItem
+binOp tok assoc m = mkMixfixItem [Nothing, Just tok, Nothing] m assoc
+
+binOp' :: Token -> Associativity -> (Holey Token, Associativity)
+binOp' tok assoc = ([Nothing, Just tok, Nothing], assoc)
+
+builtinAdjRs :: [LexicalItem]
+builtinAdjRs =
+ [ builtinEqualityRightAdjective
+ ]
+
+builtinEqualityRightAdjective :: LexicalItem
+builtinEqualityRightAdjective =
+ mkLexicalItem (unsafeReadPhrase "equal to ?") "eq"
+
+builtinVerbs :: [LexicalItemSgPl]
+builtinVerbs =
+ [ builtinEqualityVerb
+ ]
+
+builtinEqualityVerb :: LexicalItemSgPl
+builtinEqualityVerb =
+ mkLexicalItemSgPl (unsafeReadPhraseSgPl "equal[s/] ?") "eq"
+
+
+-- Some of these do/should correspond to mathlib structures,
+-- e.g.: lattice, complete lattice, ring, etc.
+--
+builtinNouns :: [LexicalItemSgPl]
+builtinNouns =
+ [ builtinSetNoun
+ , mkLexicalItemSgPl (unsafeReadPhraseSgPl "point[/s]") "point"
+ , builtinElementNoun
+ ]
+
+builtinSetNoun :: LexicalItemSgPl
+builtinSetNoun =
+ mkLexicalItemSgPl
+ (unsafeReadPhraseSgPl "set[/s]")
+ "set"
+
+builtinElementNoun :: LexicalItemSgPl
+builtinElementNoun =
+ mkLexicalItemSgPl
+ (unsafeReadPhraseSgPl "element[/s] of ?")
+ "elem"
+
+-- | Match the complete fixed-base identity, including the plural surface and
+-- authoritative marker. The ordinary 'Eq' instance intentionally compares
+-- only singular patterns.
+isBuiltinSetNoun :: LexicalItemSgPl -> Bool
+isBuiltinSetNoun item =
+ let actual = lexicalItemSgPlPattern item
+ expected = lexicalItemSgPlPattern builtinSetNoun
+ in sg actual == sg expected
+ && pl actual == pl expected
+ && lexicalItemSgPlMarker item
+ == lexicalItemSgPlMarker builtinSetNoun
+
+_Onesorted :: LexicalItemSgPl
+_Onesorted = mkLexicalItemSgPl (unsafeReadPhraseSgPl "onesorted structure[/s]") "onesorted_structure"
+
+builtinStructNouns :: [LexicalItemSgPl]
+builtinStructNouns = [_Onesorted]
+
+
+-- | Naïve splitting of lexical phrases to insert a variable slot for names in noun phrases,
+-- as in /@there exists a linear form $h$ on $E$@/, where the underlying pattern is
+-- /@linear form on ?@/. In this case we would get:
+--
+-- > splitOnVariableSlot (sg (unsafeReadPhraseSgPl "linear form[/s] on ?"))
+-- > ==
+-- > (unsafeReadPhrase "linear form", unsafeReadPhrase "on ?")
+--
+splitOnVariableSlot :: LexicalPhrase -> (LexicalPhrase, LexicalPhrase)
+splitOnVariableSlot pat = case prepositionIndices <> nonhyphenatedSlotIndices of
+ [] -> (pat, []) -- Place variable slot at the end.
+ is -> List.splitAt (minimum is) pat
+ where
+ prepositionIndices, slotIndices, nonhyphenatedSlotIndices :: [Int] -- Ascending.
+ prepositionIndices = List.findIndices isPreposition pat
+ slotIndices = List.findIndices isNothing pat
+ nonhyphenatedSlotIndices = [i | i <- slotIndices, noHyphen (nth (i + 1) pat)]
+
+ isPreposition :: Maybe Token -> Bool
+ isPreposition = \case
+ Just (Word w) -> w `Set.member` prepositions
+ _ -> False
+
+ noHyphen :: Maybe (Maybe Token) -> Bool
+ noHyphen = \case
+ Just (Just (Word w)) -> Text.head w /= '-'
+ -- If we arrive here, either the pattern is over (`Nothing`) or the next
+ -- part of the pattern is not a word that starts with a hyphen.
+ _ -> True
+
+
+-- Preposition are a closed class, but this list is not yet exhaustive.
+-- It can and should be extended when needed. The following list is a
+-- selection of the prepositions found at
+-- https://en.wikipedia.org/wiki/List_of_English_prepositions.
+--
+prepositions :: Set Text
+prepositions = Set.fromList
+ [ "about"
+ , "above"
+ , "across"
+ , "after"
+ , "against"
+ , "along", "alongside"
+ , "amid", "amidst"
+ , "among"
+ , "around"
+ , "as"
+ , "at"
+ , "atop"
+ , "before"
+ , "behind"
+ , "below"
+ , "beneath"
+ , "beside", "besides"
+ , "between"
+ , "beyond"
+ , "but"
+ , "by"
+ , "except"
+ , "for"
+ , "from"
+ , "in", "inside", "into"
+ , "like"
+ , "modulo", "mod"
+ , "near"
+ , "next"
+ , "of"
+ , "off"
+ , "on"
+ , "onto"
+ , "opposite"
+ , "out"
+ , "over"
+ , "past"
+ , "per"
+ , "sans"
+ , "till"
+ , "to"
+ , "under"
+ , "underneath"
+ , "unlike"
+ , "unto"
+ , "up", "upon"
+ , "versus"
+ , "via"
+ , "with"
+ , "within"
+ , "without"
+ ]
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-06 19:46:15 +0000