diff options
Diffstat (limited to 'source/Checking/Exact')
| -rw-r--r-- | source/Checking/Exact/Datatype.hs | 751 | ||||
| -rw-r--r-- | source/Checking/Exact/Global.hs | 116 | ||||
| -rw-r--r-- | source/Checking/Exact/Inductive.hs | 838 | ||||
| -rw-r--r-- | source/Checking/Exact/Proof.hs | 2639 | ||||
| -rw-r--r-- | source/Checking/Exact/Vocabulary.hs | 218 |
5 files changed, 0 insertions, 4562 deletions
diff --git a/source/Checking/Exact/Datatype.hs b/source/Checking/Exact/Datatype.hs deleted file mode 100644 index 61d99e5..0000000 --- a/source/Checking/Exact/Datatype.hs +++ /dev/null @@ -1,751 +0,0 @@ -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE NoImplicitPrelude #-} - --- | Exact preparation of deterministic datatype declarations. -module 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 Checking.Authority -import Checking.Core -import Checking.Datatype qualified as Datatype -import Checking.Declaration qualified as Declaration -import Checking.Exact.Global qualified as ExactGlobal -import Checking.Exact.Vocabulary -import Checking.Identity -import Checking.Semantic -import Checking.Typed.Inductive qualified as Typed -import Felix.Cache.Codec -import Felix.Module -import Felix.Meaning qualified as Meaning -import Report.Location -import Syntax.Abstract qualified as Raw -import Syntax.Interface -import 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/Checking/Exact/Global.hs b/source/Checking/Exact/Global.hs deleted file mode 100644 index 772a7e2..0000000 --- a/source/Checking/Exact/Global.hs +++ /dev/null @@ -1,116 +0,0 @@ -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE NoImplicitPrelude #-} - --- | Exact resolution of source symbols to checked semantic globals. -module Checking.Exact.Global - ( ExactGlobalResolutionError(..) - , resolveExactSourceGlobals - ) where - -import Base -import Checking.Core -import Checking.Declaration qualified as Declaration -import Checking.Exact.Vocabulary -import Checking.Identity -import Checking.Semantic -import Checking.Typed.Inductive qualified as Typed -import 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/Checking/Exact/Inductive.hs b/source/Checking/Exact/Inductive.hs deleted file mode 100644 index 441c773..0000000 --- a/source/Checking/Exact/Inductive.hs +++ /dev/null @@ -1,838 +0,0 @@ -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE NoImplicitPrelude #-} - --- | Exact preparation and atomic publication of direct set inductives. -module Checking.Exact.Inductive - ( PreparedExactInductive - , preparedExactInductiveCarrierId - , preparedExactInductiveCarrierType - , preparedExactInductiveCarrierBody - , preparedExactInductiveGuardTargets - , preparedExactInductiveFacts - , prepareExactInductive - , CheckedExactInductiveAuthorization - , lowerPreparedExactInductive - , authorizeCheckedExactInductive - , ExactInductiveError(..) - , exactInductiveErrorLocation - , renderExactInductiveError - ) where - -import Base hiding (Empty) -import Checking.Authority -import Checking.Core -import Checking.Declaration qualified as Declaration -import Checking.Exact.Global qualified as ExactGlobal -import Checking.Exact.Vocabulary -import Checking.Foundation -import Checking.Identity -import Checking.Semantic -import Checking.Typed.Inductive qualified as Typed -import Felix.Cache.Codec -import Felix.Meaning qualified as Meaning -import Report.Location -import Syntax.Abstract qualified as Raw -import Syntax.Interface -import 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/Checking/Exact/Proof.hs b/source/Checking/Exact/Proof.hs deleted file mode 100644 index 92ff500..0000000 --- a/source/Checking/Exact/Proof.hs +++ /dev/null @@ -1,2639 +0,0 @@ -{-# 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 Checking.Exact.Proof - ( PreparedExactProof - , preparedExactProofSyntaxId - , preparedExactProofFirstOmission - , prepareExactProof - , CheckedExactProofAuthorization - , lowerPreparedExactProof - , authorizeCheckedExactProof - , PreparedFinalPreludeFoundationClaim - , prepareFinalPreludeFoundationClaim - , CheckedFinalPreludeFoundationAuthorization - , lowerPreparedFinalPreludeFoundationClaim - , authorizeCheckedFinalPreludeFoundationClaim - , ExactProofError(..) - , exactProofErrorLocation - , renderExactProofError - ) where - -import Base -import Checking.Authority qualified as Authority -import Checking.Backend.Problem qualified as Backend -import Checking.Core -import Checking.Declaration qualified as Declaration -import Checking.Exact qualified as Exact -import Checking.Foundation -import Checking.Identity -import Checking.Kernel.Derivation (foundationFactDerivation) -import Checking.Kernel.Proof qualified as KernelProof -import Checking.SetConstruction -import Checking.Semantic -import Felix.Cache.Codec -import Report.Location -import 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/Checking/Exact/Vocabulary.hs b/source/Checking/Exact/Vocabulary.hs deleted file mode 100644 index 45a2844..0000000 --- a/source/Checking/Exact/Vocabulary.hs +++ /dev/null @@ -1,218 +0,0 @@ -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE NoImplicitPrelude #-} - --- | Semantic classification shared by the exact source compilers. -module Checking.Exact.Vocabulary - ( FixedSemanticMeaning(..) - , fixedSemanticMeaning - , lowerFixedEqualityPredicate - , ExactSymbolClass(..) - , classifyExactSymbol - , FixedSetTermDispatch(..) - , dispatchFixedSetTerm - ) where - -import Base hiding (Empty) -import Checking.Core -import Checking.Semantic -import Syntax.Abstract qualified as Raw -import Syntax.Internal qualified as Internal -import 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 |