{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE NoImplicitPrelude #-}

-- | Checked logical inference over scoped canonical HOL terms.
module Felix.Checking.Kernel.Semantics
    ( implicationElimination
    , implicationIntroduction
    , forallElimination
    , forallIntroduction
    , falsumElimination
    , equalityReflexivity
    , equalityCongruenceApplication
    , equalityCongruenceLambda
    , equalityModusPonens
    , convertJudgment
    , KernelSemanticsError(..)
    ) where

import Base
import Felix.Checking.Core

import Control.Monad (unless)
import Data.Bifunctor (first)
import Numeric.Natural (Natural)


data KernelSemanticsError
    = KernelContextMismatch
        ![CoreType]
        ![CoreType]
    | KernelBinderContextMismatch
        !CoreType
        ![CoreType]
    | KernelExpectedProposition !CoreType
    | KernelExpectedImplication
    | KernelImplicationPremiseMismatch
    | KernelExpectedForall
    | KernelForallArgumentTypeMismatch
        !CoreType
        !CoreType
    | KernelExpectedFalsum
    | KernelExpectedEquality
    | KernelEqualityOperandTypeMismatch
        !CoreType
        !CoreType
    | KernelExpectedFunctionEquality !CoreType
    | KernelEqualityPremiseMismatch
    | KernelConversionBudgetExhausted
    | KernelConversionMismatch
    | KernelConclusionIllTyped !CoreCheckError
    deriving stock (Show, Eq)

implicationElimination
    :: Eq global
    => (global -> Maybe CoreType)
    -> ScopedCheckedCore global
    -> ScopedCheckedCore global
    -> Either
        KernelSemanticsError
        (ScopedCheckedCore global)
implicationElimination globalType implication premise = do
    requireSameContext implication premise
    requireProposition implication
    requireProposition premise
    case scopedCoreTerm implication of
        CImp expected conclusion
            | scopedCoreTerm premise == expected ->
                checkConclusion
                    globalType
                    (scopedCoreContext implication)
                    conclusion
            | otherwise ->
                Left KernelImplicationPremiseMismatch
        _ ->
            Left KernelExpectedImplication

implicationIntroduction
    :: (global -> Maybe CoreType)
    -> ScopedCheckedCore global
    -> ScopedCheckedCore global
    -> Either
        KernelSemanticsError
        (ScopedCheckedCore global)
implicationIntroduction globalType premise conclusion = do
    requireSameContext premise conclusion
    requireProposition premise
    requireProposition conclusion
    checkConclusion
        globalType
        (scopedCoreContext premise)
        (CImp
            (scopedCoreTerm premise)
            (scopedCoreTerm conclusion))

forallElimination
    :: (global -> Maybe CoreType)
    -> ScopedCheckedCore global
    -> ScopedCheckedCore global
    -> Either
        KernelSemanticsError
        (ScopedCheckedCore global)
forallElimination globalType quantified argument = do
    requireSameContext quantified argument
    requireProposition quantified
    case scopedCoreTerm quantified of
        CForall binderType body
            | scopedCoreType argument == binderType ->
                checkConclusion
                    globalType
                    (scopedCoreContext quantified)
                    (instantiateCanonical
                        (scopedCoreTerm argument)
                        body)
            | otherwise ->
                Left
                    (KernelForallArgumentTypeMismatch
                        binderType
                        (scopedCoreType argument))
        _ ->
            Left KernelExpectedForall

forallIntroduction
    :: (global -> Maybe CoreType)
    -> CoreType
    -> ScopedCheckedCore global
    -> Either
        KernelSemanticsError
        (ScopedCheckedCore global)
forallIntroduction globalType binderType body = do
    requireProposition body
    outerContext <-
        case scopedCoreContext body of
            actualBinder : context
                | actualBinder == binderType ->
                    Right context
                | otherwise ->
                    Left
                        (KernelBinderContextMismatch
                            binderType
                            (scopedCoreContext body))
            [] ->
                Left
                    (KernelBinderContextMismatch
                        binderType
                        [])
    checkConclusion
        globalType
        outerContext
        (CForall
            binderType
            (scopedCoreTerm body))

falsumElimination
    :: (global -> Maybe CoreType)
    -> ScopedCheckedCore global
    -> ScopedCheckedCore global
    -> Either
        KernelSemanticsError
        (ScopedCheckedCore global)
falsumElimination _globalType falsum target = do
    requireSameContext falsum target
    requireProposition falsum
    requireProposition target
    case scopedCoreTerm falsum of
        CFalsum ->
            Right target
        _ ->
            Left KernelExpectedFalsum

equalityReflexivity
    :: (global -> Maybe CoreType)
    -> ScopedCheckedCore global
    -> Either
        KernelSemanticsError
        (ScopedCheckedCore global)
equalityReflexivity globalType operand =
    checkConclusion
        globalType
        (scopedCoreContext operand)
        (CEq
            (scopedCoreType operand)
            (scopedCoreTerm operand)
            (scopedCoreTerm operand))

equalityCongruenceApplication
    :: (global -> Maybe CoreType)
    -> ScopedCheckedCore global
    -> ScopedCheckedCore global
    -> Either
        KernelSemanticsError
        (ScopedCheckedCore global)
equalityCongruenceApplication
        globalType
        functionEquality
        argumentEquality = do
    requireSameContext functionEquality argumentEquality
    (functionType, leftFunction, rightFunction) <-
        equalityOperands functionEquality
    (argumentType, leftArgument, rightArgument) <-
        equalityOperands argumentEquality
    case functionType of
        TyArrow expectedArgument resultType
            | expectedArgument == argumentType ->
                checkConclusion
                    globalType
                    (scopedCoreContext functionEquality)
                    (CEq
                        resultType
                        (CApp leftFunction leftArgument)
                        (CApp rightFunction rightArgument))
            | otherwise ->
                Left
                    (KernelEqualityOperandTypeMismatch
                        expectedArgument
                        argumentType)
        other ->
            Left (KernelExpectedFunctionEquality other)

equalityCongruenceLambda
    :: (global -> Maybe CoreType)
    -> CoreType
    -> ScopedCheckedCore global
    -> Either
        KernelSemanticsError
        (ScopedCheckedCore global)
equalityCongruenceLambda
        globalType
        binderType
        bodyEquality = do
    (bodyType, leftBody, rightBody) <-
        equalityOperands bodyEquality
    outerContext <-
        case scopedCoreContext bodyEquality of
            actualBinder : context
                | actualBinder == binderType ->
                    Right context
                | otherwise ->
                    Left
                        (KernelBinderContextMismatch
                            binderType
                            (scopedCoreContext bodyEquality))
            [] ->
                Left
                    (KernelBinderContextMismatch
                        binderType
                        [])
    checkConclusion
        globalType
        outerContext
        (CEq
            (TyArrow binderType bodyType)
            (CLam binderType leftBody)
            (CLam binderType rightBody))

equalityModusPonens
    :: Eq global
    => (global -> Maybe CoreType)
    -> ScopedCheckedCore global
    -> ScopedCheckedCore global
    -> Either
        KernelSemanticsError
        (ScopedCheckedCore global)
equalityModusPonens globalType propositionEquality premise = do
    requireSameContext propositionEquality premise
    requireProposition premise
    (operandType, left, right) <-
        equalityOperands propositionEquality
    unless
        (operandType == TyProp)
        (Left
            (KernelEqualityOperandTypeMismatch
                TyProp
                operandType))
    unless
        (left == scopedCoreTerm premise)
        (Left KernelEqualityPremiseMismatch)
    checkConclusion
        globalType
        (scopedCoreContext premise)
        right

-- | Recheck a displayed proposition and independently establish beta
-- conversion within the supplied contraction budget.
convertJudgment
    :: Eq global
    => (global -> Maybe CoreType)
    -> Natural
    -> ScopedCheckedCore global
    -> ScopedCheckedCore global
    -> Either
        KernelSemanticsError
        (ScopedCheckedCore global)
convertJudgment globalType budget source target = do
    requireSameContext source target
    requireProposition source
    requireProposition target
    sourceNormal <-
        normalizeCanonical budget
            (scopedCoreTerm source)
    targetNormal <-
        normalizeCanonical budget
            (scopedCoreTerm target)
    unless
        (sourceNormal == targetNormal)
        (Left KernelConversionMismatch)
    checkConclusion
        globalType
        (scopedCoreContext target)
        (scopedCoreTerm target)

requireSameContext
    :: ScopedCheckedCore global
    -> ScopedCheckedCore global
    -> Either KernelSemanticsError ()
requireSameContext left right
    | scopedCoreContext left
        == scopedCoreContext right =
            Right ()
    | otherwise =
        Left
            (KernelContextMismatch
                (scopedCoreContext left)
                (scopedCoreContext right))

requireProposition
    :: ScopedCheckedCore global
    -> Either KernelSemanticsError ()
requireProposition value
    | scopedCoreType value == TyProp =
        Right ()
    | otherwise =
        Left
            (KernelExpectedProposition
                (scopedCoreType value))

equalityOperands
    :: ScopedCheckedCore global
    -> Either
        KernelSemanticsError
        (CoreType, CanonicalTerm global, CanonicalTerm global)
equalityOperands equality = do
    requireProposition equality
    case scopedCoreTerm equality of
        CEq operandType left right ->
            Right (operandType, left, right)
        _ ->
            Left KernelExpectedEquality

checkConclusion
    :: (global -> Maybe CoreType)
    -> [CoreType]
    -> CanonicalTerm global
    -> Either
        KernelSemanticsError
        (ScopedCheckedCore global)
checkConclusion globalType context =
    first KernelConclusionIllTyped
        . checkScopedCanonicalCore globalType context

normalizeCanonical
    :: Natural
    -> CanonicalTerm global
    -> Either
        KernelSemanticsError
        (CanonicalTerm global)
normalizeCanonical budget term =
    fst <$> normalize budget term
  where
    normalize remaining = \case
        CBound index ->
            pure (CBound index, remaining)
        CGlobal global ->
            pure (CGlobal global, remaining)
        CIntrinsic intrinsic ->
            pure (CIntrinsic intrinsic, remaining)
        COpaqueInteger integer ->
            pure (COpaqueInteger integer, remaining)
        CApp function argument -> do
            (functionNormal, afterFunction) <-
                normalize remaining function
            case functionNormal of
                CLam _binderType body -> do
                    afterContraction <-
                        consumeReduction afterFunction
                    normalize
                        afterContraction
                        (instantiateCanonical
                            argument
                            body)
                _ -> do
                    (argumentNormal, afterArgument) <-
                        normalize afterFunction argument
                    pure
                        ( CApp
                            functionNormal
                            argumentNormal
                        , afterArgument
                        )
        CLam binderType body -> do
            (bodyNormal, remaining') <-
                normalize remaining body
            pure
                (CLam binderType bodyNormal, remaining')
        CFalsum ->
            pure (CFalsum, remaining)
        CImp premise conclusion -> do
            (premiseNormal, afterPremise) <-
                normalize remaining premise
            (conclusionNormal, afterConclusion) <-
                normalize afterPremise conclusion
            pure
                ( CImp premiseNormal conclusionNormal
                , afterConclusion
                )
        CEq operandType left right -> do
            (leftNormal, afterLeft) <-
                normalize remaining left
            (rightNormal, afterRight) <-
                normalize afterLeft right
            pure
                ( CEq
                    operandType
                    leftNormal
                    rightNormal
                , afterRight
                )
        CForall binderType body -> do
            (bodyNormal, remaining') <-
                normalize remaining body
            pure
                (CForall binderType bodyNormal, remaining')

    consumeReduction 0 =
        Left KernelConversionBudgetExhausted
    consumeReduction remaining =
        Right (remaining - 1)