path: root/source/Checking/Kernel/Derivation.hs

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

-- | Private in-memory proof trees and independent kernel replay.
module Checking.Kernel.Derivation
    ( ImportIx
    , importIx
    , importIxValue
    , HypothesisIx
    , hypothesisIx
    , DerivationImportJudgment
    , derivationImportJudgment
    , derivationImportStatement
    , KernelDerivation
    , mapKernelDerivationGlobals
    , importedFactDerivation
    , localHypothesisDerivation
    , foundationFactDerivation
    , implicationEliminationDerivation
    , forallEliminationDerivation
    , falsumEliminationDerivation
    , implicationIntroductionDerivation
    , forallIntroductionDerivation
    , ConversionPlan
    , conversionPlan
    , conversionPlanBudget
    , ConversionPlanError(..)
    , convertJudgmentDerivation
    , equalityReflexivityDerivation
    , scopedEqualityReflexivityDerivation
    , equalityCongruenceApplicationDerivation
    , equalityCongruenceLambdaDerivation
    , equalityModusPonensDerivation
    , setLfpBoundDerivation
    , setLfpLeastDerivation
    , setLfpFixedDerivation
    , setLfpInductDerivation
    , weakenDerivationHypotheses
    , KernelReplayLimits
    , kernelReplayLimits
    , defaultKernelReplayLimits
    , KernelReplayLimitError(..)
    , ReplayedKernelDerivation
    , replayKernelDerivation
    , replayedKernelTarget
    , replayedKernelImportUses
    , replayedKernelFoundationUses
    , replayedKernelRuleUses
    , replayedKernelNodeCount
    , replayedKernelMaximumDepth
    , DerivationImportError(..)
    , KernelReplayError(..)
    ) where

import Base
import Checking.Core
import Checking.Foundation
import Checking.Kernel.Semantics qualified as Semantics
import Checking.Kernel.SetLfp qualified as SetLfp

import Control.Monad (unless)
import Data.Bifunctor (first)
import Data.Set qualified as Set
import Data.Vector (Vector)
import Data.Vector qualified as Vector
import Numeric.Natural (Natural)


newtype ImportIx = ImportIx Natural
    deriving stock (Show, Eq, Ord)

importIx :: Natural -> ImportIx
importIx = ImportIx

importIxValue :: ImportIx -> Natural
importIxValue (ImportIx index) =
    index

newtype HypothesisIx = HypothesisIx Natural
    deriving stock (Show, Eq, Ord)

hypothesisIx :: Natural -> HypothesisIx
hypothesisIx = HypothesisIx

newtype DerivationImportJudgment global =
    DerivationImportJudgment
        (FrozenCheckedCore global)
    deriving stock (Eq)

data DerivationImportError =
    DerivationImportIsNotProposition !CoreType
    deriving stock (Show, Eq)

derivationImportJudgment
    :: FrozenCheckedCore global
    -> Either
        DerivationImportError
        (DerivationImportJudgment global)
derivationImportJudgment statement
    | frozenCoreType statement == TyProp =
        Right (DerivationImportJudgment statement)
    | otherwise =
        Left
            (DerivationImportIsNotProposition
                (frozenCoreType statement))

derivationImportStatement
    :: DerivationImportJudgment global
    -> FrozenCheckedCore global
derivationImportStatement
        (DerivationImportJudgment statement) =
    statement

