Restore quantified terms in proposition contexts

2 files changed, 401 insertions, 13 deletions

diff --git a/source/Test/Unit/Declaration.hs b/source/Test/Unit/Declaration.hs
index 4c8c3f0..074576a 100644
--- a/source/Test/Unit/Declaration.hs
+++ b/source/Test/Unit/Declaration.hs
@@ -68,6 +68,8 @@ unitTests =
             elaboratesScopedExactPropositions
         , testCase "lowers fixed equality aliases without global support"
             lowersFixedEqualityAliases
+        , testCase "scopes quantified proposition terms"
+            scopesQuantifiedPropositionTerms
         , testCase "prepares exact claim envelopes"
             preparesExactClaimEnvelopes
         , testCase "lowers exact separation comprehensions"
@@ -2084,6 +2086,238 @@ lowersFixedEqualityAliases = do
             assertFailure
                 ("internal fixed verb failed: " <> show failure)
 
+scopesQuantifiedPropositionTerms :: Assertion
+scopesQuantifiedPropositionTerms = do
+    fixture <- makeNamedFixture "quantified-proposition-terms"
+    let x = Raw.NamedVar "x"
+        y = Raw.NamedVar "y"
+        term variable = Raw.TermExpr (Raw.ExprVar variable)
+        zero = Raw.TermExpr (Raw.ExprInteger Nowhere 0)
+        setNoun = Raw.Noun Nowhere Lexicon.builtinSetNoun []
+        setPhrase named = Raw.NounPhrase [] setNoun named [] Nothing
+        quantified quantifier variable =
+            Raw.TermQuantified
+                quantifier Nowhere (setPhrase (Just variable))
+        equalityVerb argument =
+            Raw.Verb Nowhere Lexicon.builtinEqualityVerb [argument]
+        equalityAdjective argument =
+            Raw.Adj
+                Nowhere Lexicon.builtinEqualityRightAdjective [argument]
+        equality left right = Core.CEq Core.TySet left right
+        notP proposition = Core.CImp proposition Core.CFalsum
+        andP left right = notP (Core.CImp left (notP right))
+        existsP body = notP (Core.CForall Core.TySet (notP body))
+        truth = Core.CImp Core.CFalsum Core.CFalsum
+        member left right =
+            Core.CApp
+                (Core.CApp (Core.CIntrinsic Core.Member) left)
+                right
+        soleSubject =
+            Raw.StmtNoun
+                (quantified Raw.Universally x :| [])
+                (setPhrase Nothing)
+        explicitSubject =
+            Raw.SymbolicQuantified
+                Nowhere Raw.Universally (x :| []) Raw.Unbounded Nothing
+                (Raw.StmtNoun (term x :| []) (setPhrase Nothing))
+        multipleSubjects =
+            Raw.StmtVerbPhrase
+                ( quantified Raw.Universally x
+                    :| [quantified Raw.Existentially y]
+                )
+                (Raw.VPVerb (equalityVerb zero))
+        adjectiveArgument =
+            Raw.StmtVerbPhrase
+                (zero :| [])
+                (Raw.VPAdj
+                    (equalityAdjective
+                        (quantified Raw.Universally x) :| []))
+        nounArgument =
+            Raw.StmtNoun
+                (zero :| [])
+                (Raw.NounPhrase
+                    []
+                    (Raw.Noun
+                        Nowhere Lexicon.builtinElementNoun
+                        [quantified Raw.Universally x])
+                    Nothing [] Nothing)
+        negatedSubject =
+            Raw.StmtVerbPhrase
+                (quantified Raw.Universally x :| [])
+                (Raw.VPVerbNot (equalityVerb zero))
+        negatedArgument =
+            Raw.StmtVerbPhrase
+                (zero :| [])
+                (Raw.VPVerbNot
+                    (equalityVerb (quantified Raw.Universally x)))
+        negatedStatement =
+            Raw.StmtNeg Nowhere soleSubject
+        siblingConstraints =
+            Raw.StmtNoun
+                (zero :| [])
+                (Raw.NounPhrase
+                    []
+                    (Raw.Noun
+                        Nowhere Lexicon.builtinElementNoun
+                        [quantified Raw.Universally x])
+                    Nothing
+                    [Raw.AdjR
+                        Nowhere Lexicon.builtinEqualityRightAdjective
+                        [quantified Raw.Universally y]]
+                    Nothing)
+        constrainedSubject =
+            Raw.TermQuantified Raw.Universally Nowhere
+                (Raw.NounPhrase
+                    []
+                    (Raw.Noun
+                        Nowhere Lexicon.builtinElementNoun [term x])
+                    (Just x)
+                    [Raw.AdjR
+                        Nowhere Lexicon.builtinEqualityRightAdjective [term x]]
+                    (Just
+                        (Raw.StmtVerbPhrase
+                            (term x :| [])
+                            (Raw.VPVerb (equalityVerb (term x))))))
+        constrainedStatement =
+            Raw.StmtVerbPhrase
+                (constrainedSubject :| [])
+                (Raw.VPVerb (equalityVerb (term x)))
+        xEqualsX = equality (Core.CBound 0) (Core.CBound 0)
+        cases =
+            [ ( "sole quantified subject"
+              , soleSubject
+              , Core.CForall Core.TySet truth
+              )
+            , ( "explicit sole quantified subject"
+              , explicitSubject
+              , Core.CForall Core.TySet truth
+              )
+            , ( "multiple quantified subjects"
+              , multipleSubjects
+              , Core.CForall Core.TySet
+                    (existsP
+                        (andP
+                            (equality
+                                (Core.CBound 1) (Core.COpaqueInteger 0))
+                            (equality
+                                (Core.CBound 0) (Core.COpaqueInteger 0))))
+              )
+            , ( "quantified adjective argument"
+              , adjectiveArgument
+              , Core.CForall Core.TySet
+                    (equality (Core.COpaqueInteger 0) (Core.CBound 0))
+              )
+            , ( "quantified noun argument"
+              , nounArgument
+              , Core.CForall Core.TySet
+                    (member (Core.COpaqueInteger 0) (Core.CBound 0))
+              )
+            , ( "quantified subject outside negation"
+              , negatedSubject
+              , Core.CForall Core.TySet
+                    (notP
+                        (equality
+                            (Core.CBound 0) (Core.COpaqueInteger 0)))
+              )
+            , ( "quantified argument inside negation"
+              , negatedArgument
+              , notP
+                    (Core.CForall Core.TySet
+                        (equality
+                            (Core.COpaqueInteger 0) (Core.CBound 0)))
+              )
+            , ( "statement recursion bounds a quantified subject"
+              , negatedStatement
+              , notP (Core.CForall Core.TySet truth)
+              )
+            , ( "sibling constraints own their argument quantifiers"
+              , siblingConstraints
+              , andP
+                    (Core.CForall Core.TySet
+                        (member
+                            (Core.COpaqueInteger 0)
+                            (Core.CBound 0)))
+                    (Core.CForall Core.TySet
+                        (equality
+                            (Core.COpaqueInteger 0)
+                            (Core.CBound 0)))
+              )
+            , ( "quantified noun constraints share their binder"
+              , constrainedStatement
+              , Core.CForall Core.TySet
+                    (Core.CImp
+                        (andP
+                            (member (Core.CBound 0) (Core.CBound 0))
+                            (andP xEqualsX xEqualsX))
+                        xEqualsX)
+              )
+            ]
+        prepare context statement =
+            Exact.prepareExactProposition context statement
+    activeContext <- expectRight
+        (Exact.extendExactBinderContext
+            ((Exact.exactLocalId 0, x) :| [])
+            Exact.emptyExactBinderContext)
+    let action
+            :: Declaration.ModuleDriver Text
+                ( [ Either
+                        Exact.ExactCompileError
+                        Exact.PreparedExactProposition
+                  ]
+                , Either
+                    Exact.ExactCompileError
+                    Exact.PreparedExactProposition
+                )
+        action =
+            Declaration.runProspectiveLoweringDriver do
+                compiled <- traverse
+                    (\(_label, statement, _expected) ->
+                        prepare Exact.emptyExactBinderContext statement)
+                    cases
+                collision <- prepare activeContext soleSubject
+                pure (compiled, collision)
+    runDriver fixture action >>= \case
+        Declaration.DriverSucceeded
+                (compiled, collision) _interface _prefix _closure -> do
+            for_ (zip cases compiled) \
+                    ((label, _statement, expected), result) ->
+                case result of
+                    Right prepared ->
+                        assertEqual label expected
+                            (Core.scopedCoreTerm
+                                (Exact.preparedExactPropositionCore prepared))
+                    Left failure ->
+                        assertFailure
+                            (label <> " failed: "
+                                <> Text.unpack
+                                    (Exact.renderExactCompileError failure))
+            case collision of
+                Left (Exact.ExactDuplicateLocalBinder _location variable) ->
+                    assertEqual "quantified binder collision" x variable
+                Left failure ->
+                    assertFailure
+                        ("unexpected quantified-binder collision: "
+                            <> Text.unpack
+                                (Exact.renderExactCompileError failure))
+                Right{} ->
+                    assertFailure "an active quantified binder was shadowed"
+            case compiled of
+                Right sole : Right explicit : _ ->
+                    assertEqual
+                        "sole-subject lowering remains byte-for-byte identical"
+                        (Exact.preparedExactPropositionCore sole)
+                        (Exact.preparedExactPropositionCore explicit)
+                _ ->
+                    assertFailure
+                        "sole-subject equality comparison did not compile"
+        Declaration.DriverFailed failure _prefix ->
+            assertFailure
+                ("quantified proposition-term driver failed: " <> show failure)
+        Declaration.DriverSealFailed failure _prefix ->
+            assertFailure
+                ("quantified proposition-term driver did not seal: "
+                    <> show failure)
+
 preparesExactClaimEnvelopes :: Assertion
 preparesExactClaimEnvelopes = do
     fixture <- makeNamedFixture "exact-claim-envelope"
