diff options
Diffstat (limited to 'source/Checking/Exact/Inductive.hs')
| -rw-r--r-- | source/Checking/Exact/Inductive.hs | 742 |
1 files changed, 742 insertions, 0 deletions
diff --git a/source/Checking/Exact/Inductive.hs b/source/Checking/Exact/Inductive.hs new file mode 100644 index 0000000..cbb29f0 --- /dev/null +++ b/source/Checking/Exact/Inductive.hs @@ -0,0 +1,742 @@ +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE NoImplicitPrelude #-} + +-- | Exact preparation and atomic publication of direct set inductives. +module Checking.Exact.Inductive + ( PreparedExactInductive + , preparedExactInductiveCarrierId + , preparedExactInductiveCarrierType + , preparedExactInductiveCarrierBody + , preparedExactInductiveGuardTargets + , preparedExactInductiveFacts + , prepareExactInductive + , commitPreparedExactInductive + , ExactInductiveError(..) + , exactInductiveErrorLocation + , renderExactInductiveError + ) where + +import Base hiding (Empty) +import Checking.Authority +import Checking.Core +import Checking.Declaration qualified as Declaration +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 Syntax.Lexicon + ( pattern ConsSymbol + , pattern PairSymbol + ) + +import Control.Monad (foldM, 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.Maybe (catMaybes) +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] + +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 + | ExactInductiveGlobalAlreadyVisible !Location !SemanticGlobalKey + | ExactInductiveGlobalNotVisible !Location !Internal.Symbol + | ExactInductiveGlobalAmbiguous !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 + ExactInductiveGlobalAlreadyVisible location _key -> location + ExactInductiveGlobalNotVisible location _symbol -> location + ExactInductiveGlobalAmbiguous 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" + 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 + 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 failure = + ExceptT + ExactInductiveError + (Declaration.ModuleDriver failure) + +prepareExactInductive + :: CheckedFoundation + -> Raw.Block + -> [CanonicalLexicalEntry] + -> Declaration.ModuleDriver failure + (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 + visible <- + Except.lift + (Declaration.resolveVisibleGlobalDriver 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.currentTheoryDriver + 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.objectAvailableDriver 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 failure 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 failure + ( Map.Map + Internal.Symbol + (Typed.SourceGlobal ObjectId) + , Map.Map ObjectId CoreType + ) +resolveSourceGlobals location internal direct = + foldM resolve (Map.empty, Map.empty) symbols + where + carrier = Internal.SymbolMixfix (Internal.inductiveSymbol internal) + symbols = + Set.toAscList + ( Set.delete carrier + (directSymbols direct) + `Set.difference` fixedInductiveSymbols + ) + + resolve (resolved, types) symbol = do + let keys = semanticKeys symbol + when (null keys) + (Except.throwError + (ExactInductiveGlobalNotVisible location symbol)) + matches <- + catMaybes + <$> traverse + (Except.lift + . Declaration.resolveVisibleGlobalContentDriver) + keys + case matches of + [] -> + Except.throwError + (ExactInductiveGlobalNotVisible location symbol) + [match] -> do + (source, sourceTypes) <- + Except.liftEither + (prepareSourceGlobal location match) + pure + ( Map.insert symbol source resolved + , Map.union sourceTypes types + ) + _ -> + Except.throwError + (ExactInductiveGlobalAmbiguous location symbol) + +prepareSourceGlobal + :: Location + -> ( SemanticGlobalTarget + , ObjectContent + , Map.Map ObjectId CoreType + ) + -> Either + ExactInductiveError + (Typed.SourceGlobal ObjectId, Map.Map ObjectId CoreType) +prepareSourceGlobal location (target, content, dependencies) = do + body <- + case target of + GlobalReference _identity -> + Right Nothing + TransparentExpansion _identity -> + case content of + TransparentObjectContent _theory _coreType canonical -> + Just + <$> first + (ExactInductiveGlobalContentInvalid location) + (checkCanonicalCore + (`Map.lookup` dependencies) + canonical) + _ -> + impossible + "validated transparent expansion has opaque content" + let identity = semanticGlobalTargetObject target + types = + Map.insert + identity + (objectContentType content) + dependencies + pure (Typed.SourceGlobal identity body, types) + +resolveGuard + :: Location + -> FrozenCheckedCore ObjectId + -> Prepare failure SemanticFactOccurrenceFingerprint +resolveGuard location target = do + matches <- + Except.lift + (Declaration.resolveVisibleFactTargetsDriver 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 + +fixedInductiveSymbols :: Set.Set Internal.Symbol +fixedInductiveSymbols = + Set.fromList + [ Internal.SymbolMixfix ConsSymbol + , Internal.SymbolMixfix PairSymbol + , Internal.SymbolMixfix (unarySymbol "pow") + , Internal.SymbolMixfix (unarySymbol "cumul") + , Internal.SymbolPredicate + (Internal.PredicateRelation Raw.ElementSymbol) + , Internal.SymbolPredicate + (Internal.PredicateRelation Raw.EqSymbol) + , Internal.SymbolPredicate + (Internal.PredicateRelation Raw.NeqSymbol) + , Internal.SymbolPredicate + (Internal.PredicateRelation Raw.SubseteqSymbol) + ] + where + unarySymbol command = + Raw.MixfixItem + (Raw.TokenCons (Raw.Command command) + (Raw.TokenCons Raw.InvisibleBraceL + (Raw.HoleCons + (Raw.TokenCons Raw.InvisibleBraceR Raw.End)))) + (Raw.Marker command) + Raw.NonAssoc + +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{} -> [] + +commitPreparedExactInductive + :: PreparedExactInductive + -> Declaration.ModuleDriver failure + ((), Declaration.CommittedDeclarationBatch) +commitPreparedExactInductive + (PreparedExactInductive + _location key identity asserted alias syntax typed guards) = + Declaration.commitCompiledDeclaration syntax do + traverse_ Declaration.addDeclarationObject asserted + Declaration.stageSemanticGlobalBinding + key + (GlobalReference identity) + let facts = Typed.typedInductiveFacts typed + candidateInputs = + fmap + (\fact -> + ( embedClosedCore [] + (Typed.typedInductiveFactTarget fact) + , SearchEligible + , [markerAlias + (Typed.typedInductiveFactMarker fact)] + )) + facts + (definitionCandidate, factCandidates) <- + Declaration.reserveDefinitionEquationCandidateBatch + identity + alias + candidateInputs + Declaration.authorizeCompiledDeclaration do + Declaration.authorizeDefinitionEquationCandidate + identity + definitionCandidate + sequence_ + (NonEmpty.zipWith + authorizeFact + factCandidates + facts) + where + authorizeFact candidate fact = + Declaration.authorizeKernelConstructionCandidate + (GuardedFoundationRule + (Typed.typedInductiveFactRule fact)) + candidate do + traverse_ Declaration.useAuthorizedFact guards + pure (Typed.typedInductiveFactDerivation fact) + + markerAlias (Raw.Marker name) = + semanticName name + +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)) + putCacheBytes + (encodeKernelRuleTag + (Typed.typedInductiveFactRule 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 = \case + Internal.TermVar variable -> locate variable + Internal.TermSymbol location _symbol _arguments -> location + Internal.TermSymbolStruct _symbol expression -> + maybe Nowhere termLocation expression + Internal.Apply function _arguments -> termLocation function + Internal.TermSep variable _bound _predicate -> locate variable + Internal.ReplacePred value _domain _bound _predicate -> locate value + Internal.ReplaceFun ((variable, _domain) :| _remaining) _value _condition -> + locate variable + Internal.Connected _connective left _right -> termLocation left + Internal.Lambda{} -> Nowhere + Internal.Quantified{} -> Nowhere + Internal.PropositionalConstant{} -> Nowhere + Internal.Not location _term -> location |