{-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE NoImplicitPrelude #-} -- | Private in-memory proof trees and independent kernel replay. module Felix.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 Felix.Checking.Core import Felix.Checking.Foundation import Felix.Checking.Kernel.Semantics qualified as Semantics import Felix.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