1 files changed, 0 insertions, 72 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