diff --git a/source/Test/Unit/Module.hs b/source/Test/Unit/Module.hs
index adb56d9..1564d5a 100644
--- a/source/Test/Unit/Module.hs
+++ b/source/Test/Unit/Module.hs
@@ -120,7 +120,7 @@ unitTests =
             compilesExactRelationExpressions
         , testCase "resolves source-owned set application"
             resolvesSourceOwnedApplication
-        , testCase "confines quantified terms to exact statement subjects"
+        , testCase "scopes quantified terms in proposition contexts"
             confinesExactQuantifiedTerms
         , testCase "compiles exact ordinary proofs"
             compilesExactOrdinaryProofs
@@ -2007,36 +2007,190 @@ confinesExactQuantifiedTerms = do
                         explicit
                         quantified
 
+                    propositionWorkspace <- parseFinalExactWorkspace
+                        prelude mounts
+                        "test/phase5/exact-quantified-proposition-terms.tex"
+                    observations <- newIORef []
+                    let observingResolver =
+                            Declaration.vampireResolver \prepared -> do
+                                let problem =
+                                        Provers.preparedTypedProverLogicalProblem
+                                            prepared
+                                    request =
+                                        Provers.preparedTypedProverRequest
+                                            prepared
+                                modifyIORef' observations
+                                    (<> [ ( Provers.preparedVerificationRequestId
+                                                request
+                                           , Backend.supportedPropositionTerm
+                                                (Backend.typedProblemClaim problem)
+                                           , Backend.typedProblemRoute problem
+                                           , Backend.typedProblemAuxiliaryTag
+                                                <$> Vector.toList
+                                                    (Backend.typedProblemAuxiliaries
+                                                        problem)
+                                           )
+                                        ])
+                                runNoLoggingT
+                                    (Provers.runPreparedTypedProver
+                                        prover prepared)
+                    freshModules <-
+                        compileFinalParsedWorkspaceWithResolver
+                            foundation prelude observingResolver
+                            propositionWorkspace
+                    freshRoot <- case reverse freshModules of
+                        rootModule : _ -> pure rootModule
+                        [] ->
+                            assertFailure
+                                "quantified proposition-term root is absent"
+                                >> fail "unreachable"
+                    let member left right =
+                            Core.CApp
+                                (Core.CApp
+                                    (Core.CIntrinsic Core.Member) left)
+                                right
+                        memberAtX =
+                            member (Core.CBound 0) (Core.CBound 1)
+                        expectedFunctionTarget =
+                            Core.CForall Core.TySet
+                                (Core.CEq Core.TySet
+                                    (Core.CBound 0)
+                                    (Core.CBound 0))
+                        expectedVerbRequestTarget =
+                            Core.CForall Core.TySet
+                                (Core.CImp memberAtX memberAtX)
+                        expectedVerbProposition =
+                            Core.CForall Core.TySet
+                                (Core.CForall Core.TySet
+                                    (Core.CImp memberAtX memberAtX))
+                        expectedTargets =
+                            [ expectedFunctionTarget
+                            , expectedVerbRequestTarget
+                            ]
+                        ordinaryImplicitAuxiliaries =
+                            [ Foundation.EmptyCharacteristic
+                            , Foundation.PairSetCharacteristic
+                            , Foundation.FamilyUnionCharacteristic
+                            , Foundation.PowerSetCharacteristic
+                            ]
+                    freshObservations <- readIORef observations
+                    assertEqual
+                        "nested function and verb terms have exact FOF targets"
+                        [ ( target
+                          , Backend.RouteFof
+                          , ordinaryImplicitAuxiliaries
+                          )
+                        | target <- expectedTargets
+                        ]
+                        [ (target, route, auxiliaries)
+                        | (_request, target, route, auxiliaries) <-
+                            freshObservations
+                        ]
+                    functionTarget <- checkedPropositionTermByAlias freshRoot
+                        "phase5_quantified_function_argument"
+                    verbTarget <- checkedPropositionTermByAlias freshRoot
+                        "phase5_quantified_verb_argument"
+                    assertEqual "nested function proposition core"
+                        expectedFunctionTarget
+                        (Core.frozenCoreTerm functionTarget)
+                    assertEqual "nested verb proposition core"
+                        expectedVerbProposition
+                        (Core.frozenCoreTerm verbTarget)
+                    let proofRecords moduleValue =
+                            concatMap
+                                Declaration.committedBatchProofValidations
+                                (Declaration.pendingModulePrefixBatches
+                                    (Module.sealedTypedModulePrefix moduleValue))
+                        proofAuthorizations moduleValue =
+                            Authority.validationDirectAuthorization
+                                . Semantic.proofValidationRecordCertificate
+                                <$> proofRecords moduleValue
+                    case proofAuthorizations freshRoot of
+                        [ Authority.CheckedSourceProof [_functionRequest]
+                          , Authority.CheckedSourceProof [_verbRequest]
+                          ] -> pure ()
+                        authorizations ->
+                            assertFailure
+                                ("unexpected quantified-term authority: "
+                                    <> show authorizations)
+                    assertBool
+                        "quantified terms add no escape-backed authority"
+                        (all
+                            ((== Authority.cleanAuthoritySafety)
+                                . Authority.factAuthoritySafety
+                                . Semantic.semanticFactAuthority)
+                            (concatMap
+                                (Semantic.declarationDeltaFacts
+                                    . Declaration.committedBatchDelta)
+                                (Declaration.pendingModulePrefixBatches
+                                    (Module.sealedTypedModulePrefix freshRoot))))
+
+                    traverse_
+                        (expectRightIO
+                            . Store.writePendingModulePrefix store
+                            . Module.sealedTypedModulePrefix)
+                        freshModules
+                    let validation =
+                            Declaration.WarmValidation
+                                (Declaration.validationLookup
+                                    (expectRightIO
+                                        . Store.loadProofValidation store)
+                                    (expectRightIO
+                                        . Store.loadDeclarationValidation store))
+                    warmModules <-
+                        compileParsedWorkspaceWithReadiness
+                            foundation
+                            (Module.finalPreludeReadiness prelude)
+                            unusedResolver
+                            validation
+                            propositionWorkspace
+                    warmRoot <- case reverse warmModules of
+                        rootModule : _ -> pure rootModule
+                        [] ->
+                            assertFailure
+                                "warm quantified proposition-term root is absent"
+                                >> fail "unreachable"
+                    assertEqual "fresh and warm quantified semantic interface"
+                        (Module.sealedTypedModuleSemantic freshRoot)
+                        (Module.sealedTypedModuleSemantic warmRoot)
+                    assertEqual "fresh and warm quantified request authority"
+                        (proofAuthorizations freshRoot)
+                        (proofAuthorizations warmRoot)
+                    assertEqual "fresh and warm quantified prefix"
+                        (Declaration.pendingModulePrefixCurrent
+                            (Module.sealedTypedModulePrefix freshRoot))
+                        (Declaration.pendingModulePrefixCurrent
+                            (Module.sealedTypedModulePrefix warmRoot))
+
     negative <-
