Migrate to `Felix` namespaceHEADhotg

1 files changed, 218 insertions, 0 deletions

diff --git a/source/Felix/Checking/Exact/Vocabulary.hs b/source/Felix/Checking/Exact/Vocabulary.hs
new file mode 100644
index 0000000..a712bf1
--- /dev/null
+++ b/source/Felix/Checking/Exact/Vocabulary.hs
@@ -0,0 +1,218 @@
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | Semantic classification shared by the exact source compilers.
+module Felix.Checking.Exact.Vocabulary
+    ( FixedSemanticMeaning(..)
+    , fixedSemanticMeaning
+    , lowerFixedEqualityPredicate
+    , ExactSymbolClass(..)
+    , classifyExactSymbol
+    , FixedSetTermDispatch(..)
+    , dispatchFixedSetTerm
+    ) where
+
+import Base hiding (Empty)
+import Felix.Checking.Core
+import Felix.Checking.Semantic
+import Felix.Syntax.Abstract qualified as Raw
+import Felix.Syntax.Internal qualified as Internal
+import Felix.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