Make inductive declarations transactional

1 files changed, 168 insertions, 141 deletions

diff --git a/source/Checking.hs b/source/Checking.hs
index 0d69a58..2af7c69 100644
--- a/source/Checking.hs
+++ b/source/Checking.hs
@@ -545,60 +545,6 @@ symbolOwnerByMarker :: Marker -> HashMap Symbol SymbolOwner -> Maybe SymbolOwner
 symbolOwnerByMarker marker owners =
     snd <$> List.find ((== Just marker) . objectSymbolMarker . fst) (HM.toList owners)
 
-assertOwnedSymbolsInFormula :: Formula -> Checking
-assertOwnedSymbolsInFormula phi = do
-    assertOwnedDependencies (mentionedSymbols phi)
-
-assertOwnedDependencies :: Set Symbol -> Checking
-assertOwnedDependencies dependencies = do
-    owners <- gets checkingOwnedSymbols
-    let unknown =
-            Set.filter
-                (\symbol -> ownableSymbol symbol && not (HM.member symbol owners))
-                dependencies
-    unless (Set.null unknown) do
-        throwCheckingError ("top-level fact mentions symbol(s) without prior ownership: " <> formatSymbols unknown)
-
-claimSymbolOwnership :: SymbolOwnerKind -> Symbol -> Checking
-claimSymbolOwnership ownerKind symbol =
-    claimSymbolOwnershipWithDependencies ownerKind symbol mempty
-
-claimSymbolOwnershipWithDependencies
-    :: SymbolOwnerKind
-    -> Symbol
-    -> Set Symbol
-    -> Checking
-claimSymbolOwnershipWithDependencies ownerKind symbol dependencies =
-    case objectSymbolMarker symbol of
-        Nothing ->
-            skip
-        Just _marker -> do
-            st <- get
-            let currentMarker = blockLabel st
-            (owners', ownedMarkers') <-
-                either
-                    throwCheckingError
-                    pure
-                    (validatedOwnership
-                        currentMarker
-                        ownerKind
-                        symbol
-                        st)
-            dependencyRegistry <-
-                either
-                    (throwCheckingError . dependencyRegistrationErrorText symbol)
-                    pure
-                    (Dependencies.registerDependencies
-                        symbol
-                        (Set.filter ownableSymbol dependencies)
-                        (checkingDependencies st))
-            put
-                st
-                    { checkingOwnedSymbols = owners'
-                    , checkingOwnedSymbolMarkers = ownedMarkers'
-                    , checkingDependencies = dependencyRegistry
-                    }
-
 validatedOwnership
     :: Marker
     -> SymbolOwnerKind
@@ -752,18 +698,6 @@ validatePreparedSemanticFact context owners dependencies prepared = do
                             dependencies))
             semanticDependencies
 
-freezeSymbols :: Set Symbol -> Checking
-freezeSymbols symbols = do
-    currentMarker <- gets blockLabel
-    let frozen =
-            HM.fromList
-                [ (symbol, currentMarker)
-                | symbol <- Set.toList symbols
-                , ownableSymbol symbol
-                ]
-    modify \st ->
-        st{checkingFrozenSymbols = HM.union (checkingFrozenSymbols st) frozen}
-
 checkedInductiveMentionedSymbols :: CheckedInductive -> Set Symbol
 checkedInductiveMentionedSymbols CheckedInductive{checkedInductiveSymbol, checkedInductiveDomain, checkedInductiveIntros} =
     Set.insert
@@ -1005,23 +939,6 @@ factHypotheses facts =
     | (marker, fact) <- Facts.registeredFacts facts
     ]
 
-prepareFact :: Formula -> CheckingM Facts.PreparedSemanticFact
-prepareFact phi = do
-    assertOwnedSymbolsInFormula phi
-    pure (Facts.prepareSemanticFact phi)
-
-registerPreparedFacts
-    :: NonEmpty Facts.StagedFact
-    -> Checking
-registerPreparedFacts staged = do
-    facts <- gets checkingFacts
-    case Facts.registerStagedFacts staged facts of
-        Left duplicate ->
-            throwWithLocationAndMarker
-                (\loc _blockMarker -> DuplicateMarker loc duplicate)
-        Right facts' ->
-            modify \st -> st{checkingFacts = facts'}
-
 stagePreparedFact
     :: Location
     -> Marker
@@ -1033,25 +950,6 @@ stagePreparedFact loc blockMarker factMarker =
         (factMarker :| [])
         (Facts.factOrigin loc blockMarker)
 
--- | Make a fact available to all future paragraphs.
-addFacts :: [(Marker, Formula)] -> Checking
-addFacts phis = do
-    loc <- gets stepLocation
-    reserveMarkers loc (fst <$> phis)
-    blockMarker <- gets blockLabel
-    staged <- forM phis \(marker, phi) -> do
-        phi' <- canonicalize phi
-        prepared <- prepareFact phi'
-        pure (stagePreparedFact loc blockMarker marker prepared)
-    for_ (NonEmpty.nonEmpty staged) registerPreparedFacts
-
-
-reserveMarkers :: Location -> [Marker] -> Checking
-reserveMarkers loc markers = do
-    st <- get
-    either throwIO (\markers' -> put st{definedMarkers = markers'})
-        (validatedMarkers loc markers st)
-
 validatedMarkers
     :: Location
     -> [Marker]