data KernelDerivation global
    = UseImportedFact !ImportIx
    | UseLocalHypothesis !HypothesisIx
    | UseFoundationFact !FoundationAxiomTag
    | ImplicationElimination
        !(KernelDerivation global)
        !(KernelDerivation global)
    | ForallElimination
        !(KernelDerivation global)
        !(ScopedCheckedCore global)
    | FalsumElimination
        !(KernelDerivation global)
        !(ScopedCheckedCore global)
    | ImplicationIntroduction
        !(ScopedCheckedCore global)
        !(KernelDerivation global)
    | ForallIntroduction
        !CoreType
        !(KernelDerivation global)
    | ConvertJudgment
        !(KernelDerivation global)
        !(ScopedCheckedCore global)
        !ConversionPlan
    | EqualityReflexivity
        !(ScopedCheckedCore global)
    | EqualityCongruenceApplication
        !(KernelDerivation global)
        !(KernelDerivation global)
    | EqualityCongruenceLambda
        !CoreType
        !(KernelDerivation global)
    | EqualityModusPonens
        !(KernelDerivation global)
        !(KernelDerivation global)
    | ApplySetLfpBound
        !(ScopedCheckedCore global)
        !(ScopedCheckedCore global)
    | ApplySetLfpLeast
        !(ScopedCheckedCore global)
        !(ScopedCheckedCore global)
        !(ScopedCheckedCore global)
        !(KernelDerivation global)
        !(KernelDerivation global)
    | ApplySetLfpFixed
        !(ScopedCheckedCore global)
        !(ScopedCheckedCore global)
        !(KernelDerivation global)
    | ApplySetLfpInduct
        !(ScopedCheckedCore global)
        !(ScopedCheckedCore global)
        !(ScopedCheckedCore global)
        !(ScopedCheckedCore global)
        !(KernelDerivation global)
        !(KernelDerivation global)
        !(KernelDerivation global)
    deriving stock (Eq)

mapKernelDerivationGlobals
    :: (left -> right)
    -> KernelDerivation left
    -> KernelDerivation right
mapKernelDerivationGlobals transform = go
  where
    scoped = mapScopedGlobals transform
    go = \case
        UseImportedFact index ->
            UseImportedFact index
        UseLocalHypothesis index ->
            UseLocalHypothesis index
        UseFoundationFact tag ->
            UseFoundationFact tag
        ImplicationElimination premise implication ->
            ImplicationElimination (go premise) (go implication)
        ForallElimination proof argument ->
            ForallElimination (go proof) (scoped argument)
        FalsumElimination proof target ->
            FalsumElimination (go proof) (scoped target)
        ImplicationIntroduction premise proof ->
            ImplicationIntroduction (scoped premise) (go proof)
        ForallIntroduction binderType proof ->
            ForallIntroduction binderType (go proof)
        ConvertJudgment proof target plan ->
            ConvertJudgment (go proof) (scoped target) plan
        EqualityReflexivity term ->
            EqualityReflexivity (scoped term)
        EqualityCongruenceApplication function argument ->
            EqualityCongruenceApplication (go function) (go argument)
        EqualityCongruenceLambda binderType proof ->
            EqualityCongruenceLambda binderType (go proof)
        EqualityModusPonens equality proof ->
            EqualityModusPonens (go equality) (go proof)
        ApplySetLfpBound domain operator ->
            ApplySetLfpBound (scoped domain) (scoped operator)
        ApplySetLfpLeast domain operator candidate bounded closed ->
            ApplySetLfpLeast
                (scoped domain)
                (scoped operator)
                (scoped candidate)
                (go bounded)
                (go closed)
        ApplySetLfpFixed domain operator monotone ->
            ApplySetLfpFixed
                (scoped domain)
                (scoped operator)
                (go monotone)
        ApplySetLfpInduct domain operator predicate element
                monotone member closed ->
            ApplySetLfpInduct
                (scoped domain)
                (scoped operator)
                (scoped predicate)
                (scoped element)
                (go monotone)
                (go member)
                (go closed)

importedFactDerivation
    :: ImportIx
    -> KernelDerivation global
importedFactDerivation =
    UseImportedFact

localHypothesisDerivation
    :: HypothesisIx
    -> KernelDerivation global
localHypothesisDerivation =
    UseLocalHypothesis

foundationFactDerivation
    :: FoundationAxiomTag
    -> KernelDerivation global
foundationFactDerivation =
    UseFoundationFact

implicationEliminationDerivation
    :: KernelDerivation global
    -> KernelDerivation global
    -> KernelDerivation global
implicationEliminationDerivation =
    ImplicationElimination

forallEliminationDerivation
    :: KernelDerivation global
    -> ScopedCheckedCore global
    -> KernelDerivation global
forallEliminationDerivation =
    ForallElimination

falsumEliminationDerivation
    :: KernelDerivation global
    -> ScopedCheckedCore global
    -> KernelDerivation global
falsumEliminationDerivation =
    FalsumElimination

