path: root/source/Syntax/Lexicon.hs

{-# 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 Syntax.Lexicon
    ( module Syntax.Lexicon
    , pattern ConsSymbol
    , pattern PairSymbol
    , pattern CarrierSymbol
    , pattern ApplySymbol
    , pattern DomSymbol
    ) where


import Base
import Syntax.Abstract

import Data.List qualified as List
import Data.Sequence qualified as Seq
import Data.HashSet qualified as Set
import Data.HashMap.Strict qualified as HM
import Data.Text qualified as Text
import Text.Earley.Mixfix (Holey, Associativity(..))


data Lexicon = Lexicon
    { lexiconMixfix             :: Seq (HashMap (Holey Token) (Associativity, Marker))
    , lexiconConnectives        :: [[(Holey Token, Associativity)]]
    , lexiconPrefixPredicates   :: LexicalItems PrefixPredicate
    , lexiconStructFun          :: LexicalItems StructSymbol
    , lexiconRelationSymbols    :: LexicalItems RelationSymbol
    , lexiconVerbs              :: LexicalItems (SgPl LexicalPhrase)
    , lexiconAdjLs              :: LexicalItems LexicalPhrase
    , lexiconAdjRs              :: LexicalItems LexicalPhrase
    , lexiconNouns              :: LexicalItems (SgPl LexicalPhrase)
    , lexiconStructNouns        :: LexicalItems (SgPl LexicalPhrase)
    , lexiconFuns               :: LexicalItems (SgPl LexicalPhrase)
    } deriving (Show, Eq)

-- Projection returning the union of both left and right attributes.
--
lexiconAdjs :: Lexicon -> HashMap LexicalPhrase Marker
lexiconAdjs lexicon = lexiconAdjLs lexicon <> lexiconAdjRs lexicon

lookupOp :: FunctionSymbol -> Seq (HashMap FunctionSymbol (assoc, Marker)) -> Either String Marker
lookupOp f ops = case snd <$> firstJust (HM.lookup f) ops of
    Just m -> Right m
    Nothing -> Left (show f)

lookupLexicalItem :: (Hashable a, Show a) => a -> LexicalItems a -> Either String Marker
lookupLexicalItem a items = case HM.lookup a items of
    Just m -> Right m
    Nothing -> Left (show a)

type LexicalItems a = HashMap a Marker

builtins :: Lexicon
builtins = Lexicon
    { lexiconMixfix             = builtinMixfix
    , lexiconPrefixPredicates   = builtinPrefixPredicates
    , lexiconStructFun          = builtinStructOps
    , lexiconConnectives        = builtinConnectives
    , lexiconRelationSymbols    = builtinRelationSymbols
    , lexiconAdjLs              = mempty
    , lexiconAdjRs              = builtinAdjRs
    , lexiconVerbs              = builtinVerbs
    , lexiconNouns              = builtinNouns
    , lexiconStructNouns        = builtinStructNouns
    , lexiconFuns               = mempty
    }

-- INVARIANT: 10 precedence levels for now.
builtinMixfix :: Seq (HashMap FunctionSymbol (Associativity, Marker))
builtinMixfix = Seq.fromList $ (HM.fromList <$>)
    [ []
    , [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 :: [(FunctionSymbol, (Associativity, Marker))]
        builtinIdentifiers = identifier <$>
            [ "emptyset"
            , "naturals"
            , "integers"
            , "rationals"
            , "reals"
            , "unit"
            , "zero"
            ]

prefixOps :: [(FunctionSymbol, (Associativity, Marker))]
prefixOps =
    [ ([Just (Command "rfrac"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR, Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "rfrac"))
    , ([Just (Command "unions"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "unions"))
    , ([Just (Command "cumul"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "cumul"))
    , ([Just (Command "fst"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "fst"))
    , ([Just (Command "snd"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "snd"))
    , ([Just (Command "pow"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "pow"))
    , ([Just (Command "neg"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "neg"))
    , (ConsSymbol, (NonAssoc, "cons"))
    , (PairSymbol, (NonAssoc, "pair"))
    -- NOTE Is now defined and hence no longer necessary , (ApplySymbol, (NonAssoc, "apply"))
    ]


builtinStructOps :: LexicalItems StructSymbol
builtinStructOps = HM.fromList
    [ (CarrierSymbol, "carrier")
    ]

identifier :: Text -> (Holey Token, (Associativity, Marker))
identifier cmd = ([Just (Command cmd)], (NonAssoc, Marker cmd))


builtinRelationSymbols :: LexicalItems RelationSymbol
builtinRelationSymbols = HM.fromList
    [ (Symbol "=", "eq")
    , (Command "rless", "rless")
    , (Command "neq", "neq")
    , (Command "in", "elem")
    , (Command "notin", "notelem") -- Alternative to @\not\in@.
    ]

builtinPrefixPredicates :: LexicalItems PrefixPredicate
builtinPrefixPredicates = HM.fromList
    [ (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 -> (Holey Token, (Associativity, Marker))
binOp tok assoc m = ([Nothing, Just tok, Nothing], (assoc, m))

binOp' :: Token -> Associativity -> (Holey Token, Associativity)
binOp' tok assoc = ([Nothing, Just tok, Nothing], assoc)

builtinAdjRs :: LexicalItems LexicalPhrase
builtinAdjRs = HM.fromList
    [ (unsafeReadPhrase "equal to ?", "eq")
    ]

builtinVerbs :: LexicalItems (SgPl LexicalPhrase)
builtinVerbs = HM.fromList
    [ (unsafeReadPhraseSgPl "equal[s/] ?", "eq")
    ]


-- Some of these do/should correspond to mathlib structures,
-- e.g.: lattice, complete lattice, ring, etc.
--
builtinNouns :: LexicalItems (SgPl LexicalPhrase)
builtinNouns = HM.mapKeys unsafeReadPhraseSgPl (HM.fromList
    -- Nullary
    [ ("set[/s]", "set")
    , ("point[/s]", "point")
    , ("element[/s] of ?", "elem")
    ])

_Onesorted :: SgPl LexicalPhrase
_Onesorted = unsafeReadPhraseSgPl "onesorted structure[/s]"

builtinStructNouns :: LexicalItems (SgPl LexicalPhrase)
builtinStructNouns = HM.singleton _Onesorted "onesorted_structure"


-- | 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 phrase = case prepositionIndices <> nonhyphenatedSlotIndices of
    [] -> (phrase, []) -- Place variable slot at the end.
    is -> List.splitAt (minimum is) phrase
    where
        prepositionIndices, slotIndices, nonhyphenatedSlotIndices :: [Int] -- Ascending.
        prepositionIndices = List.findIndices isPreposition phrase
        slotIndices = List.findIndices isNothing phrase
        nonhyphenatedSlotIndices = [i | i <- slotIndices, noHyphen (nth (i + 1) phrase)]

        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 :: HashSet 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"
    ]