1 files changed, 0 insertions, 105 deletions
diff --git a/source/Checking/Typed/Reflexivity.hs b/source/Checking/Typed/Reflexivity.hs
deleted file mode 100644
index f548727..0000000
--- a/source/Checking/Typed/Reflexivity.hs
+++ /dev/null
@@ -1,105 +0,0 @@
-{-# LANGUAGE DerivingStrategies #-}
-{-# LANGUAGE NoImplicitPrelude #-}
-
--- | Dependency-free typed preparation for closed ground reflexivity.
-module Checking.Typed.Reflexivity
-    ( PreparedGroundReflexivity
-    , prepareGroundReflexivity
-    , groundReflexivityTarget
-    , groundReflexivityDerivation
-    , GroundReflexivityError(..)
-    ) where
-
-import Base hiding (Empty)
-import Checking.Core
-import Checking.Kernel.Derivation
-import Checking.Transition
-import Checking.Typed.Ground
-import Syntax.Internal
-
-import Data.Bifunctor (first)
-
-
-data PreparedGroundReflexivity =
-    PreparedGroundReflexivity
-        !(FrozenCheckedCore CheckedGlobalRef)
-        !(KernelDerivation CheckedGlobalRef)
-
-groundReflexivityTarget
-    :: PreparedGroundReflexivity
-    -> FrozenCheckedCore CheckedGlobalRef
-groundReflexivityTarget
-        (PreparedGroundReflexivity target _derivation) =
-    target
-
-groundReflexivityDerivation
-    :: PreparedGroundReflexivity
-    -> KernelDerivation CheckedGlobalRef
-groundReflexivityDerivation
-        (PreparedGroundReflexivity _target derivation) =
-    derivation
-
-data GroundReflexivityError
-    = GroundReflexivityOperandIllTyped !CoreCheckError
-    | GroundReflexivityOperandFreezeFailed !FreezeError
-    | GroundReflexivityTargetIllTyped !CoreCheckError
-    | GroundReflexivityTargetFreezeFailed !FreezeError
-    deriving stock (Show, Eq)
-
--- | Return 'Nothing' when the formula is outside this intentionally small
--- typed family. A recognized formula either prepares completely or reports its
--- checked-core failure.
-prepareGroundReflexivity
-    :: Formula
-    -> Maybe
-        (Either
-            GroundReflexivityError
-            PreparedGroundReflexivity)
-prepareGroundReflexivity = \case
-    Equals _location left right -> do
-        guard (equivalent left right)
-        leftSyntax <- lowerGroundSetTerm left
-        Just do
-            leftFrozen <-
-                checkAndFreezeOperand leftSyntax
-            target <-
-                checkAndFreezeTarget
-                    leftSyntax
-                    leftSyntax
-            pure
-                (PreparedGroundReflexivity
-                    target
-                    (equalityReflexivityDerivation
-                        leftFrozen))
-    _ ->
-        Nothing
-
-checkAndFreezeOperand
-    :: CoreSyntax CheckedGlobalRef Void
-    -> Either
-        GroundReflexivityError
-        (FrozenCheckedCore CheckedGlobalRef)
-checkAndFreezeOperand syntax = do
-    checked <-
-        first GroundReflexivityOperandIllTyped
-            (checkClosedCore
-                (Just . checkedGlobalType)
-                syntax)
-    first GroundReflexivityOperandFreezeFailed
-        (freezeClosed checked)
-
-checkAndFreezeTarget
-    :: CoreSyntax CheckedGlobalRef Void
-    -> CoreSyntax CheckedGlobalRef Void
-    -> Either
-        GroundReflexivityError
-        (FrozenCheckedCore CheckedGlobalRef)
-checkAndFreezeTarget left right = do
-    checked <-
-        first GroundReflexivityTargetIllTyped
-            (checkClosedProposition
-                (Just . checkedGlobalType)
-                (coreEquality TySet left right))
-    first GroundReflexivityTargetFreezeFailed
-        (freezeClosed
-            (checkedPropositionCore checked))