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