@@ -1271,7 +1169,10 @@ checkBlocks = \case
         checkDatatype (BlockContext loc marker) datatype
         checkBlocks blocks
     BlockInductive loc marker inductiveDefn : blocks -> do
-        withLabel loc marker (checkInductive inductiveDefn)
+        let context = BlockContext loc marker
+        withBlockContext
+            context
+            (checkInductive context inductiveDefn)
         checkBlocks blocks
     BlockStruct loc marker structDefn : blocks -> do
         checkStructDefn (BlockContext loc marker) structDefn
@@ -1289,14 +1190,6 @@ withBlockContext BlockContext{blockContextLocation, blockContextMarker} ma = do
             }
     ma
 
--- | Reserve a non-structure block label and make it current.
-withLabel :: Location -> Marker -> CheckingM a -> CheckingM a
-withLabel loc marker ma = do
-    reserveMarkers loc [marker]
-    -- Set the marker as the label of the current block and upate the step location.
-    modify \st -> st{blockLabel = marker, stepLocation = loc, checkingHypothesisCounter = 0}
-    ma
-
 -- | 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
@@ -2160,18 +2053,138 @@ data CheckedInductiveCondition
         , checkedInductiveRecursiveDirect :: Bool
         }
 
-checkInductive :: Inductive -> Checking
-checkInductive inductive = do
-    claimSymbolOwnership OwnedByInductiveDefinition (SymbolMixfix (inductiveSymbol inductive))
+checkInductive :: BlockContext -> Inductive -> Checking
+checkInductive context inductive = do
+    st <- get
+    either
+        throwIO
+        pure
+        (validateInductiveHeader
+            context
+            (SymbolMixfix (inductiveSymbol inductive))
+            st)
     checked <- normalizeInductive inductive
-    frozenSymbols <- checkedInductiveFrozenSymbols checked
-    freezeSymbols frozenSymbols
-    let goals = inductiveSoundnessGoals checked
-    unless (null goals) do
-        setGoals goals
-        tellTasks
-    marker <- gets blockLabel
-    addFacts (inductiveFacts marker checked)
+    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
+    put committed
+
+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
@@ -2226,18 +2239,15 @@ ensureInductiveDefinitionIndependence checked = do
                 [] ->
                     error "definitionDependencyPath returned an empty path"
 
-checkedInductiveFrozenSymbols :: CheckedInductive -> CheckingM (Set Symbol)
-checkedInductiveFrozenSymbols checked = do
-    graph <- gets checkingDependencies
+checkedInductiveFrozenSymbols
+    :: Dependencies.DependencyRegistry
+    -> CheckedInductive
+    -> Either Symbol (Set Symbol)
+checkedInductiveFrozenSymbols graph checked =
     let seeds =
             Set.filter ownableSymbol
                 (checkedInductiveMentionedSymbols checked)
-    either
-        (\unknown ->
-            throwCheckingError
-                ("inductive specification mentions unknown symbol " <> symbolText unknown))
-        pure
-        (Dependencies.dependencyClosure graph seeds)
+    in Dependencies.dependencyClosure graph seeds
 
 normalizeInductiveIntro :: FunctionSymbol -> [VarSymbol] -> IntroRule -> CheckingM CheckedInductiveIntro
 normalizeInductiveIntro symbol params IntroRule{introConditions, introResult} = do
@@ -2412,19 +2422,36 @@ inductiveDomainGoals checked =
           conclusion = isElementOf (checkedInductiveIntroResultTerm intro) (checkedInductiveDomain checked)
     ]
 
-inductiveFacts :: Marker -> CheckedInductive -> [(Marker, Formula)]
+inductiveFacts
+    :: Marker
+    -> CheckedInductive
+    -> NonEmpty (Marker, Formula)
 inductiveFacts marker checked =
     inductiveIntroFacts marker checked
-        <> [ (inductiveDomSubsetMarker marker, inductiveDomSubsetFormula checked)
-           , (inductiveCasesMarker marker, inductiveCasesFormula checked)
-           , (inductiveInductMarker marker, inductiveInductFormula checked)
-           ]
-
-inductiveIntroFacts :: Marker -> CheckedInductive -> [(Marker, Formula)]
+        <> ( ( inductiveDomSubsetMarker marker
+             , inductiveDomSubsetFormula checked
+             )
+                :| [ ( inductiveCasesMarker marker
+                      , inductiveCasesFormula checked
+                      )
+                   , ( inductiveInductMarker marker
+                     , inductiveInductFormula checked
+                     )
+                   ]
+           )
+
+inductiveIntroFacts
+    :: Marker
+    -> CheckedInductive
+    -> NonEmpty (Marker, Formula)
 inductiveIntroFacts marker checked =
-    [ (inductiveIntroMarker marker index, inductiveIntroFormula checked intro)
-    | (index, intro) <- zip [(1 :: Int)..] (NonEmpty.toList (checkedInductiveIntros checked))
-    ]
+    NonEmpty.zipWith
+        (\index intro ->
+            ( inductiveIntroMarker marker index
+            , inductiveIntroFormula checked intro
+            ))
+        (1 :| [2 ..])
+        (checkedInductiveIntros checked)
 
 inductiveIntroMarker :: Marker -> Int -> Marker
 inductiveIntroMarker marker index =