diff options
Diffstat (limited to 'source/Felix/Checking/Kernel/Semantics.hs')
| -rw-r--r-- | source/Felix/Checking/Kernel/Semantics.hs | 436 |
1 files changed, 436 insertions, 0 deletions
diff --git a/source/Felix/Checking/Kernel/Semantics.hs b/source/Felix/Checking/Kernel/Semantics.hs new file mode 100644 index 0000000..f9cfcfa --- /dev/null +++ b/source/Felix/Checking/Kernel/Semantics.hs @@ -0,0 +1,436 @@ +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE NoImplicitPrelude #-} + +-- | Checked logical inference over scoped canonical HOL terms. +module Felix.Checking.Kernel.Semantics + ( implicationElimination + , implicationIntroduction + , forallElimination + , forallIntroduction + , falsumElimination + , equalityReflexivity + , equalityCongruenceApplication + , equalityCongruenceLambda + , equalityModusPonens + , convertJudgment + , KernelSemanticsError(..) + ) where + +import Base +import Felix.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) |