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