diff options
Diffstat (limited to 'source/Felix/Checking/Core.hs')
| -rw-r--r-- | source/Felix/Checking/Core.hs | 1604 |
1 files changed, 1604 insertions, 0 deletions
diff --git a/source/Felix/Checking/Core.hs b/source/Felix/Checking/Core.hs new file mode 100644 index 0000000..13ec218 --- /dev/null +++ b/source/Felix/Checking/Core.hs @@ -0,0 +1,1604 @@ +{-# 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 Felix.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 + , equalScopedCore + , conjoinScopedCore + , disjoinScopedCore + , negateScopedCore + , falsumScopedCore + , splitScopedSetEquality + , scopedSetInductionInstance + , closeScopedForall + , closeScopedExists + , openScopedForall + , openScopedImplication + , openScopedAssumption + , closeScopedCore + , betaNormalizeCanonical + , instantiateCanonical + , shiftCanonical + , 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 uses this intrinsic HOTG adjunction directly. The +-- ordinary source-owned @cons@ function is not consulted during lowering. +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 + +-- | Form an equality between checked operands under the same lexical +-- context. This preserves the checked-core invariant without requiring a +-- caller to recover global types merely to combine already checked terms. +equalScopedCore + :: ScopedCheckedCore global + -> ScopedCheckedCore global + -> Maybe (ScopedCheckedCore global) +equalScopedCore + (ScopedCheckedCore leftContext leftType left) + (ScopedCheckedCore rightContext rightType right) + | leftContext == rightContext + , leftType == rightType = + Just + (ScopedCheckedCore + leftContext + TyProp + (CEq leftType left right)) +equalScopedCore _left _right = + Nothing + +-- | Conjoin two checked propositions under the same lexical context. Truth +-- is normalized away so callers can build an optional source guard without +-- retaining an inert conjunct. +conjoinScopedCore + :: Eq global + => ScopedCheckedCore global + -> ScopedCheckedCore global + -> Maybe (ScopedCheckedCore global) +conjoinScopedCore + left@(ScopedCheckedCore leftContext TyProp leftTerm) + right@(ScopedCheckedCore rightContext TyProp rightTerm) + | leftContext == rightContext + , leftTerm == truth = Just right + | leftContext == rightContext + , rightTerm == truth = Just left + | leftContext == rightContext = + Just + (ScopedCheckedCore + leftContext + TyProp + (CImp + (CImp leftTerm (CImp rightTerm CFalsum)) + CFalsum)) + where + truth = CImp CFalsum CFalsum +conjoinScopedCore _left _right = + Nothing + +-- | Disjoin two checked propositions under the same lexical context using +-- the fixed classical encoding owned by the checked core. +disjoinScopedCore + :: ScopedCheckedCore global + -> ScopedCheckedCore global + -> Maybe (ScopedCheckedCore global) +disjoinScopedCore + (ScopedCheckedCore leftContext TyProp left) + (ScopedCheckedCore rightContext TyProp right) + | leftContext == rightContext = + Just + (ScopedCheckedCore + leftContext + TyProp + (CImp (CImp left CFalsum) right)) +disjoinScopedCore _left _right = + Nothing + +-- | Negate a checked proposition without changing its lexical context. +negateScopedCore + :: ScopedCheckedCore global + -> Maybe (ScopedCheckedCore global) +negateScopedCore (ScopedCheckedCore context TyProp proposition) = + Just + (ScopedCheckedCore + context + TyProp + (CImp proposition CFalsum)) +negateScopedCore _proposition = + Nothing + +-- | Checked falsum at an already established lexical context. +falsumScopedCore :: [CoreType] -> ScopedCheckedCore global +falsumScopedCore context = + ScopedCheckedCore context TyProp CFalsum + +-- | 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 + +-- | Derive the exact predicate, member-wise hypothesis, induction step, and +-- binder-level result for one set-valued ambient binder. The selected binder +-- is replaced by the newly introduced set variable; every other ambient +-- binder remains a parameter. +scopedSetInductionInstance + :: Natural + -> ScopedCheckedCore global + -> Maybe + ( ScopedCheckedCore global + , ScopedCheckedCore global + , ScopedCheckedCore global + , ScopedCheckedCore global + ) +scopedSetInductionInstance selected + (ScopedCheckedCore context TyProp property) + | binderTypeAt selected context == Just TySet = + Just (predicate, hypothesis, step, result) + where + abstractedProperty = abstractSelected 0 property + predicate = + ScopedCheckedCore + context + (TySet `TyArrow` TyProp) + (CLam TySet abstractedProperty) + hypothesis = + ScopedCheckedCore + context + TyProp + (CForall + TySet + (CImp + (CApp + (CApp + (CIntrinsic Member) + (CBound 0)) + (CBound (selected + 1))) + abstractedProperty)) + step = + ScopedCheckedCore + context + TyProp + (CForall + TySet + (CImp + (abstractSelected + 0 + (scopedCoreTerm hypothesis)) + abstractedProperty)) + result = + ScopedCheckedCore + context + TyProp + (CForall TySet abstractedProperty) + + abstractSelected 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 + (abstractSelected depth function) + (abstractSelected depth argument) + CLam binderType body -> + CLam binderType + (abstractSelected (depth + 1) body) + CFalsum -> + CFalsum + CImp premise conclusion -> + CImp + (abstractSelected depth premise) + (abstractSelected depth conclusion) + CEq operandType left right -> + CEq operandType + (abstractSelected depth left) + (abstractSelected depth right) + CForall binderType body -> + CForall binderType + (abstractSelected (depth + 1) body) +scopedSetInductionInstance _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 + +-- | Open a checked proof assumption against the current goal. Besides a +-- direct implication antecedent, the source language historically permits +-- either immediate side of one binary conjunction antecedent to be assumed +-- first. The other side remains the next implication antecedent. This is a +-- deliberately shallow structural rule: it neither flattens conjunctions nor +-- treats disjunction as an eliminable assumption. +openScopedAssumption + :: Eq global + => ScopedCheckedCore global + -> ScopedCheckedCore global + -> Maybe + ( ScopedCheckedCore global + , ScopedCheckedCore global + ) +openScopedAssumption supplied goal = do + (antecedent, conclusion) <- openScopedImplication goal + if supplied == antecedent + then pure (antecedent, conclusion) + else do + (left, right) <- splitScopedConjunction antecedent + if supplied == left + then do + remaining <- implyScopedCore right conclusion + pure (left, remaining) + else if supplied == right + then do + remaining <- implyScopedCore left conclusion + pure (right, remaining) + else Nothing + +splitScopedConjunction + :: ScopedCheckedCore global + -> Maybe + ( ScopedCheckedCore global + , ScopedCheckedCore global + ) +splitScopedConjunction + (ScopedCheckedCore context TyProp + (CImp (CImp left (CImp right CFalsum)) CFalsum)) = + Just + ( ScopedCheckedCore context TyProp left + , ScopedCheckedCore context TyProp right + ) +splitScopedConjunction _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 |