Add location info to implicit QED step

6 files changed, 22 insertions, 25 deletions

diff --git a/source/Checking.hs b/source/Checking.hs
index b3e5a2f..a79ef5a 100644
--- a/source/Checking.hs
+++ b/source/Checking.hs
@@ -59,6 +59,7 @@ check dumpPremselTraining lexicon blocks = do
             , checkingLexicon = lexicon
             , blockLabel = Marker ""
             , stepLocation = Nowhere
+            , blockEndLocation = Nowhere
             , fixedVars = mempty
             }
 
@@ -115,6 +116,7 @@ data CheckingState = CheckingState
     --
     , 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.
     }
 
 initCheckingStructs :: StructGraph
@@ -339,14 +341,15 @@ checkBlocks = \case
     BlockAbbr pos marker abbr : blocks -> do
         withLabel pos marker  (checkAbbr abbr)
         checkBlocks blocks
-    BlockLemma pos marker lemma : BlockProof _pos2 proof : blocks -> do
+    BlockLemma pos marker lemma : BlockProof _startLoc endLoc proof : blocks -> do
+        modify \st -> st{blockEndLocation = endLoc}
         withLabel pos marker (checkLemmaWithProof lemma proof)
         checkBlocks blocks
     BlockLemma pos marker  lemma : blocks -> do
         withLabel pos marker (checkLemma lemma)
         checkBlocks blocks
-    BlockProof pos _proof : _ ->
-        throwWithMarker (ProofWithoutPrecedingTheorem pos)
+    BlockProof startLoc _endLoc _proof : _ ->
+        throwWithMarker (ProofWithoutPrecedingTheorem startLoc)
     BlockSig _pos asms sig : blocks -> do
         checkSig asms sig
         checkBlocks blocks
@@ -401,21 +404,12 @@ checkAxiom (Axiom asms axiom) = addFactWithAsms asms axiom
 checkProof :: Proof -> Checking
 checkProof = \case
     Qed mloc j -> do
-        case mloc of
-            Just loc -> setLocation loc
-            Nothing -> skip
-        case j of
-            JustificationEmpty -> tellTasks
-            JustificationRef ms -> byRef ms
-            JustificationLocal -> byAssumption
-            JustificationSetExt -> do
-                goals <- gets checkingGoals
-                case goals of
-                    [goal] -> do
-                        goals' <- splitGoalWithSetExt goal
-                        setGoals goals'
-                    [] -> pure ()
-                    _ -> throwWithLocationAndMarker (MismatchedSetExt goals)
+        loc <- case mloc of
+                Just loc -> pure loc
+                Nothing -> do
+                    gets blockEndLocation
+        setLocation loc
+        justify j
     ByContradiction loc proof -> do
         setLocation loc
         goals <- gets checkingGoals
diff --git a/source/Meaning.hs b/source/Meaning.hs
index 215bae9..c8057ca 100644
--- a/source/Meaning.hs
+++ b/source/Meaning.hs
@@ -775,8 +775,8 @@ glossBlock = \case
         Sem.BlockAxiom pos marker <$> glossAxiom axiom
     Raw.BlockLemma pos marker lemma ->
         Sem.BlockLemma pos marker <$> glossLemma lemma
