{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE NoImplicitPrelude #-}

-- | Checked monomorphic HOL syntax and its nameless in-memory form.
--
-- Scoped syntax is an operational construction language.  Only a checked,
-- frozen value is semantic input to later kernel and backend boundaries.
module Felix.Checking.Core
    ( CoreType(..)
    , CoreIntrinsicTag(..)
    , coreIntrinsicType
    , CoreSyntax
    , coreLocal
    , coreGlobal
    , coreIntrinsic
    , coreOpaqueInteger
    , coreApply
    , coreLambda
    , coreFalsum
    , coreImplication
    , coreEquality
    , coreForall
    , CheckedCore
    , checkedCoreType
    , checkCore
    , checkClosedCore
    , ClosedCheckedProposition
    , checkedPropositionCore
    , checkClosedProposition
    , CoreCheckError(..)
    , CanonicalTerm(..)
    , canonicalSetInsert
    , FrozenCheckedCore
    , frozenCoreType
    , frozenCoreTerm
    , thawFrozenCore
    , frozenCoreGlobals
    , mapFrozenGlobals
    , ScopedCheckedCore
    , scopedCoreContext
    , scopedCoreType
    , scopedCoreTerm
    , mapScopedGlobals
    , checkScopedCanonicalCore
    , embedClosedCore
    , weakenCheckedScopedCore
    , weakenScopedCore
    , scopedSetDefinition
    , scopedCharacteristicDefinition
    , scopedReplacementGraph
    , implyScopedCore
    , equalScopedCore
    , conjoinScopedCore
    , disjoinScopedCore
    , negateScopedCore
    , falsumScopedCore
    , splitScopedSetEquality
    , scopedSetInductionInstance
    , closeScopedForall
    , closeScopedExists
    , openScopedForall
    , openScopedImplication
    , openScopedAssumption
    , closeScopedCore
    , betaNormalizeCanonical
    , instantiateCanonical
    , shiftCanonical
    , mapCanonicalGlobals
    , canonicalTermGlobals
    , checkCanonicalCore
    , freezeClosed
    , FreezeError(..)
    , referenceFreezeClosed
    ) where

import Base hiding (Empty)

import Bound
import Control.DeepSeq (NFData)
import Control.Monad (ap, unless)
import Data.Set qualified as Set
import Numeric.Natural (Natural)


-- | The complete monomorphic type grammar of the checked core.
data CoreType
    = TyProp
    | TySet
    | TyArrow !CoreType !CoreType
    deriving stock (Show, Eq, Ord, Generic)
    deriving anyclass (NFData)


-- | The complete set-forming primitive inventory.
data CoreIntrinsicTag
    = Member
    | Empty
    | PairSet
    | FamilyUnion
    | PowerSet
    | Sep
    | Repl
    | SetChoose
    | UnivOf
    -- | The bounded set-valued least fixed point. It denotes the elements of
    -- its bound that belong to every bounded pre-fixed point of its operator.
    | ISetLfp
    deriving stock (Show, Eq, Ord, Enum, Bounded, Generic)
    deriving anyclass (NFData)

coreIntrinsicType :: CoreIntrinsicTag -> CoreType
coreIntrinsicType = \case
    Member ->
        TySet `TyArrow` (TySet `TyArrow` TyProp)
    Empty ->
        TySet
    PairSet ->
        TySet `TyArrow` (TySet `TyArrow` TySet)
    FamilyUnion ->
        TySet `TyArrow` TySet
    PowerSet ->
        TySet `TyArrow` TySet
    Sep ->
        TySet
            `TyArrow`
                ((TySet `TyArrow` TyProp) `TyArrow` TySet)
    Repl ->
        TySet
            `TyArrow`
                ((TySet `TyArrow` TySet) `TyArrow` TySet)
    SetChoose ->
        (TySet `TyArrow` TyProp) `TyArrow` TySet
    UnivOf ->
        TySet `TyArrow` TySet
    ISetLfp ->
        TySet
            `TyArrow`
                ((TySet `TyArrow` TySet) `TyArrow` TySet)


-- | Operational scoped syntax.  Its constructors remain private because this
-- value is neither a typing certificate nor an authority-bearing term.
data CoreSyntax global local
    = CoreLocal local
    | CoreGlobal global
    | CoreIntrinsic CoreIntrinsicTag
    | CoreOpaqueInteger !Integer
    | CoreApply
        !(CoreSyntax global local)
        !(CoreSyntax global local)
    | CoreLambda
        !CoreType
        !(Scope () (CoreSyntax global) local)
    | CoreFalsum
    | CoreImplication
        !(CoreSyntax global local)
        !(CoreSyntax global local)
    | CoreEquality
        !CoreType
        !(CoreSyntax global local)
        !(CoreSyntax global local)
    | CoreForall
        !CoreType
        !(Scope () (CoreSyntax global) local)
    deriving stock (Functor, Foldable, Traversable)

instance Applicative (CoreSyntax global) where
    pure = CoreLocal
    (<*>) = ap

instance Monad (CoreSyntax global) where
    CoreLocal local >>= replace =
        replace local
    CoreGlobal global >>= _replace =
        CoreGlobal global
    CoreIntrinsic intrinsic >>= _replace =
        CoreIntrinsic intrinsic
    CoreOpaqueInteger integer >>= _replace =
        CoreOpaqueInteger integer
    CoreApply function argument >>= replace =
        CoreApply
            (function >>= replace)
            (argument >>= replace)
    CoreLambda binderType body >>= replace =
        CoreLambda binderType (body >>>= replace)
    CoreFalsum >>= _replace =
        CoreFalsum
    CoreImplication premise conclusion >>= replace =
        CoreImplication
            (premise >>= replace)
            (conclusion >>= replace)
    CoreEquality operandType left right >>= replace =
        CoreEquality
            operandType
            (left >>= replace)
            (right >>= replace)
    CoreForall binderType body >>= replace =
        CoreForall binderType (body >>>= replace)

coreLocal :: local -> CoreSyntax global local
coreLocal = CoreLocal

coreGlobal :: global -> CoreSyntax global local
coreGlobal = CoreGlobal

coreIntrinsic :: CoreIntrinsicTag -> CoreSyntax global local
coreIntrinsic = CoreIntrinsic

coreOpaqueInteger :: Integer -> CoreSyntax global local
coreOpaqueInteger = CoreOpaqueInteger

coreApply
    :: CoreSyntax global local
    -> CoreSyntax global local
    -> CoreSyntax global local
coreApply = CoreApply

coreLambda
    :: Eq local
    => CoreType
    -> local
    -> CoreSyntax global local
    -> CoreSyntax global local
coreLambda binderType local body =
    CoreLambda binderType (abstract1 local body)

coreFalsum :: CoreSyntax global local
coreFalsum = CoreFalsum

coreImplication
    :: CoreSyntax global local
    -> CoreSyntax global local
    -> CoreSyntax global local
coreImplication = CoreImplication

coreEquality
    :: CoreType
    -> CoreSyntax global local
    -> CoreSyntax global local
    -> CoreSyntax global local
coreEquality = CoreEquality

coreForall
    :: Eq local
    => CoreType
    -> local
    -> CoreSyntax global local
    -> CoreSyntax global local
coreForall binderType local body =
    CoreForall binderType (abstract1 local body)


data CoreCheckError
    = UnknownCoreGlobal
    | UnboundCoreLocal
    | UnboundCoreIndex !Natural
    | AppliedNonFunction !CoreType
    | ApplicationArgumentTypeMismatch
        !CoreType
        !CoreType
    | ImplicationOperandTypeMismatch
        !CoreType
    | EqualityOperandTypeMismatch
        !CoreType
        !CoreType
    | QuantifierBodyTypeMismatch
        !CoreType
    | ExpectedCoreType
        !CoreType
        !CoreType
    deriving stock (Show, Eq)


-- | A scoped term whose complete tree has been type checked.
data CheckedCore global local = CheckedCore
    !CoreType
    !(CoreSyntax global local)

checkedCoreType :: CheckedCore global local -> CoreType
checkedCoreType (CheckedCore coreType _syntax) =
    coreType

checkCore
    :: (global -> Maybe CoreType)
    -> (local -> Maybe CoreType)
    -> CoreSyntax global local
    -> Either CoreCheckError (CheckedCore global local)
checkCore globalType localType syntax = do
    coreType <-
        inferCore globalType localType syntax
    pure (CheckedCore coreType syntax)

checkClosedCore
    :: (global -> Maybe CoreType)
    -> CoreSyntax global local
    -> Either CoreCheckError (CheckedCore global Void)
checkClosedCore globalType syntax = do
    closedSyntax <-
        maybe
            (Left UnboundCoreLocal)
            Right
            (traverse (const Nothing) syntax)
    checkCore globalType absurd closedSyntax

newtype ClosedCheckedProposition global =
    ClosedCheckedProposition (CheckedCore global Void)

checkedPropositionCore
    :: ClosedCheckedProposition global
    -> CheckedCore global Void
checkedPropositionCore
    (ClosedCheckedProposition proposition) =
        proposition

checkClosedProposition
    :: (global -> Maybe CoreType)
    -> CoreSyntax global local
    -> Either CoreCheckError (ClosedCheckedProposition global)
checkClosedProposition globalType syntax = do
    checked <-
        checkClosedCore globalType syntax
    unless
        (checkedCoreType checked == TyProp)
        (Left
            (ExpectedCoreType
                TyProp
                (checkedCoreType checked)))
    pure (ClosedCheckedProposition checked)

inferCore
    :: forall global local
     . (global -> Maybe CoreType)
    -> (local -> Maybe CoreType)
    -> CoreSyntax global local
    -> Either CoreCheckError CoreType
inferCore globalType localType =
    infer
        (maybe
            (Left UnboundCoreLocal)
            Right
            . localType)
  where
    infer
        :: forall local'
         . (local' -> Either CoreCheckError CoreType)
        -> CoreSyntax global local'
        -> Either CoreCheckError CoreType
    infer resolveLocal = \case
        CoreLocal local ->
            resolveLocal local
        CoreGlobal global ->
            maybe
                (Left UnknownCoreGlobal)
                Right
                (globalType global)
        CoreIntrinsic intrinsic ->
            Right (coreIntrinsicType intrinsic)
        CoreOpaqueInteger{} ->
            Right TySet
        CoreApply function argument -> do
            functionType <-
                infer resolveLocal function
            argumentType <-
                infer resolveLocal argument
            case functionType of
                TyArrow expectedArgument resultType
                    | expectedArgument == argumentType ->
                        Right resultType
                    | otherwise ->
                        Left
                            (ApplicationArgumentTypeMismatch
                                expectedArgument
                                argumentType)
                other ->
                    Left (AppliedNonFunction other)
        CoreLambda binderType body -> do
            bodyType <-
                infer
                    (boundLocalType binderType resolveLocal)
                    (unscope body)
            Right (binderType `TyArrow` bodyType)
        CoreFalsum ->
            Right TyProp
        CoreImplication premise conclusion -> do
            premiseType <-
                infer resolveLocal premise
            unless
                (premiseType == TyProp)
                (Left
                    (ImplicationOperandTypeMismatch
                        premiseType))
            conclusionType <-
                infer resolveLocal conclusion
            unless
                (conclusionType == TyProp)
                (Left
                    (ImplicationOperandTypeMismatch
                        conclusionType))
            Right TyProp
        CoreEquality operandType left right -> do
            leftType <-
                infer resolveLocal left
            unless
                (leftType == operandType)
                (Left
                    (EqualityOperandTypeMismatch
                        operandType
                        leftType))
            rightType <-
                infer resolveLocal right
            unless
                (rightType == operandType)
                (Left
                    (EqualityOperandTypeMismatch
                        operandType
                        rightType))
            Right TyProp
        CoreForall binderType body -> do
            bodyType <-
                infer
                    (boundLocalType binderType resolveLocal)
                    (unscope body)
            unless
                (bodyType == TyProp)
                (Left
                    (QuantifierBodyTypeMismatch bodyType))
            Right TyProp

    boundLocalType
        :: forall local'
         . CoreType
        -> (local' -> Either CoreCheckError CoreType)
        -> Var () (CoreSyntax global local')
        -> Either CoreCheckError CoreType
    boundLocalType binderType outerType = \case
        B () ->
            Right binderType
        F outerSyntax ->
            infer outerType outerSyntax


-- | Felix-owned explicit-index syntax.  Index zero denotes the nearest
-- enclosing binder.
data CanonicalTerm global
    = CBound !Natural
    | CGlobal !global
    | CIntrinsic !CoreIntrinsicTag
    | COpaqueInteger !Integer
    | CApp
        !(CanonicalTerm global)
        !(CanonicalTerm global)
    | CLam
        !CoreType
        !(CanonicalTerm global)
    | CFalsum
    | CImp
        !(CanonicalTerm global)
        !(CanonicalTerm global)
    | CEq
        !CoreType
        !(CanonicalTerm global)
        !(CanonicalTerm global)
    | CForall
        !CoreType
        !(CanonicalTerm global)
    deriving stock (Show, Eq, Ord, Generic)
    deriving anyclass (NFData)

-- | The fixed checked-core interpretation of set insertion.
--
-- Finite-set notation uses this intrinsic HOTG adjunction directly.  The
-- ordinary source-owned @cons@ function is not consulted during lowering.
canonicalSetInsert
    :: CanonicalTerm global
    -> CanonicalTerm global
    -> CanonicalTerm global
canonicalSetInsert element set =
    CApp
        (CIntrinsic FamilyUnion)
        (CApp
            (CApp
                (CIntrinsic PairSet)
                (CApp
                    (CApp
                        (CIntrinsic PairSet)
                        element)
                    element))
            set)

data FrozenCheckedCore global = FrozenCheckedCore
    !CoreType
    !(CanonicalTerm global)
    deriving stock (Show, Eq, Ord, Generic)
    deriving anyclass (NFData)

frozenCoreType :: FrozenCheckedCore global -> CoreType
frozenCoreType (FrozenCheckedCore coreType _term) =
    coreType

frozenCoreTerm :: FrozenCheckedCore global -> CanonicalTerm global
frozenCoreTerm (FrozenCheckedCore _coreType term) =
    term

mapFrozenGlobals
    :: (global -> global')
    -> FrozenCheckedCore global
    -> FrozenCheckedCore global'
mapFrozenGlobals transform
        (FrozenCheckedCore coreType term) =
    FrozenCheckedCore
        coreType
        (mapCanonicalGlobals transform term)

-- | Recover an operational closed term from a checked frozen value. Any caller
-- that extends or substitutes it must check the resulting term again.
thawFrozenCore
    :: FrozenCheckedCore global
    -> CoreSyntax global Void
thawFrozenCore (FrozenCheckedCore _coreType term) =
    case traverse (const Nothing) (go [] term) of
        Just closedSyntax ->
            closedSyntax
        Nothing ->
            impossible
                "a frozen core term became open while being thawed"
  where
    go
        :: [Natural]
        -> CanonicalTerm global
        -> CoreSyntax global Natural
    go binders = \case
        CBound index ->
            case lookupBinder index binders of
                Just local ->
                    coreLocal local
                Nothing ->
                    impossible
                        "a frozen core term contains an unbound index"
        CGlobal global ->
            coreGlobal global
        CIntrinsic intrinsic ->
            coreIntrinsic intrinsic
        COpaqueInteger integer ->
            coreOpaqueInteger integer
        CApp function argument ->
            coreApply
                (go binders function)
                (go binders argument)
        CLam binderType body ->
            let local =
                    fromIntegral (length binders)
            in coreLambda
                binderType
                local
                (go (local : binders) body)
        CFalsum ->
            coreFalsum
        CImp premise conclusion ->
            coreImplication
                (go binders premise)
                (go binders conclusion)
        CEq operandType left right ->
            coreEquality
                operandType
                (go binders left)
                (go binders right)
        CForall binderType body ->
            let local =
                    fromIntegral (length binders)
            in coreForall
                binderType
                local
                (go (local : binders) body)

    lookupBinder
        :: Natural
        -> [Natural]
        -> Maybe Natural
    lookupBinder _index [] =
        Nothing
    lookupBinder 0 (local : _rest) =
        Just local
    lookupBinder index (_local : rest) =
        lookupBinder (index - 1) rest

frozenCoreGlobals
    :: Ord global
    => FrozenCheckedCore global
    -> Set.Set global
frozenCoreGlobals =
    canonicalTermGlobals . frozenCoreTerm

canonicalTermGlobals
    :: Ord global
    => CanonicalTerm global
    -> Set.Set global
canonicalTermGlobals = \case
    CBound{} ->
        mempty
    CGlobal global ->
        Set.singleton global
    CIntrinsic{} ->
        mempty
    COpaqueInteger{} ->
        mempty
    CApp function argument ->
        canonicalTermGlobals function
            <> canonicalTermGlobals argument
    CLam _binderType body ->
        canonicalTermGlobals body
    CFalsum ->
        mempty
    CImp premise conclusion ->
        canonicalTermGlobals premise
            <> canonicalTermGlobals conclusion
    CEq _operandType left right ->
        canonicalTermGlobals left
            <> canonicalTermGlobals right
    CForall _binderType body ->
        canonicalTermGlobals body

-- | A checked canonical term relative to the listed nearest-first binders.
-- This is the construction boundary used by kernel replay; it carries no fact
-- authority.
data ScopedCheckedCore global = ScopedCheckedCore
    ![CoreType]
    !CoreType
    !(CanonicalTerm global)
    deriving stock (Show, Eq, Ord, Generic)
    deriving anyclass (NFData)

scopedCoreContext
    :: ScopedCheckedCore global
    -> [CoreType]
scopedCoreContext
        (ScopedCheckedCore context _coreType _term) =
    context

scopedCoreType
    :: ScopedCheckedCore global
    -> CoreType
scopedCoreType
        (ScopedCheckedCore _context coreType _term) =
    coreType

scopedCoreTerm
    :: ScopedCheckedCore global
    -> CanonicalTerm global
scopedCoreTerm
        (ScopedCheckedCore _context _coreType term) =
    term

mapScopedGlobals
    :: (left -> right)
    -> ScopedCheckedCore left
    -> ScopedCheckedCore right
mapScopedGlobals transform
        (ScopedCheckedCore context coreType term) =
    ScopedCheckedCore
        context
        coreType
        (mapCanonicalGlobals transform term)

checkScopedCanonicalCore
    :: (global -> Maybe CoreType)
    -> [CoreType]
    -> CanonicalTerm global
    -> Either CoreCheckError (ScopedCheckedCore global)
checkScopedCanonicalCore globalType context term =
    ScopedCheckedCore context
        <$> inferCanonicalCore globalType context term
        <*> pure term

-- | Regard a closed term under a larger lexical context. Closed canonical
-- terms contain no indices, so this does not shift the term.
embedClosedCore
    :: [CoreType]
    -> FrozenCheckedCore global
    -> ScopedCheckedCore global
embedClosedCore context
        (FrozenCheckedCore coreType term) =
    ScopedCheckedCore context coreType term

-- | Add one nearest binder to an already checked lexical context.
weakenCheckedScopedCore
    :: CoreType
    -> ScopedCheckedCore global
    -> ScopedCheckedCore global
weakenCheckedScopedCore binderType scoped =
    ScopedCheckedCore
        (binderType : scopedCoreContext scoped)
        (scopedCoreType scoped)
        (shiftCanonical 1 0 (scopedCoreTerm scoped))

-- | Add one nearest binder to a checked lexical context.
weakenScopedCore
    :: (global -> Maybe CoreType)
    -> CoreType
    -> ScopedCheckedCore global
    -> Either CoreCheckError (ScopedCheckedCore global)
weakenScopedCore globalType binderType scoped =
    checkScopedCanonicalCore
        globalType
        (binderType : scopedCoreContext scoped)
        (shiftCanonical 1 0
            (scopedCoreTerm scoped))

-- | Introduce a fresh set-valued local definition. Separation specializes
-- the checked foundation characteristic so its local premise remains
-- first-order.
scopedSetDefinition
    :: Eq global
    => FrozenCheckedCore Void
    -> ScopedCheckedCore global
    -> Maybe (ScopedCheckedCore global)
scopedSetDefinition
        characteristic
        expression@(ScopedCheckedCore context TySet term) =
    case term of
        CApp
                (CApp (CIntrinsic Sep) bound)
                predicate@(CLam TySet _body) ->
            scopedCharacteristicDefinition
                characteristic
                expression
                ( ScopedCheckedCore context TySet bound
                    :| [ ScopedCheckedCore
                            context
                            (TySet `TyArrow` TyProp)
                            predicate
                       ]
                )
        _ ->
            Just
                (ScopedCheckedCore
                    (TySet : context)
                    TyProp
                    (CEq
                        TySet
                        (CBound 0)
                        (shiftCanonical 1 0 term)))
scopedSetDefinition _characteristic _expression =
    Nothing

-- | Specialize a checked characteristic and abstract its set-valued target
-- into one fresh nearest binder. Checked substitution and beta reduction
-- preserve the foundation row's proposition type.
scopedCharacteristicDefinition
    :: Eq global
    => FrozenCheckedCore Void
    -> ScopedCheckedCore global
    -> NonEmpty (ScopedCheckedCore global)
    -> Maybe (ScopedCheckedCore global)
scopedCharacteristicDefinition
        (FrozenCheckedCore TyProp frozen)
        (ScopedCheckedCore context TySet target)
        arguments
    | all ((== context) . scopedCoreContext) arguments = do
        specialized <-
            specialize
                (mapCanonicalGlobals absurd frozen)
                (toList arguments)
        let normalized = betaNormalizeCanonical specialized
            (found, abstracted) = abstractTarget 0 normalized
        guard found
        pure
            (ScopedCheckedCore
                (TySet : context)
                TyProp
                abstracted)
  where
    specialize term [] =
        Just term
    specialize (CForall binderType body)
            (ScopedCheckedCore _ argumentType argument : rest)
        | binderType == argumentType =
            specialize
                (instantiateCanonical argument body)
                rest
    specialize _term _arguments =
        Nothing

    abstractTarget depth term
        | term == shiftCanonical depth 0 target =
            (True, CBound (fromIntegral depth))
        | otherwise =
            case term of
                CBound index
                    | index < fromIntegral depth ->
                        (False, CBound index)
                    | otherwise ->
                        (False, CBound (index + 1))
                CGlobal global ->
                    (False, CGlobal global)
                CIntrinsic intrinsic ->
                    (False, CIntrinsic intrinsic)
                COpaqueInteger integer ->
                    (False, COpaqueInteger integer)
                CApp function argument ->
                    combine CApp
                        (abstractTarget depth function)
                        (abstractTarget depth argument)
                CLam binderType body ->
                    let (found, abstracted) =
                            abstractTarget (depth + 1) body
                    in (found, CLam binderType abstracted)
                CFalsum ->
                    (False, CFalsum)
                CImp premise conclusion ->
                    combine CImp
                        (abstractTarget depth premise)
                        (abstractTarget depth conclusion)
                CEq operandType left right ->
                    combine (CEq operandType)
                        (abstractTarget depth left)
                        (abstractTarget depth right)
                CForall binderType body ->
                    let (found, abstracted) =
                            abstractTarget (depth + 1) body
                    in (found, CForall binderType abstracted)

    combine constructor (leftFound, left) (rightFound, right) =
        (leftFound || rightFound, constructor left right)
scopedCharacteristicDefinition _characteristic _target _arguments =
    Nothing

-- | Build the replacement graph of one checked set-valued local function.
-- The ordered-pair constructor is an ordinary checked source object.
scopedReplacementGraph
    :: ScopedCheckedCore global
    -> ScopedCheckedCore global
    -> ScopedCheckedCore global
    -> Maybe
        ( ScopedCheckedCore global
        , ScopedCheckedCore global
        , ScopedCheckedCore global
        )
scopedReplacementGraph
        (ScopedCheckedCore context pairType pair)
        domain@(ScopedCheckedCore domainContext TySet domainTerm)
        (ScopedCheckedCore valueContext TySet value)
    | pairType == TySet `TyArrow` (TySet `TyArrow` TySet)
    , domainContext == context
    , valueContext == TySet : context =
        let pairValue =
                CApp
                    (CApp
                        (shiftCanonical 1 0 pair)
                        (CBound 0))
                    value
            function = CLam TySet pairValue
            graph =
                CApp
                    (CApp (CIntrinsic Repl) domainTerm)
                    function
        in Just
            ( ScopedCheckedCore context TySet graph
            , domain
            , ScopedCheckedCore
                context
                (TySet `TyArrow` TySet)
                function
            )
scopedReplacementGraph _pair _domain _value =
    Nothing

betaNormalizeCanonical
    :: CanonicalTerm global
    -> CanonicalTerm global
betaNormalizeCanonical = \case
    CApp function argument ->
        case betaNormalizeCanonical function of
            CLam _binderType body ->
                betaNormalizeCanonical
                    (instantiateCanonical
                        (betaNormalizeCanonical argument)
                        body)
            normalizedFunction ->
                CApp
                    normalizedFunction
                    (betaNormalizeCanonical argument)
    CLam binderType body ->
        CLam binderType (betaNormalizeCanonical body)
    CImp premise conclusion ->
        CImp
            (betaNormalizeCanonical premise)
            (betaNormalizeCanonical conclusion)
    CEq operandType left right ->
        CEq operandType
            (betaNormalizeCanonical left)
            (betaNormalizeCanonical right)
    CForall binderType body ->
        CForall binderType (betaNormalizeCanonical body)
    term -> term

-- | Combine two checked propositions under the same lexical context.
implyScopedCore
    :: ScopedCheckedCore global
    -> ScopedCheckedCore global
    -> Maybe (ScopedCheckedCore global)
implyScopedCore
        (ScopedCheckedCore premiseContext TyProp premise)
        (ScopedCheckedCore conclusionContext TyProp conclusion)
    | premiseContext == conclusionContext =
        Just
            (ScopedCheckedCore
                premiseContext
                TyProp
                (CImp premise conclusion))
implyScopedCore _premise _conclusion =
    Nothing

-- | Form an equality between checked operands under the same lexical
-- context.  This preserves the checked-core invariant without requiring a
-- caller to recover global types merely to combine already checked terms.
equalScopedCore
    :: ScopedCheckedCore global
    -> ScopedCheckedCore global
    -> Maybe (ScopedCheckedCore global)
equalScopedCore
        (ScopedCheckedCore leftContext leftType left)
        (ScopedCheckedCore rightContext rightType right)
    | leftContext == rightContext
    , leftType == rightType =
        Just
            (ScopedCheckedCore
                leftContext
                TyProp
                (CEq leftType left right))
equalScopedCore _left _right =
    Nothing

-- | Conjoin two checked propositions under the same lexical context.  Truth
-- is normalized away so callers can build an optional source guard without
-- retaining an inert conjunct.
conjoinScopedCore
    :: Eq global
    => ScopedCheckedCore global
    -> ScopedCheckedCore global
    -> Maybe (ScopedCheckedCore global)
conjoinScopedCore
        left@(ScopedCheckedCore leftContext TyProp leftTerm)
        right@(ScopedCheckedCore rightContext TyProp rightTerm)
    | leftContext == rightContext
    , leftTerm == truth = Just right
    | leftContext == rightContext
    , rightTerm == truth = Just left
    | leftContext == rightContext =
        Just
            (ScopedCheckedCore
                leftContext
                TyProp
                (CImp
                    (CImp leftTerm (CImp rightTerm CFalsum))
                    CFalsum))
  where
    truth = CImp CFalsum CFalsum
conjoinScopedCore _left _right =
    Nothing

-- | Disjoin two checked propositions under the same lexical context using
-- the fixed classical encoding owned by the checked core.
disjoinScopedCore
    :: ScopedCheckedCore global
    -> ScopedCheckedCore global
    -> Maybe (ScopedCheckedCore global)
disjoinScopedCore
        (ScopedCheckedCore leftContext TyProp left)
        (ScopedCheckedCore rightContext TyProp right)
    | leftContext == rightContext =
        Just
            (ScopedCheckedCore
                leftContext
                TyProp
                (CImp (CImp left CFalsum) right))
disjoinScopedCore _left _right =
    Nothing

-- | Negate a checked proposition without changing its lexical context.
negateScopedCore
    :: ScopedCheckedCore global
    -> Maybe (ScopedCheckedCore global)
negateScopedCore (ScopedCheckedCore context TyProp proposition) =
    Just
        (ScopedCheckedCore
            context
            TyProp
            (CImp proposition CFalsum))
negateScopedCore _proposition =
    Nothing

-- | Checked falsum at an already established lexical context.
falsumScopedCore :: [CoreType] -> ScopedCheckedCore global
falsumScopedCore context =
    ScopedCheckedCore context TyProp CFalsum

-- | Split a checked set equality into its two extensionality directions.
splitScopedSetEquality
    :: ScopedCheckedCore global
    -> Maybe
        ( ScopedCheckedCore global
        , ScopedCheckedCore global
        )
splitScopedSetEquality
        (ScopedCheckedCore context TyProp (CEq TySet left right)) =
    Just (subset left right, subset right left)
  where
    subset source target =
        ScopedCheckedCore
            context
            TyProp
            (CForall
                TySet
                (CImp
                    (memberOf (shiftCanonical 1 0 source))
                    (memberOf (shiftCanonical 1 0 target))))

    memberOf set =
        CApp
            (CApp
                (CIntrinsic Member)
                (CBound 0))
            set
splitScopedSetEquality _proposition =
    Nothing

-- | Derive the exact predicate, member-wise hypothesis, induction step, and
-- binder-level result for one set-valued ambient binder. The selected binder
-- is replaced by the newly introduced set variable; every other ambient
-- binder remains a parameter.
scopedSetInductionInstance
    :: Natural
    -> ScopedCheckedCore global
    -> Maybe
        ( ScopedCheckedCore global
        , ScopedCheckedCore global
        , ScopedCheckedCore global
        , ScopedCheckedCore global
        )
scopedSetInductionInstance selected
        (ScopedCheckedCore context TyProp property)
    | binderTypeAt selected context == Just TySet =
        Just (predicate, hypothesis, step, result)
  where
    abstractedProperty = abstractSelected 0 property
    predicate =
        ScopedCheckedCore
            context
            (TySet `TyArrow` TyProp)
            (CLam TySet abstractedProperty)
    hypothesis =
        ScopedCheckedCore
            context
            TyProp
            (CForall
                TySet
                (CImp
                    (CApp
                        (CApp
                            (CIntrinsic Member)
                            (CBound 0))
                        (CBound (selected + 1)))
                    abstractedProperty))
    step =
        ScopedCheckedCore
            context
            TyProp
            (CForall
                TySet
                (CImp
                    (abstractSelected
                        0
                        (scopedCoreTerm hypothesis))
                    abstractedProperty))
    result =
        ScopedCheckedCore
            context
            TyProp
            (CForall TySet abstractedProperty)

    abstractSelected depth = \case
        CBound index
            | index == depth + selected ->
                CBound depth
            | index >= depth ->
                CBound (index + 1)
            | otherwise ->
                CBound index
        CGlobal global ->
            CGlobal global
        CIntrinsic intrinsic ->
            CIntrinsic intrinsic
        COpaqueInteger integer ->
            COpaqueInteger integer
        CApp function argument ->
            CApp
                (abstractSelected depth function)
                (abstractSelected depth argument)
        CLam binderType body ->
            CLam binderType
                (abstractSelected (depth + 1) body)
        CFalsum ->
            CFalsum
        CImp premise conclusion ->
            CImp
                (abstractSelected depth premise)
                (abstractSelected depth conclusion)
        CEq operandType left right ->
            CEq operandType
                (abstractSelected depth left)
                (abstractSelected depth right)
        CForall binderType body ->
            CForall binderType
                (abstractSelected (depth + 1) body)
scopedSetInductionInstance _selected _property =
    Nothing

-- | Close the nearest checked binder as one leading universal.
closeScopedForall
    :: ScopedCheckedCore global
    -> Maybe (ScopedCheckedCore global)
closeScopedForall
        (ScopedCheckedCore (binderType : context) TyProp body) =
    Just
        (ScopedCheckedCore
            context
            TyProp
            (CForall binderType body))
closeScopedForall _scoped =
    Nothing

-- | Close the nearest checked binder as one leading existential.
closeScopedExists
    :: ScopedCheckedCore global
    -> Maybe (ScopedCheckedCore global)
closeScopedExists
        (ScopedCheckedCore (binderType : context) TyProp body) =
    Just
        (ScopedCheckedCore
            context
            TyProp
            (CImp
                (CForall binderType (CImp body CFalsum))
                CFalsum))
closeScopedExists _scoped =
    Nothing

-- | Open one checked leading universal without rechecking its body.
openScopedForall
    :: ScopedCheckedCore global
    -> Maybe (CoreType, ScopedCheckedCore global)
openScopedForall
        (ScopedCheckedCore context TyProp
            (CForall binderType body)) =
    Just
        ( binderType
        , ScopedCheckedCore
            (binderType : context)
            TyProp
            body
        )
openScopedForall _scoped =
    Nothing

-- | Split one checked implication under its unchanged ambient context.
openScopedImplication
    :: ScopedCheckedCore global
    -> Maybe
        ( ScopedCheckedCore global
        , ScopedCheckedCore global
        )
openScopedImplication
        (ScopedCheckedCore context TyProp
            (CImp premise conclusion)) =
    Just
        ( ScopedCheckedCore context TyProp premise
        , ScopedCheckedCore context TyProp conclusion
        )
openScopedImplication _scoped =
    Nothing

-- | Open a checked proof assumption against the current goal.  Besides a
-- direct implication antecedent, the source language historically permits
-- either immediate side of one binary conjunction antecedent to be assumed
-- first.  The other side remains the next implication antecedent.  This is a
-- deliberately shallow structural rule: it neither flattens conjunctions nor
-- treats disjunction as an eliminable assumption.
openScopedAssumption
    :: Eq global
    => ScopedCheckedCore global
    -> ScopedCheckedCore global
    -> Maybe
        ( ScopedCheckedCore global
        , ScopedCheckedCore global
        )
openScopedAssumption supplied goal = do
    (antecedent, conclusion) <- openScopedImplication goal
    if supplied == antecedent
        then pure (antecedent, conclusion)
        else do
            (left, right) <- splitScopedConjunction antecedent
            if supplied == left
                then do
                    remaining <- implyScopedCore right conclusion
                    pure (left, remaining)
                else if supplied == right
                    then do
                        remaining <- implyScopedCore left conclusion
                        pure (right, remaining)
                    else Nothing

splitScopedConjunction
    :: ScopedCheckedCore global
    -> Maybe
        ( ScopedCheckedCore global
        , ScopedCheckedCore global
        )
splitScopedConjunction
        (ScopedCheckedCore context TyProp
            (CImp (CImp left (CImp right CFalsum)) CFalsum)) =
    Just
        ( ScopedCheckedCore context TyProp left
        , ScopedCheckedCore context TyProp right
        )
splitScopedConjunction _scoped =
    Nothing

closeScopedCore
    :: ScopedCheckedCore global
    -> Maybe (FrozenCheckedCore global)
closeScopedCore
        (ScopedCheckedCore [] coreType term) =
    Just (FrozenCheckedCore coreType term)
closeScopedCore ScopedCheckedCore{} =
    Nothing

-- | Substitute an outer-context term for index zero and remove that binder.
instantiateCanonical
    :: CanonicalTerm global
    -> CanonicalTerm global
    -> CanonicalTerm global
instantiateCanonical argument =
    instantiateAt 0
  where
    instantiateAt depth = \case
        CBound index
            | index == depth ->
                shiftCanonical depth 0 argument
            | index > depth ->
                CBound (index - 1)
            | otherwise ->
                CBound index
        CGlobal global ->
            CGlobal global
        CIntrinsic intrinsic ->
            CIntrinsic intrinsic
        COpaqueInteger integer ->
            COpaqueInteger integer
        CApp function operand ->
            CApp
                (instantiateAt depth function)
                (instantiateAt depth operand)
        CLam binderType body ->
            CLam binderType
                (instantiateAt (depth + 1) body)
        CFalsum ->
            CFalsum
        CImp premise conclusion ->
            CImp
                (instantiateAt depth premise)
                (instantiateAt depth conclusion)
        CEq operandType left right ->
            CEq operandType
                (instantiateAt depth left)
                (instantiateAt depth right)
        CForall binderType body ->
            CForall binderType
                (instantiateAt (depth + 1) body)

mapCanonicalGlobals
    :: (global -> global')
    -> CanonicalTerm global
    -> CanonicalTerm global'
mapCanonicalGlobals transform = \case
    CBound index ->
        CBound index
    CGlobal global ->
        CGlobal (transform global)
    CIntrinsic intrinsic ->
        CIntrinsic intrinsic
    COpaqueInteger integer ->
        COpaqueInteger integer
    CApp function argument ->
        CApp
            (mapCanonicalGlobals transform function)
            (mapCanonicalGlobals transform argument)
    CLam binderType body ->
        CLam binderType
            (mapCanonicalGlobals transform body)
    CFalsum ->
        CFalsum
    CImp premise conclusion ->
        CImp
            (mapCanonicalGlobals transform premise)
            (mapCanonicalGlobals transform conclusion)
    CEq operandType left right ->
        CEq operandType
            (mapCanonicalGlobals transform left)
            (mapCanonicalGlobals transform right)
    CForall binderType body ->
        CForall binderType
            (mapCanonicalGlobals transform body)

-- | Recheck a nameless term without exposing the checked wrapper constructor.
checkCanonicalCore
    :: (global -> Maybe CoreType)
    -> CanonicalTerm global
    -> Either CoreCheckError (FrozenCheckedCore global)
checkCanonicalCore globalType term =
    FrozenCheckedCore
        <$> inferCanonicalCore globalType [] term
        <*> pure term

inferCanonicalCore
    :: (global -> Maybe CoreType)
    -> [CoreType]
    -> CanonicalTerm global
    -> Either CoreCheckError CoreType
inferCanonicalCore globalType binders = \case
    CBound index ->
        maybe
            (Left (UnboundCoreIndex index))
            Right
            (binderTypeAt index binders)
    CGlobal global ->
        maybe
            (Left UnknownCoreGlobal)
            Right
            (globalType global)
    CIntrinsic intrinsic ->
        Right (coreIntrinsicType intrinsic)
    COpaqueInteger{} ->
        Right TySet
    CApp function argument -> do
        functionType <-
            inferCanonicalCore globalType binders function
        argumentType <-
            inferCanonicalCore globalType binders argument
        case functionType of
            TyArrow expectedArgument resultType
                | expectedArgument == argumentType ->
                    Right resultType
                | otherwise ->
                    Left
                        (ApplicationArgumentTypeMismatch
                            expectedArgument
                            argumentType)
            other ->
                Left (AppliedNonFunction other)
    CLam binderType body -> do
        bodyType <-
            inferCanonicalCore
                globalType
                (binderType : binders)
                body
        Right (binderType `TyArrow` bodyType)
    CFalsum ->
        Right TyProp
    CImp premise conclusion -> do
        premiseType <-
            inferCanonicalCore globalType binders premise
        unless
            (premiseType == TyProp)
            (Left
                (ImplicationOperandTypeMismatch
                    premiseType))
        conclusionType <-
            inferCanonicalCore globalType binders conclusion
        unless
            (conclusionType == TyProp)
            (Left
                (ImplicationOperandTypeMismatch
                    conclusionType))
        Right TyProp
    CEq operandType left right -> do
        leftType <-
            inferCanonicalCore globalType binders left
        unless
            (leftType == operandType)
            (Left
                (EqualityOperandTypeMismatch
                    operandType
                    leftType))
        rightType <-
            inferCanonicalCore globalType binders right
        unless
            (rightType == operandType)
            (Left
                (EqualityOperandTypeMismatch
                    operandType
                    rightType))
        Right TyProp
    CForall binderType body -> do
        bodyType <-
            inferCanonicalCore
                globalType
                (binderType : binders)
                body
        unless
            (bodyType == TyProp)
            (Left
                (QuantifierBodyTypeMismatch bodyType))
        Right TyProp

binderTypeAt :: Natural -> [CoreType] -> Maybe CoreType
binderTypeAt _index [] =
    Nothing
binderTypeAt 0 (binderType : _rest) =
    Just binderType
binderTypeAt index (_binderType : rest) =
    binderTypeAt (index - 1) rest

shiftCanonical
    :: Natural
    -> Natural
    -> CanonicalTerm global
    -> CanonicalTerm global
shiftCanonical amount cutoff = \case
    CBound index
        | index >= cutoff ->
            CBound (index + amount)
        | otherwise ->
            CBound index
    CGlobal global ->
        CGlobal global
    CIntrinsic intrinsic ->
        CIntrinsic intrinsic
    COpaqueInteger integer ->
        COpaqueInteger integer
    CApp function argument ->
        CApp
            (shiftCanonical amount cutoff function)
            (shiftCanonical amount cutoff argument)
    CLam binderType body ->
        CLam binderType
            (shiftCanonical amount (cutoff + 1) body)
    CFalsum ->
        CFalsum
    CImp premise conclusion ->
        CImp
            (shiftCanonical amount cutoff premise)
            (shiftCanonical amount cutoff conclusion)
    CEq operandType left right ->
        CEq operandType
            (shiftCanonical amount cutoff left)
            (shiftCanonical amount cutoff right)
    CForall binderType body ->
        CForall binderType
            (shiftCanonical amount (cutoff + 1) body)

data FreezeError
    = FreeLocalInClosedCore
    deriving stock (Show, Eq)

-- | Freeze a checked closed term in one traversal of the operational syntax.
freezeClosed
    :: CheckedCore global Void
    -> Either FreezeError (FrozenCheckedCore global)
freezeClosed (CheckedCore coreType syntax) =
    FrozenCheckedCore coreType
        <$> optimizedFreeze 0 rootResolver syntax
  where
    rootResolver _depth =
        absurd

-- | Bounded executable oracle for tests.  Production code uses 'freezeClosed'.
referenceFreezeClosed
    :: CheckedCore global Void
    -> Either FreezeError (FrozenCheckedCore global)
referenceFreezeClosed (CheckedCore coreType syntax) =
    FrozenCheckedCore coreType
        <$> referenceFreeze 0 rootResolver syntax
  where
    rootResolver _depth =
        absurd

type VariableResolver local global =
    Natural
    -> local
    -> Either FreezeError (CanonicalTerm global)

optimizedFreeze
    :: Natural
    -> VariableResolver local global
    -> CoreSyntax global local
    -> Either FreezeError (CanonicalTerm global)
optimizedFreeze depth resolve = \case
    CoreLocal local ->
        resolve depth local
    CoreGlobal global ->
        Right (CGlobal global)
    CoreIntrinsic intrinsic ->
        Right (CIntrinsic intrinsic)
    CoreOpaqueInteger integer ->
        Right (COpaqueInteger integer)
    CoreApply function argument ->
        CApp
            <$> optimizedFreeze depth resolve function
            <*> optimizedFreeze depth resolve argument
    CoreLambda binderType body ->
        CLam binderType
            <$> optimizedFreeze
                (depth + 1)
                (resolveGeneralized depth resolve)
                (unscope body)
    CoreFalsum ->
        Right CFalsum
    CoreImplication premise conclusion ->
        CImp
            <$> optimizedFreeze depth resolve premise
            <*> optimizedFreeze depth resolve conclusion
    CoreEquality operandType left right ->
        CEq operandType
            <$> optimizedFreeze depth resolve left
            <*> optimizedFreeze depth resolve right
    CoreForall binderType body ->
        CForall binderType
            <$> optimizedFreeze
                (depth + 1)
                (resolveGeneralized depth resolve)
                (unscope body)
  where
    resolveGeneralized
        :: Natural
        -> VariableResolver local global
        -> VariableResolver
            (Var () (CoreSyntax global local))
            global
    resolveGeneralized binderLevel outerResolve currentDepth = \case
        B () ->
            Right
                (CBound
                    (currentDepth - binderLevel - 1))
        F outerSyntax ->
            optimizedFreeze
                currentDepth
                outerResolve
                outerSyntax

referenceFreeze
    :: Natural
    -> VariableResolver local global
    -> CoreSyntax global local
    -> Either FreezeError (CanonicalTerm global)
referenceFreeze depth resolve = \case
    CoreLocal local ->
        resolve depth local
    CoreGlobal global ->
        Right (CGlobal global)
    CoreIntrinsic intrinsic ->
        Right (CIntrinsic intrinsic)
    CoreOpaqueInteger integer ->
        Right (COpaqueInteger integer)
    CoreApply function argument ->
        CApp
            <$> referenceFreeze depth resolve function
            <*> referenceFreeze depth resolve argument
    CoreLambda binderType body ->
        CLam binderType
            <$> referenceFreeze
                (depth + 1)
                (resolveNormalized depth resolve)
                (fromScope body)
    CoreFalsum ->
        Right CFalsum
    CoreImplication premise conclusion ->
        CImp
            <$> referenceFreeze depth resolve premise
            <*> referenceFreeze depth resolve conclusion
    CoreEquality operandType left right ->
        CEq operandType
            <$> referenceFreeze depth resolve left
            <*> referenceFreeze depth resolve right
    CoreForall binderType body ->
        CForall binderType
            <$> referenceFreeze
                (depth + 1)
                (resolveNormalized depth resolve)
                (fromScope body)
  where
    resolveNormalized
        :: Natural
        -> VariableResolver local global
        -> VariableResolver (Var () local) global
    resolveNormalized binderLevel outerResolve currentDepth = \case
        B () ->
            Right
                (CBound
                    (currentDepth - binderLevel - 1))
        F outerLocal ->
            outerResolve currentDepth outerLocal