-        withAcceptedFixtureVampire "felix-exact-quantified-subject-nested"
+        withAcceptedFixtureVampire "felix-exact-quantified-term-valued"
             \prover ->
                 runNoLoggingT
                     (Api.verifyMeasured
                         prover
-                        "test/phase5/exact-quantified-subject-nested.tex")
+                        "test/phase5/exact-quantified-term-valued.tex")
     case negative of
         Right
             ( Api.VerificationCheckingFailure _report
                 (Api.VerificationTypedModuleError
                 _source
                 (Module.TypedActionFailed
-                    (Module.TypedExactProofFailed
-                        (ExactProof.ExactProofElaborationFailed
-                            (Exact.ExactQuantifiedTermRequiresStatementSubject
-                                location))))
+                    (Module.TypedExactCompileFailed
+                        (Exact.ExactQuantifiedTermRequiresPropositionContext
+                            location)))
                 prefix)
             , _measurements
             ) -> do
-            assertEqual "nested quantified term line" 8 (locLine location)
-            assertEqual "earlier exact definition remains committed"
-                1
-                (length (Declaration.pendingModulePrefixBatches prefix))
+            assertEqual "term-valued quantified term line"
+                2 (locLine location)
+            assertBool "failed term-valued abbreviation publishes no prefix"
+                (null (Declaration.pendingModulePrefixBatches prefix))
         Left failure ->
             assertFailure
-                ("unexpected nested quantified-term failure: "
+                ("unexpected term-valued quantified-term failure: "
                     <> show failure)
         Right{} ->
-            assertFailure "nested quantified exact term was admitted"
+            assertFailure "term-valued quantified exact term was admitted"
 compilesExactOrdinaryProofs :: Assertion
 compilesExactOrdinaryProofs =
     Temp.withSystemTempDirectory "felix-exact-proofs" \root -> do