diff options
Diffstat (limited to 'source/Checking/Exact/Datatype.hs')
| -rw-r--r-- | source/Checking/Exact/Datatype.hs | 751 |
1 files changed, 0 insertions, 751 deletions
diff --git a/source/Checking/Exact/Datatype.hs b/source/Checking/Exact/Datatype.hs deleted file mode 100644 index 61d99e5..0000000 --- a/source/Checking/Exact/Datatype.hs +++ /dev/null @@ -1,751 +0,0 @@ -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE NoImplicitPrelude #-} - --- | Exact preparation of deterministic datatype declarations. -module Checking.Exact.Datatype - ( PreparedExactDatatype - , preparedExactDatatypeObjects - , preparedExactDatatypeBindings - , PreparedExactDatatypeFact - , preparedExactDatatypeFacts - , preparedExactDatatypeFactMarker - , preparedExactDatatypeFactTarget - , preparedExactDatatypeFactReference - , preparedExactDatatypeDescriptor - , prepareExactDatatype - , CheckedExactDatatypeAuthorization - , lowerPreparedExactDatatype - , authorizeCheckedExactDatatype - , ExactDatatypeError(..) - , exactDatatypeErrorLocation - , renderExactDatatypeError - ) where - -import Base hiding (Empty) -import Checking.Authority -import Checking.Core -import Checking.Datatype qualified as Datatype -import Checking.Declaration qualified as Declaration -import Checking.Exact.Global qualified as ExactGlobal -import Checking.Exact.Vocabulary -import Checking.Identity -import Checking.Semantic -import Checking.Typed.Inductive qualified as Typed -import Felix.Cache.Codec -import Felix.Module -import Felix.Meaning qualified as Meaning -import Report.Location -import Syntax.Abstract qualified as Raw -import Syntax.Interface -import Syntax.Internal qualified as Internal - -import Control.Monad (unless, when) -import Control.Monad.Except (ExceptT) -import Control.Monad.Except qualified as Except -import Data.Bifunctor (first) -import Data.ByteString (ByteString) -import Data.List.NonEmpty qualified as NonEmpty -import Data.Map.Strict qualified as Map -import Data.Set qualified as Set -import Data.Text qualified as Text -import Numeric.Natural (Natural) - - -data PreparedDatatypeObject = PreparedDatatypeObject - !Internal.Symbol - !SemanticGlobalKey - !CoreType - !ObjectId - !AssertedObject - -data PreparedExactDatatypeFact = PreparedExactDatatypeFact - !Internal.Marker - !(FrozenCheckedCore ObjectId) - !TheoremRef - -preparedExactDatatypeFactMarker - :: PreparedExactDatatypeFact - -> Internal.Marker -preparedExactDatatypeFactMarker - (PreparedExactDatatypeFact marker _target _reference) = - marker - -preparedExactDatatypeFactTarget - :: PreparedExactDatatypeFact - -> FrozenCheckedCore ObjectId -preparedExactDatatypeFactTarget - (PreparedExactDatatypeFact _marker target _reference) = - target - -preparedExactDatatypeFactReference - :: PreparedExactDatatypeFact - -> TheoremRef -preparedExactDatatypeFactReference - (PreparedExactDatatypeFact _marker _target reference) = - reference - -data PreparedExactDatatype = PreparedExactDatatype - !Location - !DeclarationSyntaxId - !(NonEmpty PreparedDatatypeObject) - !(NonEmpty PreparedExactDatatypeFact) - !DatatypeCompilationDescriptor - -data CheckedExactDatatypeAuthorization = - CheckedExactDatatypeAuthorization - !DatatypeCompilationDescriptor - !ObjectId - !(NonEmpty ObjectId) - -preparedExactDatatypeObjects - :: PreparedExactDatatype - -> NonEmpty (ObjectId, CoreType) -preparedExactDatatypeObjects - (PreparedExactDatatype _location _syntax objects _facts _descriptor) = - fmap - (\(PreparedDatatypeObject _symbol _key coreType identity _asserted) -> - (identity, coreType)) - objects - -preparedExactDatatypeBindings - :: PreparedExactDatatype - -> NonEmpty (SemanticGlobalKey, SemanticGlobalTarget) -preparedExactDatatypeBindings - (PreparedExactDatatype _location _syntax objects _facts _descriptor) = - fmap - (\(PreparedDatatypeObject _symbol key _coreType identity _asserted) -> - (key, GlobalReference identity)) - objects - -preparedExactDatatypeFacts - :: PreparedExactDatatype - -> NonEmpty PreparedExactDatatypeFact -preparedExactDatatypeFacts - (PreparedExactDatatype _location _syntax _objects facts _descriptor) = - facts - -preparedExactDatatypeDescriptor - :: PreparedExactDatatype - -> DatatypeCompilationDescriptor -preparedExactDatatypeDescriptor - (PreparedExactDatatype _location _syntax _objects _facts descriptor) = - descriptor - -lowerPreparedExactDatatype - :: PreparedExactDatatype - -> Declaration.LoweringDriver - (Either - Declaration.DeclarationError - (Declaration.CheckedDeclaration - CheckedExactDatatypeAuthorization)) -lowerPreparedExactDatatype - (PreparedExactDatatype _location syntax objects facts descriptor) = - do - prepared <- - traverse - (\(PreparedExactDatatypeFact marker target _reference) -> - Declaration.prepareFrozenCandidateSpecLowering - assertedObjects - target - SearchEligible - [markerAlias marker]) - facts - pure (buildChecked <$> sequence prepared) - where - assertedObjects = - toList - (fmap - (\(PreparedDatatypeObject - _symbol _key _coreType _identity asserted) -> asserted) - objects) - bindings = - toList - (fmap - (\(PreparedDatatypeObject - _symbol key _coreType identity _asserted) -> - semanticGlobalBinding key (GlobalReference identity)) - objects) - carrier :| constructors = fmap objectIdentity objects - constructorIds = - case constructors of - firstConstructor : remainingConstructors -> - firstConstructor :| remainingConstructors - [] -> impossible "a prepared datatype has no constructor" - buildChecked specs = - Declaration.checkedCompiledDeclaration - syntax - assertedObjects - [] - bindings - [] - [ fmap - (\spec -> - Declaration.checkedCandidate - spec - (Declaration.checkedDatatypePlanning descriptor)) - specs - ] - (CheckedExactDatatypeAuthorization - descriptor carrier constructorIds) - - markerAlias (Internal.Marker name) = semanticName name - - objectIdentity - (PreparedDatatypeObject - _symbol _key _coreType identity _asserted) = - identity - -authorizeCheckedExactDatatype - :: CheckedExactDatatypeAuthorization - -> [NonEmpty Declaration.ReservedCandidate] - -> Declaration.Declaration () -authorizeCheckedExactDatatype - (CheckedExactDatatypeAuthorization descriptor carrier constructors) = - \case - [candidates] -> - Declaration.authorizeDatatypeCompilationCandidates - descriptor carrier constructors candidates - stages -> - Declaration.failDeclaration - (Declaration.CheckedAuthorizationCandidateShapeMismatch - 1 (length stages)) - -data ExactDatatypeError - = ExactDatatypeUnsupportedBlock !Location - | ExactDatatypeOccurrenceCountMismatch !Location !Int !Int - | ExactDatatypeOccurrenceMismatch !Location - | ExactDatatypeGlossFailed !Location !Meaning.GlossError - | ExactDatatypeInvalid !Location !Text - | ExactDatatypeDuplicateGlobal !Location !SemanticGlobalKey - | ExactDatatypeFixedSemanticCollision !Location !SemanticGlobalKey - | ExactDatatypeGlobalAlreadyVisible !Location !SemanticGlobalKey - | ExactDatatypeObjectAlreadyAvailable !Location !ObjectId - | ExactDatatypeGlobalResolutionFailed - !Location - !ExactGlobal.ExactGlobalResolutionError - | ExactDatatypeLoweringFailed !Location !Typed.TypedInductiveError - | ExactDatatypeExpectedSet !Location !CoreType - | ExactDatatypeExpectedProposition !Location !CoreType - deriving stock (Show, Eq) - -exactDatatypeErrorLocation :: ExactDatatypeError -> Location -exactDatatypeErrorLocation = \case - ExactDatatypeUnsupportedBlock location -> location - ExactDatatypeOccurrenceCountMismatch location _expected _actual -> location - ExactDatatypeOccurrenceMismatch location -> location - ExactDatatypeGlossFailed location _failure -> location - ExactDatatypeInvalid location _message -> location - ExactDatatypeDuplicateGlobal location _key -> location - ExactDatatypeFixedSemanticCollision location _key -> location - ExactDatatypeGlobalAlreadyVisible location _key -> location - ExactDatatypeObjectAlreadyAvailable location _identity -> location - ExactDatatypeGlobalResolutionFailed location _failure -> location - ExactDatatypeLoweringFailed location _failure -> location - ExactDatatypeExpectedSet location _actual -> location - ExactDatatypeExpectedProposition location _actual -> location - -renderExactDatatypeError :: ExactDatatypeError -> Text -renderExactDatatypeError failure = - locationToText (exactDatatypeErrorLocation failure) - <> ": " - <> case failure of - ExactDatatypeUnsupportedBlock{} -> - "this datatype source form is not supported by the typed checker" - ExactDatatypeOccurrenceCountMismatch _location expected actual -> - "the datatype has " <> shown actual - <> " syntax occurrences, but " <> shown expected - <> " are required" - ExactDatatypeOccurrenceMismatch{} -> - "a datatype syntax occurrence does not match its declaration" - ExactDatatypeGlossFailed _location glossFailure -> - "datatype elaboration failed: " <> shown glossFailure - ExactDatatypeInvalid _location message -> - "invalid datatype declaration: " <> message - ExactDatatypeDuplicateGlobal _location key -> - "the datatype declares the semantic key more than once: " - <> shown key - ExactDatatypeFixedSemanticCollision _location key -> - "the datatype collides with fixed semantics for " <> shown key - ExactDatatypeGlobalAlreadyVisible _location key -> - "the datatype global is already visible: " <> shown key - ExactDatatypeObjectAlreadyAvailable _location identity -> - "the datatype opaque object is already available: " - <> shown identity - ExactDatatypeGlobalResolutionFailed _location resolution -> - "datatype global resolution failed: " <> shown resolution - ExactDatatypeLoweringFailed _location typedFailure -> - "typed datatype lowering failed: " <> shown typedFailure - ExactDatatypeExpectedSet _location actual -> - "a datatype premise domain has type " <> shown actual - <> " instead of Set" - ExactDatatypeExpectedProposition _location actual -> - "a generated datatype fact has type " <> shown actual - <> " instead of Prop" - where - shown :: Show value => value -> Text - shown = Text.pack . show - -type Prepare = - ExceptT ExactDatatypeError (Declaration.LoweringDriver) - -type SourceOccurrence = (Location, Raw.Marker, CanonicalLexicalEntry) - -exactDatatypeInvalid - :: Location - -> Datatype.DatatypeValidationError - -> ExactDatatypeError -exactDatatypeInvalid declarationLocation failure = - ExactDatatypeInvalid - (fromMaybe - declarationLocation - (Datatype.datatypeValidationErrorLocation failure)) - (Datatype.renderDatatypeValidationError failure) - -prepareExactDatatype - :: Raw.Block - -> [SourceOccurrence] - -> Declaration.LoweringDriver - (Either ExactDatatypeError PreparedExactDatatype) -prepareExactDatatype block occurrences = - Except.runExceptT do - (location, marker, rawDatatype) <- - case block of - Raw.BlockData blockLocation _title blockMarker datatype -> - pure (blockLocation, blockMarker, datatype) - _ -> - Except.throwError - (ExactDatatypeUnsupportedBlock (locate block)) - keys <- validateOccurrences location marker rawDatatype occurrences - internal <- - case Meaning.meaning [block] of - Right - [Internal.BlockData - _internalLocation _internalMarker datatype] -> - pure datatype - Left failure -> - Except.throwError - (ExactDatatypeGlossFailed location failure) - Right _ -> - Except.throwError - (ExactDatatypeUnsupportedBlock location) - checked <- - -- The new opaque carrier has no semantic binding while its - -- declaration is prepared, so premise recursion cannot depend on - -- abbreviation expansion. Revisit this if forward aliases become - -- available. - Except.lift - (Datatype.prepareCheckedDatatype pure internal) - >>= Except.liftEither - . first (exactDatatypeInvalid location) - let symbols = - Datatype.checkedDatatypeHeadSymbol checked - :| toList - (Datatype.checkedDatatypeConstructorSymbols checked) - views = Datatype.checkedDatatypeClauseViews checked - arities = - 0 :| (length - . Datatype.checkedDatatypeClauseViewArguments - <$> toList views) - unless (NonEmpty.length symbols == NonEmpty.length keys) - (Except.throwError - (ExactDatatypeOccurrenceCountMismatch - location - (NonEmpty.length symbols) - (NonEmpty.length keys))) - validateKeys occurrences keys - slot <- Except.lift Declaration.nextDeclarationSlotLowering - theory <- Except.lift Declaration.currentTheoryLowering - objects <- - sequence - (NonEmpty.zipWith - (\index (occurrenceLocation, symbol, key, arity) -> - prepareObject - occurrenceLocation - slot theory index symbol key arity) - (0 :| [1 ..]) - (NonEmpty.zipWith - (\occurrenceLocation (symbol, key, arity) -> - (occurrenceLocation, symbol, key, arity)) - (validatedOccurrenceLocations occurrences) - (NonEmpty.zipWith - (\(symbol, key) arity -> - (symbol, key, arity)) - (NonEmpty.zip symbols keys) - arities))) - let ownedSymbols = Set.fromList (toList symbols) - generated = Datatype.checkedDatatypeGeneratedFacts checked - externalSymbols = - (foldMap - (Internal.mentionedSymbols . snd) - generated - <> foldMap premiseSymbols views) - `Set.difference` ownedSymbols - external <- - Except.lift - (ExactGlobal.resolveExactSourceGlobals externalSymbols) - >>= Except.liftEither - . first (ExactDatatypeGlobalResolutionFailed location) - let (externalGlobals, externalTypes) = external - ownedGlobals = - Map.fromList - [ (symbol, Typed.SourceGlobal identity Nothing) - | PreparedDatatypeObject - symbol _key _coreType identity _asserted <- - toList objects - ] - ownedTypes = - Map.fromList - [ (identity, coreType) - | PreparedDatatypeObject - _symbol _key coreType identity _asserted <- - toList objects - ] - sourceGlobals = Map.union ownedGlobals externalGlobals - globalTypes = Map.union ownedTypes externalTypes - resolveGlobal = (`Map.lookup` sourceGlobals) - globalType identity = - fromMaybe - (impossible - "prepared datatype global has no checked type") - (Map.lookup identity globalTypes) - preparedClauses <- - Except.liftEither - (traverse - (prepareClause location globalType resolveGlobal) - views) - facts <- - Except.liftEither - (traverse - (prepareFact location theory globalType resolveGlobal) - generated) - let carrier = objectIdentity (NonEmpty.head objects) - constructors = objectIdentity <$> NonEmpty.tail objects - descriptor = - case NonEmpty.nonEmpty constructors of - Nothing -> - impossible - "a checked datatype has no constructors" - Just nonemptyConstructors -> - datatypeCompilationDescriptor - carrier - nonemptyConstructors - (preparedExactDatatypeFactReference - <$> toList facts) - syntax = - declarationSyntaxId - (encodePreparedDatatype - objects - preparedClauses - facts - descriptor) - pure - (PreparedExactDatatype - location - syntax - objects - facts - descriptor) - where - objectIdentity - (PreparedDatatypeObject _symbol _key _coreType identity _asserted) = - identity - -validateOccurrences - :: Location - -> Raw.Marker - -> Raw.Datatype - -> [SourceOccurrence] - -> Prepare (NonEmpty SemanticGlobalKey) -validateOccurrences location marker datatype occurrences = do - expected <- - Except.liftEither - (expectedOccurrences location marker datatype) - unless (length occurrences == NonEmpty.length expected) - (Except.throwError - (ExactDatatypeOccurrenceCountMismatch - location - (NonEmpty.length expected) - (length occurrences))) - keys <- - sequence - (NonEmpty.zipWith validateOne expected - (case NonEmpty.nonEmpty occurrences of - Just nonempty -> nonempty - Nothing -> - impossible - "equal nonzero occurrence counts became empty")) - pure keys - where - validateOne - (expectedLocation, expectedMarker, expectedPattern) - (actualLocation, actualMarker, entry) = - case entry of - CanonicalExpressionFunction pat marker' _fixity - | actualMarker == expectedMarker - , marker' == expectedMarker - , pat == expectedPattern -> - pure - (SemanticExpressionFunction pat) - _ -> - Except.throwError - (ExactDatatypeOccurrenceMismatch - (bestLocation actualLocation expectedLocation)) - - bestLocation actual expected - | actual == Nowhere = expected - | otherwise = actual - -expectedOccurrences - :: Location - -> Raw.Marker - -> Raw.Datatype - -> Either - ExactDatatypeError - (NonEmpty (Location, Raw.Marker, Raw.Pattern)) -expectedOccurrences location blockMarker datatype = do - headOccurrence <- - expectedSymbol blockMarker (Raw.datatypeHeadExpr datatype) - clauses <- - traverse - (\clause -> - case Raw.datatypeClauseConstructorExpr clause of - Raw.ExprOp constructorLocation symbol _arguments -> - Right - ( constructorLocation - , Raw.mixfixMarker symbol - , Raw.mixfixPattern symbol - ) - expression -> - Left - (ExactDatatypeOccurrenceMismatch - (locate expression))) - (Raw.datatypeClauses datatype) - pure (headOccurrence :| toList clauses) - where - expectedSymbol expectedMarker = \case - Raw.ExprOp symbolLocation symbol [] -> - Right - ( symbolLocation - , expectedMarker - , Raw.mixfixPattern symbol - ) - expression -> - Left - (ExactDatatypeOccurrenceMismatch - (case locate expression of - Nowhere -> location - expressionLocation -> expressionLocation)) - -validateKeys - :: [SourceOccurrence] - -> NonEmpty SemanticGlobalKey - -> Prepare () -validateKeys occurrences keys = do - case duplicateWithLocation of - Just (duplicate, duplicateLocation) -> - Except.throwError - (ExactDatatypeDuplicateGlobal - duplicateLocation - duplicate) - Nothing -> pure () - traverse_ validateOne (NonEmpty.zip locations keys) - where - locations = validatedOccurrenceLocations occurrences - - duplicateWithLocation = - go Set.empty - [ (key, occurrenceLocation) - | (key, (occurrenceLocation, _marker, _entry)) <- - zip (toList keys) occurrences - ] - - go _seen [] = Nothing - go seen ((key, occurrenceLocation) : remaining) - | key `Set.member` seen = Just (key, occurrenceLocation) - | otherwise = go (Set.insert key seen) remaining - - validateOne (occurrenceLocation, key) = do - when (isJust (fixedSemanticMeaning key)) - (Except.throwError - (ExactDatatypeFixedSemanticCollision occurrenceLocation key)) - visible <- - Except.lift - (Declaration.resolveVisibleGlobalLowering key) - when (isJust visible) - (Except.throwError - (ExactDatatypeGlobalAlreadyVisible occurrenceLocation key)) - -validatedOccurrenceLocations - :: [SourceOccurrence] - -> NonEmpty Location -validatedOccurrenceLocations occurrences = - case NonEmpty.nonEmpty - [ occurrenceLocation - | (occurrenceLocation, _marker, _entry) <- occurrences - ] of - Just nonempty -> nonempty - Nothing -> - impossible "validated datatype occurrences are empty" - -prepareObject - :: Location - -> DeclarationSlot - -> TheoryId - -> Natural - -> Internal.Symbol - -> SemanticGlobalKey - -> Int - -> Prepare PreparedDatatypeObject -prepareObject location slot theory index symbol key arity = do - let coreType = - foldr (const (TyArrow TySet)) TySet [1 .. arity] - seed = - opaqueDeclarationSeed - (declarationSlotModule slot) - (declarationSlotOrdinal slot) - DatatypeDeclaration - (generatedObjectSlot index) - content = OpaqueObjectContent theory seed coreType - identity = opaqueObjectId theory seed coreType - available <- Except.lift (Declaration.objectAvailableLowering identity) - when available - (Except.throwError - (ExactDatatypeObjectAlreadyAvailable location identity)) - pure - (PreparedDatatypeObject - symbol - key - coreType - identity - (assertedObject identity content)) - -data PreparedClause = PreparedClause - !Internal.FunctionSymbol - ![PreparedPremise] - -data PreparedPremise - = PreparedRecursivePremise !(FrozenCheckedCore ObjectId) - | PreparedNonRecursivePremise !(FrozenCheckedCore ObjectId) - -prepareClause - :: Location - -> (ObjectId -> CoreType) - -> (Internal.Symbol -> Maybe (Typed.SourceGlobal ObjectId)) - -> Datatype.CheckedDatatypeClauseView - -> Either ExactDatatypeError PreparedClause -prepareClause location globalType resolveGlobal view = - PreparedClause - (Datatype.checkedDatatypeClauseViewConstructor view) - <$> traverse preparePremise - (Datatype.checkedDatatypeClauseViewPremises view) - where - preparePremise = \case - Datatype.CheckedRecursiveDatatypePremise _variable domain -> - PreparedRecursivePremise - <$> prepareDomain domain - Datatype.CheckedNonRecursiveDatatypePremise _variable domain -> - PreparedNonRecursivePremise - <$> prepareDomain domain - - prepareDomain domain = do - checked <- - first (ExactDatatypeLoweringFailed location) - (Typed.prepareTypedClosedTerm - globalType - resolveGlobal - domain) - unless (frozenCoreType checked == TySet) - (Left - (ExactDatatypeExpectedSet - location - (frozenCoreType checked))) - pure checked - -prepareFact - :: Location - -> TheoryId - -> (ObjectId -> CoreType) - -> (Internal.Symbol -> Maybe (Typed.SourceGlobal ObjectId)) - -> (Internal.Marker, Internal.Formula) - -> Either ExactDatatypeError PreparedExactDatatypeFact -prepareFact location theory globalType resolveGlobal (marker, formula) = do - checked <- - first (ExactDatatypeLoweringFailed location) - (Typed.prepareTypedClosedFormula - globalType - resolveGlobal - formula) - unless (frozenCoreType checked == TyProp) - (Left - (ExactDatatypeExpectedProposition - location - (frozenCoreType checked))) - pure - (PreparedExactDatatypeFact - marker - checked - (theoremRef theory - (propositionIdOf (frozenCoreTerm checked)))) - -premiseSymbols - :: Datatype.CheckedDatatypeClauseView - -> Set.Set Internal.Symbol -premiseSymbols view = - foldMap symbols - (Datatype.checkedDatatypeClauseViewPremises view) - where - symbols = \case - Datatype.CheckedRecursiveDatatypePremise _variable domain -> - Internal.mentionedSymbols domain - Datatype.CheckedNonRecursiveDatatypePremise _variable domain -> - Internal.mentionedSymbols domain - -encodePreparedDatatype - :: NonEmpty PreparedDatatypeObject - -> NonEmpty PreparedClause - -> NonEmpty PreparedExactDatatypeFact - -> DatatypeCompilationDescriptor - -> ByteString -encodePreparedDatatype objects clauses facts descriptor = - encodeCache do - putCacheTag 0x05 - putCacheList putObject (toList objects) - putCacheList putClause (toList clauses) - putCacheList putFact (toList facts) - putDirectAuthorizationCache - (TrustedCompilation - (DatatypeCompilation descriptor)) - where - putObject - (PreparedDatatypeObject - _symbol key coreType identity _asserted) = do - putSemanticGlobalKeyCache key - putCoreTypeCache coreType - putObjectIdCache identity - - putClause (PreparedClause constructor premises) = do - putSemanticGlobalKeyCache - (SemanticExpressionFunction - (Raw.mixfixPattern constructor)) - putCacheList putPremise premises - - putPremise = \case - PreparedRecursivePremise domain -> do - putCacheTag 0x00 - putCanonicalTermCache putObjectIdCache - (frozenCoreTerm domain) - PreparedNonRecursivePremise domain -> do - putCacheTag 0x01 - putCanonicalTermCache putObjectIdCache - (frozenCoreTerm domain) - - putFact fact = do - let Internal.Marker marker = - preparedExactDatatypeFactMarker fact - putCacheText marker - putCanonicalTermCache putObjectIdCache - (frozenCoreTerm - (preparedExactDatatypeFactTarget fact)) - putTheoremRefCache - (preparedExactDatatypeFactReference fact) |