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