summaryrefslogtreecommitdiff
path: root/source/Checking/Exact
diff options
context:
space:
mode:
Diffstat (limited to 'source/Checking/Exact')
-rw-r--r--source/Checking/Exact/Global.hs10
-rw-r--r--source/Checking/Exact/Inductive.hs2
-rw-r--r--source/Checking/Exact/Proof.hs108
3 files changed, 112 insertions, 8 deletions
diff --git a/source/Checking/Exact/Global.hs b/source/Checking/Exact/Global.hs
index 848b600..094255e 100644
--- a/source/Checking/Exact/Global.hs
+++ b/source/Checking/Exact/Global.hs
@@ -33,6 +33,7 @@ data ExactGlobalResolutionError
= ExactGlobalNotVisible !Internal.Symbol
| ExactGlobalAmbiguous !Internal.Symbol
| ExactGlobalUnsupported !Internal.Symbol
+ | ExactGlobalContextualUnsupported !Internal.Symbol
| ExactGlobalContentInvalid !CoreCheckError
deriving stock (Show, Eq)
@@ -71,7 +72,7 @@ resolveExactSourceGlobals symbols =
throwError (ExactGlobalNotVisible symbol)
[match] -> do
(source, sourceTypes) <-
- liftEither (prepareSourceGlobal match)
+ liftEither (prepareSourceGlobal symbol match)
pure
( Map.insert symbol source resolved
, Map.union sourceTypes types
@@ -80,14 +81,15 @@ resolveExactSourceGlobals symbols =
throwError (ExactGlobalAmbiguous symbol)
prepareSourceGlobal
- :: ( SemanticGlobalTarget
+ :: Internal.Symbol
+ -> ( SemanticGlobalTarget
, ObjectContent
, Map.Map ObjectId CoreType
)
-> Either
ExactGlobalResolutionError
(Typed.SourceGlobal ObjectId, Map.Map ObjectId CoreType)
-prepareSourceGlobal (target, content, dependencies) = do
+prepareSourceGlobal symbol (target, content, dependencies) = do
body <-
case target of
GlobalReference _identity ->
@@ -103,6 +105,8 @@ prepareSourceGlobal (target, content, dependencies) = do
_ ->
impossible
"validated transparent expansion has opaque content"
+ ContextualTransparentExpansion _identity _requirements ->
+ Left (ExactGlobalContextualUnsupported symbol)
let identity = semanticGlobalTargetObject target
types =
Map.insert
diff --git a/source/Checking/Exact/Inductive.hs b/source/Checking/Exact/Inductive.hs
index c3f281c..e873f0c 100644
--- a/source/Checking/Exact/Inductive.hs
+++ b/source/Checking/Exact/Inductive.hs
@@ -500,6 +500,8 @@ exactGlobalError location = \case
ExactInductiveGlobalAmbiguous location symbol
ExactGlobal.ExactGlobalUnsupported symbol ->
ExactInductiveUnsupportedSymbol location symbol
+ ExactGlobal.ExactGlobalContextualUnsupported symbol ->
+ ExactInductiveUnsupportedSymbol location symbol
ExactGlobal.ExactGlobalContentInvalid failure ->
ExactInductiveGlobalContentInvalid location failure
diff --git a/source/Checking/Exact/Proof.hs b/source/Checking/Exact/Proof.hs
index b66ebfe..ad95a62 100644
--- a/source/Checking/Exact/Proof.hs
+++ b/source/Checking/Exact/Proof.hs
@@ -63,6 +63,8 @@ data ExactProofError
| ExactProofExpectedImplicationGoal !Location
| ExactProofGoalStatementMismatch !Location
| ExactProofContradictionGoalMismatch !Location
+ | ExactProofLocalFunctionBinderMismatch !Location
+ | ExactProofLocalFunctionNameConflict !Location
| ExactProofUnknownReference !Location !Raw.Marker
| ExactProofElaborationFailed !Exact.ExactCompileError
| ExactProofObligationPreparationFailed
@@ -91,6 +93,8 @@ exactProofErrorLocation = \case
ExactProofExpectedImplicationGoal location -> location
ExactProofGoalStatementMismatch location -> location
ExactProofContradictionGoalMismatch location -> location
+ ExactProofLocalFunctionBinderMismatch location -> location
+ ExactProofLocalFunctionNameConflict location -> location
ExactProofUnknownReference location _marker -> location
ExactProofElaborationFailed failure ->
Exact.exactCompileErrorLocation failure
@@ -131,6 +135,10 @@ renderExactProofError = \case
at location <> "the proof step does not match the current goal"
ExactProofContradictionGoalMismatch location ->
at location <> "contradiction requires falsum as the current goal"
+ ExactProofLocalFunctionBinderMismatch location ->
+ at location <> "the function argument must match its domain binder"
+ ExactProofLocalFunctionNameConflict location ->
+ at location <> "the function and argument names must be distinct"
ExactProofUnknownReference location marker ->
at location <> "the cited fact " <> shown marker <> " is not visible"
ExactProofElaborationFailed failure ->
@@ -210,6 +218,11 @@ data PreparedProof
!(ScopedCheckedCore ObjectId)
!(ScopedCheckedCore ObjectId)
!PreparedProof
+ | PreparedDefineFunction
+ !Exact.ExactLocalId
+ !(ScopedCheckedCore ObjectId)
+ !(ScopedCheckedCore ObjectId)
+ !PreparedProof
| PreparedContradiction !PreparedDischarge
data PreparedExactProof = PreparedExactProof
@@ -277,6 +290,7 @@ prepareExactProof block explicitProof =
openEnvelopeVariables
targetCore
(Exact.preparedExactClaimVariables envelope)
+ (Exact.preparedExactClaimContext envelope)
(locals, bodyGoal, antecedents) <-
openEnvelopeAntecedents
context
@@ -410,20 +424,31 @@ prepareFinalPreludeFoundationClaim foundation block explicitProof =
openEnvelopeVariables
:: ScopedCheckedCore ObjectId
-> [Raw.VarSymbol]
+ -> Exact.ExactBinderContext
-> Prepare failure
( Exact.ExactBinderContext
, ScopedCheckedCore ObjectId
, [Exact.ExactLocalId]
)
-openEnvelopeVariables target variables =
+openEnvelopeVariables target variables preparedContext =
case NonEmpty.nonEmpty variables of
Nothing ->
- pure (Exact.emptyExactBinderContext, target, [])
- Just nonempty ->
- openFixedVariables
+ pure (preparedContext, target, [])
+ Just nonempty -> do
+ (_unannotated, opened, identities) <-
+ openFixedVariables
Exact.emptyExactBinderContext
target
nonempty
+ let expected =
+ reverse
+ (fst <$> toList
+ (Exact.exactBinderContextSupport preparedContext))
+ unless
+ (identities == expected)
+ (impossible
+ "prepared claim annotations do not match opened binders")
+ pure (preparedContext, opened, identities)
openEnvelopeAntecedents
:: Exact.ExactBinderContext
@@ -639,12 +664,16 @@ prepareProof fallback context locals inductionAntecedents goal = \case
(Exact.extendExactBinderContext
((identity, variable) :| [])
context)
+ separationCharacteristic <-
+ liftDriver
+ (Declaration.currentFoundationAxiomDriver
+ SeparationCharacteristic)
definition <-
maybe
(impossible
"an exact set expression did not form a local definition")
pure
- (scopedSetDefinition body)
+ (scopedSetDefinition separationCharacteristic body)
local <-
allocateLocal ExactLocalDefinition context' definition
PreparedDefine identity body definition
@@ -655,6 +684,65 @@ prepareProof fallback context locals inductionAntecedents goal = \case
Nothing
(weakenCheckedScopedCore TySet goal)
continuation
+ Raw.DefineFunction
+ location function argument value bound domain continuation -> do
+ unless (argument == bound)
+ (throwProof
+ (ExactProofLocalFunctionBinderMismatch (locate bound)))
+ when (function == argument)
+ (throwProof
+ (ExactProofLocalFunctionNameConflict (locate function)))
+ argumentIdentity <- allocateLocalIdentity
+ argumentContext <-
+ either
+ (throwProof . ExactProofElaborationFailed)
+ pure
+ (Exact.extendExactBinderContext
+ ((argumentIdentity, argument) :| [])
+ context)
+ graph <-
+ liftDriver
+ (Exact.prepareExactLocalFunctionGraph
+ location context argumentContext domain value)
+ >>= either
+ (throwProof . ExactProofElaborationFailed)
+ pure
+ functionIdentity <- allocateLocalIdentity
+ functionContext <-
+ either
+ (throwProof . ExactProofElaborationFailed)
+ pure
+ (Exact.extendExactBinderContext
+ ((functionIdentity, function) :| [])
+ context)
+ replacementCharacteristic <-
+ liftDriver
+ (Declaration.currentFoundationAxiomDriver
+ ReplacementCharacteristic)
+ definition <-
+ maybe
+ (impossible
+ "a checked replacement graph did not form a local definition")
+ pure
+ (scopedCharacteristicDefinition
+ replacementCharacteristic
+ (Exact.preparedExactLocalFunctionGraphCore graph)
+ ( Exact.preparedExactLocalFunctionGraphDomain graph
+ :| [Exact.preparedExactLocalFunctionGraphMap graph]
+ ))
+ local <-
+ allocateLocal ExactLocalDefinition functionContext definition
+ PreparedDefineFunction
+ functionIdentity
+ (Exact.preparedExactLocalFunctionGraphCore graph)
+ definition
+ <$> prepareProof
+ fallback
+ functionContext
+ (locals <> [local])
+ Nothing
+ (weakenCheckedScopedCore TySet goal)
+ continuation
Raw.Contradiction location justification -> do
unless
( scopedCoreType goal == TyProp
@@ -978,6 +1066,8 @@ preparedProofFirstOmission = \case
<|> preparedProofFirstOmission continuation
PreparedDefine _identity _body _definition continuation ->
preparedProofFirstOmission continuation
+ PreparedDefineFunction _identity _graph _definition continuation ->
+ preparedProofFirstOmission continuation
PreparedContradiction{} -> Nothing
executePreparedProof
@@ -1007,6 +1097,8 @@ executePreparedProof = \case
executePreparedProof continuation
PreparedDefine _identity _body _definition continuation ->
executePreparedProof continuation
+ PreparedDefineFunction _identity _graph _definition continuation ->
+ executePreparedProof continuation
PreparedContradiction discharge ->
executeDischarge discharge
@@ -1077,6 +1169,12 @@ putPreparedProof = \case
PreparedContradiction discharge -> do
putCacheTag 0x0a
putPreparedDischarge discharge
+ PreparedDefineFunction identity graph definition continuation -> do
+ putCacheTag 0x0b
+ putCacheNatural (Exact.exactLocalIdValue identity)
+ putScopedTerm graph
+ putScopedProposition definition
+ putPreparedProof continuation
putPreparedDischarge :: PreparedDischarge -> CachePut
putPreparedDischarge
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-04 07:35:20 +0000