diff options
Diffstat (limited to 'source/Checking/Core.hs')
| -rw-r--r-- | source/Checking/Core.hs | 1434 |
1 files changed, 0 insertions, 1434 deletions
diff --git a/source/Checking/Core.hs b/source/Checking/Core.hs deleted file mode 100644 index 4b7478f..0000000 --- a/source/Checking/Core.hs +++ /dev/null @@ -1,1434 +0,0 @@ -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE DeriveFoldable #-} -{-# LANGUAGE DeriveTraversable #-} -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE NoImplicitPrelude #-} - --- | Checked monomorphic HOL syntax and its nameless in-memory form. --- --- Scoped syntax is an operational construction language. Only a checked, --- frozen value is semantic input to later kernel and backend boundaries. -module Checking.Core - ( CoreType(..) - , CoreIntrinsicTag(..) - , coreIntrinsicType - , CoreSyntax - , coreLocal - , coreGlobal - , coreIntrinsic - , coreOpaqueInteger - , coreApply - , coreLambda - , coreFalsum - , coreImplication - , coreEquality - , coreForall - , CheckedCore - , checkedCoreType - , checkCore - , checkClosedCore - , ClosedCheckedProposition - , checkedPropositionCore - , checkClosedProposition - , CoreCheckError(..) - , CanonicalTerm(..) - , canonicalSetInsert - , FrozenCheckedCore - , frozenCoreType - , frozenCoreTerm - , thawFrozenCore - , frozenCoreGlobals - , mapFrozenGlobals - , ScopedCheckedCore - , scopedCoreContext - , scopedCoreType - , scopedCoreTerm - , mapScopedGlobals - , checkScopedCanonicalCore - , embedClosedCore - , weakenCheckedScopedCore - , weakenScopedCore - , scopedSetDefinition - , scopedCharacteristicDefinition - , scopedReplacementGraph - , implyScopedCore - , splitScopedSetEquality - , scopedSetInductionHypothesis - , closeScopedForall - , closeScopedExists - , openScopedForall - , openScopedImplication - , closeScopedCore - , instantiateCanonical - , mapCanonicalGlobals - , canonicalTermGlobals - , checkCanonicalCore - , freezeClosed - , FreezeError(..) - , referenceFreezeClosed - ) where - -import Base hiding (Empty) - -import Bound -import Control.DeepSeq (NFData) -import Control.Monad (ap, unless) -import Data.Set qualified as Set -import Numeric.Natural (Natural) - - --- | The complete monomorphic type grammar of the checked core. -data CoreType - = TyProp - | TySet - | TyArrow !CoreType !CoreType - deriving stock (Show, Eq, Ord, Generic) - deriving anyclass (NFData) - - --- | The complete set-forming primitive inventory. -data CoreIntrinsicTag - = Member - | Empty - | PairSet - | FamilyUnion - | PowerSet - | Sep - | Repl - | SetChoose - | UnivOf - -- | The bounded set-valued least fixed point. It denotes the elements of - -- its bound that belong to every bounded pre-fixed point of its operator. - | ISetLfp - deriving stock (Show, Eq, Ord, Enum, Bounded, Generic) - deriving anyclass (NFData) - -coreIntrinsicType :: CoreIntrinsicTag -> CoreType -coreIntrinsicType = \case - Member -> - TySet `TyArrow` (TySet `TyArrow` TyProp) - Empty -> - TySet - PairSet -> - TySet `TyArrow` (TySet `TyArrow` TySet) - FamilyUnion -> - TySet `TyArrow` TySet - PowerSet -> - TySet `TyArrow` TySet - Sep -> - TySet - `TyArrow` - ((TySet `TyArrow` TyProp) `TyArrow` TySet) - Repl -> - TySet - `TyArrow` - ((TySet `TyArrow` TySet) `TyArrow` TySet) - SetChoose -> - (TySet `TyArrow` TyProp) `TyArrow` TySet - UnivOf -> - TySet `TyArrow` TySet - ISetLfp -> - TySet - `TyArrow` - ((TySet `TyArrow` TySet) `TyArrow` TySet) - - --- | Operational scoped syntax. Its constructors remain private because this --- value is neither a typing certificate nor an authority-bearing term. -data CoreSyntax global local - = CoreLocal local - | CoreGlobal global - | CoreIntrinsic CoreIntrinsicTag - | CoreOpaqueInteger !Integer - | CoreApply - !(CoreSyntax global local) - !(CoreSyntax global local) - | CoreLambda - !CoreType - !(Scope () (CoreSyntax global) local) - | CoreFalsum - | CoreImplication - !(CoreSyntax global local) - !(CoreSyntax global local) - | CoreEquality - !CoreType - !(CoreSyntax global local) - !(CoreSyntax global local) - | CoreForall - !CoreType - !(Scope () (CoreSyntax global) local) - deriving stock (Functor, Foldable, Traversable) - -instance Applicative (CoreSyntax global) where - pure = CoreLocal - (<*>) = ap - -instance Monad (CoreSyntax global) where - CoreLocal local >>= replace = - replace local - CoreGlobal global >>= _replace = - CoreGlobal global - CoreIntrinsic intrinsic >>= _replace = - CoreIntrinsic intrinsic - CoreOpaqueInteger integer >>= _replace = - CoreOpaqueInteger integer - CoreApply function argument >>= replace = - CoreApply - (function >>= replace) - (argument >>= replace) - CoreLambda binderType body >>= replace = - CoreLambda binderType (body >>>= replace) - CoreFalsum >>= _replace = - CoreFalsum - CoreImplication premise conclusion >>= replace = - CoreImplication - (premise >>= replace) - (conclusion >>= replace) - CoreEquality operandType left right >>= replace = - CoreEquality - operandType - (left >>= replace) - (right >>= replace) - CoreForall binderType body >>= replace = - CoreForall binderType (body >>>= replace) - -coreLocal :: local -> CoreSyntax global local -coreLocal = CoreLocal - -coreGlobal :: global -> CoreSyntax global local -coreGlobal = CoreGlobal - -coreIntrinsic :: CoreIntrinsicTag -> CoreSyntax global local -coreIntrinsic = CoreIntrinsic - -coreOpaqueInteger :: Integer -> CoreSyntax global local -coreOpaqueInteger = CoreOpaqueInteger - -coreApply - :: CoreSyntax global local - -> CoreSyntax global local - -> CoreSyntax global local -coreApply = CoreApply - -coreLambda - :: Eq local - => CoreType - -> local - -> CoreSyntax global local - -> CoreSyntax global local -coreLambda binderType local body = - CoreLambda binderType (abstract1 local body) - -coreFalsum :: CoreSyntax global local -coreFalsum = CoreFalsum - -coreImplication - :: CoreSyntax global local - -> CoreSyntax global local - -> CoreSyntax global local -coreImplication = CoreImplication - -coreEquality - :: CoreType - -> CoreSyntax global local - -> CoreSyntax global local - -> CoreSyntax global local -coreEquality = CoreEquality - -coreForall - :: Eq local - => CoreType - -> local - -> CoreSyntax global local - -> CoreSyntax global local -coreForall binderType local body = - CoreForall binderType (abstract1 local body) - - -data CoreCheckError - = UnknownCoreGlobal - | UnboundCoreLocal - | UnboundCoreIndex !Natural - | AppliedNonFunction !CoreType - | ApplicationArgumentTypeMismatch - !CoreType - !CoreType - | ImplicationOperandTypeMismatch - !CoreType - | EqualityOperandTypeMismatch - !CoreType - !CoreType - | QuantifierBodyTypeMismatch - !CoreType - | ExpectedCoreType - !CoreType - !CoreType - deriving stock (Show, Eq) - - --- | A scoped term whose complete tree has been type checked. -data CheckedCore global local = CheckedCore - !CoreType - !(CoreSyntax global local) - -checkedCoreType :: CheckedCore global local -> CoreType -checkedCoreType (CheckedCore coreType _syntax) = - coreType - -checkCore - :: (global -> Maybe CoreType) - -> (local -> Maybe CoreType) - -> CoreSyntax global local - -> Either CoreCheckError (CheckedCore global local) -checkCore globalType localType syntax = do - coreType <- - inferCore globalType localType syntax - pure (CheckedCore coreType syntax) - -checkClosedCore - :: (global -> Maybe CoreType) - -> CoreSyntax global local - -> Either CoreCheckError (CheckedCore global Void) -checkClosedCore globalType syntax = do - closedSyntax <- - maybe - (Left UnboundCoreLocal) - Right - (traverse (const Nothing) syntax) - checkCore globalType absurd closedSyntax - -newtype ClosedCheckedProposition global = - ClosedCheckedProposition (CheckedCore global Void) - -checkedPropositionCore - :: ClosedCheckedProposition global - -> CheckedCore global Void -checkedPropositionCore - (ClosedCheckedProposition proposition) = - proposition - -checkClosedProposition - :: (global -> Maybe CoreType) - -> CoreSyntax global local - -> Either CoreCheckError (ClosedCheckedProposition global) -checkClosedProposition globalType syntax = do - checked <- - checkClosedCore globalType syntax - unless - (checkedCoreType checked == TyProp) - (Left - (ExpectedCoreType - TyProp - (checkedCoreType checked))) - pure (ClosedCheckedProposition checked) - -inferCore - :: forall global local - . (global -> Maybe CoreType) - -> (local -> Maybe CoreType) - -> CoreSyntax global local - -> Either CoreCheckError CoreType -inferCore globalType localType = - infer - (maybe - (Left UnboundCoreLocal) - Right - . localType) - where - infer - :: forall local' - . (local' -> Either CoreCheckError CoreType) - -> CoreSyntax global local' - -> Either CoreCheckError CoreType - infer resolveLocal = \case - CoreLocal local -> - resolveLocal local - CoreGlobal global -> - maybe - (Left UnknownCoreGlobal) - Right - (globalType global) - CoreIntrinsic intrinsic -> - Right (coreIntrinsicType intrinsic) - CoreOpaqueInteger{} -> - Right TySet - CoreApply function argument -> do - functionType <- - infer resolveLocal function - argumentType <- - infer resolveLocal argument - case functionType of - TyArrow expectedArgument resultType - | expectedArgument == argumentType -> - Right resultType - | otherwise -> - Left - (ApplicationArgumentTypeMismatch - expectedArgument - argumentType) - other -> - Left (AppliedNonFunction other) - CoreLambda binderType body -> do - bodyType <- - infer - (boundLocalType binderType resolveLocal) - (unscope body) - Right (binderType `TyArrow` bodyType) - CoreFalsum -> - Right TyProp - CoreImplication premise conclusion -> do - premiseType <- - infer resolveLocal premise - unless - (premiseType == TyProp) - (Left - (ImplicationOperandTypeMismatch - premiseType)) - conclusionType <- - infer resolveLocal conclusion - unless - (conclusionType == TyProp) - (Left - (ImplicationOperandTypeMismatch - conclusionType)) - Right TyProp - CoreEquality operandType left right -> do - leftType <- - infer resolveLocal left - unless - (leftType == operandType) - (Left - (EqualityOperandTypeMismatch - operandType - leftType)) - rightType <- - infer resolveLocal right - unless - (rightType == operandType) - (Left - (EqualityOperandTypeMismatch - operandType - rightType)) - Right TyProp - CoreForall binderType body -> do - bodyType <- - infer - (boundLocalType binderType resolveLocal) - (unscope body) - unless - (bodyType == TyProp) - (Left - (QuantifierBodyTypeMismatch bodyType)) - Right TyProp - - boundLocalType - :: forall local' - . CoreType - -> (local' -> Either CoreCheckError CoreType) - -> Var () (CoreSyntax global local') - -> Either CoreCheckError CoreType - boundLocalType binderType outerType = \case - B () -> - Right binderType - F outerSyntax -> - infer outerType outerSyntax - - --- | Felix-owned explicit-index syntax. Index zero denotes the nearest --- enclosing binder. -data CanonicalTerm global - = CBound !Natural - | CGlobal !global - | CIntrinsic !CoreIntrinsicTag - | COpaqueInteger !Integer - | CApp - !(CanonicalTerm global) - !(CanonicalTerm global) - | CLam - !CoreType - !(CanonicalTerm global) - | CFalsum - | CImp - !(CanonicalTerm global) - !(CanonicalTerm global) - | CEq - !CoreType - !(CanonicalTerm global) - !(CanonicalTerm global) - | CForall - !CoreType - !(CanonicalTerm global) - deriving stock (Show, Eq, Ord, Generic) - deriving anyclass (NFData) - --- | The fixed checked-core interpretation of set insertion. --- --- Finite-set notation and typed 'ConsSymbol' lowering share this form. -canonicalSetInsert - :: CanonicalTerm global - -> CanonicalTerm global - -> CanonicalTerm global -canonicalSetInsert element set = - CApp - (CIntrinsic FamilyUnion) - (CApp - (CApp - (CIntrinsic PairSet) - (CApp - (CApp - (CIntrinsic PairSet) - element) - element)) - set) - -data FrozenCheckedCore global = FrozenCheckedCore - !CoreType - !(CanonicalTerm global) - deriving stock (Show, Eq, Ord, Generic) - deriving anyclass (NFData) - -frozenCoreType :: FrozenCheckedCore global -> CoreType -frozenCoreType (FrozenCheckedCore coreType _term) = - coreType - -frozenCoreTerm :: FrozenCheckedCore global -> CanonicalTerm global -frozenCoreTerm (FrozenCheckedCore _coreType term) = - term - -mapFrozenGlobals - :: (global -> global') - -> FrozenCheckedCore global - -> FrozenCheckedCore global' -mapFrozenGlobals transform - (FrozenCheckedCore coreType term) = - FrozenCheckedCore - coreType - (mapCanonicalGlobals transform term) - --- | Recover an operational closed term from a checked frozen value. Any caller --- that extends or substitutes it must check the resulting term again. -thawFrozenCore - :: FrozenCheckedCore global - -> CoreSyntax global Void -thawFrozenCore (FrozenCheckedCore _coreType term) = - case traverse (const Nothing) (go [] term) of - Just closedSyntax -> - closedSyntax - Nothing -> - impossible - "a frozen core term became open while being thawed" - where - go - :: [Natural] - -> CanonicalTerm global - -> CoreSyntax global Natural - go binders = \case - CBound index -> - case lookupBinder index binders of - Just local -> - coreLocal local - Nothing -> - impossible - "a frozen core term contains an unbound index" - CGlobal global -> - coreGlobal global - CIntrinsic intrinsic -> - coreIntrinsic intrinsic - COpaqueInteger integer -> - coreOpaqueInteger integer - CApp function argument -> - coreApply - (go binders function) - (go binders argument) - CLam binderType body -> - let local = - fromIntegral (length binders) - in coreLambda - binderType - local - (go (local : binders) body) - CFalsum -> - coreFalsum - CImp premise conclusion -> - coreImplication - (go binders premise) - (go binders conclusion) - CEq operandType left right -> - coreEquality - operandType - (go binders left) - (go binders right) - CForall binderType body -> - let local = - fromIntegral (length binders) - in coreForall - binderType - local - (go (local : binders) body) - - lookupBinder - :: Natural - -> [Natural] - -> Maybe Natural - lookupBinder _index [] = - Nothing - lookupBinder 0 (local : _rest) = - Just local - lookupBinder index (_local : rest) = - lookupBinder (index - 1) rest - -frozenCoreGlobals - :: Ord global - => FrozenCheckedCore global - -> Set.Set global -frozenCoreGlobals = - canonicalTermGlobals . frozenCoreTerm - -canonicalTermGlobals - :: Ord global - => CanonicalTerm global - -> Set.Set global -canonicalTermGlobals = \case - CBound{} -> - mempty - CGlobal global -> - Set.singleton global - CIntrinsic{} -> - mempty - COpaqueInteger{} -> - mempty - CApp function argument -> - canonicalTermGlobals function - <> canonicalTermGlobals argument - CLam _binderType body -> - canonicalTermGlobals body - CFalsum -> - mempty - CImp premise conclusion -> - canonicalTermGlobals premise - <> canonicalTermGlobals conclusion - CEq _operandType left right -> - canonicalTermGlobals left - <> canonicalTermGlobals right - CForall _binderType body -> - canonicalTermGlobals body - --- | A checked canonical term relative to the listed nearest-first binders. --- This is the construction boundary used by kernel replay; it carries no fact --- authority. -data ScopedCheckedCore global = ScopedCheckedCore - ![CoreType] - !CoreType - !(CanonicalTerm global) - deriving stock (Show, Eq, Ord, Generic) - deriving anyclass (NFData) - -scopedCoreContext - :: ScopedCheckedCore global - -> [CoreType] -scopedCoreContext - (ScopedCheckedCore context _coreType _term) = - context - -scopedCoreType - :: ScopedCheckedCore global - -> CoreType -scopedCoreType - (ScopedCheckedCore _context coreType _term) = - coreType - -scopedCoreTerm - :: ScopedCheckedCore global - -> CanonicalTerm global -scopedCoreTerm - (ScopedCheckedCore _context _coreType term) = - term - -mapScopedGlobals - :: (left -> right) - -> ScopedCheckedCore left - -> ScopedCheckedCore right -mapScopedGlobals transform - (ScopedCheckedCore context coreType term) = - ScopedCheckedCore - context - coreType - (mapCanonicalGlobals transform term) - -checkScopedCanonicalCore - :: (global -> Maybe CoreType) - -> [CoreType] - -> CanonicalTerm global - -> Either CoreCheckError (ScopedCheckedCore global) -checkScopedCanonicalCore globalType context term = - ScopedCheckedCore context - <$> inferCanonicalCore globalType context term - <*> pure term - --- | Regard a closed term under a larger lexical context. Closed canonical --- terms contain no indices, so this does not shift the term. -embedClosedCore - :: [CoreType] - -> FrozenCheckedCore global - -> ScopedCheckedCore global -embedClosedCore context - (FrozenCheckedCore coreType term) = - ScopedCheckedCore context coreType term - --- | Add one nearest binder to an already checked lexical context. -weakenCheckedScopedCore - :: CoreType - -> ScopedCheckedCore global - -> ScopedCheckedCore global -weakenCheckedScopedCore binderType scoped = - ScopedCheckedCore - (binderType : scopedCoreContext scoped) - (scopedCoreType scoped) - (shiftCanonical 1 0 (scopedCoreTerm scoped)) - --- | Add one nearest binder to a checked lexical context. -weakenScopedCore - :: (global -> Maybe CoreType) - -> CoreType - -> ScopedCheckedCore global - -> Either CoreCheckError (ScopedCheckedCore global) -weakenScopedCore globalType binderType scoped = - checkScopedCanonicalCore - globalType - (binderType : scopedCoreContext scoped) - (shiftCanonical 1 0 - (scopedCoreTerm scoped)) - --- | Introduce a fresh set-valued local definition. Separation specializes --- the checked foundation characteristic so its local premise remains --- first-order. -scopedSetDefinition - :: Eq global - => FrozenCheckedCore Void - -> ScopedCheckedCore global - -> Maybe (ScopedCheckedCore global) -scopedSetDefinition - 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 term))) -scopedSetDefinition _characteristic _expression = - Nothing - --- | 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 - - 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 - --- | 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 - -> ScopedCheckedCore global - -> Maybe (ScopedCheckedCore global) -implyScopedCore - (ScopedCheckedCore premiseContext TyProp premise) - (ScopedCheckedCore conclusionContext TyProp conclusion) - | premiseContext == conclusionContext = - Just - (ScopedCheckedCore - premiseContext - TyProp - (CImp premise conclusion)) -implyScopedCore _premise _conclusion = - Nothing - --- | Split a checked set equality into its two extensionality directions. -splitScopedSetEquality - :: ScopedCheckedCore global - -> Maybe - ( ScopedCheckedCore global - , ScopedCheckedCore global - ) -splitScopedSetEquality - (ScopedCheckedCore context TyProp (CEq TySet left right)) = - Just (subset left right, subset right left) - where - subset source target = - ScopedCheckedCore - context - TyProp - (CForall - TySet - (CImp - (memberOf (shiftCanonical 1 0 source)) - (memberOf (shiftCanonical 1 0 target)))) - - memberOf set = - CApp - (CApp - (CIntrinsic Member) - (CBound 0)) - set -splitScopedSetEquality _proposition = - Nothing - --- | Form the set-induction hypothesis for one set-valued ambient binder. -scopedSetInductionHypothesis - :: Natural - -> ScopedCheckedCore global - -> Maybe (ScopedCheckedCore global) -scopedSetInductionHypothesis selected - (ScopedCheckedCore context TyProp property) - | binderTypeAt selected context == Just TySet = - Just - (ScopedCheckedCore - context - TyProp - (CForall - TySet - (CImp - (CApp - (CApp - (CIntrinsic Member) - (CBound 0)) - (CBound (selected + 1))) - (replaceSelectedWithNearest - 0 property)))) - where - replaceSelectedWithNearest depth = \case - CBound index - | index == depth + selected -> - CBound depth - | index >= depth -> - CBound (index + 1) - | otherwise -> - CBound index - CGlobal global -> - CGlobal global - CIntrinsic intrinsic -> - CIntrinsic intrinsic - COpaqueInteger integer -> - COpaqueInteger integer - CApp function argument -> - CApp - (replaceSelectedWithNearest depth function) - (replaceSelectedWithNearest depth argument) - CLam binderType body -> - CLam binderType - (replaceSelectedWithNearest (depth + 1) body) - CFalsum -> - CFalsum - CImp premise conclusion -> - CImp - (replaceSelectedWithNearest depth premise) - (replaceSelectedWithNearest depth conclusion) - CEq operandType left right -> - CEq operandType - (replaceSelectedWithNearest depth left) - (replaceSelectedWithNearest depth right) - CForall binderType body -> - CForall binderType - (replaceSelectedWithNearest (depth + 1) body) -scopedSetInductionHypothesis _selected _property = - Nothing - --- | Close the nearest checked binder as one leading universal. -closeScopedForall - :: ScopedCheckedCore global - -> Maybe (ScopedCheckedCore global) -closeScopedForall - (ScopedCheckedCore (binderType : context) TyProp body) = - Just - (ScopedCheckedCore - context - TyProp - (CForall binderType body)) -closeScopedForall _scoped = - Nothing - --- | Close the nearest checked binder as one leading existential. -closeScopedExists - :: ScopedCheckedCore global - -> Maybe (ScopedCheckedCore global) -closeScopedExists - (ScopedCheckedCore (binderType : context) TyProp body) = - Just - (ScopedCheckedCore - context - TyProp - (CImp - (CForall binderType (CImp body CFalsum)) - CFalsum)) -closeScopedExists _scoped = - Nothing - --- | Open one checked leading universal without rechecking its body. -openScopedForall - :: ScopedCheckedCore global - -> Maybe (CoreType, ScopedCheckedCore global) -openScopedForall - (ScopedCheckedCore context TyProp - (CForall binderType body)) = - Just - ( binderType - , ScopedCheckedCore - (binderType : context) - TyProp - body - ) -openScopedForall _scoped = - Nothing - --- | Split one checked implication under its unchanged ambient context. -openScopedImplication - :: ScopedCheckedCore global - -> Maybe - ( ScopedCheckedCore global - , ScopedCheckedCore global - ) -openScopedImplication - (ScopedCheckedCore context TyProp - (CImp premise conclusion)) = - Just - ( ScopedCheckedCore context TyProp premise - , ScopedCheckedCore context TyProp conclusion - ) -openScopedImplication _scoped = - Nothing - -closeScopedCore - :: ScopedCheckedCore global - -> Maybe (FrozenCheckedCore global) -closeScopedCore - (ScopedCheckedCore [] coreType term) = - Just (FrozenCheckedCore coreType term) -closeScopedCore ScopedCheckedCore{} = - Nothing - --- | Substitute an outer-context term for index zero and remove that binder. -instantiateCanonical - :: CanonicalTerm global - -> CanonicalTerm global - -> CanonicalTerm global -instantiateCanonical argument = - instantiateAt 0 - where - instantiateAt depth = \case - CBound index - | index == depth -> - shiftCanonical depth 0 argument - | index > depth -> - CBound (index - 1) - | otherwise -> - CBound index - CGlobal global -> - CGlobal global - CIntrinsic intrinsic -> - CIntrinsic intrinsic - COpaqueInteger integer -> - COpaqueInteger integer - CApp function operand -> - CApp - (instantiateAt depth function) - (instantiateAt depth operand) - CLam binderType body -> - CLam binderType - (instantiateAt (depth + 1) body) - CFalsum -> - CFalsum - CImp premise conclusion -> - CImp - (instantiateAt depth premise) - (instantiateAt depth conclusion) - CEq operandType left right -> - CEq operandType - (instantiateAt depth left) - (instantiateAt depth right) - CForall binderType body -> - CForall binderType - (instantiateAt (depth + 1) body) - -mapCanonicalGlobals - :: (global -> global') - -> CanonicalTerm global - -> CanonicalTerm global' -mapCanonicalGlobals transform = \case - CBound index -> - CBound index - CGlobal global -> - CGlobal (transform global) - CIntrinsic intrinsic -> - CIntrinsic intrinsic - COpaqueInteger integer -> - COpaqueInteger integer - CApp function argument -> - CApp - (mapCanonicalGlobals transform function) - (mapCanonicalGlobals transform argument) - CLam binderType body -> - CLam binderType - (mapCanonicalGlobals transform body) - CFalsum -> - CFalsum - CImp premise conclusion -> - CImp - (mapCanonicalGlobals transform premise) - (mapCanonicalGlobals transform conclusion) - CEq operandType left right -> - CEq operandType - (mapCanonicalGlobals transform left) - (mapCanonicalGlobals transform right) - CForall binderType body -> - CForall binderType - (mapCanonicalGlobals transform body) - --- | Recheck a nameless term without exposing the checked wrapper constructor. -checkCanonicalCore - :: (global -> Maybe CoreType) - -> CanonicalTerm global - -> Either CoreCheckError (FrozenCheckedCore global) -checkCanonicalCore globalType term = - FrozenCheckedCore - <$> inferCanonicalCore globalType [] term - <*> pure term - -inferCanonicalCore - :: (global -> Maybe CoreType) - -> [CoreType] - -> CanonicalTerm global - -> Either CoreCheckError CoreType -inferCanonicalCore globalType binders = \case - CBound index -> - maybe - (Left (UnboundCoreIndex index)) - Right - (binderTypeAt index binders) - CGlobal global -> - maybe - (Left UnknownCoreGlobal) - Right - (globalType global) - CIntrinsic intrinsic -> - Right (coreIntrinsicType intrinsic) - COpaqueInteger{} -> - Right TySet - CApp function argument -> do - functionType <- - inferCanonicalCore globalType binders function - argumentType <- - inferCanonicalCore globalType binders argument - case functionType of - TyArrow expectedArgument resultType - | expectedArgument == argumentType -> - Right resultType - | otherwise -> - Left - (ApplicationArgumentTypeMismatch - expectedArgument - argumentType) - other -> - Left (AppliedNonFunction other) - CLam binderType body -> do - bodyType <- - inferCanonicalCore - globalType - (binderType : binders) - body - Right (binderType `TyArrow` bodyType) - CFalsum -> - Right TyProp - CImp premise conclusion -> do - premiseType <- - inferCanonicalCore globalType binders premise - unless - (premiseType == TyProp) - (Left - (ImplicationOperandTypeMismatch - premiseType)) - conclusionType <- - inferCanonicalCore globalType binders conclusion - unless - (conclusionType == TyProp) - (Left - (ImplicationOperandTypeMismatch - conclusionType)) - Right TyProp - CEq operandType left right -> do - leftType <- - inferCanonicalCore globalType binders left - unless - (leftType == operandType) - (Left - (EqualityOperandTypeMismatch - operandType - leftType)) - rightType <- - inferCanonicalCore globalType binders right - unless - (rightType == operandType) - (Left - (EqualityOperandTypeMismatch - operandType - rightType)) - Right TyProp - CForall binderType body -> do - bodyType <- - inferCanonicalCore - globalType - (binderType : binders) - body - unless - (bodyType == TyProp) - (Left - (QuantifierBodyTypeMismatch bodyType)) - Right TyProp - -binderTypeAt :: Natural -> [CoreType] -> Maybe CoreType -binderTypeAt _index [] = - Nothing -binderTypeAt 0 (binderType : _rest) = - Just binderType -binderTypeAt index (_binderType : rest) = - binderTypeAt (index - 1) rest - -shiftCanonical - :: Natural - -> Natural - -> CanonicalTerm global - -> CanonicalTerm global -shiftCanonical amount cutoff = \case - CBound index - | index >= cutoff -> - CBound (index + amount) - | otherwise -> - CBound index - CGlobal global -> - CGlobal global - CIntrinsic intrinsic -> - CIntrinsic intrinsic - COpaqueInteger integer -> - COpaqueInteger integer - CApp function argument -> - CApp - (shiftCanonical amount cutoff function) - (shiftCanonical amount cutoff argument) - CLam binderType body -> - CLam binderType - (shiftCanonical amount (cutoff + 1) body) - CFalsum -> - CFalsum - CImp premise conclusion -> - CImp - (shiftCanonical amount cutoff premise) - (shiftCanonical amount cutoff conclusion) - CEq operandType left right -> - CEq operandType - (shiftCanonical amount cutoff left) - (shiftCanonical amount cutoff right) - CForall binderType body -> - CForall binderType - (shiftCanonical amount (cutoff + 1) body) - -data FreezeError - = FreeLocalInClosedCore - deriving stock (Show, Eq) - --- | Freeze a checked closed term in one traversal of the operational syntax. -freezeClosed - :: CheckedCore global Void - -> Either FreezeError (FrozenCheckedCore global) -freezeClosed (CheckedCore coreType syntax) = - FrozenCheckedCore coreType - <$> optimizedFreeze 0 rootResolver syntax - where - rootResolver _depth = - absurd - --- | Bounded executable oracle for tests. Production code uses 'freezeClosed'. -referenceFreezeClosed - :: CheckedCore global Void - -> Either FreezeError (FrozenCheckedCore global) -referenceFreezeClosed (CheckedCore coreType syntax) = - FrozenCheckedCore coreType - <$> referenceFreeze 0 rootResolver syntax - where - rootResolver _depth = - absurd - -type VariableResolver local global = - Natural - -> local - -> Either FreezeError (CanonicalTerm global) - -optimizedFreeze - :: Natural - -> VariableResolver local global - -> CoreSyntax global local - -> Either FreezeError (CanonicalTerm global) -optimizedFreeze depth resolve = \case - CoreLocal local -> - resolve depth local - CoreGlobal global -> - Right (CGlobal global) - CoreIntrinsic intrinsic -> - Right (CIntrinsic intrinsic) - CoreOpaqueInteger integer -> - Right (COpaqueInteger integer) - CoreApply function argument -> - CApp - <$> optimizedFreeze depth resolve function - <*> optimizedFreeze depth resolve argument - CoreLambda binderType body -> - CLam binderType - <$> optimizedFreeze - (depth + 1) - (resolveGeneralized depth resolve) - (unscope body) - CoreFalsum -> - Right CFalsum - CoreImplication premise conclusion -> - CImp - <$> optimizedFreeze depth resolve premise - <*> optimizedFreeze depth resolve conclusion - CoreEquality operandType left right -> - CEq operandType - <$> optimizedFreeze depth resolve left - <*> optimizedFreeze depth resolve right - CoreForall binderType body -> - CForall binderType - <$> optimizedFreeze - (depth + 1) - (resolveGeneralized depth resolve) - (unscope body) - where - resolveGeneralized - :: Natural - -> VariableResolver local global - -> VariableResolver - (Var () (CoreSyntax global local)) - global - resolveGeneralized binderLevel outerResolve currentDepth = \case - B () -> - Right - (CBound - (currentDepth - binderLevel - 1)) - F outerSyntax -> - optimizedFreeze - currentDepth - outerResolve - outerSyntax - -referenceFreeze - :: Natural - -> VariableResolver local global - -> CoreSyntax global local - -> Either FreezeError (CanonicalTerm global) -referenceFreeze depth resolve = \case - CoreLocal local -> - resolve depth local - CoreGlobal global -> - Right (CGlobal global) - CoreIntrinsic intrinsic -> - Right (CIntrinsic intrinsic) - CoreOpaqueInteger integer -> - Right (COpaqueInteger integer) - CoreApply function argument -> - CApp - <$> referenceFreeze depth resolve function - <*> referenceFreeze depth resolve argument - CoreLambda binderType body -> - CLam binderType - <$> referenceFreeze - (depth + 1) - (resolveNormalized depth resolve) - (fromScope body) - CoreFalsum -> - Right CFalsum - CoreImplication premise conclusion -> - CImp - <$> referenceFreeze depth resolve premise - <*> referenceFreeze depth resolve conclusion - CoreEquality operandType left right -> - CEq operandType - <$> referenceFreeze depth resolve left - <*> referenceFreeze depth resolve right - CoreForall binderType body -> - CForall binderType - <$> referenceFreeze - (depth + 1) - (resolveNormalized depth resolve) - (fromScope body) - where - resolveNormalized - :: Natural - -> VariableResolver local global - -> VariableResolver (Var () local) global - resolveNormalized binderLevel outerResolve currentDepth = \case - B () -> - Right - (CBound - (currentDepth - binderLevel - 1)) - F outerLocal -> - outerResolve currentDepth outerLocal |