Authorize exact datatype families

1 files changed, 47 insertions, 0 deletions

diff --git a/source/Checking/Exact/Datatype.hs b/source/Checking/Exact/Datatype.hs
index e10161d..8e0b907 100644
--- a/source/Checking/Exact/Datatype.hs
+++ b/source/Checking/Exact/Datatype.hs
@@ -14,6 +14,7 @@ module Checking.Exact.Datatype
     , preparedExactDatatypeFactReference
     , preparedExactDatatypeDescriptor
     , prepareExactDatatype
+    , commitPreparedExactDatatype
     , ExactDatatypeError(..)
     , exactDatatypeErrorLocation
     , renderExactDatatypeError
@@ -123,6 +124,52 @@ preparedExactDatatypeDescriptor
         (PreparedExactDatatype _location _syntax _objects _facts descriptor) =
     descriptor
 
+commitPreparedExactDatatype
+    :: PreparedExactDatatype
+    -> Declaration.ModuleDriver failure
+        ((), Declaration.CommittedDeclarationBatch)
+commitPreparedExactDatatype
+        (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)
+  where
+    addObject
+            (PreparedDatatypeObject
+                _symbol key _coreType identity asserted) = do
+        traverse_ Declaration.addDeclarationObject asserted
+        Declaration.stageSemanticGlobalBinding
+            key
+            (GlobalReference identity)
+
+    candidateInput
+            (PreparedExactDatatypeFact marker target _reference) =
+        ( target
+        , SearchEligible
+        , [markerAlias marker]
+        )
+
+    markerAlias (Internal.Marker name) = semanticName name
+
+    objectIdentity
+            (PreparedDatatypeObject
+                _symbol _key _coreType identity _asserted) =
+        identity
+
 data ExactDatatypeError
     = ExactDatatypeUnsupportedBlock !Location
     | ExactDatatypeOccurrenceCountMismatch !Location !Int !Int