Migrate to `Felix` namespaceHEADhotg

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"
+    ]