Migrate to `Felix` namespaceHEADhotg

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)