Migrate to `Felix` namespaceHEADhotg

1 files changed, 0 insertions, 330 deletions

diff --git a/source/Syntax/Lexicon.hs b/source/Syntax/Lexicon.hs
deleted file mode 100644
index 3e815c7..0000000
--- a/source/Syntax/Lexicon.hs
+++ /dev/null
@@ -1,330 +0,0 @@
-{-# 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 UpairSymbol
-    , pattern UnionsSymbol
-    , 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.Set qualified as Set
-import Data.Map.Strict qualified as Map
-import Data.Text qualified as Text
-import 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"
-    ]