Render checked prover problems as FOF or TH0

1 files changed, 128 insertions, 0 deletions

diff --git a/source/Test/Unit/Backend.hs b/source/Test/Unit/Backend.hs
index f1defd9..172a328 100644
--- a/source/Test/Unit/Backend.hs
+++ b/source/Test/Unit/Backend.hs
@@ -5,10 +5,14 @@ module Test.Unit.Backend (unitTests) where
 
 import Base hiding (Empty)
 import Checking.Backend.Problem
+import Checking.Backend.Tptp
 import Checking.Core
+import Provers
+import Tptp.UnsortedFirstOrder qualified as Tptp
 
 import Control.Monad (unless)
 import Data.Map.Strict qualified as Map
+import Data.Text qualified as Text
 import Data.Vector (Vector)
 import Data.Vector qualified as Vector
 import Numeric.Natural (Natural)
@@ -47,6 +51,9 @@ unitTests =
         , testCase
             "routes implicit, explicit, and local-only problems"
             routesCompleteProblems
+        , testCase
+            "renders checked FOF and TH0 problems"
+            rendersCheckedProblems
         ]
 
 classifiesPropositionEquality :: Assertion
@@ -321,6 +328,127 @@ routesCompleteProblems = do
         Right problem ->
             show (typedProblemRoute problem)
 
+rendersCheckedProblems :: Assertion
+rendersCheckedProblems = do
+    fofFrozen <- closedFrozen firstOrderClaim
+    th0Frozen <- closedFrozen higherOrderClaim
+    inventory <-
+        either
+            (assertFailure . show)
+            pure
+            (prepareTypedFactInventory
+                testGlobalType
+                [ typedBackendFactInput
+                    (0 :: Int)
+                    ("fof_fact" :| [])
+                    ("first" :: Text)
+                    fofFrozen
+                , typedBackendFactInput
+                    1
+                    ("th0_fact" :| [])
+                    "second"
+                    th0Frozen
+                ])
+    claim <-
+        checkedProposition
+            (Vector.singleton
+                (ObjectLocal, TySet))
+            (CApp
+                (CGlobal FirstOrderPredicate)
+                (CBound 0))
+    fofProblem <-
+        planned
+            inventory
+            claim
+            ImplicitFofFacts
+            FirstOrderLocals
+    th0Problem <-
+        planned
+            inventory
+            claim
+            (ExplicitFacts
+                ("th0_fact" :| []))
+            FirstOrderLocals
+    preparedFof <-
+        either
+            (assertFailure . show)
+            pure
+            (prepareTypedTptpProblem
+                fofProblem)
+    preparedTh0 <-
+        either
+            (assertFailure . show)
+            pure
+            (prepareTypedTptpProblem
+                th0Problem)
+    proverTask <-
+        either
+            (assertFailure . show)
+            pure
+            (prepareTypedProverTask
+                DirectTask
+                th0Problem)
+    assertEqual "FOF route" RouteFof
+        (preparedTypedTptpRoute preparedFof)
+    assertBool "FOF formulas"
+        ("fof(zf_h0,axiom,"
+            `Text.isInfixOf`
+                preparedTypedTptpText
+                    preparedFof)
+    assertBool "FOF has no TH0 declarations"
+        (not
+            ("thf("
+                `Text.isInfixOf`
+                    preparedTypedTptpText
+                        preparedFof))
+    assertEqual "TH0 route" RouteTh0
+        (preparedTypedTptpRoute preparedTh0)
+    assertEqual "TH0 request dialect"
+        VerificationTh0
+        (preparedVerificationDialect
+            (preparedTypedProverRequest
+                proverTask))
+    assertEqual "request preserves exact prepared text"
+        (preparedTypedTptpText preparedTh0)
+        (preparedVerificationText
+            (preparedTypedProverRequest
+                proverTask))
+    for_
+        [ "thf(zf_h0,axiom,"
+        , "^ [V0:$i]"
+        , "thf(zf_q0,conjecture,"
+        ]
+        \fragment ->
+            assertBool
+                ("TH0 contains " <> Text.unpack fragment)
+                (fragment
+                    `Text.isInfixOf`
+                        preparedTypedTptpText
+                            preparedTh0)
+    for_
+        (Map.keys
+            (preparedTypedTptpNameOrigins
+                preparedTh0))
+        \target ->
+            assertBool
+                ("valid generated name " <> Text.unpack target)
+                (if "V" `Text.isPrefixOf` target
+                    then Tptp.isProperVariable target
+                    else Tptp.isProperAtomicWord target)
+  where
+    planned inventory claim globalPolicy localPolicy =
+        either
+            (assertFailure . show)
+            pure
+            (planTypedProblem
+                testGlobalType
+                inventory
+                claim
+                []
+                []
+                globalPolicy
+                localPolicy)
+
 firstOrderClaim :: CanonicalTerm TestGlobal
 firstOrderClaim =
     CApp