diff options
Diffstat (limited to 'source/Checking/Core.hs')
| -rw-r--r-- | source/Checking/Core.hs | 217 |
1 files changed, 180 insertions, 37 deletions
diff --git a/source/Checking/Core.hs b/source/Checking/Core.hs index 6e8d175..4b7478f 100644 --- a/source/Checking/Core.hs +++ b/source/Checking/Core.hs @@ -49,6 +49,8 @@ module Checking.Core , weakenCheckedScopedCore , weakenScopedCore , scopedSetDefinition + , scopedCharacteristicDefinition + , scopedReplacementGraph , implyScopedCore , splitScopedSetEquality , scopedSetInductionHypothesis @@ -697,53 +699,194 @@ weakenScopedCore globalType binderType scoped = (shiftCanonical 1 0 (scopedCoreTerm scoped)) --- | Introduce a fresh set-valued local definition. Separation uses the --- checked characteristic rule so its local premise remains first-order. +-- | Introduce a fresh set-valued local definition. Separation specializes +-- the checked foundation characteristic so its local premise remains +-- first-order. scopedSetDefinition - :: ScopedCheckedCore global + :: Eq global + => FrozenCheckedCore Void + -> ScopedCheckedCore global -> Maybe (ScopedCheckedCore global) scopedSetDefinition - (ScopedCheckedCore context TySet expression) = - Just - (ScopedCheckedCore - (TySet : context) - TyProp - (case expression of - CApp - (CApp (CIntrinsic Sep) bound) - (CLam TySet predicate) -> - separationCharacteristic bound predicate - _ -> - CEq + characteristic + expression@(ScopedCheckedCore context TySet term) = + case term of + CApp + (CApp (CIntrinsic Sep) bound) + predicate@(CLam TySet _body) -> + scopedCharacteristicDefinition + characteristic + expression + ( ScopedCheckedCore context TySet bound + :| [ ScopedCheckedCore + context + (TySet `TyArrow` TyProp) + predicate + ] + ) + _ -> + Just + (ScopedCheckedCore + (TySet : context) + TyProp + (CEq TySet (CBound 0) - (shiftCanonical 1 0 expression))) - where - separationCharacteristic bound predicate = - CForall - TySet - (CEq - TyProp - (member (CBound 0) (CBound 1)) - (andP - (member - (CBound 0) - (shiftCanonical 2 0 bound)) - (shiftCanonical 1 1 predicate))) + (shiftCanonical 1 0 term))) +scopedSetDefinition _characteristic _expression = + Nothing - member element set = - CApp - (CApp (CIntrinsic Member) element) - set +-- | Specialize a checked characteristic and abstract its set-valued target +-- into one fresh nearest binder. Checked substitution and beta reduction +-- preserve the foundation row's proposition type. +scopedCharacteristicDefinition + :: Eq global + => FrozenCheckedCore Void + -> ScopedCheckedCore global + -> NonEmpty (ScopedCheckedCore global) + -> Maybe (ScopedCheckedCore global) +scopedCharacteristicDefinition + (FrozenCheckedCore TyProp frozen) + (ScopedCheckedCore context TySet target) + arguments + | all ((== context) . scopedCoreContext) arguments = do + specialized <- + specialize + (mapCanonicalGlobals absurd frozen) + (toList arguments) + let normalized = betaNormalizeCanonical specialized + (found, abstracted) = abstractTarget 0 normalized + guard found + pure + (ScopedCheckedCore + (TySet : context) + TyProp + abstracted) + where + specialize term [] = + Just term + specialize (CForall binderType body) + (ScopedCheckedCore _ argumentType argument : rest) + | binderType == argumentType = + specialize + (instantiateCanonical argument body) + rest + specialize _term _arguments = + Nothing - andP left right = - notP (CImp left (notP right)) + abstractTarget depth term + | term == shiftCanonical depth 0 target = + (True, CBound (fromIntegral depth)) + | otherwise = + case term of + CBound index + | index < fromIntegral depth -> + (False, CBound index) + | otherwise -> + (False, CBound (index + 1)) + CGlobal global -> + (False, CGlobal global) + CIntrinsic intrinsic -> + (False, CIntrinsic intrinsic) + COpaqueInteger integer -> + (False, COpaqueInteger integer) + CApp function argument -> + combine CApp + (abstractTarget depth function) + (abstractTarget depth argument) + CLam binderType body -> + let (found, abstracted) = + abstractTarget (depth + 1) body + in (found, CLam binderType abstracted) + CFalsum -> + (False, CFalsum) + CImp premise conclusion -> + combine CImp + (abstractTarget depth premise) + (abstractTarget depth conclusion) + CEq operandType left right -> + combine (CEq operandType) + (abstractTarget depth left) + (abstractTarget depth right) + CForall binderType body -> + let (found, abstracted) = + abstractTarget (depth + 1) body + in (found, CForall binderType abstracted) + + combine constructor (leftFound, left) (rightFound, right) = + (leftFound || rightFound, constructor left right) +scopedCharacteristicDefinition _characteristic _target _arguments = + Nothing - notP proposition = - CImp proposition CFalsum -scopedSetDefinition _expression = +-- | Build the replacement graph of one checked set-valued local function. +-- The ordered-pair constructor is an ordinary checked source object. +scopedReplacementGraph + :: ScopedCheckedCore global + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> Maybe + ( ScopedCheckedCore global + , ScopedCheckedCore global + , ScopedCheckedCore global + ) +scopedReplacementGraph + (ScopedCheckedCore context pairType pair) + domain@(ScopedCheckedCore domainContext TySet domainTerm) + (ScopedCheckedCore valueContext TySet value) + | pairType == TySet `TyArrow` (TySet `TyArrow` TySet) + , domainContext == context + , valueContext == TySet : context = + let pairValue = + CApp + (CApp + (shiftCanonical 1 0 pair) + (CBound 0)) + value + function = CLam TySet pairValue + graph = + CApp + (CApp (CIntrinsic Repl) domainTerm) + function + in Just + ( ScopedCheckedCore context TySet graph + , domain + , ScopedCheckedCore + context + (TySet `TyArrow` TySet) + function + ) +scopedReplacementGraph _pair _domain _value = Nothing +betaNormalizeCanonical + :: CanonicalTerm global + -> CanonicalTerm global +betaNormalizeCanonical = \case + CApp function argument -> + case betaNormalizeCanonical function of + CLam _binderType body -> + betaNormalizeCanonical + (instantiateCanonical + (betaNormalizeCanonical argument) + body) + normalizedFunction -> + CApp + normalizedFunction + (betaNormalizeCanonical argument) + CLam binderType body -> + CLam binderType (betaNormalizeCanonical body) + CImp premise conclusion -> + CImp + (betaNormalizeCanonical premise) + (betaNormalizeCanonical conclusion) + CEq operandType left right -> + CEq operandType + (betaNormalizeCanonical left) + (betaNormalizeCanonical right) + CForall binderType body -> + CForall binderType (betaNormalizeCanonical body) + term -> term + -- | Combine two checked propositions under the same lexical context. implyScopedCore :: ScopedCheckedCore global |