implicationIntroductionDerivation
    :: ScopedCheckedCore global
    -> KernelDerivation global
    -> KernelDerivation global
implicationIntroductionDerivation =
    ImplicationIntroduction

forallIntroductionDerivation
    :: CoreType
    -> KernelDerivation global
    -> KernelDerivation global
forallIntroductionDerivation =
    ForallIntroduction

newtype ConversionPlan = ConversionPlan Natural
    deriving stock (Show, Eq, Ord)

data ConversionPlanError =
    ConversionPlanExceedsLimit !Natural
    deriving stock (Show, Eq)

conversionPlanLimit :: Natural
conversionPlanLimit =
    100000

conversionPlan
    :: Natural
    -> Either ConversionPlanError ConversionPlan
conversionPlan budget
    | budget <= conversionPlanLimit =
        Right (ConversionPlan budget)
    | otherwise =
        Left (ConversionPlanExceedsLimit budget)

conversionPlanBudget :: ConversionPlan -> Natural
conversionPlanBudget (ConversionPlan budget) =
    budget

convertJudgmentDerivation
    :: KernelDerivation global
    -> ScopedCheckedCore global
    -> ConversionPlan
    -> KernelDerivation global
convertJudgmentDerivation =
    ConvertJudgment

equalityReflexivityDerivation
    :: FrozenCheckedCore global
    -> KernelDerivation global
equalityReflexivityDerivation =
    EqualityReflexivity . embedClosedCore []

scopedEqualityReflexivityDerivation
    :: ScopedCheckedCore global
    -> KernelDerivation global
scopedEqualityReflexivityDerivation =
    EqualityReflexivity

equalityCongruenceApplicationDerivation
    :: KernelDerivation global
    -> KernelDerivation global
    -> KernelDerivation global
equalityCongruenceApplicationDerivation =
    EqualityCongruenceApplication

equalityCongruenceLambdaDerivation
    :: CoreType
    -> KernelDerivation global
    -> KernelDerivation global
equalityCongruenceLambdaDerivation =
    EqualityCongruenceLambda

equalityModusPonensDerivation
    :: KernelDerivation global
    -> KernelDerivation global
    -> KernelDerivation global
equalityModusPonensDerivation =
    EqualityModusPonens

setLfpBoundDerivation
    :: ScopedCheckedCore global
    -> ScopedCheckedCore global
    -> KernelDerivation global
setLfpBoundDerivation =
    ApplySetLfpBound

setLfpLeastDerivation
    :: ScopedCheckedCore global
    -> ScopedCheckedCore global
    -> ScopedCheckedCore global
    -> KernelDerivation global
    -> KernelDerivation global
    -> KernelDerivation global
setLfpLeastDerivation =
    ApplySetLfpLeast

setLfpFixedDerivation
    :: ScopedCheckedCore global
    -> ScopedCheckedCore global
    -> KernelDerivation global
    -> KernelDerivation global
setLfpFixedDerivation =
    ApplySetLfpFixed

setLfpInductDerivation
    :: ScopedCheckedCore global
    -> ScopedCheckedCore global
    -> ScopedCheckedCore global
    -> ScopedCheckedCore global
    -> KernelDerivation global
    -> KernelDerivation global
    -> KernelDerivation global
    -> KernelDerivation global
setLfpInductDerivation =
    ApplySetLfpInduct

-- | Add hypotheses outside a derivation while preserving hypotheses introduced
-- by implication nodes inside it.
weakenDerivationHypotheses
    :: Natural
    -> KernelDerivation global
    -> KernelDerivation global
