Route declarations through checked envelopes

1 files changed, 70 insertions, 35 deletions

diff --git a/source/Checking/Exact/Datatype.hs b/source/Checking/Exact/Datatype.hs
index 8267dc9..1aca139 100644
--- a/source/Checking/Exact/Datatype.hs
+++ b/source/Checking/Exact/Datatype.hs
@@ -14,7 +14,9 @@ module Checking.Exact.Datatype
     , preparedExactDatatypeFactReference
     , preparedExactDatatypeDescriptor
     , prepareExactDatatype
-    , commitPreparedExactDatatype
+    , CheckedExactDatatypeAuthorization
+    , lowerPreparedExactDatatype
+    , authorizeCheckedExactDatatype
     , ExactDatatypeError(..)
     , exactDatatypeErrorLocation
     , renderExactDatatypeError
@@ -90,6 +92,12 @@ data PreparedExactDatatype = PreparedExactDatatype
     !(NonEmpty PreparedExactDatatypeFact)
     !DatatypeCompilationDescriptor
 
+data CheckedExactDatatypeAuthorization =
+    CheckedExactDatatypeAuthorization
+        !DatatypeCompilationDescriptor
+        !ObjectId
+        !(NonEmpty ObjectId)
+
 preparedExactDatatypeObjects
     :: PreparedExactDatatype
     -> NonEmpty (ObjectId, CoreType)
@@ -124,44 +132,56 @@ preparedExactDatatypeDescriptor
         (PreparedExactDatatype _location _syntax _objects _facts descriptor) =
     descriptor
 
-commitPreparedExactDatatype
+lowerPreparedExactDatatype
     :: PreparedExactDatatype
     -> Declaration.ModuleDriver failure
-        ((), Declaration.CommittedDeclarationBatch)
-commitPreparedExactDatatype
+        (Either
+            Declaration.DeclarationError
+            (Declaration.CheckedDeclaration
+                CheckedExactDatatypeAuthorization))
+lowerPreparedExactDatatype
         (PreparedExactDatatype _location syntax objects facts descriptor) =
-    Declaration.commitCompiledDeclaration syntax do
-        traverse_ addObject objects
-        candidates <-
-            Declaration.reserveFrozenPropositionCandidateBatch
-                (fmap candidateInput facts)
-        let carrier :| constructors = fmap objectIdentity objects
-        Declaration.authorizeCompiledDeclaration
-            (Declaration.authorizeDatatypeCompilationCandidates
-                descriptor
-                carrier
-                (case constructors of
-                    firstConstructor : remainingConstructors ->
-                        firstConstructor :| remainingConstructors
-                    [] ->
-                        impossible
-                            "a prepared datatype has no constructor")
-                candidates)
+    do
+        prepared <-
+            traverse
+                (\(PreparedExactDatatypeFact marker target _reference) ->
+                    Declaration.prepareFrozenCandidateSpecDriver
+                        assertedObjects
+                        target
+                        SearchEligible
+                        [markerAlias marker])
+                facts
+        pure (buildChecked <$> sequence prepared)
   where
-    addObject
-            (PreparedDatatypeObject
-                _symbol key _coreType identity asserted) = do
-        Declaration.addDeclarationObject asserted
-        Declaration.stageSemanticGlobalBinding
-            key
-            (GlobalReference identity)
-
-    candidateInput
-            (PreparedExactDatatypeFact marker target _reference) =
-        ( target
-        , SearchEligible
-        , [markerAlias marker]
-        )
+    assertedObjects =
+        toList
+            (fmap
+                (\(PreparedDatatypeObject
+                        _symbol _key _coreType _identity asserted) -> asserted)
+                objects)
+    bindings =
+        toList
+            (fmap
+                (\(PreparedDatatypeObject
+                        _symbol key _coreType identity _asserted) ->
+                    semanticGlobalBinding key (GlobalReference identity))
+                objects)
+    carrier :| constructors = fmap objectIdentity objects
+    constructorIds =
+        case constructors of
+            firstConstructor : remainingConstructors ->
+                firstConstructor :| remainingConstructors
+            [] -> impossible "a prepared datatype has no constructor"
+    buildChecked specs =
+        Declaration.checkedCompiledDeclaration
+            syntax
+            assertedObjects
+            []
+            bindings
+            []
+            [specs]
+            (CheckedExactDatatypeAuthorization
+                descriptor carrier constructorIds)
 
     markerAlias (Internal.Marker name) = semanticName name
 
@@ -170,6 +190,21 @@ commitPreparedExactDatatype
                 _symbol _key _coreType identity _asserted) =
         identity
 
+authorizeCheckedExactDatatype
+    :: CheckedExactDatatypeAuthorization
+    -> [NonEmpty Declaration.ReservedCandidate]
+    -> Declaration.Declaration ()
+authorizeCheckedExactDatatype
+        (CheckedExactDatatypeAuthorization descriptor carrier constructors) =
+    \case
+        [candidates] ->
+            Declaration.authorizeDatatypeCompilationCandidates
+                descriptor carrier constructors candidates
+        stages ->
+            Declaration.failDeclaration
+                (Declaration.CheckedDeclarationCandidateShapeMismatch
+                    1 (length stages))
+
 data ExactDatatypeError
     = ExactDatatypeUnsupportedBlock !Location
     | ExactDatatypeOccurrenceCountMismatch !Location !Int !Int