Migrate to `Felix` namespaceHEADhotg

1 files changed, 0 insertions, 218 deletions

diff --git a/source/Checking/Exact/Vocabulary.hs b/source/Checking/Exact/Vocabulary.hs
deleted file mode 100644
index 45a2844..0000000
--- a/source/Checking/Exact/Vocabulary.hs
+++ /dev/null
@@ -1,218 +0,0 @@
-{-# LANGUAGE DerivingStrategies #-}
-{-# LANGUAGE NoImplicitPrelude #-}
-
--- | Semantic classification shared by the exact source compilers.
-module Checking.Exact.Vocabulary
-    ( FixedSemanticMeaning(..)
-    , fixedSemanticMeaning
-    , lowerFixedEqualityPredicate
-    , ExactSymbolClass(..)
-    , classifyExactSymbol
-    , FixedSetTermDispatch(..)
-    , dispatchFixedSetTerm
-    ) where
-
-import Base hiding (Empty)
-import Checking.Core
-import Checking.Semantic
-import Syntax.Abstract qualified as Raw
-import Syntax.Internal qualified as Internal
-import Syntax.Lexicon qualified as Lexicon
-
-import Data.List.NonEmpty qualified as NonEmpty
-import Data.Map.Strict qualified as Map
-
-
-data FixedSemanticMeaning
-    = FixedEquality
-    | FixedDisequality
-    | FixedIntrinsic !CoreIntrinsicTag
-    | FixedNegatedIntrinsic !CoreIntrinsicTag
-    deriving stock (Show, Eq)
-
-fixedSemanticMeaning
-    :: SemanticGlobalKey
-    -> Maybe FixedSemanticMeaning
-fixedSemanticMeaning key =
-    Map.lookup key fixedSemanticVocabulary
-
--- This inventory owns every exact source form that bypasses global lookup.
-fixedSemanticVocabulary
-    :: Map.Map SemanticGlobalKey FixedSemanticMeaning
-fixedSemanticVocabulary =
-    Map.fromList
-    [ ( relationKey Raw.EqSymbol
-      , FixedEquality
-      )
-    , ( SemanticRightAdjective
-            (Raw.lexicalItemPattern
-                Lexicon.builtinEqualityRightAdjective)
-      , FixedEquality
-      )
-    , ( verbKey Lexicon.builtinEqualityVerb
-      , FixedEquality
-      )
-    , ( relationKey Raw.ElementSymbol
-      , FixedIntrinsic Member
-      )
-    , ( relationKey Raw.NotElementSymbol
-      , FixedNegatedIntrinsic Member
-      )
-    , ( relationKey Raw.NeqSymbol
-      , FixedDisequality
-      )
-    , ( nounKey Lexicon.builtinElementNoun
-      , FixedIntrinsic Member
-      )
-    , ( expressionKey
-            (Raw.TokenCons (Raw.Command "emptyset") Raw.End)
-      , FixedIntrinsic Empty
-      )
-    , ( expressionKey (Raw.mixfixPattern Raw.UnionsSymbol)
-      , FixedIntrinsic FamilyUnion
-      )
-    , ( expressionKey (unaryCommandPattern "pow")
-      , FixedIntrinsic PowerSet
-      )
-    , ( expressionKey (unaryCommandPattern "cumul")
-      , FixedIntrinsic UnivOf
-      )
-    , ( expressionKey (Raw.mixfixPattern Raw.UpairSymbol)
-      , FixedIntrinsic PairSet
-      )
-    ]
-  where
-    relationKey relation =
-        SemanticRelation
-            (Raw.relationSymbolToken relation)
-            (Raw.relationSymbolParameterArity relation)
-    nounKey item =
-        let patterns = Raw.lexicalItemSgPlPattern item
-        in SemanticNoun (Raw.sg patterns) (Raw.pl patterns)
-    verbKey item =
-        let patterns = Raw.lexicalItemSgPlPattern item
-        in SemanticVerb (Raw.sg patterns) (Raw.pl patterns)
-    expressionKey = SemanticExpressionFunction
-
--- | Lower the fixed proposition meanings shared by raw exact elaboration and
--- the reusable internal-formula path. Membership deliberately retains its
--- carrier-aware source lowering and is not handled here.
-lowerFixedEqualityPredicate
-    :: FixedSemanticMeaning
-    -> [CanonicalTerm global]
-    -> Maybe (CanonicalTerm global)
-lowerFixedEqualityPredicate meaning arguments =
-    case (meaning, arguments) of
-        (FixedEquality, [left, right]) ->
-            Just (CEq TySet left right)
-        (FixedDisequality, [left, right]) ->
-            Just (CImp (CEq TySet left right) CFalsum)
-        _ ->
-            Nothing
-
-unaryCommandPattern :: Text -> Raw.Pattern
-unaryCommandPattern command =
-    Raw.TokenCons (Raw.Command command)
-        (Raw.TokenCons Raw.InvisibleBraceL
-            (Raw.HoleCons
-                (Raw.TokenCons Raw.InvisibleBraceR Raw.End)))
-
-data ExactSymbolClass
-    = ExactClosedLiteral
-    | ExactFixedPrimitive !FixedSemanticMeaning
-    | ExactSourceGlobal !(NonEmpty SemanticGlobalKey)
-    | ExactUnsupportedSymbol
-    deriving stock (Show, Eq)
-
-classifyExactSymbol :: Internal.Symbol -> ExactSymbolClass
-classifyExactSymbol symbol =
-    case symbol of
-        Internal.SymbolInteger{} ->
-            ExactClosedLiteral
-        _ ->
-            case NonEmpty.nonEmpty (semanticKeys symbol) of
-                Nothing ->
-                    ExactUnsupportedSymbol
-                Just keys ->
-                    case firstFixed keys of
-                        Just meaning ->
-                            ExactFixedPrimitive meaning
-                        Nothing ->
-                            ExactSourceGlobal keys
-  where
-    firstFixed =
-        foldr
-            (\key found -> fixedSemanticMeaning key <|> found)
-            Nothing
-
-semanticKeys :: Internal.Symbol -> [SemanticGlobalKey]
-semanticKeys = \case
-    Internal.SymbolMixfix symbol ->
-        [SemanticExpressionFunction (Raw.mixfixPattern symbol)]
-    Internal.SymbolFun item ->
-        let patterns = Raw.lexicalItemSgPlPattern item
-        in [SemanticFunctionPhrase (Raw.sg patterns) (Raw.pl patterns)]
-    Internal.SymbolPredicate predicate ->
-        case predicate of
-            Internal.PredicateAdj item ->
-                [ SemanticLeftAdjective (Raw.lexicalItemPattern item)
-                , SemanticRightAdjective (Raw.lexicalItemPattern item)
-                ]
-            Internal.PredicateVerb item ->
-                let patterns = Raw.lexicalItemSgPlPattern item
-                in [SemanticVerb (Raw.sg patterns) (Raw.pl patterns)]
-            Internal.PredicateNoun item ->
-                let patterns = Raw.lexicalItemSgPlPattern item
-                in [SemanticNoun (Raw.sg patterns) (Raw.pl patterns)]
-            Internal.PredicateRelation relation ->
-                [ SemanticRelation
-                    (Raw.relationSymbolToken relation)
-                    (Raw.relationSymbolParameterArity relation)
-                ]
-            Internal.PredicateSymbol{} -> []
-            Internal.PredicateNounStruct{} -> []
-    Internal.SymbolInteger{} -> []
-
--- | Result of interpreting a symbol already classified by the fixed exact
--- vocabulary as a set-valued term.
-data FixedSetTermDispatch global
-    = NotFixedSetTerm
-    | LoweredFixedSetTerm !(CanonicalTerm global)
-    | RejectedFixedSetTerm
-    deriving stock (Show, Eq)
-
--- | Interpret every fixed symbol that can occur in the reusable internal-term
--- lowering. Fixed relations are handled by formula lowering.
-dispatchFixedSetTerm
-    :: Internal.Symbol
-    -> [CanonicalTerm global]
-    -> FixedSetTermDispatch global
-dispatchFixedSetTerm symbol arguments =
-    case classifyExactSymbol symbol of
-        ExactFixedPrimitive meaning ->
-            case meaning of
-                FixedIntrinsic intrinsic ->
-                    applyIntrinsic
-                        (CIntrinsic intrinsic)
-                        (coreIntrinsicType intrinsic)
-                        arguments
-                FixedNegatedIntrinsic _intrinsic ->
-                    RejectedFixedSetTerm
-                FixedEquality ->
-                    RejectedFixedSetTerm
-                FixedDisequality ->
-                    RejectedFixedSetTerm
-        _ ->
-            NotFixedSetTerm
-  where
-    applyIntrinsic term coreType remaining =
-        case (coreType, remaining) of
-            (TySet, []) ->
-                LoweredFixedSetTerm term
-            (TyArrow TySet resultType, argument : rest) ->
-                applyIntrinsic
-                    (CApp term argument)
-                    resultType
-                    rest
-            _ ->
-                RejectedFixedSetTerm