Separate ordered tuples from PairSet

2 files changed, 100 insertions, 1 deletions

diff --git a/source/Test/Unit/Lexicon.hs b/source/Test/Unit/Lexicon.hs
index cd0a886..54b4bd4 100644
--- a/source/Test/Unit/Lexicon.hs
+++ b/source/Test/Unit/Lexicon.hs
@@ -43,7 +43,7 @@ retainsBaseMixfixGrouping =
             (fmap (fmap canonicalEntryShape) baseSyntaxManifest)
         assertEqual
             "cache-epoch base syntax identity"
-            "96d03072c3d395185ef9dee2f783f49afecdb177bb68930e302f4611e97397b1"
+            "97acdc8153821b20dd0f45cf9d44870705723bb60737f7bacbb9ac31a98987a5"
             (cacheDigestHex
                 (baseSyntaxInterfaceIdDigest
                     baseSyntaxInterfaceId))
@@ -319,6 +319,7 @@ expectedBaseRows =
       , ("abs", NonAssoc)
       , ("cons", NonAssoc)
       , ("pair", NonAssoc)
+      , ("upair", NonAssoc)
       ]
     , [ ("emptyset", NonAssoc)
       , ("naturals", NonAssoc)
diff --git a/source/Test/Unit/Module.hs b/source/Test/Unit/Module.hs
index b8a7854..9cec861 100644
--- a/source/Test/Unit/Module.hs
+++ b/source/Test/Unit/Module.hs
@@ -413,6 +413,25 @@ buildsConfinedFinalPrelude = do
                     ]
                     `Set.isSubsetOf` foundationTags
                 )
+            pairsetBatch <- batchByAlias
+                (FinalPrelude.finalPreludePrefix candidate)
+                "pairset_iff"
+            pairsetFact <- sole "pairset foundation fact"
+                (Semantic.declarationDeltaFacts
+                    (Declaration.committedBatchDelta pairsetBatch))
+            assertEqual "pairset foundation safety"
+                Authority.cleanAuthoritySafety
+                (Authority.factAuthoritySafety
+                    (Semantic.semanticFactAuthority pairsetFact))
+            pairsetValidation <- sole "pairset foundation validation"
+                (Declaration.committedBatchProofValidations pairsetBatch)
+            assertEqual "pairset exact foundation authority"
+                (Authority.CheckedKernelConstruction
+                    (Authority.FoundationLeaf
+                        Foundation.PairSetCharacteristic))
+                (Authority.validationDirectAuthorization
+                    (Semantic.proofValidationRecordCertificate
+                        pairsetValidation))
         FinalPrelude.FinalPreludeBuildFailed failure prefix ->
             assertFailure
                 ("final prelude failed after "
@@ -567,8 +586,19 @@ checksProtectedNatClosure = do
                 ]
             assertTransparentObjectAlias setModule "cons"
             assertTransparentObjectAlias setModule "union"
+            assertOpaqueObjectKey
+                setModule
+                "pair"
+                (Semantic.SemanticExpressionFunction
+                    (Raw.mixfixPattern Raw.PairSymbol))
             assertCleanFactAlias setModule "cons_iff"
             assertCleanFactAlias setModule "union_iff"
+            traverse_
+                (assertSourceAxiomAlias setModule)
+                [ "pair_eq_iff"
+                , "fst_eq"
+                , "snd_eq"
+                ]
             assertBool "protected checking exercised Vampire"
                 . (> 0)
                 =<< readIORef runs
@@ -600,6 +630,27 @@ assertTransparentObjectAlias sealed name = do
         Identity.TransparentObject
         (Identity.objectIdFamily target)
 
+assertOpaqueObjectKey
+    :: Module.SealedTypedModule
+    -> Text
+    -> Semantic.SemanticGlobalKey
+    -> Assertion
+assertOpaqueObjectKey sealed name key = do
+    binding <- sole
+        ("semantic binding for " <> StrictText.unpack name)
+        [ candidate
+        | delta <- localSemanticDeltas sealed
+        , candidate <- Semantic.semanticEnvironmentBindings
+            (Semantic.declarationDeltaEnvironment delta)
+        , Semantic.semanticGlobalBindingKey candidate == key
+        ]
+    let target = Semantic.semanticGlobalTargetObject
+            (Semantic.semanticGlobalBindingTarget binding)
+    assertEqual
+        ("opaque object for " <> StrictText.unpack name)
+        Identity.OpaqueObject
+        (Identity.objectIdFamily target)
+
 localObjectAliasTarget
     :: Module.SealedTypedModule
     -> Text
@@ -640,6 +691,53 @@ assertCleanFactAlias sealed name = do
         (Authority.factAuthoritySafety
             (Semantic.semanticFactAuthority fact))
 
+assertSourceAxiomAlias
+    :: Module.SealedTypedModule
+    -> Text
+    -> Assertion
+assertSourceAxiomAlias sealed name = do
+    batch <- batchByAlias
+        (Module.sealedTypedModulePrefix sealed)
+        name
+    fact <- sole
+        ("source axiom fact " <> StrictText.unpack name)
+        (Semantic.declarationDeltaFacts
+            (Declaration.committedBatchDelta batch))
+    assertEqual
+        ("source axiom safety for " <> StrictText.unpack name)
+        (Authority.authoritySafety
+            (Authority.singletonEscapeKind Authority.SourceAxiom))
+        (Authority.factAuthoritySafety
+            (Semantic.semanticFactAuthority fact))
+    validation <- maybe
+        (assertFailure
+            ("source axiom validation for " <> StrictText.unpack name)
+            >> fail "unreachable")
+        pure
+        (Declaration.committedBatchDeclarationValidation batch)
+    certificate <- sole
+        ("source axiom certificate for " <> StrictText.unpack name)
+        (Semantic.declarationValidationRecordCertificates validation)
+    assertEqual
+        ("source axiom authority for " <> StrictText.unpack name)
+        Authority.SourceAxiomAuthorization
+        (Authority.validationDirectAuthorization certificate)
+
+batchByAlias
+    :: Declaration.PendingModulePrefix
+    -> Text
+    -> IO Declaration.CommittedDeclarationBatch
+batchByAlias prefix name =
+    sole
+        ("declaration batch for " <> StrictText.unpack name)
+        [ batch
+        | batch <- Declaration.pendingModulePrefixBatches prefix
+        , alias <- Semantic.declarationDeltaAliases
+            (Declaration.committedBatchDelta batch)
+        , Semantic.semanticAliasName alias
+            == Semantic.semanticName name
+        ]
+
 localDeltaByAlias
     :: Module.SealedTypedModule
     -> Text