summaryrefslogtreecommitdiff
path: root/source/Checking
diff options
context:
space:
mode:
Diffstat (limited to 'source/Checking')
-rw-r--r--source/Checking/Core.hs47
-rw-r--r--source/Checking/Exact.hs153
-rw-r--r--source/Checking/Exact/Proof.hs272
3 files changed, 385 insertions, 87 deletions
diff --git a/source/Checking/Core.hs b/source/Checking/Core.hs
index 4b7478f..f8466af 100644
--- a/source/Checking/Core.hs
+++ b/source/Checking/Core.hs
@@ -58,6 +58,7 @@ module Checking.Core
, closeScopedExists
, openScopedForall
, openScopedImplication
+ , openScopedAssumption
, closeScopedCore
, instantiateCanonical
, mapCanonicalGlobals
@@ -1058,6 +1059,52 @@ openScopedImplication
openScopedImplication _scoped =
Nothing
+-- | Open a checked proof assumption against the current goal. Besides a
+-- direct implication antecedent, the source language historically permits
+-- either immediate side of one binary conjunction antecedent to be assumed
+-- first. The other side remains the next implication antecedent. This is a
+-- deliberately shallow structural rule: it neither flattens conjunctions nor
+-- treats disjunction as an eliminable assumption.
+openScopedAssumption
+ :: Eq global
+ => ScopedCheckedCore global
+ -> ScopedCheckedCore global
+ -> Maybe
+ ( ScopedCheckedCore global
+ , ScopedCheckedCore global
+ )
+openScopedAssumption supplied goal = do
+ (antecedent, conclusion) <- openScopedImplication goal
+ if supplied == antecedent
+ then pure (antecedent, conclusion)
+ else do
+ (left, right) <- splitScopedConjunction antecedent
+ if supplied == left
+ then do
+ remaining <- implyScopedCore right conclusion
+ pure (left, remaining)
+ else if supplied == right
+ then do
+ remaining <- implyScopedCore left conclusion
+ pure (right, remaining)
+ else Nothing
+
+splitScopedConjunction
+ :: ScopedCheckedCore global
+ -> Maybe
+ ( ScopedCheckedCore global
+ , ScopedCheckedCore global
+ )
+splitScopedConjunction
+ (ScopedCheckedCore context TyProp
+ (CImp (CImp left (CImp right CFalsum)) CFalsum)) =
+ Just
+ ( ScopedCheckedCore context TyProp left
+ , ScopedCheckedCore context TyProp right
+ )
+splitScopedConjunction _scoped =
+ Nothing
+
closeScopedCore
:: ScopedCheckedCore global
-> Maybe (FrozenCheckedCore global)
diff --git a/source/Checking/Exact.hs b/source/Checking/Exact.hs
index c4b90c7..1788224 100644
--- a/source/Checking/Exact.hs
+++ b/source/Checking/Exact.hs
@@ -9,11 +9,15 @@ module Checking.Exact
, ExactBinderContext
, emptyExactBinderContext
, extendExactBinderContext
+ , extendExactAnonymousBinderContext
, exactBinderContextSupport
, exactBinderContextIndex
, PreparedExactProposition
, preparedExactPropositionCore
, prepareExactProposition
+ , prepareExactSymbolicBoundConstraints
+ , prepareExactSymbolicWitnessConstraints
+ , prepareExactNounWitnessConstraints
, PreparedExactSetExpression
, preparedExactSetExpressionCore
, prepareExactSetExpression
@@ -95,7 +99,7 @@ exactLocalIdValue (ExactLocalId value) = value
data ExactBinder = ExactBinder
!ExactLocalId
- !Raw.VarSymbol
+ !(Maybe Raw.VarSymbol)
!CoreType
!(Maybe ExactStructureAnnotation)
@@ -123,14 +127,33 @@ extendExactBinderContext additions (ExactBinderContext initial) =
| any (sameIdentity identity) binders =
Left (ExactDuplicateLocalIdentity (locate variable) identity)
| otherwise =
- Right (ExactBinder identity variable TySet Nothing : binders)
+ Right (ExactBinder identity (Just variable) TySet Nothing : binders)
sameVariable variable (ExactBinder _identity existing _coreType _structure) =
- existing == variable
+ existing == Just variable
sameIdentity identity (ExactBinder existing _variable _coreType _structure) =
existing == identity
+-- | Add one proof-owned binder which deliberately has no source-resolvable
+-- spelling. This is used for a nameless singular witness; it participates in
+-- checked support and de Bruijn weakening but cannot shadow or be looked up by
+-- a later source variable.
+extendExactAnonymousBinderContext
+ :: ExactLocalId
+ -> ExactBinderContext
+ -> Either ExactCompileError ExactBinderContext
+extendExactAnonymousBinderContext identity (ExactBinderContext binders)
+ | any sameIdentity binders =
+ Left (ExactDuplicateLocalIdentity Nowhere identity)
+ | otherwise =
+ Right
+ (ExactBinderContext
+ (ExactBinder identity Nothing TySet Nothing : binders))
+ where
+ sameIdentity (ExactBinder existing _variable _coreType _structure) =
+ existing == identity
+
exactBinderContextSupport
:: ExactBinderContext
-> Vector (ExactLocalId, CoreType)
@@ -150,7 +173,7 @@ exactBinderContextIndex variable (ExactBinderContext binders) =
go _index [] =
Nothing
go index (ExactBinder _identity candidate _coreType _structure : rest)
- | candidate == variable = Just index
+ | candidate == Just variable = Just index
| otherwise = go (index + 1) rest
newtype PreparedExactProposition = PreparedExactProposition
@@ -547,16 +570,88 @@ prepareExactProposition
-> Declaration.LoweringDriver
(Either ExactCompileError PreparedExactProposition)
prepareExactProposition context statement =
+ prepareExactPropositionTerm
+ context
+ (locate statement)
+ (compileStatement statement)
+
+-- | Compile the source bound of already-opened symbolic binders. This is the
+-- shared checked constraint seam used by quantified statements and proof
+-- binders, so relation signs, carrier casts, and global occurrences are
+-- elaborated exactly once by the ordinary expression compiler.
+prepareExactSymbolicBoundConstraints
+ :: ExactBinderContext
+ -> NonEmpty Raw.VarSymbol
+ -> Raw.Bound
+ -> Declaration.LoweringDriver
+ (Either ExactCompileError PreparedExactProposition)
+prepareExactSymbolicBoundConstraints context variables bound =
+ prepareExactPropositionTerm
+ context
+ (case bound of
+ Raw.Unbounded -> locate (NonEmpty.head variables)
+ _ -> locate bound)
+ (logicalConjunction
+ <$> compileSymbolicBoundConstraintList variables bound)
+
+-- | Compile the opened body used by a symbolic existential witness. Its
+-- grouping is deliberately identical to 'SymbolicExists': all bound
+-- constraints form the existential restriction and the stated proposition is
+-- its body.
+prepareExactSymbolicWitnessConstraints
+ :: ExactBinderContext
+ -> NonEmpty Raw.VarSymbol
+ -> Raw.Bound
+ -> Raw.Stmt
+ -> Declaration.LoweringDriver
+ (Either ExactCompileError PreparedExactProposition)
+prepareExactSymbolicWitnessConstraints context variables bound statement =
+ prepareExactPropositionTerm context (locate statement) do
+ constraints <-
+ logicalConjunction
+ <$> compileSymbolicBoundConstraintList variables bound
+ body <- compileStatement statement
+ pure
+ (if constraints == logicalTruth
+ then body
+ else logicalAnd constraints body)
+
+-- | Compile the checked constraint of an already-opened noun witness. Named
+-- binders are resolved normally; a nameless singular noun uses the nearest
+-- anonymous binder and therefore introduces no lookup spelling.
+prepareExactNounWitnessConstraints
+ :: ExactBinderContext
+ -> Raw.NounPhrase []
+ -> Declaration.LoweringDriver
+ (Either ExactCompileError PreparedExactProposition)
+prepareExactNounWitnessConstraints context nounPhrase =
+ case nounPhrase of
+ Raw.NounPhrase left noun variables right suchThat ->
+ prepareExactPropositionTerm context (locate noun) do
+ subjects <-
+ case NonEmpty.nonEmpty variables of
+ Just binders ->
+ toList
+ <$> traverse compileIntroducedVariable binders
+ Nothing ->
+ pure [CBound 0]
+ compileNounPhraseConstraints
+ subjects left noun right suchThat
+
+prepareExactPropositionTerm
+ :: ExactBinderContext
+ -> Location
+ -> Elaborate (CanonicalTerm ObjectId)
+ -> Declaration.LoweringDriver
+ (Either ExactCompileError PreparedExactProposition)
+prepareExactPropositionTerm context location compile =
Except.runExceptT do
let initialElaboration = initialElaborationState context
(term, finalElaboration) <-
- State.runStateT
- (compileStatement statement)
- initialElaboration
+ State.runStateT compile initialElaboration
checked <-
either
- (Except.throwError
- . ExactCoreCheckFailed (locate statement))
+ (Except.throwError . ExactCoreCheckFailed location)
pure
(checkScopedCanonicalCore
(`Map.lookup` elaborationGlobals finalElaboration)
@@ -565,7 +660,7 @@ prepareExactProposition context statement =
unless (scopedCoreType checked == TyProp)
(Except.throwError
(ExactFormulaExpectedProposition
- (locate statement)
+ location
(scopedCoreType checked)))
pure (PreparedExactProposition checked)
@@ -786,7 +881,7 @@ binderIndices :: ExactBinderContext -> Map.Map Raw.VarSymbol Natural
binderIndices (ExactBinderContext binders) =
Map.fromList
[ (variable, fromIntegral index)
- | (index, ExactBinder _identity variable _coreType _structure) <-
+ | (index, ExactBinder _identity (Just variable) _coreType _structure) <-
zip [0 :: Int ..] binders
]
@@ -2275,21 +2370,8 @@ compileSymbolicQuantified
-> Elaborate (CanonicalTerm ObjectId)
compileSymbolicQuantified quantifier variables bound suchThat compileBody =
withSetBinders variables do
- subjects <- traverse compileIntroducedVariable variables
- boundConstraints <- case bound of
- Raw.Unbounded ->
- pure []
- Raw.Bounded _location sign relation domain -> do
- domain' <- compileExpressionAsSet domain
- traverse
- (\subject -> do
- proposition <-
- compileAtomicRelationTerms
- subject relation domain'
- pure case sign of
- Raw.Positive -> proposition
- Raw.Negative -> logicalNot proposition)
- (toList subjects)
+ boundConstraints <-
+ compileSymbolicBoundConstraintList variables bound
suchThatConstraints <-
maybeToList <$> traverse compileStatement suchThat
body <- compileBody
@@ -2301,6 +2383,25 @@ compileSymbolicQuantified quantifier variables bound suchThat compileBody =
(boundConstraints <> suchThatConstraints))
body)
+compileSymbolicBoundConstraintList
+ :: NonEmpty Raw.VarSymbol
+ -> Raw.Bound
+ -> Elaborate [CanonicalTerm ObjectId]
+compileSymbolicBoundConstraintList variables = \case
+ Raw.Unbounded ->
+ pure []
+ Raw.Bounded _location sign relation domain -> do
+ subjects <- traverse compileIntroducedVariable variables
+ domain' <- compileExpressionAsSet domain
+ traverse
+ (\subject -> do
+ proposition <-
+ compileAtomicRelationTerms subject relation domain'
+ pure case sign of
+ Raw.Positive -> proposition
+ Raw.Negative -> logicalNot proposition)
+ (toList subjects)
+
compileAtomicRelationTerms
:: CanonicalTerm ObjectId
-> Raw.Relation
diff --git a/source/Checking/Exact/Proof.hs b/source/Checking/Exact/Proof.hs
index 40911b0..f3f3b9d 100644
--- a/source/Checking/Exact/Proof.hs
+++ b/source/Checking/Exact/Proof.hs
@@ -56,8 +56,6 @@ import Numeric.Natural (Natural)
data ExactProofError
= ExactProofUnsupportedClaim !Location
| ExactProofUnsupportedStep !Location
- | ExactProofBoundedFixNotSupported !Location
- | ExactProofBoundedTakeNotSupported !Location
| ExactProofSetInductionVariableRequired !Location
| ExactProofSetInductionVariableNotActive
!Location !Raw.VarSymbol
@@ -86,8 +84,6 @@ exactProofErrorLocation :: ExactProofError -> Location
exactProofErrorLocation = \case
ExactProofUnsupportedClaim location -> location
ExactProofUnsupportedStep location -> location
- ExactProofBoundedFixNotSupported location -> location
- ExactProofBoundedTakeNotSupported location -> location
ExactProofSetInductionVariableRequired location -> location
ExactProofSetInductionVariableNotActive location _variable ->
location
@@ -115,10 +111,6 @@ renderExactProofError = \case
at location <> "this claim is not yet supported by the typed checker"
ExactProofUnsupportedStep location ->
at location <> "this proof step is not yet supported by the typed checker"
- ExactProofBoundedFixNotSupported location ->
- at location <> "bounded proof binders are not yet supported"
- ExactProofBoundedTakeNotSupported location ->
- at location <> "bounded proof witnesses are not yet supported"
ExactProofSetInductionVariableRequired location ->
at location <> "exact set induction requires a named set variable"
ExactProofSetInductionVariableNotActive location variable ->
@@ -485,34 +477,47 @@ prepareProof fallback context locals inductionAntecedents goal = \case
goal
justification
Raw.FixSymbolic location variables bound continuation -> do
- unless (bound == Raw.Unbounded)
- (throwProof
- (ExactProofBoundedFixNotSupported location))
(context', goal', identities) <-
openFixedVariables context goal variables
- PreparedFix identities
- <$> prepareProof
- fallback
- context'
- locals
- Nothing
- goal'
- continuation
+ case bound of
+ Raw.Unbounded ->
+ PreparedFix identities
+ <$> prepareProof
+ fallback
+ context'
+ locals
+ Nothing
+ goal'
+ continuation
+ _ -> do
+ constraint <-
+ prepareSymbolicBoundConstraints
+ context' variables bound
+ prepareGuardedFix
+ fallback location context' locals goal'
+ identities constraint continuation
+ Raw.FixSuchThat location variables statement continuation -> do
+ (context', goal', identities) <-
+ openFixedVariables context goal variables
+ constraint <-
+ Exact.preparedExactPropositionCore
+ <$> prepareStatement context' statement
+ prepareGuardedFix
+ fallback location context' locals goal'
+ identities constraint continuation
Raw.Assume location statement continuation -> do
- (antecedent, conclusion) <-
+ supplied <- prepareStatement context statement
+ when (isNothing (openScopedImplication goal))
+ (throwProof (ExactProofExpectedImplicationGoal location))
+ (assumption, conclusion) <-
maybe
- (throwProof
- (ExactProofExpectedImplicationGoal location))
+ (throwProof (ExactProofGoalStatementMismatch location))
pure
- (openScopedImplication goal)
- supplied <- prepareStatement context statement
- unless
- (Exact.preparedExactPropositionCore supplied
- == antecedent)
- (throwProof
- (ExactProofGoalStatementMismatch location))
- local <- allocateLocal ExactAssumption context antecedent
- PreparedAssume antecedent
+ (openScopedAssumption
+ (Exact.preparedExactPropositionCore supplied)
+ goal)
+ local <- allocateLocal ExactAssumption context assumption
+ PreparedAssume assumption
<$> prepareProof
fallback
context
@@ -521,36 +526,13 @@ prepareProof fallback context locals inductionAntecedents goal = \case
conclusion
continuation
Raw.TakeVar location variables bound statement justification continuation -> do
- unless (bound == Raw.Unbounded)
- (throwProof
- (ExactProofBoundedTakeNotSupported location))
- identities <-
- traverse (const allocateLocalIdentity) variables
- context' <-
- either
- (throwProof . ExactProofElaborationFailed)
- pure
- (Exact.extendExactBinderContext
- (NonEmpty.zip identities variables)
- context)
- witness <-
- Exact.preparedExactPropositionCore
- <$> prepareStatement context' statement
- let witnessCount = length (toList variables)
- existence = closeTakenWitnesses witnessCount witness
- goal' = weakenForTakenWitnesses witnessCount goal
- discharge <-
- prepareDischarge
- location context locals existence justification
- local <- allocateLocal ExactAssumption context' witness
- PreparedTake (toList identities) witness discharge
- <$> prepareProof
- fallback
- context'
- (locals <> [local])
- Nothing
- goal'
- continuation
+ prepareSymbolicTake
+ fallback location context locals goal variables bound statement
+ justification continuation
+ Raw.TakeNoun location nounPhrase justification continuation ->
+ prepareNounTake
+ fallback location context locals goal nounPhrase
+ justification continuation
Raw.BySetInduction location variable continuation ->
case (inductionAntecedents, continuation) of
(Nothing, _proof) ->
@@ -593,6 +575,12 @@ prepareProof fallback context locals inductionAntecedents goal = \case
justification
(Just _antecedents, _proof) ->
throwProof (ExactProofUnsupportedStep location)
+ Raw.Have location Nothing
+ (Raw.SymbolicExists _existential variables bound statement)
+ justification continuation ->
+ prepareSymbolicTake
+ fallback location context locals goal variables bound statement
+ justification continuation
Raw.Have location since statement justification continuation -> do
when (isJust since)
(throwProof (ExactProofUnsupportedStep location))
@@ -756,6 +744,168 @@ prepareProof fallback context locals inductionAntecedents goal = \case
(impossible "an exact claim antecedent changed context")
(implyScopedCore antecedent conclusion)
+prepareGuardedFix
+ :: Location
+ -> Location
+ -> Exact.ExactBinderContext
+ -> [PreparedLocal]
+ -> ScopedCheckedCore ObjectId
+ -> [Exact.ExactLocalId]
+ -> ScopedCheckedCore ObjectId
+ -> Raw.Proof
+ -> Prepare PreparedProof
+prepareGuardedFix
+ fallback location context locals goal identities constraint continuation = do
+ (antecedent, conclusion) <-
+ maybe
+ (throwProof (ExactProofExpectedImplicationGoal location))
+ pure
+ (openScopedImplication goal)
+ unless (constraint == antecedent)
+ (throwProof (ExactProofGoalStatementMismatch location))
+ local <- allocateLocal ExactAssumption context constraint
+ prepared <-
+ prepareProof
+ fallback
+ context
+ (locals <> [local])
+ Nothing
+ conclusion
+ continuation
+ pure (PreparedFix identities (PreparedAssume constraint prepared))
+
+prepareSymbolicBoundConstraints
+ :: Exact.ExactBinderContext
+ -> NonEmpty Raw.VarSymbol
+ -> Raw.Bound
+ -> Prepare (ScopedCheckedCore ObjectId)
+prepareSymbolicBoundConstraints context variables bound =
+ Exact.preparedExactPropositionCore
+ <$> ( liftDriver
+ (Exact.prepareExactSymbolicBoundConstraints
+ context variables bound)
+ >>= either
+ (throwProof . ExactProofElaborationFailed)
+ pure
+ )
+
+prepareSymbolicTake
+ :: Location
+ -> Location
+ -> Exact.ExactBinderContext
+ -> [PreparedLocal]
+ -> ScopedCheckedCore ObjectId
+ -> NonEmpty Raw.VarSymbol
+ -> Raw.Bound
+ -> Raw.Stmt
+ -> Raw.Justification
+ -> Raw.Proof
+ -> Prepare PreparedProof
+prepareSymbolicTake
+ fallback location context locals goal variables bound statement
+ justification continuation = do
+ identities <- traverse (const allocateLocalIdentity) variables
+ context' <-
+ either
+ (throwProof . ExactProofElaborationFailed)
+ pure
+ (Exact.extendExactBinderContext
+ (NonEmpty.zip identities variables)
+ context)
+ witness <-
+ Exact.preparedExactPropositionCore
+ <$> ( liftDriver
+ (Exact.prepareExactSymbolicWitnessConstraints
+ context' variables bound statement)
+ >>= either
+ (throwProof . ExactProofElaborationFailed)
+ pure
+ )
+ prepareTake
+ fallback location context locals goal context'
+ (toList identities) witness justification continuation
+
+prepareNounTake
+ :: Location
+ -> Location
+ -> Exact.ExactBinderContext
+ -> [PreparedLocal]
+ -> ScopedCheckedCore ObjectId
+ -> Raw.NounPhrase []
+ -> Raw.Justification
+ -> Raw.Proof
+ -> Prepare PreparedProof
+prepareNounTake
+ fallback location context locals goal nounPhrase
+ justification continuation = do
+ (identities, context') <-
+ case nounPhrase of
+ Raw.NounPhrase _left _noun variables _right _suchThat ->
+ case NonEmpty.nonEmpty variables of
+ Just binders -> do
+ identities <-
+ traverse (const allocateLocalIdentity) binders
+ context' <-
+ either
+ (throwProof . ExactProofElaborationFailed)
+ pure
+ (Exact.extendExactBinderContext
+ (NonEmpty.zip identities binders)
+ context)
+ pure (toList identities, context')
+ Nothing -> do
+ identity <- allocateLocalIdentity
+ context' <-
+ either
+ (throwProof . ExactProofElaborationFailed)
+ pure
+ (Exact.extendExactAnonymousBinderContext
+ identity context)
+ pure ([identity], context')
+ witness <-
+ Exact.preparedExactPropositionCore
+ <$> ( liftDriver
+ (Exact.prepareExactNounWitnessConstraints
+ context' nounPhrase)
+ >>= either
+ (throwProof . ExactProofElaborationFailed)
+ pure
+ )
+ prepareTake
+ fallback location context locals goal context'
+ identities witness justification continuation
+
+prepareTake
+ :: Location
+ -> Location
+ -> Exact.ExactBinderContext
+ -> [PreparedLocal]
+ -> ScopedCheckedCore ObjectId
+ -> Exact.ExactBinderContext
+ -> [Exact.ExactLocalId]
+ -> ScopedCheckedCore ObjectId
+ -> Raw.Justification
+ -> Raw.Proof
+ -> Prepare PreparedProof
+prepareTake
+ fallback location context locals goal witnessContext
+ identities witness justification continuation = do
+ let witnessCount = length identities
+ existence = closeTakenWitnesses witnessCount witness
+ goal' = weakenForTakenWitnesses witnessCount goal
+ discharge <-
+ prepareDischarge
+ location context locals existence justification
+ local <- allocateLocal ExactAssumption witnessContext witness
+ PreparedTake identities witness discharge
+ <$> prepareProof
+ fallback
+ witnessContext
+ (locals <> [local])
+ Nothing
+ goal'
+ continuation
+
-- The discharged existential and the opened witness premise are the same
-- checked proposition viewed on opposite sides of existential elimination.
closeTakenWitnesses
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-05 11:57:50 +0000