diff options
Diffstat (limited to 'source/Checking/Kernel')
| -rw-r--r-- | source/Checking/Kernel/Derivation.hs | 1264 | ||||
| -rw-r--r-- | source/Checking/Kernel/Proof.hs | 1166 | ||||
| -rw-r--r-- | source/Checking/Kernel/Semantics.hs | 436 | ||||
| -rw-r--r-- | source/Checking/Kernel/SetLfp.hs | 762 |
4 files changed, 0 insertions, 3628 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 diff --git a/source/Checking/Kernel/Proof.hs b/source/Checking/Kernel/Proof.hs deleted file mode 100644 index 42324d1..0000000 --- a/source/Checking/Kernel/Proof.hs +++ /dev/null @@ -1,1166 +0,0 @@ -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE NoImplicitPrelude #-} - --- | Small proof-producing natural-deduction combinators. Every resulting tree --- is still replayed independently before it can authorize a fact. -module Checking.Kernel.Proof - ( ProofContext - , rootProofContext - , proofContextTypes - , scopedTerm - , BuiltProof - , builtProofStatement - , builtProofDerivation - , importedProof - , foundationProof - , hypothesisProof - , implicationEliminationProof - , implicationIntroductionProof - , forallEliminationProof - , forallIntroductionProof - , falsumEliminationProof - , equalityReflexivityProof - , equalityReverseProof - , equalityCongruenceApplicationProof - , equalityModusPonensProof - , conversionProof - , doubleNegationEliminationProof - , conjunctionTerm - , conjunctionIntroductionProof - , conjunctionLeftProof - , conjunctionRightProof - , disjunctionTerm - , disjunctionLeftProof - , disjunctionRightProof - , disjunctionEliminationProof - , existentialTerm - , existentialIntroductionProof - , existentialEliminationProof - , setLfpBoundProof - , setLfpFixedProof - , setLfpInductProof - , KernelProofBuildError(..) - ) where - -import Base -import Checking.Core -import Checking.Foundation -import Checking.Kernel.Derivation -import Checking.Kernel.Semantics qualified as Semantics -import Checking.Kernel.SetLfp qualified as SetLfp - -import Control.Monad (unless) -import Data.Bifunctor (first) -import Data.List qualified as List -import Data.Text qualified as Text - - -data ProofContext global = ProofContext - !CheckedFoundation - !(global -> Maybe CoreType) - ![CoreType] - ![ScopedCheckedCore global] - -rootProofContext - :: CheckedFoundation - -> (global -> Maybe CoreType) - -> ProofContext global -rootProofContext foundation globalType = - ProofContext foundation globalType [] [] - -proofContextTypes - :: ProofContext global - -> [CoreType] -proofContextTypes - (ProofContext - _foundation - _globalType - context - _hypotheses) = - context - -data BuiltProof global = BuiltProof - !(ScopedCheckedCore global) - !(KernelDerivation global) - -builtProofStatement - :: BuiltProof global - -> ScopedCheckedCore global -builtProofStatement - (BuiltProof statement _derivation) = - statement - -builtProofDerivation - :: BuiltProof global - -> KernelDerivation global -builtProofDerivation - (BuiltProof _statement derivation) = - derivation - -data KernelProofBuildError - = ProofTermIllTyped !CoreCheckError - | ProofSemanticsFailed - !Semantics.KernelSemanticsError - | ProofFoundationArgumentMismatch - !FoundationAxiomTag - | ProofHypothesisNotFound - | ProofExpectedEquality - | ProofExpectedUnaryBinder - | ProofSetLfpRuleFailed !Text - | ProofConversionPlanFailed !Text - deriving stock (Show, Eq) - -scopedTerm - :: ProofContext global - -> CanonicalTerm global - -> Either - KernelProofBuildError - (ScopedCheckedCore global) -scopedTerm - (ProofContext - _foundation - globalType - context - _hypotheses) = - first ProofTermIllTyped - . checkScopedCanonicalCore - globalType - context - -importedProof - :: ProofContext global - -> ImportIx - -> FrozenCheckedCore global - -> Either - KernelProofBuildError - (BuiltProof global) -importedProof context index statement = - pure - (BuiltProof - (embedClosedCore - (proofContextTypes context) - statement) - (importedFactDerivation index)) - -foundationProof - :: ProofContext global - -> FoundationAxiomTag - -> Either - KernelProofBuildError - (BuiltProof global) -foundationProof - context@(ProofContext - foundation - _globalType - _types - _hypotheses) - tag = - pure - (BuiltProof - (embedClosedCore - (proofContextTypes context) - (mapFrozenGlobals - absurd - (foundationAxiomFrozen - foundation - tag))) - (foundationFactDerivation tag)) - -hypothesisProof - :: Eq global - => ProofContext global - -> ScopedCheckedCore global - -> Either - KernelProofBuildError - (BuiltProof global) -hypothesisProof - (ProofContext - _foundation - _globalType - _context - hypotheses) - statement = - case List.findIndex (== statement) hypotheses of - Nothing -> - Left ProofHypothesisNotFound - Just index -> - pure - (BuiltProof - statement - (localHypothesisDerivation - (hypothesisIx - (fromIntegral index)))) - -implicationEliminationProof - :: Eq global - => ProofContext global - -> BuiltProof global - -> BuiltProof global - -> Either - KernelProofBuildError - (BuiltProof global) -implicationEliminationProof - (ProofContext - _foundation - globalType - _context - _hypotheses) - implication - premise = do - conclusion <- - first ProofSemanticsFailed - (Semantics.implicationElimination - globalType - (builtProofStatement implication) - (builtProofStatement premise)) - pure - (BuiltProof - conclusion - (implicationEliminationDerivation - (builtProofDerivation implication) - (builtProofDerivation premise))) - -implicationIntroductionProof - :: ProofContext global - -> ScopedCheckedCore global - -> ( ProofContext global - -> BuiltProof global - -> Either - KernelProofBuildError - (BuiltProof global) - ) - -> Either - KernelProofBuildError - (BuiltProof global) -implicationIntroductionProof - (ProofContext - foundation - globalType - types - hypotheses) - premise - buildBody = do - let extended = - ProofContext - foundation - globalType - types - (premise : hypotheses) - premiseProof = - BuiltProof - premise - (localHypothesisDerivation - (hypothesisIx 0)) - body <- - buildBody extended premiseProof - conclusion <- - first ProofSemanticsFailed - (Semantics.implicationIntroduction - globalType - premise - (builtProofStatement body)) - pure - (BuiltProof - conclusion - (implicationIntroductionDerivation - premise - (builtProofDerivation body))) - -forallEliminationProof - :: ProofContext global - -> BuiltProof global - -> ScopedCheckedCore global - -> Either - KernelProofBuildError - (BuiltProof global) -forallEliminationProof - (ProofContext - _foundation - globalType - _types - _hypotheses) - quantified - argument = do - conclusion <- - first ProofSemanticsFailed - (Semantics.forallElimination - globalType - (builtProofStatement quantified) - argument) - pure - (BuiltProof - conclusion - (forallEliminationDerivation - (builtProofDerivation quantified) - argument)) - -forallIntroductionProof - :: ProofContext global - -> CoreType - -> ( ProofContext global - -> ScopedCheckedCore global - -> Either - KernelProofBuildError - (BuiltProof global) - ) - -> Either - KernelProofBuildError - (BuiltProof global) -forallIntroductionProof - (ProofContext - foundation - globalType - types - hypotheses) - binderType - buildBody = do - weakenedHypotheses <- - traverse - (first ProofTermIllTyped - . weakenScopedCore - globalType - binderType) - hypotheses - let extended = - ProofContext - foundation - globalType - (binderType : types) - weakenedHypotheses - variable <- - scopedTerm extended (CBound 0) - body <- - buildBody extended variable - conclusion <- - first ProofSemanticsFailed - (Semantics.forallIntroduction - globalType - binderType - (builtProofStatement body)) - pure - (BuiltProof - conclusion - (forallIntroductionDerivation - binderType - (builtProofDerivation body))) - -falsumEliminationProof - :: ProofContext global - -> BuiltProof global - -> ScopedCheckedCore global - -> Either - KernelProofBuildError - (BuiltProof global) -falsumEliminationProof - (ProofContext - _foundation - globalType - _types - _hypotheses) - falsum - target = do - conclusion <- - first ProofSemanticsFailed - (Semantics.falsumElimination - globalType - (builtProofStatement falsum) - target) - pure - (BuiltProof - conclusion - (falsumEliminationDerivation - (builtProofDerivation falsum) - target)) - -equalityReflexivityProof - :: ProofContext global - -> ScopedCheckedCore global - -> Either - KernelProofBuildError - (BuiltProof global) -equalityReflexivityProof - (ProofContext - _foundation - globalType - _types - _hypotheses) - operand = do - equality <- - first ProofSemanticsFailed - (Semantics.equalityReflexivity - globalType - operand) - pure - (BuiltProof - equality - (scopedEqualityReflexivityDerivation - operand)) - -equalityCongruenceApplicationProof - :: ProofContext global - -> BuiltProof global - -> BuiltProof global - -> Either - KernelProofBuildError - (BuiltProof global) -equalityCongruenceApplicationProof - (ProofContext - _foundation - globalType - _types - _hypotheses) - functionEquality - argumentEquality = do - equality <- - first ProofSemanticsFailed - (Semantics.equalityCongruenceApplication - globalType - (builtProofStatement functionEquality) - (builtProofStatement argumentEquality)) - pure - (BuiltProof - equality - (equalityCongruenceApplicationDerivation - (builtProofDerivation - functionEquality) - (builtProofDerivation - argumentEquality))) - -equalityModusPonensProof - :: Eq global - => ProofContext global - -> BuiltProof global - -> BuiltProof global - -> Either - KernelProofBuildError - (BuiltProof global) -equalityModusPonensProof - (ProofContext - _foundation - globalType - _types - _hypotheses) - equality - premise = do - conclusion <- - first ProofSemanticsFailed - (Semantics.equalityModusPonens - globalType - (builtProofStatement equality) - (builtProofStatement premise)) - pure - (BuiltProof - conclusion - (equalityModusPonensDerivation - (builtProofDerivation equality) - (builtProofDerivation premise))) - -conversionProof - :: Eq global - => ProofContext global - -> BuiltProof global - -> ScopedCheckedCore global - -> Either - KernelProofBuildError - (BuiltProof global) -conversionProof - (ProofContext - _foundation - globalType - _types - _hypotheses) - source - target = do - plan <- - first (ProofConversionPlanFailed . Text.pack . show) - (conversionPlan 100000) - result <- - first ProofSemanticsFailed - (Semantics.convertJudgment - globalType - (conversionPlanBudget plan) - (builtProofStatement source) - target) - pure - (BuiltProof - result - (convertJudgmentDerivation - (builtProofDerivation source) - target - plan)) - -equalityReverseProof - :: Eq global - => ProofContext global - -> BuiltProof global - -> Either - KernelProofBuildError - (BuiltProof global) -equalityReverseProof context equality = do - (operandType, left, right) <- - equalityParts - (builtProofStatement equality) - leftOperand <- - scopedTerm context left - weakenedLeft <- - first ProofTermIllTyped - (weakenScopedCore - (contextGlobalType context) - operandType - leftOperand) - function <- - scopedTerm context - (CLam operandType - (CEq - operandType - (CBound 0) - (scopedCoreTerm - weakenedLeft))) - functionReflexivity <- - equalityReflexivityProof - context - function - appliedEquality <- - equalityCongruenceApplicationProof - context - functionReflexivity - equality - leftReflexivity <- - equalityReflexivityProof - context - leftOperand - appliedLeft <- - scopedTerm context - (CApp - (scopedCoreTerm function) - left) - appliedLeftReflexivity <- - conversionProof - context - leftReflexivity - appliedLeft - reversedApplication <- - equalityModusPonensProof - context - appliedEquality - appliedLeftReflexivity - expected <- - scopedTerm context - (CEq operandType right left) - conversionProof - context - reversedApplication - expected - -doubleNegationEliminationProof - :: Eq global - => ProofContext global - -> ScopedCheckedCore global - -> BuiltProof global - -> Either - KernelProofBuildError - (BuiltProof global) -doubleNegationEliminationProof - context - target - doubleNegation = do - axiom <- - foundationProof - context - DoubleNegationElim - instanceProof <- - forallEliminationProof - context - axiom - target - implicationEliminationProof - context - instanceProof - doubleNegation - -conjunctionTerm - :: CanonicalTerm global - -> CanonicalTerm global - -> CanonicalTerm global -conjunctionTerm left right = - CImp - (CImp left - (CImp right CFalsum)) - CFalsum - -conjunctionIntroductionProof - :: Eq global - => ProofContext global - -> BuiltProof global - -> BuiltProof global - -> Either - KernelProofBuildError - (BuiltProof global) -conjunctionIntroductionProof - context - left - right = do - let leftTerm = - scopedCoreTerm - (builtProofStatement left) - rightTerm = - scopedCoreTerm - (builtProofStatement right) - refuter <- - scopedTerm context - (CImp leftTerm - (CImp rightTerm CFalsum)) - implicationIntroductionProof - context - refuter - (\extended refuterProof -> do - firstApplication <- - implicationEliminationProof - extended - refuterProof - (weakenForHypothesis left) - implicationEliminationProof - extended - firstApplication - (weakenForHypothesis right)) - -conjunctionLeftProof - :: Eq global - => ProofContext global - -> CanonicalTerm global - -> CanonicalTerm global - -> BuiltProof global - -> Either - KernelProofBuildError - (BuiltProof global) -conjunctionLeftProof context left right conjunction = do - leftProposition <- - scopedTerm context left - notLeft <- - scopedTerm context - (CImp left CFalsum) - doubleNegation <- - implicationIntroductionProof - context - notLeft - (\withNotLeft _notLeftProof -> do - leftAtRefuter <- - scopedTerm withNotLeft left - refuterProof <- - implicationIntroductionProof - withNotLeft - leftAtRefuter - (\withLeft leftProof -> do - rightProposition <- - scopedTerm withLeft right - implicationIntroductionProof - withLeft - rightProposition - (\withBoth _rightProof -> do - notLeftCurrent <- - hypothesisProof - withBoth - notLeft - implicationEliminationProof - withBoth - notLeftCurrent - (weakenForHypothesis - leftProof))) - implicationEliminationProof - withNotLeft - (weakenForHypothesis conjunction) - refuterProof) - doubleNegationEliminationProof - context - leftProposition - doubleNegation - -conjunctionRightProof - :: Eq global - => ProofContext global - -> CanonicalTerm global - -> CanonicalTerm global - -> BuiltProof global - -> Either - KernelProofBuildError - (BuiltProof global) -conjunctionRightProof context left right conjunction = do - rightProposition <- - scopedTerm context right - notRight <- - scopedTerm context - (CImp right CFalsum) - doubleNegation <- - implicationIntroductionProof - context - notRight - (\withNotRight _notRightProof -> do - leftAtRefuter <- - scopedTerm withNotRight left - refuterProof <- - implicationIntroductionProof - withNotRight - leftAtRefuter - (\withLeft _leftProof -> do - rightAtLeft <- - scopedTerm - withLeft - right - implicationIntroductionProof - withLeft - rightAtLeft - (\withBoth rightProof -> do - notRightCurrent <- - hypothesisProof - withBoth - notRight - implicationEliminationProof - withBoth - notRightCurrent - rightProof)) - implicationEliminationProof - withNotRight - (weakenForHypothesis conjunction) - refuterProof) - doubleNegationEliminationProof - context - rightProposition - doubleNegation - -disjunctionTerm - :: CanonicalTerm global - -> CanonicalTerm global - -> CanonicalTerm global -disjunctionTerm left right = - CImp - (CImp left CFalsum) - right - -disjunctionLeftProof - :: Eq global - => ProofContext global - -> CanonicalTerm global - -> BuiltProof global - -> Either - KernelProofBuildError - (BuiltProof global) -disjunctionLeftProof context right leftProof = do - notLeft <- - scopedTerm context - (CImp - (scopedCoreTerm - (builtProofStatement leftProof)) - CFalsum) - rightTarget <- - scopedTerm context right - implicationIntroductionProof - context - notLeft - (\extended notLeftProof -> do - falsum <- - implicationEliminationProof - extended - notLeftProof - (weakenForHypothesis - leftProof) - falsumEliminationProof - extended - falsum - rightTarget) - -disjunctionRightProof - :: ProofContext global - -> CanonicalTerm global - -> BuiltProof global - -> Either - KernelProofBuildError - (BuiltProof global) -disjunctionRightProof context left rightProof = do - notLeft <- - scopedTerm context - (CImp left CFalsum) - implicationIntroductionProof - context - notLeft - (\_extended _notLeftProof -> - pure - (weakenForHypothesis - rightProof)) - -disjunctionEliminationProof - :: Eq global - => ProofContext global - -> CanonicalTerm global - -> CanonicalTerm global - -> BuiltProof global - -> ScopedCheckedCore global - -> ( ProofContext global - -> BuiltProof global - -> Either - KernelProofBuildError - (BuiltProof global) - ) - -> ( ProofContext global - -> BuiltProof global - -> Either - KernelProofBuildError - (BuiltProof global) - ) - -> Either - KernelProofBuildError - (BuiltProof global) -disjunctionEliminationProof - context - left - right - disjunction - result - leftCase - rightCase = do - leftProposition <- - scopedTerm context left - rightProposition <- - scopedTerm context right - leftImplication <- - implicationIntroductionProof - context - leftProposition - leftCase - rightImplication <- - implicationIntroductionProof - context - rightProposition - rightCase - notResult <- - scopedTerm context - (CImp - (scopedCoreTerm result) - CFalsum) - doubleNegation <- - implicationIntroductionProof - context - notResult - (\extended notResultProof -> do - leftAtNotResult <- - scopedTerm extended left - notLeftProof <- - implicationIntroductionProof - extended - leftAtNotResult - (\withLeft leftProof -> do - resultProof <- - implicationEliminationProof - withLeft - (weakenForHypothesis - (weakenForHypothesis - leftImplication)) - leftProof - implicationEliminationProof - withLeft - (weakenForHypothesis - notResultProof) - resultProof) - rightProof <- - implicationEliminationProof - extended - (weakenForHypothesis - disjunction) - notLeftProof - resultProof <- - implicationEliminationProof - extended - (weakenForHypothesis - rightImplication) - rightProof - implicationEliminationProof - extended - notResultProof - resultProof) - doubleNegationEliminationProof - context - result - doubleNegation - -existentialTerm - :: CoreType - -> CanonicalTerm global - -> CanonicalTerm global -existentialTerm binderType body = - CImp - (CForall binderType - (CImp body CFalsum)) - CFalsum - -existentialIntroductionProof - :: Eq global - => ProofContext global - -> CoreType - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> BuiltProof global - -> Either - KernelProofBuildError - (BuiltProof global) -existentialIntroductionProof - context - binderType - bodyUnderBinder - witness - bodyAtWitness = do - unless - (proofContextTypes context - == drop 1 - (scopedCoreContext - bodyUnderBinder)) - (Left ProofExpectedUnaryBinder) - universalNegation <- - scopedTerm context - (CForall binderType - (CImp - (scopedCoreTerm - bodyUnderBinder) - CFalsum)) - implicationIntroductionProof - context - universalNegation - (\extended universalProof -> do - negatedBody <- - forallEliminationProof - extended - universalProof - witness - implicationEliminationProof - extended - negatedBody - (weakenForHypothesis - bodyAtWitness)) - -existentialEliminationProof - :: Eq global - => ProofContext global - -> CoreType - -> ScopedCheckedCore global - -> BuiltProof global - -> ScopedCheckedCore global - -> ( ProofContext global - -> ScopedCheckedCore global - -> BuiltProof global - -> Either - KernelProofBuildError - (BuiltProof global) - ) - -> Either - KernelProofBuildError - (BuiltProof global) -existentialEliminationProof - context - binderType - bodyUnderBinder - existential - result - bodyCase = do - notResult <- - scopedTerm context - (CImp - (scopedCoreTerm result) - CFalsum) - notResultUnderBinder <- - first ProofTermIllTyped - (weakenScopedCore - (contextGlobalType context) - binderType - notResult) - doubleNegation <- - implicationIntroductionProof - context - notResult - (\withNotResult _notResultProof -> do - universalNegation <- - forallIntroductionProof - withNotResult - binderType - (\withBinder variable -> do - let body = - bodyUnderBinder - implicationIntroductionProof - withBinder - body - (\withBody bodyProof -> do - resultProof <- - bodyCase - withBody - variable - bodyProof - notResultCurrent <- - hypothesisProof - withBody - notResultUnderBinder - implicationEliminationProof - withBody - notResultCurrent - resultProof)) - implicationEliminationProof - withNotResult - (weakenForHypothesis - existential) - universalNegation) - doubleNegationEliminationProof - context - result - doubleNegation - -setLfpBoundProof - :: ProofContext global - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> Either - KernelProofBuildError - (BuiltProof global) -setLfpBoundProof - (ProofContext - foundation - globalType - _types - _hypotheses) - domain - operator = do - result <- - first (ProofSetLfpRuleFailed . Text.pack . show) - (SetLfp.setLfpBound - foundation - globalType - domain - operator) - pure - (BuiltProof - result - (setLfpBoundDerivation - domain - operator)) - -setLfpFixedProof - :: Eq global - => ProofContext global - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> BuiltProof global - -> Either - KernelProofBuildError - (BuiltProof global) -setLfpFixedProof - (ProofContext - foundation - globalType - _types - _hypotheses) - domain - operator - monotone = do - result <- - first (ProofSetLfpRuleFailed . Text.pack . show) - (SetLfp.setLfpFixed - foundation - globalType - domain - operator - (builtProofStatement - monotone)) - pure - (BuiltProof - result - (setLfpFixedDerivation - domain - operator - (builtProofDerivation - monotone))) - -setLfpInductProof - :: Eq global - => ProofContext global - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> BuiltProof global - -> BuiltProof global - -> BuiltProof global - -> Either - KernelProofBuildError - (BuiltProof global) -setLfpInductProof - (ProofContext - foundation - globalType - _types - _hypotheses) - domain - operator - predicate - element - monotone - member - closure = do - result <- - first (ProofSetLfpRuleFailed . Text.pack . show) - (SetLfp.setLfpInduct - foundation - globalType - domain - operator - predicate - element - (builtProofStatement - monotone) - (builtProofStatement - member) - (builtProofStatement - closure)) - pure - (BuiltProof - result - (setLfpInductDerivation - domain - operator - predicate - element - (builtProofDerivation - monotone) - (builtProofDerivation - member) - (builtProofDerivation - closure))) - -contextGlobalType - :: ProofContext global - -> (global -> Maybe CoreType) -contextGlobalType - (ProofContext - _foundation - globalType - _types - _hypotheses) = - globalType - -equalityParts - :: ScopedCheckedCore global - -> Either - KernelProofBuildError - ( CoreType - , CanonicalTerm global - , CanonicalTerm global - ) -equalityParts equality = - case scopedCoreTerm equality of - CEq operandType left right -> - Right (operandType, left, right) - _ -> - Left ProofExpectedEquality - -weakenForHypothesis - :: BuiltProof global - -> BuiltProof global -weakenForHypothesis - (BuiltProof statement derivation) = - BuiltProof - statement - (weakenDerivationHypotheses 1 derivation) diff --git a/source/Checking/Kernel/Semantics.hs b/source/Checking/Kernel/Semantics.hs deleted file mode 100644 index 3306b09..0000000 --- a/source/Checking/Kernel/Semantics.hs +++ /dev/null @@ -1,436 +0,0 @@ -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE NoImplicitPrelude #-} - --- | Checked logical inference over scoped canonical HOL terms. -module Checking.Kernel.Semantics - ( implicationElimination - , implicationIntroduction - , forallElimination - , forallIntroduction - , falsumElimination - , equalityReflexivity - , equalityCongruenceApplication - , equalityCongruenceLambda - , equalityModusPonens - , convertJudgment - , KernelSemanticsError(..) - ) where - -import Base -import Checking.Core - -import Control.Monad (unless) -import Data.Bifunctor (first) -import Numeric.Natural (Natural) - - -data KernelSemanticsError - = KernelContextMismatch - ![CoreType] - ![CoreType] - | KernelBinderContextMismatch - !CoreType - ![CoreType] - | KernelExpectedProposition !CoreType - | KernelExpectedImplication - | KernelImplicationPremiseMismatch - | KernelExpectedForall - | KernelForallArgumentTypeMismatch - !CoreType - !CoreType - | KernelExpectedFalsum - | KernelExpectedEquality - | KernelEqualityOperandTypeMismatch - !CoreType - !CoreType - | KernelExpectedFunctionEquality !CoreType - | KernelEqualityPremiseMismatch - | KernelConversionBudgetExhausted - | KernelConversionMismatch - | KernelConclusionIllTyped !CoreCheckError - deriving stock (Show, Eq) - -implicationElimination - :: Eq global - => (global -> Maybe CoreType) - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> Either - KernelSemanticsError - (ScopedCheckedCore global) -implicationElimination globalType implication premise = do - requireSameContext implication premise - requireProposition implication - requireProposition premise - case scopedCoreTerm implication of - CImp expected conclusion - | scopedCoreTerm premise == expected -> - checkConclusion - globalType - (scopedCoreContext implication) - conclusion - | otherwise -> - Left KernelImplicationPremiseMismatch - _ -> - Left KernelExpectedImplication - -implicationIntroduction - :: (global -> Maybe CoreType) - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> Either - KernelSemanticsError - (ScopedCheckedCore global) -implicationIntroduction globalType premise conclusion = do - requireSameContext premise conclusion - requireProposition premise - requireProposition conclusion - checkConclusion - globalType - (scopedCoreContext premise) - (CImp - (scopedCoreTerm premise) - (scopedCoreTerm conclusion)) - -forallElimination - :: (global -> Maybe CoreType) - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> Either - KernelSemanticsError - (ScopedCheckedCore global) -forallElimination globalType quantified argument = do - requireSameContext quantified argument - requireProposition quantified - case scopedCoreTerm quantified of - CForall binderType body - | scopedCoreType argument == binderType -> - checkConclusion - globalType - (scopedCoreContext quantified) - (instantiateCanonical - (scopedCoreTerm argument) - body) - | otherwise -> - Left - (KernelForallArgumentTypeMismatch - binderType - (scopedCoreType argument)) - _ -> - Left KernelExpectedForall - -forallIntroduction - :: (global -> Maybe CoreType) - -> CoreType - -> ScopedCheckedCore global - -> Either - KernelSemanticsError - (ScopedCheckedCore global) -forallIntroduction globalType binderType body = do - requireProposition body - outerContext <- - case scopedCoreContext body of - actualBinder : context - | actualBinder == binderType -> - Right context - | otherwise -> - Left - (KernelBinderContextMismatch - binderType - (scopedCoreContext body)) - [] -> - Left - (KernelBinderContextMismatch - binderType - []) - checkConclusion - globalType - outerContext - (CForall - binderType - (scopedCoreTerm body)) - -falsumElimination - :: (global -> Maybe CoreType) - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> Either - KernelSemanticsError - (ScopedCheckedCore global) -falsumElimination _globalType falsum target = do - requireSameContext falsum target - requireProposition falsum - requireProposition target - case scopedCoreTerm falsum of - CFalsum -> - Right target - _ -> - Left KernelExpectedFalsum - -equalityReflexivity - :: (global -> Maybe CoreType) - -> ScopedCheckedCore global - -> Either - KernelSemanticsError - (ScopedCheckedCore global) -equalityReflexivity globalType operand = - checkConclusion - globalType - (scopedCoreContext operand) - (CEq - (scopedCoreType operand) - (scopedCoreTerm operand) - (scopedCoreTerm operand)) - -equalityCongruenceApplication - :: (global -> Maybe CoreType) - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> Either - KernelSemanticsError - (ScopedCheckedCore global) -equalityCongruenceApplication - globalType - functionEquality - argumentEquality = do - requireSameContext functionEquality argumentEquality - (functionType, leftFunction, rightFunction) <- - equalityOperands functionEquality - (argumentType, leftArgument, rightArgument) <- - equalityOperands argumentEquality - case functionType of - TyArrow expectedArgument resultType - | expectedArgument == argumentType -> - checkConclusion - globalType - (scopedCoreContext functionEquality) - (CEq - resultType - (CApp leftFunction leftArgument) - (CApp rightFunction rightArgument)) - | otherwise -> - Left - (KernelEqualityOperandTypeMismatch - expectedArgument - argumentType) - other -> - Left (KernelExpectedFunctionEquality other) - -equalityCongruenceLambda - :: (global -> Maybe CoreType) - -> CoreType - -> ScopedCheckedCore global - -> Either - KernelSemanticsError - (ScopedCheckedCore global) -equalityCongruenceLambda - globalType - binderType - bodyEquality = do - (bodyType, leftBody, rightBody) <- - equalityOperands bodyEquality - outerContext <- - case scopedCoreContext bodyEquality of - actualBinder : context - | actualBinder == binderType -> - Right context - | otherwise -> - Left - (KernelBinderContextMismatch - binderType - (scopedCoreContext bodyEquality)) - [] -> - Left - (KernelBinderContextMismatch - binderType - []) - checkConclusion - globalType - outerContext - (CEq - (TyArrow binderType bodyType) - (CLam binderType leftBody) - (CLam binderType rightBody)) - -equalityModusPonens - :: Eq global - => (global -> Maybe CoreType) - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> Either - KernelSemanticsError - (ScopedCheckedCore global) -equalityModusPonens globalType propositionEquality premise = do - requireSameContext propositionEquality premise - requireProposition premise - (operandType, left, right) <- - equalityOperands propositionEquality - unless - (operandType == TyProp) - (Left - (KernelEqualityOperandTypeMismatch - TyProp - operandType)) - unless - (left == scopedCoreTerm premise) - (Left KernelEqualityPremiseMismatch) - checkConclusion - globalType - (scopedCoreContext premise) - right - --- | Recheck a displayed proposition and independently establish beta --- conversion within the supplied contraction budget. -convertJudgment - :: Eq global - => (global -> Maybe CoreType) - -> Natural - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> Either - KernelSemanticsError - (ScopedCheckedCore global) -convertJudgment globalType budget source target = do - requireSameContext source target - requireProposition source - requireProposition target - sourceNormal <- - normalizeCanonical budget - (scopedCoreTerm source) - targetNormal <- - normalizeCanonical budget - (scopedCoreTerm target) - unless - (sourceNormal == targetNormal) - (Left KernelConversionMismatch) - checkConclusion - globalType - (scopedCoreContext target) - (scopedCoreTerm target) - -requireSameContext - :: ScopedCheckedCore global - -> ScopedCheckedCore global - -> Either KernelSemanticsError () -requireSameContext left right - | scopedCoreContext left - == scopedCoreContext right = - Right () - | otherwise = - Left - (KernelContextMismatch - (scopedCoreContext left) - (scopedCoreContext right)) - -requireProposition - :: ScopedCheckedCore global - -> Either KernelSemanticsError () -requireProposition value - | scopedCoreType value == TyProp = - Right () - | otherwise = - Left - (KernelExpectedProposition - (scopedCoreType value)) - -equalityOperands - :: ScopedCheckedCore global - -> Either - KernelSemanticsError - (CoreType, CanonicalTerm global, CanonicalTerm global) -equalityOperands equality = do - requireProposition equality - case scopedCoreTerm equality of - CEq operandType left right -> - Right (operandType, left, right) - _ -> - Left KernelExpectedEquality - -checkConclusion - :: (global -> Maybe CoreType) - -> [CoreType] - -> CanonicalTerm global - -> Either - KernelSemanticsError - (ScopedCheckedCore global) -checkConclusion globalType context = - first KernelConclusionIllTyped - . checkScopedCanonicalCore globalType context - -normalizeCanonical - :: Natural - -> CanonicalTerm global - -> Either - KernelSemanticsError - (CanonicalTerm global) -normalizeCanonical budget term = - fst <$> normalize budget term - where - normalize remaining = \case - CBound index -> - pure (CBound index, remaining) - CGlobal global -> - pure (CGlobal global, remaining) - CIntrinsic intrinsic -> - pure (CIntrinsic intrinsic, remaining) - COpaqueInteger integer -> - pure (COpaqueInteger integer, remaining) - CApp function argument -> do - (functionNormal, afterFunction) <- - normalize remaining function - case functionNormal of - CLam _binderType body -> do - afterContraction <- - consumeReduction afterFunction - normalize - afterContraction - (instantiateCanonical - argument - body) - _ -> do - (argumentNormal, afterArgument) <- - normalize afterFunction argument - pure - ( CApp - functionNormal - argumentNormal - , afterArgument - ) - CLam binderType body -> do - (bodyNormal, remaining') <- - normalize remaining body - pure - (CLam binderType bodyNormal, remaining') - CFalsum -> - pure (CFalsum, remaining) - CImp premise conclusion -> do - (premiseNormal, afterPremise) <- - normalize remaining premise - (conclusionNormal, afterConclusion) <- - normalize afterPremise conclusion - pure - ( CImp premiseNormal conclusionNormal - , afterConclusion - ) - CEq operandType left right -> do - (leftNormal, afterLeft) <- - normalize remaining left - (rightNormal, afterRight) <- - normalize afterLeft right - pure - ( CEq - operandType - leftNormal - rightNormal - , afterRight - ) - CForall binderType body -> do - (bodyNormal, remaining') <- - normalize remaining body - pure - (CForall binderType bodyNormal, remaining') - - consumeReduction 0 = - Left KernelConversionBudgetExhausted - consumeReduction remaining = - Right (remaining - 1) diff --git a/source/Checking/Kernel/SetLfp.hs b/source/Checking/Kernel/SetLfp.hs deleted file mode 100644 index e3fa175..0000000 --- a/source/Checking/Kernel/SetLfp.hs +++ /dev/null @@ -1,762 +0,0 @@ -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE NoImplicitPrelude #-} - --- | The four checked rules for the bounded set-valued least fixed point. -module Checking.Kernel.SetLfp - ( setLfpBound - , setLfpLeast - , setLfpFixed - , setLfpInduct - , setLfpTerm - , memberProposition - , subsetProposition - , boundedMonoProposition - , inductionClosureProposition - , SetLfpRuleError(..) - ) where - -import Base -import Checking.Core -import Checking.Foundation - -import Data.Bifunctor (first) -import Numeric.Natural (Natural) - - -data SetLfpRuleError - = SetLfpRuleSignatureMismatch - !KernelRuleTag - !KernelRuleSignature - !KernelRuleSignature - | SetLfpRuleContextMismatch - !KernelRuleTag - ![CoreType] - ![CoreType] - | SetLfpRuleArgumentTypeMismatch - !KernelRuleTag - !Natural - !CoreType - !CoreType - | SetLfpRulePremiseIsNotProposition - !KernelRuleTag - !Natural - !CoreType - | SetLfpRulePremiseMismatch - !KernelRuleTag - !Natural - | SetLfpRuleConstructionIllTyped - !KernelRuleTag - !CoreCheckError - deriving stock (Show, Eq) - -setLfpBound - :: CheckedFoundation - -> (global -> Maybe CoreType) - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> Either - SetLfpRuleError - (ScopedCheckedCore global) -setLfpBound foundation globalType domain operator = do - validateApplication - foundation - SetLfpBound - [domain, operator] - [] - fixedPoint <- - setLfpTermFor - SetLfpBound - globalType - domain - operator - subsetFor - SetLfpBound - globalType - fixedPoint - domain - -setLfpLeast - :: Eq global - => CheckedFoundation - -> (global -> Maybe CoreType) - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> Either - SetLfpRuleError - (ScopedCheckedCore global) -setLfpLeast - foundation - globalType - domain - operator - candidate - closedPremise - boundedPremise = do - validateApplication - foundation - SetLfpLeast - [domain, operator, candidate] - [closedPremise, boundedPremise] - operatorCandidate <- - applyFor - SetLfpLeast - globalType - operator - candidate - expectedClosed <- - subsetFor - SetLfpLeast - globalType - operatorCandidate - candidate - expectedBounded <- - subsetFor - SetLfpLeast - globalType - candidate - domain - requirePremise - SetLfpLeast - 0 - expectedClosed - closedPremise - requirePremise - SetLfpLeast - 1 - expectedBounded - boundedPremise - fixedPoint <- - setLfpTermFor - SetLfpLeast - globalType - domain - operator - subsetFor - SetLfpLeast - globalType - fixedPoint - candidate - -setLfpFixed - :: Eq global - => CheckedFoundation - -> (global -> Maybe CoreType) - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> Either - SetLfpRuleError - (ScopedCheckedCore global) -setLfpFixed - foundation - globalType - domain - operator - monotonePremise = do - validateApplication - foundation - SetLfpFixed - [domain, operator] - [monotonePremise] - expectedMonotone <- - boundedMonoFor - SetLfpFixed - globalType - domain - operator - requirePremise - SetLfpFixed - 0 - expectedMonotone - monotonePremise - fixedPoint <- - setLfpTermFor - SetLfpFixed - globalType - domain - operator - unfolded <- - applyFor - SetLfpFixed - globalType - operator - fixedPoint - checkedFor - SetLfpFixed - globalType - (scopedCoreContext domain) - (CEq - TySet - (scopedCoreTerm fixedPoint) - (scopedCoreTerm unfolded)) - -setLfpInduct - :: Eq global - => CheckedFoundation - -> (global -> Maybe CoreType) - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> Either - SetLfpRuleError - (ScopedCheckedCore global) -setLfpInduct - foundation - globalType - domain - operator - predicate - element - monotonePremise - memberPremise - closurePremise = do - validateApplication - foundation - SetLfpInduct - [domain, operator, predicate, element] - [monotonePremise, memberPremise, closurePremise] - expectedMonotone <- - boundedMonoFor - SetLfpInduct - globalType - domain - operator - requirePremise - SetLfpInduct - 0 - expectedMonotone - monotonePremise - fixedPoint <- - setLfpTermFor - SetLfpInduct - globalType - domain - operator - expectedMember <- - memberFor - SetLfpInduct - globalType - element - fixedPoint - requirePremise - SetLfpInduct - 1 - expectedMember - memberPremise - expectedClosure <- - inductionClosureFor - SetLfpInduct - globalType - fixedPoint - operator - predicate - requirePremise - SetLfpInduct - 2 - expectedClosure - closurePremise - applyFor - SetLfpInduct - globalType - predicate - element - -setLfpTerm - :: (global -> Maybe CoreType) - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> Either - SetLfpRuleError - (ScopedCheckedCore global) -setLfpTerm = - setLfpTermFor SetLfpBound - -memberProposition - :: (global -> Maybe CoreType) - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> Either - SetLfpRuleError - (ScopedCheckedCore global) -memberProposition = - memberFor SetLfpInduct - -subsetProposition - :: (global -> Maybe CoreType) - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> Either - SetLfpRuleError - (ScopedCheckedCore global) -subsetProposition = - subsetFor SetLfpBound - -boundedMonoProposition - :: (global -> Maybe CoreType) - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> Either - SetLfpRuleError - (ScopedCheckedCore global) -boundedMonoProposition = - boundedMonoFor SetLfpFixed - -inductionClosureProposition - :: (global -> Maybe CoreType) - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> Either - SetLfpRuleError - (ScopedCheckedCore global) -inductionClosureProposition globalType domain operator predicate = do - fixedPoint <- - setLfpTermFor - SetLfpInduct - globalType - domain - operator - inductionClosureFor - SetLfpInduct - globalType - fixedPoint - operator - predicate - -validateApplication - :: CheckedFoundation - -> KernelRuleTag - -> [ScopedCheckedCore global] - -> [ScopedCheckedCore global] - -> Either SetLfpRuleError () -validateApplication foundation tag arguments premises = do - let expected = - expectedSignature tag - actual = - foundationRuleSignature foundation tag - if actual == expected - then pure () - else - Left - (SetLfpRuleSignatureMismatch - tag - expected - actual) - case arguments of - [] -> - pure () - firstArgument : remainingArguments -> do - traverse_ - (requireContext tag firstArgument) - remainingArguments - traverse_ - (requireContext tag firstArgument) - premises - traverse_ - (uncurry - (requireArgumentType tag)) - (zip [0 ..] arguments) - traverse_ - (uncurry - (requireProposition tag)) - (zip [0 ..] premises) - -expectedSignature :: KernelRuleTag -> KernelRuleSignature -expectedSignature = \case - SetLfpBound -> - KernelRuleSignature - [TySet, TySet `TyArrow` TySet] - 0 - SetLfpLeast -> - KernelRuleSignature - [TySet, TySet `TyArrow` TySet, TySet] - 2 - SetLfpFixed -> - KernelRuleSignature - [TySet, TySet `TyArrow` TySet] - 1 - SetLfpInduct -> - KernelRuleSignature - [ TySet - , TySet `TyArrow` TySet - , TySet `TyArrow` TyProp - , TySet - ] - 3 - -expectedArgumentTypes - :: KernelRuleTag - -> [CoreType] -expectedArgumentTypes tag = - case expectedSignature tag of - KernelRuleSignature argumentTypes _premiseCount -> - argumentTypes - -requireContext - :: KernelRuleTag - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> Either SetLfpRuleError () -requireContext tag expected actual - | scopedCoreContext expected - == scopedCoreContext actual = - Right () - | otherwise = - Left - (SetLfpRuleContextMismatch - tag - (scopedCoreContext expected) - (scopedCoreContext actual)) - -requireArgumentType - :: KernelRuleTag - -> Natural - -> ScopedCheckedCore global - -> Either SetLfpRuleError () -requireArgumentType tag index argument = - case atNatural index (expectedArgumentTypes tag) of - Nothing -> - impossible - "fixed-point rule argument inventory is inconsistent" - Just expected - | scopedCoreType argument == expected -> - Right () - | otherwise -> - Left - (SetLfpRuleArgumentTypeMismatch - tag - index - expected - (scopedCoreType argument)) - -requireProposition - :: KernelRuleTag - -> Natural - -> ScopedCheckedCore global - -> Either SetLfpRuleError () -requireProposition tag index premise - | scopedCoreType premise == TyProp = - Right () - | otherwise = - Left - (SetLfpRulePremiseIsNotProposition - tag - index - (scopedCoreType premise)) - -requirePremise - :: Eq global - => KernelRuleTag - -> Natural - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> Either SetLfpRuleError () -requirePremise tag index expected actual - | expected == actual = - Right () - | otherwise = - Left - (SetLfpRulePremiseMismatch - tag - index) - -setLfpTermFor - :: KernelRuleTag - -> (global -> Maybe CoreType) - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> Either - SetLfpRuleError - (ScopedCheckedCore global) -setLfpTermFor tag globalType domain operator = - checkedFor tag globalType - (scopedCoreContext domain) - (CApp - (CApp - (CIntrinsic ISetLfp) - (scopedCoreTerm domain)) - (scopedCoreTerm operator)) - -applyFor - :: KernelRuleTag - -> (global -> Maybe CoreType) - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> Either - SetLfpRuleError - (ScopedCheckedCore global) -applyFor tag globalType function argument = do - requireContext tag function argument - checkedFor tag globalType - (scopedCoreContext function) - (CApp - (scopedCoreTerm function) - (scopedCoreTerm argument)) - -memberFor - :: KernelRuleTag - -> (global -> Maybe CoreType) - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> Either - SetLfpRuleError - (ScopedCheckedCore global) -memberFor tag globalType element set = do - requireContext tag element set - checkedFor tag globalType - (scopedCoreContext element) - (CApp - (CApp - (CIntrinsic Member) - (scopedCoreTerm element)) - (scopedCoreTerm set)) - -subsetFor - :: KernelRuleTag - -> (global -> Maybe CoreType) - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> Either - SetLfpRuleError - (ScopedCheckedCore global) -subsetFor tag globalType left right = do - requireContext tag left right - left' <- weakenFor tag globalType TySet left - right' <- weakenFor tag globalType TySet right - element <- - checkedFor tag globalType - (TySet : scopedCoreContext left) - (CBound 0) - inLeft <- - memberFor tag globalType element left' - inRight <- - memberFor tag globalType element right' - checkedFor tag globalType - (scopedCoreContext left) - (CForall - TySet - (CImp - (scopedCoreTerm inLeft) - (scopedCoreTerm inRight))) - -boundedMonoFor - :: KernelRuleTag - -> (global -> Maybe CoreType) - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> Either - SetLfpRuleError - (ScopedCheckedCore global) -boundedMonoFor tag globalType domain operator = do - requireContext tag domain operator - operatorDomain <- - applyFor tag globalType operator domain - bounded <- - subsetFor tag globalType operatorDomain domain - - domainX <- - weakenFor tag globalType TySet domain - operatorX <- - weakenFor tag globalType TySet operator - domainXY <- - weakenFor tag globalType TySet domainX - operatorXY <- - weakenFor tag globalType TySet operatorX - let xyContext = - TySet : TySet : scopedCoreContext domain - x <- - checkedFor tag globalType - xyContext - (CBound 1) - y <- - checkedFor tag globalType - xyContext - (CBound 0) - xSubsetY <- - subsetFor tag globalType x y - ySubsetDomain <- - subsetFor tag globalType y domainXY - antecedent <- - conjunctionFor - tag - globalType - xSubsetY - ySubsetDomain - operatorXValue <- - applyFor tag globalType operatorXY x - operatorYValue <- - applyFor tag globalType operatorXY y - imageSubset <- - subsetFor - tag - globalType - operatorXValue - operatorYValue - monotoneBody <- - implicationFor - tag - globalType - antecedent - imageSubset - quantifiedY <- - closeForallFor tag globalType TySet monotoneBody - quantifiedXY <- - closeForallFor tag globalType TySet quantifiedY - conjunctionFor - tag - globalType - bounded - quantifiedXY - -inductionClosureFor - :: KernelRuleTag - -> (global -> Maybe CoreType) - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> Either - SetLfpRuleError - (ScopedCheckedCore global) -inductionClosureFor - tag - globalType - fixedPoint - operator - predicate = do - fixedPoint' <- - weakenFor tag globalType TySet fixedPoint - operator' <- - weakenFor tag globalType TySet operator - predicate' <- - weakenFor tag globalType TySet predicate - element <- - checkedFor tag globalType - (TySet : scopedCoreContext fixedPoint) - (CBound 0) - separated <- - checkedFor tag globalType - (scopedCoreContext fixedPoint') - (CApp - (CApp - (CIntrinsic Sep) - (scopedCoreTerm fixedPoint')) - (scopedCoreTerm predicate')) - unfolded <- - applyFor tag globalType operator' separated - memberUnfolded <- - memberFor tag globalType element unfolded - predicateElement <- - applyFor tag globalType predicate' element - body <- - implicationFor - tag - globalType - memberUnfolded - predicateElement - closeForallFor tag globalType TySet body - -conjunctionFor - :: KernelRuleTag - -> (global -> Maybe CoreType) - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> Either - SetLfpRuleError - (ScopedCheckedCore global) -conjunctionFor tag globalType left right = do - requireContext tag left right - checkedFor tag globalType - (scopedCoreContext left) - (CImp - (CImp - (scopedCoreTerm left) - (CImp - (scopedCoreTerm right) - CFalsum)) - CFalsum) - -implicationFor - :: KernelRuleTag - -> (global -> Maybe CoreType) - -> ScopedCheckedCore global - -> ScopedCheckedCore global - -> Either - SetLfpRuleError - (ScopedCheckedCore global) -implicationFor tag globalType premise conclusion = do - requireContext tag premise conclusion - checkedFor tag globalType - (scopedCoreContext premise) - (CImp - (scopedCoreTerm premise) - (scopedCoreTerm conclusion)) - -closeForallFor - :: KernelRuleTag - -> (global -> Maybe CoreType) - -> CoreType - -> ScopedCheckedCore global - -> Either - SetLfpRuleError - (ScopedCheckedCore global) -closeForallFor tag globalType binderType body = - case scopedCoreContext body of - actualBinder : outerContext - | actualBinder == binderType -> - checkedFor tag globalType - outerContext - (CForall - binderType - (scopedCoreTerm body)) - _ -> - Left - (SetLfpRuleContextMismatch - tag - (binderType : drop 1 - (scopedCoreContext body)) - (scopedCoreContext body)) - -weakenFor - :: KernelRuleTag - -> (global -> Maybe CoreType) - -> CoreType - -> ScopedCheckedCore global - -> Either - SetLfpRuleError - (ScopedCheckedCore global) -weakenFor tag globalType binderType = - first - (SetLfpRuleConstructionIllTyped tag) - . weakenScopedCore - globalType - binderType - -checkedFor - :: KernelRuleTag - -> (global -> Maybe CoreType) - -> [CoreType] - -> CanonicalTerm global - -> Either - SetLfpRuleError - (ScopedCheckedCore global) -checkedFor tag globalType context = - first - (SetLfpRuleConstructionIllTyped tag) - . checkScopedCanonicalCore - globalType - context - -atNatural :: Natural -> [a] -> Maybe a -atNatural _index [] = - Nothing -atNatural 0 (value : _rest) = - Just value -atNatural index (_value : rest) = - atNatural (index - 1) rest |