{-# 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