diff options
Diffstat (limited to 'source/Checking/Exact.hs')
| -rw-r--r-- | source/Checking/Exact.hs | 3936 |
1 files changed, 0 insertions, 3936 deletions
diff --git a/source/Checking/Exact.hs b/source/Checking/Exact.hs deleted file mode 100644 index 47e3859..0000000 --- a/source/Checking/Exact.hs +++ /dev/null @@ -1,3936 +0,0 @@ -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE NoImplicitPrelude #-} - --- | Direct compiler for the first exact monomorphic declaration family. -module 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 Checking.Core -import Checking.Declaration qualified as Declaration -import Checking.Exact.Vocabulary -import Checking.Identity -import Checking.SetConstruction -import Checking.Semantic -import Felix.Cache.Codec -import Felix.Module -import Report.Location -import Syntax.Abstract qualified as Raw -import Syntax.Interface (CanonicalLexicalEntry(..)) -import 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 |