Plan and admit module declarations prospectively

1 files changed, 17 insertions, 12 deletions

diff --git a/source/Checking/Exact/Datatype.hs b/source/Checking/Exact/Datatype.hs
index 1aca139..d80053b 100644
--- a/source/Checking/Exact/Datatype.hs
+++ b/source/Checking/Exact/Datatype.hs
@@ -134,7 +134,7 @@ preparedExactDatatypeDescriptor
 
 lowerPreparedExactDatatype
     :: PreparedExactDatatype
-    -> Declaration.ModuleDriver failure
+    -> Declaration.LoweringDriver
         (Either
             Declaration.DeclarationError
             (Declaration.CheckedDeclaration
@@ -145,7 +145,7 @@ lowerPreparedExactDatatype
         prepared <-
             traverse
                 (\(PreparedExactDatatypeFact marker target _reference) ->
-                    Declaration.prepareFrozenCandidateSpecDriver
+                    Declaration.prepareFrozenCandidateSpecLowering
                         assertedObjects
                         target
                         SearchEligible
@@ -180,6 +180,11 @@ lowerPreparedExactDatatype
             bindings
             []
             [specs]
+            [ fmap
+                (const
+                    (Declaration.checkedDatatypePlanning descriptor))
+                specs
+            ]
             (CheckedExactDatatypeAuthorization
                 descriptor carrier constructorIds)
 
@@ -280,8 +285,8 @@ renderExactDatatypeError failure =
     shown :: Show value => value -> Text
     shown = Text.pack . show
 
-type Prepare failure =
-    ExceptT ExactDatatypeError (Declaration.ModuleDriver failure)
+type Prepare =
+    ExceptT ExactDatatypeError (Declaration.LoweringDriver)
 
 type SourceOccurrence = (Location, Raw.Marker, CanonicalLexicalEntry)
 
@@ -299,7 +304,7 @@ exactDatatypeInvalid declarationLocation failure =
 prepareExactDatatype
     :: Raw.Block
     -> [SourceOccurrence]
-    -> Declaration.ModuleDriver failure
+    -> Declaration.LoweringDriver
         (Either ExactDatatypeError PreparedExactDatatype)
 prepareExactDatatype block occurrences =
     Except.runExceptT do
@@ -348,8 +353,8 @@ prepareExactDatatype block occurrences =
                     (NonEmpty.length symbols)
                     (NonEmpty.length keys)))
         validateKeys occurrences keys
-        slot <- Except.lift Declaration.nextDeclarationSlotDriver
-        theory <- Except.lift Declaration.currentTheoryDriver
+        slot <- Except.lift Declaration.nextDeclarationSlotLowering
+        theory <- Except.lift Declaration.currentTheoryLowering
         objects <-
             sequence
                 (NonEmpty.zipWith
@@ -450,7 +455,7 @@ validateOccurrences
     -> Raw.Marker
     -> Raw.Datatype
     -> [SourceOccurrence]
-    -> Prepare failure (NonEmpty SemanticGlobalKey)
+    -> Prepare (NonEmpty SemanticGlobalKey)
 validateOccurrences location marker datatype occurrences = do
     expected <-
         Except.liftEither
@@ -534,7 +539,7 @@ expectedOccurrences location blockMarker datatype = do
 validateKeys
     :: [SourceOccurrence]
     -> NonEmpty SemanticGlobalKey
-    -> Prepare failure ()
+    -> Prepare ()
 validateKeys occurrences keys = do
     case duplicateWithLocation of
         Just (duplicate, duplicateLocation) ->
@@ -565,7 +570,7 @@ validateKeys occurrences keys = do
                 (ExactDatatypeFixedSemanticCollision occurrenceLocation key))
         visible <-
             Except.lift
-                (Declaration.resolveVisibleGlobalDriver key)
+                (Declaration.resolveVisibleGlobalLowering key)
         when (isJust visible)
             (Except.throwError
                 (ExactDatatypeGlobalAlreadyVisible occurrenceLocation key))
@@ -590,7 +595,7 @@ prepareObject
     -> Internal.Symbol
     -> SemanticGlobalKey
     -> Int
-    -> Prepare failure PreparedDatatypeObject
+    -> Prepare PreparedDatatypeObject
 prepareObject location slot theory index symbol key arity = do
     let coreType =
             foldr (const (TyArrow TySet)) TySet [1 .. arity]
@@ -602,7 +607,7 @@ prepareObject location slot theory index symbol key arity = do
                 (generatedObjectSlot index)
         content = OpaqueObjectContent theory seed coreType
         identity = opaqueObjectId theory seed coreType
-    available <- Except.lift (Declaration.objectAvailableDriver identity)
+    available <- Except.lift (Declaration.objectAvailableLowering identity)
     when available
         (Except.throwError
             (ExactDatatypeObjectAlreadyAvailable location identity))