-    Raw.BlockProof pos proof ->
-        Sem.BlockProof pos <$> glossProof proof
+    Raw.BlockProof startLoc proof endLoc ->
+        Sem.BlockProof startLoc endLoc <$> glossProof proof
     Raw.BlockDefn pos marker defn -> do
         defn' <- glossDefn defn
         whenLeft (isWellformedDefn defn') (\err -> throwError (GlossDefnError err marker))
diff --git a/source/Megalodon.hs b/source/Megalodon.hs
index 295ab15..e7dfeb5 100644
--- a/source/Megalodon.hs
+++ b/source/Megalodon.hs
@@ -30,7 +30,7 @@ buildBlocks lexi = \case
     BlockAxiom _pos lbl (Axiom asms stmt) : blocks ->
         let phi = closure (unAsm <$> asms) stmt
         in text "Fact " <> buildMarker lbl <> text " : " <> buildFormula lexi phi <> text ".\nAdmitted.\n" <> buildBlocks lexi blocks
-    BlockLemma _pos lbl (Lemma asms stmt) : BlockProof _ _ : blocks ->
+    BlockLemma _pos lbl (Lemma asms stmt) : BlockProof _ _ _ : blocks ->
         let phi = closure (unAsm <$> asms) stmt
         in text "Theorem " <> buildMarker lbl <> text " : " <> buildFormula lexi phi <> text ".\nAdmitted.\n" <> buildBlocks lexi blocks
     BlockLemma _pos lbl (Lemma asms stmt) : blocks ->
diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs
index 4926ca0..94e33fb 100644
--- a/source/Syntax/Abstract.hs
+++ b/source/Syntax/Abstract.hs
@@ -499,7 +499,7 @@ instance IsString Marker where
 data Block
     = BlockAxiom Location Marker Axiom
     | BlockLemma Location Marker Lemma
-    | BlockProof Location Proof
+    | BlockProof Location Proof Location -- ^ Proof start and ending location.
     | BlockDefn Location Marker Defn
     | BlockAbbr Location Marker Abbreviation
     | BlockData Location Datatype
diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs
index 4c34b57..30e57ea 100644
--- a/source/Syntax/Concrete.hs
+++ b/source/Syntax/Concrete.hs
@@ -416,7 +416,7 @@ grammar lexicon@Lexicon{..} = mdo
 
     blockAxiom  <- rule $ uncurry3 BlockAxiom     <$> envPos  "axiom" axiom
     blockLemma  <- rule $ uncurry3 BlockLemma     <$> lemmaEnv lemma
-    blockProof  <- rule $ uncurry  BlockProof     <$> envPos_ "proof" proof
+    blockProof  <- rule $ uncurry3 BlockProof     <$> envStartEndLocation "proof" proof
     blockDefn   <- rule $ uncurry3 BlockDefn      <$> envPos "definition" defn
     blockAbbr   <- rule $ uncurry3 BlockAbbr      <$> envPos "abbreviation" abbreviation
     blockData   <- rule $ uncurry  BlockData      <$> envPos_ "datatype" datatype
@@ -647,6 +647,9 @@ envPos kind body = do
 envPos_ :: Text -> Prod r Text (Located Token) a -> Prod r Text (Located Token) (Location, a)
 envPos_ kind body = (,) <$> begin kind <*> (optional label *> body) <* end kind
 
+envStartEndLocation :: Text -> Prod r Text (Located Token) a -> Prod r Text (Located Token) (Location, a, Location)
+envStartEndLocation kind body = (,,) <$> begin kind <*> (optional label *> body) <*> end kind
+
 env_ :: Text -> Prod r Text (Located Token) a -> Prod r Text (Located Token) a
 env_ kind body = begin kind *> optional label *> body <* end kind
 
diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs
index 42829bb..52c9099 100644
--- a/source/Syntax/Internal.hs
+++ b/source/Syntax/Internal.hs
@@ -412,7 +412,7 @@ data Proof
     = Omitted
     -- ^ Ends a proof without further verification.
     -- This results in a “gap” in the formalization.
-    | Qed {mpos :: Maybe Location, by :: Justification}
+    | Qed {mloc :: Maybe Location, by :: Justification}
     -- ^ Ends of a proof, leaving automation to discharge the current goal using the given justification.
     | ByContradiction Location Proof
     -- ^ Take the dual of the current goal as an assumption and
@@ -549,7 +549,7 @@ data Abbreviation
 data Block
     = BlockAxiom Location Marker Axiom
     | BlockLemma Location Marker Lemma
-    | BlockProof Location Proof
+    | BlockProof Location Location Proof
     | BlockDefn Location Marker Defn
     | BlockAbbr Location Marker Abbreviation
     | BlockStruct Location Marker StructDefn