diff options
Diffstat (limited to 'source/Checking.hs')
| -rw-r--r-- | source/Checking.hs | 4265 |
1 files changed, 0 insertions, 4265 deletions
diff --git a/source/Checking.hs b/source/Checking.hs deleted file mode 100644 index ed5731a..0000000 --- a/source/Checking.hs +++ /dev/null @@ -1,4265 +0,0 @@ -{-# LANGUAGE MultiWayIf #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE NoImplicitPrelude #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE RecordWildCards #-} -{-# OPTIONS_GHC -Wno-name-shadowing #-} - - -module Checking where - - -import Base hiding (locally) -import Checking.Core qualified as Core -import Checking.Dependencies qualified as Dependencies -import Checking.Datatype qualified as Datatype -import Checking.Exact.Vocabulary qualified as ExactVocabulary -import Checking.Facts qualified as Facts -import Checking.Kernel.Derivation - ( importIx - , importedFactDerivation - ) -import Checking.Legacy -import Checking.Obligation -import Checking.Structure qualified as Structure -import Checking.Transition qualified as Transition -import Checking.Typed.Atomic qualified as TypedAtomic -import Checking.Typed.Inductive qualified as TypedInductive -import Checking.Typed.Reflexivity qualified as TypedReflexivity -import StructGraph -import Syntax.Internal -import Syntax.Lexicon -import Encoding -import Report.Location - -import Bound.Scope -import Bound.Var (Var(..), unvar) -import Control.Exception (Exception) -import Control.Monad.Reader -import Control.Monad.State -import Data.Bifunctor (first) -import Data.HashMap.Strict qualified as HM -import Data.HashSet qualified as HS -import Data.IORef (newIORef, modifyIORef', readIORef) -import Data.List qualified as List -import Data.List.NonEmpty qualified as NonEmpty -import Data.Map.Strict qualified as Map -import Data.Set qualified as Set -import Data.Text qualified as Text -import Data.Text.IO qualified as Text -import Data.Vector (Vector) -import Data.Vector qualified as Vector -import System.FilePath.Posix -import UnliftIO.Directory - -type Checking = CheckingM () -type CheckingM = StateT CheckingState IO - --- | Like 'Base.locally', but preserves declaration-local counters across --- nested proof blocks. -locally :: CheckingM a -> CheckingM a -locally ma = do - st <- get - a <- ma - st' <- get - put - st - { checkingHypothesisCounter = - checkingHypothesisCounter st' - , checkingNextObligationOrdinal = - checkingNextObligationOrdinal st' - , checkingResolvedObligationBatches = - checkingResolvedObligationBatches st' - } - pure a - -check :: WithDumpPremselTraining -> [Block] -> IO [Task] -check dumpPremselTraining blocks = - fmap preparedObligationTask - <$> checkPrepared - dumpPremselTraining - id - blocks - -checkPrepared - :: WithDumpPremselTraining - -> (Task -> Task) - -> [Block] - -> IO [PreparedObligation] -checkPrepared dumpPremselTraining prepareTask blocks = do - obligationsRef <- newIORef [] - void - (runStateT - (checkBlocks blocks) - (initialCheckingStateWithTaskPreparation - dumpPremselTraining - prepareTask - (\batch -> - for_ - (preparedBatchObligations batch) - (\obligation -> - when - (preparedObligationMethod obligation - == ProveWithVampire) - (modifyIORef' - obligationsRef - (obligation :)))))) - reverse <$> readIORef obligationsRef - -checkWith - :: WithDumpPremselTraining - -> [Block] - -> (PreparedObligationBatch -> IO ()) - -> IO () -checkWith dumpPremselTraining blocks emitBatch = - void - (runStateT - (checkBlocks blocks) - (initialCheckingState - dumpPremselTraining - emitBatch)) - -initialCheckingState - :: WithDumpPremselTraining - -> (PreparedObligationBatch -> IO ()) - -> CheckingState -initialCheckingState dumpPremselTraining = - initialCheckingStateWithTaskPreparation - dumpPremselTraining - id - -initialCheckingStateWithTaskPreparation - :: WithDumpPremselTraining - -> (Task -> Task) - -> (PreparedObligationBatch -> IO ()) - -> CheckingState -initialCheckingStateWithTaskPreparation - dumpPremselTraining - prepareTask - emitBatch = - initialCheckingStateWithBatchHandler - dumpPremselTraining - prepareTask - (ObserveObligationBatches emitBatch) - Nothing - Nothing - -initialLegacyCheckingStateWithTaskPreparation - :: WithDumpPremselTraining - -> (Task -> Task) - -> LegacyModuleStage - -> (PreparedObligationBatch -> IO ResolvedObligationBatch) - -> CheckingState -initialLegacyCheckingStateWithTaskPreparation - dumpPremselTraining - prepareTask - stage - resolveBatch = - checkingStateWithEnvironment - (legacyStageImportedCheckingEnvironment stage) - ( (initialCheckingStateWithBatchHandler - dumpPremselTraining - prepareTask - (ResolveObligationBatches resolveBatch) - (Just stage) - Nothing) - { checkingFacts = legacyStageFactRegistry stage - } - ) - -initialTransitionCheckingStateWithTaskPreparation - :: WithDumpPremselTraining - -> (Task -> Task) - -> Transition.TransitionModuleBuilder - -> (PreparedObligationBatch -> IO ResolvedObligationBatch) - -> CheckingState -initialTransitionCheckingStateWithTaskPreparation - dumpPremselTraining - prepareTask - builder - resolveBatch = - checkingStateWithEnvironment - (Transition.transitionBuilderImportedCheckingEnvironment - builder) - ( (initialCheckingStateWithBatchHandler - dumpPremselTraining - prepareTask - (ResolveObligationBatches resolveBatch) - (Just - (Transition.transitionBuilderLegacyStage - builder)) - (Just builder)) - { checkingFacts = - legacyStageFactRegistry - (Transition.transitionBuilderLegacyStage - builder) - } - ) - --- | Production V1 checking uses the complete contracted task and has no --- premise-selection or training mode. -initialTransitionCheckingState - :: Transition.TransitionModuleBuilder - -> (PreparedObligationBatch -> IO ResolvedObligationBatch) - -> CheckingState -initialTransitionCheckingState = - initialTransitionCheckingStateWithTaskPreparation - WithoutDumpPremselTraining - contractionTask - -initialCheckingStateWithBatchHandler - :: WithDumpPremselTraining - -> (Task -> Task) - -> ObligationBatchHandler - -> Maybe LegacyModuleStage - -> Maybe Transition.TransitionModuleBuilder - -> CheckingState -initialCheckingStateWithBatchHandler - dumpPremselTraining - prepareTask - batchHandler - legacyStage - transitionBuilder = - CheckingState - { checkingAssumptions = [] - , checkingDumpPremselTraining = dumpPremselTraining - , checkingGoals = [] - , checkingFacts = Facts.emptyFactRegistry - , checkingDirectness = Direct - , checkingAbbreviations = initAbbreviations - , checkingPredicateDefinitions = mempty - , checkingDependencies = - Dependencies.fromRootSymbols (Set.fromList builtinSymbols) - , checkingOwnedSymbols = builtinOwnedSymbols - , checkingOwnedSymbolMarkers = builtinOwnedSymbolMarkers - , checkingFrozenSymbols = mempty - , checkingStructs = initCheckingStructs - , checkingStructContext = mempty - , definedMarkers = HS.empty - , blockLabel = Marker "" - , stepLocation = Nowhere - , blockEndLocation = Nowhere - , localVars = mempty - , checkingHypothesisCounter = 0 - , checkingNextObligationOrdinal = - legacyObligationOrdinal 0 - , checkingPrepareTask = prepareTask - , checkingObligationBatchHandler = batchHandler - , checkingResolvedObligationBatches = [] - , checkingDeclarationFactProducers = [] - , checkingLegacyModuleStage = legacyStage - , checkingTransitionModuleBuilder = - transitionBuilder - } - -runCheckingBlocks :: [Block] -> CheckingState -> IO CheckingState -runCheckingBlocks blocks checkingState = - snd <$> runStateT (checkBlocks blocks) checkingState - -checkingStateEnvironment - :: CheckingState - -> LegacyCheckingEnvironment -checkingStateEnvironment state = - legacyCheckingEnvironment - (checkingAbbreviations state) - (checkingPredicateDefinitions state) - (checkingDependencies state) - (checkingOwnedSymbols state) - (checkingOwnedSymbolMarkers state) - (checkingFrozenSymbols state) - (checkingStructs state) - (definedMarkers state) - -checkingStateWithEnvironment - :: LegacyCheckingEnvironment - -> CheckingState - -> CheckingState -checkingStateWithEnvironment environment state = - state - { checkingAbbreviations = - legacyEnvironmentAbbreviations environment - , checkingPredicateDefinitions = - legacyEnvironmentPredicateDefinitions environment - , checkingDependencies = - legacyEnvironmentDependencies environment - , checkingOwnedSymbols = - legacyEnvironmentOwnedSymbols environment - , checkingOwnedSymbolMarkers = - legacyEnvironmentOwnedSymbolMarkers environment - , checkingFrozenSymbols = - legacyEnvironmentFrozenSymbols environment - , checkingStructs = - legacyEnvironmentStructs environment - , definedMarkers = - legacyEnvironmentDefinedMarkers environment - } - -data WithDumpPremselTraining = WithoutDumpPremselTraining | WithDumpPremselTraining - -data ObligationBatchHandler - = ObserveObligationBatches - (PreparedObligationBatch -> IO ()) - | ResolveObligationBatches - (PreparedObligationBatch -> IO ResolvedObligationBatch) - --- | The checking state manages contextual information while checking and --- emits generated proof tasks through a callback. --- INVARIANT: All formulas in the checking state that eventually --- get exported should have all their abbreviations resolved. -data CheckingState = CheckingState - { checkingDumpPremselTraining :: WithDumpPremselTraining - - , checkingAssumptions :: [CurrentHypothesis] - -- ^ Local assumptions. - -- - , checkingGoals :: [Formula] - -- ^ The current goals. INVARIANT: these should always be canonicalized and have all abbreviations resolved. - -- - , checkingFacts :: Facts.FactRegistry - -- ^ Canonical axioms and proven results with separate registration metadata. - -- - -- - , checkingDirectness :: Directness - -- ^ E can detect contradictory axioms and warns about them. - -- In an indirect proof (e.g. a proof by contradiction) we want - -- to ignore that warning. - -- - , checkingAbbreviations :: HashMap Symbol (Scope Int ExprOf Void) - -- ^ Abbreviations are definitions that automatically get expanded. - -- They are given by a closed rhs (hence the 'Void' indicating no free variables). - -- INVARIANT: The bound 'Int' values must be lower than the arity of the symbol. - -- - , checkingPredicateDefinitions :: HashMap Predicate [Scope Int ExprOf Void] - -- ^ Definitions of predicate that we can match against in assumptions. - -- Axioms and theorems that have the shape of a definition can be added as alternate definitions. - -- - , checkingDependencies :: Dependencies.DependencyRegistry - -- ^ Backward-only dependencies of every owned symbol. - -- - , checkingOwnedSymbols :: HashMap Symbol SymbolOwner - -- ^ Top-level symbols with an established introducing owner in this document. - -- - , checkingOwnedSymbolMarkers :: HashSet Marker - -- ^ Object-language markers claimed by top-level symbols. - -- INVARIANT: contains the marker of every key in 'checkingOwnedSymbols'. - -- - , checkingFrozenSymbols :: HashMap Symbol Marker - -- ^ Symbols mentioned in an inductive specification may not be defined later. - -- - , checkingStructs :: StructGraph - -- ^ Graph of structs defined so far. - -- - , checkingStructContext :: StructContext - -- ^ Structure labels and operations in scope for carrier and operation annotation. - -- - , localVars :: Set VarSymbol - -- ^ Keeps track of the variables that are locally constant. - -- - , definedMarkers :: HashSet Marker - -- ^ Markers for toplevel sections need to be unique. This keeps track of the - -- markers used thus far. - -- - , blockLabel :: Marker -- ^ Label/marker of the current block - , stepLocation :: Location -- ^ Location of the current proof step - , blockEndLocation :: Location -- ^ Ending of the current proof block, useful for error messages for implicit QEDs. - , checkingHypothesisCounter :: Int -- ^ Counter for labeling local hypotheses within a proof. - , checkingNextObligationOrdinal :: LegacyObligationOrdinal - , checkingPrepareTask :: Task -> Task - , checkingObligationBatchHandler :: ObligationBatchHandler - , checkingResolvedObligationBatches - :: [ResolvedObligationBatch] - , checkingDeclarationFactProducers - :: [LegacyFactProducer] - , checkingLegacyModuleStage - :: Maybe LegacyModuleStage - , checkingTransitionModuleBuilder - :: Maybe Transition.TransitionModuleBuilder - } - -data CurrentHypothesis = CurrentHypothesis - !Hypothesis - !Location - !Marker - -data StructContext = StructContext - { structContextLabels :: Set VarSymbol - , structContextOps :: HashMap StructSymbol VarSymbol - } - -data BlockContext = BlockContext - { blockContextLocation :: !Location - , blockContextMarker :: !Marker - } - deriving (Show, Eq) - -instance Semigroup StructContext where - StructContext labels ops <> StructContext labels' ops' = - StructContext (labels <> labels') (ops <> ops') - -instance Monoid StructContext where - mempty = StructContext mempty mempty - -initCheckingStructs :: StructGraph -initCheckingStructs = StructGraph.insert - _Onesorted - mempty -- no parents - (Set.singleton CarrierSymbol) -- used for casting X -> \carrier[X] - (Set.singleton CarrierSymbol) - mempty -- empty graph - -initAbbreviations :: HashMap Symbol (Scope Int ExprOf Void) -initAbbreviations = HM.fromList - [ (SymbolPredicate (PredicateRelation NotElementSymbol), toScope (isNotElementOf Nowhere (TermVar (B 0)) (TermVar (B 1)))) - , (SymbolPredicate (PredicateVerb (mkLexicalItemSgPl (unsafeReadPhraseSgPl "equal[s/] ?") "eq")), toScope (Equals Nowhere (TermVar (B 0))( TermVar (B 1)))) - , (SymbolPredicate (PredicateNoun (mkLexicalItemSgPl (unsafeReadPhraseSgPl "element[/s] of ?") "elem")), toScope (isElementOf (TermVar (B 0)) (TermVar (B 1)))) - ] - -builtinOwnerMarker :: Marker -builtinOwnerMarker = Marker "<builtin>" - -builtinOwner :: SymbolOwner -builtinOwner = - SymbolOwner - { symbolOwnerKind = OwnedByBuiltin - , symbolOwnerMarker = builtinOwnerMarker - } - -builtinOwnedSymbols :: HashMap Symbol SymbolOwner -builtinOwnedSymbols = - HM.fromList - [ (symbol, builtinOwner) - | symbol <- builtinSymbols - ] - -builtinOwnedSymbolMarkers :: HashSet Marker -builtinOwnedSymbolMarkers = - HS.fromList - [ marker - | symbol <- builtinSymbols - , Just marker <- [objectSymbolMarker symbol] - ] - -initialLegacyCheckingEnvironment - :: LegacyCheckingEnvironment -initialLegacyCheckingEnvironment = - legacyCheckingEnvironment - initAbbreviations - mempty - (Dependencies.fromRootSymbols - (Set.fromList builtinSymbols)) - builtinOwnedSymbols - builtinOwnedSymbolMarkers - mempty - initCheckingStructs - mempty - -builtinReservedMixfixMarkers :: Set Marker -builtinReservedMixfixMarkers = - Set.fromList - [ "cons" - , "cumul" - , "emptyset" - , "naturals" - , "pair" - , "pow" - , "union" - ] - -builtinSymbols :: [Symbol] -builtinSymbols = - List.nub - ( [ SymbolMixfix mixfix - | level <- toList (lexiconMixfixTable builtins) - , mixfix <- Map.elems level - , mixfixMarker mixfix `Set.member` builtinReservedMixfixMarkers - ] - <> [ SymbolPredicate (PredicateRelation relation) - | relation <- lexiconRelationSymbols builtins - ] - <> [ SymbolPredicate (PredicateAdj adj) - | adj <- lexiconAdjLs builtins <> lexiconAdjRs builtins - ] - <> [ SymbolPredicate (PredicateVerb verb) - | verb <- lexiconVerbs builtins - ] - <> [ SymbolPredicate (PredicateNoun noun) - | noun <- lexiconNouns builtins - ] - <> [ SymbolPredicate (PredicateNounStruct noun) - | noun <- lexiconStructNouns builtins - ] - <> [ SymbolPredicate (PredicateSymbol name) - | (PrefixPredicate name _arity, _marker) <- lexiconPrefixPredicates builtins - ] - <> [ SymbolFun fun - | fun <- lexiconFuns builtins - ] - ) - -data CheckingError - = DuplicateMarker Location Marker - | UnknownStructureParent StructPhrase Location Marker - | ByContradictionOnMultipleGoals Location Marker - | BySetInductionSyntacticMismatch Location Marker - | ByOrdInductionSyntacticMismatch Location Marker - | SetExtensionalityWithTake Location Marker - | ProofWithoutPrecedingTheorem Location Marker - | CouldNotEliminateHigherOrder FunctionSymbol Term Location Marker - | UnresolvedStructureOperation StructSymbol Location Marker - | AmbiguousInductionVar Location Marker - | MismatchedSetExt [Formula] Location Marker - | MismatchedAssume Formula Formula Location Marker - | CheckingError Text Location Marker - deriving (Show, Eq) - -instance Exception CheckingError - -checkingErrorContext :: CheckingError -> (Location, Marker) -checkingErrorContext = \case - DuplicateMarker location marker -> (location, marker) - UnknownStructureParent _parent location marker -> (location, marker) - ByContradictionOnMultipleGoals location marker -> (location, marker) - BySetInductionSyntacticMismatch location marker -> (location, marker) - ByOrdInductionSyntacticMismatch location marker -> (location, marker) - SetExtensionalityWithTake location marker -> (location, marker) - ProofWithoutPrecedingTheorem location marker -> (location, marker) - CouldNotEliminateHigherOrder _symbol _term location marker -> - (location, marker) - UnresolvedStructureOperation _symbol location marker -> (location, marker) - AmbiguousInductionVar location marker -> (location, marker) - MismatchedSetExt _formulas location marker -> (location, marker) - MismatchedAssume _assumption _goal location marker -> (location, marker) - CheckingError _message location marker -> (location, marker) - -renderCheckingError :: CheckingError -> Text -renderCheckingError failure = - locationToText location - <> " in " <> markerTextOf marker <> ": " <> reason failure - where - (location, marker) = checkingErrorContext failure - - reason = \case - DuplicateMarker{} -> - "marker is already registered" - UnknownStructureParent parent _location _marker -> - "unknown parent structure " <> Text.pack (show parent) - ByContradictionOnMultipleGoals{} -> - "proof by contradiction requires exactly one open goal" - BySetInductionSyntacticMismatch{} -> - "the goal does not have the required set-induction shape" - ByOrdInductionSyntacticMismatch{} -> - "the goal does not have the required ordinal-induction shape" - SetExtensionalityWithTake{} -> - "set extensionality cannot be used after a Take step" - ProofWithoutPrecedingTheorem{} -> - "proof has no preceding theorem" - CouldNotEliminateHigherOrder symbol _term _location _marker -> - "could not eliminate higher-order symbol " - <> Text.pack (show symbol) - UnresolvedStructureOperation symbol _location _marker -> - "unresolved structure operation " <> Text.pack (show symbol) - AmbiguousInductionVar{} -> - "the induction variable is ambiguous" - MismatchedSetExt{} -> - "set extensionality does not match the open goal" - MismatchedAssume{} -> - "assumption does not match the open goal" - CheckingError message _location _marker -> - message - -data LegacyDeclarationAdmissionError - = LegacyFactRegistryIsNotAnExtension !Text - | LegacyFactProducerCountMismatch !Int !Int - | LegacyFactPremiseHasNoAuthorization - !LegacyObligationOrdinal - !Marker - | LegacyPreparedPremiseSelectionMismatch - !LegacyObligationOrdinal - | LegacyStageAdmissionFailed !LegacyModuleStageError - | TransitionStageAdmissionFailed - !Transition.TransitionModuleError - deriving (Show, Eq) - -instance Exception LegacyDeclarationAdmissionError - -throwWithLocationAndMarker :: (Location -> Marker -> CheckingError) -> CheckingM a -throwWithLocationAndMarker err = do - m <- gets blockLabel - loc <- gets stepLocation - throwIO (err loc m) - -throwWithMarker :: (Marker -> CheckingError) -> CheckingM a -throwWithMarker err = do - m <- gets blockLabel - throwIO (err m) - -assume :: [Asm] -> Checking -assume asms = traverse_ go asms - where - go :: Asm -> Checking - go = \case - Asm phi -> do - ctx <- structContextFromAssertion phi - addStructContextAndRefreshGoals ctx - assumeFormula phi - AsmStruct x sp -> - instantiateStruct x sp - -assumeFormula :: Formula -> Checking -assumeFormula phi = do - phi' <- canonicalize phi - let phiContracted = contraction phi' - case phiContracted of - Top -> skip - _ -> do - marker <- nextHypothesisMarker - let hypo = Hypothesis marker phi' - location <- gets stepLocation - declarationMarker <- gets blockLabel - modify \st -> - st - { checkingAssumptions = - CurrentHypothesis - hypo - location - declarationMarker - : checkingAssumptions st - } - -instantiateStruct :: VarSymbol -> StructPhrase -> Checking -instantiateStruct x sp = do - ctx <- structContextFor x sp - addStructContextAndRefreshGoals ctx - assumeFormula (structPredicate x sp) - -structPredicate :: VarSymbol -> StructPhrase -> Formula -structPredicate x sp = - TermSymbol Nowhere (SymbolPredicate (PredicateNounStruct sp)) [TermVar x] - -structContextFromAssertion :: Formula -> CheckingM StructContext -structContextFromAssertion = \case - TermSymbol _ (SymbolPredicate (PredicateNounStruct sp)) [TermVar x] -> - structContextFor x sp - _ -> - pure mempty - -structContextFor :: VarSymbol -> StructPhrase -> CheckingM StructContext -structContextFor x sp = do - structGraph <- gets checkingStructs - case StructGraph.lookupSymbols sp structGraph of - Nothing -> - throwWithLocationAndMarker (UnknownStructureParent sp) - Just symbols -> - pure (structContextFromSymbols x symbols) - -structContextFromSymbols :: VarSymbol -> Set StructSymbol -> StructContext -structContextFromSymbols x symbols = - StructContext (Set.singleton x) (HM.fromList [(op, x) | op <- Set.toList symbols]) - -addStructContext :: StructContext -> Checking -addStructContext ctx = - modify \st -> st - { checkingStructContext = ctx <> checkingStructContext st - } - -addStructContextAndRefreshGoals :: StructContext -> Checking -addStructContextAndRefreshGoals ctx - | structContextIsEmpty ctx = skip - | otherwise = do - addStructContext ctx - goals <- gets checkingGoals - setGoals goals - -structContextIsEmpty :: StructContext -> Bool -structContextIsEmpty StructContext{..} = - Set.null structContextLabels && HM.null structContextOps - -registerAssumptionStructContexts :: [Asm] -> Checking -registerAssumptionStructContexts asms = do - ctx <- assumptionStructContext asms - addStructContext ctx - -assumptionStructContext :: [Asm] -> CheckingM StructContext -assumptionStructContext asms = do - contexts <- traverse asmStructContext asms - pure (foldl' (\older newer -> newer <> older) mempty contexts) - -asmStructContext :: Asm -> CheckingM StructContext -asmStructContext = \case - Asm phi -> - structContextFromAssertion phi - AsmStruct x sp -> - structContextFor x sp - - -setLocation :: Location -> Checking -setLocation loc = modify \st -> st{stepLocation = loc} - - --- | Replace all current goals with a new goal. Use with care! -setGoals :: [Formula] -> Checking -setGoals goals = do - goals <- traverse canonicalize goals - modify $ \st -> st{checkingGoals = goals} - -nextHypothesisMarker :: CheckingM Marker -nextHypothesisMarker = do - st <- get - let next = checkingHypothesisCounter st + 1 - let marker = Marker ("_local_" <> Text.pack (show next)) - put st{checkingHypothesisCounter = next} - pure marker - -registerLemmaLocalVars :: [Asm] -> Formula -> Checking -registerLemmaLocalVars asms goal = - addLocalVars (Set.unions (freeVars goal : (asmLocalVars <$> asms))) - -asmLocalVars :: Asm -> Set VarSymbol -asmLocalVars = \case - Asm phi -> - freeVars phi - AsmStruct x _ -> - Set.singleton x - -addLocalVars :: Set VarSymbol -> Checking -addLocalVars vars = - modify \st -> st{localVars = vars <> localVars st} - -checkFreshLocalVars :: Text -> [VarSymbol] -> Checking -checkFreshLocalVars context vars = do - let duplicates = duplicateVars vars - unless (Set.null duplicates) do - throwCheckingError (context <> " introduces the same variable more than once: " <> formatVars duplicates) - inScope <- gets localVars - let shadowed = Set.fromList vars `Set.intersection` inScope - unless (Set.null shadowed) do - throwCheckingError (context <> " tries to introduce variable(s) already in scope: " <> formatVars shadowed) - -checkBinderVarsFresh :: Text -> [VarSymbol] -> Checking -checkBinderVarsFresh context vars = do - let duplicates = duplicateVars vars - unless (Set.null duplicates) do - throwCheckingError (context <> " uses the same binder variable more than once: " <> formatVars duplicates) - inScope <- gets localVars - let shadowed = Set.fromList vars `Set.intersection` inScope - unless (Set.null shadowed) do - throwCheckingError (context <> " binder variable(s) shadow local variable(s): " <> formatVars shadowed) - -assertKnownFormulaVars :: Text -> Formula -> Checking -assertKnownFormulaVars context phi = do - known <- gets localVars - assertKnownFormulaVarsWith context known phi - -assertKnownFormulaVarsWith :: Text -> Set VarSymbol -> Formula -> Checking -assertKnownFormulaVarsWith context known phi = do - let unknown = freeVars phi `Set.difference` known - unless (Set.null unknown) do - throwCheckingError (context <> " mentions variable(s) that are not in scope: " <> formatVars unknown) - -assertKnownTermVars :: Text -> Term -> Checking -assertKnownTermVars = assertKnownFormulaVars - -assertKnownTermVarsWith :: Text -> Set VarSymbol -> Term -> Checking -assertKnownTermVarsWith = assertKnownFormulaVarsWith - -throwCheckingError :: Text -> CheckingM a -throwCheckingError msg = - throwWithLocationAndMarker (CheckingError msg) - -duplicateVars :: [VarSymbol] -> Set VarSymbol -duplicateVars = - snd . foldl' step (Set.empty, Set.empty) - where - step (seen, duplicates) x - | x `Set.member` seen = (seen, Set.insert x duplicates) - | otherwise = (Set.insert x seen, duplicates) - -formatVars :: Set VarSymbol -> Text -formatVars vars = - Text.intercalate ", " (formatVar <$> Set.toList vars) - -formatVar :: VarSymbol -> Text -formatVar = \case - NamedVar x -> x - FreshVar n -> "_" <> Text.pack (show n) - -formatSymbols :: Set Symbol -> Text -formatSymbols symbols = - Text.intercalate ", " (symbolText <$> Set.toList symbols) - -ownableSymbol :: Symbol -> Bool -ownableSymbol = - isJust . objectSymbolMarker - -markerTextOf :: Marker -> Text -markerTextOf (Marker text) = text - -symbolText :: Symbol -> Text -symbolText = \case - SymbolMixfix symbol -> - markerTextOf (mixfixMarker symbol) - SymbolFun symbol -> - markerTextOf (lexicalItemSgPlMarker symbol) - SymbolInteger n -> - Text.pack (show n) - SymbolPredicate predicate -> - predicateText predicate - -predicateText :: Predicate -> Text -predicateText = - markerTextOf . predicateObjectMarker - -symbolOwnerKindText :: SymbolOwnerKind -> Text -symbolOwnerKindText = \case - OwnedByBuiltin -> - "builtin" - OwnedBySignaturePredicate -> - "signature predicate" - OwnedBySignatureFormula -> - "signature formula" - OwnedByAbbreviation -> - "abbreviation" - OwnedByPredicateDefinition -> - "predicate definition" - OwnedByFunctionDefinition -> - "function definition" - OwnedByOperatorDefinition -> - "operator definition" - OwnedByDatatypeHead -> - "datatype" - OwnedByDatatypeConstructor -> - "datatype constructor" - OwnedByInductiveDefinition -> - "inductive definition" - OwnedByStructureDefinition -> - "structure definition" - -symbolOwnerText :: SymbolOwner -> Text -symbolOwnerText SymbolOwner{symbolOwnerKind, symbolOwnerMarker} = - symbolOwnerKindText symbolOwnerKind - <> " " - <> markerTextOf symbolOwnerMarker - --- Multiple matches can only be builtin aliases, which all have 'builtinOwner'. -symbolOwnerByMarker :: Marker -> HashMap Symbol SymbolOwner -> Maybe SymbolOwner -symbolOwnerByMarker marker owners = - snd <$> List.find ((== Just marker) . objectSymbolMarker . fst) (HM.toList owners) - -validatedOwnership - :: Marker - -> SymbolOwnerKind - -> Symbol - -> CheckingState - -> Either Text (HashMap Symbol SymbolOwner, HashSet Marker) -validatedOwnership currentMarker ownerKind symbol st = do - marker <- - maybe - (Left ("symbol has no object marker: " <> symbolText symbol)) - Right - (objectSymbolMarker symbol) - let owners = checkingOwnedSymbols st - for_ (HM.lookup symbol owners) \owner -> - Left - ( "symbol " - <> symbolText symbol - <> " is already owned by " - <> symbolOwnerText owner - ) - let ownedMarkers = checkingOwnedSymbolMarkers st - when (marker `HS.member` ownedMarkers) do - Left - ( "object-symbol marker " - <> markerTextOf marker - <> " is already owned" - <> maybe - "" - ((" by " <>) . symbolOwnerText) - (symbolOwnerByMarker marker owners) - ) - case HM.lookup symbol (checkingFrozenSymbols st) of - Just frozenBy | frozenBy /= currentMarker -> - Left - ( "symbol " - <> symbolText symbol - <> " is frozen by inductive block " - <> markerTextOf frozenBy - <> " and cannot be defined here" - ) - _ -> - Right - ( HM.insert - symbol - (SymbolOwner ownerKind currentMarker) - owners - , HS.insert marker ownedMarkers - ) - -dependencyRegistrationErrorText - :: Symbol - -> Dependencies.DependencyRegistrationError - -> Text -dependencyRegistrationErrorText owner = \case - Dependencies.DependencyOwnerAlreadyRegistered _ -> - "dependencies are already registered for symbol " <> symbolText owner - Dependencies.SelfDependency _ -> - "definition of symbol " <> symbolText owner <> " is self-referential" - Dependencies.UnknownDependency unknown -> - "definition of symbol " - <> symbolText owner - <> " depends on unknown symbol " - <> symbolText unknown - -validatedSymbolRegistration - :: BlockContext - -> SymbolOwnerKind - -> Symbol - -> Set Symbol - -> CheckingState - -> Either - CheckingError - ( HashMap Symbol SymbolOwner - , HashSet Marker - , Dependencies.DependencyRegistry - ) -validatedSymbolRegistration context ownerKind symbol dependencies st = - case objectSymbolMarker symbol of - Nothing -> - Right - ( checkingOwnedSymbols st - , checkingOwnedSymbolMarkers st - , checkingDependencies st - ) - Just _marker -> do - (owners', ownedMarkers') <- - first - (checkingErrorAt context) - (validatedOwnership - (blockContextMarker context) - ownerKind - symbol - st) - dependencies' <- - first - ( checkingErrorAt context - . dependencyRegistrationErrorText symbol - ) - (Dependencies.registerDependencies - symbol - (Set.filter ownableSymbol dependencies) - (checkingDependencies st)) - pure (owners', ownedMarkers', dependencies') - -validateOwnedDependenciesAt - :: BlockContext - -> HashMap Symbol SymbolOwner - -> Set Symbol - -> Either CheckingError () -validateOwnedDependenciesAt context owners dependencies = - unless (Set.null unknown) do - Left - (checkingErrorAt - context - ( "top-level fact mentions symbol(s) without prior ownership: " - <> formatSymbols unknown - )) - where - unknown = - Set.filter - (\symbol -> - ownableSymbol symbol - && not (HM.member symbol owners)) - dependencies - -validatePreparedSemanticFact - :: BlockContext - -> HashMap Symbol SymbolOwner - -> Dependencies.DependencyRegistry - -> Facts.PreparedSemanticFact - -> Either CheckingError () -validatePreparedSemanticFact context owners dependencies prepared = do - validateOwnedDependenciesAt context owners semanticDependencies - unless (Set.null unknownDependencies) do - Left - (checkingErrorAt - context - ( "top-level fact depends on unknown symbol(s): " - <> formatSymbols unknownDependencies - )) - where - semanticDependencies = - Facts.preparedSemanticDependencies prepared - unknownDependencies = - Set.filter - (\symbol -> - ownableSymbol symbol - && isNothing - (Dependencies.lookupDependencies - symbol - dependencies)) - semanticDependencies - -checkedInductiveMentionedSymbols :: CheckedInductive -> Set Symbol -checkedInductiveMentionedSymbols CheckedInductive{checkedInductiveSymbol, checkedInductiveDomain, checkedInductiveIntros} = - Set.insert - (SymbolMixfix checkedInductiveSymbol) - ( mentionedSymbols checkedInductiveDomain - <> Set.unions (checkedInductiveIntroMentionedSymbols <$> NonEmpty.toList checkedInductiveIntros) - ) - -checkedInductiveIntroMentionedSymbols :: CheckedInductiveIntro -> Set Symbol -checkedInductiveIntroMentionedSymbols CheckedInductiveIntro{checkedInductiveIntroConditions, checkedInductiveIntroResultTerm} = - mentionedSymbols checkedInductiveIntroResultTerm - <> Set.unions (checkedInductiveConditionMentionedSymbols <$> checkedInductiveIntroConditions) - -checkedInductiveConditionMentionedSymbols :: CheckedInductiveCondition -> Set Symbol -checkedInductiveConditionMentionedSymbols = \case - CheckedInductiveSideCondition phi -> - mentionedSymbols phi - CheckedInductiveRecursiveCondition{checkedInductiveRecursiveTerm, checkedInductiveRecursiveCarrierTemplate} -> - mentionedSymbols checkedInductiveRecursiveTerm - <> mentionedSymbols (fromScope checkedInductiveRecursiveCarrierTemplate) - -formatSymbolPath :: NonEmpty Symbol -> Text -formatSymbolPath = - Text.intercalate " -> " . fmap symbolText . toList - -definitionParts :: Defn -> (SymbolOwnerKind, Symbol, [Asm], Expr) -definitionParts = \case - DefnPredicate asms predicate _vs body -> - (OwnedByPredicateDefinition, SymbolPredicate predicate, asms, body) - DefnFun asms fun _vs rhs -> - (OwnedByFunctionDefinition, SymbolFun fun, asms, rhs) - DefnOp op _vs rhs -> - (OwnedByOperatorDefinition, SymbolMixfix op, [], rhs) - -checkedDefinitionDependencies :: Symbol -> [Asm] -> Expr -> CheckingM (Set Symbol) -checkedDefinitionDependencies symbol asms definiens = do - assumptionFormulas <- traverse asmFormula asms - expandedAssumptions <- traverse unabbreviate assumptionFormulas - expandedDefiniens <- unabbreviate definiens - let dependencies = - mentionedSymbols expandedDefiniens - <> Set.unions (mentionedSymbols <$> expandedAssumptions) - when (symbol `Set.member` dependencies) do - throwCheckingError - ("definition of symbol " <> symbolText symbol <> " is self-referential") - pure dependencies - -checkDatatype :: BlockContext -> Syntax.Internal.Datatype -> Checking -checkDatatype context datatype = do - structContext <- gets checkingStructContext - checked <- - Datatype.prepareCheckedDatatype - (canonicalizeWithAt context structContext) - datatype - >>= either - ( throwIO - . checkingErrorAt context - . Datatype.renderDatatypeValidationError - ) - pure - st <- get - committed <- - either - throwIO - pure - (commitCheckedDatatype context checked st) - putDeclarationCandidate committed - setDeclarationFactProducers - ( LegacyDeclarationRuleProducer - . LegacyDatatypeRule - <$> NonEmpty.toList - (Datatype.checkedDatatypeFactRoles checked) - ) - --- | Validate and commit every state row introduced by one datatype. -commitCheckedDatatype - :: BlockContext - -> Datatype.CheckedDatatype - -> CheckingState - -> Either CheckingError CheckingState -commitCheckedDatatype context checked st = do - blockMarkers <- - validatedMarkers - location - [blockMarker] - st - (owners', ownedMarkers') <- - foldM validateOwner - (checkingOwnedSymbols st, checkingOwnedSymbolMarkers st) - ownedSymbols - markers' <- - validatedMarkers - location - factMarkers - st{definedMarkers = blockMarkers} - dependencies' <- - foldM registerDependency - (checkingDependencies st) - (snd <$> ownedSymbols) - traverse_ - (validatePreparedDatatypeFact - context - owners' - dependencies') - (Facts.stagedFactSemantic <$> stagedFacts) - facts' <- - first - (DuplicateMarker location) - (Facts.registerStagedFacts - stagedFacts - (checkingFacts st)) - pure - st - { checkingFacts = facts' - , checkingDependencies = dependencies' - , checkingOwnedSymbols = owners' - , checkingOwnedSymbolMarkers = ownedMarkers' - , definedMarkers = markers' - , blockLabel = blockMarker - , stepLocation = location - , checkingHypothesisCounter = 0 - } - where - location = blockContextLocation context - blockMarker = blockContextMarker context - stagedFacts = - Datatype.checkedDatatypeFacts location blockMarker checked - factMarkers = - toList (stagedFacts >>= Facts.stagedFactAliases) - ownedSymbols = - ( OwnedByDatatypeHead - , Datatype.checkedDatatypeHeadSymbol checked - ) - : [ (OwnedByDatatypeConstructor, symbol) - | symbol <- - toList - (Datatype.checkedDatatypeConstructorSymbols checked) - ] - - validateOwner - (owners, ownedMarkers) - (ownerKind, symbol) = - first - (checkingErrorAt context) - (validatedOwnership - blockMarker - ownerKind - symbol - st - { checkingOwnedSymbols = owners - , checkingOwnedSymbolMarkers = ownedMarkers - }) - - registerDependency dependencies symbol = - first - ( checkingErrorAt context - . dependencyRegistrationErrorText symbol - ) - (Dependencies.registerDependencies - symbol - mempty - dependencies) - -validatePreparedDatatypeFact - :: BlockContext - -> HashMap Symbol SymbolOwner - -> Dependencies.DependencyRegistry - -> Facts.PreparedSemanticFact - -> Either CheckingError () -validatePreparedDatatypeFact context owners dependencies prepared = - case Set.lookupMin unknownOwners of - Just _unknown -> - Left - (checkingErrorAt - context - ( "top-level fact mentions symbol(s) without prior ownership: " - <> formatSymbols unknownOwners - )) - Nothing -> - case Set.lookupMin unknownDependencies of - Nothing -> - Right () - Just unknown -> - Left - (checkingErrorAt - context - ( "datatype fact depends on unknown symbol " - <> symbolText unknown - )) - where - semanticDependencies = - Facts.preparedSemanticDependencies prepared - unknownOwners = - Set.filter - (\symbol -> - requiresDatatypeOwnership symbol - && not (HM.member symbol owners)) - semanticDependencies - unknownDependencies = - Set.filter - (\symbol -> - requiresDatatypeOwnership symbol - && isNothing - (Dependencies.lookupDependencies - symbol - dependencies)) - semanticDependencies - - -- Exact fixed terms do not require a legacy source declaration. - requiresDatatypeOwnership symbol = - ownableSymbol symbol - && case ExactVocabulary.classifyExactSymbol symbol of - ExactVocabulary.ExactFixedPrimitive{} -> False - _ -> True - -functionSymbolText :: FunctionSymbol -> Text -functionSymbolText symbol = case mixfixMarker symbol of - Marker name -> name - -freshDatatypeVar :: Set VarSymbol -> Text -> VarSymbol -freshDatatypeVar used base = - List.head - [ NamedVar candidate - | candidate <- base : [base <> Text.pack (show n) | n <- [(1 :: Int)..]] - , NamedVar candidate `Set.notMember` used - ] - -freshGeneratedVar :: Set VarSymbol -> Text -> VarSymbol -freshGeneratedVar = freshDatatypeVar - -forallIfNeeded :: [VarSymbol] -> Formula -> Formula -forallIfNeeded [] phi = phi -forallIfNeeded xs phi = makeForall xs phi - -existsIfNeeded :: [VarSymbol] -> Formula -> Formula -existsIfNeeded [] phi = phi -existsIfNeeded xs phi = makeExists xs phi - -impliesFrom :: [Formula] -> Formula -> Formula -impliesFrom [] conclusion = conclusion -impliesFrom premises conclusion = makeConjunction premises `Implies` conclusion - - --- | Prepare one complete current goal batch. -tellTasks :: Checking -tellTasks = - emitCurrentObligations ProveWithVampire - -omitCurrentGoals :: Location -> Checking -omitCurrentGoals location = do - emitCurrentObligations (RecordExplicitGap location) - setGoals [] - -emitCurrentObligations :: ObligationMethod -> Checking -emitCurrentObligations method = do - goals <- gets checkingGoals - marker <- gets blockLabel - facts <- gets checkingFacts - assumptions <- gets checkingAssumptions - directness <- gets checkingDirectness - location <- gets stepLocation - firstOrdinal <- gets checkingNextObligationOrdinal - prepareTask <- gets checkingPrepareTask - batchHandler <- gets checkingObligationBatchHandler - legacyStage <- gets checkingLegacyModuleStage - let premises = - factPremises legacyStage facts - <> (currentHypothesisPremise <$> assumptions) - (batch, nextOrdinal) = - case method of - ProveWithVampire -> - prepareObligationBatch - prepareTask - firstOrdinal - premises - directness - marker - location - goals - RecordExplicitGap gapLocation -> - prepareOmittedObligationBatch - prepareTask - firstOrdinal - premises - directness - marker - gapLocation - goals - modify \st -> - st - { checkingNextObligationOrdinal = - nextOrdinal - } - case batchHandler of - ObserveObligationBatches emitBatch -> - liftIO (emitBatch batch) - ResolveObligationBatches resolveBatch -> do - resolved <- liftIO (resolveBatch batch) - modify \st -> - st - { checkingResolvedObligationBatches = - checkingResolvedObligationBatches st - <> [resolved] - } - -factPremises - :: Maybe LegacyModuleStage - -> Facts.FactRegistry - -> [PreparedPremise] -factPremises legacyStage facts = - [ preparedPremise - (Hypothesis marker (Facts.preparedSemanticStatement fact)) - (case legacyStage >>= lookupLegacyStageFact marker of - Nothing -> - RegisteredFactPremise origin - Just entry -> - RegisteredLegacyFactPremise - (legacyFactEntryReference entry) - origin - (legacyFactEntryTrustDependencies entry)) - | (marker, fact, origin) <- - Facts.registeredFactsWithOrigins facts - ] - -factHypotheses :: Facts.FactRegistry -> [Hypothesis] -factHypotheses = - fmap preparedPremiseHypothesis . factPremises Nothing - -currentHypothesisPremise :: CurrentHypothesis -> PreparedPremise -currentHypothesisPremise - (CurrentHypothesis hypothesis location marker) = - preparedPremise - hypothesis - (LocalHypothesisPremise location marker) - -stagePreparedFact - :: Location - -> Marker - -> Marker - -> Facts.PreparedSemanticFact - -> Facts.StagedFact -stagePreparedFact loc blockMarker factMarker = - Facts.stageFact - (factMarker :| []) - (Facts.factOrigin loc blockMarker) - -validatedMarkers - :: Location - -> [Marker] - -> CheckingState - -> Either CheckingError (HashSet Marker) -validatedMarkers loc markers st = - case firstDuplicateMarker (definedMarkers st) HS.empty markers of - Just marker -> - Left (DuplicateMarker loc marker) - Nothing -> - Right (foldr HS.insert (definedMarkers st) markers) - -firstDuplicateMarker - :: HashSet Marker - -> HashSet Marker - -> [Marker] - -> Maybe Marker -firstDuplicateMarker _seenGlobals _seenLocals [] = - Nothing -firstDuplicateMarker seenGlobals seenLocals (marker:rest) - | HS.member marker seenGlobals || HS.member marker seenLocals = - Just marker - | otherwise = - firstDuplicateMarker - seenGlobals - (HS.insert marker seenLocals) - rest - - - -canonicalizedFactWithAsms :: [Asm] -> Formula -> CheckingM Formula -canonicalizedFactWithAsms asms stmt = do - (asms', structContext) <- mergeAssumptions asms - asms'' <- traverse (canonicalizeWith structContext) asms' - stmt' <- canonicalizeWith structContext stmt - pure - (case asms'' of - [] -> forallClosure mempty stmt' - _ -> forallClosure mempty (makeConjunction asms'' `Implies` stmt') - ) - -unabbreviateWith :: (forall a. HashMap Symbol (Scope Int ExprOf a)) -> (forall b. ExprOf b -> ExprOf b) -unabbreviateWith abbrs = unabbr - where - unabbr :: ExprOf b -> ExprOf b - unabbr = \case - TermSymbol loc sym es -> - let es' = unabbr <$> es - in case HM.lookup sym abbrs of - Nothing -> TermSymbol loc sym es' - Just scope -> - unabbr - (instantiate - (\k -> - nth k es - ?? impossible - "abbreviation index exceeds application arity") - scope) - Not loc e -> - Not loc (unabbr e) - Apply e es -> - Apply (unabbr e) (unabbr <$> es) - TermSep vs e scope -> - TermSep vs (unabbr e) (hoistScope unabbr scope) - ReplacePred y x xB scope -> - ReplacePred y x (unabbr xB) (hoistScope unabbr scope) - ReplaceFun bounds scope cond -> - ReplaceFun ((\(x, e) -> (x, unabbr e)) <$> bounds) (hoistScope unabbr scope) (hoistScope unabbr cond) - Connected con e1 e2 -> - Connected con (unabbr e1) (unabbr e2) - Lambda scope -> - Lambda (hoistScope unabbr scope) - Quantified quant scope -> - Quantified quant (hoistScope unabbr scope) - e@PropositionalConstant{} -> - e - e@TermVar{} -> - e - TermSymbolStruct symb e -> - TermSymbolStruct symb (unabbr <$> e) - -mentionsSymbol :: Symbol -> ExprOf a -> Bool -mentionsSymbol target = \case - TermVar{} -> - False - TermSymbol _loc sym es -> - sym == target || any (mentionsSymbol target) es - TermSymbolStruct _symb e -> - maybe False (mentionsSymbol target) e - Apply e es -> - mentionsSymbol target e || any (mentionsSymbol target) es - TermSep _x bound scope -> - mentionsSymbol target bound || mentionsSymbol target (fromScope scope) - ReplacePred _y _x bound scope -> - mentionsSymbol target bound || mentionsSymbol target (fromScope scope) - ReplaceFun bounds lhs cond -> - any (mentionsSymbol target . snd) bounds - || mentionsSymbol target (fromScope lhs) - || mentionsSymbol target (fromScope cond) - Connected _conn e1 e2 -> - mentionsSymbol target e1 || mentionsSymbol target e2 - Lambda scope -> - mentionsSymbol target (fromScope scope) - Quantified _quant scope -> - mentionsSymbol target (fromScope scope) - PropositionalConstant{} -> - False - Not _loc e -> - mentionsSymbol target e - --- | Unroll supported comprehensions in equations and reject leftover ones. --- E.g. /@B = \\{f(a) | a\\in A \\}@/ turns into --- /@\\forall b. b\\in B \\iff \\exists a\\in A. b = f(a)@/. -desugarComprehensionsAt - :: BlockContext - -> ExprOf a - -> CheckingM (ExprOf a) -desugarComprehensionsAt context = go - where - go :: forall b. ExprOf b -> CheckingM (ExprOf b) - go = \case - -- We only desugar comprehensions directly under equations. - -- Any remaining comprehension is currently unsupported. - e@TermSep{} -> - reject e - e@ReplacePred{} -> - reject e - e@ReplaceFun{} -> - reject e - e@TermVar{} -> - pure e - e@PropositionalConstant{} -> - pure e - TermSymbolStruct symbol Nothing -> - throwIO - (UnresolvedStructureOperation - symbol - (blockContextLocation context) - (blockContextMarker context)) - TermSymbolStruct symbol (Just argument) -> - TermSymbolStruct symbol . Just <$> go argument - -- - Equals _pos e (TermSep x bound scope) -> - go (desugarSeparation e x bound scope) - Equals _pos (TermSep x bound scope) e -> - go (desugarSeparation e x bound scope) - -- - Equals _pos e (ReplaceFun bounds scope cond) -> - go (makeReplacementIff (F <$> e) bounds scope cond) - Equals _pos (ReplaceFun bounds scope cond) e -> - go (makeReplacementIff (F <$> e) bounds scope cond) - -- - Apply e es -> - Apply <$> go e <*> traverse go es - Not loc e -> - Not loc <$> go e - TermSymbol loc sym es -> - TermSymbol loc sym <$> traverse go es - Connected conn e1 e2 -> - Connected conn <$> go e1 <*> go e2 - Lambda scope -> - Lambda <$> transverseScope go scope - Quantified quant scope -> - Quantified quant <$> transverseScope go scope - - reject :: ExprOf a -> CheckingM b - reject _ = - throwIO - (CheckingError - "Could not eliminate set comprehensions in this step. Nested comprehensions are not supported yet." - (blockContextLocation context) - (blockContextMarker context)) - - desugarSeparation - :: ExprOf a - -> VarSymbol - -> ExprOf a - -> Scope () ExprOf a - -> ExprOf a - desugarSeparation e x bound scope = - let phi = isElementOf (TermVar (B x)) (F <$> e) - psi = isElementOf (TermVar (B x)) (F <$> bound) - rho = fromScope (mapBound (const x) scope) - in Quantified Universally (toScope (phi `Iff` (psi `And` rho))) - - - - -checkBlocks :: [Block] -> Checking -checkBlocks = \case - BlockAxiom loc marker axiom : blocks -> do - let context = BlockContext loc marker - withBlockContext context (checkAxiom context axiom) - checkBlocks blocks - BlockDefn loc marker defn : blocks -> do - let context = BlockContext loc marker - withBlockContext context (checkDefn context defn) - checkBlocks blocks - BlockAbbr loc marker abbr : blocks -> do - let context = BlockContext loc marker - withBlockContext context (checkAbbr context abbr) - checkBlocks blocks - BlockLemma loc marker lemma : BlockProof _startLoc endLoc proof : blocks -> do - modify \st -> st{blockEndLocation = endLoc} - let context = BlockContext loc marker - withBlockContext - context - (checkLemmaWithProof context lemma proof) - checkBlocks blocks - BlockLemma loc marker lemma : blocks -> do - let context = BlockContext loc marker - withBlockContext context (checkLemma context lemma) - checkBlocks blocks - BlockProof startLoc _endLoc _proof : _ -> - throwWithMarker (ProofWithoutPrecedingTheorem startLoc) - BlockSig loc marker asms sig : blocks -> do - let context = BlockContext loc marker - withBlockContext context (checkSig context asms sig) - checkBlocks blocks - BlockData loc marker datatype : blocks -> do - let context = BlockContext loc marker - withBlockContext context (checkDatatype context datatype) - checkBlocks blocks - BlockInductive loc marker inductiveDefn : blocks -> do - let context = BlockContext loc marker - withBlockContext - context - (checkInductive context inductiveDefn) - checkBlocks blocks - BlockStruct loc marker structDefn : blocks -> do - let context = BlockContext loc marker - withBlockContext context (checkStructDefn context structDefn) - checkBlocks blocks - [] -> skip - --- | Make a block's diagnostic context current without publishing its label. -withBlockContext :: BlockContext -> CheckingM a -> CheckingM a -withBlockContext BlockContext{blockContextLocation, blockContextMarker} ma = do - previous <- get - modify \st -> - st - { blockLabel = blockContextMarker - , stepLocation = blockContextLocation - , checkingHypothesisCounter = 0 - , checkingNextObligationOrdinal = - legacyObligationOrdinal 0 - , checkingResolvedObligationBatches = [] - , checkingDeclarationFactProducers = [] - , checkingTransitionModuleBuilder = - Transition.beginTransitionDeclaration - <$> checkingTransitionModuleBuilder st - } - result <- ma - finalizeLegacyDeclaration previous - pure result - -setDeclarationFactProducers - :: [LegacyFactProducer] - -> Checking -setDeclarationFactProducers producers = - modify \st -> - st{checkingDeclarationFactProducers = producers} - -putDeclarationCandidate :: CheckingState -> Checking -putDeclarationCandidate candidate = do - current <- get - put - candidate - { checkingHypothesisCounter = - checkingHypothesisCounter current - , checkingNextObligationOrdinal = - checkingNextObligationOrdinal current - , checkingResolvedObligationBatches = - checkingResolvedObligationBatches current - , checkingDeclarationFactProducers = - checkingDeclarationFactProducers current - } - -finalizeLegacyDeclaration :: CheckingState -> Checking -finalizeLegacyDeclaration previous = do - current <- get - case checkingLegacyModuleStage current of - Nothing -> - pure () - Just stage -> do - stagedFacts <- - either - (throwIO - . LegacyFactRegistryIsNotAnExtension) - pure - (Facts.factRegistryExtension - (checkingFacts previous) - (checkingFacts current)) - let producers = - checkingDeclarationFactProducers current - unless - (length producers == length stagedFacts) - (throwIO - (LegacyFactProducerCountMismatch - (length producers) - (length stagedFacts))) - case stagedFacts of - [] -> - pure () - firstStaged : remainingStaged -> do - reservation <- - either - (throwIO - . LegacyStageAdmissionFailed) - pure - (reserveLegacyDeclaration - (firstStaged :| remainingStaged) - stage) - admitted <- - authorizeLegacyDeclaration - stage - reservation - producers - (checkingResolvedObligationBatches - current) - stage' <- - either - (throwIO - . LegacyStageAdmissionFailed) - pure - (appendEstablishedLegacyDeclaration - reservation - admitted - stage) - unless - (legacyStageFactRegistry stage' - == checkingFacts current) - (throwIO - (LegacyFactRegistryIsNotAnExtension - "checker and legacy-stage fact registries diverged")) - transitionBuilder' <- - traverse - (either - (throwIO - . TransitionStageAdmissionFailed) - pure - . Transition.transitionBuilderWithLegacyStage - stage') - (checkingTransitionModuleBuilder - current) - put - current - { checkingLegacyModuleStage = - Just stage' - , checkingTransitionModuleBuilder = - transitionBuilder' - } - -authorizeLegacyDeclaration - :: LegacyModuleStage - -> LegacyDeclarationReservation - -> [LegacyFactProducer] - -> [ResolvedObligationBatch] - -> CheckingM (NonEmpty H1LegacyAdmittedFact) -authorizeLegacyDeclaration stage reservation producers batches = do - established <- - traverse - (establishedLegacyObligation - (legacyStageModuleOrdinal stage)) - [ (batch, obligation) - | batch <- batches - , obligation <- - Vector.toList - (resolvedBatchObligations batch) - ] - let reserved = - NonEmpty.toList - (legacyReservedFacts reservation) - authorizationInputs = - zip producers reserved - admitted <- - traverse - (authorizeOne established) - authorizationInputs - case admitted of - firstAdmitted : remainingAdmitted -> - pure (firstAdmitted :| remainingAdmitted) - [] -> - impossible - "nonempty legacy reservation produced no admitted facts" - where - authorizeOne established (producer, reserved) = - case producer of - LegacyDeclaredAssumptionProducer kind -> - pure - (authorizeLegacyDeclaredAssumption - stage - kind - reserved) - LegacyDirectObligationProducer -> - case directLegacyAuthorization - reserved - batches - established of - Just admitted -> - pure admitted - Nothing -> - pure - (authorizeLegacyRule - (LegacyTheoremRule - LegacyOrdinaryTheoremFinalization) - (legacyEstablishedPredecessors - established) - (foldMap - establishedLegacyTrust - established) - reserved) - LegacyDeclarationRuleProducer tag -> - pure - (authorizeLegacyRule - tag - (legacyEstablishedPredecessors - established) - (foldMap - establishedLegacyTrust - established) - reserved) - -data EstablishedLegacyObligation = EstablishedLegacyObligation - !ResolvedObligation - !SessionLegacyObligationRef - !Marker - !(Vector LegacyFactRef) - !LegacyTrustDependencies - !LegacyTrustDependencies - -establishedLegacyTrust - :: EstablishedLegacyObligation - -> LegacyTrustDependencies -establishedLegacyTrust - (EstablishedLegacyObligation - _resolved - _reference - _marker - _factPredecessors - _predecessorTrust - trust) = - trust - -legacyEstablishedPredecessors - :: [EstablishedLegacyObligation] - -> Vector (LegacyRulePredecessor LegacyFactRef) -legacyEstablishedPredecessors established = - Vector.fromList - [ predecessor - | EstablishedLegacyObligation - _resolved - obligationReference - _marker - factReferences - _predecessorTrust - _trust <- - established - , predecessor <- - (legacyRuleFactPredecessor - <$> Vector.toList factReferences) - <> [ legacyRuleObligationPredecessor - obligationReference - ] - ] - -establishedLegacyObligation - :: LegacyModuleOrdinal - -> (ResolvedObligationBatch, ResolvedObligation) - -> CheckingM EstablishedLegacyObligation -establishedLegacyObligation moduleOrdinal (batch, resolved) = do - let prepared = - resolvedObligationPrepared resolved - ordinal = - preparedObligationOrdinal prepared - selected = - preparedObligationSelectedPremises prepared - expectedHypotheses = - taskHypotheses - (preparedObligationTask prepared) - unless - ( (preparedPremiseHypothesis - <$> Vector.toList selected) - == expectedHypotheses - ) - (throwIO - (LegacyPreparedPremiseSelectionMismatch - ordinal)) - (factReferences, predecessorTrust) <- - foldM - (collectPremise ordinal) - ([], mempty) - selected - let marker = - preparedBatchMarker - (resolvedBatchPrepared batch) - obligationReference = - sessionLegacyObligationRef - moduleOrdinal - marker - ordinal - trust = - case - ( resolvedObligationVampireRun resolved - , resolvedObligationGapLocation resolved - ) - of - (Just _accepted, Nothing) -> - legacyTrustedVampireTrust - obligationReference - predecessorTrust - (Nothing, Just gapLocation) -> - legacyGapTrust - obligationReference - gapLocation - marker - predecessorTrust - _ -> - impossible - "resolved legacy obligation has no evidence" - pure - (EstablishedLegacyObligation - resolved - obligationReference - marker - (Vector.fromList (reverse factReferences)) - predecessorTrust - trust) - where - collectPremise ordinal (references, trust) premise = - case preparedPremiseOrigin premise of - RegisteredLegacyFactPremise - reference - _origin - premiseTrust -> - pure - ( reference : references - , trust <> premiseTrust - ) - RegisteredFactPremise _origin -> - throwIO - (LegacyFactPremiseHasNoAuthorization - ordinal - (hypothesisMarker - (preparedPremiseHypothesis - premise))) - LocalHypothesisPremise{} -> - pure (references, trust) - -directLegacyAuthorization - :: LegacyReservedFact - -> [ResolvedObligationBatch] - -> [EstablishedLegacyObligation] - -> Maybe H1LegacyAdmittedFact -directLegacyAuthorization reserved batches established = - case (batches, established) of - ([batch], [establishedObligation]) - | Vector.length - (preparedBatchObligations - (resolvedBatchPrepared batch)) - == 1 - , directTarget batch establishedObligation - == reservedTarget -> - directFromEvidence establishedObligation - _ -> - Nothing - where - reservedTarget = - legacyPreparedFormula - (prepareLegacyProposition - (Facts.stagedFactSemantic - (legacyReservedStagedFact reserved))) - - directTarget batch - (EstablishedLegacyObligation - resolved - _reference - _marker - _facts - _predecessorTrust - _trust) = - forallClosure - mempty - (case localPremises of - [] -> - taskConjecture task - _ -> - makeConjunction localPremises - `Implies` taskConjecture task) - where - task = - preparedObligationTask - (resolvedObligationPrepared resolved) - localPremises = - reverse - [ hypothesisFormula - (preparedPremiseHypothesis premise) - | premise <- - Vector.toList - (preparedBatchPremises - (resolvedBatchPrepared batch)) - , LocalHypothesisPremise{} <- - [preparedPremiseOrigin premise] - ] - - directFromEvidence - (EstablishedLegacyObligation - resolved - reference - marker - _factReferences - predecessorTrust - _trust) = - case - ( resolvedObligationVampireRun resolved - , resolvedObligationGapLocation resolved - ) of - (Just accepted, Nothing) -> - Just - (authorizeLegacyTrustedVampire - reference - accepted - predecessorTrust - reserved) - (Nothing, Just gapLocation) -> - Just - (authorizeLegacyGap - reference - gapLocation - marker - predecessorTrust - reserved) - _ -> - Nothing - --- | Verification of a lemma with a proof. --- We skip omitted proofs and treat them as proper gaps of the formalization. --- This is useful when developing a formalization, as it makes it easy to --- leave difficult proofs for later. -checkLemmaWithProof - :: BlockContext - -> Lemma - -> Proof - -> Checking -checkLemmaWithProof context (Lemma asms goal) proof = do - committed <- prepareOrdinaryFactCommit context asms goal - locally do - registerLemmaLocalVars asms goal - registerAssumptionStructContexts asms - assume asms - setGoals [goal] - checkProof proof - putDeclarationCandidate committed - setDeclarationFactProducers - [LegacyDirectObligationProducer] - - --- | Verification of a lemma without a proof. -checkLemma :: BlockContext -> Lemma -> Checking -checkLemma context (Lemma asms goal) = do - staged <- - prepareOrdinaryStagedFact context asms goal - st <- get - case prepareTypedGroundReflexivity context staged st of - Nothing -> do - case prepareTypedAtomicReuse context staged st of - Nothing -> do - committed <- - either - throwIO - pure - (commitOrdinaryFact context staged st) - locally do - registerLemmaLocalVars asms goal - registerAssumptionStructContexts asms - assume asms - setGoals [goal] - tellTasks - putDeclarationCandidate committed - setDeclarationFactProducers - [LegacyDirectObligationProducer] - Just result -> do - committed <- - either throwIO pure result - putDeclarationCandidate committed - setDeclarationFactProducers [] - Just result -> do - committed <- - either throwIO pure result - putDeclarationCandidate committed - setDeclarationFactProducers [] - - -checkAxiom :: BlockContext -> Axiom -> Checking -checkAxiom context (Axiom asms axiom) = do - staged <- - prepareOrdinaryStagedFact context asms axiom - st <- get - case prepareTypedAtomicAssumption context staged st of - Nothing -> do - committed <- - either - throwIO - pure - (commitOrdinaryFact context staged st) - putDeclarationCandidate committed - setDeclarationFactProducers - [ LegacyDeclaredAssumptionProducer - DeclaredUserAxiom - ] - Just result -> do - committed <- - either throwIO pure result - putDeclarationCandidate committed - setDeclarationFactProducers [] - -prepareOrdinaryFactCommit - :: BlockContext - -> [Asm] - -> Formula - -> CheckingM CheckingState -prepareOrdinaryFactCommit context asms statement = do - staged <- - prepareOrdinaryStagedFact - context - asms - statement - st <- get - either - throwIO - pure - (commitOrdinaryFact context staged st) - -prepareOrdinaryStagedFact - :: BlockContext - -> [Asm] - -> Formula - -> CheckingM Facts.StagedFact -prepareOrdinaryStagedFact context asms statement = do - prepared <- - Facts.prepareSemanticFact - <$> canonicalizedFactWithAsms asms statement - pure - (stagePreparedFact - (blockContextLocation context) - (blockContextMarker context) - (blockContextMarker context) - prepared) - -prepareTypedGroundReflexivity - :: BlockContext - -> Facts.StagedFact - -> CheckingState - -> Maybe (Either CheckingError CheckingState) -prepareTypedGroundReflexivity context staged st = do - builder <- - checkingTransitionModuleBuilder st - prepared <- - TypedReflexivity.prepareGroundReflexivity - (Facts.preparedSemanticStatement - (Facts.stagedFactSemantic staged)) - pure do - typed <- - first - (checkingErrorAt context - . ("typed reflexivity preparation failed: " - <>) - . Text.pack - . show) - prepared - markers' <- - validatedMarkers - (blockContextLocation context) - [blockContextMarker context] - st - validatePreparedSemanticFact - context - (checkingOwnedSymbols st) - (checkingDependencies st) - (Facts.stagedFactSemantic staged) - builder' <- - first - (checkingErrorAt context - . ("typed reflexivity admission failed: " - <>) - . Text.pack - . show) - (Transition.commitTransitionKernelFact - (blockContextMarker context :| []) - (Transition.origin - (blockContextLocation context) - Nothing - (Just - (blockContextMarker context))) - (TypedReflexivity.groundReflexivityTarget - typed) - (TypedReflexivity.groundReflexivityDerivation - typed) - builder) - pure - st - { definedMarkers = markers' - , blockLabel = - blockContextMarker context - , stepLocation = - blockContextLocation context - , checkingHypothesisCounter = 0 - , checkingTransitionModuleBuilder = - Just builder' - } - -prepareTypedAtomicAssumption - :: BlockContext - -> Facts.StagedFact - -> CheckingState - -> Maybe (Either CheckingError CheckingState) -prepareTypedAtomicAssumption context staged st = do - builder <- - checkingTransitionModuleBuilder st - preparation <- - TypedAtomic.prepareClosedAtomic - (`Transition.lookupTransitionGlobal` builder) - (Facts.preparedSemanticStatement - (Facts.stagedFactSemantic staged)) - pure do - prepared <- - first - (typedFactError - context - "typed atomic preparation failed: ") - preparation - markers' <- - validateTypedFactState - context - staged - st - builder' <- - first - (typedFactError - context - "typed declared-assumption registration failed: ") - (Transition.commitTransitionTypedDeclaredAssumption - (blockContextMarker context :| []) - (typedFactOrigin context) - DeclaredUserAxiom - (TypedAtomic.closedAtomicStatement - prepared) - builder) - pure - (publishTypedFactState - context - markers' - builder' - st) - -prepareTypedAtomicReuse - :: BlockContext - -> Facts.StagedFact - -> CheckingState - -> Maybe (Either CheckingError CheckingState) -prepareTypedAtomicReuse context staged st = do - builder <- - checkingTransitionModuleBuilder st - preparation <- - TypedAtomic.prepareClosedAtomic - (`Transition.lookupTransitionGlobal` builder) - (Facts.preparedSemanticStatement - (Facts.stagedFactSemantic staged)) - case preparation of - Left err -> - Just - (Left - (typedFactError - context - "typed atomic preparation failed: " - err)) - Right prepared -> do - let target = - TypedAtomic.closedAtomicStatement - prepared - case Transition.lookupTransitionTypedImport - target - builder of - Left err -> - Just - (Left - (typedFactError - context - "typed import lookup failed: " - err)) - Right Nothing -> - Nothing - Right (Just imported) -> - pure do - markers' <- - validateTypedFactState - context - staged - st - builder' <- - first - (typedFactError - context - "typed imported-fact admission failed: ") - (Transition.commitTransitionKernelFactWithImports - (blockContextMarker context :| []) - (typedFactOrigin context) - (Vector.singleton imported) - target - (importedFactDerivation - (importIx 0)) - builder) - pure - (publishTypedFactState - context - markers' - builder' - st) - -validateTypedFactState - :: BlockContext - -> Facts.StagedFact - -> CheckingState - -> Either CheckingError (HashSet Marker) -validateTypedFactState context staged st = do - markers' <- - validatedMarkers - (blockContextLocation context) - [blockContextMarker context] - st - validatePreparedSemanticFact - context - (checkingOwnedSymbols st) - (checkingDependencies st) - (Facts.stagedFactSemantic staged) - pure markers' - -publishTypedFactState - :: BlockContext - -> HashSet Marker - -> Transition.TransitionModuleBuilder - -> CheckingState - -> CheckingState -publishTypedFactState context markers' builder st = - st - { definedMarkers = markers' - , blockLabel = - blockContextMarker context - , stepLocation = - blockContextLocation context - , checkingHypothesisCounter = 0 - , checkingTransitionModuleBuilder = - Just builder - } - -typedFactOrigin - :: BlockContext - -> Transition.Origin -typedFactOrigin context = - Transition.origin - (blockContextLocation context) - Nothing - (Just - (blockContextMarker context)) - -typedFactError - :: Show error - => BlockContext - -> Text - -> error - -> CheckingError -typedFactError context prefix = - checkingErrorAt context - . (prefix <>) - . Text.pack - . show - --- | Validate and commit one ordinary axiom or proven fact. -commitOrdinaryFact - :: BlockContext - -> Facts.StagedFact - -> CheckingState - -> Either CheckingError CheckingState -commitOrdinaryFact context staged st = do - markers' <- - validatedMarkers location [marker] st - validatePreparedSemanticFact - context - (checkingOwnedSymbols st) - (checkingDependencies st) - (Facts.stagedFactSemantic staged) - facts' <- - first - (DuplicateMarker location) - (Facts.registerStagedFacts - (staged :| []) - (checkingFacts st)) - pure - st - { checkingFacts = facts' - , definedMarkers = markers' - , blockLabel = marker - , stepLocation = location - } - where - location = - blockContextLocation context - marker = - blockContextMarker context - -checkProof :: Proof -> Checking -checkProof = \case - Qed mloc j -> do - loc <- case mloc of - Just loc -> pure loc - Nothing -> do - gets blockEndLocation - setLocation loc - justify j - Contradiction loc j -> do - setLocation loc - setGoals [Bottom] - justify j - ByContradiction loc proof -> do - setLocation loc - goals <- gets checkingGoals - case goals of - [goal] -> do - assume [Asm (Not loc goal)] - modify \st -> - st - { checkingGoals = [Bottom] - , checkingDirectness = Indirect goal - } - checkProof proof - _ -> throwWithLocationAndMarker (ByContradictionOnMultipleGoals) - ByCase loc splits -> do - setLocation loc - for_ splits \(Case split _) -> - assertKnownFormulaVars "case split" split - for_ splits checkCase - setGoals [makeDisjunction (caseOf <$> splits)] - tellTasks - BySetInduction loc mx continue -> do - setLocation loc - goals <- gets checkingGoals - case goals of - Forall scope : goals' -> do - let zs = nubOrd (bindings scope) - z <- case mx of - Nothing -> case zs of - [z'] -> pure z' - _ -> throwWithMarker (AmbiguousInductionVar loc) - Just (TermVar z') -> pure z' - _ -> throwWithMarker (AmbiguousInductionVar loc) - checkFreshLocalVars "set induction" [z] - let y = NamedVar "IndAntecedent" - let ys = List.delete z zs - let anteInst bv = if bv == z then TermVar y else TermVar bv - let antecedent = makeForall (y : ys) ((isElementOf (TermVar y) (TermVar z)) `Implies` instantiate anteInst scope) - addLocalVars (Set.singleton z) - assume [Asm antecedent] - let consequent = instantiate TermVar scope - setGoals (consequent : goals') - checkProof continue - _ -> throwWithMarker (BySetInductionSyntacticMismatch loc) - ByOrdInduction loc continue -> do - setLocation loc - goals <- gets checkingGoals - case goals of - Forall scope : goals' -> case fromScope scope of - Implies (IsOrd loc' (TermVar (B _))) rhs -> do - let zs = nubOrd (bindings scope) - z <- case zs of - [z'] -> pure z' - _ -> throwWithMarker (AmbiguousInductionVar loc') - checkFreshLocalVars "ordinal induction" [z] - -- LATER: this is kinda sketchy: - -- we now use the induction variable in two ways: - -- we assume the induction hypothesis, where we recycle the induction variable both as a bound variable and a free variable - -- we then need to show that under that hypothesis the claim holds for the free variable... - let hypo = Forall (toScope (Implies (isElementOf (TermVar (B z)) (TermVar (F z))) rhs)) - addLocalVars (Set.singleton z) - assume [Asm (IsOrd loc' (TermVar z)), Asm hypo] - let goal' = unvar id id <$> rhs -- we "instantiate" the single bound variable on the rhs - setGoals (goal' : goals') - checkProof continue - _ -> - throwWithMarker - (ByOrdInductionSyntacticMismatch loc) - _ -> - throwWithMarker - (ByOrdInductionSyntacticMismatch loc) - Assume loc phi continue -> do - setLocation loc - assertKnownFormulaVars "assumption step" phi - goals' <- matchAssumptionWithGoal loc phi - assume [Asm phi] - setGoals goals' - checkProof continue - Fix loc xs suchThat continue -> do - setLocation loc - checkFreshLocalVars "fix step" (toList xs) - fixing xs - addLocalVars (Set.fromList (toList xs)) - unless (suchThat == Top) do - assertKnownFormulaVars "fix constraint" suchThat - checkProof case suchThat of - Top -> continue - _ -> Assume loc suchThat continue - Subclaim loc subclaim subproof continue -> do - setLocation loc - assertKnownFormulaVars "subclaim" subclaim - context <- - BlockContext - <$> gets stepLocation - <*> gets blockLabel - locally - (checkLemmaWithProof - context - (Lemma [] subclaim) - subproof) - assume [Asm subclaim] - checkProof continue - Omitted loc -> do - setLocation loc - omitCurrentGoals loc - Suffices loc reduction by proof -> do - setLocation loc - assertKnownFormulaVars "suffices step" reduction - goals <- gets checkingGoals - setGoals [reduction `Implies` makeConjunction goals] - justify by - setGoals [reduction] - checkProof proof - Take loc _witnesses _suchThat JustificationSetExt _continue -> do - setLocation loc - throwWithLocationAndMarker SetExtensionalityWithTake - Take loc witnesses suchThat by continue -> locally do - setLocation loc - checkFreshLocalVars "take step" (toList witnesses) - known <- gets localVars - assertKnownFormulaVarsWith "take witness statement" (known <> Set.fromList (toList witnesses)) suchThat - goals <- gets checkingGoals - setGoals [makeExists witnesses suchThat] - justify by - addLocalVars (Set.fromList (toList witnesses)) - assume [Asm suchThat] - setGoals goals - checkProof continue - Have loc claim (JustificationRef ms) continue -> locally do - setLocation loc - assertKnownFormulaVars "claim" claim - goals <- gets checkingGoals - setGoals [claim] - byRef ms -- locally prove things with just refs and local assumptions - assume [Asm claim] - setGoals goals - checkProof continue - Have loc claim JustificationLocal continue -> locally do - setLocation loc - assertKnownFormulaVars "claim" claim - goals <- gets checkingGoals - setGoals [claim] - byAssumption -- locally prove things with just local assumptions - assume [Asm claim] - setGoals goals - checkProof continue - Have loc claim by continue -> do - setLocation loc - assertKnownFormulaVars "claim" claim - locally do - goals <- gets checkingGoals - claims <- case by of - JustificationEmpty -> - pure [claim] - JustificationSetExt -> - splitGoalWithSetExt claim - -- NOTE: we already handled @JustificationRef ms@ and GHC recognizes this - setGoals claims - tellTasks - assume [Asm claim] - setGoals goals - checkProof continue - Define loc x t continue -> locally do - setLocation loc - checkFreshLocalVars "definition step" [x] - assertKnownTermVars "definition right-hand side" t - addLocalVars (Set.singleton x) - case t of - TermSep y yBound phi -> - assume [Asm $ - makeForall [y] $ - Iff (isElementOf (TermVar y) (TermVar x)) - ((isElementOf (TermVar y) yBound) `And` instantiate1 (TermVar y) phi) - ] - ReplacePred _y _x xBound scope -> do - goals <- gets checkingGoals - let x' = FreshVar 0 - let y = FreshVar 1 - let y' = FreshVar 2 - let fromReplacementVar = \case - ReplacementDomVar -> TermVar x' - ReplacementRangeVar -> TermVar y - let fromReplacementVar' = \case - ReplacementDomVar -> TermVar x' - ReplacementRangeVar -> TermVar y' - let phi = instantiate fromReplacementVar scope - let psi = instantiate fromReplacementVar' scope - let singleValued = - makeForall [x'] $ - (TermVar x' `isElementOf` xBound) `Implies` - makeForall [y, y'] (((phi `And` psi) `Implies` (TermVar y `equals` TermVar y'))) - setGoals [singleValued] - tellTasks - - -- Now we restore the goals, which should already be canonical, so we don't need to canonicalize them again. - modify (\st -> st{checkingGoals = goals}) - assume [Asm $ - makeForall [y] $ - (TermVar y `isElementOf` TermVar x) - `Iff` - makeExists [x'] ((TermVar x' `isElementOf` xBound) `And` phi) - ] - ReplaceFun bounds lhs cond -> - assume [Asm (makeReplacementIff (TermVar (F x)) bounds lhs cond)] - _ -> - assume [Asm (Equals loc (TermVar x) t)] - checkProof continue - DefineFunction loc funVar argVar valueExpr domExpr continue -> do - setLocation loc - checkFreshLocalVars "function definition" [funVar] - checkBinderVarsFresh "function definition" [argVar] - when (funVar == argVar) do - throwCheckingError "function definition uses the same variable for the function and its argument" - known <- gets localVars - assertKnownTermVarsWith "function definition domain" known domExpr - assertKnownTermVarsWith "function definition value" (Set.insert argVar known) valueExpr - addLocalVars (Set.singleton funVar) - -- we're given f, x, e, d - assume - [ Asm (Equals loc (TermOp Nowhere DomSymbol [TermVar funVar]) domExpr) -- dom(f) = d - , Asm (makeForall [argVar] ((isElementOf (TermVar argVar) domExpr) `Implies` (Equals Nowhere (TermOp Nowhere ApplySymbol [TermVar funVar, TermVar argVar]) valueExpr))) -- f(x) = e for all x\in d - , Asm (rightUniqueAdj loc (TermVar funVar)) - , Asm (relationNoun loc (TermVar funVar)) - ] - checkProof continue - Calc loc quant calc continue -> do - setLocation loc - for_ (calculation quant calc) \(goal, _) -> - assertKnownFormulaVars "calculation step" goal - assertKnownFormulaVars "calculation result" (calcResult quant calc) - checkCalc quant calc - assume [Asm (calcResult quant calc)] - checkProof continue - DefineFunctionLocal loc funVar argVar domVar ranExpr definitions continue -> do -- TODO refactor - setLocation loc - checkFreshLocalVars "local function definition" [funVar] - checkBinderVarsFresh "local function definition" [argVar] - when (funVar == argVar) do - throwCheckingError "local function definition uses the same variable for the function and its argument" - known <- gets localVars - assertKnownFormulaVarsWith "local function definition range" known ranExpr - let knownWithArg = Set.insert argVar known - for_ definitions \(expr, frm) -> do - assertKnownTermVarsWith "local function definition case expression" knownWithArg expr - assertKnownFormulaVarsWith "local function definition case condition" knownWithArg frm - unless (domVar `Set.member` known) do - throwCheckingError ("local function definition domain variable is not in scope: " <> formatVars (Set.singleton domVar)) - addLocalVars (Set.singleton funVar) - -- We have f: X \to Y and x \mapsto ... - -- definition is a nonempty list of (expresssion e, formula phi) - -- such that f(x) = e if phi(x) - -- since we do a case deduction in the definition there has to be a check that, - -- our domains in the case are a disjunct union of dom(f) - assume - [Asm (Equals Nowhere (TermOp Nowhere DomSymbol [TermVar funVar]) (TermVar domVar)) - ,Asm (rightUniqueAdj Nowhere (TermVar funVar)) - ,Asm (relationNoun Nowhere (TermVar funVar))] - - goals <- gets checkingGoals - setGoals [makeForall [argVar] ((isElementOf (TermVar argVar) (TermVar domVar)) `Iff` localFunctionGoal definitions)] - tellTasks - - locals <- gets localVars - assume [Asm (makeForall [argVar] (isElementOf (TermVar argVar) (TermVar domVar) `Implies` isElementOf (TermOp Nowhere ApplySymbol [TermVar funVar, TermVar argVar]) ranExpr))] -- function f from \dom(f) \to \ran(f) - assume (functionSubdomianExpression funVar argVar domVar locals (NonEmpty.toList definitions)) --behavior on the subdomians - setGoals goals - checkProof continue - --- |Creats the Goal \forall x. x \in dom{f} \iff (phi_{1}(x) \xor (\phi_{2}(x) \xor (... \xor (\phi_{n}) ..))) --- where the phi_{i} are the subdomain statments -localFunctionGoal :: NonEmpty (Term,Formula) -> Formula -localFunctionGoal xs = makeXor $ map snd $ NonEmpty.toList xs - - --- We have our list of expr and forumlas, in this case normaly someone would write --- f(x) = ....cases --- & (\frac{1}{k} \cdot x) &\text{if} x \in \[k, k+1\) --- --- since we have to bind all globaly free Varibels we generate following asumptions. --- --- For x \mapsto expr(x,ys,cs) , if formula(x,ys) ; here cs are just global constants --- -> \forall x,ys: ( formula(x,ys) => expr(x,ys,cs)) - - -functionSubdomianExpression :: VarSymbol -> VarSymbol -> VarSymbol -> Set VarSymbol -> [(Term, Formula)] -> [Asm] -functionSubdomianExpression f a d s (x:xs) = singleFunctionSubdomianExpression f a d s x : functionSubdomianExpression f a d s xs -functionSubdomianExpression _ _ _ _ [] = [] - -singleFunctionSubdomianExpression :: VarSymbol -> VarSymbol -> VarSymbol -> Set VarSymbol -> (Term, Formula) -> Asm -singleFunctionSubdomianExpression funVar argVar domVar fixedV (expr, frm) = let - -- boundVar = Set.toList (freeVars expr) in - -- let def = makeForall (argVar:boundVar) (((TermVar argVar `IsElementOf` TermVar domVar) `And` frm) `Implies` TermOp ApplySymbol [TermVar funVar, TermVar argVar] `Equals` expr) - boundVar = fixedV in - let def = forallClosure boundVar (((isElementOf (TermVar argVar) (TermVar domVar)) `And` frm) `Implies` Equals Nowhere (TermOp Nowhere ApplySymbol [TermVar funVar, TermVar argVar]) expr) - in Asm def - - - -checkCalc :: CalcQuantifier -> Calc -> Checking -checkCalc quant calc = locally do - let tasks = calculation quant calc - forM_ tasks tell - where - tell = \case - (goal, by) -> setGoals [goal] *> justify by - - -makeReplacementIff - :: forall a. (ExprOf (Var VarSymbol a) -- ^ Newly defined local constant. - -> NonEmpty (VarSymbol, ExprOf a) -- ^ Bounds of the replacement. - -> Scope VarSymbol ExprOf a -- ^ Left hand side (function application). - -> Scope VarSymbol ExprOf a -- ^ Optional constraints on bounds (can just be 'Top'). - -> ExprOf a) -makeReplacementIff e bounds lhs cond = - Forall (toScope (Iff (isElementOf (TermVar (B "frv")) e) existsPreimage)) - where - existsPreimage :: ExprOf (Var VarSymbol a) - existsPreimage = Exists (toScope replaceBound) - - replaceBound :: ExprOf (Var VarSymbol (Var VarSymbol a)) - replaceBound = makeConjunction [isElementOf (TermVar (B x)) (F . F <$> xB) | (x, xB) <- toList bounds] `And` replaceCond - - replaceEq :: ExprOf (Var VarSymbol (Var VarSymbol a)) - replaceEq = Equals Nowhere (nestF <$> fromScope lhs) (TermVar (F (B "frv"))) - - replaceCond :: ExprOf (Var VarSymbol (Var VarSymbol a)) - replaceCond = case fromScope cond of - Top -> replaceEq - cond' -> replaceEq `And` (nestF <$> cond') - - nestF :: Var b a1 -> Var b (Var b1 a1) - nestF (B a) = B a - nestF (F a) = F (F a) - - -splitGoalWithSetExt :: Formula -> CheckingM [Formula] -splitGoalWithSetExt = \case - NotEquals loc x y -> do - let z = FreshVar 0 - elemNotElem x' y' = makeExists [FreshVar 0] (And (IsElementOf loc (TermVar z) x') (isNotElementOf loc (TermVar z) y')) - pure [elemNotElem x y `Or` elemNotElem y x] - Equals loc x y -> do - let z = FreshVar 0 - subset x' y' = makeForall [FreshVar 0] (Implies (IsElementOf loc (TermVar z) x') (IsElementOf loc (TermVar z) y')) - pure [subset x y, subset y x] - goal -> throwWithLocationAndMarker (MismatchedSetExt [goal]) - -justify :: Justification -> Checking -justify = \case - JustificationEmpty -> tellTasks - JustificationLocal -> byAssumption - JustificationRef ms -> byRef ms - JustificationSetExt -> do - goals <- gets checkingGoals - case goals of - [goal] -> do - goals' <- splitGoalWithSetExt goal - setGoals goals' - tellTasks - _ -> throwWithLocationAndMarker (MismatchedSetExt goals) - -byRef :: NonEmpty Marker -> Checking -byRef ms = locally do - facts <- gets checkingFacts - dumpPremselTraining <- gets checkingDumpPremselTraining - case dumpPremselTraining of - WithDumpPremselTraining -> dumpTrainingData facts ms - WithoutDumpPremselTraining -> skip - case Facts.restrictFactRegistry ms facts of - Left (Marker str) -> - throwWithLocationAndMarker - (CheckingError ("unknown marker: " <> str)) - Right facts' -> modify (\st -> st{checkingFacts = facts'}) *> tellTasks - -byAssumption :: Checking -byAssumption = locally do - modify (\st -> st{checkingFacts = Facts.emptyFactRegistry}) *> tellTasks - -dumpTrainingData :: Facts.FactRegistry -> NonEmpty Marker -> Checking -dumpTrainingData facts ms = do - (picked, unpicked) <- - case Facts.partitionFactRegistry ms facts of - Left (Marker str) -> - throwWithLocationAndMarker - (CheckingError ("unknown marker: " <> str)) - Right partitioned -> - pure partitioned - goals <- gets checkingGoals - Marker m_ <- gets blockLabel - let dir = "premseldump" - let makePath k = dir </> (Text.unpack m_ <> show (k :: Int)) <.> "txt" - dumpTrainingExample goal = - let prepared = - prepareTrainingTptpTask - goal - (factHypotheses picked) - (factHypotheses unpicked) - k = hash goal - example = preparedTptpTextNewline prepared - in do - liftIO (Text.writeFile (makePath k) example) - liftIO (createDirectoryIfMissing True dir) - forM_ goals dumpTrainingExample - --- | Since the case tactic replaces /all/ current goals with the disjunction --- of the different case hypotheses, each case proof must cover all goals. -checkCase :: Case -> Checking -checkCase (Case split proof) = locally do - assume [Asm split] - checkProof proof - - -checkDefn :: BlockContext -> Defn -> Checking -checkDefn context defn = do - let (ownerKind, definedSymbol, definitionAsms, definiens) = definitionParts defn - dependencies <- checkedDefinitionDependencies definedSymbol definitionAsms definiens - (prepared, soundnessGoals) <- prepareDefinitionFact context defn - let staged = - stagePreparedFact - (blockContextLocation context) - (blockContextMarker context) - (blockContextMarker context) - prepared - st <- get - committed <- - either - throwIO - pure - (commitDefinition - context - ownerKind - definedSymbol - dependencies - staged - st) - unless (null soundnessGoals) do - locally do - modify \current -> - current{checkingGoals = soundnessGoals} - tellTasks - putDeclarationCandidate committed - setDeclarationFactProducers - [ LegacyDeclarationRuleProducer - (LegacyDefinitionRule - LegacyDefinitionEquation) - ] - -prepareDefinitionFact - :: BlockContext - -> Defn - -> CheckingM (Facts.PreparedSemanticFact, [Formula]) -prepareDefinitionFact context = \case - DefnPredicate asms symb vs f -> do - -- We first need to take the universal closure of the defining formula - -- while ignoring the variables that occur on the lhs, then take the - -- universal formula of the equivalence, quantifying the remaining - -- variables (from the lhs). - let vs' = TermVar <$> toList vs - let f' = forallClosure (Set.fromList (toList vs)) f - prepared <- - prepareWithAsms - asms - (Atomic location symb vs' `Iff` f') - pure (prepared, []) - DefnFun asms fun vs rhs -> do - let lhs = - TermSymbol location (SymbolFun fun) (TermVar <$> vs) - prepared <- - prepareWithAsms asms (Equals location lhs rhs) - pure (prepared, []) - DefnOp op vs (TermSep x bound phi) -> do - let generated = - makeForall (x : vs) $ - Iff (TermVar x `isElementOf` TermOp location op (TermVar <$> vs)) - ((TermVar x `isElementOf` bound) `And` instantiate1 (TermVar x) phi) - prepared <- prepare generated - pure (prepared, []) - DefnOp op vs (TermSymbol _pos rhsSymbol [x, y]) | rhsSymbol == SymbolMixfix ConsSymbol -> do - -- TODO generalize this to support arbitrarily many applications of _Cons - -- and also handle the case of emptyset or singleton as final argument separately - -- so that finite set terms get recognized in full. - let phi = - isElementOf - (TermVar "any") - (TermOp location op (TermVar <$> vs)) - let psi = - (isElementOf (TermVar "any") y) - `Or` (Equals location (TermVar "any") x) - prepared <- - prepare (makeForall ("any" : vs) (phi `Iff` psi)) - pure (prepared, []) - DefnOp op vs (ReplacePred _y _x xBound scope) -> do - let x = (FreshVar 0) - let y = (FreshVar 1) - let y' = (FreshVar 2) - let fromReplacementVar = \case - ReplacementDomVar -> TermVar x - ReplacementRangeVar -> TermVar y - let fromReplacementVar' = \case - ReplacementDomVar -> TermVar x - ReplacementRangeVar -> TermVar y' - let phi = instantiate fromReplacementVar scope - let psi = instantiate fromReplacementVar' scope - let singleValued = makeForall [x] ((TermVar x `isElementOf` xBound) `Implies` makeForall [y, y'] ((phi `And` psi) `Implies` (TermVar y `equals` TermVar y'))) - let generated = - makeForall (y : vs) - ((TermVar y `isElementOf` TermOp Nowhere op (TermVar <$> vs)) - `Iff` - makeExists [x] ((TermVar x `isElementOf` xBound) `And` phi)) - preparedGoal <- canonicalize singleValued - prepared <- prepare generated - pure (prepared, [preparedGoal]) - DefnOp op vs (ReplaceFun bounds lhs cond) -> do - let generated = forallClosure mempty (makeReplacementIff (TermOp Nowhere op (TermVar . F <$> vs)) bounds lhs cond) - prepared <- prepare generated - pure (prepared, []) - DefnOp op vs rhs -> - if containsHigherOrderConstructs rhs - then - throwIO - (CouldNotEliminateHigherOrder - op - rhs - location - (blockContextMarker context)) - else do - let lhs = TermSymbol Nowhere (SymbolMixfix op) (TermVar <$> vs) - prepared <- - prepareWithAsms [] (Equals Nowhere lhs rhs) - pure (prepared, []) - where - location = - blockContextLocation context - - prepare formula = - Facts.prepareSemanticFact <$> canonicalize formula - - prepareWithAsms asms formula = - Facts.prepareSemanticFact - <$> canonicalizedFactWithAsms asms formula - --- | Validate and commit every state row introduced by one definition. -commitDefinition - :: BlockContext - -> SymbolOwnerKind - -> Symbol - -> Set Symbol - -> Facts.StagedFact - -> CheckingState - -> Either CheckingError CheckingState -commitDefinition context ownerKind symbol dependencies staged st = do - markers' <- - validatedMarkers location [marker] st - validateOwnedDependenciesAt - context - (checkingOwnedSymbols st) - dependencies - (owners', ownedMarkers', dependencies') <- - validatedSymbolRegistration - context - ownerKind - symbol - dependencies - st - validatePreparedSemanticFact - context - owners' - dependencies' - (Facts.stagedFactSemantic staged) - facts' <- - first - (DuplicateMarker location) - (Facts.registerStagedFacts - (staged :| []) - (checkingFacts st)) - pure - st - { checkingFacts = facts' - , checkingDependencies = dependencies' - , checkingOwnedSymbols = owners' - , checkingOwnedSymbolMarkers = ownedMarkers' - , definedMarkers = markers' - , blockLabel = marker - , stepLocation = location - , checkingHypothesisCounter = 0 - } - where - location = - blockContextLocation context - marker = - blockContextMarker context - - -checkSig :: BlockContext -> [Asm] -> Signature -> Checking -checkSig context asms signature = do - (ownerKind, symbol, staged, typedCoreType) <- case signature of - SignatureFormula formula -> do - symbol <- - maybe - (throwIO - (checkingErrorAt - context - "could not recover the declared symbol from SignatureFormula")) - pure - (recoverSignatureFormulaSymbol formula) - prepared <- - Facts.prepareSemanticFact - <$> canonicalizedFactWithAsms asms formula - pure - ( OwnedBySignatureFormula - , symbol - , Just - (stagePreparedFact - (blockContextLocation context) - (blockContextMarker context) - (blockContextMarker context) - prepared) - , Nothing - ) - SignaturePredicate predicate variables -> - pure - ( OwnedBySignaturePredicate - , SymbolPredicate predicate - , Nothing - , Just - (foldr - Core.TyArrow - Core.TyProp - (replicate - (length variables) - Core.TySet)) - ) - st <- get - committed <- - either - throwIO - pure - (commitSignature context ownerKind symbol staged st) - transitionBuilder' <- - case typedCoreType of - Nothing -> - pure - (checkingTransitionModuleBuilder - committed) - Just coreType -> - traverse - (either - (throwIO - . checkingErrorAt - context - . ("typed signature registration failed: " - <>) - . Text.pack - . show) - pure - . Transition.commitTransitionOpaqueGlobal - symbol - coreType - (Transition.origin - (blockContextLocation context) - Nothing - (Just - (blockContextMarker - context)))) - (checkingTransitionModuleBuilder - committed) - putDeclarationCandidate - committed - { checkingTransitionModuleBuilder = - transitionBuilder' - } - setDeclarationFactProducers - (case staged of - Nothing -> - [] - Just _ -> - [ LegacyDeclaredAssumptionProducer - OpaqueAssumption - ]) - --- | Validate and commit every state row introduced by one signature. -commitSignature - :: BlockContext - -> SymbolOwnerKind - -> Symbol - -> Maybe Facts.StagedFact - -> CheckingState - -> Either CheckingError CheckingState -commitSignature context ownerKind symbol staged st = do - markers' <- - validatedMarkers location [marker] st - (owners', ownedMarkers', dependencies') <- - validatedSymbolRegistration - context - ownerKind - symbol - mempty - st - facts' <- - case staged of - Nothing -> - Right (checkingFacts st) - Just fact -> do - validatePreparedSemanticFact - context - owners' - dependencies' - (Facts.stagedFactSemantic fact) - first - (DuplicateMarker location) - (Facts.registerStagedFacts - (fact :| []) - (checkingFacts st)) - pure - st - { checkingFacts = facts' - , checkingDependencies = dependencies' - , checkingOwnedSymbols = owners' - , checkingOwnedSymbolMarkers = ownedMarkers' - , definedMarkers = markers' - , blockLabel = marker - , stepLocation = location - , checkingHypothesisCounter = 0 - } - where - location = - blockContextLocation context - marker = - blockContextMarker context - -recoverSignatureFormulaSymbol :: Formula -> Maybe Symbol -recoverSignatureFormulaSymbol = \case - Forall scope - | [boundVar] <- nubOrd (bindings scope) -> - case fromScope scope of - Equals _ (TermVar (B lhsVar)) (TermSymbol _ symbol@(SymbolMixfix _) _args) `Implies` _ - | lhsVar == boundVar -> - Just symbol - _ -> - Nothing - | otherwise -> - Nothing - _ -> - Nothing - -mergeAssumptions :: [Asm] -> CheckingM ([Formula], StructContext) -mergeAssumptions asms = do - ctx <- assumptionStructContext asms - phis <- traverse asmFormula asms - pure (phis, ctx) - -asmFormula :: Asm -> CheckingM Formula -asmFormula = \case - Asm phi -> - pure phi - AsmStruct x phrase -> - pure (structPredicate x phrase) - -canonicalize :: Formula -> CheckingM Formula -canonicalize phi = do - ctx <- gets checkingStructContext - canonicalizeWith ctx phi - --- | Canonicalize using an explicit structure context instead of the checker state's current one. -canonicalizeWith :: StructContext -> Formula -> CheckingM Formula -canonicalizeWith ctx phi = do - blockContext <- - BlockContext - <$> gets stepLocation - <*> gets blockLabel - canonicalizeWithAt blockContext ctx phi - -canonicalizeWithAt - :: BlockContext - -> StructContext - -> Formula - -> CheckingM Formula -canonicalizeWithAt blockContext ctx phi = do - phi' <- unabbreviate phi - desugarComprehensionsAt - blockContext - (annotateWithStructContext ctx phi') - -annotateWithStructContext :: StructContext -> Formula -> Formula -annotateWithStructContext StructContext{..} = - annotateWith structContextLabels structContextOps - -unabbreviate :: ExprOf a -> CheckingM (ExprOf a) -unabbreviate phi = do - abbrs <- gets checkingAbbreviations - pure (unabbreviateWith ((absurd <$>) <$> abbrs) phi) - - -data CheckedInductive = CheckedInductive - { checkedInductiveSymbol :: FunctionSymbol - , checkedInductiveParams :: [VarSymbol] - , checkedInductiveDomain :: Expr - , checkedInductiveIntros :: NonEmpty CheckedInductiveIntro - } - -data CheckedInductiveIntro = CheckedInductiveIntro - { checkedInductiveIntroVars :: [VarSymbol] - , checkedInductiveIntroConditions :: [CheckedInductiveCondition] - , checkedInductiveIntroResultTerm :: Term - } - -data CheckedInductiveCondition - = CheckedInductiveSideCondition Formula - | CheckedInductiveRecursiveCondition - { checkedInductiveRecursiveTerm :: Term - , checkedInductiveRecursiveCarrierTemplate :: Scope VarSymbol ExprOf VarSymbol - , checkedInductiveRecursiveDirect :: Bool - } - -checkInductive :: BlockContext -> Inductive -> Checking -checkInductive context inductive = do - st <- get - either - throwIO - pure - (validateInductiveHeader - context - (SymbolMixfix (inductiveSymbol inductive)) - st) - checked <- normalizeInductive inductive - case checkingTransitionModuleBuilder st of - Nothing -> - checkLegacyInductive context checked st - Just builder -> - checkTypedInductive - context - checked - builder - st - -checkLegacyInductive - :: BlockContext - -> CheckedInductive - -> CheckingState - -> Checking -checkLegacyInductive context checked st = do - soundnessGoals <- - traverse canonicalize (inductiveSoundnessGoals checked) - stagedFacts <- - traverse - (\(factMarker, formula) -> do - canonical <- canonicalize formula - pure - (stagePreparedFact - (blockContextLocation context) - (blockContextMarker context) - factMarker - (Facts.prepareSemanticFact canonical))) - (inductiveFacts - (blockContextMarker context) - checked) - committed <- - either - throwIO - pure - (commitInductive - context - checked - stagedFacts - st) - unless (null soundnessGoals) do - locally do - modify \current -> - current{checkingGoals = soundnessGoals} - tellTasks - putDeclarationCandidate committed - setDeclarationFactProducers - ( LegacyDeclarationRuleProducer - . LegacyInductiveRule - <$> inductiveFactRoles checked - ) - -checkTypedInductive - :: BlockContext - -> CheckedInductive - -> Transition.TransitionModuleBuilder - -> CheckingState - -> Checking -checkTypedInductive context checked builder st = do - direct <- - either - throwIO - pure - (directInductive context checked) - prepared <- - either - ( throwIO - . typedInductiveError - context - "typed inductive preparation failed: " - ) - pure - (TypedInductive.prepareTypedInductive - Transition.checkedGlobalType - (Transition.transitionBuilderFoundation - builder) - (typedSourceGlobal builder) - (blockContextMarker context) - direct) - imports <- - Vector.fromList - <$> traverse - (uncurry - (typedInductiveGuardImport - context - builder)) - (zip - [1 :: Int ..] - (Vector.toList - (TypedInductive.typedInductiveGuardTargets - prepared))) - builderWithCarrier <- - either - ( throwIO - . typedInductiveError - context - "typed inductive carrier registration failed: " - ) - pure - (Transition.commitTransitionTransparentGlobal - (SymbolMixfix - (checkedInductiveSymbol checked)) - (TypedInductive.typedInductiveCarrierType - prepared) - (TypedInductive.typedInductiveCarrierBody - prepared) - (typedFactOrigin context) - builder) - builder' <- - foldM - (commitTypedInductiveFact - context - imports) - builderWithCarrier - (TypedInductive.typedInductiveFacts - prepared) - committed <- - either - throwIO - pure - (commitTypedInductiveState - context - checked - (TypedInductive.typedInductiveFactMarker - <$> TypedInductive.typedInductiveFacts - prepared) - builder' - st) - putDeclarationCandidate committed - setDeclarationFactProducers [] - -directInductive - :: BlockContext - -> CheckedInductive - -> Either CheckingError TypedInductive.DirectInductive -directInductive context checked = - TypedInductive.DirectInductive - (checkedInductiveParams checked) - (checkedInductiveDomain checked) - <$> traverse directClause - (checkedInductiveIntros checked) - where - directClause intro = - TypedInductive.DirectInductiveClause - (checkedInductiveIntroVars intro) - <$> traverse directCondition - (checkedInductiveIntroConditions intro) - <*> pure - (checkedInductiveIntroResultTerm intro) - - directCondition = \case - CheckedInductiveSideCondition formula -> - Right - (TypedInductive.DirectSideCondition - formula) - CheckedInductiveRecursiveCondition - { checkedInductiveRecursiveTerm - , checkedInductiveRecursiveDirect = True - } -> - Right - (TypedInductive.DirectRecursiveCondition - checkedInductiveRecursiveTerm) - CheckedInductiveRecursiveCondition{} -> - Left - (checkingErrorAt context - "nested inductive recursion is not supported by the typed set-valued inductive slice") - -typedSourceGlobal - :: Transition.TransitionModuleBuilder - -> Symbol - -> Maybe - (TypedInductive.SourceGlobal - Transition.CheckedGlobalRef) -typedSourceGlobal builder symbol = do - reference <- - Transition.lookupTransitionGlobal - symbol - builder - pure - (TypedInductive.SourceGlobal - reference - (Transition.lookupTransitionGlobalBody - symbol - builder)) - -typedInductiveGuardImport - :: BlockContext - -> Transition.TransitionModuleBuilder - -> Int - -> Core.FrozenCheckedCore - Transition.CheckedGlobalRef - -> CheckingM Transition.TransitionDerivationImport -typedInductiveGuardImport - context - builder - ordinal - target = do - found <- - either - ( throwIO - . typedInductiveError - context - "typed inductive guard lookup failed: " - ) - pure - (Transition.lookupTransitionTypedImport - target - builder) - maybe - (throwIO - (checkingErrorAt context - ( "typed inductive domain guard " - <> Text.pack (show ordinal) - <> " has no authorized typed fact" - ))) - pure - found - -commitTypedInductiveFact - :: BlockContext - -> Vector Transition.TransitionDerivationImport - -> Transition.TransitionModuleBuilder - -> TypedInductive.PreparedTypedInductiveFact - Transition.CheckedGlobalRef - -> CheckingM Transition.TransitionModuleBuilder -commitTypedInductiveFact context imports builder fact = do - either - ( throwIO - . typedInductiveError - context - "typed inductive fact admission failed: " - ) - pure - (Transition.commitTransitionKernelFactWithImports - (TypedInductive.typedInductiveFactMarker - fact - :| []) - (typedFactOrigin context) - imports - (TypedInductive.typedInductiveFactTarget - fact) - (TypedInductive.typedInductiveFactDerivation - fact) - builder) - -commitTypedInductiveState - :: BlockContext - -> CheckedInductive - -> NonEmpty Marker - -> Transition.TransitionModuleBuilder - -> CheckingState - -> Either CheckingError CheckingState -commitTypedInductiveState - context - checked - factMarkers - builder - st = do - markers' <- - validatedMarkers - location - (marker : NonEmpty.toList factMarkers) - st - (owners', ownedMarkers', dependencies') <- - validatedSymbolRegistration - context - OwnedByInductiveDefinition - carrier - mempty - st - frozenSymbols <- - first - ( checkingErrorAt context - . ("inductive specification mentions unknown symbol " <>) - . symbolText - ) - (checkedInductiveFrozenSymbols - dependencies' - checked) - let frozen = - HM.fromList - [ (symbol, marker) - | symbol <- Set.toList frozenSymbols - , ownableSymbol symbol - ] - pure - st - { checkingDependencies = dependencies' - , checkingOwnedSymbols = owners' - , checkingOwnedSymbolMarkers = ownedMarkers' - , checkingFrozenSymbols = - HM.union - (checkingFrozenSymbols st) - frozen - , definedMarkers = markers' - , blockLabel = marker - , stepLocation = location - , checkingHypothesisCounter = 0 - , checkingTransitionModuleBuilder = - Just builder - } - where - location = - blockContextLocation context - marker = - blockContextMarker context - carrier = - SymbolMixfix - (checkedInductiveSymbol checked) - -typedInductiveError - :: Show error - => BlockContext - -> Text - -> error - -> CheckingError -typedInductiveError context prefix = - checkingErrorAt context - . (prefix <>) - . Text.pack - . show - -validateInductiveHeader - :: BlockContext - -> Symbol - -> CheckingState - -> Either CheckingError () -validateInductiveHeader context carrier st = do - void - (validatedMarkers - (blockContextLocation context) - [blockContextMarker context] - st) - void - (validatedSymbolRegistration - context - OwnedByInductiveDefinition - carrier - mempty - st) - --- | Validate and commit every state row introduced by one inductive. -commitInductive - :: BlockContext - -> CheckedInductive - -> NonEmpty Facts.StagedFact - -> CheckingState - -> Either CheckingError CheckingState -commitInductive context checked stagedFacts st = do - markers' <- - validatedMarkers - location - (marker : factMarkers) - st - (owners', ownedMarkers', dependencies') <- - validatedSymbolRegistration - context - OwnedByInductiveDefinition - carrier - mempty - st - frozenSymbols <- - first - ( checkingErrorAt context - . ("inductive specification mentions unknown symbol " <>) - . symbolText - ) - (checkedInductiveFrozenSymbols - dependencies' - checked) - traverse_ - (validatePreparedSemanticFact - context - owners' - dependencies') - (Facts.stagedFactSemantic <$> stagedFacts) - facts' <- - first - (DuplicateMarker location) - (Facts.registerStagedFacts - stagedFacts - (checkingFacts st)) - let frozen = - HM.fromList - [ (symbol, marker) - | symbol <- Set.toList frozenSymbols - , ownableSymbol symbol - ] - pure - st - { checkingFacts = facts' - , checkingDependencies = dependencies' - , checkingOwnedSymbols = owners' - , checkingOwnedSymbolMarkers = ownedMarkers' - , checkingFrozenSymbols = - HM.union - (checkingFrozenSymbols st) - frozen - , definedMarkers = markers' - , blockLabel = marker - , stepLocation = location - , checkingHypothesisCounter = 0 - } - where - location = - blockContextLocation context - marker = - blockContextMarker context - carrier = - SymbolMixfix (checkedInductiveSymbol checked) - factMarkers = - toList (stagedFacts >>= Facts.stagedFactAliases) - -normalizeInductive :: Inductive -> CheckingM CheckedInductive -normalizeInductive Inductive{..} = do - let duplicateParams = duplicateVars inductiveParams - unless (Set.null duplicateParams) do - throwCheckingError ("inductive parameters must be linear: " <> formatVars duplicateParams) - checkedInductiveDomain <- canonicalize inductiveDomain - let illegalDomainVars = freeVars checkedInductiveDomain `Set.difference` Set.fromList inductiveParams - unless (Set.null illegalDomainVars) do - throwCheckingError ("inductive domain may only mention the inductive parameters: " <> formatVars illegalDomainVars) - when (mentionsSymbol (SymbolMixfix inductiveSymbol) checkedInductiveDomain) do - throwCheckingError "inductive domain must be independent of the inductive symbol" - checkedInductiveIntros <- traverse (normalizeInductiveIntro inductiveSymbol inductiveParams) inductiveIntros - let checked = - CheckedInductive - { checkedInductiveSymbol = inductiveSymbol - , checkedInductiveParams = inductiveParams - , checkedInductiveDomain - , checkedInductiveIntros - } - ensureInductiveDefinitionIndependence checked - pure checked - -ensureInductiveDefinitionIndependence :: CheckedInductive -> Checking -ensureInductiveDefinitionIndependence checked = do - graph <- gets checkingDependencies - let carrier = SymbolMixfix (checkedInductiveSymbol checked) - externalSymbols = - Set.filter ownableSymbol - (Set.delete carrier (checkedInductiveMentionedSymbols checked)) - path <- - either - (\unknown -> - throwCheckingError - ("inductive specification mentions unknown symbol " <> symbolText unknown)) - pure - (Dependencies.dependencyPath graph externalSymbols carrier) - case path of - Nothing -> - skip - Just path -> - throwCheckingError - ( "inductive specification mentions symbol " - <> symbolText (NonEmpty.head path) - <> " whose definition depends on the inductive symbol " - <> functionSymbolText (checkedInductiveSymbol checked) - <> " via " - <> formatSymbolPath path - ) - -checkedInductiveFrozenSymbols - :: Dependencies.DependencyRegistry - -> CheckedInductive - -> Either Symbol (Set Symbol) -checkedInductiveFrozenSymbols graph checked = - let seeds = - Set.filter ownableSymbol - (checkedInductiveMentionedSymbols checked) - in Dependencies.dependencyClosure graph seeds - -normalizeInductiveIntro :: FunctionSymbol -> [VarSymbol] -> IntroRule -> CheckingM CheckedInductiveIntro -normalizeInductiveIntro symbol params IntroRule{introConditions, introResult} = do - introConditions' <- traverse canonicalize introConditions - introResult' <- canonicalize introResult - checkedInductiveIntroConditions <- traverse (normalizeInductiveCondition symbol params) introConditions' - checkedInductiveIntroResultTerm <- normalizeInductiveResult symbol params introResult' - let paramSet = Set.fromList params - checkedInductiveIntroVars = - List.filter (`Set.notMember` paramSet) (orderedUniqueVars (concatMap toList introConditions' <> toList checkedInductiveIntroResultTerm)) - pure CheckedInductiveIntro - { checkedInductiveIntroVars - , checkedInductiveIntroConditions - , checkedInductiveIntroResultTerm - } - -normalizeInductiveResult :: FunctionSymbol -> [VarSymbol] -> Formula -> CheckingM Term -normalizeInductiveResult symbol params = \case - IsElementOf _ resultTerm carrier - | not (matchesInductiveCarrier symbol (TermVar <$> params) carrier) -> - throwCheckingError "inductive rule result must have the form t \\in F(args)" - | mentionsSymbol (SymbolMixfix symbol) resultTerm -> - throwCheckingError "inductive rule result term must not mention the inductive symbol" - | otherwise -> - pure resultTerm - _ -> - throwCheckingError "inductive rule result must have the form t \\in F(args)" - -normalizeInductiveCondition :: FunctionSymbol -> [VarSymbol] -> Formula -> CheckingM CheckedInductiveCondition -normalizeInductiveCondition symbol params phi - | not (mentionsSymbol (SymbolMixfix symbol) phi) = - pure (CheckedInductiveSideCondition phi) - | otherwise = case phi of - IsElementOf _ recursiveTerm recursiveCarrier -> do - when (mentionsSymbol (SymbolMixfix symbol) recursiveTerm) do - throwCheckingError "inductive recursive occurrence must appear in the carrier of a membership premise" - let placeholder = - freshGeneratedVar - (freeVars phi <> Set.fromList params) - "__inductive" - -- Ordinary definitions are tracked separately through the top-level - -- freshness/dependency checks. At this stage we only decompose the - -- explicit recursive carrier occurrence that remains in the premise. - recursiveCarrierTemplateExpr <- - either throwCheckingError pure - (replaceInductiveApplications symbol (TermVar <$> params) (TermVar placeholder) recursiveCarrier) - let checkedInductiveRecursiveDirect = recursiveCarrierTemplateExpr == TermVar placeholder - pure CheckedInductiveRecursiveCondition - { checkedInductiveRecursiveTerm = recursiveTerm - , checkedInductiveRecursiveCarrierTemplate = abstractVarSymbol placeholder recursiveCarrierTemplateExpr - , checkedInductiveRecursiveDirect - } - _ -> - throwCheckingError "inductive recursive premise must be a direct membership condition" - -replaceInductiveApplications :: Eq a => FunctionSymbol -> [ExprOf a] -> ExprOf a -> ExprOf a -> Either Text (ExprOf a) -replaceInductiveApplications symbol targetArgs replacement = - go targetArgs replacement - where - go :: Eq a => [ExprOf a] -> ExprOf a -> ExprOf a -> Either Text (ExprOf a) - go liftedArgs liftedReplacement = \case - TermVar x -> - Right (TermVar x) - TermSymbol loc sym args - | sym == SymbolMixfix symbol && sameInductiveArgs liftedArgs args -> - Right liftedReplacement - | sym == SymbolMixfix symbol -> - Left ("inductive symbol " <> functionSymbolText symbol <> " occurred with the wrong arguments") - | otherwise -> - TermSymbol loc sym <$> traverse (go liftedArgs liftedReplacement) args - TermSymbolStruct structSymbol expr -> - TermSymbolStruct structSymbol <$> traverse (go liftedArgs liftedReplacement) expr - Apply expr args -> - Apply <$> go liftedArgs liftedReplacement expr <*> traverse (go liftedArgs liftedReplacement) args - TermSep x bound scope -> do - bound' <- go liftedArgs liftedReplacement bound - scope' <- go (map (F <$>) liftedArgs) (F <$> liftedReplacement) (fromScope scope) - pure (TermSep x bound' (toScope scope')) - ReplacePred y x bound scope -> do - bound' <- go liftedArgs liftedReplacement bound - scope' <- go (map (F <$>) liftedArgs) (F <$> liftedReplacement) (fromScope scope) - pure (ReplacePred y x bound' (toScope scope')) - ReplaceFun bounds lhs cond -> do - bounds' <- traverse (\(x, bound) -> do - bound' <- go liftedArgs liftedReplacement bound - pure (x, bound')) bounds - lhs' <- go (map (F <$>) liftedArgs) (F <$> liftedReplacement) (fromScope lhs) - cond' <- go (map (F <$>) liftedArgs) (F <$> liftedReplacement) (fromScope cond) - pure (ReplaceFun bounds' (toScope lhs') (toScope cond')) - Connected conn left right -> - Connected conn <$> go liftedArgs liftedReplacement left <*> go liftedArgs liftedReplacement right - Lambda scope -> do - scope' <- go (map (F <$>) liftedArgs) (F <$> liftedReplacement) (fromScope scope) - pure (Lambda (toScope scope')) - Quantified quant scope -> do - scope' <- go (map (F <$>) liftedArgs) (F <$> liftedReplacement) (fromScope scope) - pure (Quantified quant (toScope scope')) - PropositionalConstant p -> - Right (PropositionalConstant p) - Not loc expr -> - Not loc <$> go liftedArgs liftedReplacement expr - -matchesInductiveCarrier :: Eq a => FunctionSymbol -> [ExprOf a] -> ExprOf a -> Bool -matchesInductiveCarrier symbol targetArgs = \case - TermSymbol _loc (SymbolMixfix symbol') args -> - symbol == symbol' && sameInductiveArgs targetArgs args - _ -> - False - -sameInductiveArgs :: Eq a => [ExprOf a] -> [ExprOf a] -> Bool -sameInductiveArgs left right = - length left == length right && and (zipWith equivalent left right) - -orderedUniqueVars :: Ord a => [a] -> [a] -orderedUniqueVars = - reverse . snd . foldl' step (Set.empty, []) - where - step (seen, acc) x - | x `Set.member` seen = (seen, acc) - | otherwise = (Set.insert x seen, x : acc) - -inductiveCarrierTerm :: CheckedInductive -> Expr -inductiveCarrierTerm CheckedInductive{checkedInductiveSymbol, checkedInductiveParams} = - TermOp Nowhere checkedInductiveSymbol (TermVar <$> checkedInductiveParams) - -inductiveConditionFormula :: CheckedInductive -> CheckedInductiveCondition -> Formula -inductiveConditionFormula checked = - inductiveConditionFormulaAt checked (inductiveCarrierTerm checked) - -inductiveConditionFormulaAt :: CheckedInductive -> Expr -> CheckedInductiveCondition -> Formula -inductiveConditionFormulaAt _ replacement = \case - CheckedInductiveSideCondition phi -> - phi - CheckedInductiveRecursiveCondition{checkedInductiveRecursiveTerm, checkedInductiveRecursiveCarrierTemplate} -> - isElementOf checkedInductiveRecursiveTerm (instantiate1 replacement checkedInductiveRecursiveCarrierTemplate) - -semanticSubsetFormula :: Set VarSymbol -> Expr -> Expr -> Formula -semanticSubsetFormula reserved left right = - makeForall [witnessVar] - (isElementOf (TermVar witnessVar) left `Implies` isElementOf (TermVar witnessVar) right) - where - witnessVar = freshGeneratedVar (reserved <> freeVars left <> freeVars right) "x" - -inductiveSoundnessGoals :: CheckedInductive -> [Formula] -inductiveSoundnessGoals checked = - inductiveMonotonicityGoals checked <> inductiveDomainGoals checked - -inductiveMonotonicityGoals :: CheckedInductive -> [Formula] -inductiveMonotonicityGoals checked = - [ forallIfNeeded [leftVar, rightVar] - ( semanticSubsetFormula usedVars (TermVar leftVar) (TermVar rightVar) - `Implies` - semanticSubsetFormula usedVars - (instantiate1 (TermVar leftVar) checkedInductiveRecursiveCarrierTemplate) - (instantiate1 (TermVar rightVar) checkedInductiveRecursiveCarrierTemplate) - ) - | intro <- NonEmpty.toList (checkedInductiveIntros checked) - , CheckedInductiveRecursiveCondition{checkedInductiveRecursiveCarrierTemplate, checkedInductiveRecursiveDirect} <- checkedInductiveIntroConditions intro - , not checkedInductiveRecursiveDirect - ] - where - usedVars = inductiveUsedVars checked - leftVar = freshGeneratedVar usedVars "xa" - rightVar = freshGeneratedVar (Set.insert leftVar usedVars) "xb" - -inductiveDomainGoals :: CheckedInductive -> [Formula] -inductiveDomainGoals checked = - [ forallIfNeeded (orderedUniqueVars (checkedInductiveParams checked <> checkedInductiveIntroVars intro)) - (impliesFrom premises conclusion) - | intro <- NonEmpty.toList (checkedInductiveIntros checked) - , let premises = inductiveConditionFormulaAt checked (checkedInductiveDomain checked) <$> checkedInductiveIntroConditions intro - conclusion = isElementOf (checkedInductiveIntroResultTerm intro) (checkedInductiveDomain checked) - ] - -inductiveFacts - :: Marker - -> CheckedInductive - -> NonEmpty (Marker, Formula) -inductiveFacts marker checked = - inductiveIntroFacts marker checked - <> ( ( inductiveDomSubsetMarker marker - , inductiveDomSubsetFormula checked - ) - :| [ ( inductiveCasesMarker marker - , inductiveCasesFormula checked - ) - , ( inductiveInductMarker marker - , inductiveInductFormula checked - ) - ] - ) - -inductiveFactRoles - :: CheckedInductive - -> [LegacyInductiveFactRole] -inductiveFactRoles checked = - replicate - (length (checkedInductiveIntros checked)) - LegacyInductiveIntroduction - <> [ LegacyInductiveDomainSubset - , LegacyInductiveCases - , LegacyInductiveInduction - ] - -inductiveIntroFacts - :: Marker - -> CheckedInductive - -> NonEmpty (Marker, Formula) -inductiveIntroFacts marker checked = - NonEmpty.zipWith - (\index intro -> - ( inductiveIntroMarker marker index - , inductiveIntroFormula checked intro - )) - (1 :| [2 ..]) - (checkedInductiveIntros checked) - -inductiveIntroMarker :: Marker -> Int -> Marker -inductiveIntroMarker marker index = - Marker (inductiveMarkerText marker <> "_intro_" <> Text.pack (show index)) - -inductiveDomSubsetMarker :: Marker -> Marker -inductiveDomSubsetMarker marker = - Marker (inductiveMarkerText marker <> "_dom_subset") - -inductiveCasesMarker :: Marker -> Marker -inductiveCasesMarker marker = - Marker (inductiveMarkerText marker <> "_cases") - -inductiveInductMarker :: Marker -> Marker -inductiveInductMarker marker = - Marker (inductiveMarkerText marker <> "_induct") - -inductiveMarkerText :: Marker -> Text -inductiveMarkerText (Marker text) = text - -inductiveIntroFormula :: CheckedInductive -> CheckedInductiveIntro -> Formula -inductiveIntroFormula checked intro = - forallIfNeeded - (orderedUniqueVars (checkedInductiveParams checked <> checkedInductiveIntroVars intro)) - (impliesFrom premises conclusion) - where - premises = inductiveConditionFormula checked <$> checkedInductiveIntroConditions intro - conclusion = isElementOf (checkedInductiveIntroResultTerm intro) (inductiveCarrierTerm checked) - -inductiveDomSubsetFormula :: CheckedInductive -> Formula -inductiveDomSubsetFormula checked = - forallIfNeeded (checkedInductiveParams checked) - (semanticSubsetFormula (inductiveUsedVars checked) (inductiveCarrierTerm checked) (checkedInductiveDomain checked)) - -inductiveCasesFormula :: CheckedInductive -> Formula -inductiveCasesFormula checked = - forallIfNeeded - (orderedUniqueVars (checkedInductiveParams checked <> [witnessVar])) - (impliesFrom [isElementOf (TermVar witnessVar) (inductiveCarrierTerm checked)] (makeDisjunction disjuncts)) - where - witnessVar = freshGeneratedVar (inductiveUsedVars checked) "x" - disjuncts = inductiveCaseDisjunct witnessVar <$> NonEmpty.toList (checkedInductiveIntros checked) - inductiveCaseDisjunct x intro = - existsIfNeeded - (checkedInductiveIntroVars intro) - (makeConjunction (premises <> [Equals Nowhere (TermVar x) (checkedInductiveIntroResultTerm intro)])) - where - premises = inductiveConditionFormula checked <$> checkedInductiveIntroConditions intro - -inductiveInductFormula :: CheckedInductive -> Formula -inductiveInductFormula checked = - forallIfNeeded - (orderedUniqueVars (checkedInductiveParams checked <> [subsetVar])) - (impliesFrom closures conclusion) - where - subsetVar = freshGeneratedVar (inductiveUsedVars checked) "S" - closures = inductiveInductionClosure checked subsetVar <$> NonEmpty.toList (checkedInductiveIntros checked) - conclusion = - semanticSubsetFormula - (Set.insert subsetVar (inductiveUsedVars checked)) - (inductiveCarrierTerm checked) - (TermVar subsetVar) - -inductiveInductionClosure :: CheckedInductive -> VarSymbol -> CheckedInductiveIntro -> Formula -inductiveInductionClosure checked subsetVar intro = - forallIfNeeded (checkedInductiveIntroVars intro) (impliesFrom premises conclusion) - where - premises = inductiveConditionFormulaAt checked (TermVar subsetVar) <$> checkedInductiveIntroConditions intro - conclusion = isElementOf (checkedInductiveIntroResultTerm intro) (TermVar subsetVar) - -inductiveUsedVars :: CheckedInductive -> Set VarSymbol -inductiveUsedVars CheckedInductive{checkedInductiveParams, checkedInductiveIntros} = - Set.fromList - ( checkedInductiveParams - <> [ var - | intro <- NonEmpty.toList checkedInductiveIntros - , var <- checkedInductiveIntroVars intro - ] - ) - -checkStructDefn :: BlockContext -> StructDefn -> Checking -checkStructDefn context structDefn@StructDefn{..} = do - structGraph <- gets checkingStructs - resolvedParents <- - forM (Set.toList structParents) \parent -> - case StructGraph.lookup parent structGraph of - Nothing -> - throwIO - (UnknownStructureParent - parent - (blockContextLocation context) - (blockContextMarker context)) - Just struct -> - pure struct - let ancestors = - structParents - <> Set.unions (StructGraph.structAncestors <$> resolvedParents) - inheritedSymbols = - Set.unions (StructGraph.structSymbols <$> resolvedParents) - structContext = - structContextFromSymbols - structDefnLabel - (structDefnFixes <> inheritedSymbols) - assumptions <- - forM structDefnAssumes \(assumptionMarker, assumption) -> do - canonical <- - canonicalizeWithAt context structContext assumption - pure (assumptionMarker, canonical) - let canonicalStructDefn = - structDefn{structDefnAssumes = assumptions} - checked <- - either - (throwIO . structurePreparationCheckingError context) - pure - (Structure.prepareCheckedStructDefn - (blockContextLocation context) - (blockContextMarker context) - canonicalStructDefn - ancestors - inheritedSymbols) - st <- get - committed <- - either - throwIO - pure - (commitCheckedStructDefn context checked st) - putDeclarationCandidate committed - setDeclarationFactProducers - ( LegacyDeclarationRuleProducer - . LegacyStructureRule - <$> NonEmpty.toList - (Structure.checkedStructFactRoles checked) - ) - -structurePreparationCheckingError - :: BlockContext - -> Structure.StructurePreparationError - -> CheckingError -structurePreparationCheckingError context = \case - Structure.SelfReferentialStructure symbol -> - CheckingError - ( "structure definition of symbol " - <> symbolText symbol - <> " is self-referential" - ) - (blockContextLocation context) - (blockContextMarker context) - --- | Validate and commit every state row introduced by one structure. -commitCheckedStructDefn - :: BlockContext - -> Structure.CheckedStructDefn - -> CheckingState - -> Either CheckingError CheckingState -commitCheckedStructDefn context checked st = do - markers' <- - validatedMarkers - location - (NonEmpty.toList (Structure.checkedStructMarkers checked)) - st - (owners', ownedMarkers') <- - first (checkingErrorAt context) - (validatedOwnership - marker - OwnedByStructureDefinition - structureSymbol - st) - dependencies' <- - first - (checkingErrorAt context . dependencyRegistrationErrorText structureSymbol) - (Dependencies.registerDependencies - structureSymbol - semanticDependencies - (checkingDependencies st)) - traverse_ - (validatePreparedDependencies dependencies') - (Structure.checkedStructSemanticFacts checked) - facts' <- - first - (DuplicateMarker location) - (Facts.registerStagedFacts - (Structure.checkedStructFacts checked) - (checkingFacts st)) - pure - st - { checkingFacts = facts' - , checkingDependencies = dependencies' - , checkingOwnedSymbols = owners' - , checkingOwnedSymbolMarkers = ownedMarkers' - , checkingStructs = - StructGraph.insert - (Structure.checkedStructPhrase checked) - (Structure.checkedStructAncestors checked) - (Structure.checkedStructInternalSymbols checked) - (Structure.checkedStructAllSymbols checked) - (checkingStructs st) - , definedMarkers = markers' - , blockLabel = marker - , stepLocation = location - , checkingHypothesisCounter = 0 - } - where - location = blockContextLocation context - marker = blockContextMarker context - structureSymbol = Structure.checkedStructSymbol checked - semanticDependencies = - Set.filter ownableSymbol - (Structure.checkedStructDependencies checked) - - validatePreparedDependencies dependencyRegistry prepared = - case - Set.lookupMin - ( Set.filter - (\dependency -> - ownableSymbol dependency - && isNothing - (Dependencies.lookupDependencies - dependency - dependencyRegistry)) - (Facts.preparedSemanticDependencies prepared) - ) - of - Nothing -> - Right () - Just unknown -> - Left - (checkingErrorAt context - ( "structure fact depends on unknown symbol " - <> symbolText unknown - )) - -checkingErrorAt :: BlockContext -> Text -> CheckingError -checkingErrorAt context message = - CheckingError - message - (blockContextLocation context) - (blockContextMarker context) - - -fixing :: NonEmpty VarSymbol -> Checking -fixing xs = do - goals <- gets checkingGoals - (goal, goals') <- case goals of - goal : goals' -> return (goal, goals') - _ -> throwWithLocationAndMarker (CheckingError "No open goals, cannot use \"fix\" step") - goal' <- case goal of - Forall body | [_bv] <- nubOrd (bindings body) -> - -- If there's only one quantified variable we can freely choose a new name. - -- This is useful for nameless quantified phrases such as @every _ is an element of _@. - case xs of - x :| [] -> return (instantiate (\_bv -> TermVar x) body) - _ -> throwWithLocationAndMarker (CheckingError "Couldn't use \"fix\" step: only one bound variable but multiple variables to be fixed") - Forall body | toList xs `List.intersect` nubOrd (bindings body) == toList xs -> - return (Forall (instantiateSome xs body)) - Forall body -> - throwWithLocationAndMarker (CheckingError ("You can only use a \"fix\" step if all specified variables occur in the outermost quantifier. Variables to be fixed were: " - <> Text.pack (show xs) <> " but only the following are bound: " <> Text.pack (show (nubOrd (bindings body))))) - _ -> - throwWithLocationAndMarker (CheckingError "You can only use a \"fix\" step if the goal is universal.") - setGoals (goal' : goals') - --- | A trusted rule that reduces a goal after introducing one assumption. -data GoalReduction - = ImplicationIntroduction Formula Formula - | CurryLeftConjunct Formula Formula Formula - | CurryRightConjunct Formula Formula Formula - deriving (Show, Eq) - -goalReductionAssumption :: GoalReduction -> Formula -goalReductionAssumption = \case - ImplicationIntroduction assumption _conclusion -> - assumption - CurryLeftConjunct assumption _right _conclusion -> - assumption - CurryRightConjunct _left assumption _conclusion -> - assumption - -goalReductionResidual :: GoalReduction -> Formula -goalReductionResidual = \case - ImplicationIntroduction _assumption conclusion -> - conclusion - CurryLeftConjunct _assumption right conclusion -> - right `Implies` conclusion - CurryRightConjunct left _assumption conclusion -> - left `Implies` conclusion - -reduceGoalWithAssumption :: Formula -> Formula -> Maybe GoalReduction -reduceGoalWithAssumption assumption = \case - (left `And` right) `Implies` conclusion - | equivalent left assumption -> - Just (CurryLeftConjunct assumption right conclusion) - | equivalent right assumption -> - Just (CurryRightConjunct left assumption conclusion) - antecedent `Implies` conclusion - | equivalent antecedent assumption -> - Just (ImplicationIntroduction assumption conclusion) - _ -> - Nothing - --- | An assumption step in a proof is supposed to match the goal. -matchAssumptionWithGoal :: Location -> Formula -> CheckingM [Formula] -matchAssumptionWithGoal loc asm = do - asm' <- canonicalize asm - goals <- gets checkingGoals - (goal, goals') <- case goals of - goal : goals' -> - pure (goal, goals') - [] -> - impossible "assumption proof step without an open goal" - defns <- gets checkingPredicateDefinitions - case reduceGoalWithAssumption asm' goal of - Just reduction -> - pure (goalReductionResidual reduction : goals') - -- - -- Unfolding definitions against atomic goals - Nothing -> case goal of - phi@(Atomic _pos p args) -> - let rhos = (HM.lookup p defns ?? []) - rhos' = - [ instantiate - (\k -> - nth k args - ?? impossible - "predicate definition index exceeds application arity") - (absurd <$> rho) - | rho <- rhos - ] - in case firstJust (reduceGoalWithAssumption asm') rhos' of - Nothing -> throwWithMarker (MismatchedAssume asm' phi loc) - Just reduction -> - pure (goalReductionResidual reduction : goals') - phi -> throwWithMarker (MismatchedAssume asm' phi loc) - - -checkAbbr :: BlockContext -> Abbreviation -> Checking -checkAbbr context (Abbreviation symbol scope) = do - scope' <- transverseScope unabbreviate scope - when (mentionsSymbol symbol (fromScope scope')) do - throwIO - (checkingErrorAt - context - "abbreviation is self-referential") - st <- get - either - throwIO - put - (commitAbbreviation context symbol scope' st) - --- | Validate and commit every state row introduced by one abbreviation. -commitAbbreviation - :: BlockContext - -> Symbol - -> Scope Int ExprOf Void - -> CheckingState - -> Either CheckingError CheckingState -commitAbbreviation context symbol scope st = do - markers' <- - validatedMarkers location [marker] st - (owners', ownedMarkers', dependencies') <- - validatedSymbolRegistration - context - OwnedByAbbreviation - symbol - mempty - st - pure - st - { checkingAbbreviations = - HM.insert - symbol - scope - (checkingAbbreviations st) - , checkingDependencies = dependencies' - , checkingOwnedSymbols = owners' - , checkingOwnedSymbolMarkers = ownedMarkers' - , definedMarkers = markers' - , blockLabel = marker - , stepLocation = location - , checkingHypothesisCounter = 0 - } - where - location = - blockContextLocation context - marker = - blockContextMarker context |