{-# 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)