diff options
Diffstat (limited to 'source/Felix/Checking/Kernel/Derivation.hs')
| -rw-r--r-- | source/Felix/Checking/Kernel/Derivation.hs | 1264 |
1 files changed, 1264 insertions, 0 deletions
diff --git a/source/Felix/Checking/Kernel/Derivation.hs b/source/Felix/Checking/Kernel/Derivation.hs new file mode 100644 index 0000000..e83b376 --- /dev/null +++ b/source/Felix/Checking/Kernel/Derivation.hs @@ -0,0 +1,1264 @@ +{-# 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 |