Activate exact order checking

3 files changed, 91 insertions, 1 deletions

diff --git a/source/Felix/Migration.hs b/source/Felix/Migration.hs
index 15bf3a5..7596e26 100644
--- a/source/Felix/Migration.hs
+++ b/source/Felix/Migration.hs
@@ -184,6 +184,7 @@ phase53LibraryMigrationModules =
         , migrationLibraryModule "set/fixpoint.tex"
         , migrationLibraryModule "set/equinumerosity.tex"
         , migrationLibraryModule "order/quasiorder.tex"
+        , migrationLibraryModule "order/order.tex"
         ]
 
 -- | Sources whose complete graphs may enter the typed driver.
diff --git a/source/Test/Unit/Migration.hs b/source/Test/Unit/Migration.hs
index 9bfacad..5f27721 100644
--- a/source/Test/Unit/Migration.hs
+++ b/source/Test/Unit/Migration.hs
@@ -139,6 +139,12 @@ selectsCompleteGraphDriver = do
         , ( "order/quasiorder.tex"
           , ["relation.tex", "relation/properties.tex"]
           )
+        , ( "order/order.tex"
+          , [ "relation.tex"
+            , "relation/properties.tex"
+            , "order/quasiorder.tex"
+            ]
+          )
         ]
         \(path, expectedImports) -> do
             (phase53, _phase53Measurements) <-
diff --git a/source/Test/Unit/Module.hs b/source/Test/Unit/Module.hs
index b7fb85d..2864c33 100644
--- a/source/Test/Unit/Module.hs
+++ b/source/Test/Unit/Module.hs
@@ -1121,6 +1121,68 @@ checksPhase53LibraryClosures = do
                         assertNoLocalFactEscapeKind
                             quasiorderModule Authority.Omitted
                         assertNoLocalSourceAxiom quasiorderModule
+                checkRoot "order/order.tex"
+                    \moduleAt -> do
+                        (_relationParsed, relationModule) <-
+                            moduleAt "relation.tex"
+                        (_propertiesParsed, propertiesModule) <-
+                            moduleAt "relation/properties.tex"
+                        (_quasiorderParsed, quasiorderModule) <-
+                            moduleAt "order/quasiorder.tex"
+                        (_orderParsed, orderModule) <-
+                            moduleAt "order/order.tex"
+                        assertEqual "order semantic imports"
+                            [ preludeSemanticId
+                            , semanticId relationModule
+                            , semanticId propertiesModule
+                            , semanticId quasiorderModule
+                            ]
+                            (Semantic.semanticInterfaceDirectInputs
+                                (Module.sealedTypedModuleSemantic orderModule))
+                        quasiorderDescriptor <- sole "quasiorder descriptor"
+                            (semanticStructureDescriptors
+                                (Module.sealedTypedModuleSemantic
+                                    quasiorderModule))
+                        orderDescriptor <- sole "order descriptor"
+                            (semanticStructureDescriptors
+                                (Module.sealedTypedModuleSemantic orderModule))
+                        assertEqual "order inherits the quasiorder descriptor"
+                            [Semantic.semanticStructureDescriptorPhrase
+                                quasiorderDescriptor]
+                            (Semantic.semanticStructureDescriptorParents
+                                orderDescriptor)
+                        assertEqual "order allocates no replacement operation"
+                            []
+                            (Semantic.semanticStructureDescriptorOperations
+                                orderDescriptor)
+                        quasiorderOperation <- sole "quasiorder operation"
+                            (Semantic.semanticStructureDescriptorOperations
+                                quasiorderDescriptor)
+                        antisymmetry <- checkedPropositionTermByAlias
+                            orderModule "orderedset_antisym"
+                        assertBool "order reuses the inherited lt object"
+                            ( Semantic.semanticStructureOperationObject
+                                quasiorderOperation
+                                `Set.member`
+                                    Core.canonicalTermGlobals
+                                        (Core.frozenCoreTerm antisymmetry)
+                            )
+                        structureDelta <-
+                            localDeltaByAlias orderModule "orderedset"
+                        assertBool "order structure facts are independently clean"
+                            (all
+                                ((== Authority.cleanAuthoritySafety)
+                                    . Authority.factAuthoritySafety
+                                    . Semantic.semanticFactAuthority)
+                                (Semantic.declarationDeltaFacts
+                                    structureDelta))
+                        assertFactAliasEscapeKind
+                            orderModule
+                            "subseteqrel_is_order"
+                            Authority.SourceAxiom
+                        assertNoLocalFactEscapeKind
+                            orderModule Authority.Omitted
+                        assertNoLocalSourceAxiom orderModule
   where
     semanticId =
         Semantic.semanticInterfaceAssertedId
@@ -1227,9 +1289,29 @@ checkedPropositionTermByAlias sealed name = do
     batch <- batchByAlias
         (Module.sealedTypedModulePrefix sealed)
         name
+    alias <- sole
+        ("semantic alias for " <> StrictText.unpack name)
+        [ candidate
+        | candidate <- Semantic.declarationDeltaAliases
+            (Declaration.committedBatchDelta batch)
+        , Semantic.semanticAliasName candidate
+            == Semantic.semanticName name
+        ]
+    occurrence <- sole
+        ("semantic fact for " <> StrictText.unpack name)
+        [ candidate
+        | candidate <- Semantic.declarationDeltaFacts
+            (Declaration.committedBatchDelta batch)
+        , Semantic.semanticFactFingerprint candidate
+            == Semantic.semanticAliasTarget alias
+        ]
     proposition <- sole
         ("checked proposition for " <> StrictText.unpack name)
-        (Declaration.committedBatchPropositions batch)
+        [ candidate
+        | candidate <- Declaration.committedBatchPropositions batch
+        , Identity.checkedPropositionId candidate
+            == Semantic.semanticFactProposition occurrence
+        ]
     pure (Identity.checkedPropositionTerm proposition)
 
 assertFactAliasEscapeKind
@@ -5491,6 +5573,7 @@ routesProductionVerification =
             , ("Cantor", "set/cantor.tex")
             , ("equinumerosity", "set/equinumerosity.tex")
             , ("quasiorder", "order/quasiorder.tex")
+            , ("order", "order/order.tex")
             ]
             \(label, path) ->
                 assertRoute ("typed " <> label)