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 | 691 | ||||
| -rw-r--r-- | source/Checking/Exact/Proof.hs | 1359 | ||||
| -rw-r--r-- | source/Checking/Exact/Vocabulary.hs | 190 |
5 files changed, 0 insertions, 3107 deletions
diff --git a/source/Checking/Exact/Datatype.hs b/source/Checking/Exact/Datatype.hs deleted file mode 100644 index 14ee58c..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 Meaning qualified -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 ca6fb83..0000000 --- a/source/Checking/Exact/Inductive.hs +++ /dev/null @@ -1,691 +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 Meaning qualified -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] - -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 - | ExactInductiveNestedRecursion !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 - ExactInductiveNestedRecursion 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" - ExactInductiveNestedRecursion{} -> - "nested inductive recursion is not supported by the typed checker" - 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)) - | matchesCarrier carrier parameters recursiveCarrier -> - Right - (Typed.DirectRecursiveCondition recursiveTerm) - | otherwise -> - Left - (ExactInductiveNestedRecursion - (termLocation recursiveCarrier)) - _ -> - Left - (ExactInductiveNestedRecursion - (termLocation formula)) - -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 -> - Internal.mentionedSymbols term - -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 - objects = maybeToList asserted - definition <- - Declaration.prepareDefinitionEquationSpecLowering - objects identity alias - preparedFacts <- - traverse - (\fact -> - Declaration.prepareCandidateSpecLowering - objects - (embedClosedCore [] - (Typed.typedInductiveFactTarget fact)) - SearchEligible - [markerAlias - (Typed.typedInductiveFactMarker fact)]) - facts - pure do - definitionSpec <- definition - factSpecs <- sequence preparedFacts - pure - (Declaration.checkedCompiledDeclaration - syntax - objects - [] - [semanticGlobalBinding key (GlobalReference identity)] - [] - [ Declaration.checkedCandidate definitionSpec - (Declaration.checkedDefinitionEquationPlanning identity) - :| [ Declaration.checkedCandidate factSpec - (Declaration.checkedKernelPlanning - (GuardedFoundationRules - (guardedRuleSet - (Typed.typedInductiveFactRules - fact))) - guards) - | (factSpec, fact) <- - zip (toList factSpecs) (toList facts) - ] - ] - (CheckedExactInductiveAuthorization - identity typed guards)) - where - markerAlias (Raw.Marker name) = - semanticName name - -authorizeCheckedExactInductive - :: CheckedExactInductiveAuthorization - -> [NonEmpty Declaration.ReservedCandidate] - -> Declaration.Declaration () -authorizeCheckedExactInductive - (CheckedExactInductiveAuthorization identity typed guards) = \case - [definitionCandidate :| candidates] -> do - 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)) - stages -> - Declaration.failDeclaration - (Declaration.CheckedAuthorizationCandidateShapeMismatch - 1 (length stages)) - where - authorizeFact candidate fact = - Declaration.authorizeKernelConstructionCandidate - (GuardedFoundationRules - (guardedRuleSet - (Typed.typedInductiveFactRules fact))) - candidate do - traverse_ Declaration.useAuthorizedFact guards - 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)) - putCacheText (semanticNameText alias) - putCacheList putFact - (toList (Typed.typedInductiveFacts typed)) - where - 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 40911b0..0000000 --- a/source/Checking/Exact/Proof.hs +++ /dev/null @@ -1,1359 +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.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.Set qualified as Set -import Data.Text qualified as Text -import Data.Vector (Vector) -import Numeric.Natural (Natural) - - -data ExactProofError - = ExactProofUnsupportedClaim !Location - | ExactProofUnsupportedStep !Location - | ExactProofBoundedFixNotSupported !Location - | ExactProofBoundedTakeNotSupported !Location - | ExactProofSetInductionVariableRequired !Location - | ExactProofSetInductionVariableNotActive - !Location !Raw.VarSymbol - | ExactProofSetInductionNotOutermost !Location - | ExactProofSetInductionGoalMismatch !Location - | ExactProofSetExtensionalityGoalMismatch !Location - | ExactProofSetExtensionalityDirectionsUnavailable !Location - | ExactProofExpectedUniversalGoal !Location - | ExactProofExpectedImplicationGoal !Location - | ExactProofGoalStatementMismatch !Location - | ExactProofContradictionGoalMismatch !Location - | 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 - ExactProofBoundedFixNotSupported location -> location - ExactProofBoundedTakeNotSupported location -> location - ExactProofSetInductionVariableRequired location -> location - ExactProofSetInductionVariableNotActive location _variable -> - location - ExactProofSetInductionNotOutermost location -> location - ExactProofSetInductionGoalMismatch location -> location - ExactProofSetExtensionalityGoalMismatch location -> location - ExactProofSetExtensionalityDirectionsUnavailable location -> location - ExactProofExpectedUniversalGoal location -> location - ExactProofExpectedImplicationGoal location -> location - ExactProofGoalStatementMismatch location -> location - ExactProofContradictionGoalMismatch location -> 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" - ExactProofBoundedFixNotSupported location -> - at location <> "bounded proof binders are not yet supported" - ExactProofBoundedTakeNotSupported location -> - at location <> "bounded proof witnesses are not yet supported" - ExactProofSetInductionVariableRequired location -> - at location <> "exact set induction requires a named set variable" - ExactProofSetInductionVariableNotActive location variable -> - at location <> "the set-induction variable " <> shown variable - <> " is not an active exact binder" - ExactProofSetInductionNotOutermost location -> - at location <> "set induction must currently be outermost" - 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" - ExactProofContradictionGoalMismatch location -> - at location <> "contradiction requires falsum as the current goal" - ExactProofLocalFunctionBinderMismatch location -> - at location <> "the function argument must match its domain binder" - ExactProofLocalFunctionNameConflict location -> - at location <> "the function and argument names must be distinct" - ExactProofUnknownReference location marker -> - at location <> "the cited fact " <> shown marker <> " is not visible" - ExactProofElaborationFailed failure -> - 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 - 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 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 - !(ScopedCheckedCore ObjectId) - !PreparedDischarge - | PreparedHave - !(ScopedCheckedCore ObjectId) - !PreparedDischarge - !PreparedProof - | PreparedSubclaim - !(ScopedCheckedCore ObjectId) - !PreparedProof - !PreparedProof - | PreparedDefine - !Exact.ExactLocalId - !(ScopedCheckedCore ObjectId) - !(ScopedCheckedCore ObjectId) - !PreparedProof - | PreparedDefineFunction - !Exact.ExactLocalId - !(ScopedCheckedCore ObjectId) - !(ScopedCheckedCore ObjectId) - !PreparedProof - | PreparedContradiction !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) - bodyProof <- - case explicitProof of - Nothing -> - PreparedImplicitAuto - <$> prepareDischargeWith - DirectDischarge - [] - Nothing - location - context - locals - bodyGoal - Raw.JustificationEmpty - Just sourceProof -> - prepareProof - location - context - locals - (Just antecedents) - 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) - -prepareProof - :: Location - -> Exact.ExactBinderContext - -> [PreparedLocal] - -- Only the initial proof carries set-induction antecedents. - -> Maybe [ScopedCheckedCore ObjectId] - -> ScopedCheckedCore ObjectId - -> Raw.Proof - -> Prepare PreparedProof -prepareProof fallback context locals inductionAntecedents 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 - unless (bound == Raw.Unbounded) - (throwProof - (ExactProofBoundedFixNotSupported location)) - (context', goal', identities) <- - openFixedVariables context goal variables - PreparedFix identities - <$> prepareProof - fallback - context' - locals - Nothing - goal' - continuation - Raw.Assume location statement continuation -> do - (antecedent, conclusion) <- - maybe - (throwProof - (ExactProofExpectedImplicationGoal location)) - pure - (openScopedImplication goal) - supplied <- prepareStatement context statement - unless - (Exact.preparedExactPropositionCore supplied - == antecedent) - (throwProof - (ExactProofGoalStatementMismatch location)) - local <- allocateLocal ExactAssumption context antecedent - PreparedAssume antecedent - <$> prepareProof - fallback - context - (locals <> [local]) - Nothing - conclusion - continuation - Raw.TakeVar location variables bound statement justification continuation -> do - unless (bound == Raw.Unbounded) - (throwProof - (ExactProofBoundedTakeNotSupported location)) - identities <- - traverse (const allocateLocalIdentity) variables - context' <- - either - (throwProof . ExactProofElaborationFailed) - pure - (Exact.extendExactBinderContext - (NonEmpty.zip identities variables) - context) - witness <- - Exact.preparedExactPropositionCore - <$> prepareStatement context' statement - let witnessCount = length (toList variables) - existence = closeTakenWitnesses witnessCount witness - goal' = weakenForTakenWitnesses witnessCount goal - discharge <- - prepareDischarge - location context locals existence justification - local <- allocateLocal ExactAssumption context' witness - PreparedTake (toList identities) witness discharge - <$> prepareProof - fallback - context' - (locals <> [local]) - Nothing - goal' - continuation - Raw.BySetInduction location variable continuation -> - case (inductionAntecedents, continuation) of - (Nothing, _proof) -> - throwProof - (ExactProofSetInductionNotOutermost location) - (Just antecedents, Raw.Qed maybeLocation justification) -> do - sourceVariable <- - case variable of - Just (Raw.TermExpr (Raw.ExprVar candidate)) -> - pure candidate - _ -> - throwProof - (ExactProofSetInductionVariableRequired - location) - selected <- - maybe - (throwProof - (ExactProofSetInductionVariableNotActive - location - sourceVariable)) - pure - (Exact.exactBinderContextIndex - sourceVariable context) - let property = - foldr implyChecked goal antecedents - hypothesis <- - maybe - (throwProof - (ExactProofSetInductionGoalMismatch - location)) - pure - (scopedSetInductionHypothesis selected property) - local <- allocateLocal ExactAssumption context hypothesis - PreparedSetInduction hypothesis - <$> prepareDischarge - (fromMaybe location maybeLocation) - context - (locals <> [local]) - goal - justification - (Just _antecedents, _proof) -> - throwProof (ExactProofUnsupportedStep location) - Raw.Have location since statement justification continuation -> do - when (isJust since) - (throwProof (ExactProofUnsupportedStep location)) - 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]) - Nothing - goal - continuation - Raw.Subclaim location statement subproof continuation -> do - claim <- - Exact.preparedExactPropositionCore - <$> prepareStatement context statement - preparedSubproof <- - prepareProof - location - context - locals - Nothing - claim - subproof - local <- allocateLocal ExactDerivedClaim context claim - PreparedSubclaim claim preparedSubproof - <$> prepareProof - fallback - context - (locals <> [local]) - Nothing - goal - continuation - Raw.Define _location variable expression continuation -> do - body <- - Exact.preparedExactSetExpressionCore - <$> ( liftDriver - (Exact.prepareExactSetExpression - context expression) - >>= either - (throwProof . ExactProofElaborationFailed) - pure - ) - identity <- allocateLocalIdentity - context' <- - either - (throwProof . ExactProofElaborationFailed) - pure - (Exact.extendExactBinderContext - ((identity, variable) :| []) - context) - 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]) - Nothing - (weakenCheckedScopedCore TySet goal) - continuation - Raw.DefineFunction - location function argument value bound domain continuation -> do - unless (argument == bound) - (throwProof - (ExactProofLocalFunctionBinderMismatch (locate bound))) - when (function == argument) - (throwProof - (ExactProofLocalFunctionNameConflict (locate function))) - argumentIdentity <- allocateLocalIdentity - argumentContext <- - either - (throwProof . ExactProofElaborationFailed) - pure - (Exact.extendExactBinderContext - ((argumentIdentity, argument) :| []) - context) - graph <- - liftDriver - (Exact.prepareExactLocalFunctionGraph - location context argumentContext domain value) - >>= either - (throwProof . ExactProofElaborationFailed) - pure - functionIdentity <- allocateLocalIdentity - functionContext <- - either - (throwProof . ExactProofElaborationFailed) - pure - (Exact.extendExactBinderContext - ((functionIdentity, function) :| []) - context) - replacementCharacteristic <- - liftDriver - (Declaration.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]) - Nothing - (weakenCheckedScopedCore TySet goal) - continuation - Raw.Contradiction location justification -> do - unless - ( scopedCoreType goal == TyProp - && scopedCoreTerm goal == CFalsum - ) - (throwProof - (ExactProofContradictionGoalMismatch location)) - PreparedContradiction - <$> prepareDischargeWith - IndirectContradictionDischarge - [] - Nothing - location - context - locals - goal - justification - proof -> - throwProof - (ExactProofUnsupportedStep - (proofLocation fallback proof)) - where - implyChecked antecedent conclusion = - fromMaybe - (impossible "an exact claim antecedent changed context") - (implyScopedCore antecedent conclusion) - --- 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) - -prepareDischarge - :: Location - -> Exact.ExactBinderContext - -> [PreparedLocal] - -> ScopedCheckedCore ObjectId - -> Raw.Justification - -> Prepare PreparedDischarge -prepareDischarge location context locals goal justification = - prepareDischargeWith - DirectDischarge - [] Nothing location context locals goal justification - -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 - -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 _hypothesis _discharge -> Nothing - PreparedHave _claim _discharge continuation -> - preparedProofFirstOmission continuation - PreparedSubclaim _claim subproof continuation -> - preparedProofFirstOmission subproof - <|> preparedProofFirstOmission continuation - PreparedDefine _identity _body _definition continuation -> - preparedProofFirstOmission continuation - PreparedDefineFunction _identity _graph _definition continuation -> - preparedProofFirstOmission continuation - 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 _hypothesis discharge -> - plannedDischargeRequests discharge - PreparedHave _claim discharge continuation -> - plannedDischargeRequests discharge <> plannedProofRequests continuation - PreparedSubclaim _claim subproof continuation -> - plannedProofRequests subproof <> plannedProofRequests continuation - PreparedDefine _identity _body _definition continuation -> - plannedProofRequests continuation - PreparedDefineFunction _identity _graph _definition continuation -> - plannedProofRequests continuation - PreparedContradiction discharge -> - plannedDischargeRequests discharge - -plannedDischargeRequests - :: PreparedDischarge - -> [Declaration.CheckedPlannedVampireRequest] -plannedDischargeRequests = \case - PreparedVampireDischarge location _justification _goal obligation -> - [Declaration.checkedPlannedVampireRequest location obligation] - PreparedSetExtensionality{} -> [] - -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 _hypothesis discharge -> - executeDischarge discharge - PreparedHave _claim discharge continuation -> do - executeDischarge discharge - executePreparedProof continuation - PreparedSubclaim _claim subproof continuation -> do - executePreparedProof subproof - executePreparedProof continuation - PreparedDefine _identity _body _definition continuation -> - executePreparedProof continuation - PreparedDefineFunction _identity _graph _definition continuation -> - executePreparedProof continuation - PreparedContradiction discharge -> - executeDischarge discharge - -executeDischarge - :: PreparedDischarge - -> Declaration.CandidateProof () -executeDischarge - (PreparedVampireDischarge - location _justification _goal obligation) = - Declaration.locateProofObligation location - (Declaration.acceptPreparedVampireObligation obligation) -executeDischarge PreparedSetExtensionality{} = - pure () - -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 hypothesis discharge -> do - putCacheTag 0x07 - putScopedProposition hypothesis - putPreparedDischarge discharge - PreparedHave claim discharge continuation -> do - putCacheTag 0x04 - putScopedProposition claim - putPreparedDischarge discharge - putPreparedProof continuation - PreparedSubclaim claim subproof continuation -> do - putCacheTag 0x05 - putScopedProposition claim - putPreparedProof subproof - putPreparedProof continuation - PreparedDefine identity body definition continuation -> do - putCacheTag 0x09 - putCacheNatural (Exact.exactLocalIdValue identity) - putScopedTerm body - putScopedProposition definition - putPreparedProof continuation - PreparedContradiction discharge -> do - putCacheTag 0x0a - putPreparedDischarge discharge - PreparedDefineFunction identity graph definition continuation -> do - putCacheTag 0x0b - putCacheNatural (Exact.exactLocalIdValue identity) - putScopedTerm graph - putScopedProposition definition - putPreparedProof continuation - -putPreparedDischarge :: PreparedDischarge -> CachePut -putPreparedDischarge - (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 - -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 5701f64..0000000 --- a/source/Checking/Exact/Vocabulary.hs +++ /dev/null @@ -1,190 +0,0 @@ -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE NoImplicitPrelude #-} - --- | Semantic classification shared by the exact source compilers. -module Checking.Exact.Vocabulary - ( FixedSemanticMeaning(..) - , fixedSemanticMeaning - , 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 - ) - , ( 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 (unaryCommandPattern "unions") - , 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) - expressionKey = SemanticExpressionFunction - -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 |