weakenDerivationHypotheses amount =
    shift 0
  where
    shift cutoff = \case
        UseImportedFact index ->
            UseImportedFact index
        UseLocalHypothesis (HypothesisIx index) ->
            UseLocalHypothesis
                (HypothesisIx
                    (if index >= cutoff
                        then index + amount
                        else index))
        UseFoundationFact tag ->
            UseFoundationFact tag
        ImplicationElimination implication premise ->
            ImplicationElimination
                (shift cutoff implication)
                (shift cutoff premise)
        ForallElimination quantified argument ->
            ForallElimination
                (shift cutoff quantified)
                argument
        FalsumElimination falsum target ->
            FalsumElimination
                (shift cutoff falsum)
                target
        ImplicationIntroduction premise body ->
            ImplicationIntroduction
                premise
                (shift (cutoff + 1) body)
        ForallIntroduction binderType body ->
            ForallIntroduction
                binderType
                (shift cutoff body)
        ConvertJudgment source target plan ->
            ConvertJudgment
                (shift cutoff source)
                target
                plan
        EqualityReflexivity operand ->
            EqualityReflexivity operand
        EqualityCongruenceApplication function argument ->
            EqualityCongruenceApplication
                (shift cutoff function)
                (shift cutoff argument)
        EqualityCongruenceLambda binderType body ->
            EqualityCongruenceLambda
                binderType
                (shift cutoff body)
        EqualityModusPonens equality premise ->
            EqualityModusPonens
                (shift cutoff equality)
                (shift cutoff premise)
        ApplySetLfpBound domain operator ->
            ApplySetLfpBound domain operator
        ApplySetLfpLeast
                domain operator candidate
                closed bounded ->
            ApplySetLfpLeast
                domain
                operator
                candidate
                (shift cutoff closed)
                (shift cutoff bounded)
        ApplySetLfpFixed domain operator monotone ->
            ApplySetLfpFixed
                domain
                operator
                (shift cutoff monotone)
        ApplySetLfpInduct
                domain operator predicate element
                monotone member closure ->
            ApplySetLfpInduct
                domain
                operator
                predicate
                element
                (shift cutoff monotone)
                (shift cutoff member)
                (shift cutoff closure)

data KernelReplayLimits = KernelReplayLimits
    !Natural
    !Natural
    deriving stock (Show, Eq)

data KernelReplayLimitError
    = KernelReplayNodeLimitIsZero
    | KernelReplayNodeLimitTooLarge !Natural
    | KernelReplayDepthLimitTooLarge !Natural
    deriving stock (Show, Eq)

maximumKernelReplayNodes :: Natural
maximumKernelReplayNodes =
    1000000

maximumKernelReplayDepth :: Natural
maximumKernelReplayDepth =
    4096

kernelReplayLimits
    :: Natural
    -> Natural
    -> Either KernelReplayLimitError KernelReplayLimits
kernelReplayLimits nodeLimit depthLimit
    | nodeLimit == 0 =
        Left KernelReplayNodeLimitIsZero
    | nodeLimit > maximumKernelReplayNodes =
        Left (KernelReplayNodeLimitTooLarge nodeLimit)
    | depthLimit > maximumKernelReplayDepth =
        Left (KernelReplayDepthLimitTooLarge depthLimit)
    | otherwise =
        Right
            (KernelReplayLimits
                nodeLimit
                depthLimit)

defaultKernelReplayLimits :: KernelReplayLimits
defaultKernelReplayLimits =
    KernelReplayLimits
        200000
        2048

data ReplayedKernelDerivation global =
    ReplayedKernelDerivation
        !(FrozenCheckedCore global)
        !(Set ImportIx)
        !(Set FoundationAxiomTag)
        !(Set KernelRuleTag)
        !Natural
        !Natural
    deriving stock (Eq)

replayedKernelTarget
    :: ReplayedKernelDerivation global
    -> FrozenCheckedCore global
replayedKernelTarget
        (ReplayedKernelDerivation
            target
            _importUses
            _foundationUses
            _ruleUses
            _nodeCount
            _maximumDepth) =
    target

replayedKernelImportUses
    :: ReplayedKernelDerivation global
    -> Set ImportIx
replayedKernelImportUses
        (ReplayedKernelDerivation
            _target
            importUses
            _foundationUses
            _ruleUses
            _nodeCount
            _maximumDepth) =
    importUses

replayedKernelFoundationUses
    :: ReplayedKernelDerivation global
    -> Set FoundationAxiomTag
replayedKernelFoundationUses
        (ReplayedKernelDerivation
            _target
            _importUses
            foundationUses
            _ruleUses
            _nodeCount
            _maximumDepth) =
    foundationUses

replayedKernelRuleUses
    :: ReplayedKernelDerivation global
    -> Set KernelRuleTag
