2 files changed, 0 insertions, 177 deletions
diff --git a/source/Checking/Typed/Atomic.hs b/source/Checking/Typed/Atomic.hs
deleted file mode 100644
index 449928f..0000000
--- a/source/Checking/Typed/Atomic.hs
+++ /dev/null
@@ -1,72 +0,0 @@
-{-# LANGUAGE DerivingStrategies #-}
-{-# LANGUAGE NoImplicitPrelude #-}
-
--- | Closed applications of checked predicate signatures to ground sets.
-module Checking.Typed.Atomic
-    ( PreparedClosedAtomic
-    , prepareClosedAtomic
-    , closedAtomicStatement
-    , ClosedAtomicError(..)
-    ) where
-
-import Base
-import Checking.Core
-import Checking.Transition
-import Checking.Typed.Ground
-import Syntax.Internal
-
-import Data.Bifunctor (first)
-
-
-newtype PreparedClosedAtomic =
-    PreparedClosedAtomic
-        (FrozenCheckedCore CheckedGlobalRef)
-
-closedAtomicStatement
-    :: PreparedClosedAtomic
-    -> FrozenCheckedCore CheckedGlobalRef
-closedAtomicStatement
-        (PreparedClosedAtomic statement) =
-    statement
-
-data ClosedAtomicError
-    = ClosedAtomicIllTyped !CoreCheckError
-    | ClosedAtomicFreezeFailed !FreezeError
-    deriving stock (Show, Eq)
-
--- | Return 'Nothing' outside this deliberately small typed family. Once a
--- checked predicate global and ground arguments match, formation is total or
--- reports its typed-core failure.
-prepareClosedAtomic
-    :: (Symbol -> Maybe CheckedGlobalRef)
-    -> Formula
-    -> Maybe
-        (Either
-            ClosedAtomicError
-            PreparedClosedAtomic)
-prepareClosedAtomic resolveGlobal = \case
-    Atomic _location predicate arguments -> do
-        reference <-
-            resolveGlobal
-                (SymbolPredicate predicate)
-        loweredArguments <-
-            traverse lowerGroundSetTerm arguments
-        Just do
-            checked <-
-                first ClosedAtomicIllTyped
-                    (checkClosedProposition
-                        (Just . checkedGlobalType)
-                        (foldl'
-                            coreApply
-                            (coreGlobal reference)
-                            loweredArguments))
-            statement <-
-                first ClosedAtomicFreezeFailed
-                    (freezeClosed
-                        (checkedPropositionCore
-                            checked))
-            pure
-                (PreparedClosedAtomic
-                    statement)
-    _ ->
-        Nothing
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))