diff options
Diffstat (limited to 'source/Checking/Exact.hs')
| -rw-r--r-- | source/Checking/Exact.hs | 1121 |
1 files changed, 1056 insertions, 65 deletions
diff --git a/source/Checking/Exact.hs b/source/Checking/Exact.hs index 6bb8bd6..6ee258e 100644 --- a/source/Checking/Exact.hs +++ b/source/Checking/Exact.hs @@ -17,9 +17,15 @@ module Checking.Exact , PreparedExactSetExpression , preparedExactSetExpressionCore , prepareExactSetExpression + , PreparedExactLocalFunctionGraph + , preparedExactLocalFunctionGraphCore + , preparedExactLocalFunctionGraphDomain + , preparedExactLocalFunctionGraphMap + , prepareExactLocalFunctionGraph , PreparedExactClaimEnvelope , preparedExactClaimTarget , preparedExactClaimVariables + , preparedExactClaimContext , preparedExactClaimAntecedentCount , prepareExactClaimEnvelope , PreparedExactDeclaration @@ -31,6 +37,9 @@ module Checking.Exact , preparedExactIsDefinition , prepareExactDeclaration , commitPreparedExactBinding + , PreparedExactStructure + , prepareExactStructure + , commitPreparedExactStructure , PreparedExactSourceAxiom , prepareExactSourceAxiom , commitPreparedExactSourceAxiom @@ -49,7 +58,7 @@ import Felix.Cache.Codec import Felix.Module import Report.Location import Syntax.Abstract qualified as Raw -import Syntax.Interface (CanonicalLexicalEntry) +import Syntax.Interface (CanonicalLexicalEntry(..)) import Syntax.Lexicon qualified as Lexicon import Control.Monad.Except (ExceptT) @@ -59,6 +68,7 @@ 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.Bifunctor (first) import Data.List.NonEmpty qualified as NonEmpty import Data.Map.Strict qualified as Map import Data.Maybe (catMaybes) @@ -83,6 +93,12 @@ data ExactBinder = ExactBinder !ExactLocalId !Raw.VarSymbol !CoreType + !(Maybe ExactStructureAnnotation) + +data ExactStructureAnnotation = ExactStructureAnnotation + !SemanticStructurePhrase + !(Maybe ObjectId) + !(Map.Map Raw.StructSymbol ObjectId) -- | The active nearest-first binders of one exact proof scope. newtype ExactBinderContext = ExactBinderContext [ExactBinder] @@ -103,12 +119,12 @@ extendExactBinderContext additions (ExactBinderContext initial) = | any (sameIdentity identity) binders = Left (ExactDuplicateLocalIdentity (locate variable) identity) | otherwise = - Right (ExactBinder identity variable TySet : binders) + Right (ExactBinder identity variable TySet Nothing : binders) - sameVariable variable (ExactBinder _identity existing _coreType) = + sameVariable variable (ExactBinder _identity existing _coreType _structure) = existing == variable - sameIdentity identity (ExactBinder existing _variable _coreType) = + sameIdentity identity (ExactBinder existing _variable _coreType _structure) = existing == identity exactBinderContextSupport @@ -117,7 +133,7 @@ exactBinderContextSupport exactBinderContextSupport (ExactBinderContext binders) = Vector.fromList [ (identity, coreType) - | ExactBinder identity _variable coreType <- binders + | ExactBinder identity _variable coreType _structure <- binders ] exactBinderContextIndex @@ -129,7 +145,7 @@ exactBinderContextIndex variable (ExactBinderContext binders) = where go _index [] = Nothing - go index (ExactBinder _identity candidate _coreType : rest) + go index (ExactBinder _identity candidate _coreType _structure : rest) | candidate == variable = Just index | otherwise = go (index + 1) rest @@ -151,33 +167,70 @@ preparedExactSetExpressionCore preparedExactSetExpressionCore (PreparedExactSetExpression expression) = expression +-- | A checked replacement graph and the two checked arguments used to +-- specialize its foundation characteristic. This is transient proof +-- preparation data, not a declaration or durable object. +data PreparedExactLocalFunctionGraph = PreparedExactLocalFunctionGraph + !(ScopedCheckedCore ObjectId) + !(ScopedCheckedCore ObjectId) + !(ScopedCheckedCore ObjectId) + +preparedExactLocalFunctionGraphCore + :: PreparedExactLocalFunctionGraph + -> ScopedCheckedCore ObjectId +preparedExactLocalFunctionGraphCore + (PreparedExactLocalFunctionGraph graph _domain _function) = + graph + +preparedExactLocalFunctionGraphDomain + :: PreparedExactLocalFunctionGraph + -> ScopedCheckedCore ObjectId +preparedExactLocalFunctionGraphDomain + (PreparedExactLocalFunctionGraph _graph domain _function) = + domain + +preparedExactLocalFunctionGraphMap + :: PreparedExactLocalFunctionGraph + -> ScopedCheckedCore ObjectId +preparedExactLocalFunctionGraphMap + (PreparedExactLocalFunctionGraph _graph _domain function) = + function + -- | One authoritative closed proposition prepared from a top-level claim -- header and conclusion. The remaining fields are transient opening data for -- the proof compiler. data PreparedExactClaimEnvelope = PreparedExactClaimEnvelope !(ScopedCheckedCore ObjectId) ![Raw.VarSymbol] + !ExactBinderContext !Natural preparedExactClaimTarget :: PreparedExactClaimEnvelope -> ScopedCheckedCore ObjectId preparedExactClaimTarget - (PreparedExactClaimEnvelope target _variables _antecedents) = + (PreparedExactClaimEnvelope target _variables _context _antecedents) = target preparedExactClaimVariables :: PreparedExactClaimEnvelope -> [Raw.VarSymbol] preparedExactClaimVariables - (PreparedExactClaimEnvelope _target variables _antecedents) = + (PreparedExactClaimEnvelope _target variables _context _antecedents) = variables +preparedExactClaimContext + :: PreparedExactClaimEnvelope + -> ExactBinderContext +preparedExactClaimContext + (PreparedExactClaimEnvelope _target _variables context _antecedents) = + context + preparedExactClaimAntecedentCount :: PreparedExactClaimEnvelope -> Natural preparedExactClaimAntecedentCount - (PreparedExactClaimEnvelope _target _variables antecedents) = + (PreparedExactClaimEnvelope _target _variables _context antecedents) = antecedents @@ -191,7 +244,7 @@ data PreparedExactDeclaration = PreparedExactDeclaration !Location !ExactDeclarationFamily !SemanticGlobalKey - !ObjectId + !SemanticGlobalTarget !(Maybe AssertedObject) !(Maybe SemanticName) !DeclarationSyntaxId @@ -209,7 +262,7 @@ preparedExactGlobalKey preparedExactObjectId :: PreparedExactDeclaration -> ObjectId preparedExactObjectId (PreparedExactDeclaration _location _family _key target _object _alias _syntax) = - target + semanticGlobalTargetObject target preparedExactObject :: PreparedExactDeclaration @@ -235,11 +288,8 @@ preparedExactGlobalTarget -> SemanticGlobalTarget preparedExactGlobalTarget (PreparedExactDeclaration - _location family _key target _object _alias _syntax) = - case family of - ExactSignature -> GlobalReference target - ExactAbbreviation -> TransparentExpansion target - ExactDefinition -> GlobalReference target + _location _family _key target _object _alias _syntax) = + target preparedDefinitionAlias :: PreparedExactDeclaration @@ -255,6 +305,20 @@ data PreparedExactSourceAxiom = PreparedExactSourceAxiom !(ScopedCheckedCore ObjectId) !DeclarationSyntaxId +data PreparedExactStructureFact = PreparedExactStructureFact + !Location + !(FrozenCheckedCore ObjectId) + !SemanticName + +data PreparedExactStructure = PreparedExactStructure + !Location + ![AssertedObject] + !ObjectId + !SemanticStructureDescriptor + !SemanticName + ![PreparedExactStructureFact] + !DeclarationSyntaxId + data ExactCompileError = ExactUnsupportedDeclaration !Location | ExactUnsupportedDeclarationBody !Location @@ -277,6 +341,28 @@ data ExactCompileError | ExactObjectTypeMismatch !Location !CoreType !CoreType | ExactUnsupportedHeaderAssumption !Location | ExactQuantifiedTermRequiresStatementSubject !Location + | ExactStructureNotVisible !Location !SemanticStructurePhrase + | ExactBaseStructureNotAssertable !Location !SemanticStructurePhrase + | ExactDuplicateStructureAnnotation !Location !Raw.VarSymbol + | ExactStructureOperationNotAvailable !Location !Raw.StructSymbol + | ExactStructureOperationAmbiguous + !Location !Raw.StructSymbol ![ObjectId] + | ExactContextualExpansionNotAvailable + !Location !SemanticGlobalKey + | ExactContextualRequirementConflict + !Location !Raw.StructSymbol !ObjectId !ObjectId + | ExactStructureOccurrenceMismatch !Location + | ExactStructureSelfParent !Location !SemanticStructurePhrase + | ExactStructureDuplicateParent !Location !SemanticStructurePhrase + | ExactStructureAlreadyVisible !Location !SemanticStructurePhrase + | ExactStructureDuplicateOperation !Location !Raw.StructSymbol + | ExactStructureOperationAlreadyInherited !Location !Raw.StructSymbol + | ExactStructureOperationConflict + !Location !Raw.StructSymbol + !SemanticStructurePhrase !SemanticStructurePhrase + | ExactStructureHasNoCarrier !Location !SemanticStructurePhrase + | ExactStructureDescriptorInvalid !Location !SemanticEnvironmentError + | ExactStructureObjectNotVisible !Location !ObjectId deriving stock (Show, Eq) exactCompileErrorLocation :: ExactCompileError -> Location @@ -301,6 +387,23 @@ exactCompileErrorLocation = \case ExactObjectTypeMismatch location _expected _actual -> location ExactUnsupportedHeaderAssumption location -> location ExactQuantifiedTermRequiresStatementSubject location -> location + ExactStructureNotVisible location _phrase -> location + ExactBaseStructureNotAssertable location _phrase -> location + ExactDuplicateStructureAnnotation location _variable -> location + ExactStructureOperationNotAvailable location _symbol -> location + ExactStructureOperationAmbiguous location _symbol _objects -> location + ExactContextualExpansionNotAvailable location _key -> location + ExactContextualRequirementConflict location _symbol _first _second -> location + ExactStructureOccurrenceMismatch location -> location + ExactStructureSelfParent location _phrase -> location + ExactStructureDuplicateParent location _phrase -> location + ExactStructureAlreadyVisible location _phrase -> location + ExactStructureDuplicateOperation location _symbol -> location + ExactStructureOperationAlreadyInherited location _symbol -> location + ExactStructureOperationConflict location _symbol _first _second -> location + ExactStructureHasNoCarrier location _phrase -> location + ExactStructureDescriptorInvalid location _failure -> location + ExactStructureObjectNotVisible location _object -> location renderExactCompileError :: ExactCompileError -> Text renderExactCompileError = \case @@ -348,6 +451,56 @@ renderExactCompileError = \case ExactQuantifiedTermRequiresStatementSubject location -> at location <> "a quantified term must be the sole subject of an exact statement" + ExactStructureNotVisible location structurePhrase -> + at location <> "the structure " <> shown structurePhrase <> " is not visible" + ExactBaseStructureNotAssertable location structurePhrase -> + at location <> "the metadata-only structure " <> shown structurePhrase + <> " cannot be asserted" + ExactDuplicateStructureAnnotation location variable -> + at location <> "the structure binder " <> shown variable + <> " is annotated more than once" + ExactStructureOperationNotAvailable location symbol -> + at location <> "the structure operation " <> shown symbol + <> " is not available in the active structure scope" + ExactStructureOperationAmbiguous location symbol objects -> + at location <> "the structure operation " <> shown symbol + <> " is ambiguous between " <> shown objects + ExactContextualExpansionNotAvailable location key -> + at location <> "the contextual abbreviation " <> shown key + <> " has no compatible active structure" + ExactContextualRequirementConflict location symbol firstObject secondObject -> + at location <> "the contextual abbreviation requires incompatible " + <> shown symbol <> " operations " <> shown firstObject + <> " and " <> shown secondObject + ExactStructureOccurrenceMismatch location -> + at location <> "the structure syntax occurrences do not match the declaration" + ExactStructureSelfParent location structurePhrase -> + at location <> "the structure " <> shown structurePhrase + <> " cannot inherit from itself" + ExactStructureDuplicateParent location structurePhrase -> + at location <> "the parent structure " <> shown structurePhrase + <> " is repeated" + ExactStructureAlreadyVisible location structurePhrase -> + at location <> "the structure " <> shown structurePhrase + <> " is already declared" + ExactStructureDuplicateOperation location symbol -> + at location <> "the structure operation " <> shown symbol + <> " is repeated" + ExactStructureOperationAlreadyInherited location symbol -> + at location <> "the structure operation " <> shown symbol + <> " is already inherited" + ExactStructureOperationConflict location symbol firstOrigin secondOrigin -> + at location <> "the inherited structure operation " <> shown symbol + <> " conflicts between " <> shown firstOrigin + <> " and " <> shown secondOrigin + ExactStructureHasNoCarrier location structurePhrase -> + at location <> "the structure " <> shown structurePhrase + <> " does not inherit the base carrier operation" + ExactStructureDescriptorInvalid location _failure -> + at location <> "the canonical structure descriptor is inconsistent" + ExactStructureObjectNotVisible location identity -> + at location <> "the structure fact mentions unavailable object " + <> shown identity where at location = locationToText location <> ": " shown :: Show value => value -> Text @@ -355,7 +508,11 @@ renderExactCompileError = \case data ElaborationState = ElaborationState { elaborationBinders :: !(Map.Map Raw.VarSymbol Natural) + , elaborationStructures :: !(Map.Map Natural ExactStructureAnnotation) , elaborationGlobals :: !(Map.Map ObjectId CoreType) + , elaborationContextualBinder :: !(Maybe Natural) + , elaborationContextualRequirements + :: !(Map.Map Raw.StructSymbol ObjectId) } type Elaborate failure = @@ -371,6 +528,9 @@ data PreparedHead = PreparedHead data PreparedBody = OpaqueBody | TransparentBody !(CanonicalTerm ObjectId) + | ContextualTransparentBody + !(Map.Map Raw.StructSymbol ObjectId) + !(CanonicalTerm ObjectId) prepareExactProposition :: ExactBinderContext @@ -379,10 +539,7 @@ prepareExactProposition (Either ExactCompileError PreparedExactProposition) prepareExactProposition context statement = Except.runExceptT do - let initialElaboration = - ElaborationState - (binderIndices context) - mempty + let initialElaboration = initialElaborationState context (term, finalElaboration) <- State.runStateT (compileStatement statement) @@ -410,10 +567,7 @@ prepareExactSetExpression (Either ExactCompileError PreparedExactSetExpression) prepareExactSetExpression context expression = Except.runExceptT do - let initialElaboration = - ElaborationState - (binderIndices context) - mempty + let initialElaboration = initialElaborationState context (term, finalElaboration) <- State.runStateT (compileExpressionAsSet expression) @@ -434,6 +588,61 @@ prepareExactSetExpression context expression = (scopedCoreType checked))) pure (PreparedExactSetExpression checked) +prepareExactLocalFunctionGraph + :: Location + -> ExactBinderContext + -> ExactBinderContext + -> Raw.Expr + -> Raw.Expr + -> Declaration.ModuleDriver failure + (Either ExactCompileError PreparedExactLocalFunctionGraph) +prepareExactLocalFunctionGraph + location context argumentContext domainExpression valueExpression = + Except.runExceptT do + domain <- + preparedExactSetExpressionCore + <$> ( Except.lift + (prepareExactSetExpression context domainExpression) + >>= Except.liftEither + ) + value <- + preparedExactSetExpressionCore + <$> ( Except.lift + (prepareExactSetExpression + argumentContext valueExpression) + >>= Except.liftEither + ) + pair <- prepareOrderedPair + case scopedReplacementGraph pair domain value of + Just (graph, checkedDomain, function) -> + pure + (PreparedExactLocalFunctionGraph + graph checkedDomain function) + Nothing -> + impossible + "checked local-function components did not form a replacement graph" + where + prepareOrderedPair = do + let initialElaboration = initialElaborationState context + key = + SemanticExpressionFunction + (Raw.mixfixPattern Raw.PairSymbol) + expected = TySet `TyArrow` (TySet `TyArrow` TySet) + ((term, actual), finalElaboration) <- + State.runStateT + (applyResolvedTyped location key []) + initialElaboration + unless (actual == expected) + (Except.throwError + (ExactObjectTypeMismatch location expected actual)) + either + (Except.throwError . ExactCoreCheckFailed location) + pure + (checkScopedCanonicalCore + (`Map.lookup` elaborationGlobals finalElaboration) + (binderTypes context) + term) + prepareExactClaimEnvelope :: [Raw.Asm] -> Raw.Stmt @@ -463,12 +672,13 @@ prepareExactClaimEnvelope assumptions statement = discover (variables <> [variable]) extended Left failure -> pure (Left failure) - Right (target, antecedentCount) -> + Right (target, antecedentCount, structures) -> pure (Right (PreparedExactClaimEnvelope target variables + (annotateBinderContext structures context) antecedentCount)) prepareExactClaimAttempt @@ -478,13 +688,13 @@ prepareExactClaimAttempt -> Declaration.ModuleDriver failure (Either ExactCompileError - (ScopedCheckedCore ObjectId, Natural)) + ( ScopedCheckedCore ObjectId + , Natural + , Map.Map Natural ExactStructureAnnotation + )) prepareExactClaimAttempt context assumptions statement = Except.runExceptT do - let initialElaboration = - ElaborationState - (binderIndices context) - mempty + let initialElaboration = initialElaborationState context ((antecedents, conclusion), finalElaboration) <- State.runStateT ( do @@ -519,7 +729,11 @@ prepareExactClaimAttempt context assumptions statement = closed = closeClaimBinders implication unless (null (scopedCoreContext closed)) (impossible "exact claim closure retained a binder") - pure (closed, fromIntegral (length antecedents)) + pure + ( closed + , fromIntegral (length antecedents) + , elaborationStructures finalElaboration + ) checkEnvelopeProposition :: ElaborationState @@ -563,16 +777,47 @@ binderIndices :: ExactBinderContext -> Map.Map Raw.VarSymbol Natural binderIndices (ExactBinderContext binders) = Map.fromList [ (variable, fromIntegral index) - | (index, ExactBinder _identity variable _coreType) <- + | (index, ExactBinder _identity variable _coreType _structure) <- + zip [0 :: Int ..] binders + ] + +binderStructures + :: ExactBinderContext + -> Map.Map Natural ExactStructureAnnotation +binderStructures (ExactBinderContext binders) = + Map.fromList + [ (fromIntegral index, structure) + | (index, ExactBinder _identity _variable _coreType (Just structure)) <- zip [0 :: Int ..] binders ] binderTypes :: ExactBinderContext -> [CoreType] binderTypes (ExactBinderContext binders) = [ coreType - | ExactBinder _identity _variable coreType <- binders + | ExactBinder _identity _variable coreType _structure <- binders ] +initialElaborationState :: ExactBinderContext -> ElaborationState +initialElaborationState context = + ElaborationState + (binderIndices context) + (binderStructures context) + mempty + Nothing + mempty + +annotateBinderContext + :: Map.Map Natural ExactStructureAnnotation + -> ExactBinderContext + -> ExactBinderContext +annotateBinderContext structures (ExactBinderContext binders) = + ExactBinderContext + [ ExactBinder identity variable coreType + (Map.lookup (fromIntegral index) structures) + | (index, ExactBinder identity variable coreType _old) <- + zip [0 :: Int ..] binders + ] + compileHeaderAssumption :: Raw.Asm -> Elaborate failure [(Location, CanonicalTerm ObjectId)] @@ -595,7 +840,9 @@ compileHeaderAssumption = \case ] Raw.AsmLetIn variables domain -> do variableTerms <- traverse compileIntroducedVariable variables - domainTerm <- compileExpressionAsSet domain + domainTerm <- + compileExpressionAsSet domain + >>= structureCarrierCast (locate domain) pure [ ( locate variable , CApp @@ -616,9 +863,44 @@ compileHeaderAssumption = \case Raw.AsmLetThe variable _function -> Except.throwError (ExactUnsupportedHeaderAssumption (locate variable)) - Raw.AsmLetStruct variable _structure -> - Except.throwError - (ExactUnsupportedHeaderAssumption (locate variable)) + Raw.AsmLetStruct variable structure -> do + subject <- compileIntroducedVariable variable + annotation <- + resolveStructureAnnotation + (locate variable) + structure + index <- + maybe + (impossible "an introduced structure variable is unbound") + pure + =<< Map.lookup variable <$> State.gets elaborationBinders + existing <- State.gets (Map.lookup index . elaborationStructures) + when + (isJust existing) + (Except.throwError + (ExactDuplicateStructureAnnotation + (locate variable) variable)) + State.modify' \state -> + state + { elaborationStructures = + Map.insert index annotation + (elaborationStructures state) + } + predicate <- + maybe + (impossible "an assertable structure has no predicate") + pure + (structureAnnotationPredicate annotation) + recordExactGlobal + predicate + (TyArrow TySet TyProp) + pure + [ ( locate variable + , CApp + (CGlobal predicate) + subject + ) + ] compileIntroducedVariable :: Raw.VarSymbol @@ -626,6 +908,63 @@ compileIntroducedVariable compileIntroducedVariable variable = compileExpressionAsSet (Raw.ExprVar variable) +resolveStructureAnnotation + :: Location + -> Raw.StructPhrase + -> Elaborate failure ExactStructureAnnotation +resolveStructureAnnotation location rawPhrase = do + let structurePhrase = semanticStructurePhrase rawPhrase + resolved <- + State.lift + (Except.lift + (Declaration.resolveVisibleStructureDriver structurePhrase)) + structure <- + maybe + (Except.throwError + (ExactStructureNotVisible location structurePhrase)) + pure + resolved + predicate <- + maybe + (Except.throwError + (ExactBaseStructureNotAssertable location structurePhrase)) + pure + (Declaration.resolvedStructurePredicate structure) + pure + (ExactStructureAnnotation + structurePhrase + (Just predicate) + (Declaration.resolvedStructureOperations structure)) + +structureAnnotationPredicate :: ExactStructureAnnotation -> Maybe ObjectId +structureAnnotationPredicate + (ExactStructureAnnotation _ predicate _operations) = + predicate + +structureAnnotationOperation + :: Raw.StructSymbol + -> ExactStructureAnnotation + -> Maybe ObjectId +structureAnnotationOperation symbol + (ExactStructureAnnotation _phrase _predicate operations) = + Map.lookup symbol operations + +recordExactGlobal :: ObjectId -> CoreType -> Elaborate failure () +recordExactGlobal identity coreType = do + existing <- State.gets (Map.lookup identity . elaborationGlobals) + case existing of + Nothing -> + State.modify' \state -> + state + { elaborationGlobals = + Map.insert identity coreType + (elaborationGlobals state) + } + Just actual + | actual == coreType -> pure () + | otherwise -> + impossible "one exact global acquired two checked types" + prepareExactSourceAxiom :: Raw.Block -> Declaration.ModuleDriver failure @@ -704,13 +1043,24 @@ prepareExactDeclaration block entries = case rawBody of Nothing -> pure (OpaqueBody, Map.empty) Just buildBody -> do - let initialElaboration = ElaborationState mempty mempty + let initialElaboration = + ElaborationState + mempty mempty mempty Nothing mempty (canonical, finalElaboration) <- State.runStateT buildBody initialElaboration - pure - ( TransparentBody canonical - , elaborationGlobals finalElaboration - ) + let requirements = + elaborationContextualRequirements finalElaboration + body + | Map.null requirements = + TransparentBody canonical + | family == ExactAbbreviation = + ContextualTransparentBody + requirements + (CLam TySet canonical) + | otherwise = + impossible + "a non-abbreviation acquired contextual requirements" + pure (body, elaborationGlobals finalElaboration) let PreparedHead semanticKey _parameters coreType = head' unless (semanticKey == key) (Except.throwError @@ -726,8 +1076,8 @@ prepareExactDeclaration block entries = (generatedObjectSlot 0) content' = OpaqueObjectContent theory seed coreType - pure - (opaqueObjectId theory seed coreType, content') + identity = opaqueObjectId theory seed coreType + pure (GlobalReference identity, content') TransparentBody canonical -> do checked <- either @@ -749,15 +1099,54 @@ prepareExactDeclaration block entries = theory coreType canonical + let identity = + transparentObjectId theory coreType canonical + semanticTarget = + case family of + ExactAbbreviation -> + TransparentExpansion identity + ExactDefinition -> GlobalReference identity + ExactSignature -> + impossible + "a signature acquired a transparent body" + pure (semanticTarget, content') + ContextualTransparentBody requirements canonical -> do + let contextualType = TyArrow TySet coreType + checked <- + either + (Except.throwError + . ExactCoreCheckFailed (locate block)) + pure + (checkCanonicalCore + (`Map.lookup` globals) + canonical) + unless + (frozenCoreType checked == contextualType) + (Except.throwError + (ExactObjectTypeMismatch + (locate block) + contextualType + (frozenCoreType checked))) + let content' = + TransparentObjectContent + theory + contextualType + canonical + identity = + transparentObjectId + theory contextualType canonical pure - ( transparentObjectId theory coreType canonical + ( ContextualTransparentExpansion + identity requirements , content' ) - available <- Except.lift (Declaration.objectAvailableDriver target) + let targetObject = semanticGlobalTargetObject target + available <- + Except.lift (Declaration.objectAvailableDriver targetObject) let alias = definitionAlias block asserted | available = Nothing - | otherwise = Just (assertedObject target content) + | otherwise = Just (assertedObject targetObject content) syntax = declarationSyntaxId (encodePreparedSyntax family head' body alias) @@ -801,6 +1190,367 @@ commitPreparedExactBinding prepared (preparedExactObjectId prepared)) candidate) +prepareExactStructure + :: Raw.Block + -> [CanonicalLexicalEntry] + -> Declaration.ModuleDriver failure + (Either ExactCompileError PreparedExactStructure) +prepareExactStructure block entries = + Except.runExceptT do + (location, marker, structure) <- + case block of + Raw.BlockStruct location _title (Raw.Marker marker) structure -> + pure (location, marker, structure) + _ -> Except.throwError + (ExactUnsupportedDeclaration (locate block)) + validateStructureOccurrences location structure entries + let structurePhrase = + semanticStructurePhrase (Raw.structPhrase structure) + parentPhrases = + semanticStructurePhrase <$> Raw.structParents structure + when + (structurePhrase `elem` parentPhrases) + (Except.throwError + (ExactStructureSelfParent location structurePhrase)) + case firstDuplicate parentPhrases of + Just duplicate -> + Except.throwError + (ExactStructureDuplicateParent location duplicate) + Nothing -> pure () + visible <- Except.lift + (Declaration.resolveVisibleStructureDriver structurePhrase) + when + (isJust visible) + (Except.throwError + (ExactStructureAlreadyVisible location structurePhrase)) + parents <- traverse (resolveParent location) parentPhrases + inherited <- + foldM mergeParentOperations Map.empty + (zip parentPhrases parents) + case firstDuplicate (Raw.structFixes structure) of + Just duplicate -> + Except.throwError + (ExactStructureDuplicateOperation location duplicate) + Nothing -> pure () + traverse_ + (\symbol -> + when + (Map.member symbol inherited) + (Except.throwError + (ExactStructureOperationAlreadyInherited + location symbol))) + (Raw.structFixes structure) + slot <- Except.lift Declaration.nextDeclarationSlotDriver + theory <- Except.lift Declaration.currentTheoryDriver + let operationType = TyArrow TySet TySet + makeOperation index symbol = + let seed = + opaqueDeclarationSeed + (declarationSlotModule slot) + (declarationSlotOrdinal slot) + StructureDeclaration + (generatedObjectSlot index) + content = OpaqueObjectContent theory seed operationType + identity = opaqueObjectId theory seed operationType + in ( symbol + , identity + , assertedObject identity content + ) + ownOperations = + zipWith makeOperation [0 ..] (Raw.structFixes structure) + operationObjects = + [ asserted + | (_symbol, _identity, asserted) <- ownOperations + ] + completeOperations = + Map.union + (Map.fromList + [ (symbol, identity) + | (symbol, identity, _asserted) <- ownOperations + ]) + (fst <$> inherited) + unless + (Map.member Raw.CarrierSymbol completeOperations) + (Except.throwError + (ExactStructureHasNoCarrier location structurePhrase)) + context <- + either Except.throwError pure + (extendExactBinderContext + ((exactLocalId 0, Raw.structLabel structure) :| []) + emptyExactBinderContext) + let provisionalAnnotation = + ExactStructureAnnotation + structurePhrase Nothing completeOperations + structureContext = + annotateBinderContext + (Map.singleton 0 provisionalAnnotation) + context + checkedAssumptions <- + traverse + (\(assumptionMarker, assumption) -> do + prepared <- Except.lift + (prepareExactProposition structureContext assumption) + proposition <- Except.liftEither prepared + pure + ( locate assumption + , assumptionMarker + , preparedExactPropositionCore proposition + )) + (Raw.structAssumes structure) + parentTerms <- + fmap catMaybes + (traverse + (\parent -> + case Declaration.resolvedStructurePredicate parent of + Nothing -> pure Nothing + Just predicate -> + pure + (Just + (CApp + (CGlobal predicate) + (CBound 0)))) + parents) + let assumptionTerms = + [ scopedCoreTerm proposition + | (_assumptionLocation, _assumptionMarker, proposition) <- + checkedAssumptions + ] + predicateBody = + CLam TySet + (logicalConjunction + (parentTerms <> assumptionTerms)) + predicateType = TyArrow TySet TyProp + predicateContent = + TransparentObjectContent theory predicateType predicateBody + predicate = + transparentObjectId theory predicateType predicateBody + predicateAvailable <- + Except.lift (Declaration.objectAvailableDriver predicate) + let predicateObject = + [ assertedObject predicate predicateContent + | not predicateAvailable + ] + ownBindings = + [ semanticStructureOperation symbol identity + | (symbol, identity, _asserted) <- ownOperations + ] + descriptor <- + Except.liftEither + (first + (ExactStructureDescriptorInvalid location) + (semanticStructureDescriptor + structurePhrase + (Just predicate) + parentPhrases + ownBindings)) + let structureApplication = + CApp (CGlobal predicate) (CBound 0) + inheritance = + [ ( location + , semanticName (marker <> "inherit") + , CForall TySet + (CImp structureApplication + (logicalConjunction parentTerms)) + ) + | not (null parentTerms) + ] + projections = + [ ( assumptionLocation + , semanticName assumptionMarker + , CForall TySet + (CImp structureApplication + (scopedCoreTerm proposition)) + ) + | ( assumptionLocation + , Raw.Marker assumptionMarker + , proposition + ) <- checkedAssumptions + ] + generatedTerms = inheritance <> projections + localTypes = + Map.fromList + ((predicate, predicateType) + : [ (identity, operationType) + | (_symbol, identity, _asserted) <- ownOperations + ]) + resolvedTypes <- + resolveStructureGlobalTypes + localTypes + [ term + | (_factLocation, _alias, term) <- generatedTerms + ] + generated <- + traverse + (\(factLocation, alias, term) -> do + frozen <- + either + (Except.throwError + . ExactCoreCheckFailed factLocation) + pure + (checkCanonicalCore + (`Map.lookup` resolvedTypes) + term) + pure + (PreparedExactStructureFact + factLocation frozen alias)) + generatedTerms + environment <- + Except.liftEither + (first + (ExactStructureDescriptorInvalid location) + (semanticEnvironmentWithStructures [] [descriptor])) + let syntax = + declarationSyntaxId + (encodePreparedStructure + environment + predicate + generated) + pure + (PreparedExactStructure + location + (operationObjects <> predicateObject) + predicate + descriptor + (semanticName marker) + generated + syntax) + where + resolveParent location structurePhrase = do + resolved <- Except.lift + (Declaration.resolveVisibleStructureDriver structurePhrase) + maybe + (Except.throwError + (ExactStructureNotVisible location structurePhrase)) + pure + resolved + + mergeParentOperations inherited (parentPhrase, parent) = + foldM + (insertParentOperation parentPhrase) + inherited + (Map.toAscList + (Declaration.resolvedStructureOperations parent)) + + insertParentOperation parentPhrase inherited (symbol, identity) = + case Map.lookup symbol inherited of + Nothing -> + pure + (Map.insert symbol (identity, parentPhrase) inherited) + Just (existing, existingOrigin) + | existing == identity -> pure inherited + | otherwise -> + Except.throwError + (ExactStructureOperationConflict + (locate block) + symbol + existingOrigin + parentPhrase) + + resolveStructureGlobalTypes localTypes terms = do + let dependencies = Set.unions (canonicalTermGlobals <$> terms) + foldM + (\types identity -> + case Map.lookup identity types of + Just{} -> pure types + Nothing -> do + coreType <- Except.lift + (Declaration.objectTypeDriver identity) + case coreType of + Nothing -> + Except.throwError + (ExactStructureObjectNotVisible + (locate block) identity) + Just actual -> + pure (Map.insert identity actual types)) + localTypes + (Set.toAscList dependencies) + +commitPreparedExactStructure + :: PreparedExactStructure + -> Declaration.ModuleDriver failure + ((), Declaration.CommittedDeclarationBatch) +commitPreparedExactStructure + (PreparedExactStructure + _location objects predicate descriptor alias generated syntax) = + Declaration.commitCompiledDeclaration syntax do + traverse_ Declaration.addDeclarationObject objects + Declaration.stageSemanticStructureDescriptor descriptor + definition <- + Declaration.reservePointwiseDefinitionEquationCandidate + predicate alias + generatedCandidates <- + case NonEmpty.nonEmpty generated of + Nothing -> pure [] + Just nonempty -> do + candidates <- + Declaration.reserveFrozenPropositionCandidateBatch + ( fmap + (\(PreparedExactStructureFact + _factLocation target factAlias) -> + (target, SearchEligible, [factAlias])) + nonempty + ) + pure (toList candidates) + Declaration.authorizeCompiledDeclaration do + Declaration.authorizeDefinitionEquationCandidate + predicate definition + case NonEmpty.nonEmpty + (zip generatedCandidates generated) of + Nothing -> pure () + Just ready -> + Declaration.authorizeVampireCandidateBatch + ( fmap + (\(candidate, PreparedExactStructureFact + factLocation _target _factAlias) -> + ( factLocation + , candidate + , do + void + (Declaration.useStagedCandidate + definition) + Declaration.prepareCurrentCandidateVampire + )) + ready + ) + +validateStructureOccurrences + :: Location + -> Raw.StructDefn + -> [CanonicalLexicalEntry] + -> ExceptT ExactCompileError (Declaration.ModuleDriver failure) () +validateStructureOccurrences location structure entries = do + let Raw.LexicalItemSgPl forms structureMarker = + Raw.structPhrase structure + expected = + CanonicalStructureNoun + (Raw.sg forms) + (Raw.pl forms) + structureMarker + : [ CanonicalStructureOperation command + | Raw.StructSymbol command <- Raw.structFixes structure + ] + unless + (entries == expected) + (Except.throwError + (ExactStructureOccurrenceMismatch location)) + +encodePreparedStructure + :: SemanticEnvironmentDelta + -> ObjectId + -> [PreparedExactStructureFact] + -> ByteString +encodePreparedStructure environment predicate generated = + encodeCache do + putCacheTag 0x04 + putSemanticEnvironmentDeltaCache environment + putObjectIdCache predicate + putCacheList + (\(PreparedExactStructureFact _location target alias) -> do + putCanonicalTermCache putObjectIdCache + (frozenCoreTerm target) + putCacheText (semanticNameText alias)) + generated + prepareHead :: Raw.Block -> SemanticGlobalKey @@ -870,32 +1620,32 @@ prepareAbbreviation prepareAbbreviation location key = \case Raw.AbbreviationEq (Raw.SymbolPattern symbol parameters) expression -> do ensureExpressionKey location symbol key - makeTransparentHead + makeContextualTransparentHead location key parameters TySet (compileExpressionAsSet expression) Raw.AbbreviationFun (Raw.Fun _ item parameters) term -> do ensureFunctionPhraseKey location item key - makeTransparentHead + makeContextualTransparentHead location key parameters TySet (compileTermAsSet term) Raw.AbbreviationAdj subject (Raw.Adj _ item arguments) statement -> do ensureAdjectiveKey location item key - makeTransparentHead + makeContextualTransparentHead location key (subject : arguments) TyProp (compileStatement statement) Raw.AbbreviationVerb subject (Raw.Verb _ item arguments) statement -> do ensureVerbKey location item key - makeTransparentHead + makeContextualTransparentHead location key (subject : arguments) TyProp (compileStatement statement) Raw.AbbreviationNoun subject (Raw.Noun _ item arguments) statement -> do ensureNounKey location item key - makeTransparentHead + makeContextualTransparentHead location key (subject : arguments) TyProp (compileStatement statement) Raw.AbbreviationRel left relation parameters right statement -> do ensureRelationKey location relation key - makeTransparentHead + makeContextualTransparentHead location key (parameters <> [left, right]) TyProp (compileStatement statement) @@ -994,6 +1744,32 @@ makeTransparentHead location key parameters resultType body = do pure (foldr (const (CLam TySet)) body' parameters) pure (prepared, close) +makeContextualTransparentHead + :: Location + -> SemanticGlobalKey + -> [Raw.VarSymbol] + -> CoreType + -> Elaborate failure (CanonicalTerm ObjectId) + -> ExceptT + ExactCompileError + (Declaration.ModuleDriver failure) + ( PreparedHead + , Elaborate failure (CanonicalTerm ObjectId) + ) +makeContextualTransparentHead location key parameters resultType body = do + (prepared, binders) <- + prepareParameters location key parameters resultType + let close = do + State.modify' \state -> + state + { elaborationBinders = binders + , elaborationContextualBinder = + Just (fromIntegral (length parameters)) + } + body' <- body + pure (foldr (const (CLam TySet)) body' parameters) + pure (prepared, close) + makePreparedHead :: Location -> SemanticGlobalKey @@ -1105,6 +1881,8 @@ compileExpression = \case location key compiled + Raw.ExprStructOp location symbol maybeArgument -> + compileStructureOperation location symbol maybeArgument Raw.ExprFiniteSet _location elements -> do compiled <- traverse compileExpressionAsSet elements pure @@ -1131,9 +1909,129 @@ compileExpression = \case Raw.ExprReplacePred location _value _variable _bound _predicate -> Except.throwError (ExactUnsupportedDeclarationBody location) - expression -> - Except.throwError - (ExactUnsupportedDeclarationBody (locate expression)) + +compileStructureOperation + :: Location + -> Raw.StructSymbol + -> Maybe Raw.Expr + -> Elaborate failure (CanonicalTerm ObjectId, CoreType) +compileStructureOperation location symbol maybeArgument = do + (argument, object) <- + case maybeArgument of + Just expression -> do + term <- compileExpressionAsSet expression + structures <- State.gets elaborationStructures + case termStructureAnnotation term structures of + Just annotation -> do + object <- + maybe + (Except.throwError + (ExactStructureOperationNotAvailable + location symbol)) + pure + (structureAnnotationOperation + symbol annotation) + pure (term, object) + Nothing -> do + object <- + resolveUniqueStructureOperation location symbol + pure (term, object) + Nothing -> do + structures <- State.gets elaborationStructures + case + [ (CBound index, object) + | (index, structure) <- Map.toAscList structures + , Just object <- + [structureAnnotationOperation symbol structure] + ] of + firstMatch : _ -> pure firstMatch + [] -> do + contextual <- State.gets elaborationContextualBinder + case contextual of + Nothing -> + Except.throwError + (ExactStructureOperationNotAvailable + location symbol) + Just index -> do + object <- + resolveUniqueStructureOperation + location symbol + recordContextualRequirement + location symbol object + pure (CBound index, object) + recordExactGlobal object (TyArrow TySet TySet) + pure (CApp (CGlobal object) argument, TySet) + where + termStructureAnnotation term structures = + case term of + CBound index -> Map.lookup index structures + _ -> Nothing + +resolveUniqueStructureOperation + :: Location + -> Raw.StructSymbol + -> Elaborate failure ObjectId +resolveUniqueStructureOperation location symbol = do + objects <- + State.lift + (Except.lift + (Declaration.resolveVisibleStructureOperationObjectsDriver + symbol)) + case objects of + [] -> + Except.throwError + (ExactStructureOperationNotAvailable location symbol) + [object] -> pure object + _ -> + Except.throwError + (ExactStructureOperationAmbiguous location symbol objects) + +recordContextualRequirement + :: Location + -> Raw.StructSymbol + -> ObjectId + -> Elaborate failure () +recordContextualRequirement location symbol object = do + existing <- + State.gets + (Map.lookup symbol . elaborationContextualRequirements) + case existing of + Nothing -> + State.modify' \state -> + state + { elaborationContextualRequirements = + Map.insert symbol object + (elaborationContextualRequirements state) + } + Just actual + | actual == object -> pure () + | otherwise -> + Except.throwError + (ExactContextualRequirementConflict + location symbol actual object) + +structureCarrierCast + :: Location + -> CanonicalTerm ObjectId + -> Elaborate failure (CanonicalTerm ObjectId) +structureCarrierCast location term = + case term of + CBound index -> do + annotation <- State.gets (Map.lookup index . elaborationStructures) + case annotation of + Nothing -> pure term + Just structure -> do + carrier <- + maybe + (Except.throwError + (ExactStructureOperationNotAvailable + location Raw.CarrierSymbol)) + pure + (structureAnnotationOperation + Raw.CarrierSymbol structure) + recordExactGlobal carrier (TyArrow TySet TySet) + pure (CApp (CGlobal carrier) term) + _ -> pure term compileReplacement :: Raw.Expr @@ -1215,9 +2113,22 @@ compileStatement = \case _location quantifier variables bound suchThat statement -> compileSymbolicQuantified quantifier variables bound suchThat (compileStatement statement) - statement -> - Except.throwError - (ExactUnsupportedDeclarationBody (locate statement)) + Raw.StmtStruct term rawPhrase -> do + subject <- compileTermAsSet term + annotation <- + resolveStructureAnnotation (locate term) rawPhrase + predicate <- + maybe + (impossible "an assertable structure has no predicate") + pure + (structureAnnotationPredicate annotation) + recordExactGlobal + predicate + (TyArrow TySet TyProp) + pure + (CApp + (CGlobal predicate) + subject) compileQuantifiedTermSubject :: Raw.Quantifier @@ -1291,6 +2202,10 @@ compileAtomicRelationTerms left relation right = (Raw.relationSymbolToken symbol) (Raw.relationSymbolParameterArity symbol) compiledParameters <- traverse compileExpressionAsSet parameters + checkedRight <- + if symbol == Raw.ElementSymbol && null parameters + then structureCarrierCast location right + else pure right case fixedSemanticMeaning key of Just FixedEquality | null parameters -> pure (CEq TySet left right) @@ -1304,7 +2219,7 @@ compileAtomicRelationTerms left relation right = (CIntrinsic intrinsic) (coreIntrinsicType intrinsic) ((\term -> (term, TySet)) - <$> (compiledParameters <> [left, right])) + <$> (compiledParameters <> [left, checkedRight])) unless (actual == TyProp) (Except.throwError (ExactFormulaExpectedProposition location actual)) @@ -1316,7 +2231,7 @@ compileAtomicRelationTerms left relation right = (CIntrinsic intrinsic) (coreIntrinsicType intrinsic) ((\term -> (term, TySet)) - <$> (compiledParameters <> [left, right])) + <$> (compiledParameters <> [left, checkedRight])) unless (actual == TyProp) (Except.throwError (ExactFormulaExpectedProposition location actual)) @@ -1326,7 +2241,7 @@ compileAtomicRelationTerms left relation right = applyResolvedTyped location key ((\term -> (term, TySet)) - <$> (compiledParameters <> [left, right])) + <$> (compiledParameters <> [left, checkedRight])) unless (actual == TyProp) (Except.throwError (ExactFormulaExpectedProposition location actual)) @@ -1562,11 +2477,22 @@ withAnonymousSetBinder -> Elaborate failure value withAnonymousSetBinder action = do outer <- State.gets elaborationBinders + outerStructures <- State.gets elaborationStructures + outerContextual <- State.gets elaborationContextualBinder State.modify' \state -> - state{elaborationBinders = (+ 1) <$> outer} + state + { elaborationBinders = (+ 1) <$> outer + , elaborationStructures = + Map.mapKeysMonotonic (+ 1) outerStructures + , elaborationContextualBinder = (+ 1) <$> outerContextual + } result <- action (CBound 0) State.modify' \state -> - state{elaborationBinders = outer} + state + { elaborationBinders = outer + , elaborationStructures = outerStructures + , elaborationContextualBinder = outerContextual + } pure result withSetBinders @@ -1575,6 +2501,8 @@ withSetBinders -> Elaborate failure value withSetBinders variables action = do outer <- State.gets elaborationBinders + outerStructures <- State.gets elaborationStructures + outerContextual <- State.gets elaborationContextualBinder case firstDuplicate (toList variables) of Just duplicate -> Except.throwError @@ -1599,10 +2527,18 @@ withSetBinders variables action = do State.modify' \state -> state { elaborationBinders = introduced <> shifted + , elaborationStructures = + Map.mapKeysMonotonic (+ binderCount) outerStructures + , elaborationContextualBinder = + (+ binderCount) <$> outerContextual } result <- action State.modify' \state -> - state{elaborationBinders = outer} + state + { elaborationBinders = outer + , elaborationStructures = outerStructures + , elaborationContextualBinder = outerContextual + } pure result compileFormula @@ -1930,6 +2866,54 @@ applyResolvedTyped location key arguments = do _ -> impossible "validated transparent expansion has opaque content" + ContextualTransparentExpansion _identity requirements -> + case content of + TransparentObjectContent _theory coreType body -> do + State.modify' \state -> + state + { elaborationGlobals = + Map.union + dependencies + (elaborationGlobals state) + } + contextArgument <- + resolveContextualExpansionArgument + location key requirements + applyExpandedTyped + location body coreType + ((contextArgument, TySet) : arguments) + _ -> + impossible + "validated contextual expansion has opaque content" + +resolveContextualExpansionArgument + :: Location + -> SemanticGlobalKey + -> Map.Map Raw.StructSymbol ObjectId + -> Elaborate failure (CanonicalTerm ObjectId) +resolveContextualExpansionArgument location key requirements = do + contextual <- State.gets elaborationContextualBinder + case contextual of + Just index -> do + traverse_ + (uncurry (recordContextualRequirement location)) + (Map.toAscList requirements) + pure (CBound index) + Nothing -> do + structures <- State.gets elaborationStructures + case + [ CBound index + | (index, structure) <- Map.toAscList structures + , all + (\(symbol, object) -> + structureAnnotationOperation symbol structure + == Just object) + (Map.toAscList requirements) + ] of + firstMatch : _ -> pure firstMatch + [] -> + Except.throwError + (ExactContextualExpansionNotAvailable location key) applyExpandedTyped :: Location @@ -2093,6 +3077,13 @@ encodePreparedSyntax TransparentBody canonical -> do putCacheTag 0x01 putCanonicalTermCache putObjectIdCache canonical + ContextualTransparentBody requirements canonical -> do + putCacheTag 0x02 + putCanonicalCacheMap + (\(Raw.StructSymbol symbol) -> putCacheText symbol) + putObjectIdCache + requirements + putCanonicalTermCache putObjectIdCache canonical putCacheMaybe (putCacheText . semanticNameText) alias |