replayedKernelRuleUses
        (ReplayedKernelDerivation
            _target
            _importUses
            _foundationUses
            ruleUses
            _nodeCount
            _maximumDepth) =
    ruleUses

replayedKernelNodeCount
    :: ReplayedKernelDerivation global
    -> Natural
replayedKernelNodeCount
        (ReplayedKernelDerivation
            _target
            _importUses
            _foundationUses
            _ruleUses
            nodeCount
            _maximumDepth) =
    nodeCount

replayedKernelMaximumDepth
    :: ReplayedKernelDerivation global
    -> Natural
replayedKernelMaximumDepth
        (ReplayedKernelDerivation
            _target
            _importUses
            _foundationUses
            _ruleUses
            _nodeCount
            maximumDepth) =
    maximumDepth

data ReplayStep global = ReplayStep
    !(ScopedCheckedCore global)
    !(Set ImportIx)
    !(Set FoundationAxiomTag)
    !(Set KernelRuleTag)
    !Natural
    !Natural

data KernelReplayError
    = KernelReplaySemanticsError
        !Semantics.KernelSemanticsError
    | KernelReplaySetLfpRuleError
        !SetLfp.SetLfpRuleError
    | KernelReplayImportOutOfBounds !ImportIx
    | KernelReplayHypothesisOutOfBounds !HypothesisIx
    | KernelReplayStoredContextMismatch
        ![CoreType]
        ![CoreType]
    | KernelReplayStoredTermIllTyped !CoreCheckError
    | KernelReplayStoredTypeMismatch
        !CoreType
        !CoreType
    | KernelReplayWeakeningError !CoreCheckError
    | KernelReplayNodeLimitExceeded !Natural
    | KernelReplayDepthLimitExceeded !Natural
    | KernelReplayRootRemainedOpen
    | KernelReplayTargetMismatch
    deriving stock (Show, Eq)

replayKernelDerivation
    :: Eq global
    => CheckedFoundation
    -> KernelReplayLimits
    -> (global -> Maybe CoreType)
    -> Vector (DerivationImportJudgment global)
    -> FrozenCheckedCore global
    -> KernelDerivation global
    -> Either
        KernelReplayError
        (ReplayedKernelDerivation global)
