diff options
| author | adelon <22380201+adelon@users.noreply.github.com> | 2026-07-28 20:18:16 +0200 |
|---|---|---|
| committer | adelon <22380201+adelon@users.noreply.github.com> | 2026-07-28 21:05:10 +0200 |
| commit | a03cd6977c4eecbb590f4c9df01bbe0569c37a42 (patch) | |
| tree | 685cb8fe06668e053e1b89a857b5f5748eee2c41 /source/Checking/Kernel | |
| parent | e788d5b3acf05f9e277c6af513324c5940054d80 (diff) | |
Remove obsolete kernel authorization projection
Diffstat (limited to 'source/Checking/Kernel')
| -rw-r--r-- | source/Checking/Kernel/Derivation.hs | 84 |
1 files changed, 0 insertions, 84 deletions
diff --git a/source/Checking/Kernel/Derivation.hs b/source/Checking/Kernel/Derivation.hs index f034683..d745104 100644 --- a/source/Checking/Kernel/Derivation.hs +++ b/source/Checking/Kernel/Derivation.hs @@ -47,15 +47,8 @@ module Checking.Kernel.Derivation , replayedKernelRuleUses , replayedKernelNodeCount , replayedKernelMaximumDepth - , CheckedKernelDerivation - , authorizeImportFreeDerivation - , checkedKernelTarget - , checkedKernelNodeCount - , checkedKernelFoundationUses - , checkedKernelRuleUses , DerivationImportError(..) , KernelReplayError(..) - , DerivationAuthorizationError(..) ) where import Base @@ -545,58 +538,6 @@ replayedKernelMaximumDepth maximumDepth) = maximumDepth -data CheckedKernelDerivation global = - CheckedKernelDerivation - !(FrozenCheckedCore global) - !(Set FoundationAxiomTag) - !(Set KernelRuleTag) - !Natural - deriving stock (Eq) - -checkedKernelTarget - :: CheckedKernelDerivation global - -> FrozenCheckedCore global -checkedKernelTarget - (CheckedKernelDerivation - target - _foundationUses - _ruleUses - _nodeCount) = - target - -checkedKernelNodeCount - :: CheckedKernelDerivation global - -> Natural -checkedKernelNodeCount - (CheckedKernelDerivation - _target - _foundationUses - _ruleUses - nodeCount) = - nodeCount - -checkedKernelFoundationUses - :: CheckedKernelDerivation global - -> Set FoundationAxiomTag -checkedKernelFoundationUses - (CheckedKernelDerivation - _target - foundationUses - _ruleUses - _nodeCount) = - foundationUses - -checkedKernelRuleUses - :: CheckedKernelDerivation global - -> Set KernelRuleTag -checkedKernelRuleUses - (CheckedKernelDerivation - _target - _foundationUses - ruleUses - _nodeCount) = - ruleUses - data ReplayStep global = ReplayStep !(ScopedCheckedCore global) !(Set ImportIx) @@ -1080,31 +1021,6 @@ replayKernelDerivation KernelReplayLimits _nodeLimit depthLimit -> depthLimit -data DerivationAuthorizationError = - DerivationContainsImports !(Set ImportIx) - deriving stock (Show, Eq) - --- | Close the authorization boundary only for a replay whose used-import set --- is empty. Import-bearing replay is sealed by the transition inventory when --- its first production consumer lands. -authorizeImportFreeDerivation - :: ReplayedKernelDerivation global - -> Either - DerivationAuthorizationError - (CheckedKernelDerivation global) -authorizeImportFreeDerivation replayed - | Set.null (replayedKernelImportUses replayed) = - Right - (CheckedKernelDerivation - (replayedKernelTarget replayed) - (replayedKernelFoundationUses replayed) - (replayedKernelRuleUses replayed) - (replayedKernelNodeCount replayed)) - | otherwise = - Left - (DerivationContainsImports - (replayedKernelImportUses replayed)) - leaf :: Natural -> ScopedCheckedCore global |