diff options
Diffstat (limited to 'source/Checking/Exact.hs')
| -rw-r--r-- | source/Checking/Exact.hs | 299 |
1 files changed, 220 insertions, 79 deletions
diff --git a/source/Checking/Exact.hs b/source/Checking/Exact.hs index d0278f5..1788224 100644 --- a/source/Checking/Exact.hs +++ b/source/Checking/Exact.hs @@ -9,11 +9,15 @@ module Checking.Exact , ExactBinderContext , emptyExactBinderContext , extendExactBinderContext + , extendExactAnonymousBinderContext , exactBinderContextSupport , exactBinderContextIndex , PreparedExactProposition , preparedExactPropositionCore , prepareExactProposition + , prepareExactSymbolicBoundConstraints + , prepareExactSymbolicWitnessConstraints + , prepareExactNounWitnessConstraints , PreparedExactSetExpression , preparedExactSetExpressionCore , prepareExactSetExpression @@ -95,7 +99,7 @@ exactLocalIdValue (ExactLocalId value) = value data ExactBinder = ExactBinder !ExactLocalId - !Raw.VarSymbol + !(Maybe Raw.VarSymbol) !CoreType !(Maybe ExactStructureAnnotation) @@ -123,14 +127,33 @@ extendExactBinderContext additions (ExactBinderContext initial) = | any (sameIdentity identity) binders = Left (ExactDuplicateLocalIdentity (locate variable) identity) | otherwise = - Right (ExactBinder identity variable TySet Nothing : binders) + Right (ExactBinder identity (Just variable) TySet Nothing : binders) sameVariable variable (ExactBinder _identity existing _coreType _structure) = - existing == variable + 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) @@ -150,7 +173,7 @@ exactBinderContextIndex variable (ExactBinderContext binders) = go _index [] = Nothing go index (ExactBinder _identity candidate _coreType _structure : rest) - | candidate == variable = Just index + | candidate == Just variable = Just index | otherwise = go (index + 1) rest newtype PreparedExactProposition = PreparedExactProposition @@ -547,16 +570,88 @@ prepareExactProposition -> 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 - (compileStatement statement) - initialElaboration + State.runStateT compile initialElaboration checked <- either - (Except.throwError - . ExactCoreCheckFailed (locate statement)) + (Except.throwError . ExactCoreCheckFailed location) pure (checkScopedCanonicalCore (`Map.lookup` elaborationGlobals finalElaboration) @@ -565,7 +660,7 @@ prepareExactProposition context statement = unless (scopedCoreType checked == TyProp) (Except.throwError (ExactFormulaExpectedProposition - (locate statement) + location (scopedCoreType checked))) pure (PreparedExactProposition checked) @@ -786,7 +881,7 @@ binderIndices :: ExactBinderContext -> Map.Map Raw.VarSymbol Natural binderIndices (ExactBinderContext binders) = Map.fromList [ (variable, fromIntegral index) - | (index, ExactBinder _identity variable _coreType _structure) <- + | (index, ExactBinder _identity (Just variable) _coreType _structure) <- zip [0 :: Int ..] binders ] @@ -849,18 +944,17 @@ compileHeaderAssumption = \case ] Raw.AsmLetIn variables domain -> do variableTerms <- traverse compileIntroducedVariable variables - domainTerm <- - compileExpressionAsSet domain - >>= structureCarrierCast (locate domain) - pure - [ ( locate variable - , CApp - (CApp (CIntrinsic Member) variableTerm) - domainTerm - ) - | (variable, variableTerm) <- - zip (toList variables) (toList variableTerms) - ] + 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 @@ -2130,6 +2224,22 @@ structureCarrierCast location term = 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 + compileReplacement :: Raw.Expr -> NonEmpty (Raw.VarSymbol, Raw.Expr) @@ -2260,21 +2370,8 @@ compileSymbolicQuantified -> Elaborate (CanonicalTerm ObjectId) compileSymbolicQuantified quantifier variables bound suchThat compileBody = withSetBinders variables do - subjects <- traverse compileIntroducedVariable variables - boundConstraints <- case bound of - Raw.Unbounded -> - pure [] - Raw.Bounded _location sign relation domain -> do - domain' <- compileExpressionAsSet domain - traverse - (\subject -> do - proposition <- - compileAtomicRelationTerms - subject relation domain' - pure case sign of - Raw.Positive -> proposition - Raw.Negative -> logicalNot proposition) - (toList subjects) + boundConstraints <- + compileSymbolicBoundConstraintList variables bound suchThatConstraints <- maybeToList <$> traverse compileStatement suchThat body <- compileBody @@ -2286,6 +2383,25 @@ compileSymbolicQuantified quantifier variables bound suchThat compileBody = (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 @@ -2299,16 +2415,18 @@ compileAtomicRelationTerms left relation right = (Raw.relationSymbolToken symbol) (Raw.relationSymbolParameterArity symbol) compiledParameters <- traverse compileExpressionAsSet parameters - checkedRight <- - if symbol == Raw.ElementSymbol && null parameters - then structureCarrierCast location right - else pure right case fixedSemanticMeaning key of Just FixedEquality | null parameters -> pure (CEq TySet left right) 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 @@ -2316,7 +2434,7 @@ compileAtomicRelationTerms left relation right = (CIntrinsic intrinsic) (coreIntrinsicType intrinsic) ((\term -> (term, TySet)) - <$> (compiledParameters <> [left, checkedRight])) + <$> (compiledParameters <> [left, right])) unless (actual == TyProp) (Except.throwError (ExactFormulaExpectedProposition location actual)) @@ -2328,7 +2446,7 @@ compileAtomicRelationTerms left relation right = (CIntrinsic intrinsic) (coreIntrinsicType intrinsic) ((\term -> (term, TySet)) - <$> (compiledParameters <> [left, checkedRight])) + <$> (compiledParameters <> [left, right])) unless (actual == TyProp) (Except.throwError (ExactFormulaExpectedProposition location actual)) @@ -2338,7 +2456,7 @@ compileAtomicRelationTerms left relation right = applyResolvedTyped location key ((\term -> (term, TySet)) - <$> (compiledParameters <> [left, checkedRight])) + <$> (compiledParameters <> [left, right])) unless (actual == TyProp) (Except.throwError (ExactFormulaExpectedProposition location actual)) @@ -2424,6 +2542,13 @@ compileNoun subject (Raw.Noun location item arguments) key = SemanticNoun (Raw.sg patterns) (Raw.pl patterns) compiled <- traverse compileTermAsSet arguments 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 @@ -2770,6 +2895,18 @@ compileAtomicRelation left relation 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]) @@ -2827,10 +2964,7 @@ compileRelationExpression location expression left right = do (SemanticExpressionFunction (Raw.mixfixPattern Raw.PairSymbol)) [left, right] - pure - (CApp - (CApp (CIntrinsic Member) pair) - relation) + compileMembership location Raw.Positive pair relation compileRelationChain :: Raw.Chain @@ -2884,14 +3018,8 @@ applyResolvedPredicate -> SemanticGlobalKey -> [CanonicalTerm ObjectId] -> Elaborate (CanonicalTerm ObjectId) -applyResolvedPredicate location key arguments = do - (term, actual) <- - applyResolvedTyped - location key ((\argument -> (argument, TySet)) <$> arguments) - unless (actual == TyProp) - (Except.throwError - (ExactFormulaExpectedProposition location actual)) - pure term +applyResolvedPredicate location key = + applyResolvedPredicateChoice location (key :| []) applyResolvedPredicateChoice :: Location @@ -2899,28 +3027,41 @@ applyResolvedPredicateChoice -> [CanonicalTerm ObjectId] -> Elaborate (CanonicalTerm ObjectId) applyResolvedPredicateChoice location keys arguments = 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" + 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 |