replayKernelDerivation
        checkedFoundationValue
        limits
        globalType
        imports
        expectedTarget
        derivation =
    checkedFoundationValue `seq` do
        expectedTarget' <-
            recheckClosed expectedTarget
        ReplayStep
            synthesized
            importUses
            foundationUses
            ruleUses
            nodeCount
            maximumDepth <-
                replay [] [] 0 derivation
        closed <-
            maybe
                (Left KernelReplayRootRemainedOpen)
                Right
                (closeScopedCore synthesized)
        unless
            (closed == expectedTarget')
            (Left KernelReplayTargetMismatch)
        pure
            (ReplayedKernelDerivation
                closed
                importUses
                foundationUses
                ruleUses
                nodeCount
                maximumDepth)
  where
    replay context hypotheses depth derivationNode
        | depth > replayDepthLimit =
            Left
                (KernelReplayDepthLimitExceeded
                    replayDepthLimit)
        | otherwise = do
            step <-
                replayWithin
                    context
                    hypotheses
                    depth
                    derivationNode
            if stepNodeCount step > replayNodeLimit
                then
                    Left
                        (KernelReplayNodeLimitExceeded
                            replayNodeLimit)
                else
                    Right step

    replayWithin context hypotheses depth = \case
        UseImportedFact index -> do
            judgment <-
                lookupImport index
            statement <-
                recheckStored
                    context
                    (embedClosedCore context
                        (derivationImportStatement
                            judgment))
            pure
                (leaf
                    depth
                    statement
                    (Set.singleton index)
                    mempty)
        UseLocalHypothesis index -> do
            hypothesis <-
                lookupHypothesis index hypotheses
            checkedHypothesis <-
                recheckStored context hypothesis
            pure
                (leaf
                    depth
                    checkedHypothesis
                    mempty
                    mempty)
        UseFoundationFact tag -> do
            statement <-
                recheckStored
                    context
                    (embedClosedCore context
                        (mapFrozenGlobals
                            absurd
                            (foundationAxiomFrozen
                                checkedFoundationValue
                                tag)))
            pure
                (leaf
                    depth
                    statement
                    mempty
                    (Set.singleton tag))
        ImplicationElimination implication premise -> do
            implicationStep <-
                replay context hypotheses (depth + 1) implication
            premiseStep <-
                replay context hypotheses (depth + 1) premise
            combine2 depth
                (Semantics.implicationElimination
                    globalType
                    (stepValue implicationStep)
                    (stepValue premiseStep))
                implicationStep
                premiseStep
        ForallElimination quantified argument -> do
            argument' <-
                recheckStored context argument
            quantifiedStep <-
                replay context hypotheses (depth + 1) quantified
            combine1 depth
                (Semantics.forallElimination
                    globalType
                    (stepValue quantifiedStep)
                    argument')
                quantifiedStep
        FalsumElimination falsum target -> do
            target' <-
                recheckStored context target
            falsumStep <-
                replay context hypotheses (depth + 1) falsum
            combine1 depth
                (Semantics.falsumElimination
                    globalType
                    (stepValue falsumStep)
                    target')
                falsumStep
        ImplicationIntroduction premise body -> do
            premise' <-
                recheckStored context premise
            bodyStep <-
                replay
                    context
                    (premise' : hypotheses)
                    (depth + 1)
                    body
            combine1 depth
                (Semantics.implicationIntroduction
                    globalType
                    premise'
                    (stepValue bodyStep))
                bodyStep
        ForallIntroduction binderType body -> do
            weakenedHypotheses <-
                traverse
                    (first KernelReplayWeakeningError
                        . weakenScopedCore
                            globalType
                            binderType)
                    hypotheses
            bodyStep <-
                replay
                    (binderType : context)
                    weakenedHypotheses
                    (depth + 1)
                    body
            combine1 depth
                (Semantics.forallIntroduction
                    globalType
                    binderType
                    (stepValue bodyStep))
                bodyStep
        ConvertJudgment source target plan -> do
            target' <-
                recheckStored context target
            sourceStep <-
                replay
                    context
                    hypotheses
                    (depth + 1)
                    source
            combine1 depth
                (Semantics.convertJudgment
                    globalType
                    (conversionPlanBudget plan)
                    (stepValue sourceStep)
                    target')
                sourceStep
        EqualityReflexivity operand -> do
            operand' <-
                recheckStored context operand
            value <-
                first KernelReplaySemanticsError
                    (Semantics.equalityReflexivity
                        globalType
                        operand')
            pure (leaf depth value mempty mempty)
        EqualityCongruenceApplication
                functionEquality
                argumentEquality -> do
            functionStep <-
                replay
                    context
                    hypotheses
                    (depth + 1)
                    functionEquality
            argumentStep <-
                replay
                    context
                    hypotheses
                    (depth + 1)
                    argumentEquality
            combine2 depth
                (Semantics.equalityCongruenceApplication
                    globalType
                    (stepValue functionStep)
                    (stepValue argumentStep))
                functionStep
                argumentStep
        EqualityCongruenceLambda binderType bodyEquality -> do
            weakenedHypotheses <-
                traverse
                    (first KernelReplayWeakeningError
                        . weakenScopedCore
                            globalType
                            binderType)
                    hypotheses
            bodyStep <-
                replay
                    (binderType : context)
                    weakenedHypotheses
                    (depth + 1)
                    bodyEquality
            combine1 depth
                (Semantics.equalityCongruenceLambda
                    globalType
                    binderType
                    (stepValue bodyStep))
                bodyStep
        EqualityModusPonens equality premise -> do
            equalityStep <-
                replay context hypotheses (depth + 1) equality
            premiseStep <-
                replay context hypotheses (depth + 1) premise
            combine2 depth
                (Semantics.equalityModusPonens
                    globalType
                    (stepValue equalityStep)
                    (stepValue premiseStep))
                equalityStep
                premiseStep
        ApplySetLfpBound domain operator -> do
            domain' <-
                recheckStored context domain
            operator' <-
                recheckStored context operator
            value <-
                first KernelReplaySetLfpRuleError
                    (SetLfp.setLfpBound
                        checkedFoundationValue
                        globalType
                        domain'
                        operator')
            pure
                (ruleLeaf
                    depth
                    SetLfpBound
                    value)
        ApplySetLfpLeast
                domain
                operator
                candidate
                closedPremise
                boundedPremise -> do
            domain' <-
                recheckStored context domain
            operator' <-
                recheckStored context operator
            candidate' <-
                recheckStored context candidate
            closedStep <-
                replay
                    context
                    hypotheses
                    (depth + 1)
                    closedPremise
            boundedStep <-
                replay
                    context
                    hypotheses
                    (depth + 1)
                    boundedPremise
            combineRule depth SetLfpLeast
                (SetLfp.setLfpLeast
                    checkedFoundationValue
                    globalType
                    domain'
                    operator'
                    candidate'
                    (stepValue closedStep)
                    (stepValue boundedStep))
                [closedStep, boundedStep]
        ApplySetLfpFixed domain operator monotonePremise -> do
            domain' <-
                recheckStored context domain
            operator' <-
                recheckStored context operator
            monotoneStep <-
                replay
                    context
                    hypotheses
                    (depth + 1)
                    monotonePremise
            combineRule depth SetLfpFixed
                (SetLfp.setLfpFixed
                    checkedFoundationValue
                    globalType
                    domain'
                    operator'
                    (stepValue monotoneStep))
                [monotoneStep]
        ApplySetLfpInduct
                domain
                operator
                predicate
                element
                monotonePremise
                memberPremise
                closurePremise -> do
            domain' <-
                recheckStored context domain
            operator' <-
                recheckStored context operator
            predicate' <-
                recheckStored context predicate
            element' <-
                recheckStored context element
            monotoneStep <-
                replay
                    context
                    hypotheses
                    (depth + 1)
                    monotonePremise
            memberStep <-
                replay
                    context
                    hypotheses
                    (depth + 1)
                    memberPremise
            closureStep <-
                replay
                    context
                    hypotheses
                    (depth + 1)
                    closurePremise
            combineRule depth SetLfpInduct
                (SetLfp.setLfpInduct
                    checkedFoundationValue
                    globalType
                    domain'
                    operator'
                    predicate'
                    element'
                    (stepValue monotoneStep)
                    (stepValue memberStep)
                    (stepValue closureStep))
                [ monotoneStep
                , memberStep
                , closureStep
                ]

    lookupImport index@(ImportIx naturalIndex)
        | naturalIndex
            > fromIntegral (maxBound :: Int) =
                Left
                    (KernelReplayImportOutOfBounds
                        index)
        | otherwise =
            maybe
                (Left
                    (KernelReplayImportOutOfBounds
                        index))
                Right
                (imports
                    Vector.!?
                        (fromIntegral naturalIndex))

    lookupHypothesis
            index@(HypothesisIx naturalIndex)
            hypotheses =
        maybe
            (Left
                (KernelReplayHypothesisOutOfBounds
                    index))
            Right
            (atNatural naturalIndex hypotheses)

    requireContext expected value
        | scopedCoreContext value == expected =
            Right ()
        | otherwise =
            Left
                (KernelReplayStoredContextMismatch
                    expected
                    (scopedCoreContext value))

    recheckStored expectedContext stored = do
        requireContext expectedContext stored
        checked <-
            first KernelReplayStoredTermIllTyped
                (checkScopedCanonicalCore
                    globalType
                    expectedContext
                    (scopedCoreTerm stored))
        unless
            (scopedCoreType checked
                == scopedCoreType stored)
            (Left
                (KernelReplayStoredTypeMismatch
                    (scopedCoreType stored)
                    (scopedCoreType checked)))
        pure checked

    recheckClosed stored = do
        checked <-
            first KernelReplayStoredTermIllTyped
                (checkCanonicalCore
                    globalType
                    (frozenCoreTerm stored))
        unless
            (frozenCoreType checked
                == frozenCoreType stored)
            (Left
                (KernelReplayStoredTypeMismatch
                    (frozenCoreType stored)
                    (frozenCoreType checked)))
        pure checked

    replayNodeLimit =
        case limits of
            KernelReplayLimits nodeLimit _depthLimit ->
                nodeLimit

    replayDepthLimit =
        case limits of
            KernelReplayLimits _nodeLimit depthLimit ->
                depthLimit

leaf
    :: Natural
    -> ScopedCheckedCore global
    -> Set ImportIx
    -> Set FoundationAxiomTag
    -> ReplayStep global
leaf depth value importUses foundationUses =
    ReplayStep
        value
        importUses
        foundationUses
        mempty
        1
        depth

ruleLeaf
    :: Natural
    -> KernelRuleTag
    -> ScopedCheckedCore global
    -> ReplayStep global
ruleLeaf depth tag value =
    ReplayStep
        value
        mempty
        mempty
        (Set.singleton tag)
        1
        depth

stepValue :: ReplayStep global -> ScopedCheckedCore global
stepValue
        (ReplayStep
            value
            _importUses
            _foundationUses
            _ruleUses
            _nodeCount
            _maximumDepth) =
    value

combine1
    :: Natural
    -> Either
        Semantics.KernelSemanticsError
        (ScopedCheckedCore global)
    -> ReplayStep global
    -> Either KernelReplayError (ReplayStep global)
combine1 depth synthesized child = do
    value <-
        first KernelReplaySemanticsError synthesized
    pure
        (ReplayStep
            value
            (stepImportUses child)
            (stepFoundationUses child)
            (stepRuleUses child)
            (1 + stepNodeCount child)
            (max depth
                (stepMaximumDepth child)))

combine2
    :: Natural
    -> Either
        Semantics.KernelSemanticsError
        (ScopedCheckedCore global)
    -> ReplayStep global
    -> ReplayStep global
    -> Either KernelReplayError (ReplayStep global)
combine2 depth synthesized left right = do
    value <-
        first KernelReplaySemanticsError synthesized
    pure
        (ReplayStep
            value
            (stepImportUses left
                <> stepImportUses right)
            (stepFoundationUses left
                <> stepFoundationUses right)
            (stepRuleUses left
                <> stepRuleUses right)
            (1
                + stepNodeCount left
                + stepNodeCount right)
            (maximum
                [ depth
                , stepMaximumDepth left
                , stepMaximumDepth right
                ]))

combineRule
    :: Natural
    -> KernelRuleTag
    -> Either
        SetLfp.SetLfpRuleError
        (ScopedCheckedCore global)
    -> [ReplayStep global]
    -> Either KernelReplayError (ReplayStep global)
combineRule depth tag synthesized children = do
    value <-
        first KernelReplaySetLfpRuleError synthesized
    pure
        (ReplayStep
            value
            (foldMap stepImportUses children)
            (foldMap stepFoundationUses children)
            (Set.insert tag
                (foldMap stepRuleUses children))
            (1 + sum (stepNodeCount <$> children))
            (maximum
                (depth
                    : (stepMaximumDepth <$> children))))

stepImportUses
    :: ReplayStep global
    -> Set ImportIx
stepImportUses
        (ReplayStep
            _value
            importUses
            _foundationUses
            _ruleUses
            _nodeCount
            _maximumDepth) =
    importUses

stepFoundationUses
    :: ReplayStep global
    -> Set FoundationAxiomTag
stepFoundationUses
        (ReplayStep
            _value
            _importUses
            foundationUses
            _ruleUses
            _nodeCount
            _maximumDepth) =
    foundationUses

stepRuleUses
    :: ReplayStep global
    -> Set KernelRuleTag
stepRuleUses
        (ReplayStep
            _value
            _importUses
            _foundationUses
            ruleUses
            _nodeCount
            _maximumDepth) =
    ruleUses

stepNodeCount :: ReplayStep global -> Natural
stepNodeCount
        (ReplayStep
            _value
            _importUses
            _foundationUses
            _ruleUses
            nodeCount
            _maximumDepth) =
    nodeCount

stepMaximumDepth :: ReplayStep global -> Natural
stepMaximumDepth
        (ReplayStep
            _value
            _importUses
            _foundationUses
            _ruleUses
            _nodeCount
            maximumDepth) =
    maximumDepth

atNatural :: Natural -> [a] -> Maybe a
atNatural _index [] =
    Nothing
atNatural 0 (value : _rest) =
    Just value
atNatural index (_value : rest) =
    atNatural (index - 1) rest