diff options
Diffstat (limited to 'source/Checking/Exact.hs')
| -rw-r--r-- | source/Checking/Exact.hs | 153 |
1 files changed, 127 insertions, 26 deletions
diff --git a/source/Checking/Exact.hs b/source/Checking/Exact.hs index c4b90c7..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 ] @@ -2275,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 @@ -2301,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 |