diff options
Diffstat (limited to 'source/Felix/Checking/Exact')
| -rw-r--r-- | source/Felix/Checking/Exact/Datatype.hs | 751 | ||||
| -rw-r--r-- | source/Felix/Checking/Exact/Global.hs | 116 | ||||
| -rw-r--r-- | source/Felix/Checking/Exact/Inductive.hs | 838 | ||||
| -rw-r--r-- | source/Felix/Checking/Exact/Proof.hs | 2639 | ||||
| -rw-r--r-- | source/Felix/Checking/Exact/Vocabulary.hs | 218 |
5 files changed, 4562 insertions, 0 deletions
diff --git a/source/Felix/Checking/Exact/Datatype.hs b/source/Felix/Checking/Exact/Datatype.hs new file mode 100644 index 0000000..be943cd --- /dev/null +++ b/source/Felix/Checking/Exact/Datatype.hs @@ -0,0 +1,751 @@ +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE NoImplicitPrelude #-} + +-- | Exact preparation of deterministic datatype declarations. +module Felix.Checking.Exact.Datatype + ( PreparedExactDatatype + , preparedExactDatatypeObjects + , preparedExactDatatypeBindings + , PreparedExactDatatypeFact + , preparedExactDatatypeFacts + , preparedExactDatatypeFactMarker + , preparedExactDatatypeFactTarget + , preparedExactDatatypeFactReference + , preparedExactDatatypeDescriptor + , prepareExactDatatype + , CheckedExactDatatypeAuthorization + , lowerPreparedExactDatatype + , authorizeCheckedExactDatatype + , ExactDatatypeError(..) + , exactDatatypeErrorLocation + , renderExactDatatypeError + ) where + +import Base hiding (Empty) +import Felix.Checking.Authority +import Felix.Checking.Core +import Felix.Checking.Datatype qualified as Datatype +import Felix.Checking.Declaration qualified as Declaration +import Felix.Checking.Exact.Global qualified as ExactGlobal +import Felix.Checking.Exact.Vocabulary +import Felix.Checking.Identity +import Felix.Checking.Semantic +import Felix.Checking.Typed.Inductive qualified as Typed +import Felix.Cache.Codec +import Felix.Module +import Felix.Meaning qualified as Meaning +import Felix.Report.Location +import Felix.Syntax.Abstract qualified as Raw +import Felix.Syntax.Interface +import Felix.Syntax.Internal qualified as Internal + +import Control.Monad (unless, when) +import Control.Monad.Except (ExceptT) +import Control.Monad.Except qualified as Except +import Data.Bifunctor (first) +import Data.ByteString (ByteString) +import Data.List.NonEmpty qualified as NonEmpty +import Data.Map.Strict qualified as Map +import Data.Set qualified as Set +import Data.Text qualified as Text +import Numeric.Natural (Natural) + + +data PreparedDatatypeObject = PreparedDatatypeObject + !Internal.Symbol + !SemanticGlobalKey + !CoreType + !ObjectId + !AssertedObject + +data PreparedExactDatatypeFact = PreparedExactDatatypeFact + !Internal.Marker + !(FrozenCheckedCore ObjectId) + !TheoremRef + +preparedExactDatatypeFactMarker + :: PreparedExactDatatypeFact + -> Internal.Marker +preparedExactDatatypeFactMarker + (PreparedExactDatatypeFact marker _target _reference) = + marker + +preparedExactDatatypeFactTarget + :: PreparedExactDatatypeFact + -> FrozenCheckedCore ObjectId +preparedExactDatatypeFactTarget + (PreparedExactDatatypeFact _marker target _reference) = + target + +preparedExactDatatypeFactReference + :: PreparedExactDatatypeFact + -> TheoremRef +preparedExactDatatypeFactReference + (PreparedExactDatatypeFact _marker _target reference) = + reference + +data PreparedExactDatatype = PreparedExactDatatype + !Location + !DeclarationSyntaxId + !(NonEmpty PreparedDatatypeObject) + !(NonEmpty PreparedExactDatatypeFact) + !DatatypeCompilationDescriptor + +data CheckedExactDatatypeAuthorization = + CheckedExactDatatypeAuthorization + !DatatypeCompilationDescriptor + !ObjectId + !(NonEmpty ObjectId) + +preparedExactDatatypeObjects + :: PreparedExactDatatype + -> NonEmpty (ObjectId, CoreType) +preparedExactDatatypeObjects + (PreparedExactDatatype _location _syntax objects _facts _descriptor) = + fmap + (\(PreparedDatatypeObject _symbol _key coreType identity _asserted) -> + (identity, coreType)) + objects + +preparedExactDatatypeBindings + :: PreparedExactDatatype + -> NonEmpty (SemanticGlobalKey, SemanticGlobalTarget) +preparedExactDatatypeBindings + (PreparedExactDatatype _location _syntax objects _facts _descriptor) = + fmap + (\(PreparedDatatypeObject _symbol key _coreType identity _asserted) -> + (key, GlobalReference identity)) + objects + +preparedExactDatatypeFacts + :: PreparedExactDatatype + -> NonEmpty PreparedExactDatatypeFact +preparedExactDatatypeFacts + (PreparedExactDatatype _location _syntax _objects facts _descriptor) = + facts + +preparedExactDatatypeDescriptor + :: PreparedExactDatatype + -> DatatypeCompilationDescriptor +preparedExactDatatypeDescriptor + (PreparedExactDatatype _location _syntax _objects _facts descriptor) = + descriptor + +lowerPreparedExactDatatype + :: PreparedExactDatatype + -> Declaration.LoweringDriver + (Either + Declaration.DeclarationError + (Declaration.CheckedDeclaration + CheckedExactDatatypeAuthorization)) +lowerPreparedExactDatatype + (PreparedExactDatatype _location syntax objects facts descriptor) = + do + prepared <- + traverse + (\(PreparedExactDatatypeFact marker target _reference) -> + Declaration.prepareFrozenCandidateSpecLowering + assertedObjects + target + SearchEligible + [markerAlias marker]) + facts + pure (buildChecked <$> sequence prepared) + where + assertedObjects = + toList + (fmap + (\(PreparedDatatypeObject + _symbol _key _coreType _identity asserted) -> asserted) + objects) + bindings = + toList + (fmap + (\(PreparedDatatypeObject + _symbol key _coreType identity _asserted) -> + semanticGlobalBinding key (GlobalReference identity)) + objects) + carrier :| constructors = fmap objectIdentity objects + constructorIds = + case constructors of + firstConstructor : remainingConstructors -> + firstConstructor :| remainingConstructors + [] -> impossible "a prepared datatype has no constructor" + buildChecked specs = + Declaration.checkedCompiledDeclaration + syntax + assertedObjects + [] + bindings + [] + [ fmap + (\spec -> + Declaration.checkedCandidate + spec + (Declaration.checkedDatatypePlanning descriptor)) + specs + ] + (CheckedExactDatatypeAuthorization + descriptor carrier constructorIds) + + markerAlias (Internal.Marker name) = semanticName name + + objectIdentity + (PreparedDatatypeObject + _symbol _key _coreType identity _asserted) = + identity + +authorizeCheckedExactDatatype + :: CheckedExactDatatypeAuthorization + -> [NonEmpty Declaration.ReservedCandidate] + -> Declaration.Declaration () +authorizeCheckedExactDatatype + (CheckedExactDatatypeAuthorization descriptor carrier constructors) = + \case + [candidates] -> + Declaration.authorizeDatatypeCompilationCandidates + descriptor carrier constructors candidates + stages -> + Declaration.failDeclaration + (Declaration.CheckedAuthorizationCandidateShapeMismatch + 1 (length stages)) + +data ExactDatatypeError + = ExactDatatypeUnsupportedBlock !Location + | ExactDatatypeOccurrenceCountMismatch !Location !Int !Int + | ExactDatatypeOccurrenceMismatch !Location + | ExactDatatypeGlossFailed !Location !Meaning.GlossError + | ExactDatatypeInvalid !Location !Text + | ExactDatatypeDuplicateGlobal !Location !SemanticGlobalKey + | ExactDatatypeFixedSemanticCollision !Location !SemanticGlobalKey + | ExactDatatypeGlobalAlreadyVisible !Location !SemanticGlobalKey + | ExactDatatypeObjectAlreadyAvailable !Location !ObjectId + | ExactDatatypeGlobalResolutionFailed + !Location + !ExactGlobal.ExactGlobalResolutionError + | ExactDatatypeLoweringFailed !Location !Typed.TypedInductiveError + | ExactDatatypeExpectedSet !Location !CoreType + | ExactDatatypeExpectedProposition !Location !CoreType + deriving stock (Show, Eq) + +exactDatatypeErrorLocation :: ExactDatatypeError -> Location +exactDatatypeErrorLocation = \case + ExactDatatypeUnsupportedBlock location -> location + ExactDatatypeOccurrenceCountMismatch location _expected _actual -> location + ExactDatatypeOccurrenceMismatch location -> location + ExactDatatypeGlossFailed location _failure -> location + ExactDatatypeInvalid location _message -> location + ExactDatatypeDuplicateGlobal location _key -> location + ExactDatatypeFixedSemanticCollision location _key -> location + ExactDatatypeGlobalAlreadyVisible location _key -> location + ExactDatatypeObjectAlreadyAvailable location _identity -> location + ExactDatatypeGlobalResolutionFailed location _failure -> location + ExactDatatypeLoweringFailed location _failure -> location + ExactDatatypeExpectedSet location _actual -> location + ExactDatatypeExpectedProposition location _actual -> location + +renderExactDatatypeError :: ExactDatatypeError -> Text +renderExactDatatypeError failure = + locationToText (exactDatatypeErrorLocation failure) + <> ": " + <> case failure of + ExactDatatypeUnsupportedBlock{} -> + "this datatype source form is not supported by the typed checker" + ExactDatatypeOccurrenceCountMismatch _location expected actual -> + "the datatype has " <> shown actual + <> " syntax occurrences, but " <> shown expected + <> " are required" + ExactDatatypeOccurrenceMismatch{} -> + "a datatype syntax occurrence does not match its declaration" + ExactDatatypeGlossFailed _location glossFailure -> + "datatype elaboration failed: " <> shown glossFailure + ExactDatatypeInvalid _location message -> + "invalid datatype declaration: " <> message + ExactDatatypeDuplicateGlobal _location key -> + "the datatype declares the semantic key more than once: " + <> shown key + ExactDatatypeFixedSemanticCollision _location key -> + "the datatype collides with fixed semantics for " <> shown key + ExactDatatypeGlobalAlreadyVisible _location key -> + "the datatype global is already visible: " <> shown key + ExactDatatypeObjectAlreadyAvailable _location identity -> + "the datatype opaque object is already available: " + <> shown identity + ExactDatatypeGlobalResolutionFailed _location resolution -> + "datatype global resolution failed: " <> shown resolution + ExactDatatypeLoweringFailed _location typedFailure -> + "typed datatype lowering failed: " <> shown typedFailure + ExactDatatypeExpectedSet _location actual -> + "a datatype premise domain has type " <> shown actual + <> " instead of Set" + ExactDatatypeExpectedProposition _location actual -> + "a generated datatype fact has type " <> shown actual + <> " instead of Prop" + where + shown :: Show value => value -> Text + shown = Text.pack . show + +type Prepare = + ExceptT ExactDatatypeError (Declaration.LoweringDriver) + +type SourceOccurrence = (Location, Raw.Marker, CanonicalLexicalEntry) + +exactDatatypeInvalid + :: Location + -> Datatype.DatatypeValidationError + -> ExactDatatypeError +exactDatatypeInvalid declarationLocation failure = + ExactDatatypeInvalid + (fromMaybe + declarationLocation + (Datatype.datatypeValidationErrorLocation failure)) + (Datatype.renderDatatypeValidationError failure) + +prepareExactDatatype + :: Raw.Block + -> [SourceOccurrence] + -> Declaration.LoweringDriver + (Either ExactDatatypeError PreparedExactDatatype) +prepareExactDatatype block occurrences = + Except.runExceptT do + (location, marker, rawDatatype) <- + case block of + Raw.BlockData blockLocation _title blockMarker datatype -> + pure (blockLocation, blockMarker, datatype) + _ -> + Except.throwError + (ExactDatatypeUnsupportedBlock (locate block)) + keys <- validateOccurrences location marker rawDatatype occurrences + internal <- + case Meaning.meaning [block] of + Right + [Internal.BlockData + _internalLocation _internalMarker datatype] -> + pure datatype + Left failure -> + Except.throwError + (ExactDatatypeGlossFailed location failure) + Right _ -> + Except.throwError + (ExactDatatypeUnsupportedBlock location) + checked <- + -- The new opaque carrier has no semantic binding while its + -- declaration is prepared, so premise recursion cannot depend on + -- abbreviation expansion. Revisit this if forward aliases become + -- available. + Except.lift + (Datatype.prepareCheckedDatatype pure internal) + >>= Except.liftEither + . first (exactDatatypeInvalid location) + let symbols = + Datatype.checkedDatatypeHeadSymbol checked + :| toList + (Datatype.checkedDatatypeConstructorSymbols checked) + views = Datatype.checkedDatatypeClauseViews checked + arities = + 0 :| (length + . Datatype.checkedDatatypeClauseViewArguments + <$> toList views) + unless (NonEmpty.length symbols == NonEmpty.length keys) + (Except.throwError + (ExactDatatypeOccurrenceCountMismatch + location + (NonEmpty.length symbols) + (NonEmpty.length keys))) + validateKeys occurrences keys + slot <- Except.lift Declaration.nextDeclarationSlotLowering + theory <- Except.lift Declaration.currentTheoryLowering + objects <- + sequence + (NonEmpty.zipWith + (\index (occurrenceLocation, symbol, key, arity) -> + prepareObject + occurrenceLocation + slot theory index symbol key arity) + (0 :| [1 ..]) + (NonEmpty.zipWith + (\occurrenceLocation (symbol, key, arity) -> + (occurrenceLocation, symbol, key, arity)) + (validatedOccurrenceLocations occurrences) + (NonEmpty.zipWith + (\(symbol, key) arity -> + (symbol, key, arity)) + (NonEmpty.zip symbols keys) + arities))) + let ownedSymbols = Set.fromList (toList symbols) + generated = Datatype.checkedDatatypeGeneratedFacts checked + externalSymbols = + (foldMap + (Internal.mentionedSymbols . snd) + generated + <> foldMap premiseSymbols views) + `Set.difference` ownedSymbols + external <- + Except.lift + (ExactGlobal.resolveExactSourceGlobals externalSymbols) + >>= Except.liftEither + . first (ExactDatatypeGlobalResolutionFailed location) + let (externalGlobals, externalTypes) = external + ownedGlobals = + Map.fromList + [ (symbol, Typed.SourceGlobal identity Nothing) + | PreparedDatatypeObject + symbol _key _coreType identity _asserted <- + toList objects + ] + ownedTypes = + Map.fromList + [ (identity, coreType) + | PreparedDatatypeObject + _symbol _key coreType identity _asserted <- + toList objects + ] + sourceGlobals = Map.union ownedGlobals externalGlobals + globalTypes = Map.union ownedTypes externalTypes + resolveGlobal = (`Map.lookup` sourceGlobals) + globalType identity = + fromMaybe + (impossible + "prepared datatype global has no checked type") + (Map.lookup identity globalTypes) + preparedClauses <- + Except.liftEither + (traverse + (prepareClause location globalType resolveGlobal) + views) + facts <- + Except.liftEither + (traverse + (prepareFact location theory globalType resolveGlobal) + generated) + let carrier = objectIdentity (NonEmpty.head objects) + constructors = objectIdentity <$> NonEmpty.tail objects + descriptor = + case NonEmpty.nonEmpty constructors of + Nothing -> + impossible + "a checked datatype has no constructors" + Just nonemptyConstructors -> + datatypeCompilationDescriptor + carrier + nonemptyConstructors + (preparedExactDatatypeFactReference + <$> toList facts) + syntax = + declarationSyntaxId + (encodePreparedDatatype + objects + preparedClauses + facts + descriptor) + pure + (PreparedExactDatatype + location + syntax + objects + facts + descriptor) + where + objectIdentity + (PreparedDatatypeObject _symbol _key _coreType identity _asserted) = + identity + +validateOccurrences + :: Location + -> Raw.Marker + -> Raw.Datatype + -> [SourceOccurrence] + -> Prepare (NonEmpty SemanticGlobalKey) +validateOccurrences location marker datatype occurrences = do + expected <- + Except.liftEither + (expectedOccurrences location marker datatype) + unless (length occurrences == NonEmpty.length expected) + (Except.throwError + (ExactDatatypeOccurrenceCountMismatch + location + (NonEmpty.length expected) + (length occurrences))) + keys <- + sequence + (NonEmpty.zipWith validateOne expected + (case NonEmpty.nonEmpty occurrences of + Just nonempty -> nonempty + Nothing -> + impossible + "equal nonzero occurrence counts became empty")) + pure keys + where + validateOne + (expectedLocation, expectedMarker, expectedPattern) + (actualLocation, actualMarker, entry) = + case entry of + CanonicalExpressionFunction pat marker' _fixity + | actualMarker == expectedMarker + , marker' == expectedMarker + , pat == expectedPattern -> + pure + (SemanticExpressionFunction pat) + _ -> + Except.throwError + (ExactDatatypeOccurrenceMismatch + (bestLocation actualLocation expectedLocation)) + + bestLocation actual expected + | actual == Nowhere = expected + | otherwise = actual + +expectedOccurrences + :: Location + -> Raw.Marker + -> Raw.Datatype + -> Either + ExactDatatypeError + (NonEmpty (Location, Raw.Marker, Raw.Pattern)) +expectedOccurrences location blockMarker datatype = do + headOccurrence <- + expectedSymbol blockMarker (Raw.datatypeHeadExpr datatype) + clauses <- + traverse + (\clause -> + case Raw.datatypeClauseConstructorExpr clause of + Raw.ExprOp constructorLocation symbol _arguments -> + Right + ( constructorLocation + , Raw.mixfixMarker symbol + , Raw.mixfixPattern symbol + ) + expression -> + Left + (ExactDatatypeOccurrenceMismatch + (locate expression))) + (Raw.datatypeClauses datatype) + pure (headOccurrence :| toList clauses) + where + expectedSymbol expectedMarker = \case + Raw.ExprOp symbolLocation symbol [] -> + Right + ( symbolLocation + , expectedMarker + , Raw.mixfixPattern symbol + ) + expression -> + Left + (ExactDatatypeOccurrenceMismatch + (case locate expression of + Nowhere -> location + expressionLocation -> expressionLocation)) + +validateKeys + :: [SourceOccurrence] + -> NonEmpty SemanticGlobalKey + -> Prepare () +validateKeys occurrences keys = do + case duplicateWithLocation of + Just (duplicate, duplicateLocation) -> + Except.throwError + (ExactDatatypeDuplicateGlobal + duplicateLocation + duplicate) + Nothing -> pure () + traverse_ validateOne (NonEmpty.zip locations keys) + where + locations = validatedOccurrenceLocations occurrences + + duplicateWithLocation = + go Set.empty + [ (key, occurrenceLocation) + | (key, (occurrenceLocation, _marker, _entry)) <- + zip (toList keys) occurrences + ] + + go _seen [] = Nothing + go seen ((key, occurrenceLocation) : remaining) + | key `Set.member` seen = Just (key, occurrenceLocation) + | otherwise = go (Set.insert key seen) remaining + + validateOne (occurrenceLocation, key) = do + when (isJust (fixedSemanticMeaning key)) + (Except.throwError + (ExactDatatypeFixedSemanticCollision occurrenceLocation key)) + visible <- + Except.lift + (Declaration.resolveVisibleGlobalLowering key) + when (isJust visible) + (Except.throwError + (ExactDatatypeGlobalAlreadyVisible occurrenceLocation key)) + +validatedOccurrenceLocations + :: [SourceOccurrence] + -> NonEmpty Location +validatedOccurrenceLocations occurrences = + case NonEmpty.nonEmpty + [ occurrenceLocation + | (occurrenceLocation, _marker, _entry) <- occurrences + ] of + Just nonempty -> nonempty + Nothing -> + impossible "validated datatype occurrences are empty" + +prepareObject + :: Location + -> DeclarationSlot + -> TheoryId + -> Natural + -> Internal.Symbol + -> SemanticGlobalKey + -> Int + -> Prepare PreparedDatatypeObject +prepareObject location slot theory index symbol key arity = do + let coreType = + foldr (const (TyArrow TySet)) TySet [1 .. arity] + seed = + opaqueDeclarationSeed + (declarationSlotModule slot) + (declarationSlotOrdinal slot) + DatatypeDeclaration + (generatedObjectSlot index) + content = OpaqueObjectContent theory seed coreType + identity = opaqueObjectId theory seed coreType + available <- Except.lift (Declaration.objectAvailableLowering identity) + when available + (Except.throwError + (ExactDatatypeObjectAlreadyAvailable location identity)) + pure + (PreparedDatatypeObject + symbol + key + coreType + identity + (assertedObject identity content)) + +data PreparedClause = PreparedClause + !Internal.FunctionSymbol + ![PreparedPremise] + +data PreparedPremise + = PreparedRecursivePremise !(FrozenCheckedCore ObjectId) + | PreparedNonRecursivePremise !(FrozenCheckedCore ObjectId) + +prepareClause + :: Location + -> (ObjectId -> CoreType) + -> (Internal.Symbol -> Maybe (Typed.SourceGlobal ObjectId)) + -> Datatype.CheckedDatatypeClauseView + -> Either ExactDatatypeError PreparedClause +prepareClause location globalType resolveGlobal view = + PreparedClause + (Datatype.checkedDatatypeClauseViewConstructor view) + <$> traverse preparePremise + (Datatype.checkedDatatypeClauseViewPremises view) + where + preparePremise = \case + Datatype.CheckedRecursiveDatatypePremise _variable domain -> + PreparedRecursivePremise + <$> prepareDomain domain + Datatype.CheckedNonRecursiveDatatypePremise _variable domain -> + PreparedNonRecursivePremise + <$> prepareDomain domain + + prepareDomain domain = do + checked <- + first (ExactDatatypeLoweringFailed location) + (Typed.prepareTypedClosedTerm + globalType + resolveGlobal + domain) + unless (frozenCoreType checked == TySet) + (Left + (ExactDatatypeExpectedSet + location + (frozenCoreType checked))) + pure checked + +prepareFact + :: Location + -> TheoryId + -> (ObjectId -> CoreType) + -> (Internal.Symbol -> Maybe (Typed.SourceGlobal ObjectId)) + -> (Internal.Marker, Internal.Formula) + -> Either ExactDatatypeError PreparedExactDatatypeFact +prepareFact location theory globalType resolveGlobal (marker, formula) = do + checked <- + first (ExactDatatypeLoweringFailed location) + (Typed.prepareTypedClosedFormula + globalType + resolveGlobal + formula) + unless (frozenCoreType checked == TyProp) + (Left + (ExactDatatypeExpectedProposition + location + (frozenCoreType checked))) + pure + (PreparedExactDatatypeFact + marker + checked + (theoremRef theory + (propositionIdOf (frozenCoreTerm checked)))) + +premiseSymbols + :: Datatype.CheckedDatatypeClauseView + -> Set.Set Internal.Symbol +premiseSymbols view = + foldMap symbols + (Datatype.checkedDatatypeClauseViewPremises view) + where + symbols = \case + Datatype.CheckedRecursiveDatatypePremise _variable domain -> + Internal.mentionedSymbols domain + Datatype.CheckedNonRecursiveDatatypePremise _variable domain -> + Internal.mentionedSymbols domain + +encodePreparedDatatype + :: NonEmpty PreparedDatatypeObject + -> NonEmpty PreparedClause + -> NonEmpty PreparedExactDatatypeFact + -> DatatypeCompilationDescriptor + -> ByteString +encodePreparedDatatype objects clauses facts descriptor = + encodeCache do + putCacheTag 0x05 + putCacheList putObject (toList objects) + putCacheList putClause (toList clauses) + putCacheList putFact (toList facts) + putDirectAuthorizationCache + (TrustedCompilation + (DatatypeCompilation descriptor)) + where + putObject + (PreparedDatatypeObject + _symbol key coreType identity _asserted) = do + putSemanticGlobalKeyCache key + putCoreTypeCache coreType + putObjectIdCache identity + + putClause (PreparedClause constructor premises) = do + putSemanticGlobalKeyCache + (SemanticExpressionFunction + (Raw.mixfixPattern constructor)) + putCacheList putPremise premises + + putPremise = \case + PreparedRecursivePremise domain -> do + putCacheTag 0x00 + putCanonicalTermCache putObjectIdCache + (frozenCoreTerm domain) + PreparedNonRecursivePremise domain -> do + putCacheTag 0x01 + putCanonicalTermCache putObjectIdCache + (frozenCoreTerm domain) + + putFact fact = do + let Internal.Marker marker = + preparedExactDatatypeFactMarker fact + putCacheText marker + putCanonicalTermCache putObjectIdCache + (frozenCoreTerm + (preparedExactDatatypeFactTarget fact)) + putTheoremRefCache + (preparedExactDatatypeFactReference fact) diff --git a/source/Felix/Checking/Exact/Global.hs b/source/Felix/Checking/Exact/Global.hs new file mode 100644 index 0000000..d4040e6 --- /dev/null +++ b/source/Felix/Checking/Exact/Global.hs @@ -0,0 +1,116 @@ +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE NoImplicitPrelude #-} + +-- | Exact resolution of source symbols to checked semantic globals. +module Felix.Checking.Exact.Global + ( ExactGlobalResolutionError(..) + , resolveExactSourceGlobals + ) where + +import Base +import Felix.Checking.Core +import Felix.Checking.Declaration qualified as Declaration +import Felix.Checking.Exact.Vocabulary +import Felix.Checking.Identity +import Felix.Checking.Semantic +import Felix.Checking.Typed.Inductive qualified as Typed +import Felix.Syntax.Internal qualified as Internal + +import Control.Monad (foldM) +import Control.Monad.Except + ( liftEither + , runExceptT + , throwError + ) +import Control.Monad.Trans.Class (lift) +import Data.Bifunctor (first) +import Data.Map.Strict qualified as Map +import Data.Maybe (catMaybes) +import Data.Set qualified as Set + + +data ExactGlobalResolutionError + = ExactGlobalNotVisible !Internal.Symbol + | ExactGlobalAmbiguous !Internal.Symbol + | ExactGlobalUnsupported !Internal.Symbol + | ExactGlobalContextualUnsupported !Internal.Symbol + | ExactGlobalContentInvalid !CoreCheckError + deriving stock (Show, Eq) + +resolveExactSourceGlobals + :: Set.Set Internal.Symbol + -> Declaration.LoweringDriver + (Either + ExactGlobalResolutionError + ( Map.Map + Internal.Symbol + (Typed.SourceGlobal ObjectId) + , Map.Map ObjectId CoreType + )) +resolveExactSourceGlobals symbols = + runExceptT + (foldM resolve (Map.empty, Map.empty) + (Set.toAscList symbols)) + where + resolve (resolved, types) symbol = + case classifyExactSymbol symbol of + ExactClosedLiteral -> + pure (resolved, types) + ExactFixedPrimitive _meaning -> + pure (resolved, types) + ExactUnsupportedSymbol -> + throwError (ExactGlobalUnsupported symbol) + ExactSourceGlobal keys -> do + matches <- + catMaybes + <$> traverse + (lift + . Declaration.resolveVisibleGlobalContentLowering) + (toList keys) + case matches of + [] -> + throwError (ExactGlobalNotVisible symbol) + [match] -> do + (source, sourceTypes) <- + liftEither (prepareSourceGlobal symbol match) + pure + ( Map.insert symbol source resolved + , Map.union sourceTypes types + ) + _ -> + throwError (ExactGlobalAmbiguous symbol) + +prepareSourceGlobal + :: Internal.Symbol + -> ( SemanticGlobalTarget + , ObjectContent + , Map.Map ObjectId CoreType + ) + -> Either + ExactGlobalResolutionError + (Typed.SourceGlobal ObjectId, Map.Map ObjectId CoreType) +prepareSourceGlobal symbol (target, content, dependencies) = do + body <- + case target of + GlobalReference _identity -> + Right Nothing + TransparentExpansion _identity -> + case content of + TransparentObjectContent _theory _coreType canonical -> + Just + <$> first ExactGlobalContentInvalid + (checkCanonicalCore + (`Map.lookup` dependencies) + canonical) + _ -> + impossible + "validated transparent expansion has opaque content" + ContextualTransparentExpansion _identity _requirements -> + Left (ExactGlobalContextualUnsupported symbol) + let identity = semanticGlobalTargetObject target + types = + Map.insert + identity + (objectContentType content) + dependencies + pure (Typed.SourceGlobal identity body, types) diff --git a/source/Felix/Checking/Exact/Inductive.hs b/source/Felix/Checking/Exact/Inductive.hs new file mode 100644 index 0000000..5817b34 --- /dev/null +++ b/source/Felix/Checking/Exact/Inductive.hs @@ -0,0 +1,838 @@ +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE NoImplicitPrelude #-} + +-- | Exact preparation and atomic publication of direct set inductives. +module Felix.Checking.Exact.Inductive + ( PreparedExactInductive + , preparedExactInductiveCarrierId + , preparedExactInductiveCarrierType + , preparedExactInductiveCarrierBody + , preparedExactInductiveGuardTargets + , preparedExactInductiveFacts + , prepareExactInductive + , CheckedExactInductiveAuthorization + , lowerPreparedExactInductive + , authorizeCheckedExactInductive + , ExactInductiveError(..) + , exactInductiveErrorLocation + , renderExactInductiveError + ) where + +import Base hiding (Empty) +import Felix.Checking.Authority +import Felix.Checking.Core +import Felix.Checking.Declaration qualified as Declaration +import Felix.Checking.Exact.Global qualified as ExactGlobal +import Felix.Checking.Exact.Vocabulary +import Felix.Checking.Foundation +import Felix.Checking.Identity +import Felix.Checking.Semantic +import Felix.Checking.Typed.Inductive qualified as Typed +import Felix.Cache.Codec +import Felix.Meaning qualified as Meaning +import Felix.Report.Location +import Felix.Syntax.Abstract qualified as Raw +import Felix.Syntax.Interface +import Felix.Syntax.Internal qualified as Internal + +import Control.Monad (unless, when) +import Control.Monad.Except (ExceptT) +import Control.Monad.Except qualified as Except +import Data.Bifunctor (first) +import Data.ByteString (ByteString) +import Data.List qualified as List +import Data.List.NonEmpty qualified as NonEmpty +import Data.Map.Strict qualified as Map +import Data.Set qualified as Set +import Data.Text qualified as Text +import Data.Vector qualified as Vector + + +data PreparedExactInductive = PreparedExactInductive + !Location + !SemanticGlobalKey + !ObjectId + !(Maybe AssertedObject) + !SemanticName + !DeclarationSyntaxId + !(Typed.PreparedTypedInductive ObjectId) + ![SemanticFactOccurrenceFingerprint] + +data CheckedExactInductiveAuthorization = + CheckedExactInductiveAuthorization + !ObjectId + !(Typed.PreparedTypedInductive ObjectId) + ![SemanticFactOccurrenceFingerprint] + ![(Location, Declaration.PreparedVampireObligation Void ())] + +preparedExactInductiveCarrierId + :: PreparedExactInductive + -> ObjectId +preparedExactInductiveCarrierId + (PreparedExactInductive + _location _key identity _asserted _alias _syntax _typed _guards) = + identity + +preparedExactInductiveCarrierType + :: PreparedExactInductive + -> CoreType +preparedExactInductiveCarrierType + (PreparedExactInductive + _location _key _identity _asserted _alias _syntax typed _guards) = + Typed.typedInductiveCarrierType typed + +preparedExactInductiveCarrierBody + :: PreparedExactInductive + -> FrozenCheckedCore ObjectId +preparedExactInductiveCarrierBody + (PreparedExactInductive + _location _key _identity _asserted _alias _syntax typed _guards) = + Typed.typedInductiveCarrierBody typed + +preparedExactInductiveGuardTargets + :: PreparedExactInductive + -> Vector.Vector (FrozenCheckedCore ObjectId) +preparedExactInductiveGuardTargets + (PreparedExactInductive + _location _key _identity _asserted _alias _syntax typed _guards) = + Typed.typedInductiveGuardTargets typed + +preparedExactInductiveFacts + :: PreparedExactInductive + -> NonEmpty (Typed.PreparedTypedInductiveFact ObjectId) +preparedExactInductiveFacts + (PreparedExactInductive + _location _key _identity _asserted _alias _syntax typed _guards) = + Typed.typedInductiveFacts typed + +data ExactInductiveError + = ExactInductiveUnsupportedBlock !Location + | ExactInductiveOccurrenceMissing !Location + | ExactInductiveOccurrenceAmbiguous !Location + | ExactInductiveHeadMismatch !Location + | ExactInductiveGlossFailed !Location !Meaning.GlossError + | ExactInductiveDuplicateParameter !Location !Internal.VarSymbol + | ExactInductiveDomainFreeVariable !Location !Internal.VarSymbol + | ExactInductiveDomainMentionsCarrier !Location + | ExactInductiveResultShape !Location + | ExactInductiveResultMentionsCarrier !Location + | ExactInductiveRecursiveTermMentionsCarrier !Location + | ExactInductiveRecursiveCarrierWrongArguments !Location + | ExactInductiveRecursiveCarrierOutsideMembership !Location + | ExactInductiveUnsupportedRecursiveCarrierContext !Location + | ExactInductiveFixedSemanticCollision !Location !SemanticGlobalKey + | ExactInductiveGlobalAlreadyVisible !Location !SemanticGlobalKey + | ExactInductiveGlobalNotVisible !Location !Internal.Symbol + | ExactInductiveGlobalAmbiguous !Location !Internal.Symbol + | ExactInductiveUnsupportedSymbol !Location !Internal.Symbol + | ExactInductiveGlobalContentInvalid !Location !CoreCheckError + | ExactInductivePreparationFailed + !Location + !Typed.TypedInductiveError + | ExactInductiveGuardMissing !Location + | ExactInductiveGuardAmbiguous !Location + deriving stock (Show, Eq) + +exactInductiveErrorLocation :: ExactInductiveError -> Location +exactInductiveErrorLocation = \case + ExactInductiveUnsupportedBlock location -> location + ExactInductiveOccurrenceMissing location -> location + ExactInductiveOccurrenceAmbiguous location -> location + ExactInductiveHeadMismatch location -> location + ExactInductiveGlossFailed location _failure -> location + ExactInductiveDuplicateParameter location _parameter -> location + ExactInductiveDomainFreeVariable location _variable -> location + ExactInductiveDomainMentionsCarrier location -> location + ExactInductiveResultShape location -> location + ExactInductiveResultMentionsCarrier location -> location + ExactInductiveRecursiveTermMentionsCarrier location -> location + ExactInductiveRecursiveCarrierWrongArguments location -> location + ExactInductiveRecursiveCarrierOutsideMembership location -> location + ExactInductiveUnsupportedRecursiveCarrierContext location -> location + ExactInductiveFixedSemanticCollision location _key -> location + ExactInductiveGlobalAlreadyVisible location _key -> location + ExactInductiveGlobalNotVisible location _symbol -> location + ExactInductiveGlobalAmbiguous location _symbol -> location + ExactInductiveUnsupportedSymbol location _symbol -> location + ExactInductiveGlobalContentInvalid location _failure -> location + ExactInductivePreparationFailed location _failure -> location + ExactInductiveGuardMissing location -> location + ExactInductiveGuardAmbiguous location -> location + +renderExactInductiveError :: ExactInductiveError -> Text +renderExactInductiveError failure = + locationToText (exactInductiveErrorLocation failure) + <> ": " + <> case failure of + ExactInductiveUnsupportedBlock{} -> + "this inductive source form is not supported by the typed checker" + ExactInductiveOccurrenceMissing{} -> + "the inductive declaration has no associated syntax occurrence" + ExactInductiveOccurrenceAmbiguous{} -> + "the inductive declaration has more than one semantic head" + ExactInductiveHeadMismatch{} -> + "the inductive head does not match its syntax occurrence" + ExactInductiveGlossFailed _location glossFailure -> + "inductive elaboration failed: " <> shown glossFailure + ExactInductiveDuplicateParameter _location parameter -> + "the inductive parameter is repeated: " <> shown parameter + ExactInductiveDomainFreeVariable _location variable -> + "the inductive domain contains an unbound variable: " + <> shown variable + ExactInductiveDomainMentionsCarrier{} -> + "the inductive domain must be independent of its carrier" + ExactInductiveResultShape{} -> + "an inductive result must have the form t \\in F(args)" + ExactInductiveResultMentionsCarrier{} -> + "an inductive result term must not mention its carrier" + ExactInductiveRecursiveTermMentionsCarrier{} -> + "a recursive occurrence must be in the carrier of a membership premise" + ExactInductiveRecursiveCarrierWrongArguments{} -> + "the inductive carrier occurs with arguments other than its declared parameters" + ExactInductiveRecursiveCarrierOutsideMembership{} -> + "an inductive carrier occurrence must be in the set operand of a membership premise" + ExactInductiveUnsupportedRecursiveCarrierContext{} -> + "this recursive carrier context is outside the supported first-order set-term fragment" + ExactInductiveFixedSemanticCollision _location key -> + "the inductive carrier collides with fixed semantics for " + <> shown key + ExactInductiveGlobalAlreadyVisible _location key -> + "the inductive carrier is already visible: " <> shown key + ExactInductiveGlobalNotVisible _location symbol -> + "an inductive source symbol is not visible: " <> shown symbol + ExactInductiveGlobalAmbiguous _location symbol -> + "an inductive source symbol has more than one meaning: " + <> shown symbol + ExactInductiveUnsupportedSymbol _location symbol -> + "this inductive source symbol is not supported: " + <> shown symbol + ExactInductiveGlobalContentInvalid _location coreFailure -> + "an inductive global has invalid checked content: " + <> shown coreFailure + ExactInductivePreparationFailed _location typedFailure -> + "typed inductive preparation failed: " <> shown typedFailure + ExactInductiveGuardMissing{} -> + "an inductive domain guard has no visible authorized fact" + ExactInductiveGuardAmbiguous{} -> + "an inductive domain guard matches more than one visible fact" + where + shown :: Show value => value -> Text + shown = Text.pack . show + +type Prepare = + ExceptT + ExactInductiveError + (Declaration.LoweringDriver) + +prepareExactInductive + :: CheckedFoundation + -> Raw.Block + -> [CanonicalLexicalEntry] + -> Declaration.LoweringDriver + (Either ExactInductiveError PreparedExactInductive) +prepareExactInductive foundation block entries = + Except.runExceptT do + (location, marker, rawInductive) <- + case block of + Raw.BlockInductive blockLocation _title blockMarker inductive -> + pure (blockLocation, blockMarker, inductive) + _ -> + Except.throwError + (ExactInductiveUnsupportedBlock (locate block)) + key <- validateOccurrence location rawInductive entries + when + (isJust (fixedSemanticMeaning key)) + (Except.throwError + (ExactInductiveFixedSemanticCollision location key)) + visible <- + Except.lift + (Declaration.resolveVisibleGlobalLowering key) + when (isJust visible) + (Except.throwError + (ExactInductiveGlobalAlreadyVisible location key)) + internal <- + case Meaning.meaning [block] of + Right + [Internal.BlockInductive + _internalLocation _internalMarker inductive] -> + pure inductive + Left failure -> + Except.throwError + (ExactInductiveGlossFailed location failure) + Right _ -> + Except.throwError + (ExactInductiveUnsupportedBlock location) + direct <- + Except.liftEither + (normalizeDirectInductive internal) + (sourceGlobals, globalTypes) <- + resolveSourceGlobals location internal direct + typed <- + Except.liftEither + (first + (ExactInductivePreparationFailed location) + (Typed.prepareTypedInductive + (requireGlobalType globalTypes) + foundation + (`Map.lookup` sourceGlobals) + marker + direct)) + guards <- + traverse + (resolveGuard location) + (Vector.toList + (Typed.typedInductiveGuardTargets typed)) + theory <- Except.lift Declaration.currentTheoryLowering + let carrierType = Typed.typedInductiveCarrierType typed + carrierBody = Typed.typedInductiveCarrierBody typed + carrierTerm = frozenCoreTerm carrierBody + identity = + transparentObjectId theory carrierType carrierTerm + content = + TransparentObjectContent theory carrierType carrierTerm + alias = case marker of + Raw.Marker name -> semanticName name + available <- + Except.lift + (Declaration.objectAvailableLowering identity) + let asserted + | available = Nothing + | otherwise = Just (assertedObject identity content) + syntax = + declarationSyntaxId + (encodePreparedInductive key alias typed) + pure + (PreparedExactInductive + location + key + identity + asserted + alias + syntax + typed + guards) + where + requireGlobalType types identity = + fromMaybe + (impossible + "prepared inductive global has no checked type") + (Map.lookup identity types) + +validateOccurrence + :: Location + -> Raw.Inductive + -> [CanonicalLexicalEntry] + -> Prepare SemanticGlobalKey +validateOccurrence location rawInductive entries = do + entry <- + case entries of + [] -> + Except.throwError + (ExactInductiveOccurrenceMissing location) + [single] -> pure single + _ -> + Except.throwError + (ExactInductiveOccurrenceAmbiguous location) + key <- + maybe + (Except.throwError + (ExactInductiveHeadMismatch location)) + pure + (semanticGlobalKeyFromLexicalEntry entry) + let Raw.SymbolPattern headSymbol _parameters = + Raw.inductiveSymbolPattern rawInductive + expected = + SemanticExpressionFunction + (Raw.mixfixPattern headSymbol) + unless (key == expected) + (Except.throwError + (ExactInductiveHeadMismatch location)) + pure key + +normalizeDirectInductive + :: Internal.Inductive + -> Either ExactInductiveError Typed.DirectInductive +normalizeDirectInductive inductive = do + case firstDuplicate (Internal.inductiveParams inductive) of + Just duplicate -> + Left + (ExactInductiveDuplicateParameter + (locate duplicate) + duplicate) + Nothing -> pure () + let parameters = Internal.inductiveParams inductive + parameterSet = Set.fromList parameters + domain = Internal.inductiveDomain inductive + carrier = Internal.inductiveSymbol inductive + domainVariables = + orderedUnique + (toList domain) + case find (`Set.notMember` parameterSet) domainVariables of + Just variable -> + Left + (ExactInductiveDomainFreeVariable + (locate variable) + variable) + Nothing -> pure () + when + (Internal.SymbolMixfix carrier + `Set.member` Internal.mentionedSymbols domain) + (Left + (ExactInductiveDomainMentionsCarrier + (termLocation domain))) + clauses <- + traverse + (normalizeClause carrier parameters) + (Internal.inductiveIntros inductive) + pure + (Typed.DirectInductive + parameters + domain + clauses) + +normalizeClause + :: Internal.FunctionSymbol + -> [Internal.VarSymbol] + -> Internal.IntroRule + -> Either ExactInductiveError Typed.DirectInductiveClause +normalizeClause carrier parameters rule = do + conditions <- + traverse + (normalizeCondition carrier parameters) + (Internal.introConditions rule) + result <- + normalizeResult + carrier + parameters + (Internal.introResult rule) + let parameterSet = Set.fromList parameters + variables = + List.filter (`Set.notMember` parameterSet) + (orderedUnique + ( concatMap toList + (Internal.introConditions rule) + <> toList result + )) + pure + (Typed.DirectInductiveClause + variables + conditions + result) + +normalizeResult + :: Internal.FunctionSymbol + -> [Internal.VarSymbol] + -> Internal.Formula + -> Either ExactInductiveError Internal.Term +normalizeResult carrier parameters = \case + Internal.IsElementOf _location result target + | not (matchesCarrier carrier parameters target) -> + Left (ExactInductiveResultShape (termLocation target)) + | Internal.SymbolMixfix carrier + `Set.member` Internal.mentionedSymbols result -> + Left + (ExactInductiveResultMentionsCarrier + (termLocation result)) + | otherwise -> + Right result + formula -> + Left (ExactInductiveResultShape (termLocation formula)) + +normalizeCondition + :: Internal.FunctionSymbol + -> [Internal.VarSymbol] + -> Internal.Formula + -> Either ExactInductiveError Typed.DirectInductiveCondition +normalizeCondition carrier parameters formula + | not + (Internal.SymbolMixfix carrier + `Set.member` Internal.mentionedSymbols formula) = + Right (Typed.DirectSideCondition formula) + | otherwise = + case formula of + Internal.IsElementOf _location recursiveTerm recursiveCarrier + | Internal.SymbolMixfix carrier + `Set.member` + Internal.mentionedSymbols recursiveTerm -> + Left + (ExactInductiveRecursiveTermMentionsCarrier + (termLocation recursiveTerm)) + | otherwise -> do + context <- + first recursiveCarrierContextError + (Typed.prepareRecursiveCarrierContext + carrier parameters recursiveCarrier) + Right + (Typed.DirectRecursiveCondition + recursiveTerm context) + _ -> + Left + (ExactInductiveRecursiveCarrierOutsideMembership + (termLocation formula)) + +recursiveCarrierContextError + :: Typed.RecursiveCarrierContextError + -> ExactInductiveError +recursiveCarrierContextError = \case + Typed.RecursiveCarrierWrongArguments location -> + ExactInductiveRecursiveCarrierWrongArguments location + Typed.RecursiveCarrierUnsupportedContext location -> + ExactInductiveUnsupportedRecursiveCarrierContext location + +matchesCarrier + :: Internal.FunctionSymbol + -> [Internal.VarSymbol] + -> Internal.Term + -> Bool +matchesCarrier carrier parameters = \case + Internal.TermSymbol _location (Internal.SymbolMixfix actual) arguments -> + actual == carrier + && length arguments == length parameters + && and + (zipWith + (\argument parameter -> + argument == Internal.TermVar parameter) + arguments + parameters) + _ -> False + +resolveSourceGlobals + :: Location + -> Internal.Inductive + -> Typed.DirectInductive + -> Prepare + ( Map.Map + Internal.Symbol + (Typed.SourceGlobal ObjectId) + , Map.Map ObjectId CoreType + ) +resolveSourceGlobals location internal direct = + Except.lift + (ExactGlobal.resolveExactSourceGlobals symbols) + >>= Except.liftEither + . first (exactGlobalError location) + where + carrier = Internal.SymbolMixfix (Internal.inductiveSymbol internal) + symbols = + Set.delete carrier (directSymbols direct) + +exactGlobalError + :: Location + -> ExactGlobal.ExactGlobalResolutionError + -> ExactInductiveError +exactGlobalError location = \case + ExactGlobal.ExactGlobalNotVisible symbol -> + ExactInductiveGlobalNotVisible location symbol + ExactGlobal.ExactGlobalAmbiguous symbol -> + ExactInductiveGlobalAmbiguous location symbol + ExactGlobal.ExactGlobalUnsupported symbol -> + ExactInductiveUnsupportedSymbol location symbol + ExactGlobal.ExactGlobalContextualUnsupported symbol -> + ExactInductiveUnsupportedSymbol location symbol + ExactGlobal.ExactGlobalContentInvalid failure -> + ExactInductiveGlobalContentInvalid location failure + +resolveGuard + :: Location + -> FrozenCheckedCore ObjectId + -> Prepare SemanticFactOccurrenceFingerprint +resolveGuard location target = do + matches <- + Except.lift + (Declaration.resolveVisibleFactTargetsLowering target) + case matches of + [] -> + Except.throwError (ExactInductiveGuardMissing location) + [fingerprint] -> + pure fingerprint + _ -> + Except.throwError (ExactInductiveGuardAmbiguous location) + +directSymbols :: Typed.DirectInductive -> Set.Set Internal.Symbol +directSymbols direct = + Internal.mentionedSymbols (Typed.directInductiveDomain direct) + <> foldMap clauseSymbols + (Typed.directInductiveClauses direct) + where + clauseSymbols clause = + foldMap conditionSymbols + (Typed.directClauseConditions clause) + <> Internal.mentionedSymbols + (Typed.directClauseResult clause) + conditionSymbols = \case + Typed.DirectSideCondition formula -> + Internal.mentionedSymbols formula + Typed.DirectRecursiveCondition term context -> + Internal.mentionedSymbols term + <> Typed.recursiveCarrierContextSymbols context + +lowerPreparedExactInductive + :: PreparedExactInductive + -> Declaration.LoweringDriver + (Either + Declaration.DeclarationError + (Declaration.CheckedDeclaration + CheckedExactInductiveAuthorization)) +lowerPreparedExactInductive + (PreparedExactInductive + _location key identity asserted alias syntax typed guards) = + do + let facts = Typed.typedInductiveFacts typed + monotonicities = + Vector.toList + (Typed.typedInductiveMonotonicities typed) + objects = maybeToList asserted + definition <- + Declaration.prepareDefinitionEquationSpecLowering + objects identity alias + preparedMonotonicities <- + traverse + (\monotonicity -> Except.runExceptT do + let factLocation = + Typed.typedInductiveMonotonicityLocation + monotonicity + target = + Typed.typedInductiveMonotonicityTarget + monotonicity + spec <- + Except.lift + (Declaration.prepareFrozenCandidateSpecLowering + objects target SearchIneligible []) + >>= Except.liftEither + obligation <- + Except.lift + (Declaration.prepareScopedVampireObligationLowering + Vector.empty + (embedClosedCore [] target) + [] + [] + Declaration.VampireImplicitPremises) + >>= either + (Except.throwError + . Declaration.ProofObligationFailedAt + factLocation + . Declaration.CurrentCandidateVampirePreparationFailed) + pure + pure + ( Declaration.checkedCandidate + spec + (Declaration.checkedSourceProofPlanning + [ Declaration.checkedPlannedVampireRequest + factLocation obligation + ] + []) + , (factLocation, obligation) + )) + monotonicities + preparedCandidates <- + traverse + (\fact -> do + prepared <- + Declaration.prepareCandidateSpecLowering + objects + (embedClosedCore [] + (Typed.typedInductiveFactTarget fact)) + SearchEligible + [markerAlias + (Typed.typedInductiveFactMarker fact)] + let descriptor = + GuardedFoundationRules + (guardedRuleSet + (Typed.typedInductiveFactRules fact)) + planning + | null monotonicities = + Declaration.checkedKernelPlanning + descriptor guards + | otherwise = + Declaration.checkedKernelPlanningWithStaged + descriptor + guards + (if Typed.typedInductiveFactRequiresMonotonicities + fact + then + [ Declaration.plannedEarlierCandidate + 1 index + | (index, _target) <- + zip [0 ..] monotonicities + ] + else []) + pure + (fmap + (\spec -> + Declaration.checkedCandidate spec planning) + prepared)) + facts + pure do + definitionSpec <- definition + monotonicityCandidates <- sequence preparedMonotonicities + factCandidates <- sequence preparedCandidates + let stages + | null monotonicityCandidates = + [ Declaration.checkedCandidate definitionSpec + (Declaration.checkedDefinitionEquationPlanning identity) + :| toList factCandidates + ] + | otherwise = + [ Declaration.checkedCandidate definitionSpec + (Declaration.checkedDefinitionEquationPlanning identity) + :| [] + , NonEmpty.fromList (fst <$> monotonicityCandidates) + , factCandidates + ] + pure + (Declaration.checkedCompiledDeclaration + syntax + objects + [] + [semanticGlobalBinding key (GlobalReference identity)] + [] + stages + (CheckedExactInductiveAuthorization + identity typed guards + (snd <$> monotonicityCandidates))) + where + markerAlias (Raw.Marker name) = + semanticName name + +authorizeCheckedExactInductive + :: CheckedExactInductiveAuthorization + -> [NonEmpty Declaration.ReservedCandidate] + -> Declaration.Declaration () +authorizeCheckedExactInductive + (CheckedExactInductiveAuthorization + identity typed guards monotonicityObligations) = \case + [definitionCandidate :| candidates] -> do + unless (null monotonicityObligations) + (Declaration.failDeclaration + (Declaration.CheckedAuthorizationCandidateShapeMismatch 3 1)) + Declaration.authorizeDefinitionEquationCandidate + identity definitionCandidate + let facts = Typed.typedInductiveFacts typed + case NonEmpty.nonEmpty candidates of + Just factCandidates + | NonEmpty.length factCandidates == NonEmpty.length facts -> + sequence_ + (NonEmpty.zipWith + (authorizeFact []) + factCandidates + facts) + _ -> + Declaration.failDeclaration + (Declaration.CheckedAuthorizationCandidateShapeMismatch + (1 + NonEmpty.length facts) + (1 + length candidates)) + [ definitionCandidate :| [] + , monotonicityCandidates + , factCandidates + ] + | NonEmpty.length monotonicityCandidates + == length monotonicityObligations + , NonEmpty.length factCandidates + == NonEmpty.length (Typed.typedInductiveFacts typed) -> do + obligations <- + maybe + (Declaration.failDeclaration + (Declaration.CheckedAuthorizationCandidateShapeMismatch + 1 0)) + pure + (NonEmpty.nonEmpty monotonicityObligations) + Declaration.authorizeDefinitionEquationCandidate + identity definitionCandidate + Declaration.authorizeVampireCandidateBatch + (NonEmpty.zipWith + (\candidate (factLocation, obligation) -> + (factLocation, candidate, pure obligation)) + monotonicityCandidates + obligations) + sequence_ + (NonEmpty.zipWith + (\candidate fact -> + authorizeFact + (if Typed.typedInductiveFactRequiresMonotonicities + fact + then NonEmpty.toList monotonicityCandidates + else []) + candidate + fact) + factCandidates + (Typed.typedInductiveFacts typed)) + stages -> + Declaration.failDeclaration + (Declaration.CheckedAuthorizationCandidateShapeMismatch + (if null monotonicityObligations then 1 else 3) + (length stages)) + where + authorizeFact monotonicityCandidates candidate fact = + Declaration.authorizeKernelConstructionCandidate + (GuardedFoundationRules + (guardedRuleSet + (Typed.typedInductiveFactRules fact))) + candidate do + traverse_ Declaration.useAuthorizedFact guards + traverse_ + Declaration.useStagedCandidate + monotonicityCandidates + pure (Typed.typedInductiveFactDerivation fact) + + +encodePreparedInductive + :: SemanticGlobalKey + -> SemanticName + -> Typed.PreparedTypedInductive ObjectId + -> ByteString +encodePreparedInductive key alias typed = + encodeCache do + putCacheTag 0x04 + putSemanticGlobalKeyCache key + putCoreTypeCache + (Typed.typedInductiveCarrierType typed) + putCanonicalTermCache putObjectIdCache + (frozenCoreTerm + (Typed.typedInductiveCarrierBody typed)) + putCacheList putFrozenTerm + (Vector.toList + (Typed.typedInductiveContextInventory typed)) + putCacheList + (putFrozenTerm + . Typed.typedInductiveMonotonicityTarget) + (Vector.toList + (Typed.typedInductiveMonotonicities typed)) + putCacheText (semanticNameText alias) + putCacheList putFact + (toList (Typed.typedInductiveFacts typed)) + where + putFrozenTerm = + putCanonicalTermCache putObjectIdCache . frozenCoreTerm + + putFact fact = do + let Raw.Marker marker = + Typed.typedInductiveFactMarker fact + putCacheText marker + putCanonicalTermCache putObjectIdCache + (frozenCoreTerm + (Typed.typedInductiveFactTarget fact)) + putCacheList + (putCacheBytes . encodeKernelRuleTag) + (toList (Typed.typedInductiveFactRules fact)) + +firstDuplicate :: Ord value => [value] -> Maybe value +firstDuplicate = + go Set.empty + where + go _seen [] = Nothing + go seen (value : remaining) + | value `Set.member` seen = Just value + | otherwise = + go (Set.insert value seen) remaining + +orderedUnique :: Ord value => [value] -> [value] +orderedUnique = + reverse . snd . foldl' step (Set.empty, []) + where + step (seen, values) value + | value `Set.member` seen = (seen, values) + | otherwise = + (Set.insert value seen, value : values) + +termLocation :: Internal.Expr -> Location +termLocation = Internal.exprLocation diff --git a/source/Felix/Checking/Exact/Proof.hs b/source/Felix/Checking/Exact/Proof.hs new file mode 100644 index 0000000..e2149c4 --- /dev/null +++ b/source/Felix/Checking/Exact/Proof.hs @@ -0,0 +1,2639 @@ +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE NoImplicitPrelude #-} + +-- | Exact lowering for the first ordinary theorem/proof fragment. +-- +-- This module is the trusted owner of structural local-proof composition. Its +-- private prepared tree controls when assumptions and proved local claims +-- become available and executes discharges depth-first. The declaration +-- boundary validates typed tasks and authority; it does not reconstruct this +-- derivation. +module Felix.Checking.Exact.Proof + ( PreparedExactProof + , preparedExactProofSyntaxId + , preparedExactProofFirstOmission + , prepareExactProof + , CheckedExactProofAuthorization + , lowerPreparedExactProof + , authorizeCheckedExactProof + , PreparedFinalPreludeFoundationClaim + , prepareFinalPreludeFoundationClaim + , CheckedFinalPreludeFoundationAuthorization + , lowerPreparedFinalPreludeFoundationClaim + , authorizeCheckedFinalPreludeFoundationClaim + , ExactProofError(..) + , exactProofErrorLocation + , renderExactProofError + ) where + +import Base +import Felix.Checking.Authority qualified as Authority +import Felix.Checking.Backend.Problem qualified as Backend +import Felix.Checking.Core +import Felix.Checking.Declaration qualified as Declaration +import Felix.Checking.Exact qualified as Exact +import Felix.Checking.Foundation +import Felix.Checking.Identity +import Felix.Checking.Kernel.Derivation (foundationFactDerivation) +import Felix.Checking.Kernel.Proof qualified as KernelProof +import Felix.Checking.SetConstruction +import Felix.Checking.Semantic +import Felix.Cache.Codec +import Felix.Report.Location +import Felix.Syntax.Abstract qualified as Raw + +import Control.Monad.Except (ExceptT) +import Control.Monad.Except qualified as Except +import Control.Monad (foldM, unless, when) +import Control.Monad.State.Strict (StateT) +import Control.Monad.State.Strict qualified as State +import Data.ByteString (ByteString) +import Data.List.NonEmpty qualified as NonEmpty +import Data.Map.Strict qualified as Map +import Data.Set qualified as Set +import Data.Text qualified as Text +import Data.Vector (Vector) +import Data.Vector qualified as Vector +import Numeric.Natural (Natural) + + +data ExactProofError + = ExactProofUnsupportedClaim !Location + | ExactProofUnsupportedStep !Location + | ExactProofSetInductionVariableRequired !Location + | ExactProofSetInductionVariableNotActive + !Location !Raw.VarSymbol + | ExactProofSetInductionFocusAmbiguous !Location + | ExactProofSetInductionActiveBinderIneligible + !Location !Raw.VarSymbol + | ExactProofSetInductionBinderConflict + !Location !Raw.VarSymbol + | ExactProofSetInductionGoalMismatch !Location + | ExactProofSetExtensionalityGoalMismatch !Location + | ExactProofSetExtensionalityDirectionsUnavailable !Location + | ExactProofExpectedUniversalGoal !Location + | ExactProofExpectedImplicationGoal !Location + | ExactProofGoalStatementMismatch !Location + | ExactProofEmptyCaseSplit !Location + | ExactProofStructuralCompositionFailed + !Location !KernelProof.KernelProofBuildError + | ExactProofLocalFunctionBinderMismatch !Location + | ExactProofLocalFunctionNameConflict !Location + | ExactProofUnknownReference !Location !Raw.Marker + | ExactProofElaborationFailed !Exact.ExactCompileError + | ExactProofObligationPreparationFailed + !Location + !(Declaration.VampireObligationPreparationError + Exact.ExactLocalId) + | ExactProofFoundationLeafRequiresImplicitAuto !Location + | ExactProofFoundationLeafTargetMismatch !Location + | ExactProofFoundationLeafTargetAmbiguous !Location + deriving stock (Show, Eq) + +exactProofErrorLocation :: ExactProofError -> Location +exactProofErrorLocation = \case + ExactProofUnsupportedClaim location -> location + ExactProofUnsupportedStep location -> location + ExactProofSetInductionVariableRequired location -> location + ExactProofSetInductionVariableNotActive location _variable -> + location + ExactProofSetInductionFocusAmbiguous location -> location + ExactProofSetInductionActiveBinderIneligible location _variable -> + location + ExactProofSetInductionBinderConflict location _variable -> + location + ExactProofSetInductionGoalMismatch location -> location + ExactProofSetExtensionalityGoalMismatch location -> location + ExactProofSetExtensionalityDirectionsUnavailable location -> location + ExactProofExpectedUniversalGoal location -> location + ExactProofExpectedImplicationGoal location -> location + ExactProofGoalStatementMismatch location -> location + ExactProofEmptyCaseSplit location -> location + ExactProofStructuralCompositionFailed location _failure -> location + ExactProofLocalFunctionBinderMismatch location -> location + ExactProofLocalFunctionNameConflict location -> location + ExactProofUnknownReference location _marker -> location + ExactProofElaborationFailed failure -> + Exact.exactCompileErrorLocation failure + ExactProofObligationPreparationFailed location _failure -> location + ExactProofFoundationLeafRequiresImplicitAuto location -> location + ExactProofFoundationLeafTargetMismatch location -> location + ExactProofFoundationLeafTargetAmbiguous location -> location + +renderExactProofError :: ExactProofError -> Text +renderExactProofError = \case + ExactProofUnsupportedClaim location -> + 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" + ExactProofSetInductionVariableRequired location -> + at location <> "exact set induction requires a named set variable" + ExactProofSetInductionVariableNotActive location variable -> + at location <> "the set-induction variable " <> shown variable + <> " is not an eligible exact focus" + ExactProofSetInductionFocusAmbiguous location -> + at location + <> "set induction without an explicit variable has no unique focus" + ExactProofSetInductionActiveBinderIneligible location variable -> + at location <> "the active binder " <> shown variable + <> " is not an eligible set-induction focus" + ExactProofSetInductionBinderConflict location variable -> + at location <> "the leading set-induction binder " <> shown variable + <> " conflicts with an active exact binder" + ExactProofSetInductionGoalMismatch location -> + at location <> "the set-induction variable does not belong to this goal" + ExactProofSetExtensionalityGoalMismatch location -> + at location <> "set extensionality requires a set-equality goal" + ExactProofSetExtensionalityDirectionsUnavailable location -> + at location + <> "set extensionality requires both directions as proved local claims" + ExactProofExpectedUniversalGoal location -> + at location <> "this fix step requires a universal goal" + ExactProofExpectedImplicationGoal location -> + at location <> "this assume step requires an implication goal" + ExactProofGoalStatementMismatch location -> + at location <> "the proof step does not match the current goal" + ExactProofEmptyCaseSplit location -> + at location <> "case analysis requires at least one case" + ExactProofStructuralCompositionFailed location failure -> + at location <> "invalid structural proof composition: " <> shown failure + 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 -> + Exact.renderExactCompileError failure + ExactProofObligationPreparationFailed location failure -> + at location <> "the exact proof obligation is invalid: " <> shown failure + ExactProofFoundationLeafRequiresImplicitAuto location -> + at location + <> "a confined foundation claim requires an implicit Auto proof" + ExactProofFoundationLeafTargetMismatch location -> + at location <> "the claim does not exactly match a foundation axiom" + ExactProofFoundationLeafTargetAmbiguous location -> + at location <> "the claim matches more than one foundation axiom" + where + at location = locationToText location <> ": " + shown :: Show value => value -> Text + shown = Text.pack . show + +data ExactLocalOrigin + = ExactAssumption + | ExactDerivedClaim + | ExactLocalDefinition + | ExactLocalConstructionExtensional + | ExactLocalConstructionEquation + deriving stock (Show, Eq, Ord) + +data PreparedLocal = PreparedLocal + !Backend.LocalPremiseOrdinal + !ExactLocalOrigin + !(Vector (Exact.ExactLocalId, CoreType)) + !(ScopedCheckedCore ObjectId) + +data PreparedJustification + = PreparedAuto + | PreparedReferences + !(NonEmpty SemanticFactOccurrenceFingerprint) + | PreparedLocalOnly + +data PreparedDischarge + = PreparedVampireDischarge + !Location + !PreparedJustification + !(ScopedCheckedCore ObjectId) + !(Declaration.PreparedVampireObligation + Exact.ExactLocalId + ExactLocalOrigin) + | PreparedSetExtensionality + !Location + !(ScopedCheckedCore ObjectId) + +data PreparedCalculationLink = PreparedCalculationLink + !(ScopedCheckedCore ObjectId) + !PreparedDischarge + +-- The private constructor stores every destination with the discharge derived +-- from its immediately preceding endpoint. Planning and admission can +-- therefore traverse one immutable sequence without re-associating shapes. +data PreparedCalculation = PreparedCheckedCalculation + !CoreType + ![Exact.ExactLocalId] + !(Maybe (ScopedCheckedCore ObjectId)) + !(ScopedCheckedCore ObjectId) + !(NonEmpty PreparedCalculationLink) + !(ScopedCheckedCore ObjectId) + +data PreparedSinceEvidence + = PreparedSinceExisting !PreparedLocal + | PreparedSinceDischarged !PreparedDischarge !PreparedLocal + +data PreparedCase = PreparedCase + !(ScopedCheckedCore ObjectId) + !PreparedProof + +data PreparedCaseAnalysis = PreparedCaseAnalysis + !(ScopedCheckedCore ObjectId) + !(NonEmpty PreparedCase) + !(ScopedCheckedCore ObjectId) + !PreparedDischarge + +data InitialSetInductionFocus = InitialSetInductionFocus + !Raw.VarSymbol + !Exact.ExactLocalId + !Natural + +data InitialSetInductionView = InitialSetInductionView + ![InitialSetInductionFocus] + !(Vector (Exact.ExactLocalId, CoreType)) + !(ScopedCheckedCore ObjectId) + ![ScopedCheckedCore ObjectId] + !(ScopedCheckedCore ObjectId) + !(Maybe Raw.VarSymbol) + +data SetInductionBoundary + = InitialClaimInduction !InitialSetInductionView + -- A direct source-statement goal may retain only its leading binder name. + -- Recursive proof transformations deliberately discard this hint. + | SourceStatementInduction !(Maybe Raw.VarSymbol) + | RecursiveProofInduction + +data SelectedSetInductionFocus + = SelectedInitialSetInduction !InitialSetInductionFocus + | SelectedLeadingSetInduction !(Maybe Raw.VarSymbol) + +data PreparedSetInductionFocus + = PreparedInitialSetInductionFocus + !Exact.ExactLocalId + !Natural + | PreparedLeadingSetInductionFocus + !Exact.ExactLocalId + +data PreparedSetInduction = PreparedCheckedSetInduction + !PreparedSetInductionFocus + !(ScopedCheckedCore ObjectId) + ![ScopedCheckedCore ObjectId] + !(ScopedCheckedCore ObjectId) + !(ScopedCheckedCore ObjectId) + !(ScopedCheckedCore ObjectId) + !PreparedProof + +data PreparedProof + = PreparedImplicitAuto !PreparedDischarge + | PreparedQed !PreparedDischarge + | PreparedOmitted + !Location + !(ScopedCheckedCore ObjectId) + | PreparedFix ![Exact.ExactLocalId] !PreparedProof + | PreparedAssume + !(ScopedCheckedCore ObjectId) + !PreparedProof + | PreparedTake + ![Exact.ExactLocalId] + !(ScopedCheckedCore ObjectId) + !PreparedDischarge + !PreparedProof + | PreparedSetInduction !PreparedSetInduction + | PreparedHave + !(ScopedCheckedCore ObjectId) + !PreparedDischarge + !PreparedProof + | PreparedSuffices + !(ScopedCheckedCore ObjectId) + !(ScopedCheckedCore ObjectId) + !(ScopedCheckedCore ObjectId) + !PreparedDischarge + !PreparedProof + | PreparedCalculate + !PreparedCalculation + !PreparedProof + | PreparedSince + !(ScopedCheckedCore ObjectId) + !PreparedSinceEvidence + !(ScopedCheckedCore ObjectId) + !PreparedDischarge + !PreparedProof + | PreparedSubclaim + !(ScopedCheckedCore ObjectId) + !PreparedProof + !PreparedProof + | PreparedDefine + !Exact.ExactLocalId + !(ScopedCheckedCore ObjectId) + !(NonEmpty (ScopedCheckedCore ObjectId)) + !PreparedProof + | PreparedDefineRelational + !Exact.ExactLocalId + !(ScopedCheckedCore ObjectId) + !PreparedDischarge + !(NonEmpty (ScopedCheckedCore ObjectId)) + !PreparedProof + | PreparedDefineFunction + !Exact.ExactLocalId + !(ScopedCheckedCore ObjectId) + !(ScopedCheckedCore ObjectId) + !PreparedProof + | PreparedByCase !PreparedCaseAnalysis + | PreparedByContradiction + !(ScopedCheckedCore ObjectId) + !(ScopedCheckedCore ObjectId) + !(ScopedCheckedCore ObjectId) + !PreparedProof + | PreparedContradiction + !(ScopedCheckedCore ObjectId) + !(ScopedCheckedCore ObjectId) + !PreparedDischarge + +data PreparedExactProof = PreparedExactProof + !Location + !SemanticName + !(ScopedCheckedCore ObjectId) + !PreparedProof + !ProofSyntaxId + +data PreparedFinalPreludeFoundationClaim = + PreparedFinalPreludeFoundationClaim + !Location + !SemanticName + !(ScopedCheckedCore ObjectId) + !FoundationAxiomTag + !ProofSyntaxId + +preparedExactProofSyntaxId :: PreparedExactProof -> ProofSyntaxId +preparedExactProofSyntaxId + (PreparedExactProof _location _alias _target _proof syntax) = + syntax + +preparedExactProofFirstOmission :: PreparedExactProof -> Maybe Location +preparedExactProofFirstOmission + (PreparedExactProof _location _alias _target proof _syntax) = + preparedProofFirstOmission proof + +data PrepareState = PrepareState + { prepareNextLocal :: !Natural + , prepareNextPremise :: !Natural + } + +type Prepare = + StateT + PrepareState + (ExceptT ExactProofError (Declaration.LoweringDriver)) + +prepareExactProof + :: Raw.Block + -> Maybe Raw.Proof + -> Declaration.LoweringDriver + (Either ExactProofError PreparedExactProof) +prepareExactProof block explicitProof = + Except.runExceptT + (State.evalStateT prepare initialState) + where + initialState = PrepareState 0 0 + + prepare = + case block of + Raw.BlockClaim + _kind location _title (Raw.Marker marker) + (Raw.Claim assumptions statement) -> do + envelope <- + liftDriver + (Exact.prepareExactClaimEnvelope assumptions statement) + >>= either + (throwProof . ExactProofElaborationFailed) + pure + let targetCore = Exact.preparedExactClaimTarget envelope + unless (null (scopedCoreContext targetCore)) + (throwProof + (ExactProofUnsupportedClaim location)) + (context, openedGoal, identities) <- + openEnvelopeVariables + targetCore + (Exact.preparedExactClaimVariables envelope) + (Exact.preparedExactClaimContext envelope) + (locals, bodyGoal, antecedents) <- + openEnvelopeAntecedents + context + openedGoal + (Exact.preparedExactClaimAntecedentCount envelope) + initialInduction <- + prepareInitialSetInductionView + statement + context + (Exact.preparedExactClaimVariables envelope) + identities + antecedents + bodyGoal + bodyProof <- + case explicitProof of + Nothing -> + PreparedImplicitAuto + <$> prepareDischarge + location + context + locals + bodyGoal + Raw.JustificationEmpty + Just sourceProof -> + prepareProof + location + context + locals + (InitialClaimInduction initialInduction) + bodyGoal + sourceProof + let withAssumptions = + foldr PreparedAssume bodyProof antecedents + proof = + case identities of + [] -> withAssumptions + _ -> PreparedFix identities withAssumptions + pure + (PreparedExactProof + location + (semanticName marker) + targetCore + proof + (proofSyntaxId + (encodePreparedProof proof))) + _ -> + throwProof + (ExactProofUnsupportedClaim (locate block)) + +prepareFinalPreludeFoundationClaim + :: CheckedFoundation + -> Raw.Block + -> Maybe Raw.Proof + -> Declaration.LoweringDriver + (Either ExactProofError PreparedFinalPreludeFoundationClaim) +prepareFinalPreludeFoundationClaim foundation block explicitProof = + Except.runExceptT do + case (block, explicitProof) of + ( Raw.BlockClaim + _kind location _title (Raw.Marker marker) + (Raw.Claim assumptions statement) + , Nothing + ) -> do + envelope <- + Except.lift + (Exact.prepareExactClaimEnvelope + assumptions + statement) + >>= either + (Except.throwError + . ExactProofElaborationFailed) + pure + unless + ( null (Exact.preparedExactClaimVariables envelope) + && Exact.preparedExactClaimAntecedentCount envelope + == 0 + ) + (Except.throwError + (ExactProofFoundationLeafRequiresImplicitAuto + location)) + let target = Exact.preparedExactClaimTarget envelope + matches = + [ tag + | tag <- [minBound .. maxBound] + , target == foundationTarget tag + ] + tag <- case matches of + [] -> + Except.throwError + (ExactProofFoundationLeafTargetMismatch location) + [only] -> + pure only + _ -> + Except.throwError + (ExactProofFoundationLeafTargetAmbiguous location) + pure + (PreparedFinalPreludeFoundationClaim + location + (semanticName marker) + target + tag + (implicitAutoProofSyntaxId target)) + (Raw.BlockClaim _kind location _title _marker _claim, Just{}) -> + Except.throwError + (ExactProofFoundationLeafRequiresImplicitAuto location) + _ -> + Except.throwError + (ExactProofUnsupportedClaim (locate block)) + where + foundationTarget tag = + embedClosedCore [] + (mapFrozenGlobals + absurd + (foundationAxiomFrozen foundation tag)) + +openEnvelopeVariables + :: ScopedCheckedCore ObjectId + -> [Raw.VarSymbol] + -> Exact.ExactBinderContext + -> Prepare + ( Exact.ExactBinderContext + , ScopedCheckedCore ObjectId + , [Exact.ExactLocalId] + ) +openEnvelopeVariables target variables preparedContext = + case NonEmpty.nonEmpty variables of + Nothing -> + 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 + -> ScopedCheckedCore ObjectId + -> Natural + -> Prepare + ( [PreparedLocal] + , ScopedCheckedCore ObjectId + , [ScopedCheckedCore ObjectId] + ) +openEnvelopeAntecedents context initialGoal initialCount = + go [] [] initialGoal initialCount + where + go locals antecedents goal 0 = + pure (locals, goal, antecedents) + go locals antecedents goal remaining = do + (antecedent, conclusion) <- + maybe + (impossible + "a prepared claim envelope has too few implications") + pure + (openScopedImplication goal) + local <- allocateLocal ExactAssumption context antecedent + go + (locals <> [local]) + (antecedents <> [antecedent]) + conclusion + (remaining - 1) + +prepareInitialSetInductionView + :: Raw.Stmt + -> Exact.ExactBinderContext + -> [Raw.VarSymbol] + -> [Exact.ExactLocalId] + -> [ScopedCheckedCore ObjectId] + -> ScopedCheckedCore ObjectId + -> Prepare InitialSetInductionView +prepareInitialSetInductionView + statement context variables identities antecedents bodyGoal = do + unless (length variables == length identities) + (impossible + "opened claim binders lost their source identity association") + foci <- traverse checkedFocus (zip variables identities) + let property = foldr implyChecked bodyGoal antecedents + support = Exact.exactBinderContextSupport context + unless + ( scopedCoreContext property + == (snd <$> Vector.toList support) + ) + (impossible + "initial set-induction property changed its checked context") + pure + (InitialSetInductionView + foci support property antecedents bodyGoal + (claimLeadingUniversalName statement)) + where + checkedFocus (variable, identity) = do + index <- + maybe + (impossible + "an opened claim binder is absent from its exact context") + pure + (Exact.exactBinderContextIndex variable context) + case Exact.exactBinderContextSupport context + Vector.!? (fromIntegral index) of + Just (actualIdentity, TySet) + | actualIdentity == identity -> + pure + (InitialSetInductionFocus + variable identity index) + _ -> + impossible + "an initial set-induction focus changed identity or type" + + implyChecked antecedent conclusion = + fromMaybe + (impossible + "an exact claim antecedent changed context") + (implyScopedCore antecedent conclusion) + +claimLeadingUniversalName :: Raw.Stmt -> Maybe Raw.VarSymbol +claimLeadingUniversalName = \case + Raw.StmtFormula + (Raw.FormulaQuantified _location Raw.Universally + (variable :| _rest) _bound _formula) -> + Just variable + Raw.SymbolicForall _location (variable :| _rest) + _bound _suchThat _statement -> + Just variable + Raw.StmtQuantPhrase + _location + (Raw.QuantPhrase Raw.Universally + (Raw.NounPhrase _left _noun variables _right _suchThat)) + _statement -> + listToMaybe variables + Raw.StmtVerbPhrase + (Raw.TermQuantified Raw.Universally _location + (Raw.NounPhrase _left _noun variable _right _suchThat) + :| []) + _verb -> + variable + Raw.StmtNoun + (Raw.TermQuantified Raw.Universally _location + (Raw.NounPhrase _left _noun variable _right _suchThat) + :| []) + _nounPhrase -> + variable + _statement -> + Nothing + +prepareProof + :: Location + -> Exact.ExactBinderContext + -> [PreparedLocal] + -> SetInductionBoundary + -> ScopedCheckedCore ObjectId + -> Raw.Proof + -> Prepare PreparedProof +prepareProof fallback context locals inductionBoundary goal = \case + Raw.Omitted location -> + pure (PreparedOmitted location goal) + Raw.Qed maybeLocation justification -> + PreparedQed + <$> prepareDischarge + (fromMaybe fallback maybeLocation) + context + locals + goal + justification + Raw.FixSymbolic location variables bound continuation -> do + (context', goal', identities) <- + openFixedVariables context goal variables + case bound of + Raw.Unbounded -> + PreparedFix identities + <$> prepareProof + fallback + context' + locals + RecursiveProofInduction + 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 + supplied <- prepareStatement context statement + when (isNothing (openScopedImplication goal)) + (throwProof (ExactProofExpectedImplicationGoal location)) + (assumption, conclusion) <- + maybe + (throwProof (ExactProofGoalStatementMismatch location)) + pure + (openScopedAssumption + (Exact.preparedExactPropositionCore supplied) + goal) + local <- allocateLocal ExactAssumption context assumption + PreparedAssume assumption + <$> prepareProof + fallback + context + (locals <> [local]) + RecursiveProofInduction + conclusion + continuation + Raw.TakeVar location variables bound statement justification continuation -> do + 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 -> + prepareSetInduction + fallback location context locals inductionBoundary goal + variable continuation + 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 Nothing statement justification continuation -> do + claim <- + Exact.preparedExactPropositionCore + <$> prepareStatement context statement + discharge <- + prepareDischarge + location context locals claim justification + local <- allocateLocal ExactDerivedClaim context claim + PreparedHave claim discharge + <$> prepareProof + fallback + context + (locals <> [local]) + RecursiveProofInduction + goal + continuation + Raw.Have location (Just sinceStatement) + statement justification continuation -> do + sinceProposition <- + Exact.preparedExactPropositionCore + <$> prepareStatement context sinceStatement + claim <- + Exact.preparedExactPropositionCore + <$> prepareStatement context statement + (evidence, sinceLocals) <- + case find (localMatches sinceProposition) locals of + Just existing -> + pure (PreparedSinceExisting existing, locals) + Nothing -> do + discharge <- + prepareDischarge + location + context + locals + sinceProposition + Raw.JustificationLocal + local <- + allocateLocal + ExactDerivedClaim context sinceProposition + pure + ( PreparedSinceDischarged discharge local + , locals <> [local] + ) + claimDischarge <- + prepareDischarge + location context sinceLocals claim justification + claimLocal <- + allocateLocal ExactDerivedClaim context claim + PreparedSince + sinceProposition evidence claim claimDischarge + <$> prepareProof + fallback + context + (sinceLocals <> [claimLocal]) + RecursiveProofInduction + goal + continuation + Raw.Suffices location statement justification continuation -> do + reduction <- + Exact.preparedExactPropositionCore + <$> prepareStatement context statement + implication <- + maybe + (impossible + "a checked suffices reduction changed lexical context") + pure + (implyScopedCore reduction goal) + discharge <- + prepareDischarge + location context locals implication justification + PreparedSuffices goal reduction implication discharge + <$> prepareProof + fallback + context + locals + (SourceStatementInduction + (claimLeadingUniversalName statement)) + reduction + continuation + Raw.Calc location quantifier calculation continuation -> do + prepared <- + prepareCalculation + location context locals quantifier calculation + local <- + allocateLocal + ExactDerivedClaim + context + (preparedCalculationResult prepared) + PreparedCalculate prepared + <$> prepareProof + fallback + context + (locals <> [local]) + RecursiveProofInduction + goal + continuation + Raw.Subclaim location statement subproof continuation -> do + claim <- + Exact.preparedExactPropositionCore + <$> prepareStatement context statement + preparedSubproof <- + prepareProof + location + context + locals + (SourceStatementInduction + (claimLeadingUniversalName statement)) + claim + subproof + local <- allocateLocal ExactDerivedClaim context claim + PreparedSubclaim claim preparedSubproof + <$> prepareProof + fallback + context + (locals <> [local]) + RecursiveProofInduction + goal + continuation + Raw.Define location variable expression continuation -> do + preparedBody <- + liftDriver + (Exact.prepareExactSetExpression context expression) + >>= either + (throwProof . ExactProofElaborationFailed) + pure + let body = Exact.preparedExactSetExpressionCore preparedBody + identity <- allocateLocalIdentity + context' <- + either + (throwProof . ExactProofElaborationFailed) + pure + (Exact.extendExactBinderContext + ((identity, variable) :| []) + context) + case Exact.preparedExactSetExpressionConstruction preparedBody of + Nothing -> do + separationCharacteristic <- + liftDriver + (Declaration.currentFoundationAxiomLowering + SeparationCharacteristic) + definition <- + maybe + (impossible + "an exact set expression did not form a local definition") + pure + (scopedSetDefinition separationCharacteristic body) + local <- + allocateLocal ExactLocalDefinition context' definition + PreparedDefine identity body (definition :| []) + <$> prepareProof + fallback context' (locals <> [local]) + RecursiveProofInduction + (weakenCheckedScopedCore TySet goal) + continuation + Just (Exact.PreparedUnconditionalSetConstruction construction) -> do + characteristics <- prepareConstructionFoundation + (extensional, equation) <- + maybe + (impossible + "a checked named construction has no definition views") + pure + (namedSetConstructionLocalViews + characteristics construction) + extensionalLocal <- + allocateLocal + ExactLocalConstructionExtensional context' extensional + equationLocal <- + allocateLocal + ExactLocalConstructionEquation context' equation + PreparedDefine identity body (extensional :| [equation]) + <$> prepareProof + fallback context' + (locals <> [extensionalLocal, equationLocal]) + RecursiveProofInduction + (weakenCheckedScopedCore TySet goal) + continuation + Just (Exact.PreparedRelationalSetConstruction construction) -> do + characteristics <- prepareConstructionFoundation + let functionality = + relationalSetConstructionFunctionality construction + discharge <- + prepareDischarge + location context locals functionality + Raw.JustificationEmpty + (extensional, equation) <- + maybe + (impossible + "a checked relational construction has no admitted definition views") + pure + (relationalSetConstructionLocalViews + characteristics construction functionality) + extensionalLocal <- + allocateLocal + ExactLocalConstructionExtensional context' extensional + equationLocal <- + allocateLocal + ExactLocalConstructionEquation context' equation + PreparedDefineRelational + identity body discharge (extensional :| [equation]) + <$> prepareProof + fallback context' + (locals <> [extensionalLocal, equationLocal]) + RecursiveProofInduction + (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.currentFoundationAxiomLowering + 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]) + RecursiveProofInduction + (weakenCheckedScopedCore TySet goal) + continuation + Raw.ByCase location sourceCases -> + prepareByCase + location context locals goal sourceCases + Raw.ByContradiction location continuation -> do + let falsum = falsumScopedCore (scopedCoreContext goal) + negation <- + maybe + (structuralFailure + location + "proof by contradiction requires a proposition goal") + pure + (negateScopedCore goal) + local <- allocateLocal ExactAssumption context negation + prepared <- + prepareProof + location + context + (locals <> [local]) + RecursiveProofInduction + falsum + continuation + validateStructuralComposition + location [goal, negation, falsum] + (\foundation globalType -> + KernelProof.validateDoubleNegationComposition + foundation globalType goal negation falsum) + pure + (PreparedByContradiction + goal negation falsum prepared) + Raw.Contradiction location justification -> do + let falsum = falsumScopedCore (scopedCoreContext goal) + discharge <- + prepareDischarge + location + context + locals + falsum + justification + validateStructuralComposition + location [goal, falsum] + (\foundation globalType -> + KernelProof.validateFalsumEliminationComposition + foundation globalType goal falsum) + pure (PreparedContradiction goal falsum discharge) + proof -> + throwProof + (ExactProofUnsupportedStep + (proofLocation fallback proof)) + where + localMatches proposition + (PreparedLocal _ordinal _origin _support local) = + local == proposition + +prepareSetInduction + :: Location + -> Location + -> Exact.ExactBinderContext + -> [PreparedLocal] + -> SetInductionBoundary + -> ScopedCheckedCore ObjectId + -> Maybe Raw.Term + -> Raw.Proof + -> Prepare PreparedProof +prepareSetInduction + fallback location context locals boundary goal sourceFocus + continuation = do + selected <- + selectSetInductionFocus + location context boundary goal sourceFocus + case selected of + SelectedInitialSetInduction + (InitialSetInductionFocus _variable identity index) -> do + (foci, expectedSupport, property, antecedents, childTarget) <- + case boundary of + InitialClaimInduction + (InitialSetInductionView + foundFoci support foundProperty + foundAntecedents foundTarget _leadingName) -> + pure + ( foundFoci + , support + , foundProperty + , foundAntecedents + , foundTarget + ) + RecursiveProofInduction -> + impossible + "an initial induction focus escaped its claim boundary" + SourceStatementInduction _leadingName -> + impossible + "an initial induction focus escaped its claim boundary" + unless + ( Exact.exactBinderContextSupport context == expectedSupport + && goal == childTarget + && any (sameInitialFocus identity index) foci + ) + (throwProof + (ExactProofSetInductionGoalMismatch location)) + PreparedSetInduction + <$> prepareCheckedSetInduction + fallback location context locals + (PreparedInitialSetInductionFocus identity index) + index property antecedents childTarget continuation + SelectedLeadingSetInduction sourceName -> do + (binderType, property) <- + maybe + (throwProof + (ExactProofSetInductionGoalMismatch location)) + pure + (openScopedForall goal) + unless (binderType == TySet) + (throwProof + (ExactProofSetInductionGoalMismatch location)) + identity <- allocateLocalIdentity + extendedContext <- + either + (throwProof . ExactProofElaborationFailed) + pure + (case sourceName of + Just variable -> + Exact.extendExactBinderContext + ((identity, variable) :| []) + context + Nothing -> + Exact.extendExactAnonymousBinderContext + identity context) + let expectedResult = weakenCheckedScopedCore TySet goal + prepared <- prepareCheckedSetInduction + fallback location extendedContext locals + (PreparedLeadingSetInductionFocus identity) + 0 property [] property continuation + unless + (preparedSetInductionResult prepared == expectedResult) + (throwProof + (ExactProofSetInductionGoalMismatch location)) + pure (PreparedSetInduction prepared) + where + sameInitialFocus expectedIdentity expectedIndex + (InitialSetInductionFocus _variable identity index) = + identity == expectedIdentity && index == expectedIndex + +prepareCheckedSetInduction + :: Location + -> Location + -> Exact.ExactBinderContext + -> [PreparedLocal] + -> PreparedSetInductionFocus + -> Natural + -> ScopedCheckedCore ObjectId + -> [ScopedCheckedCore ObjectId] + -> ScopedCheckedCore ObjectId + -> Raw.Proof + -> Prepare PreparedSetInduction +prepareCheckedSetInduction + fallback location context locals focus selected property antecedents + childTarget continuation = do + (_predicate, hypothesis, _step, result) <- + maybe + (throwProof + (ExactProofSetInductionGoalMismatch location)) + pure + (scopedSetInductionInstance selected property) + validateStructuralComposition + location + (property : hypothesis : result : childTarget : antecedents) + (\foundation globalType -> + KernelProof.validateSetInductionComposition + foundation globalType selected property antecedents + childTarget hypothesis result) + local <- allocateLocal ExactAssumption context hypothesis + child <- + prepareProof + fallback + context + (locals <> [local]) + RecursiveProofInduction + childTarget + continuation + pure + (PreparedCheckedSetInduction + focus property antecedents childTarget hypothesis result child) + +preparedSetInductionResult + :: PreparedSetInduction + -> ScopedCheckedCore ObjectId +preparedSetInductionResult + (PreparedCheckedSetInduction + _focus _property _antecedents _target _hypothesis result _child) = + result + +selectSetInductionFocus + :: Location + -> Exact.ExactBinderContext + -> SetInductionBoundary + -> ScopedCheckedCore ObjectId + -> Maybe Raw.Term + -> Prepare SelectedSetInductionFocus +selectSetInductionFocus location context boundary goal sourceFocus = do + explicit <- traverse simpleVariable sourceFocus + let (initialFoci, retainedLeadingName) = + case boundary of + InitialClaimInduction + (InitialSetInductionView + foci _support _property _antecedents _target + leadingName) -> + (foci, leadingName) + SourceStatementInduction leadingName -> + ([], leadingName) + RecursiveProofInduction -> + ([], Nothing) + leadingAvailable = + case openScopedForall goal of + Just (TySet, _body) -> True + _ -> False + case explicit of + Just variable -> + case find (initialNamed variable) initialFoci of + Just focus -> + pure (SelectedInitialSetInduction focus) + Nothing + | leadingAvailable + , isJust + (Exact.exactBinderContextIndex variable context) -> + throwProof + (ExactProofSetInductionBinderConflict + location variable) + | leadingAvailable -> + pure + (SelectedLeadingSetInduction + (Just variable)) + | isJust + (Exact.exactBinderContextIndex variable context) -> + throwProof + (ExactProofSetInductionActiveBinderIneligible + location variable) + | otherwise -> + throwProof + (ExactProofSetInductionVariableNotActive + location variable) + Nothing -> + case + ( (SelectedInitialSetInduction <$> initialFoci) + <> [ SelectedLeadingSetInduction retainedLeadingName + | leadingAvailable + ] + ) of + [only] -> pure only + _ -> + throwProof + (ExactProofSetInductionFocusAmbiguous location) + where + simpleVariable = \case + Raw.TermExpr (Raw.ExprVar variable) -> + pure variable + _term -> + throwProof + (ExactProofSetInductionVariableRequired location) + + initialNamed variable + (InitialSetInductionFocus candidate _identity _index) = + candidate == variable + +prepareByCase + :: Location + -> Exact.ExactBinderContext + -> [PreparedLocal] + -> ScopedCheckedCore ObjectId + -> [Raw.Case] + -> Prepare PreparedProof +prepareByCase location context locals goal sourceCases = do + cases <- + maybe + (throwProof (ExactProofEmptyCaseSplit location)) + (traverse prepareCase) + (NonEmpty.nonEmpty sourceCases) + exhaustive <- + foldM disjoin + (preparedCaseAssumption (NonEmpty.head cases)) + (preparedCaseAssumption <$> NonEmpty.tail cases) + discharge <- + prepareDischarge + location context locals exhaustive Raw.JustificationEmpty + validateStructuralComposition + location + (goal : exhaustive : (preparedCaseAssumption <$> toList cases)) + (\foundation globalType -> + KernelProof.validateCaseAnalysisComposition + foundation + globalType + goal + (preparedCaseAssumption <$> cases) + exhaustive) + pure + (PreparedByCase + (PreparedCaseAnalysis goal cases exhaustive discharge)) + where + prepareCase (Raw.Case statement child) = do + assumption <- + Exact.preparedExactPropositionCore + <$> prepareStatement context statement + local <- allocateLocal ExactAssumption context assumption + prepared <- + prepareProof + (locate statement) + context + (locals <> [local]) + RecursiveProofInduction + goal + child + pure (PreparedCase assumption prepared) + + disjoin left right = + maybe + (structuralFailure + location + "case assumptions changed type or lexical context") + pure + (disjoinScopedCore left right) + +preparedCaseAssumption + :: PreparedCase + -> ScopedCheckedCore ObjectId +preparedCaseAssumption (PreparedCase assumption _proof) = + assumption + +preparedCaseProof :: PreparedCase -> PreparedProof +preparedCaseProof (PreparedCase _assumption proof) = + proof + +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]) + RecursiveProofInduction + conclusion + continuation + pure (PreparedFix identities (PreparedAssume constraint prepared)) + +prepareCalculation + :: Location + -> Exact.ExactBinderContext + -> [PreparedLocal] + -> Maybe Raw.CalcQuantifier + -> Raw.Calc + -> Prepare PreparedCalculation +prepareCalculation location context locals quantifier calculation = do + (identities, calculationContext, calculationGuard) <- + prepareCalculationScope context quantifier + case calculation of + Raw.Equation first destinations -> do + firstChecked <- prepareSetEndpoint calculationContext first + checkedDestinations <- + traverse + (\(destination, justification) -> do + checked <- + prepareSetEndpoint calculationContext destination + pure + ( locate destination + , checked + , justification + )) + destinations + finishCalculation + location context locals TySet identities calculationGuard + firstChecked checkedDestinations + Raw.Biconditionals first destinations -> do + firstChecked <- preparePropositionEndpoint calculationContext first + checkedDestinations <- + traverse + (\(destination, justification) -> do + checked <- + preparePropositionEndpoint + calculationContext destination + pure + ( locate destination + , checked + , justification + )) + destinations + finishCalculation + location context locals TyProp identities calculationGuard + firstChecked checkedDestinations + where + prepareSetEndpoint endpointContext expression = + Exact.preparedExactSetExpressionCore + <$> ( liftDriver + (Exact.prepareExactSetExpression + endpointContext expression) + >>= either + (throwProof . ExactProofElaborationFailed) + pure + ) + + preparePropositionEndpoint endpointContext formula = + Exact.preparedExactPropositionCore + <$> prepareStatement endpointContext (Raw.StmtFormula formula) + +prepareCalculationScope + :: Exact.ExactBinderContext + -> Maybe Raw.CalcQuantifier + -> Prepare + ( [Exact.ExactLocalId] + , Exact.ExactBinderContext + , Maybe (ScopedCheckedCore ObjectId) + ) +prepareCalculationScope context = \case + Nothing -> + pure ([], context, Nothing) + Just (Raw.CalcQuantifier variables bound suchThat) -> do + identities <- traverse (const allocateLocalIdentity) variables + calculationContext <- + either + (throwProof . ExactProofElaborationFailed) + pure + (Exact.extendExactBinderContext + (NonEmpty.zip identities variables) + context) + boundGuard <- + prepareSymbolicBoundConstraints + calculationContext variables bound + suchThatGuard <- + traverse + (fmap Exact.preparedExactPropositionCore + . prepareStatement calculationContext) + suchThat + calculationGuard <- + normalizeCalculationGuard + (boundGuard : maybeToList suchThatGuard) + pure (toList identities, calculationContext, calculationGuard) + +normalizeCalculationGuard + :: [ScopedCheckedCore ObjectId] + -> Prepare (Maybe (ScopedCheckedCore ObjectId)) +normalizeCalculationGuard guards = + foldM add Nothing guards + where + add accumulated constraint + | isScopedTruth constraint = pure accumulated + | otherwise = + case accumulated of + Nothing -> pure (Just constraint) + Just previous -> + Just + <$> maybe + (impossible + "checked calculation guards changed context") + pure + (conjoinScopedCore previous constraint) + + isScopedTruth proposition = + scopedCoreType proposition == TyProp + && scopedCoreTerm proposition == CImp CFalsum CFalsum + +finishCalculation + :: Location + -> Exact.ExactBinderContext + -> [PreparedLocal] + -> CoreType + -> [Exact.ExactLocalId] + -> Maybe (ScopedCheckedCore ObjectId) + -> ScopedCheckedCore ObjectId + -> NonEmpty + ( Location + , ScopedCheckedCore ObjectId + , Raw.Justification + ) + -> Prepare PreparedCalculation +finishCalculation + fallback context locals operandType identities calculationGuard + first destinations = do + links <- prepareCalculationLinks first destinations + let finalEndpoint = preparedCalculationLinkDestination (NonEmpty.last links) + resultOpen <- + calculationEquality first finalEndpoint + result <- + closeCalculationProposition identities calculationGuard resultOpen + pure + (PreparedCheckedCalculation + operandType identities calculationGuard first links result) + where + prepareCalculationLinks previous (destination :| rest) = do + (next, firstLink) <- prepareCalculationLink previous destination + later <- prepareRemainingCalculationLinks next rest + pure (firstLink :| later) + + prepareRemainingCalculationLinks _previous [] = + pure [] + prepareRemainingCalculationLinks previous (destination : rest) = do + (next, link) <- prepareCalculationLink previous destination + (link :) <$> prepareRemainingCalculationLinks next rest + + prepareCalculationLink previous + (destinationLocation, destination, justification) = do + linkOpen <- calculationEquality previous destination + link <- closeCalculationProposition + identities calculationGuard linkOpen + discharge <- + prepareDischarge + (if destinationLocation == Nowhere + then fallback + else destinationLocation) + context + locals + link + justification + pure + ( destination + , PreparedCalculationLink destination discharge + ) + + calculationEquality left right = + maybe + (impossible + "checked calculation endpoints changed type or context") + pure + (equalScopedCore left right) + +closeCalculationProposition + :: [Exact.ExactLocalId] + -> Maybe (ScopedCheckedCore ObjectId) + -> ScopedCheckedCore ObjectId + -> Prepare (ScopedCheckedCore ObjectId) +closeCalculationProposition identities calculationGuard proposition = do + guarded <- + case calculationGuard of + Nothing -> pure proposition + Just constraint -> + maybe + (impossible + "a checked calculation guard changed context") + pure + (implyScopedCore constraint proposition) + pure (closeBinders (length identities) guarded) + where + closeBinders 0 closed = closed + closeBinders remaining open = + closeBinders (remaining - 1) + (fromMaybe + (impossible + "a checked calculation lost a quantified binder") + (closeScopedForall open)) + +preparedCalculationResult + :: PreparedCalculation + -> ScopedCheckedCore ObjectId +preparedCalculationResult + (PreparedCheckedCalculation + _operandType _identities _guard _first _links result) = + result + +preparedCalculationLinkDestination + :: PreparedCalculationLink + -> ScopedCheckedCore ObjectId +preparedCalculationLinkDestination + (PreparedCalculationLink destination _discharge) = + destination + +preparedCalculationLinkDischarge + :: PreparedCalculationLink + -> PreparedDischarge +preparedCalculationLinkDischarge + (PreparedCalculationLink _destination discharge) = + discharge + +preparedDischargeGoal + :: PreparedDischarge + -> ScopedCheckedCore ObjectId +preparedDischargeGoal = \case + PreparedVampireDischarge _location _justification goal _obligation -> + goal + PreparedSetExtensionality _location goal -> + goal + +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]) + RecursiveProofInduction + goal' + continuation + +-- The discharged existential and the opened witness premise are the same +-- checked proposition viewed on opposite sides of existential elimination. +closeTakenWitnesses + :: Int + -> ScopedCheckedCore ObjectId + -> ScopedCheckedCore ObjectId +closeTakenWitnesses binderCount = go binderCount + where + go 0 proposition = proposition + go remaining proposition = + go (remaining - 1) + (fromMaybe + (impossible "a taken witness has no checked binder") + (closeScopedExists proposition)) + +weakenForTakenWitnesses + :: Int + -> ScopedCheckedCore ObjectId + -> ScopedCheckedCore ObjectId +weakenForTakenWitnesses binderCount = go binderCount + where + go 0 proposition = proposition + go remaining proposition = + go (remaining - 1) + (weakenCheckedScopedCore TySet proposition) + +openFixedVariables + :: Exact.ExactBinderContext + -> ScopedCheckedCore ObjectId + -> NonEmpty Raw.VarSymbol + -> Prepare + ( Exact.ExactBinderContext + , ScopedCheckedCore ObjectId + , [Exact.ExactLocalId] + ) +openFixedVariables initialContext initialGoal variables = + foldM openOne + (initialContext, initialGoal, []) + (toList variables) + where + openOne (context, goal, identities) variable = do + (binderType, body) <- + maybe + (throwProof + (ExactProofExpectedUniversalGoal + (locate variable))) + pure + (openScopedForall goal) + unless (binderType == TySet) + (throwProof + (ExactProofExpectedUniversalGoal + (locate variable))) + identity <- allocateLocalIdentity + context' <- + either + (throwProof . ExactProofElaborationFailed) + pure + (Exact.extendExactBinderContext + ((identity, variable) :| []) + context) + pure (context', body, identities <> [identity]) + +allocateLocalIdentity :: Prepare Exact.ExactLocalId +allocateLocalIdentity = do + state <- State.get + State.put + state + { prepareNextLocal = prepareNextLocal state + 1 + } + pure (Exact.exactLocalId (prepareNextLocal state)) + +allocateLocal + :: ExactLocalOrigin + -> Exact.ExactBinderContext + -> ScopedCheckedCore ObjectId + -> Prepare PreparedLocal +allocateLocal origin context proposition = do + state <- State.get + State.put + state + { prepareNextPremise = prepareNextPremise state + 1 + } + pure + (PreparedLocal + (Backend.localPremiseOrdinal + (prepareNextPremise state)) + origin + (Exact.exactBinderContextSupport context) + proposition) + +prepareConstructionFoundation + :: Prepare SetConstructionFoundation +prepareConstructionFoundation = do + familyUnion <- foundation FamilyUnionCharacteristic + separation <- foundation SeparationCharacteristic + replacement <- foundation ReplacementCharacteristic + setChoose <- foundation SetChooseWitness + pure + (setConstructionFoundation + familyUnion separation replacement setChoose) + where + foundation tag = + liftDriver + (Declaration.currentFoundationAxiomLowering tag) + +prepareDischarge + :: Location + -> Exact.ExactBinderContext + -> [PreparedLocal] + -> ScopedCheckedCore ObjectId + -> Raw.Justification + -> Prepare PreparedDischarge +prepareDischarge location context locals goal justification = + prepareDischargeWith + (dischargeModeFor goal) + [] Nothing location context locals goal justification + +-- A contradictory-axioms answer can establish falsum, but never an unrelated +-- proposition directly. Derive that distinction from the checked target so +-- every surface proof spelling reaches the same guarded request path. +dischargeModeFor :: ScopedCheckedCore ObjectId -> DischargeMode +dischargeModeFor goal + | scopedCoreType goal == TyProp + , scopedCoreTerm goal == CFalsum = + IndirectContradictionDischarge + | otherwise = + DirectDischarge + +data DischargeMode + = DirectDischarge + | IndirectContradictionDischarge + +prepareDischargeWith + :: DischargeMode + -> [FoundationAxiomTag] + -> Maybe Declaration.VampirePremiseSelection + -> Location + -> Exact.ExactBinderContext + -> [PreparedLocal] + -> ScopedCheckedCore ObjectId + -> Raw.Justification + -> Prepare PreparedDischarge +prepareDischargeWith + dischargeMode auxiliaries selectionOverride + location context locals goal justification = + case justification of + Raw.JustificationSetExt -> do + (leftToRight, rightToLeft) <- + maybe + (throwProof + (ExactProofSetExtensionalityGoalMismatch location)) + pure + (splitScopedSetEquality goal) + unless + ( hasDerivedLocal leftToRight + && hasDerivedLocal rightToLeft + ) + (throwProof + (ExactProofSetExtensionalityDirectionsUnavailable + location)) + pure (PreparedSetExtensionality location goal) + _ -> do + preparedJustification <- + prepareJustification location justification + prepared <- + liftDriver + (prepareObligation + (Exact.exactBinderContextSupport context) + goal + (toScopedPremise <$> locals) + auxiliaries + (fromMaybe + (vampirePremiseSelection preparedJustification) + selectionOverride)) + >>= either + (throwProof + . ExactProofObligationPreparationFailed location) + pure + pure + (PreparedVampireDischarge + location + preparedJustification + goal + prepared) + where + prepareObligation = + case dischargeMode of + DirectDischarge -> + Declaration.prepareScopedVampireObligationLowering + IndirectContradictionDischarge -> + Declaration.prepareScopedContradictionObligationLowering + + hasDerivedLocal proposition = + any + (\case + PreparedLocal + _ordinal ExactDerivedClaim _support local -> + local == proposition + PreparedLocal{} -> + False) + locals + + toScopedPremise + (PreparedLocal ordinal origin support proposition) = + Declaration.scopedVampirePremise + ordinal origin support proposition + +prepareJustification + :: Location + -> Raw.Justification + -> Prepare PreparedJustification +prepareJustification _location Raw.JustificationEmpty = + pure PreparedAuto +prepareJustification location (Raw.JustificationRef markers) = do + resolved <- traverse (resolveReference location) (toList markers) + let unique = stableUnique resolved + case unique of + [] -> + impossible "a nonempty citation list resolved to no facts" + first : rest -> + pure (PreparedReferences (first :| rest)) +prepareJustification _location Raw.JustificationLocal = + pure PreparedLocalOnly +prepareJustification location Raw.JustificationSetExt = + throwProof (ExactProofUnsupportedStep location) + +vampirePremiseSelection + :: PreparedJustification + -> Declaration.VampirePremiseSelection +vampirePremiseSelection = \case + PreparedAuto -> + Declaration.VampireImplicitPremises + PreparedReferences fingerprints -> + Declaration.VampireExplicitPremises fingerprints + PreparedLocalOnly -> + Declaration.VampireLocalPremises + +resolveReference + :: Location + -> Raw.Marker + -> Prepare SemanticFactOccurrenceFingerprint +resolveReference location marker@(Raw.Marker name) = do + resolved <- + liftDriver + (Declaration.resolveVisibleFactAliasLowering + (semanticName name)) + maybe + (throwProof + (ExactProofUnknownReference location marker)) + pure + resolved + +prepareStatement + :: Exact.ExactBinderContext + -> Raw.Stmt + -> Prepare Exact.PreparedExactProposition +prepareStatement context statement = + liftDriver + (Exact.prepareExactProposition context statement) + >>= either + (throwProof . ExactProofElaborationFailed) + pure + +validateStructuralComposition + :: Location + -> [ScopedCheckedCore ObjectId] + -> ( CheckedFoundation + -> (ObjectId -> Maybe CoreType) + -> Either KernelProof.KernelProofBuildError () + ) + -> Prepare () +validateStructuralComposition location propositions validate = do + foundation <- + liftDriver Declaration.currentFoundationLowering + let identities = + Set.toAscList + (Set.unions + ( canonicalTermGlobals . scopedCoreTerm + <$> propositions + )) + types <- + traverse + (\identity -> do + coreType <- + liftDriver + (Declaration.objectTypeLowering identity) + maybe + (impossible + "a checked structural proof lost a global object") + (\availableType -> pure (identity, availableType)) + coreType) + identities + either + (throwProof + . ExactProofStructuralCompositionFailed location) + pure + (validate foundation + (\identity -> Map.lookup identity (Map.fromList types))) + +structuralFailure :: Location -> Text -> Prepare value +structuralFailure location message = + throwProof + (ExactProofStructuralCompositionFailed + location + (KernelProof.ProofStructuralCompositionMismatch message)) + +data CheckedExactProofAuthorization = CheckedExactProofAuthorization + !PreparedProof + !Bool + +lowerPreparedExactProof + :: PreparedExactProof + -> Declaration.LoweringDriver + (Either + Declaration.DeclarationError + (Declaration.CheckedDeclaration CheckedExactProofAuthorization)) +lowerPreparedExactProof + (PreparedExactProof _location alias target proof syntax) = + fmap checked + <$> Declaration.prepareCandidateSpecLowering + [] target SearchEligible [alias] + where + checked spec = + Declaration.checkedProofDeclaration + syntax [] [] [] [] + [Declaration.checkedCandidate spec planning :| []] + (CheckedExactProofAuthorization + proof + (isJust (preparedProofFirstOmission proof))) + where + requests = plannedProofRequests proof + planning + | isJust (preparedProofFirstOmission proof) = + Declaration.checkedOmittedPlanning requests [] + | otherwise = + Declaration.checkedSourceProofPlanning requests [] + +authorizeCheckedExactProof + :: CheckedExactProofAuthorization + -> [NonEmpty Declaration.ReservedCandidate] + -> Declaration.Declaration () +authorizeCheckedExactProof + (CheckedExactProofAuthorization proof hasOmission) = \case + [candidate :| []] + | hasOmission -> + Declaration.authorizeOmittedCandidate + candidate + (executePreparedProof proof) + | otherwise -> + Declaration.authorizeVampireCandidate + candidate + (executePreparedProof proof) + stages -> + Declaration.failDeclaration + (Declaration.CheckedAuthorizationCandidateShapeMismatch + 1 (length stages)) + +data CheckedFinalPreludeFoundationAuthorization = + CheckedFinalPreludeFoundationAuthorization !FoundationAxiomTag + +lowerPreparedFinalPreludeFoundationClaim + :: PreparedFinalPreludeFoundationClaim + -> Declaration.LoweringDriver + (Either + Declaration.DeclarationError + (Declaration.CheckedDeclaration + CheckedFinalPreludeFoundationAuthorization)) +lowerPreparedFinalPreludeFoundationClaim + (PreparedFinalPreludeFoundationClaim + _location alias target tag syntax) = + fmap checked + <$> Declaration.prepareCandidateSpecLowering + [] target SearchEligible [alias] + where + checked spec = + Declaration.checkedProofDeclaration + syntax [] [] [] [] + [ Declaration.checkedCandidate spec + (Declaration.checkedKernelPlanning + (Authority.FoundationLeaf tag) []) + :| [] + ] + (CheckedFinalPreludeFoundationAuthorization tag) + +authorizeCheckedFinalPreludeFoundationClaim + :: CheckedFinalPreludeFoundationAuthorization + -> [NonEmpty Declaration.ReservedCandidate] + -> Declaration.Declaration () +authorizeCheckedFinalPreludeFoundationClaim + (CheckedFinalPreludeFoundationAuthorization tag) = \case + [candidate :| []] -> + Declaration.authorizeKernelConstructionCandidate + (Authority.FoundationLeaf tag) + candidate + (pure (foundationFactDerivation tag)) + stages -> + Declaration.failDeclaration + (Declaration.CheckedAuthorizationCandidateShapeMismatch + 1 (length stages)) + +preparedProofFirstOmission :: PreparedProof -> Maybe Location +preparedProofFirstOmission = \case + PreparedImplicitAuto{} -> Nothing + PreparedQed{} -> Nothing + PreparedOmitted location _goal -> Just location + PreparedFix _identities continuation -> + preparedProofFirstOmission continuation + PreparedAssume _antecedent continuation -> + preparedProofFirstOmission continuation + PreparedTake _identities _witness _discharge continuation -> + preparedProofFirstOmission continuation + PreparedSetInduction + (PreparedCheckedSetInduction + _focus _property _antecedents _target + _hypothesis _result child) -> + preparedProofFirstOmission child + PreparedHave _claim _discharge continuation -> + preparedProofFirstOmission continuation + PreparedSuffices _goal _reduction _implication _discharge continuation -> + preparedProofFirstOmission continuation + PreparedCalculate _calculation continuation -> + preparedProofFirstOmission continuation + PreparedSince _since _evidence _claim _discharge continuation -> + preparedProofFirstOmission continuation + PreparedSubclaim _claim subproof continuation -> + preparedProofFirstOmission subproof + <|> preparedProofFirstOmission continuation + PreparedDefine _identity _body _definition continuation -> + preparedProofFirstOmission continuation + PreparedDefineRelational + _identity _body _functionality _definitions continuation -> + preparedProofFirstOmission continuation + PreparedDefineFunction _identity _graph _definition continuation -> + preparedProofFirstOmission continuation + PreparedByCase (PreparedCaseAnalysis _goal cases _exhaustive _discharge) -> + foldr + ((<|>) . preparedProofFirstOmission . preparedCaseProof) + Nothing + cases + PreparedByContradiction _goal _negation _falsum child -> + preparedProofFirstOmission child + PreparedContradiction{} -> Nothing + +plannedProofRequests + :: PreparedProof + -> [Declaration.CheckedPlannedVampireRequest] +plannedProofRequests = \case + PreparedImplicitAuto discharge -> plannedDischargeRequests discharge + PreparedQed discharge -> plannedDischargeRequests discharge + PreparedOmitted{} -> [] + PreparedFix _identities continuation -> + plannedProofRequests continuation + PreparedAssume _antecedent continuation -> + plannedProofRequests continuation + PreparedTake _identities _witness discharge continuation -> + plannedDischargeRequests discharge <> plannedProofRequests continuation + PreparedSetInduction + (PreparedCheckedSetInduction + _focus _property _antecedents _target + _hypothesis _result child) -> + plannedProofRequests child + PreparedHave _claim discharge continuation -> + plannedDischargeRequests discharge <> plannedProofRequests continuation + PreparedSuffices _goal _reduction _implication discharge continuation -> + plannedDischargeRequests discharge <> plannedProofRequests continuation + PreparedCalculate calculation continuation -> + plannedCalculationRequests calculation + <> plannedProofRequests continuation + PreparedSince _since evidence _claim discharge continuation -> + plannedSinceEvidenceRequests evidence + <> plannedDischargeRequests discharge + <> plannedProofRequests continuation + PreparedSubclaim _claim subproof continuation -> + plannedProofRequests subproof <> plannedProofRequests continuation + PreparedDefine _identity _body _definition continuation -> + plannedProofRequests continuation + PreparedDefineRelational + _identity _body functionality _definitions continuation -> + plannedDischargeRequests functionality + <> plannedProofRequests continuation + PreparedDefineFunction _identity _graph _definition continuation -> + plannedProofRequests continuation + PreparedByCase + (PreparedCaseAnalysis _goal cases _exhaustive discharge) -> + concatMap + (plannedProofRequests . preparedCaseProof) + (toList cases) + <> plannedDischargeRequests discharge + PreparedByContradiction _goal _negation _falsum child -> + plannedProofRequests child + PreparedContradiction _goal _falsum discharge -> + plannedDischargeRequests discharge + +plannedDischargeRequests + :: PreparedDischarge + -> [Declaration.CheckedPlannedVampireRequest] +plannedDischargeRequests = \case + PreparedVampireDischarge location _justification _goal obligation -> + [Declaration.checkedPlannedVampireRequest location obligation] + PreparedSetExtensionality{} -> [] + +plannedCalculationRequests + :: PreparedCalculation + -> [Declaration.CheckedPlannedVampireRequest] +plannedCalculationRequests + (PreparedCheckedCalculation + _operandType _identities _guard _first links _result) = + concatMap + (plannedDischargeRequests . preparedCalculationLinkDischarge) + (toList links) + +plannedSinceEvidenceRequests + :: PreparedSinceEvidence + -> [Declaration.CheckedPlannedVampireRequest] +plannedSinceEvidenceRequests = \case + PreparedSinceExisting{} -> [] + PreparedSinceDischarged discharge _local -> + plannedDischargeRequests discharge + +executePreparedProof + :: PreparedProof + -> Declaration.CandidateProof () +executePreparedProof = \case + PreparedImplicitAuto discharge -> + executeDischarge discharge + PreparedQed discharge -> + executeDischarge discharge + PreparedOmitted _location _goal -> + Declaration.recordOmittedUse + PreparedFix _identities continuation -> + executePreparedProof continuation + PreparedAssume _antecedent continuation -> + executePreparedProof continuation + PreparedTake _identities _witness discharge continuation -> do + executeDischarge discharge + executePreparedProof continuation + PreparedSetInduction + (PreparedCheckedSetInduction + _focus _property _antecedents _target + _hypothesis _result child) -> + executePreparedProof child + PreparedHave _claim discharge continuation -> do + executeDischarge discharge + executePreparedProof continuation + PreparedSuffices goal reduction implication discharge continuation -> do + executeDischarge discharge + executePreparedProof continuation + unless + (implyScopedCore reduction goal == Just implication) + (impossible "a prepared suffices implication diverged") + PreparedCalculate calculation continuation -> do + executePreparedCalculation calculation + executePreparedProof continuation + PreparedSince sinceProposition evidence _claim discharge continuation -> do + executeSinceEvidence sinceProposition evidence + executeDischarge discharge + executePreparedProof continuation + PreparedSubclaim _claim subproof continuation -> do + executePreparedProof subproof + executePreparedProof continuation + PreparedDefine _identity _body _definition continuation -> + executePreparedProof continuation + PreparedDefineRelational + _identity _body functionality _definitions continuation -> do + executeDischarge functionality + executePreparedProof continuation + PreparedDefineFunction _identity _graph _definition continuation -> + executePreparedProof continuation + PreparedByCase + (PreparedCaseAnalysis _goal cases _exhaustive discharge) -> do + traverse_ (executePreparedProof . preparedCaseProof) cases + executeDischarge discharge + PreparedByContradiction _goal _negation _falsum child -> + executePreparedProof child + PreparedContradiction _goal _falsum discharge -> + executeDischarge discharge + +executeDischarge + :: PreparedDischarge + -> Declaration.CandidateProof () +executeDischarge + (PreparedVampireDischarge + location _justification _goal obligation) = + Declaration.locateProofObligation location + (Declaration.acceptPreparedVampireObligation obligation) +executeDischarge PreparedSetExtensionality{} = + pure () + +executePreparedCalculation + :: PreparedCalculation + -> Declaration.CandidateProof () +executePreparedCalculation + (PreparedCheckedCalculation + _operandType _identities _guard _first links _result) = + traverse_ + (executeDischarge . preparedCalculationLinkDischarge) + links + +executeSinceEvidence + :: ScopedCheckedCore ObjectId + -> PreparedSinceEvidence + -> Declaration.CandidateProof () +executeSinceEvidence proposition = \case + PreparedSinceExisting local -> + unless (preparedLocalProposition local == proposition) + (impossible "a structural since premise diverged") + PreparedSinceDischarged discharge local -> do + executeDischarge discharge + unless + ( preparedDischargeGoal discharge == proposition + && preparedLocalProposition local == proposition + ) + (impossible "a discharged since premise diverged") + +preparedLocalProposition + :: PreparedLocal + -> ScopedCheckedCore ObjectId +preparedLocalProposition + (PreparedLocal _ordinal _origin _support proposition) = + proposition + +encodePreparedProof :: PreparedProof -> ByteString +encodePreparedProof = + encodeCache . putPreparedProof + +putPreparedProof :: PreparedProof -> CachePut +putPreparedProof = \case + PreparedImplicitAuto discharge -> do + putCacheTag 0x00 + putPreparedDischarge discharge + PreparedQed discharge -> do + putCacheTag 0x01 + putPreparedDischarge discharge + PreparedOmitted _location goal -> do + putCacheTag 0x06 + putScopedProposition goal + PreparedFix identities continuation -> do + putCacheTag 0x02 + putCacheList + (putCacheNatural . Exact.exactLocalIdValue) + identities + putPreparedProof continuation + PreparedAssume antecedent continuation -> do + putCacheTag 0x03 + putScopedProposition antecedent + putPreparedProof continuation + PreparedTake identities witness discharge continuation -> do + putCacheTag 0x08 + putCacheList + (putCacheNatural . Exact.exactLocalIdValue) + identities + putScopedProposition witness + putPreparedDischarge discharge + putPreparedProof continuation + PreparedSetInduction + (PreparedCheckedSetInduction + focus property antecedents target hypothesis result child) -> do + putCacheTag 0x07 + putPreparedSetInductionFocus focus + putScopedProposition property + putCacheList putScopedProposition antecedents + putScopedProposition target + putScopedProposition hypothesis + putScopedProposition result + putPreparedProof child + PreparedHave claim discharge continuation -> do + putCacheTag 0x04 + putScopedProposition claim + putPreparedDischarge discharge + putPreparedProof continuation + PreparedSuffices goal reduction implication discharge continuation -> do + putCacheTag 0x0c + putScopedProposition goal + putScopedProposition reduction + putScopedProposition implication + putPreparedDischarge discharge + putPreparedProof continuation + PreparedCalculate calculation continuation -> do + putCacheTag 0x0d + putPreparedCalculation calculation + putPreparedProof continuation + PreparedSince sinceProposition evidence claim discharge continuation -> do + putCacheTag 0x0e + putScopedProposition sinceProposition + putPreparedSinceEvidence evidence + putScopedProposition claim + putPreparedDischarge discharge + putPreparedProof continuation + PreparedSubclaim claim subproof continuation -> do + putCacheTag 0x05 + putScopedProposition claim + putPreparedProof subproof + putPreparedProof continuation + PreparedDefine identity body definitions continuation -> do + putCacheTag 0x09 + putCacheNatural (Exact.exactLocalIdValue identity) + putScopedTerm body + putCacheList putScopedProposition (toList definitions) + putPreparedProof continuation + PreparedDefineRelational + identity body functionality definitions continuation -> do + putCacheTag 0x11 + putCacheNatural (Exact.exactLocalIdValue identity) + putScopedTerm body + putPreparedDischarge functionality + putCacheList putScopedProposition (toList definitions) + putPreparedProof continuation + PreparedByCase caseAnalysis -> do + putCacheTag 0x0f + putPreparedCaseAnalysis caseAnalysis + PreparedByContradiction goal negation falsum child -> do + putCacheTag 0x10 + putScopedProposition goal + putScopedProposition negation + putScopedProposition falsum + putPreparedProof child + PreparedContradiction goal falsum discharge -> do + putCacheTag 0x0a + putScopedProposition goal + putScopedProposition falsum + putPreparedDischarge discharge + PreparedDefineFunction identity graph definition continuation -> do + putCacheTag 0x0b + putCacheNatural (Exact.exactLocalIdValue identity) + putScopedTerm graph + putScopedProposition definition + putPreparedProof continuation + +putPreparedSetInductionFocus + :: PreparedSetInductionFocus + -> CachePut +putPreparedSetInductionFocus = \case + PreparedInitialSetInductionFocus identity index -> do + putCacheTag 0x00 + putCacheNatural (Exact.exactLocalIdValue identity) + putCacheNatural index + PreparedLeadingSetInductionFocus identity -> do + putCacheTag 0x01 + putCacheNatural (Exact.exactLocalIdValue identity) + +putPreparedDischarge :: PreparedDischarge -> CachePut +putPreparedDischarge + (PreparedVampireDischarge + _location justification goal _obligation) = do + putPreparedDischargeSyntax justification goal +putPreparedDischarge + (PreparedSetExtensionality _location goal) = do + putCacheTag 0x03 + putScopedProposition goal + +putPreparedDischargeSyntax + :: PreparedJustification + -> ScopedCheckedCore ObjectId + -> CachePut +putPreparedDischargeSyntax justification goal = do + putPreparedJustification justification + putScopedProposition goal + +putPreparedCalculation :: PreparedCalculation -> CachePut +putPreparedCalculation + (PreparedCheckedCalculation + operandType identities calculationGuard first links result) = do + putCoreTypeCache operandType + putCacheList + (putCacheNatural . Exact.exactLocalIdValue) + identities + putCacheMaybe putScopedProposition calculationGuard + putCacheList putScopedTerm + (first : (preparedCalculationLinkDestination <$> toList links)) + putCacheList putPreparedDischarge + (preparedCalculationLinkDischarge <$> toList links) + putScopedProposition result + +putPreparedSinceEvidence :: PreparedSinceEvidence -> CachePut +putPreparedSinceEvidence = \case + PreparedSinceExisting local -> do + putCacheTag 0x00 + putPreparedLocalEvidence local + PreparedSinceDischarged discharge local -> do + putCacheTag 0x01 + putPreparedDischarge discharge + putPreparedLocalEvidence local + +putPreparedCaseAnalysis :: PreparedCaseAnalysis -> CachePut +putPreparedCaseAnalysis + (PreparedCaseAnalysis goal cases exhaustive discharge) = do + putScopedProposition goal + putCacheList putPreparedCase (toList cases) + putScopedProposition exhaustive + putPreparedDischarge discharge + +putPreparedCase :: PreparedCase -> CachePut +putPreparedCase (PreparedCase assumption proof) = do + putScopedProposition assumption + putPreparedProof proof + +putPreparedLocalEvidence :: PreparedLocal -> CachePut +putPreparedLocalEvidence + (PreparedLocal ordinal _origin support proposition) = do + putCacheNatural (Backend.localPremiseOrdinalValue ordinal) + putCacheList + (\(identity, coreType) -> do + putCacheNatural (Exact.exactLocalIdValue identity) + putCoreTypeCache coreType) + (Vector.toList support) + putScopedProposition proposition + +implicitAutoProofSyntaxId + :: ScopedCheckedCore ObjectId + -> ProofSyntaxId +implicitAutoProofSyntaxId goal = + proofSyntaxId + (encodeCache do + putCacheTag 0x00 + putPreparedDischargeSyntax PreparedAuto goal) + +putPreparedJustification :: PreparedJustification -> CachePut +putPreparedJustification = \case + PreparedAuto -> + putCacheTag 0x00 + PreparedReferences fingerprints -> do + putCacheTag 0x01 + putCacheList + putSemanticFactOccurrenceFingerprintCache + (toList fingerprints) + PreparedLocalOnly -> + putCacheTag 0x02 + +putScopedProposition + :: ScopedCheckedCore ObjectId + -> CachePut +putScopedProposition proposition = do + putCacheList putCoreTypeCache + (scopedCoreContext proposition) + putCanonicalTermCache putObjectIdCache + (scopedCoreTerm proposition) + +putScopedTerm + :: ScopedCheckedCore ObjectId + -> CachePut +putScopedTerm term = do + putCacheList putCoreTypeCache + (scopedCoreContext term) + putCoreTypeCache (scopedCoreType term) + putCanonicalTermCache putObjectIdCache + (scopedCoreTerm term) + +proofLocation :: Location -> Raw.Proof -> Location +proofLocation fallback = \case + Raw.Omitted location -> location + Raw.Qed maybeLocation _justification -> + fromMaybe fallback maybeLocation + Raw.Contradiction location _justification -> location + Raw.ByCase location _cases -> location + Raw.ByContradiction location _proof -> location + Raw.BySetInduction location _term _proof -> location + Raw.ByOrdInduction location _proof -> location + Raw.Assume location _statement _proof -> location + Raw.FixSymbolic location _variables _bound _proof -> location + Raw.FixSuchThat location _variables _statement _proof -> location + Raw.Calc location _quantifier _calculation _proof -> location + Raw.TakeVar location _variables _bound _statement _justification _proof -> + location + Raw.TakeNoun location _noun _justification _proof -> location + Raw.Have location _since _statement _justification _proof -> location + Raw.Suffices location _statement _justification _proof -> location + Raw.Subclaim location _statement _subproof _proof -> location + Raw.Define location _variable _expression _proof -> location + Raw.DefineFunction location _function _argument _value _bound _domain _proof -> + location + Raw.DefineFunctionLocal + location _function _argument _value _bound _target _rules _proof -> + location + +throwProof :: ExactProofError -> Prepare value +throwProof = + State.lift . Except.throwError + +liftDriver + :: Declaration.LoweringDriver value + -> Prepare value +liftDriver = + State.lift . Except.lift + +stableUnique :: Ord value => [value] -> [value] +stableUnique = + reverse . snd + . foldl' + (\(seen, reversed) value -> + if value `Set.member` seen + then (seen, reversed) + else + ( Set.insert value seen + , value : reversed + )) + (Set.empty, []) diff --git a/source/Felix/Checking/Exact/Vocabulary.hs b/source/Felix/Checking/Exact/Vocabulary.hs new file mode 100644 index 0000000..a712bf1 --- /dev/null +++ b/source/Felix/Checking/Exact/Vocabulary.hs @@ -0,0 +1,218 @@ +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE NoImplicitPrelude #-} + +-- | Semantic classification shared by the exact source compilers. +module Felix.Checking.Exact.Vocabulary + ( FixedSemanticMeaning(..) + , fixedSemanticMeaning + , lowerFixedEqualityPredicate + , ExactSymbolClass(..) + , classifyExactSymbol + , FixedSetTermDispatch(..) + , dispatchFixedSetTerm + ) where + +import Base hiding (Empty) +import Felix.Checking.Core +import Felix.Checking.Semantic +import Felix.Syntax.Abstract qualified as Raw +import Felix.Syntax.Internal qualified as Internal +import Felix.Syntax.Lexicon qualified as Lexicon + +import Data.List.NonEmpty qualified as NonEmpty +import Data.Map.Strict qualified as Map + + +data FixedSemanticMeaning + = FixedEquality + | FixedDisequality + | FixedIntrinsic !CoreIntrinsicTag + | FixedNegatedIntrinsic !CoreIntrinsicTag + deriving stock (Show, Eq) + +fixedSemanticMeaning + :: SemanticGlobalKey + -> Maybe FixedSemanticMeaning +fixedSemanticMeaning key = + Map.lookup key fixedSemanticVocabulary + +-- This inventory owns every exact source form that bypasses global lookup. +fixedSemanticVocabulary + :: Map.Map SemanticGlobalKey FixedSemanticMeaning +fixedSemanticVocabulary = + Map.fromList + [ ( relationKey Raw.EqSymbol + , FixedEquality + ) + , ( SemanticRightAdjective + (Raw.lexicalItemPattern + Lexicon.builtinEqualityRightAdjective) + , FixedEquality + ) + , ( verbKey Lexicon.builtinEqualityVerb + , FixedEquality + ) + , ( relationKey Raw.ElementSymbol + , FixedIntrinsic Member + ) + , ( relationKey Raw.NotElementSymbol + , FixedNegatedIntrinsic Member + ) + , ( relationKey Raw.NeqSymbol + , FixedDisequality + ) + , ( nounKey Lexicon.builtinElementNoun + , FixedIntrinsic Member + ) + , ( expressionKey + (Raw.TokenCons (Raw.Command "emptyset") Raw.End) + , FixedIntrinsic Empty + ) + , ( expressionKey (Raw.mixfixPattern Raw.UnionsSymbol) + , FixedIntrinsic FamilyUnion + ) + , ( expressionKey (unaryCommandPattern "pow") + , FixedIntrinsic PowerSet + ) + , ( expressionKey (unaryCommandPattern "cumul") + , FixedIntrinsic UnivOf + ) + , ( expressionKey (Raw.mixfixPattern Raw.UpairSymbol) + , FixedIntrinsic PairSet + ) + ] + where + relationKey relation = + SemanticRelation + (Raw.relationSymbolToken relation) + (Raw.relationSymbolParameterArity relation) + nounKey item = + let patterns = Raw.lexicalItemSgPlPattern item + in SemanticNoun (Raw.sg patterns) (Raw.pl patterns) + verbKey item = + let patterns = Raw.lexicalItemSgPlPattern item + in SemanticVerb (Raw.sg patterns) (Raw.pl patterns) + expressionKey = SemanticExpressionFunction + +-- | Lower the fixed proposition meanings shared by raw exact elaboration and +-- the reusable internal-formula path. Membership deliberately retains its +-- carrier-aware source lowering and is not handled here. +lowerFixedEqualityPredicate + :: FixedSemanticMeaning + -> [CanonicalTerm global] + -> Maybe (CanonicalTerm global) +lowerFixedEqualityPredicate meaning arguments = + case (meaning, arguments) of + (FixedEquality, [left, right]) -> + Just (CEq TySet left right) + (FixedDisequality, [left, right]) -> + Just (CImp (CEq TySet left right) CFalsum) + _ -> + Nothing + +unaryCommandPattern :: Text -> Raw.Pattern +unaryCommandPattern command = + Raw.TokenCons (Raw.Command command) + (Raw.TokenCons Raw.InvisibleBraceL + (Raw.HoleCons + (Raw.TokenCons Raw.InvisibleBraceR Raw.End))) + +data ExactSymbolClass + = ExactClosedLiteral + | ExactFixedPrimitive !FixedSemanticMeaning + | ExactSourceGlobal !(NonEmpty SemanticGlobalKey) + | ExactUnsupportedSymbol + deriving stock (Show, Eq) + +classifyExactSymbol :: Internal.Symbol -> ExactSymbolClass +classifyExactSymbol symbol = + case symbol of + Internal.SymbolInteger{} -> + ExactClosedLiteral + _ -> + case NonEmpty.nonEmpty (semanticKeys symbol) of + Nothing -> + ExactUnsupportedSymbol + Just keys -> + case firstFixed keys of + Just meaning -> + ExactFixedPrimitive meaning + Nothing -> + ExactSourceGlobal keys + where + firstFixed = + foldr + (\key found -> fixedSemanticMeaning key <|> found) + Nothing + +semanticKeys :: Internal.Symbol -> [SemanticGlobalKey] +semanticKeys = \case + Internal.SymbolMixfix symbol -> + [SemanticExpressionFunction (Raw.mixfixPattern symbol)] + Internal.SymbolFun item -> + let patterns = Raw.lexicalItemSgPlPattern item + in [SemanticFunctionPhrase (Raw.sg patterns) (Raw.pl patterns)] + Internal.SymbolPredicate predicate -> + case predicate of + Internal.PredicateAdj item -> + [ SemanticLeftAdjective (Raw.lexicalItemPattern item) + , SemanticRightAdjective (Raw.lexicalItemPattern item) + ] + Internal.PredicateVerb item -> + let patterns = Raw.lexicalItemSgPlPattern item + in [SemanticVerb (Raw.sg patterns) (Raw.pl patterns)] + Internal.PredicateNoun item -> + let patterns = Raw.lexicalItemSgPlPattern item + in [SemanticNoun (Raw.sg patterns) (Raw.pl patterns)] + Internal.PredicateRelation relation -> + [ SemanticRelation + (Raw.relationSymbolToken relation) + (Raw.relationSymbolParameterArity relation) + ] + Internal.PredicateSymbol{} -> [] + Internal.PredicateNounStruct{} -> [] + Internal.SymbolInteger{} -> [] + +-- | Result of interpreting a symbol already classified by the fixed exact +-- vocabulary as a set-valued term. +data FixedSetTermDispatch global + = NotFixedSetTerm + | LoweredFixedSetTerm !(CanonicalTerm global) + | RejectedFixedSetTerm + deriving stock (Show, Eq) + +-- | Interpret every fixed symbol that can occur in the reusable internal-term +-- lowering. Fixed relations are handled by formula lowering. +dispatchFixedSetTerm + :: Internal.Symbol + -> [CanonicalTerm global] + -> FixedSetTermDispatch global +dispatchFixedSetTerm symbol arguments = + case classifyExactSymbol symbol of + ExactFixedPrimitive meaning -> + case meaning of + FixedIntrinsic intrinsic -> + applyIntrinsic + (CIntrinsic intrinsic) + (coreIntrinsicType intrinsic) + arguments + FixedNegatedIntrinsic _intrinsic -> + RejectedFixedSetTerm + FixedEquality -> + RejectedFixedSetTerm + FixedDisequality -> + RejectedFixedSetTerm + _ -> + NotFixedSetTerm + where + applyIntrinsic term coreType remaining = + case (coreType, remaining) of + (TySet, []) -> + LoweredFixedSetTerm term + (TyArrow TySet resultType, argument : rest) -> + applyIntrinsic + (CApp term argument) + resultType + rest + _ -> + RejectedFixedSetTerm |