summaryrefslogtreecommitdiff
path: root/source/Test/Unit/Backend.hs
diff options
context:
space:
mode:
Diffstat (limited to 'source/Test/Unit/Backend.hs')
-rw-r--r--source/Test/Unit/Backend.hs541
1 files changed, 0 insertions, 541 deletions
diff --git a/source/Test/Unit/Backend.hs b/source/Test/Unit/Backend.hs
deleted file mode 100644
index 11c36b8..0000000
--- a/source/Test/Unit/Backend.hs
+++ /dev/null
@@ -1,541 +0,0 @@
-{-# LANGUAGE NoImplicitPrelude #-}
-{-# LANGUAGE OverloadedStrings #-}
-
-module Test.Unit.Backend (unitTests) where
-
-import Base hiding (Empty)
-import Checking.Backend.Problem
-import Checking.Backend.Tptp
-import Checking.Core
-import Checking.Foundation qualified as Foundation
-import Provers
-import Tptp.UnsortedFirstOrder qualified as Tptp
-
-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)
-import Test.Tasty
-import Test.Tasty.HUnit
-
-
-data TestGlobal
- = FirstOrderPredicate
- | HigherOrderPredicate
- deriving (Show, Eq, Ord)
-
-testGlobalType :: TestGlobal -> Maybe CoreType
-testGlobalType = \case
- FirstOrderPredicate ->
- Just (TySet `TyArrow` TyProp)
- HigherOrderPredicate ->
- Just
- ((TySet `TyArrow` TyProp)
- `TyArrow` TyProp)
-
-data TestLocal
- = ObjectLocal
- | PredicateLocal
- deriving (Show, Eq, Ord)
-
-unitTests :: TestTree
-unitTests =
- testGroup "Typed backend problem"
- [ testCase
- "projects proposition equality as equivalence"
- classifiesPropositionEquality
- , testCase
- "projects exact ambient support"
- projectsExactAmbientSupport
- , testCase
- "routes implicit, explicit, and local-only problems"
- routesCompleteProblems
- , testCase
- "renders checked FOF and TH0 problems"
- rendersCheckedProblems
- ]
-
-classifiesPropositionEquality :: Assertion
-classifiesPropositionEquality = do
- proposition <-
- checkedProposition
- Vector.empty
- (CEq TyProp CFalsum CFalsum)
- capability <-
- either
- (assertFailure . show)
- pure
- (classifySupportedProposition
- testGlobalType
- proposition)
- case capability of
- FofProjectable{} ->
- pure ()
- RequiresTh0 exclusions ->
- assertFailure
- ("proposition equality was not projected: "
- <> show exclusions)
-
-projectsExactAmbientSupport :: Assertion
-projectsExactAmbientSupport = do
- let term :: CanonicalTerm Void
- term =
- CForall TySet
- (CEq TySet
- (CBound 1)
- (CBound 3))
- scoped <-
- either
- (assertFailure . show)
- pure
- (checkScopedCanonicalCore
- (const Nothing)
- [TySet, TySet, TySet]
- term)
- projected <-
- either
- (assertFailure . show)
- pure
- (projectSupportedProposition
- (const Nothing)
- (Vector.fromList
- [ (0 :: Int, TySet)
- , (1, TySet)
- , (2, TySet)
- ])
- scoped)
- assertEqual
- "unused middle support is removed"
- (Vector.fromList
- [ (0 :: Int, TySet)
- , (2, TySet)
- ])
- (supportedPropositionSupport projected)
- assertEqual
- "indices are remapped below nested binders"
- (CForall TySet
- (CEq TySet
- (CBound 1)
- (CBound 2)))
- (supportedPropositionTerm projected)
-
-routesCompleteProblems :: Assertion
-routesCompleteProblems = do
- fofFact <-
- checkedBackendFact
- (0 :: Int)
- firstOrderClaim
- th0Fact <-
- checkedBackendFact
- (1 :: Int)
- higherOrderClaim
- let fofFacts =
- Vector.singleton fofFact
- th0Facts =
- Vector.singleton th0Fact
- claim <-
- checkedProposition
- (Vector.singleton
- (ObjectLocal, TySet))
- (CApp
- (CGlobal FirstOrderPredicate)
- (CBound 0))
- firstOrderLocal <-
- checkedLocalPremise
- 0
- "first-order local"
- claim
- higherOrderLocalProposition <-
- checkedProposition
- (Vector.singleton
- (PredicateLocal,
- TySet `TyArrow` TyProp))
- (CApp
- (CGlobal HigherOrderPredicate)
- (CBound 0))
- higherOrderLocal <-
- checkedLocalPremise
- 1
- "higher-order local"
- higherOrderLocalProposition
-
- implicit <-
- planned
- fofFacts
- claim
- [higherOrderLocal, firstOrderLocal]
- []
- ImplicitFofPremises
- FirstOrderLocals
- assertEqual "implicit route" RouteFof
- (typedProblemRoute implicit)
- assertEqual "implicit FOF globals" [0]
- (typedBackendFactReference
- <$> toList
- (typedProblemGlobalPremises
- implicit))
- assertEqual "first-order local only" [0]
- (localPremiseOrdinalValue
- . typedLocalPremiseOrdinal
- <$> toList
- (typedProblemLocalPremises
- implicit))
-
- explicitFof <-
- planned
- fofFacts
- claim
- [firstOrderLocal]
- []
- ExplicitGlobalPremises
- FirstOrderLocals
- assertEqual "explicit FOF route" RouteFof
- (typedProblemRoute explicitFof)
-
- explicitTh0 <-
- planned
- th0Facts
- claim
- [firstOrderLocal]
- []
- ExplicitGlobalPremises
- FirstOrderLocals
- assertEqual "explicit TH0 route" RouteTh0
- (typedProblemRoute explicitTh0)
-
- localOnly <-
- planned
- Vector.empty
- claim
- [higherOrderLocal, firstOrderLocal]
- []
- NoGlobalPremises
- AllLocals
- assertEqual "local-only TH0 route" RouteTh0
- (typedProblemRoute localOnly)
- assertEqual "local order restored" [0, 1]
- (localPremiseOrdinalValue
- . typedLocalPremiseOrdinal
- <$> toList
- (typedProblemLocalPremises
- localOnly))
- assertEqual
- "complete ambient local inventory"
- (Map.fromList
- [ (ObjectLocal, TySet)
- , (PredicateLocal,
- TySet `TyArrow` TyProp)
- ])
- (typedProblemLocalTypes localOnly)
-
- case planTypedProblem
- testGlobalType
- Vector.empty
- claim
- [firstOrderLocal, firstOrderLocal]
- []
- NoGlobalPremises
- AllLocals of
- Left
- (TypedProblemDuplicateLocalPremiseOrdinal
- duplicateOrdinal) ->
- assertEqual
- "duplicate local ordinal"
- 0
- (localPremiseOrdinalValue
- duplicateOrdinal)
- result ->
- assertFailure
- ("expected duplicate local ordinal error, got "
- <> showProblemResult result)
-
- higherOrderClaimProposition <-
- checkedProposition
- Vector.empty
- higherOrderClaim
- case planTypedProblem
- testGlobalType
- fofFacts
- higherOrderClaimProposition
- []
- []
- ImplicitFofPremises
- FirstOrderLocals of
- Left
- TypedProblemExplicitHigherOrderJustificationRequired{} ->
- pure ()
- result ->
- assertFailure
- ("expected explicit higher-order error, got "
- <> showProblemResult result)
- checkedFoundationValue <-
- either
- (assertFailure . show)
- pure
- Foundation.checkedFoundation
- case planTypedProblem
- testGlobalType
- fofFacts
- claim
- []
- [typedFoundationAuxiliaryInput
- checkedFoundationValue
- Foundation.SeparationCharacteristic]
- ImplicitFofPremises
- FirstOrderLocals of
- Left
- TypedProblemExplicitHigherOrderJustificationRequired{} ->
- pure ()
- result ->
- assertFailure
- ("expected implicit higher-order auxiliary error, got "
- <> showProblemResult result)
- unusedContext <-
- either
- (assertFailure . show)
- pure
- (checkScopedCanonicalCore
- testGlobalType
- [TySet `TyArrow` TyProp]
- firstOrderClaim)
- case supportedProposition
- (Vector.singleton
- (PredicateLocal,
- TySet `TyArrow` TyProp))
- unusedContext of
- Left (UnusedSupportedLocal PredicateLocal) ->
- pure ()
- Left err ->
- assertFailure
- ("unexpected exact-support error: "
- <> show err)
- Right _ ->
- assertFailure
- "unused ambient local entered exact support"
- where
- planned selectedFacts claim locals auxiliaries
- globalPolicy localPolicy =
- either
- (assertFailure . show)
- pure
- (planTypedProblem
- testGlobalType
- selectedFacts
- claim
- locals
- auxiliaries
- globalPolicy
- localPolicy)
-
- showProblemResult = \case
- Left err ->
- show err
- Right problem ->
- show (typedProblemRoute problem)
-
-rendersCheckedProblems :: Assertion
-rendersCheckedProblems = do
- fofFact <-
- checkedBackendFact
- (0 :: Int)
- firstOrderClaim
- th0Fact <-
- checkedBackendFact
- (1 :: Int)
- higherOrderClaim
- claim <-
- checkedProposition
- (Vector.singleton
- (ObjectLocal, TySet))
- (CApp
- (CGlobal FirstOrderPredicate)
- (CBound 0))
- fofProblem <-
- planned
- (Vector.singleton fofFact)
- claim
- ImplicitFofPremises
- FirstOrderLocals
- th0Problem <-
- planned
- (Vector.singleton th0Fact)
- claim
- ExplicitGlobalPremises
- 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 selectedFacts claim globalPolicy localPolicy =
- either
- (assertFailure . show)
- pure
- (planTypedProblem
- testGlobalType
- selectedFacts
- claim
- []
- []
- globalPolicy
- localPolicy)
-
-firstOrderClaim :: CanonicalTerm TestGlobal
-firstOrderClaim =
- CApp
- (CGlobal FirstOrderPredicate)
- (CIntrinsic Empty)
-
-higherOrderClaim :: CanonicalTerm TestGlobal
-higherOrderClaim =
- CApp
- (CGlobal HigherOrderPredicate)
- (CLam TySet
- (CApp
- (CGlobal FirstOrderPredicate)
- (CBound 0)))
-
-checkedProposition
- :: Vector (TestLocal, CoreType)
- -> CanonicalTerm TestGlobal
- -> IO
- (SupportedProposition
- TestLocal
- TestGlobal)
-checkedProposition support term = do
- checked <-
- either
- (assertFailure . show)
- pure
- (checkScopedCanonicalCore
- testGlobalType
- (snd <$> Vector.toList support)
- term)
- either
- (assertFailure . show)
- pure
- (supportedProposition support checked)
-
-checkedClosedProposition
- :: CanonicalTerm TestGlobal
- -> IO
- (SupportedProposition
- Void
- TestGlobal)
-checkedClosedProposition term = do
- checked <-
- either
- (assertFailure . show)
- pure
- (checkScopedCanonicalCore
- testGlobalType
- []
- term)
- either
- (assertFailure . show)
- pure
- (supportedProposition
- Vector.empty
- checked)
-
-checkedBackendFact
- :: ref
- -> CanonicalTerm TestGlobal
- -> IO (TypedBackendFact ref TestGlobal)
-checkedBackendFact reference term = do
- proposition <-
- checkedClosedProposition term
- capability <-
- either
- (assertFailure . show)
- pure
- (classifySupportedProposition
- testGlobalType
- proposition)
- pure
- (typedBackendFact
- reference
- proposition
- capability)
-
-checkedLocalPremise
- :: Natural
- -> Text
- -> SupportedProposition TestLocal TestGlobal
- -> IO
- (TypedLocalPremise
- TestLocal
- Text
- TestGlobal)
-checkedLocalPremise ordinal premiseOrigin proposition =
- either
- (assertFailure . show)
- pure
- (typedLocalPremise
- testGlobalType
- (localPremiseOrdinal ordinal)
- premiseOrigin
- proposition)
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-06 18:44:22 +0000