Migrate to `Felix` namespaceHEADhotg

1 files changed, 0 insertions, 436 deletions

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)