diff options
Diffstat (limited to 'source/Felix/Checking/Exact.hs')
| -rw-r--r-- | source/Felix/Checking/Exact.hs | 3936 |
1 files changed, 3936 insertions, 0 deletions
diff --git a/source/Felix/Checking/Exact.hs b/source/Felix/Checking/Exact.hs new file mode 100644 index 0000000..c829743 --- /dev/null +++ b/source/Felix/Checking/Exact.hs @@ -0,0 +1,3936 @@ +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE NoImplicitPrelude #-} + +-- | Direct compiler for the first exact monomorphic declaration family. +module Felix.Checking.Exact + ( ExactLocalId + , exactLocalId + , exactLocalIdValue + , ExactBinderContext + , emptyExactBinderContext + , extendExactBinderContext + , extendExactAnonymousBinderContext + , exactBinderContextSupport + , exactBinderContextIndex + , PreparedExactProposition + , preparedExactPropositionCore + , prepareExactProposition + , prepareExactSymbolicBoundConstraints + , prepareExactSymbolicWitnessConstraints + , prepareExactNounWitnessConstraints + , PreparedExactSetExpression + , PreparedExactSetConstruction(..) + , preparedExactSetExpressionCore + , preparedExactSetExpressionConstruction + , prepareExactSetExpression + , PreparedExactLocalFunctionGraph + , preparedExactLocalFunctionGraphCore + , preparedExactLocalFunctionGraphDomain + , preparedExactLocalFunctionGraphMap + , prepareExactLocalFunctionGraph + , PreparedExactClaimEnvelope + , preparedExactClaimTarget + , preparedExactClaimVariables + , preparedExactClaimContext + , preparedExactClaimAntecedentCount + , prepareExactClaimEnvelope + , PreparedExactDeclaration + , preparedExactLocation + , preparedExactGlobalKey + , preparedExactObjectId + , preparedExactObject + , preparedExactSyntaxId + , preparedExactIsDefinition + , prepareExactDeclaration + , lowerPreparedExactBinding + , CheckedExactBindingAuthorization + , authorizeCheckedExactBinding + , PreparedExactStructure + , prepareExactStructure + , CheckedExactStructureAuthorization + , lowerPreparedExactStructure + , authorizeCheckedExactStructure + , PreparedExactSourceAxiom + , prepareExactSourceAxiom + , lowerPreparedExactSourceAxiom + , authorizeCheckedExactSourceAxiom + , ExactCompileError(..) + , exactCompileErrorLocation + , renderExactCompileError + ) where + +import Base hiding (Empty) +import Felix.Cache.Codec +import Felix.Checking.Core +import Felix.Checking.Declaration qualified as Declaration +import Felix.Checking.Exact.Vocabulary +import Felix.Checking.Identity +import Felix.Checking.Semantic +import Felix.Checking.SetConstruction +import Felix.Module +import Felix.Report.Location +import Felix.Syntax.Abstract qualified as Raw +import Felix.Syntax.Interface (CanonicalLexicalEntry(..)) +import Felix.Syntax.Lexicon qualified as Lexicon + +import Control.Monad.Except (ExceptT) +import Control.Monad.Except (MonadError, throwError) +import Control.Monad.Except qualified as Except +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) +import Data.Set qualified as Set +import Data.Text qualified as Text +import Data.Vector (Vector) +import Data.Vector qualified as Vector +import Numeric.Natural (Natural) + + +-- | A disposable identity allocated in source order within one proof. +newtype ExactLocalId = ExactLocalId Natural + deriving stock (Show, Eq, Ord) + +exactLocalId :: Natural -> ExactLocalId +exactLocalId = ExactLocalId + +exactLocalIdValue :: ExactLocalId -> Natural +exactLocalIdValue (ExactLocalId value) = value + +data ExactBinder = ExactBinder + !ExactLocalId + !(Maybe 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] + +emptyExactBinderContext :: ExactBinderContext +emptyExactBinderContext = ExactBinderContext [] + +extendExactBinderContext + :: NonEmpty (ExactLocalId, Raw.VarSymbol) + -> ExactBinderContext + -> Either ExactCompileError ExactBinderContext +extendExactBinderContext additions (ExactBinderContext initial) = + ExactBinderContext <$> foldM add initial (toList additions) + where + add binders (identity, variable) + | any (sameVariable variable) binders = + Left (ExactDuplicateLocalBinder (locate variable) variable) + | any (sameIdentity identity) binders = + Left (ExactDuplicateLocalIdentity (locate variable) identity) + | otherwise = + Right (ExactBinder identity (Just variable) TySet Nothing : binders) + + sameVariable variable (ExactBinder _identity existing _coreType _structure) = + existing == Just variable + + sameIdentity identity (ExactBinder existing _variable _coreType _structure) = + existing == identity + +-- | Add one proof-owned binder which deliberately has no source-resolvable +-- spelling. This is used for a nameless singular witness; it participates in +-- checked support and de Bruijn weakening but cannot shadow or be looked up by +-- a later source variable. +extendExactAnonymousBinderContext + :: ExactLocalId + -> ExactBinderContext + -> Either ExactCompileError ExactBinderContext +extendExactAnonymousBinderContext identity (ExactBinderContext binders) + | any sameIdentity binders = + Left (ExactDuplicateLocalIdentity Nowhere identity) + | otherwise = + Right + (ExactBinderContext + (ExactBinder identity Nothing TySet Nothing : binders)) + where + sameIdentity (ExactBinder existing _variable _coreType _structure) = + existing == identity + +exactBinderContextSupport + :: ExactBinderContext + -> Vector (ExactLocalId, CoreType) +exactBinderContextSupport (ExactBinderContext binders) = + Vector.fromList + [ (identity, coreType) + | ExactBinder identity _variable coreType _structure <- binders + ] + +exactBinderContextIndex + :: Raw.VarSymbol + -> ExactBinderContext + -> Maybe Natural +exactBinderContextIndex variable (ExactBinderContext binders) = + go 0 binders + where + go _index [] = + Nothing + go index (ExactBinder _identity candidate _coreType _structure : rest) + | candidate == Just variable = Just index + | otherwise = go (index + 1) rest + +newtype PreparedExactProposition = PreparedExactProposition + (ScopedCheckedCore ObjectId) + +preparedExactPropositionCore + :: PreparedExactProposition + -> ScopedCheckedCore ObjectId +preparedExactPropositionCore (PreparedExactProposition proposition) = + proposition + +data PreparedExactSetExpression = PreparedExactSetExpression + !(ScopedCheckedCore ObjectId) + !(Maybe PreparedExactSetConstruction) + +data PreparedExactSetConstruction + = PreparedUnconditionalSetConstruction + !(NamedSetConstruction ObjectId) + | PreparedRelationalSetConstruction + !(CheckedRelationalSetConstruction ObjectId) + +preparedExactSetExpressionCore + :: PreparedExactSetExpression + -> ScopedCheckedCore ObjectId +preparedExactSetExpressionCore (PreparedExactSetExpression expression _construction) = + expression + +preparedExactSetExpressionConstruction + :: PreparedExactSetExpression + -> Maybe PreparedExactSetConstruction +preparedExactSetExpressionConstruction + (PreparedExactSetExpression _expression construction) = + construction + +-- | 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 _context _antecedents) = + target + +preparedExactClaimVariables + :: PreparedExactClaimEnvelope + -> [Raw.VarSymbol] +preparedExactClaimVariables + (PreparedExactClaimEnvelope _target variables _context _antecedents) = + variables + +preparedExactClaimContext + :: PreparedExactClaimEnvelope + -> ExactBinderContext +preparedExactClaimContext + (PreparedExactClaimEnvelope _target _variables context _antecedents) = + context + +preparedExactClaimAntecedentCount + :: PreparedExactClaimEnvelope + -> Natural +preparedExactClaimAntecedentCount + (PreparedExactClaimEnvelope _target _variables _context antecedents) = + antecedents + + +data ExactDeclarationFamily + = ExactSignature + | ExactAbbreviation + | ExactDefinition + deriving stock (Show, Eq, Ord) + +data PreparedExactDeclaration = PreparedExactDeclaration + !Location + !ExactDeclarationFamily + !SemanticGlobalKey + !SemanticGlobalTarget + !(Maybe AssertedObject) + !(Maybe SemanticName) + !(Maybe PreparedExactSetConstruction) + !DeclarationSyntaxId + +preparedExactLocation :: PreparedExactDeclaration -> Location +preparedExactLocation + (PreparedExactDeclaration location _family _key _target _object _alias _construction _syntax) = + location + +preparedExactGlobalKey :: PreparedExactDeclaration -> SemanticGlobalKey +preparedExactGlobalKey + (PreparedExactDeclaration _location _family key _target _object _alias _construction _syntax) = + key + +preparedExactObjectId :: PreparedExactDeclaration -> ObjectId +preparedExactObjectId + (PreparedExactDeclaration _location _family _key target _object _alias _construction _syntax) = + semanticGlobalTargetObject target + +preparedExactObject + :: PreparedExactDeclaration + -> Maybe AssertedObject +preparedExactObject + (PreparedExactDeclaration _location _family _key _target object _alias _construction _syntax) = + object + +preparedExactSyntaxId + :: PreparedExactDeclaration + -> DeclarationSyntaxId +preparedExactSyntaxId + (PreparedExactDeclaration _location _family _key _target _object _alias _construction syntax) = + syntax + +preparedExactIsDefinition :: PreparedExactDeclaration -> Bool +preparedExactIsDefinition + (PreparedExactDeclaration _location family _key _target _object _alias _construction _syntax) = + family == ExactDefinition + +preparedExactGlobalTarget + :: PreparedExactDeclaration + -> SemanticGlobalTarget +preparedExactGlobalTarget + (PreparedExactDeclaration + _location _family _key target _object _alias _construction _syntax) = + target + +preparedDefinitionAlias + :: PreparedExactDeclaration + -> Maybe SemanticName +preparedDefinitionAlias + (PreparedExactDeclaration + _location _family _key _target _object alias _construction _syntax) = + alias + +preparedDefinitionConstruction + :: PreparedExactDeclaration + -> Maybe PreparedExactSetConstruction +preparedDefinitionConstruction + (PreparedExactDeclaration + _location _family _key _target _object _alias construction _syntax) = + construction + +data PreparedExactSourceAxiom = PreparedExactSourceAxiom + !Location + !SemanticName + !(ScopedCheckedCore ObjectId) + !DeclarationSyntaxId + +data PreparedExactStructureFact = PreparedExactStructureFact + !Location + !(FrozenCheckedCore ObjectId) + !SemanticName + +data PreparedExactStructure = PreparedExactStructure + !Location + ![AssertedObject] + !ObjectId + !SemanticStructureDescriptor + !SemanticName + ![PreparedExactStructureFact] + !DeclarationSyntaxId + +data CheckedExactStructureAuthorization = + CheckedExactStructureAuthorization + !ObjectId + ![(Location, Declaration.PreparedVampireObligation Void ())] + +data ExactCompileError + = ExactUnsupportedDeclaration !Location + | ExactUnsupportedDeclarationBody !Location + | ExactNonCanonicalSetDefinitionAnnotation !Location + | ExactGuardedTransparentDefinition !Location + | ExactGuardedOpaqueSignature !Location + | ExactDefinitionCombinedSymbolicAlias !Location + | ExactRelationalReplacementRequiresNamedDefinition !Location + | ExactDeclarationOccurrenceMissing !Location + | ExactDeclarationOccurrenceAmbiguous !Location + | ExactDeclarationHeadMismatch !Location + | ExactFixedSemanticCollision !Location !SemanticGlobalKey + | ExactGlobalAlreadyVisible !Location !SemanticGlobalKey + | ExactGlobalNotVisible !Location !SemanticGlobalKey + | ExactDuplicateParameter !Location !Raw.VarSymbol + | ExactDuplicateLocalBinder !Location !Raw.VarSymbol + | ExactDuplicateLocalIdentity !Location !ExactLocalId + | ExactFreeVariable !Location !Raw.VarSymbol + | ExactApplicationExpectedFunction !Location !CoreType + | ExactApplicationArgumentMismatch + !Location !CoreType !CoreType + | ExactExpressionExpectedSet !Location !CoreType + | ExactFormulaExpectedProposition !Location !CoreType + | ExactCoreCheckFailed !Location !CoreCheckError + | ExactObjectTypeMismatch !Location !CoreType !CoreType + | ExactUnsupportedHeaderAssumption !Location + | ExactQuantifiedTermRequiresPropositionContext !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 +exactCompileErrorLocation = \case + ExactUnsupportedDeclaration location -> location + ExactUnsupportedDeclarationBody location -> location + ExactNonCanonicalSetDefinitionAnnotation location -> location + ExactGuardedTransparentDefinition location -> location + ExactGuardedOpaqueSignature location -> location + ExactDefinitionCombinedSymbolicAlias location -> location + ExactRelationalReplacementRequiresNamedDefinition location -> location + ExactDeclarationOccurrenceMissing location -> location + ExactDeclarationOccurrenceAmbiguous location -> location + ExactDeclarationHeadMismatch location -> location + ExactFixedSemanticCollision location _key -> location + ExactGlobalAlreadyVisible location _key -> location + ExactGlobalNotVisible location _key -> location + ExactDuplicateParameter location _parameter -> location + ExactDuplicateLocalBinder location _variable -> location + ExactDuplicateLocalIdentity location _identity -> location + ExactFreeVariable location _variable -> location + ExactApplicationExpectedFunction location _actual -> location + ExactApplicationArgumentMismatch location _expected _actual -> location + ExactExpressionExpectedSet location _actual -> location + ExactFormulaExpectedProposition location _actual -> location + ExactCoreCheckFailed location _failure -> location + ExactObjectTypeMismatch location _expected _actual -> location + ExactUnsupportedHeaderAssumption location -> location + ExactQuantifiedTermRequiresPropositionContext 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 + ExactUnsupportedDeclaration location -> + at location <> "this declaration is not yet supported by the typed checker" + ExactUnsupportedDeclarationBody location -> + at location <> "this source form is not yet supported by exact elaboration" + ExactNonCanonicalSetDefinitionAnnotation location -> + at location + <> "only the unmodified built-in noun `set` is a harmless definition annotation; " + <> "state a total condition in the definiens, or, where a corresponding opaque signature form exists, use it with a following explicit axiom; otherwise migrate the spelling or leave it unsupported" + ExactGuardedTransparentDefinition location -> + at location + <> "a transparent definition cannot have a header assumption; " + <> "state a total condition in the definiens, or, where a corresponding opaque signature form exists, use it with a following explicit axiom; otherwise migrate the spelling or leave it unsupported" + ExactGuardedOpaqueSignature location -> + at location + <> "an opaque signature cannot have a header assumption; " + <> "state the condition in a following explicit axiom" + ExactDefinitionCombinedSymbolicAlias location -> + at location + <> "a functional definition cannot declare a symbolic equivalent at the same time; " + <> "define the symbolic operator first, then define the functional phrase as an abbreviation applying it" + ExactRelationalReplacementRequiresNamedDefinition location -> + at location + <> "relational replacement is supported only as the outer body of a named definition" + ExactDeclarationOccurrenceMissing location -> + at location <> "the declaration has no associated syntax occurrence" + ExactDeclarationOccurrenceAmbiguous location -> + at location <> "the declaration has more than one semantic head" + ExactDeclarationHeadMismatch location -> + at location <> "the parsed declaration head does not match its syntax occurrence" + ExactFixedSemanticCollision location key -> + at location <> "the declaration collides with fixed semantics for " + <> shown key + ExactGlobalAlreadyVisible location key -> + at location <> "the global " <> shown key <> " is already declared" + ExactGlobalNotVisible location key -> + at location <> "the global " <> shown key <> " is not visible" + ExactDuplicateParameter location parameter -> + at location <> "the declaration parameter " <> shown parameter <> " is repeated" + ExactDuplicateLocalBinder location variable -> + at location <> "the proof binder " <> shown variable <> " is already active" + ExactDuplicateLocalIdentity location identity -> + at location <> "the proof-local identity " <> shown identity <> " is already active" + ExactFreeVariable location variable -> + at location <> "the exact source form contains the free variable " <> shown variable + ExactApplicationExpectedFunction location actual -> + at location <> "an application expected a function, but found " <> shown actual + ExactApplicationArgumentMismatch location expected actual -> + at location <> "an application expected " <> shown expected + <> ", but found " <> shown actual + ExactExpressionExpectedSet location actual -> + at location <> "an expression has type " <> shown actual <> " instead of Set" + ExactFormulaExpectedProposition location actual -> + at location <> "a formula has type " <> shown actual <> " instead of Prop" + ExactCoreCheckFailed location failure -> + at location <> "the checked declaration core is invalid: " <> shown failure + ExactObjectTypeMismatch location expected actual -> + at location <> "the declaration object has type " <> shown actual + <> " instead of " <> shown expected + ExactUnsupportedHeaderAssumption location -> + at location <> "this top-level header assumption is not yet supported by exact elaboration" + ExactQuantifiedTermRequiresPropositionContext location -> + at location + <> "a quantified term requires a containing proposition" + 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 + shown = Text.pack . show + +data ElaborationState = ElaborationState + { elaborationBinders :: !(Map.Map Raw.VarSymbol Natural) + -- Counts every active de Bruijn binder, including anonymous and + -- contextual binders which have no entry in 'elaborationBinders'. + , elaborationBinderDepth :: !Natural + , elaborationStructures :: !(Map.Map Natural ExactStructureAnnotation) + , elaborationGlobals :: !(Map.Map ObjectId CoreType) + , elaborationContextualBinder :: !(Maybe Natural) + , elaborationContextualRequirements + :: !(Map.Map Raw.StructSymbol ObjectId) + } + +type Elaborate = + StateT + ElaborationState + (ExceptT ExactCompileError (Declaration.LoweringDriver)) + +data PreparedHead = PreparedHead + !SemanticGlobalKey + ![Raw.VarSymbol] + !CoreType + +data PreparedBody + = OpaqueBody + | TransparentBody + !(CanonicalTerm ObjectId) + !(Maybe PreparedExactSetConstruction) + | ContextualTransparentBody + !(Map.Map Raw.StructSymbol ObjectId) + !(CanonicalTerm ObjectId) + +data CompiledBody = CompiledBody + !(CanonicalTerm ObjectId) + !(Maybe CompiledNamedSetConstruction) + +data CompiledNamedSetConstruction + = CompiledSeparationConstruction + !(CanonicalTerm ObjectId) + !(CanonicalTerm ObjectId) + | CompiledFunctionalReplacementConstruction + !(NonEmpty (CanonicalTerm ObjectId)) + !(CanonicalTerm ObjectId) + !(Maybe (CanonicalTerm ObjectId)) + | CompiledRelationalReplacementConstruction + !(CanonicalTerm ObjectId) + !(CanonicalTerm ObjectId) + +prepareExactProposition + :: ExactBinderContext + -> Raw.Stmt + -> Declaration.LoweringDriver + (Either ExactCompileError PreparedExactProposition) +prepareExactProposition context statement = + prepareExactPropositionTerm + context + (locate statement) + (compileStatement statement) + +-- | Compile the source bound of already-opened symbolic binders. This is the +-- shared checked constraint seam used by quantified statements and proof +-- binders, so relation signs, carrier casts, and global occurrences are +-- elaborated exactly once by the ordinary expression compiler. +prepareExactSymbolicBoundConstraints + :: ExactBinderContext + -> NonEmpty Raw.VarSymbol + -> Raw.Bound + -> Declaration.LoweringDriver + (Either ExactCompileError PreparedExactProposition) +prepareExactSymbolicBoundConstraints context variables bound = + prepareExactPropositionTerm + context + (case bound of + Raw.Unbounded -> locate (NonEmpty.head variables) + _ -> locate bound) + (logicalConjunction + <$> compileSymbolicBoundConstraintList variables bound) + +-- | Compile the opened body used by a symbolic existential witness. Its +-- grouping is deliberately identical to 'SymbolicExists': all bound +-- constraints form the existential restriction and the stated proposition is +-- its body. +prepareExactSymbolicWitnessConstraints + :: ExactBinderContext + -> NonEmpty Raw.VarSymbol + -> Raw.Bound + -> Raw.Stmt + -> Declaration.LoweringDriver + (Either ExactCompileError PreparedExactProposition) +prepareExactSymbolicWitnessConstraints context variables bound statement = + prepareExactPropositionTerm context (locate statement) do + constraints <- + logicalConjunction + <$> compileSymbolicBoundConstraintList variables bound + body <- compileStatement statement + pure + (if constraints == logicalTruth + then body + else logicalAnd constraints body) + +-- | Compile the checked constraint of an already-opened noun witness. Named +-- binders are resolved normally; a nameless singular noun uses the nearest +-- anonymous binder and therefore introduces no lookup spelling. +prepareExactNounWitnessConstraints + :: ExactBinderContext + -> Raw.NounPhrase [] + -> Declaration.LoweringDriver + (Either ExactCompileError PreparedExactProposition) +prepareExactNounWitnessConstraints context nounPhrase = + case nounPhrase of + Raw.NounPhrase left noun variables right suchThat -> + prepareExactPropositionTerm context (locate noun) do + subjects <- + case NonEmpty.nonEmpty variables of + Just binders -> + toList + <$> traverse compileIntroducedVariable binders + Nothing -> + pure [CBound 0] + compileNounPhraseConstraints + subjects left noun right suchThat + +prepareExactPropositionTerm + :: ExactBinderContext + -> Location + -> Elaborate (CanonicalTerm ObjectId) + -> Declaration.LoweringDriver + (Either ExactCompileError PreparedExactProposition) +prepareExactPropositionTerm context location compile = + Except.runExceptT do + let initialElaboration = initialElaborationState context + (term, finalElaboration) <- + State.runStateT compile initialElaboration + checked <- + either + (Except.throwError . ExactCoreCheckFailed location) + pure + (checkScopedCanonicalCore + (`Map.lookup` elaborationGlobals finalElaboration) + (binderTypes context) + term) + unless (scopedCoreType checked == TyProp) + (Except.throwError + (ExactFormulaExpectedProposition + location + (scopedCoreType checked))) + pure (PreparedExactProposition checked) + +prepareExactSetExpression + :: ExactBinderContext + -> Raw.Expr + -> Declaration.LoweringDriver + (Either ExactCompileError PreparedExactSetExpression) +prepareExactSetExpression context expression = + Except.runExceptT do + let initialElaboration = initialElaborationState context + (compiled, finalElaboration) <- + State.runStateT + (compileNamedSetExpression expression) + initialElaboration + let CompiledBody term rawConstruction = compiled + checked <- + either + (Except.throwError + . ExactCoreCheckFailed (locate expression)) + pure + (checkScopedCanonicalCore + (`Map.lookup` elaborationGlobals finalElaboration) + (binderTypes context) + term) + unless (scopedCoreType checked == TySet) + (Except.throwError + (ExactExpressionExpectedSet + (locate expression) + (scopedCoreType checked))) + construction <- + Except.liftEither + (traverse + (checkCompiledNamedSetConstruction + (`Map.lookup` elaborationGlobals finalElaboration) + (binderTypes context)) + rawConstruction) + traverse_ + (\checkedConstruction -> + unless + (preparedSetConstructionTerm checkedConstruction == checked) + (impossible + "exact named construction disagrees with its checked expression")) + construction + pure (PreparedExactSetExpression checked construction) + +checkCompiledNamedSetConstruction + :: (ObjectId -> Maybe CoreType) + -> [CoreType] + -> CompiledNamedSetConstruction + -> Either ExactCompileError PreparedExactSetConstruction +checkCompiledNamedSetConstruction globalType context = \case + CompiledSeparationConstruction bound predicate -> do + checkedBound <- checkAt context TySet bound + checkedPredicate <- checkAt (TySet : context) TyProp predicate + maybe + (Left + (ExactCoreCheckFailed + Nowhere + (ExpectedCoreType TySet TyProp))) + (Right . PreparedUnconditionalSetConstruction) + (checkedSeparationConstruction + globalType checkedBound checkedPredicate) + CompiledFunctionalReplacementConstruction domains value condition -> do + let domainList = NonEmpty.toList domains + fullContext = replicate (length domainList) TySet <> context + checkedDomains <- + traverse + (\(depth, domain) -> + checkAt + (replicate depth TySet <> context) + TySet + domain) + (zip [0..] domainList) + checkedValue <- checkAt fullContext TySet value + checkedCondition <- traverse (checkAt fullContext TyProp) condition + maybe + (Left + (ExactCoreCheckFailed + Nowhere + (ExpectedCoreType TySet TyProp))) + (Right . PreparedUnconditionalSetConstruction) + (checkedFunctionalReplacementConstruction + globalType + (NonEmpty.fromList checkedDomains) + checkedValue + checkedCondition) + CompiledRelationalReplacementConstruction domain relation -> do + checkedDomain <- checkAt context TySet domain + checkedRelation <- checkAt (TySet : TySet : context) TyProp relation + maybe + (Left + (ExactCoreCheckFailed + Nowhere + (ExpectedCoreType TySet TyProp))) + (Right . PreparedRelationalSetConstruction) + (checkedRelationalReplacementConstruction + globalType checkedDomain checkedRelation) + where + checkAt expectedContext expectedType term = do + checked <- + first + (ExactCoreCheckFailed Nowhere) + (checkScopedCanonicalCore globalType expectedContext term) + unless + (scopedCoreType checked == expectedType) + (Left + (ExactCoreCheckFailed + Nowhere + (ExpectedCoreType + expectedType + (scopedCoreType checked)))) + pure checked + +preparedSetConstructionTerm + :: PreparedExactSetConstruction + -> ScopedCheckedCore ObjectId +preparedSetConstructionTerm = \case + PreparedUnconditionalSetConstruction construction -> + namedSetConstructionTerm construction + PreparedRelationalSetConstruction construction -> + relationalSetConstructionTerm construction + +preparedSetConstructionClosedBody + :: PreparedExactSetConstruction + -> FrozenCheckedCore ObjectId +preparedSetConstructionClosedBody = \case + PreparedUnconditionalSetConstruction construction -> + namedSetConstructionClosedBody construction + PreparedRelationalSetConstruction construction -> + relationalSetConstructionClosedBody construction + +prepareExactLocalFunctionGraph + :: Location + -> ExactBinderContext + -> ExactBinderContext + -> Raw.Expr + -> Raw.Expr + -> Declaration.LoweringDriver + (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 + -> Declaration.LoweringDriver + (Either ExactCompileError PreparedExactClaimEnvelope) +prepareExactClaimEnvelope assumptions statement = + discover [] emptyExactBinderContext + where + discover variables context = do + attempted <- prepareExactClaimAttempt context assumptions statement + case attempted of + Left (ExactFreeVariable _location variable) + | variable `elem` variables -> + impossible + "exact claim discovery repeated an active free variable" + | otherwise -> + case extendExactBinderContext + ( ( exactLocalId + (fromIntegral (length variables)) + , variable + ) :| [] + ) + context of + Left failure -> + pure (Left failure) + Right extended -> + discover (variables <> [variable]) extended + Left failure -> + pure (Left failure) + Right (target, antecedentCount, structures) -> + pure + (Right + (PreparedExactClaimEnvelope + target + variables + (annotateBinderContext structures context) + antecedentCount)) + +prepareExactClaimAttempt + :: ExactBinderContext + -> [Raw.Asm] + -> Raw.Stmt + -> Declaration.LoweringDriver + (Either + ExactCompileError + ( ScopedCheckedCore ObjectId + , Natural + , Map.Map Natural ExactStructureAnnotation + )) +prepareExactClaimAttempt context assumptions statement = + Except.runExceptT do + let initialElaboration = initialElaborationState context + ((antecedents, conclusion), finalElaboration) <- + State.runStateT + ( do + antecedents <- + concat <$> traverse compileHeaderAssumption assumptions + conclusion <- compileStatement statement + pure (antecedents, conclusion) + ) + initialElaboration + checkedAntecedents <- + traverse + (uncurry + (checkEnvelopeProposition + finalElaboration + context)) + antecedents + checkedConclusion <- + checkEnvelopeProposition + finalElaboration + context + (locate statement) + conclusion + let implication = + foldr + (\antecedent continuation -> + fromMaybe + (impossible + "checked claim antecedents have unequal contexts") + (implyScopedCore antecedent continuation)) + checkedConclusion + checkedAntecedents + closed = closeClaimBinders implication + unless (null (scopedCoreContext closed)) + (impossible "exact claim closure retained a binder") + pure + ( closed + , fromIntegral (length antecedents) + , elaborationStructures finalElaboration + ) + +checkEnvelopeProposition + :: ElaborationState + -> ExactBinderContext + -> Location + -> CanonicalTerm ObjectId + -> ExceptT + ExactCompileError + (Declaration.LoweringDriver) + (ScopedCheckedCore ObjectId) +checkEnvelopeProposition elaboration context location term = do + checked <- + either + (Except.throwError . ExactCoreCheckFailed location) + pure + (checkScopedCanonicalCore + (`Map.lookup` elaborationGlobals elaboration) + (binderTypes context) + term) + unless (scopedCoreType checked == TyProp) + (Except.throwError + (ExactFormulaExpectedProposition + location + (scopedCoreType checked))) + pure checked + +closeClaimBinders + :: ScopedCheckedCore global + -> ScopedCheckedCore global +closeClaimBinders scoped = + case scopedCoreContext scoped of + [] -> scoped + _binder : _remaining -> + closeClaimBinders + (fromMaybe + (impossible + "a checked claim binder could not be closed") + (closeScopedForall scoped)) + +binderIndices :: ExactBinderContext -> Map.Map Raw.VarSymbol Natural +binderIndices (ExactBinderContext binders) = + Map.fromList + [ (variable, fromIntegral index) + | (index, ExactBinder _identity (Just 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 _structure <- binders + ] + +initialElaborationState :: ExactBinderContext -> ElaborationState +initialElaborationState context = + ElaborationState + { elaborationBinders = binderIndices context + , elaborationBinderDepth = + fromIntegral (length (binderTypes context)) + , elaborationStructures = binderStructures context + , elaborationGlobals = mempty + , elaborationContextualBinder = Nothing + , elaborationContextualRequirements = 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 [(Location, CanonicalTerm ObjectId)] +compileHeaderAssumption = \case + Raw.AsmSuppose statement -> do + proposition <- compileStatement statement + pure [(locate statement, proposition)] + Raw.AsmLetNoun variables nounPhrase + | exactSetNounPhrase nounPhrase -> do + traverse_ compileIntroducedVariable variables + pure [] + | otherwise -> do + subjects <- traverse compileIntroducedVariable variables + constraints <- + traverse (`compileNounPhraseMaybe` nounPhrase) subjects + pure + [ (locate variable, constraint) + | (variable, constraint) <- + zip (toList variables) (toList constraints) + ] + Raw.AsmLetIn variables domain -> do + variableTerms <- traverse compileIntroducedVariable variables + domainTerm <- compileExpressionAsSet domain + traverse + (\(variable, variableTerm) -> do + proposition <- + compileMembership + (locate domain) + Raw.Positive + variableTerm + domainTerm + pure (locate variable, proposition)) + (zip (toList variables) (toList variableTerms)) + Raw.AsmLetEq variable expression -> do + variableTerm <- compileIntroducedVariable variable + expressionTerm <- compileExpressionAsSet expression + pure + [ ( locate variable + , CEq TySet variableTerm expressionTerm + ) + ] + Raw.AsmLetThe variable _function -> + 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 + -> Elaborate (CanonicalTerm ObjectId) +compileIntroducedVariable variable = + compileExpressionAsSet (Raw.ExprVar variable) + +resolveStructureAnnotation + :: Location + -> Raw.StructPhrase + -> Elaborate ExactStructureAnnotation +resolveStructureAnnotation location rawPhrase = do + let structurePhrase = semanticStructurePhrase rawPhrase + resolved <- + State.lift + (Except.lift + (Declaration.resolveVisibleStructureLowering 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 () +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.LoweringDriver + (Either ExactCompileError PreparedExactSourceAxiom) +prepareExactSourceAxiom = \case + Raw.BlockAxiom + location _title (Raw.Marker marker) + (Raw.Axiom assumptions statement) -> do + prepared <- prepareExactClaimEnvelope assumptions statement + pure do + envelope <- prepared + let core = preparedExactClaimTarget envelope + alias = semanticName marker + unless (null (scopedCoreContext core)) + (Left (ExactUnsupportedDeclarationBody location)) + pure + (PreparedExactSourceAxiom + location + alias + core + (declarationSyntaxId + (encodePreparedSourceAxiom core alias))) + block -> + pure (Left (ExactUnsupportedDeclaration (locate block))) + +lowerPreparedExactSourceAxiom + :: PreparedExactSourceAxiom + -> Declaration.LoweringDriver + (Either + Declaration.DeclarationError + (Declaration.CheckedDeclaration ())) +lowerPreparedExactSourceAxiom + (PreparedExactSourceAxiom _location alias target syntax) = + fmap + (\spec -> + Declaration.checkedCompiledDeclaration + syntax [] [] [] [] + [ Declaration.checkedCandidate + spec + Declaration.checkedSourceAxiomPlanning + :| [] + ] + ()) + <$> Declaration.prepareCandidateSpecLowering + [] target SearchEligible [alias] + +authorizeCheckedExactSourceAxiom + :: () + -> [NonEmpty Declaration.ReservedCandidate] + -> Declaration.Declaration () +authorizeCheckedExactSourceAxiom () = \case + [candidate :| []] -> + Declaration.authorizeSourceAxiomCandidate candidate + stages -> + Declaration.failDeclaration + (Declaration.CheckedAuthorizationCandidateShapeMismatch + 1 (length stages)) + +prepareExactDeclaration + :: Raw.Block + -> [CanonicalLexicalEntry] + -> Declaration.LoweringDriver + (Either ExactCompileError PreparedExactDeclaration) +prepareExactDeclaration block entries = + Except.runExceptT do + entry <- + case entries of + [] -> Except.throwError + (ExactDeclarationOccurrenceMissing (locate block)) + [single] -> pure single + _ -> Except.throwError + (ExactDeclarationOccurrenceAmbiguous (locate block)) + key <- + maybe + (Except.throwError + (ExactUnsupportedDeclaration (locate block))) + pure + (semanticGlobalKeyFromLexicalEntry entry) + when + (isJust (fixedSemanticMeaning key)) + (Except.throwError + (ExactFixedSemanticCollision (locate block) key)) + visible <- Except.lift + (Declaration.resolveVisibleGlobalLowering key) + when + (isJust visible) + (Except.throwError + (ExactGlobalAlreadyVisible (locate block) key)) + (head', family, rawBody) <- + prepareHead block key + slot <- Except.lift Declaration.nextDeclarationSlotLowering + theory <- Except.lift Declaration.currentTheoryLowering + (body, globals) <- + case rawBody of + Nothing -> pure (OpaqueBody, Map.empty) + Just buildBody -> do + let initialElaboration = + ElaborationState + { elaborationBinders = mempty + , elaborationBinderDepth = 0 + , elaborationStructures = mempty + , elaborationGlobals = mempty + , elaborationContextualBinder = Nothing + , elaborationContextualRequirements = mempty + } + (CompiledBody canonical rawConstruction, finalElaboration) <- + State.runStateT buildBody initialElaboration + let PreparedHead _semanticKey parameters _coreType = head' + construction <- + Except.liftEither + (traverse + (checkCompiledNamedSetConstruction + (`Map.lookup` + elaborationGlobals finalElaboration) + (replicate (length parameters) TySet)) + rawConstruction) + traverse_ + (\checkedConstruction -> + unless + (frozenCoreTerm + (preparedSetConstructionClosedBody + checkedConstruction) + == canonical) + (impossible + "exact named construction disagrees with its transparent body")) + construction + let requirements = + elaborationContextualRequirements finalElaboration + body + | Map.null requirements = + TransparentBody canonical construction + | 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 + (ExactDeclarationHeadMismatch (locate block))) + (target, content) <- + case body of + OpaqueBody -> do + let seed = + opaqueDeclarationSeed + (declarationSlotModule slot) + (declarationSlotOrdinal slot) + SignatureDeclaration + (generatedObjectSlot 0) + content' = + OpaqueObjectContent theory seed coreType + identity = opaqueObjectId theory seed coreType + pure (GlobalReference identity, content') + TransparentBody canonical _construction -> do + checked <- + either + (Except.throwError + . ExactCoreCheckFailed (locate block)) + pure + (checkCanonicalCore + (`Map.lookup` globals) + canonical) + unless + (frozenCoreType checked == coreType) + (Except.throwError + (ExactObjectTypeMismatch + (locate block) + coreType + (frozenCoreType checked))) + let content' = + TransparentObjectContent + 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 + ( ContextualTransparentExpansion + identity requirements + , content' + ) + let targetObject = semanticGlobalTargetObject target + available <- + Except.lift (Declaration.objectAvailableLowering targetObject) + let alias = definitionAlias block + asserted + | available = Nothing + | otherwise = Just (assertedObject targetObject content) + syntax = + declarationSyntaxId + (encodePreparedSyntax family head' body alias) + pure + (PreparedExactDeclaration + (locate block) + family + key + target + asserted + alias + (case family of + ExactDefinition -> case body of + TransparentBody _canonical construction -> construction + _ -> Nothing + _ -> Nothing) + syntax) + +lowerPreparedExactBinding + :: PreparedExactDeclaration + -> Declaration.LoweringDriver + (Either + Declaration.DeclarationError + (Declaration.CheckedDeclaration CheckedExactBindingAuthorization)) +lowerPreparedExactBinding prepared = + case preparedDefinitionAlias prepared of + Nothing -> + pure + (Right + (checked [] CheckedExactBindingNone)) + Just alias -> case preparedDefinitionConstruction prepared of + Nothing -> + fmap + (\spec -> + checked + [ Declaration.checkedCandidate + spec + (Declaration.checkedDefinitionEquationPlanning + identity) + :| [] + ] + (CheckedExactBindingDefinition identity)) + <$> Declaration.prepareDefinitionEquationSpecLowering + objects identity alias + Just (PreparedUnconditionalSetConstruction construction) -> + Except.runExceptT do + equation <- + Except.lift + (Declaration.prepareDefinitionEquationSpecWithEligibilityLowering + objects identity SearchIneligible alias) + >>= Except.liftEither + (extensional, descriptor) <- + Except.lift + (Declaration.prepareNamedSetConstructionSpecLowering + objects identity construction) + >>= Except.liftEither + pure + (checked + [ Declaration.checkedCandidate + equation + (Declaration.checkedDefinitionEquationPlanning + identity) + :| [ Declaration.checkedCandidate + extensional + (Declaration.checkedKernelPlanning + descriptor []) + ] + ] + (CheckedExactBindingConstruction + identity construction)) + Just (PreparedRelationalSetConstruction construction) -> + Except.runExceptT do + equation <- + Except.lift + (Declaration.prepareDefinitionEquationSpecWithEligibilityLowering + objects identity SearchIneligible alias) + >>= Except.liftEither + let functionality = + relationalSetConstructionClosedFunctionality + construction + functionalityScoped = + embedClosedCore [] functionality + functionalitySpec <- + Except.lift + (Declaration.prepareFrozenCandidateSpecLowering + objects functionality SearchIneligible []) + >>= Except.liftEither + obligation <- + Except.lift + (Declaration.prepareScopedVampireObligationLowering + Vector.empty + functionalityScoped + [] + [] + Declaration.VampireImplicitPremises) + >>= either + (Except.throwError + . Declaration.ProofObligationFailedAt location + . Declaration.CurrentCandidateVampirePreparationFailed) + pure + (extensional, descriptor) <- + Except.lift + (Declaration.prepareRelationalSetConstructionSpecLowering + objects identity construction functionality) + >>= Except.liftEither + pure + (checked + [ Declaration.checkedCandidate + equation + (Declaration.checkedDefinitionEquationPlanning + identity) + :| [ Declaration.checkedCandidate + functionalitySpec + (Declaration.checkedSourceProofPlanning + [Declaration.checkedPlannedVampireRequest + location obligation] + []) + ] + , Declaration.checkedCandidate + extensional + (Declaration.checkedStagedKernelPlanning + descriptor + [Declaration.plannedEarlierCandidate 0 1]) + :| [] + ] + (CheckedExactBindingRelationalConstruction + identity construction obligation)) + where + identity = preparedExactObjectId prepared + objects = maybeToList (preparedExactObject prepared) + location = preparedExactLocation prepared + checked stages body = + Declaration.checkedCompiledDeclaration + (preparedExactSyntaxId prepared) + objects + [] + [semanticGlobalBinding + (preparedExactGlobalKey prepared) + (preparedExactGlobalTarget prepared)] + [] + stages + body + +data CheckedExactBindingAuthorization + = CheckedExactBindingNone + | CheckedExactBindingDefinition !ObjectId + | CheckedExactBindingConstruction + !ObjectId + !(NamedSetConstruction ObjectId) + | CheckedExactBindingRelationalConstruction + !ObjectId + !(CheckedRelationalSetConstruction ObjectId) + !(Declaration.PreparedVampireObligation Void ()) + +authorizeCheckedExactBinding + :: CheckedExactBindingAuthorization + -> [NonEmpty Declaration.ReservedCandidate] + -> Declaration.Declaration () +authorizeCheckedExactBinding body stages = + case (body, stages) of + (CheckedExactBindingNone, []) -> pure () + (CheckedExactBindingDefinition identity, [candidate :| []]) -> + Declaration.authorizeDefinitionEquationCandidate + identity candidate + ( CheckedExactBindingConstruction identity construction + , [equation :| [extensional]] + ) -> do + Declaration.authorizeDefinitionEquationCandidate + identity equation + Declaration.authorizeNamedSetConstructionCandidate + identity construction extensional + ( CheckedExactBindingRelationalConstruction + identity construction obligation + , [equation :| [functionality], extensional :| []] + ) -> do + Declaration.authorizeDefinitionEquationCandidate + identity equation + Declaration.authorizeVampireCandidate + functionality + (Declaration.acceptPreparedVampireObligation obligation) + Declaration.authorizeRelationalSetConstructionCandidate + identity construction functionality extensional + _ -> + Declaration.failDeclaration + (Declaration.CheckedAuthorizationCandidateShapeMismatch + (case body of + CheckedExactBindingNone -> 0 + CheckedExactBindingDefinition{} -> 1 + CheckedExactBindingConstruction{} -> 1 + CheckedExactBindingRelationalConstruction{} -> 2) + (length stages)) + +prepareExactStructure + :: Raw.Block + -> [CanonicalLexicalEntry] + -> Declaration.LoweringDriver + (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.resolveVisibleStructureLowering 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.nextDeclarationSlotLowering + theory <- Except.lift Declaration.currentTheoryLowering + 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.objectAvailableLowering 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.resolveVisibleStructureLowering 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.objectTypeLowering identity) + case coreType of + Nothing -> + Except.throwError + (ExactStructureObjectNotVisible + (locate block) identity) + Just actual -> + pure (Map.insert identity actual types)) + localTypes + (Set.toAscList dependencies) + +lowerPreparedExactStructure + :: PreparedExactStructure + -> Declaration.LoweringDriver + (Either + Declaration.DeclarationError + (Declaration.CheckedDeclaration + CheckedExactStructureAuthorization)) +lowerPreparedExactStructure + (PreparedExactStructure + _location objects predicate descriptor alias generatedFacts syntax) = + Except.runExceptT do + definition <- + Except.lift + (Declaration.preparePointwiseDefinitionEquationSpecLowering + objects predicate alias) + >>= Except.liftEither + generatedCandidates <- + traverse + (\(PreparedExactStructureFact + factLocation target factAlias) -> do + generatedSpec <- Except.lift + (Declaration.prepareFrozenCandidateSpecLowering + objects target SearchEligible [factAlias]) + >>= Except.liftEither + obligation <- Except.lift + (Declaration.prepareStagedCandidateVampireLowering + factLocation objects definition generatedSpec) + >>= Except.liftEither + pure + ( Declaration.checkedCandidate generatedSpec + (Declaration.checkedSourceProofPlanning + [ Declaration.checkedPlannedVampireRequest + factLocation obligation + ] + [ Declaration.plannedEarlierCandidate 0 0 + ]) + , (factLocation, obligation) + )) + generatedFacts + let generatedAuthorizations = + snd <$> generatedCandidates + stages = + [ Declaration.checkedCandidate definition + (Declaration.checkedDefinitionEquationPlanning predicate) + :| [] + ] + <> maybeToList + (NonEmpty.nonEmpty + (fst <$> generatedCandidates)) + body = + CheckedExactStructureAuthorization + predicate + generatedAuthorizations + pure + (Declaration.checkedCompiledDeclaration + syntax objects [] [] [descriptor] stages + body) + +authorizeCheckedExactStructure + :: CheckedExactStructureAuthorization + -> [NonEmpty Declaration.ReservedCandidate] + -> Declaration.Declaration () +authorizeCheckedExactStructure + (CheckedExactStructureAuthorization predicate obligations) + stages = + case (obligations, stages) of + ([], [definition :| []]) -> + Declaration.authorizeDefinitionEquationCandidate + predicate definition + (_, [definition :| [], generatedCandidates]) + | length obligations == NonEmpty.length generatedCandidates -> do + Declaration.authorizeDefinitionEquationCandidate + predicate definition + Declaration.authorizeVampireCandidateBatch + (NonEmpty.zipWith + (\candidate (factLocation, obligation) -> + ( factLocation + , candidate + , do + void + (Declaration.useStagedCandidate + definition) + pure obligation + )) + generatedCandidates + (NonEmpty.fromList obligations)) + _ -> + Declaration.failDeclaration + (Declaration.CheckedAuthorizationCandidateShapeMismatch + (if null obligations then 1 else 2) + (length stages)) + +validateStructureOccurrences + :: Location + -> Raw.StructDefn + -> [CanonicalLexicalEntry] + -> ExceptT ExactCompileError (Declaration.LoweringDriver) () +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 + -> ExceptT + ExactCompileError + (Declaration.LoweringDriver) + ( PreparedHead + , ExactDeclarationFamily + , Maybe (Elaborate CompiledBody) + ) +prepareHead block key = + case block of + Raw.BlockSig location _title _marker assumptions signature -> do + rejectHeaderAssumptions ExactGuardedOpaqueSignature assumptions + head' <- prepareSignature location key signature + pure (head', ExactSignature, Nothing) + Raw.BlockAbbr location _title _marker abbreviation -> do + (head', buildBody) <- + prepareAbbreviation location key abbreviation + pure (head', ExactAbbreviation, Just buildBody) + Raw.BlockDefn location _title _marker definition -> do + (head', buildBody) <- + prepareDefinition location key definition + pure (head', ExactDefinition, Just buildBody) + _ -> + Except.throwError (ExactUnsupportedDeclaration (locate block)) + +prepareSignature + :: Location + -> SemanticGlobalKey + -> Raw.Signature + -> ExceptT + ExactCompileError + (Declaration.LoweringDriver) + PreparedHead +prepareSignature location key = \case + Raw.SignatureAdj subject (Raw.Adj _ item arguments) -> do + ensureAdjectiveKey location item key + makePreparedHead + location key (subject : arguments) TyProp + Raw.SignatureSymbolic (Raw.SymbolPattern symbol parameters) nounPhrase -> do + unless + ( key + == SemanticExpressionFunction + (Raw.mixfixPattern symbol) + ) + (Except.throwError (ExactDeclarationHeadMismatch location)) + unless + (exactSetNounPhrase nounPhrase) + (Except.throwError (ExactUnsupportedDeclarationBody location)) + makePreparedHead location key parameters TySet + _ -> + Except.throwError (ExactUnsupportedDeclaration location) + +prepareAbbreviation + :: Location + -> SemanticGlobalKey + -> Raw.Abbreviation + -> ExceptT + ExactCompileError + (Declaration.LoweringDriver) + ( PreparedHead + , Elaborate CompiledBody + ) +prepareAbbreviation location key = \case + Raw.AbbreviationEq (Raw.SymbolPattern symbol parameters) expression -> do + ensureExpressionKey location symbol key + makeContextualTransparentHead + location key parameters TySet + (ordinaryCompiledBody <$> compileExpressionAsSet expression) + Raw.AbbreviationFun (Raw.Fun _ item parameters) term -> do + ensureFunctionPhraseKey location item key + makeContextualTransparentHead + location key parameters TySet + (ordinaryCompiledBody <$> compileTermAsSet term) + Raw.AbbreviationAdj subject (Raw.Adj _ item arguments) statement -> do + ensureAdjectiveKey location item key + makeContextualTransparentHead + location key (subject : arguments) TyProp + (ordinaryCompiledBody <$> compileStatement statement) + Raw.AbbreviationVerb subject (Raw.Verb _ item arguments) statement -> do + ensureVerbKey location item key + makeContextualTransparentHead + location key (subject : arguments) TyProp + (ordinaryCompiledBody <$> compileStatement statement) + Raw.AbbreviationNoun subject (Raw.Noun _ item arguments) statement -> do + ensureNounKey location item key + makeContextualTransparentHead + location key (subject : arguments) TyProp + (ordinaryCompiledBody <$> compileStatement statement) + Raw.AbbreviationRel left relation parameters right statement -> do + ensureRelationKey location relation key + makeContextualTransparentHead + location key (parameters <> [left, right]) TyProp + (ordinaryCompiledBody <$> compileStatement statement) + +prepareDefinition + :: Location + -> SemanticGlobalKey + -> Raw.Defn + -> ExceptT + ExactCompileError + (Declaration.LoweringDriver) + ( PreparedHead + , Elaborate CompiledBody + ) +prepareDefinition location key = \case + Raw.Defn assumptions head' statement -> do + rejectHeaderAssumptions ExactGuardedTransparentDefinition assumptions + (parameters, resultType) <- + definitionHead location key head' + makeTransparentHead + location key parameters resultType + (ordinaryCompiledBody <$> compileStatement statement) + Raw.DefnFun assumptions (Raw.Fun _ item parameters) symbolic term -> do + rejectHeaderAssumptions ExactGuardedTransparentDefinition assumptions + traverse_ + (Except.throwError + . ExactDefinitionCombinedSymbolicAlias + . locate) + symbolic + ensureFunctionPhraseKey location item key + makeTransparentHead + location key parameters TySet + (compileNamedSetTerm term) + Raw.DefnOp (Raw.SymbolPattern symbol parameters) expression -> do + ensureExpressionKey location symbol key + makeTransparentHead + location key parameters TySet + (compileNamedSetExpression expression) + +definitionHead + :: Location + -> SemanticGlobalKey + -> Raw.DefnHead + -> ExceptT + ExactCompileError + (Declaration.LoweringDriver) + ([Raw.VarSymbol], CoreType) +definitionHead location key = \case + Raw.DefnAdj annotation subject (Raw.Adj _ item arguments) -> do + validateDefinitionAnnotation annotation + ensureAdjectiveKey location item key + pure (subject : arguments, TyProp) + Raw.DefnVerb annotation subject (Raw.Verb _ item arguments) -> do + validateDefinitionAnnotation annotation + ensureVerbKey location item key + pure (subject : arguments, TyProp) + Raw.DefnNoun subject (Raw.Noun _ item arguments) -> do + ensureNounKey location item key + pure (subject : arguments, TyProp) + Raw.DefnRel left relation parameters right -> do + ensureRelationKey location relation key + pure (parameters <> [left, right], TyProp) + Raw.DefnSymbolicPredicate + (Raw.PrefixPredicate command arity) + _marker + parameters -> do + unless + ( key + == SemanticPrefixPredicate + command + (fromIntegral arity) + ) + (Except.throwError (ExactDeclarationHeadMismatch location)) + pure (toList parameters, TyProp) + +validateDefinitionAnnotation + :: MonadError ExactCompileError monad + => Maybe (Raw.NounPhrase Maybe) + -> monad () +validateDefinitionAnnotation = traverse_ \nounPhrase -> + unless (exactSetNounPhrase nounPhrase) + (throwError + (ExactNonCanonicalSetDefinitionAnnotation + (exactNounPhraseLocation nounPhrase))) + +rejectHeaderAssumptions + :: MonadError ExactCompileError monad + => (Location -> ExactCompileError) + -> [Raw.Asm] + -> monad () +rejectHeaderAssumptions makeError = \case + [] -> pure () + assumption : _ -> + throwError (makeError (exactAssumptionLocation assumption)) + +exactAssumptionLocation :: Raw.Asm -> Location +exactAssumptionLocation = \case + Raw.AsmSuppose statement -> locate statement + Raw.AsmLetNoun variables _nounPhrase -> locate variables + Raw.AsmLetIn variables _expression -> locate variables + Raw.AsmLetThe variable _function -> locate variable + Raw.AsmLetEq variable _expression -> locate variable + Raw.AsmLetStruct variable _structure -> locate variable + +exactNounPhraseLocation :: Raw.NounPhraseOf t argument -> Location +exactNounPhraseLocation + (Raw.NounPhrase _left noun _variables _right _suchThat) = + locate noun + +makeTransparentHead + :: Location + -> SemanticGlobalKey + -> [Raw.VarSymbol] + -> CoreType + -> Elaborate CompiledBody + -> ExceptT + ExactCompileError + (Declaration.LoweringDriver) + ( PreparedHead + , Elaborate CompiledBody + ) +makeTransparentHead location key parameters resultType body = do + (prepared, binders) <- + prepareParameters location key parameters resultType + let close = do + State.modify' \state -> + state + { elaborationBinders = binders + , elaborationBinderDepth = + fromIntegral (length parameters) + } + CompiledBody body' construction <- body + pure + (CompiledBody + (foldr (const (CLam TySet)) body' parameters) + construction) + pure (prepared, close) + +makeContextualTransparentHead + :: Location + -> SemanticGlobalKey + -> [Raw.VarSymbol] + -> CoreType + -> Elaborate CompiledBody + -> ExceptT + ExactCompileError + (Declaration.LoweringDriver) + ( PreparedHead + , Elaborate CompiledBody + ) +makeContextualTransparentHead location key parameters resultType body = do + (prepared, binders) <- + prepareParameters location key parameters resultType + let close = do + State.modify' \state -> + state + { elaborationBinders = binders + , elaborationBinderDepth = + fromIntegral (length parameters) + 1 + , elaborationContextualBinder = + Just (fromIntegral (length parameters)) + } + CompiledBody body' _construction <- body + pure + (CompiledBody + (foldr (const (CLam TySet)) body' parameters) + Nothing) + pure (prepared, close) + +makePreparedHead + :: Location + -> SemanticGlobalKey + -> [Raw.VarSymbol] + -> CoreType + -> ExceptT + ExactCompileError + (Declaration.LoweringDriver) + PreparedHead +makePreparedHead location key parameters resultType = do + (prepared, _binders) <- + prepareParameters location key parameters resultType + pure prepared + +prepareParameters + :: Location + -> SemanticGlobalKey + -> [Raw.VarSymbol] + -> CoreType + -> ExceptT + ExactCompileError + (Declaration.LoweringDriver) + ( PreparedHead + , Map.Map Raw.VarSymbol Natural + ) +prepareParameters + location key parameters resultType = do + case firstDuplicate parameters of + Just duplicate -> + Except.throwError + (ExactDuplicateParameter location duplicate) + Nothing -> pure () + let indices = + reverse (take (length parameters) [0 ..]) + binders = + Map.fromList + (zip parameters indices) + coreType = foldr (const (TyArrow TySet)) resultType parameters + pure + ( PreparedHead key parameters coreType + , binders + ) + +compileExpressionAsSet + :: Raw.Expr + -> Elaborate (CanonicalTerm ObjectId) +compileExpressionAsSet expression = do + (term, actual) <- compileExpression expression + unless (actual == TySet) + (Except.throwError + (ExactExpressionExpectedSet (locate expression) actual)) + pure term + +-- | Compile one set expression once while retaining the checked-source shape +-- needed only when that expression is subsequently named by a definition. +-- Nested constructions remain ordinary exact terms. +compileNamedSetExpression + :: Raw.Expr + -> Elaborate CompiledBody +compileNamedSetExpression = \case + Raw.ExprSep _location variable bound predicate -> do + (term, bound', predicate') <- + compileSeparation variable bound predicate + pure + (CompiledBody term + (Just + (CompiledSeparationConstruction + bound' predicate'))) + Raw.ExprReplace _location value bounds condition -> do + replacement <- + compileFunctionalReplacement value bounds condition + pure + (CompiledBody + (compiledFunctionalReplacementTerm replacement) + (Just + (CompiledFunctionalReplacementConstruction + (compiledFunctionalReplacementDomains replacement) + (compiledFunctionalReplacementValue replacement) + (compiledFunctionalReplacementCondition replacement)))) + Raw.ExprReplacePred _location range domainVariable bound predicate -> do + (term, domain, relation) <- + compileRelationalReplacement + range domainVariable bound predicate + pure + (CompiledBody term + (Just + (CompiledRelationalReplacementConstruction + domain relation))) + expression -> + (`CompiledBody` Nothing) + <$> compileExpressionAsSet expression + +compileNamedSetTerm :: Raw.Term -> Elaborate CompiledBody +compileNamedSetTerm = \case + Raw.TermExpr expression -> compileNamedSetExpression expression + term -> ordinaryCompiledBody <$> compileTermAsSet term + +ordinaryCompiledBody :: CanonicalTerm ObjectId -> CompiledBody +ordinaryCompiledBody term = CompiledBody term Nothing + +compileTermAsSet + :: Raw.Term + -> Elaborate (CanonicalTerm ObjectId) +compileTermAsSet = \case + Raw.TermExpr expression -> + compileExpressionAsSet expression + Raw.TermFun (Raw.Fun location item arguments) -> do + let patterns = Raw.lexicalItemSgPlPattern item + key = SemanticFunctionPhrase (Raw.sg patterns) (Raw.pl patterns) + compiled <- traverse compileTermAsSet arguments + applyResolved location key compiled + Raw.TermQuantified _quantifier location _nounPhrase -> + Except.throwError + (ExactQuantifiedTermRequiresPropositionContext location) + term -> + Except.throwError + (ExactUnsupportedDeclarationBody (locate term)) + +-- | Compile a source term only at a proposition consumer. Indefinite terms +-- own the continuation, so their noun constraints and quantifier surround +-- exactly the proposition which consumes the resulting set. Function-phrase +-- arguments recurse through the same seam and therefore never masquerade as +-- independently set-valued terms. +compileTermInProposition + :: Raw.Term + -> (CanonicalTerm ObjectId + -> Elaborate (CanonicalTerm ObjectId)) + -> Elaborate (CanonicalTerm ObjectId) +compileTermInProposition term continuation = + case term of + Raw.TermExpr expression -> + compileExpressionAsSet expression >>= continuation + Raw.TermFun (Raw.Fun location item arguments) -> do + let patterns = Raw.lexicalItemSgPlPattern item + key = + SemanticFunctionPhrase + (Raw.sg patterns) + (Raw.pl patterns) + compileTermsInProposition arguments \compiled -> do + value <- applyResolved location key compiled + continuation value + Raw.TermQuantified quantifier _location nounPhrase -> + compileQuantifiedTermInProposition + quantifier nounPhrase continuation + Raw.TermIota location _variable _statement -> + Except.throwError (ExactUnsupportedDeclarationBody location) + +-- | Compile source-ordered proposition terms. The first source occurrence +-- receives the outermost continuation and therefore the widest scope. +compileTermsInProposition + :: [Raw.Term] + -> ([CanonicalTerm ObjectId] + -> Elaborate (CanonicalTerm ObjectId)) + -> Elaborate (CanonicalTerm ObjectId) +compileTermsInProposition terms continuation = + case terms of + [] -> continuation [] + term : remaining -> + compileTermInProposition term \compiled -> do + compiledDepth <- State.gets elaborationBinderDepth + compileTermsInProposition remaining \rest -> do + compiled' <- + weakenElaboratedTermFrom compiledDepth compiled + continuation (compiled' : rest) + +weakenElaboratedTermFrom + :: Natural + -> CanonicalTerm ObjectId + -> Elaborate (CanonicalTerm ObjectId) +weakenElaboratedTermFrom originalDepth term = do + currentDepth <- State.gets elaborationBinderDepth + when (currentDepth < originalDepth) + (impossible + "a proposition-term continuation escaped its binder scope") + pure + (shiftCanonical + (currentDepth - originalDepth) + 0 + term) + +compileExpression + :: Raw.Expr + -> Elaborate (CanonicalTerm ObjectId, CoreType) +compileExpression = \case + Raw.ExprVar variable -> do + binders <- State.gets elaborationBinders + case Map.lookup variable binders of + Just index -> + pure (CBound index, TySet) + Nothing -> + Except.throwError + (ExactFreeVariable (locate variable) variable) + Raw.ExprInteger _location integer -> + pure (COpaqueInteger (toInteger integer), TySet) + Raw.ExprOp location symbol arguments -> do + let key = + SemanticExpressionFunction + (Raw.mixfixPattern symbol) + compiled <- traverse compileExpression arguments + case fixedSemanticMeaning key of + Just (FixedIntrinsic intrinsic) -> + applyTyped + location + (CIntrinsic intrinsic) + (coreIntrinsicType intrinsic) + compiled + Just (FixedNegatedIntrinsic _intrinsic) -> + impossible + "expression key resolved to a negated intrinsic" + Just FixedEquality -> + impossible + "expression key resolved to fixed equality" + Just FixedDisequality -> + impossible + "expression key resolved to fixed disequality" + Nothing -> + applyResolvedTyped + location + key + compiled + Raw.ExprStructOp location symbol maybeArgument -> + compileStructureOperation location symbol maybeArgument + Raw.ExprFiniteSet _location elements -> do + compiled <- traverse compileExpressionAsSet elements + pure + ( foldr + canonicalSetInsert + (CIntrinsic Empty) + compiled + , TySet + ) + Raw.ExprSep _location variable bound predicate -> do + (term, _bound, _predicate) <- + compileSeparation variable bound predicate + pure (term, TySet) + Raw.ExprReplace _location value bounds condition -> do + replacement <- + compileFunctionalReplacement value bounds condition + pure (compiledFunctionalReplacementTerm replacement, TySet) + Raw.ExprReplacePred location _value _variable _bound _predicate -> + Except.throwError + (ExactRelationalReplacementRequiresNamedDefinition location) + +compileStructureOperation + :: Location + -> Raw.StructSymbol + -> Maybe Raw.Expr + -> Elaborate (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 ObjectId +resolveUniqueStructureOperation location symbol = do + objects <- + State.lift + (Except.lift + (Declaration.resolveVisibleStructureOperationObjectsLowering + symbol)) + case objects of + [] -> + Except.throwError + (ExactStructureOperationNotAvailable location symbol) + [object] -> pure object + _ -> + Except.throwError + (ExactStructureOperationAmbiguous location symbol objects) + +recordContextualRequirement + :: Location + -> Raw.StructSymbol + -> ObjectId + -> Elaborate () +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 (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 + +compileMembership + :: Location + -> Raw.Sign + -> CanonicalTerm ObjectId + -> CanonicalTerm ObjectId + -> Elaborate (CanonicalTerm ObjectId) +compileMembership location sign element set = do + checkedSet <- structureCarrierCast location set + let proposition = + CApp + (CApp (CIntrinsic Member) element) + checkedSet + pure case sign of + Raw.Positive -> proposition + Raw.Negative -> logicalNot proposition + +compileSeparation + :: Raw.VarSymbol + -> Raw.Expr + -> Raw.Stmt + -> Elaborate + ( CanonicalTerm ObjectId + , CanonicalTerm ObjectId + , CanonicalTerm ObjectId + ) +compileSeparation variable bound predicate = do + bound' <- compileExpressionAsSet bound + predicate' <- + withSetBinders (variable :| []) + (compileStatement predicate) + pure + ( CApp + (CApp (CIntrinsic Sep) bound') + (CLam TySet predicate') + , bound' + , predicate' + ) + +compileRelationalReplacement + :: Raw.VarSymbol + -> Raw.VarSymbol + -> Raw.Expr + -> Raw.Stmt + -> Elaborate + ( CanonicalTerm ObjectId + , CanonicalTerm ObjectId + , CanonicalTerm ObjectId + ) +compileRelationalReplacement range domainVariable bound predicate = do + domain <- compileExpressionAsSet bound + relation <- + withSetBinders (domainVariable :| [range]) + (compileStatement predicate) + let restrictedDomain = + CApp + (CApp (CIntrinsic Sep) domain) + (CLam TySet (logicalExists relation)) + choiceFunction = + CLam TySet + (CApp (CIntrinsic SetChoose) (CLam TySet relation)) + replacement = + CApp + (CApp (CIntrinsic Repl) restrictedDomain) + choiceFunction + pure (replacement, domain, relation) + +data CompiledFunctionalReplacement = CompiledFunctionalReplacement + !(CanonicalTerm ObjectId) + !(NonEmpty (CanonicalTerm ObjectId)) + !(CanonicalTerm ObjectId) + !(Maybe (CanonicalTerm ObjectId)) + +compiledFunctionalReplacementTerm + :: CompiledFunctionalReplacement + -> CanonicalTerm ObjectId +compiledFunctionalReplacementTerm + (CompiledFunctionalReplacement term _domains _value _condition) = + term + +compiledFunctionalReplacementDomains + :: CompiledFunctionalReplacement + -> NonEmpty (CanonicalTerm ObjectId) +compiledFunctionalReplacementDomains + (CompiledFunctionalReplacement _term domains _value _condition) = + domains + +compiledFunctionalReplacementValue + :: CompiledFunctionalReplacement + -> CanonicalTerm ObjectId +compiledFunctionalReplacementValue + (CompiledFunctionalReplacement _term _domains value _condition) = + value + +compiledFunctionalReplacementCondition + :: CompiledFunctionalReplacement + -> Maybe (CanonicalTerm ObjectId) +compiledFunctionalReplacementCondition + (CompiledFunctionalReplacement _term _domains _value condition) = + condition + +compileFunctionalReplacement + :: Raw.Expr + -> NonEmpty (Raw.VarSymbol, Raw.Expr) + -> Maybe Raw.Stmt + -> Elaborate CompiledFunctionalReplacement +compileFunctionalReplacement + value ((variable, domain) :| remaining) condition = do + domain' <- compileExpressionAsSet domain + case remaining of + [] -> do + (value', condition') <- + withSetBinders (variable :| []) do + value' <- compileExpressionAsSet value + condition' <- traverse compileStatement condition + pure (value', condition') + let filteredDomain = + case condition' of + Nothing -> domain' + Just predicate -> + CApp + (CApp (CIntrinsic Sep) domain') + (CLam TySet predicate) + pure + (CompiledFunctionalReplacement + (CApp + (CApp (CIntrinsic Repl) filteredDomain) + (CLam TySet value')) + (domain' :| []) + value' + condition') + next : rest -> do + nested <- + withSetBinders (variable :| []) + (compileFunctionalReplacement + value (next :| rest) condition) + pure + (CompiledFunctionalReplacement + (CApp + (CIntrinsic FamilyUnion) + (CApp + (CApp (CIntrinsic Repl) domain') + (CLam TySet + (compiledFunctionalReplacementTerm nested)))) + (domain' + NonEmpty.<| + compiledFunctionalReplacementDomains nested) + (compiledFunctionalReplacementValue nested) + (compiledFunctionalReplacementCondition nested)) + +compileStatement + :: Raw.Stmt + -> Elaborate (CanonicalTerm ObjectId) +compileStatement = \case + Raw.StmtFormula formula -> + compileFormula formula + Raw.StmtVerbPhrase terms verbPhrase -> + compileTermsInProposition (toList terms) \subjects -> + logicalConjunction + <$> traverse (`compileVerbPhrase` verbPhrase) subjects + Raw.StmtNoun terms nounPhrase -> + compileTermsInProposition (toList terms) \subjects -> + logicalConjunction + <$> traverse (`compileNounPhraseMaybe` nounPhrase) subjects + Raw.StmtExists _location nounPhrase -> + compileExistentialNounPhrase nounPhrase + Raw.StmtQuantPhrase + _location + (Raw.QuantPhrase quantifier nounPhrase) + statement -> + compileQuantifiedNounPhrase quantifier nounPhrase statement + Raw.StmtConnected connective location left right -> + compileConnective + (fromMaybe (locate left) location) + connective + compileStatement + left + right + Raw.StmtNeg _location statement -> + logicalNot <$> compileStatement statement + Raw.SymbolicQuantified + _location quantifier variables bound suchThat statement -> + compileSymbolicQuantified + quantifier variables bound suchThat (compileStatement statement) + Raw.StmtStruct term rawPhrase -> + compileTermInProposition term \subject -> do + 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) + +compileQuantifiedTermInProposition + :: Raw.Quantifier + -> Raw.NounPhrase Maybe + -> (CanonicalTerm ObjectId + -> Elaborate (CanonicalTerm ObjectId)) + -> Elaborate (CanonicalTerm ObjectId) +compileQuantifiedTermInProposition quantifier + (Raw.NounPhrase left noun named right suchThat) + compileBody = + case named of + Nothing -> + withAnonymousSetBinder compileFor + Just variable -> + withSetBinders (variable :| []) do + subject <- compileIntroducedVariable variable + compileFor subject + where + compileFor subject = do + constraints <- + compileNounPhraseConstraints + [subject] left noun right suchThat + body <- compileBody subject + pure (quantifyNounPhrase quantifier 1 constraints body) + +compileSymbolicQuantified + :: Raw.Quantifier + -> NonEmpty Raw.VarSymbol + -> Raw.Bound + -> Maybe Raw.Stmt + -> Elaborate (CanonicalTerm ObjectId) + -> Elaborate (CanonicalTerm ObjectId) +compileSymbolicQuantified quantifier variables bound suchThat compileBody = + withSetBinders variables do + boundConstraints <- + compileSymbolicBoundConstraintList variables bound + suchThatConstraints <- + maybeToList <$> traverse compileStatement suchThat + body <- compileBody + pure + (quantifyNounPhrase + quantifier + (length (toList variables)) + (logicalConjunction + (boundConstraints <> suchThatConstraints)) + body) + +compileSymbolicBoundConstraintList + :: NonEmpty Raw.VarSymbol + -> Raw.Bound + -> Elaborate [CanonicalTerm ObjectId] +compileSymbolicBoundConstraintList variables = \case + Raw.Unbounded -> + pure [] + Raw.Bounded _location sign relation domain -> do + subjects <- traverse compileIntroducedVariable variables + domain' <- compileExpressionAsSet domain + traverse + (\subject -> do + proposition <- + compileAtomicRelationTerms subject relation domain' + pure case sign of + Raw.Positive -> proposition + Raw.Negative -> logicalNot proposition) + (toList subjects) + +compileAtomicRelationTerms + :: CanonicalTerm ObjectId + -> Raw.Relation + -> CanonicalTerm ObjectId + -> Elaborate (CanonicalTerm ObjectId) +compileAtomicRelationTerms left relation right = + case relation of + Raw.Relation location symbol parameters -> do + let key = + SemanticRelation + (Raw.relationSymbolToken symbol) + (Raw.relationSymbolParameterArity symbol) + compiledParameters <- traverse compileExpressionAsSet parameters + case fixedSemanticMeaning key of + Just FixedEquality + | null parameters -> pure (CEq TySet left right) + Just FixedDisequality + | null parameters -> + pure (logicalNot (CEq TySet left right)) + Just (FixedIntrinsic Member) + | null parameters -> + compileMembership location Raw.Positive left right + Just (FixedNegatedIntrinsic Member) + | null parameters -> + compileMembership location Raw.Negative left right + Just (FixedIntrinsic intrinsic) -> do + (term, actual) <- + applyTyped + location + (CIntrinsic intrinsic) + (coreIntrinsicType intrinsic) + ((\term -> (term, TySet)) + <$> (compiledParameters <> [left, right])) + unless (actual == TyProp) + (Except.throwError + (ExactFormulaExpectedProposition location actual)) + pure term + Just (FixedNegatedIntrinsic intrinsic) -> do + (term, actual) <- + applyTyped + location + (CIntrinsic intrinsic) + (coreIntrinsicType intrinsic) + ((\term -> (term, TySet)) + <$> (compiledParameters <> [left, right])) + unless (actual == TyProp) + (Except.throwError + (ExactFormulaExpectedProposition location actual)) + pure (logicalNot term) + _ -> do + (term, actual) <- + applyResolvedTyped + location key + ((\term -> (term, TySet)) + <$> (compiledParameters <> [left, right])) + unless (actual == TyProp) + (Except.throwError + (ExactFormulaExpectedProposition location actual)) + pure term + Raw.RelationExpr location expression -> + compileRelationExpression location expression left right + +compileVerbPhrase + :: CanonicalTerm ObjectId + -> Raw.VerbPhrase + -> Elaborate (CanonicalTerm ObjectId) +compileVerbPhrase subject = \case + Raw.VPVerb verb -> + compileVerb subject verb + Raw.VPVerbNot verb -> + logicalNot <$> compileVerb subject verb + Raw.VPAdj adjectives -> + logicalConjunction + <$> traverse (compileAdjective subject) adjectives + Raw.VPAdjNot adjectives -> + logicalNot . logicalConjunction + <$> traverse (compileAdjective subject) adjectives + +compilePredicateArguments + :: CanonicalTerm ObjectId + -> [Raw.Term] + -> ( CanonicalTerm ObjectId + -> [CanonicalTerm ObjectId] + -> Elaborate (CanonicalTerm ObjectId) + ) + -> Elaborate (CanonicalTerm ObjectId) +compilePredicateArguments subject arguments continuation = do + subjectDepth <- State.gets elaborationBinderDepth + compileTermsInProposition arguments \compiled -> do + subject' <- weakenElaboratedTermFrom subjectDepth subject + continuation subject' compiled + +compileVerb + :: CanonicalTerm ObjectId + -> Raw.Verb + -> Elaborate (CanonicalTerm ObjectId) +compileVerb subject (Raw.Verb location item arguments) = do + let patterns = Raw.lexicalItemSgPlPattern item + compilePredicateArguments subject arguments \subject' compiled -> + applyResolvedPredicate + location + (SemanticVerb (Raw.sg patterns) (Raw.pl patterns)) + (subject' : compiled) + +compileAdjective + :: CanonicalTerm ObjectId + -> Raw.Adj + -> Elaborate (CanonicalTerm ObjectId) +compileAdjective subject (Raw.Adj location item arguments) = + compilePredicateArguments subject arguments \subject' compiled -> + applyResolvedPredicateChoice + location + ( SemanticRightAdjective (Raw.lexicalItemPattern item) + :| [SemanticLeftAdjective (Raw.lexicalItemPattern item)] + ) + (subject' : compiled) + +compileLeftAdjective + :: CanonicalTerm ObjectId + -> Raw.AdjL + -> Elaborate (CanonicalTerm ObjectId) +compileLeftAdjective subject (Raw.AdjL location item arguments) = + compilePredicateArguments subject arguments \subject' compiled -> + applyResolvedPredicate + location + (SemanticLeftAdjective (Raw.lexicalItemPattern item)) + (subject' : compiled) + +compileRightAttribute + :: CanonicalTerm ObjectId + -> Raw.AdjR + -> Elaborate (CanonicalTerm ObjectId) +compileRightAttribute subject = \case + Raw.AdjR location item arguments -> + compilePredicateArguments subject arguments \subject' compiled -> + applyResolvedPredicate + location + (SemanticRightAdjective (Raw.lexicalItemPattern item)) + (subject' : compiled) + Raw.AttrRThat verbPhrase -> + compileVerbPhrase subject verbPhrase + +compileNoun + :: CanonicalTerm ObjectId + -> Raw.Noun + -> Elaborate (CanonicalTerm ObjectId) +compileNoun subject (Raw.Noun location item arguments) + | Lexicon.isBuiltinSetNoun item = + pure logicalTruth + | otherwise = do + let patterns = Raw.lexicalItemSgPlPattern item + key = SemanticNoun (Raw.sg patterns) (Raw.pl patterns) + compilePredicateArguments subject arguments \subject' compiled -> + case fixedSemanticMeaning key of + Just (FixedIntrinsic Member) -> + case compiled of + [set] -> + compileMembership + location Raw.Positive subject' set + _ -> + impossible + "the fixed element noun does not have one argument" + Just (FixedIntrinsic intrinsic) -> do + (term, actual) <- + applyTyped + location + (CIntrinsic intrinsic) + (coreIntrinsicType intrinsic) + ((\argument -> (argument, TySet)) + <$> (subject' : compiled)) + unless (actual == TyProp) + (Except.throwError + (ExactFormulaExpectedProposition location actual)) + pure term + Just{} -> + impossible "a fixed noun is not a predicate intrinsic" + Nothing -> + applyResolvedPredicate + location key (subject' : compiled) + +compileNounPhraseConstraints + :: [CanonicalTerm ObjectId] + -> [Raw.AdjL] + -> Raw.Noun + -> [Raw.AdjR] + -> Maybe Raw.Stmt + -> Elaborate (CanonicalTerm ObjectId) +compileNounPhraseConstraints subjects left noun right suchThat = do + nounConstraints <- traverse (`compileNoun` noun) subjects + leftConstraints <- concat + <$> traverse + (\subject -> traverse (compileLeftAdjective subject) left) + subjects + rightConstraints <- concat + <$> traverse + (\subject -> traverse (compileRightAttribute subject) right) + subjects + suchThatConstraint <- traverse compileStatement suchThat + pure + (logicalConjunction + ( nounConstraints + <> leftConstraints + <> rightConstraints + <> maybeToList suchThatConstraint + )) + +compileNounPhraseMaybe + :: CanonicalTerm ObjectId + -> Raw.NounPhrase Maybe + -> Elaborate (CanonicalTerm ObjectId) +compileNounPhraseMaybe subject + (Raw.NounPhrase left noun named right suchThat) = + case named of + Nothing -> + compileNounPhraseConstraints + [subject] left noun right suchThat + Just variable -> do + abstracted <- + withSetBinders (variable :| []) + (compileNounPhraseConstraints + [CBound 0] left noun right suchThat) + pure (instantiateCanonical subject abstracted) + +compileExistentialNounPhrase + :: Raw.NounPhrase [] + -> Elaborate (CanonicalTerm ObjectId) +compileExistentialNounPhrase + (Raw.NounPhrase left noun variables right suchThat) = + case NonEmpty.nonEmpty variables of + Just binders -> + withSetBinders binders do + subjects <- traverse compileIntroducedVariable binders + constraints <- + compileNounPhraseConstraints + (toList subjects) left noun right suchThat + pure + (foldr + (const logicalExists) + constraints + binders) + Nothing -> + withAnonymousSetBinder \subject -> + logicalExists + <$> compileNounPhraseConstraints + [subject] left noun right suchThat + +compileQuantifiedNounPhrase + :: Raw.Quantifier + -> Raw.NounPhrase [] + -> Raw.Stmt + -> Elaborate (CanonicalTerm ObjectId) +compileQuantifiedNounPhrase quantifier + (Raw.NounPhrase left noun variables right suchThat) + statement = + case NonEmpty.nonEmpty variables of + Just binders -> + withSetBinders binders do + subjects <- traverse compileIntroducedVariable binders + constraints <- + compileNounPhraseConstraints + (toList subjects) left noun right suchThat + body <- compileStatement statement + pure + (quantifyNounPhrase + quantifier + (length (toList binders)) + constraints + body) + Nothing -> + withAnonymousSetBinder \subject -> do + constraints <- + compileNounPhraseConstraints + [subject] left noun right suchThat + body <- compileStatement statement + pure (quantifyNounPhrase quantifier 1 constraints body) + +quantifyNounPhrase + :: Raw.Quantifier + -> Int + -> CanonicalTerm ObjectId + -> CanonicalTerm ObjectId + -> CanonicalTerm ObjectId +quantifyNounPhrase quantifier binderCount constraints body = + case quantifier of + Raw.Universally -> + quantify + (if constraints == logicalTruth + then body + else CImp constraints body) + Raw.Existentially -> + quantify + (if constraints == logicalTruth + then body + else logicalAnd constraints body) + Raw.Nonexistentially -> + logicalNot + (quantify + (if constraints == logicalTruth + then body + else logicalAnd constraints body)) + where + quantify scoped = + foldr (const binder) scoped [1 .. binderCount] + binder = case quantifier of + Raw.Universally -> CForall TySet + Raw.Existentially -> logicalExists + Raw.Nonexistentially -> logicalExists + +withAnonymousSetBinder + :: (CanonicalTerm ObjectId -> Elaborate value) + -> Elaborate value +withAnonymousSetBinder action = do + outer <- State.gets elaborationBinders + outerDepth <- State.gets elaborationBinderDepth + outerStructures <- State.gets elaborationStructures + outerContextual <- State.gets elaborationContextualBinder + State.modify' \state -> + state + { elaborationBinders = (+ 1) <$> outer + , elaborationBinderDepth = outerDepth + 1 + , elaborationStructures = + Map.mapKeysMonotonic (+ 1) outerStructures + , elaborationContextualBinder = (+ 1) <$> outerContextual + } + result <- action (CBound 0) + State.modify' \state -> + state + { elaborationBinders = outer + , elaborationBinderDepth = outerDepth + , elaborationStructures = outerStructures + , elaborationContextualBinder = outerContextual + } + pure result + +withSetBinders + :: NonEmpty Raw.VarSymbol + -> Elaborate value + -> Elaborate value +withSetBinders variables action = do + outer <- State.gets elaborationBinders + outerDepth <- State.gets elaborationBinderDepth + outerStructures <- State.gets elaborationStructures + outerContextual <- State.gets elaborationContextualBinder + case firstDuplicate (toList variables) of + Just duplicate -> + Except.throwError + (ExactDuplicateLocalBinder + (locate duplicate) + duplicate) + Nothing -> pure () + case find (`Map.member` outer) (toList variables) of + Just shadowed -> + Except.throwError + (ExactDuplicateLocalBinder + (locate shadowed) + shadowed) + Nothing -> pure () + let binderCount = fromIntegral (length (toList variables)) + shifted = (+ binderCount) <$> outer + introduced = + Map.fromList + (zip + (toList variables) + (reverse [0 .. binderCount - 1])) + State.modify' \state -> + state + { elaborationBinders = introduced <> shifted + , elaborationBinderDepth = outerDepth + binderCount + , elaborationStructures = + Map.mapKeysMonotonic (+ binderCount) outerStructures + , elaborationContextualBinder = + (+ binderCount) <$> outerContextual + } + result <- action + State.modify' \state -> + state + { elaborationBinders = outer + , elaborationBinderDepth = outerDepth + , elaborationStructures = outerStructures + , elaborationContextualBinder = outerContextual + } + pure result + +compileFormula + :: Raw.Formula + -> Elaborate (CanonicalTerm ObjectId) +compileFormula = \case + Raw.FormulaChain chain -> + compileRelationChain chain + Raw.PropositionalConstant _ Raw.IsBottom -> + pure CFalsum + Raw.PropositionalConstant _ Raw.IsTop -> + pure (CImp CFalsum CFalsum) + Raw.FormulaNeg _ formula -> + logicalNot <$> compileFormula formula + Raw.FormulaPredicate + location + (Raw.PrefixPredicate command arity) + _marker + arguments -> do + compiled <- traverse compileExpression arguments + (term, actual) <- + applyResolvedTyped + location + (SemanticPrefixPredicate + command + (fromIntegral arity)) + (toList compiled) + unless (actual == TyProp) + (Except.throwError + (ExactFormulaExpectedProposition location actual)) + pure term + Raw.Connected location connective left right -> + compileConnective + location + connective + compileFormula + left + right + Raw.FormulaQuantified + _location quantifier variables bound formula -> + compileSymbolicQuantified + quantifier variables bound Nothing (compileFormula formula) +compileConnective + :: Location + -> Raw.Connective + -> (input -> Elaborate (CanonicalTerm ObjectId)) + -> input + -> input + -> Elaborate (CanonicalTerm ObjectId) +compileConnective _location connective compile left right = do + left' <- compile left + right' <- compile right + case connective of + Raw.Conjunction -> + pure (logicalAnd left' right') + Raw.Disjunction -> + pure (logicalOr left' right') + Raw.Implication -> + pure (CImp left' right') + Raw.Equivalence -> + pure (CEq TyProp left' right') + Raw.ExclusiveOr -> + pure + (logicalAnd + (logicalOr left' right') + (logicalNot (logicalAnd left' right'))) + Raw.NegatedDisjunction -> + pure (logicalNot (logicalOr left' right')) + +logicalAnd + :: CanonicalTerm global + -> CanonicalTerm global + -> CanonicalTerm global +logicalAnd left right = + logicalNot (CImp left (logicalNot right)) + +logicalTruth :: CanonicalTerm global +logicalTruth = + CImp CFalsum CFalsum + +logicalConjunction + :: (Foldable collection, Eq global) + => collection (CanonicalTerm global) + -> CanonicalTerm global +logicalConjunction = + foldr combine logicalTruth + where + combine proposition remaining + | proposition == logicalTruth = remaining + | remaining == logicalTruth = proposition + | otherwise = logicalAnd proposition remaining + +logicalOr + :: CanonicalTerm global + -> CanonicalTerm global + -> CanonicalTerm global +logicalOr left right = + CImp (logicalNot left) right + +logicalExists + :: CanonicalTerm global + -> CanonicalTerm global +logicalExists body = + logicalNot (CForall TySet (logicalNot body)) + +compileAtomicRelation + :: NonEmpty Raw.Expr + -> Raw.Relation + -> NonEmpty Raw.Expr + -> Elaborate (CanonicalTerm ObjectId) +compileAtomicRelation left relation right = + case (toList left, relation, toList right) of + ([leftExpression], Raw.Relation location symbol parameters, [rightExpression]) -> do + let key = + SemanticRelation + (Raw.relationSymbolToken symbol) + (Raw.relationSymbolParameterArity symbol) + case fixedSemanticMeaning key of + Just FixedEquality + | null parameters -> do + left' <- compileExpressionAsSet leftExpression + right' <- compileExpressionAsSet rightExpression + pure (CEq TySet left' right') + | otherwise -> + Except.throwError + (ExactUnsupportedDeclarationBody location) + Just FixedDisequality + | null parameters -> do + left' <- compileExpressionAsSet leftExpression + right' <- compileExpressionAsSet rightExpression + pure (logicalNot (CEq TySet left' right')) + | otherwise -> + Except.throwError + (ExactUnsupportedDeclarationBody location) + Just (FixedIntrinsic Member) + | null parameters -> do + left' <- compileExpressionAsSet leftExpression + right' <- compileExpressionAsSet rightExpression + compileMembership + location Raw.Positive left' right' + Just (FixedNegatedIntrinsic Member) + | null parameters -> do + left' <- compileExpressionAsSet leftExpression + right' <- compileExpressionAsSet rightExpression + compileMembership + location Raw.Negative left' right' + Just (FixedIntrinsic intrinsic) -> do + compiled <- traverse compileExpression + (parameters <> [leftExpression, rightExpression]) + (term, actual) <- + applyTyped + location + (CIntrinsic intrinsic) + (coreIntrinsicType intrinsic) + compiled + unless (actual == TyProp) + (Except.throwError + (ExactFormulaExpectedProposition location actual)) + pure term + Just (FixedNegatedIntrinsic intrinsic) -> do + compiled <- traverse compileExpression + (parameters <> [leftExpression, rightExpression]) + (term, actual) <- + applyTyped + location + (CIntrinsic intrinsic) + (coreIntrinsicType intrinsic) + compiled + unless (actual == TyProp) + (Except.throwError + (ExactFormulaExpectedProposition location actual)) + pure (logicalNot term) + Nothing -> do + compiled <- traverse compileExpression + (parameters <> [leftExpression, rightExpression]) + (term, actual) <- + applyResolvedTyped location key compiled + unless (actual == TyProp) + (Except.throwError + (ExactFormulaExpectedProposition location actual)) + pure term + ([leftExpression], Raw.RelationExpr location expression, [rightExpression]) -> do + left' <- compileExpressionAsSet leftExpression + right' <- compileExpressionAsSet rightExpression + compileRelationExpression location expression left' right' + _ -> + Except.throwError + (ExactUnsupportedDeclarationBody (locate relation)) + +compileRelationExpression + :: Location + -> Raw.Expr + -> CanonicalTerm ObjectId + -> CanonicalTerm ObjectId + -> Elaborate (CanonicalTerm ObjectId) +compileRelationExpression location expression left right = do + relation <- compileExpressionAsSet expression + pair <- + applyResolved + location + (SemanticExpressionFunction + (Raw.mixfixPattern Raw.PairSymbol)) + [left, right] + compileMembership location Raw.Positive pair relation + +compileRelationChain + :: Raw.Chain + -> Elaborate (CanonicalTerm ObjectId) +compileRelationChain chain = + logicalConjunction <$> traverse compileLink (chainLinks chain) + where + compileLink (sign, relation, left, right) = do + proposition <- + compileAtomicRelation + (left :| []) relation (right :| []) + pure case sign of + Raw.Positive -> proposition + Raw.Negative -> logicalNot proposition + + chainLinks = \case + Raw.ChainBase left sign relation right -> + [ (sign, relation, leftExpression, rightExpression) + | leftExpression <- toList left + , rightExpression <- toList right + ] + Raw.ChainCons left sign relation rest -> + let firstRight = chainFirstLeft rest + in + [ (sign, relation, leftExpression, rightExpression) + | leftExpression <- toList left + , rightExpression <- toList firstRight + ] + <> chainLinks rest + + chainFirstLeft = \case + Raw.ChainBase left _sign _relation _right -> left + Raw.ChainCons left _sign _relation _rest -> left + +applyResolved + :: Location + -> SemanticGlobalKey + -> [CanonicalTerm ObjectId] + -> Elaborate (CanonicalTerm ObjectId) +applyResolved location key arguments = do + (term, actual) <- + applyResolvedTyped + location key ((\argument -> (argument, TySet)) <$> arguments) + unless (actual == TySet) + (Except.throwError + (ExactExpressionExpectedSet location actual)) + pure term + +applyResolvedPredicate + :: Location + -> SemanticGlobalKey + -> [CanonicalTerm ObjectId] + -> Elaborate (CanonicalTerm ObjectId) +applyResolvedPredicate location key = + applyResolvedPredicateChoice location (key :| []) + +applyResolvedPredicateChoice + :: Location + -> NonEmpty SemanticGlobalKey + -> [CanonicalTerm ObjectId] + -> Elaborate (CanonicalTerm ObjectId) +applyResolvedPredicateChoice location keys arguments = do + case firstFixedMeaning (toList keys) of + Just meaning -> + maybe + (impossible + "a fixed equality predicate has an invalid source arity") + pure + (lowerFixedEqualityPredicate meaning arguments) + Nothing -> do + visible <- for (toList keys) \key -> do + found <- + State.lift + (Except.lift + (Declaration.resolveVisibleGlobalLowering key)) + pure ((\target -> (key, target)) <$> found) + case catMaybes visible of + [(key, _target)] -> do + (term, actual) <- + applyResolvedTyped + location key + ((\argument -> (argument, TySet)) <$> arguments) + unless (actual == TyProp) + (Except.throwError + (ExactFormulaExpectedProposition location actual)) + pure term + [] -> + Except.throwError + (ExactGlobalNotVisible location (NonEmpty.head keys)) + _ -> + impossible + "one adjective surface resolves to several exact globals" + where + firstFixedMeaning = + foldr + (\key found -> fixedSemanticMeaning key <|> found) + Nothing + +applyResolvedTyped + :: Location + -> SemanticGlobalKey + -> [(CanonicalTerm ObjectId, CoreType)] + -> Elaborate (CanonicalTerm ObjectId, CoreType) +applyResolvedTyped location key arguments = do + visible <- + State.lift + (Except.lift + (Declaration.resolveVisibleGlobalContentLowering key)) + (target, content, dependencies) <- + maybe + (Except.throwError (ExactGlobalNotVisible location key)) + pure + visible + case target of + GlobalReference identity -> do + let coreType = objectContentType content + State.modify' \state -> + state + { elaborationGlobals = + Map.insert + identity coreType + (elaborationGlobals state) + } + applyTyped location (CGlobal identity) coreType arguments + TransparentExpansion _identity -> + case content of + TransparentObjectContent _theory coreType body -> do + State.modify' \state -> + state + { elaborationGlobals = + Map.union + dependencies + (elaborationGlobals state) + } + applyExpandedTyped + location body coreType arguments + _ -> + 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 (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 + -> CanonicalTerm ObjectId + -> CoreType + -> [(CanonicalTerm ObjectId, CoreType)] + -> Elaborate (CanonicalTerm ObjectId, CoreType) +applyExpandedTyped location body coreType arguments = + foldM step (body, coreType) arguments + where + step (current, currentType) (argument, argumentType) = + case currentType of + TyArrow expected result + | expected == argumentType -> + pure + ( case current of + CLam binderType lambdaBody + | binderType == expected -> + instantiateCanonical + argument lambdaBody + _ -> CApp current argument + , result + ) + | otherwise -> + Except.throwError + (ExactApplicationArgumentMismatch + location expected argumentType) + actual -> + Except.throwError + (ExactApplicationExpectedFunction location actual) + +applyTyped + :: Location + -> CanonicalTerm ObjectId + -> CoreType + -> [(CanonicalTerm ObjectId, CoreType)] + -> Elaborate (CanonicalTerm ObjectId, CoreType) +applyTyped location function functionType arguments = + foldM step (function, functionType) arguments + where + step (currentFunction, currentType) (argument, argumentType) = + case currentType of + TyArrow expected result + | expected == argumentType -> + pure (CApp currentFunction argument, result) + | otherwise -> + Except.throwError + (ExactApplicationArgumentMismatch + location expected argumentType) + actual -> + Except.throwError + (ExactApplicationExpectedFunction location actual) + +logicalNot :: CanonicalTerm global -> CanonicalTerm global +logicalNot proposition = + CImp proposition CFalsum + +ensureExpressionKey + :: MonadError ExactCompileError monad + => Location + -> Raw.FunctionSymbol + -> SemanticGlobalKey + -> monad () +ensureExpressionKey location symbol key = + unless + (key == SemanticExpressionFunction (Raw.mixfixPattern symbol)) + (throwError (ExactDeclarationHeadMismatch location)) + +ensureAdjectiveKey + :: MonadError ExactCompileError monad + => Location + -> Raw.LexicalItem + -> SemanticGlobalKey + -> monad () +ensureAdjectiveKey location item key = + unless + ( key == SemanticLeftAdjective (Raw.lexicalItemPattern item) + || key == SemanticRightAdjective (Raw.lexicalItemPattern item) + ) + (throwError (ExactDeclarationHeadMismatch location)) + +ensureFunctionPhraseKey + :: MonadError ExactCompileError monad + => Location + -> Raw.LexicalItemSgPl + -> SemanticGlobalKey + -> monad () +ensureFunctionPhraseKey location item key = + let patterns = Raw.lexicalItemSgPlPattern item + in unless + (key == SemanticFunctionPhrase (Raw.sg patterns) (Raw.pl patterns)) + (throwError (ExactDeclarationHeadMismatch location)) + +ensureNounKey + :: MonadError ExactCompileError monad + => Location + -> Raw.LexicalItemSgPl + -> SemanticGlobalKey + -> monad () +ensureNounKey location item key = + let patterns = Raw.lexicalItemSgPlPattern item + in unless + (key == SemanticNoun (Raw.sg patterns) (Raw.pl patterns)) + (throwError (ExactDeclarationHeadMismatch location)) + +ensureVerbKey + :: MonadError ExactCompileError monad + => Location + -> Raw.LexicalItemSgPl + -> SemanticGlobalKey + -> monad () +ensureVerbKey location item key = + let patterns = Raw.lexicalItemSgPlPattern item + in unless + (key == SemanticVerb (Raw.sg patterns) (Raw.pl patterns)) + (throwError (ExactDeclarationHeadMismatch location)) + +ensureRelationKey + :: MonadError ExactCompileError monad + => Location + -> Raw.RelationSymbol + -> SemanticGlobalKey + -> monad () +ensureRelationKey location relation key = + unless + ( key + == SemanticRelation + (Raw.relationSymbolToken relation) + (Raw.relationSymbolParameterArity relation) + ) + (throwError (ExactDeclarationHeadMismatch location)) + +exactSetNounPhrase :: Raw.NounPhrase Maybe -> Bool +exactSetNounPhrase = \case + Raw.NounPhrase + [] + (Raw.Noun _ item []) + Nothing + [] + Nothing -> + Lexicon.isBuiltinSetNoun item + _ -> False + +encodePreparedSyntax + :: ExactDeclarationFamily + -> PreparedHead + -> PreparedBody + -> Maybe SemanticName + -> ByteString +encodePreparedSyntax + family (PreparedHead key _parameters coreType) body alias = + encodeCache do + putCacheTag case family of + ExactSignature -> 0x00 + ExactAbbreviation -> 0x01 + ExactDefinition -> 0x02 + putSemanticGlobalKeyCache key + putCoreTypeCache coreType + case body of + OpaqueBody -> putCacheTag 0x00 + TransparentBody canonical _construction -> 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 + +encodePreparedSourceAxiom + :: ScopedCheckedCore ObjectId + -> SemanticName + -> ByteString +encodePreparedSourceAxiom proposition alias = + encodeCache do + putCacheTag 0x03 + putCanonicalTermCache putObjectIdCache + (scopedCoreTerm proposition) + putCacheText (semanticNameText alias) + +definitionAlias :: Raw.Block -> Maybe SemanticName +definitionAlias = \case + Raw.BlockDefn _location _title (Raw.Marker marker) _definition -> + Just (semanticName marker) + _ -> Nothing + +firstDuplicate :: Ord value => [value] -> Maybe value +firstDuplicate = + go Set.empty + where + go _seen [] = Nothing + go seen (value : rest) + | value `Set.member` seen = Just value + | otherwise = go (Set.insert value seen) rest |