diff options
36 files changed, 192 insertions, 63 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 diff --git a/test/golden/byRef/encoding tasks.golden b/test/golden/byRef/encoding tasks.golden index 3038289..81d12f7 100644 --- a/test/golden/byRef/encoding tasks.golden +++ b/test/golden/byRef/encoding tasks.golden @@ -9,7 +9,7 @@ fof(prop1,axiom,![Xa]:Xa=Xa). fof(prop4,conjecture,![Xd]:Xd=Xd,"test/examples/byRef.tex 20:5"). fof(prop1,axiom,![Xa]:Xa=Xa). ------------------ -fof(prop4,conjecture,fe=fe,"test/examples/byRef.tex 20:5"). +fof(prop4,conjecture,fe=fe,"test/examples/byRef.tex 21:1"). fof(prop3,axiom,![Xc]:Xc=Xc). fof(prop2,axiom,![Xb]:Xb=Xb). fof(prop1,axiom,![Xa]:Xa=Xa). diff --git a/test/golden/byRef/generating tasks.golden b/test/golden/byRef/generating tasks.golden index e707cec..b6fe103 100644 --- a/test/golden/byRef/generating tasks.golden +++ b/test/golden/byRef/generating tasks.golden @@ -320,8 +320,8 @@ , taskConjectureLabel = Marker "prop4" , taskLocation = Location { locFile = "test/examples/byRef.tex" - , locLine = 20 - , locColumn = 5 + , locLine = 21 + , locColumn = 1 } , taskConjecture = TermSymbol ( Location diff --git a/test/golden/byRef/glossing.golden b/test/golden/byRef/glossing.golden index 38204d8..f236b83 100644 --- a/test/golden/byRef/glossing.golden +++ b/test/golden/byRef/glossing.golden @@ -89,8 +89,14 @@ , locColumn = 1 } ) + ( Location + { locFile = "test/examples/byRef.tex" + , locLine = 14 + , locColumn = 1 + } + ) ( Qed - { mpos = Just + { mloc = Just ( Location { locFile = "test/examples/byRef.tex" , locLine = 13 @@ -136,6 +142,12 @@ , locColumn = 1 } ) + ( Location + { locFile = "test/examples/byRef.tex" + , locLine = 21 + , locColumn = 1 + } + ) ( Have ( Location { locFile = "test/examples/byRef.tex" @@ -173,7 +185,7 @@ ( Marker "prop1" :| [] ) ) ( Qed - { mpos = Nothing + { mloc = Nothing , by = JustificationEmpty } ) diff --git a/test/golden/byRef/parsing.golden b/test/golden/byRef/parsing.golden index de15f45..7ef9886 100644 --- a/test/golden/byRef/parsing.golden +++ b/test/golden/byRef/parsing.golden @@ -108,6 +108,12 @@ ( Marker "prop1" :| [] ) ) ) + ( Location + { locFile = "test/examples/byRef.tex" + , locLine = 14 + , locColumn = 1 + } + ) , BlockLemma ( Location { locFile = "test/examples/byRef.tex" @@ -187,6 +193,12 @@ ( Marker "prop1" :| [] ) ) ( Qed Nothing JustificationEmpty ) ) + ( Location + { locFile = "test/examples/byRef.tex" + , locLine = 21 + , locColumn = 1 + } + ) , BlockLemma ( Location { locFile = "test/examples/byRef.tex" diff --git a/test/golden/calc/encoding tasks.golden b/test/golden/calc/encoding tasks.golden index ec9a6eb..ee28b36 100644 --- a/test/golden/calc/encoding tasks.golden +++ b/test/golden/calc/encoding tasks.golden @@ -10,7 +10,7 @@ fof(trivial,axiom,![Xx]:Xx=Xx). fof(alsotrivial,conjecture,fy=fy,"test/examples/calc.tex 13:5"). fof(trivial,axiom,![Xx]:Xx=Xx). ------------------ -fof(alsotrivial,conjecture,fy=fy,"test/examples/calc.tex 13:5"). +fof(alsotrivial,conjecture,fy=fy,"test/examples/calc.tex 20:1"). fof(irrelevant,axiom,![Xz]:Xz=Xz). fof(trivial,axiom,![Xx]:Xx=Xx). fof(alsotrivial1,axiom,fy=fy). @@ -23,7 +23,7 @@ fof(trivial,axiom,![Xx]:Xx=Xx). fof(trivial_biconditionals,conjecture,fy=fy,"test/examples/calc.tex 26:5"). fof(trivial,axiom,![Xx]:Xx=Xx). ------------------ -fof(trivial_biconditionals,conjecture,fy=fy,"test/examples/calc.tex 26:5"). +fof(trivial_biconditionals,conjecture,fy=fy,"test/examples/calc.tex 33:1"). fof(alsotrivial,axiom,![Xy]:Xy=Xy). fof(irrelevant,axiom,![Xz]:Xz=Xz). fof(trivial,axiom,![Xx]:Xx=Xx). diff --git a/test/golden/calc/generating tasks.golden b/test/golden/calc/generating tasks.golden index abe8f45..b853856 100644 --- a/test/golden/calc/generating tasks.golden +++ b/test/golden/calc/generating tasks.golden @@ -304,8 +304,8 @@ , taskConjectureLabel = Marker "alsotrivial" , taskLocation = Location { locFile = "test/examples/calc.tex" - , locLine = 13 - , locColumn = 5 + , locLine = 20 + , locColumn = 1 } , taskConjecture = TermSymbol ( Location @@ -624,8 +624,8 @@ , taskConjectureLabel = Marker "trivial_biconditionals" , taskLocation = Location { locFile = "test/examples/calc.tex" - , locLine = 26 - , locColumn = 5 + , locLine = 33 + , locColumn = 1 } , taskConjecture = TermSymbol ( Location diff --git a/test/golden/calc/glossing.golden b/test/golden/calc/glossing.golden index 185b815..41e307c 100644 --- a/test/golden/calc/glossing.golden +++ b/test/golden/calc/glossing.golden @@ -89,6 +89,12 @@ , locColumn = 1 } ) + ( Location + { locFile = "test/examples/calc.tex" + , locLine = 20 + , locColumn = 1 + } + ) ( Calc ( Location { locFile = "test/examples/calc.tex" @@ -115,7 +121,7 @@ ) ) ( Qed - { mpos = Nothing + { mloc = Nothing , by = JustificationEmpty } ) @@ -155,6 +161,12 @@ , locColumn = 1 } ) + ( Location + { locFile = "test/examples/calc.tex" + , locLine = 33 + , locColumn = 1 + } + ) ( Calc ( Location { locFile = "test/examples/calc.tex" @@ -210,7 +222,7 @@ ) ) ( Qed - { mpos = Nothing + { mloc = Nothing , by = JustificationEmpty } ) diff --git a/test/golden/calc/parsing.golden b/test/golden/calc/parsing.golden index 749f903..d674c0f 100644 --- a/test/golden/calc/parsing.golden +++ b/test/golden/calc/parsing.golden @@ -121,6 +121,12 @@ ) ) ( Qed Nothing JustificationEmpty ) ) + ( Location + { locFile = "test/examples/calc.tex" + , locLine = 20 + , locColumn = 1 + } + ) , BlockLemma ( Location { locFile = "test/examples/calc.tex" @@ -203,4 +209,10 @@ ) ) ( Qed Nothing JustificationEmpty ) ) + ( Location + { locFile = "test/examples/calc.tex" + , locLine = 33 + , locColumn = 1 + } + ) ]
\ No newline at end of file diff --git a/test/golden/no-reflexive-set/glossing.golden b/test/golden/no-reflexive-set/glossing.golden index fc60015..befc74b 100644 --- a/test/golden/no-reflexive-set/glossing.golden +++ b/test/golden/no-reflexive-set/glossing.golden @@ -51,6 +51,12 @@ , locColumn = 1 } ) + ( Location + { locFile = "test/examples/no-reflexive-set.tex" + , locLine = 11 + , locColumn = 1 + } + ) ( BySetInduction ( Location { locFile = "test/examples/no-reflexive-set.tex" @@ -59,7 +65,7 @@ } ) Nothing ( Qed - { mpos = Just + { mloc = Just ( Location { locFile = "test/examples/no-reflexive-set.tex" , locLine = 10 diff --git a/test/golden/no-reflexive-set/parsing.golden b/test/golden/no-reflexive-set/parsing.golden index b529ae8..b15c698 100644 --- a/test/golden/no-reflexive-set/parsing.golden +++ b/test/golden/no-reflexive-set/parsing.golden @@ -77,4 +77,10 @@ ) JustificationEmpty ) ) + ( Location + { locFile = "test/examples/no-reflexive-set.tex" + , locLine = 11 + , locColumn = 1 + } + ) ]
\ No newline at end of file diff --git a/test/golden/proofassume/encoding tasks.golden b/test/golden/proofassume/encoding tasks.golden index 16c4a45..1311590 100644 --- a/test/golden/proofassume/encoding tasks.golden +++ b/test/golden/proofassume/encoding tasks.golden @@ -1,7 +1,7 @@ fof(assumetest,conjecture,elem(fx,fy),"test/examples/proofassume.tex 6:5"). fof(assumetest1,axiom,elem(fx,fy)). ------------------ -fof(assumetest,conjecture,elem(fx,fy),"test/examples/proofassume.tex 6:5"). +fof(assumetest,conjecture,elem(fx,fy),"test/examples/proofassume.tex 7:1"). fof(assumetest1,axiom,elem(fx,fy)). fof(assumetest2,axiom,elem(fx,fy)). ------------------ @@ -10,7 +10,7 @@ fof(assumetest,axiom,![Xx,Xy]:(elem(Xx,Xy)=>elem(Xx,Xy))). fof(assumetesttwo1,axiom,elem(fx,fy)). fof(assumetesttwo2,axiom,elem(fa,fb)). ------------------ -fof(assumetesttwo,conjecture,elem(fx,fy),"test/examples/proofassume.tex 15:5"). +fof(assumetesttwo,conjecture,elem(fx,fy),"test/examples/proofassume.tex 16:1"). fof(assumetest,axiom,![Xx,Xy]:(elem(Xx,Xy)=>elem(Xx,Xy))). fof(assumetesttwo1,axiom,elem(fx,fy)). fof(assumetesttwo2,axiom,elem(fx,fy)). diff --git a/test/golden/proofassume/generating tasks.golden b/test/golden/proofassume/generating tasks.golden index 9098694..0d61018 100644 --- a/test/golden/proofassume/generating tasks.golden +++ b/test/golden/proofassume/generating tasks.golden @@ -93,8 +93,8 @@ , taskConjectureLabel = Marker "assumetest" , taskLocation = Location { locFile = "test/examples/proofassume.tex" - , locLine = 6 - , locColumn = 5 + , locLine = 7 + , locColumn = 1 } , taskConjecture = TermSymbol ( Location @@ -353,8 +353,8 @@ , taskConjectureLabel = Marker "assumetesttwo" , taskLocation = Location { locFile = "test/examples/proofassume.tex" - , locLine = 15 - , locColumn = 5 + , locLine = 16 + , locColumn = 1 } , taskConjecture = TermSymbol ( Location diff --git a/test/golden/proofassume/glossing.golden b/test/golden/proofassume/glossing.golden index 7ce9761..7668356 100644 --- a/test/golden/proofassume/glossing.golden +++ b/test/golden/proofassume/glossing.golden @@ -53,6 +53,12 @@ , locColumn = 1 } ) + ( Location + { locFile = "test/examples/proofassume.tex" + , locLine = 7 + , locColumn = 1 + } + ) ( Assume ( Location { locFile = "test/examples/proofassume.tex" @@ -104,7 +110,7 @@ ] ) JustificationEmpty ( Qed - { mpos = Nothing + { mloc = Nothing , by = JustificationEmpty } ) @@ -185,6 +191,12 @@ , locColumn = 1 } ) + ( Location + { locFile = "test/examples/proofassume.tex" + , locLine = 16 + , locColumn = 1 + } + ) ( Assume ( Location { locFile = "test/examples/proofassume.tex" @@ -261,7 +273,7 @@ ] ) JustificationEmpty ( Qed - { mpos = Nothing + { mloc = Nothing , by = JustificationEmpty } ) diff --git a/test/golden/proofassume/parsing.golden b/test/golden/proofassume/parsing.golden index 1b7837f..1b0276d 100644 --- a/test/golden/proofassume/parsing.golden +++ b/test/golden/proofassume/parsing.golden @@ -120,6 +120,12 @@ ) JustificationEmpty ( Qed Nothing JustificationEmpty ) ) ) + ( Location + { locFile = "test/examples/proofassume.tex" + , locLine = 7 + , locColumn = 1 + } + ) , BlockLemma ( Location { locFile = "test/examples/proofassume.tex" @@ -293,4 +299,10 @@ ) ) ) + ( Location + { locFile = "test/examples/proofassume.tex" + , locLine = 16 + , locColumn = 1 + } + ) ]
\ No newline at end of file diff --git a/test/golden/proofdefinefunction/encoding tasks.golden b/test/golden/proofdefinefunction/encoding tasks.golden index 1f1de12..5f0d64c 100644 --- a/test/golden/proofdefinefunction/encoding tasks.golden +++ b/test/golden/proofdefinefunction/encoding tasks.golden @@ -1,4 +1,4 @@ -fof(definefunctiontest,conjecture,elem(fx,fy)=>elem(fx,fy),"test/examples/proofdefinefunction.tex 26:5"). +fof(definefunctiontest,conjecture,elem(fx,fy)=>elem(fx,fy),"test/examples/proofdefinefunction.tex 27:1"). fof(relation,axiom,![Xf]:(relation(Xf)<=>Xf=Xf)). fof(rightunique,axiom,![Xf]:(rightunique(Xf)<=>Xf=Xf)). fof(dom,axiom,![Xf]:dom(Xf)=Xf). diff --git a/test/golden/proofdefinefunction/generating tasks.golden b/test/golden/proofdefinefunction/generating tasks.golden index 32276cc..2c2f89d 100644 --- a/test/golden/proofdefinefunction/generating tasks.golden +++ b/test/golden/proofdefinefunction/generating tasks.golden @@ -395,8 +395,8 @@ , taskConjectureLabel = Marker "definefunctiontest" , taskLocation = Location { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 26 - , locColumn = 5 + , locLine = 27 + , locColumn = 1 } , taskConjecture = Connected Implication ( TermSymbol diff --git a/test/golden/proofdefinefunction/glossing.golden b/test/golden/proofdefinefunction/glossing.golden index 4886067..a7dfb0c 100644 --- a/test/golden/proofdefinefunction/glossing.golden +++ b/test/golden/proofdefinefunction/glossing.golden @@ -174,6 +174,12 @@ , locColumn = 1 } ) + ( Location + { locFile = "test/examples/proofdefinefunction.tex" + , locLine = 27 + , locColumn = 1 + } + ) ( DefineFunction ( Location { locFile = "test/examples/proofdefinefunction.tex" @@ -190,7 +196,7 @@ ( NamedVar "x" ) ) ( Qed - { mpos = Nothing + { mloc = Nothing , by = JustificationEmpty } ) diff --git a/test/golden/proofdefinefunction/parsing.golden b/test/golden/proofdefinefunction/parsing.golden index de3f9a8..00b85d9 100644 --- a/test/golden/proofdefinefunction/parsing.golden +++ b/test/golden/proofdefinefunction/parsing.golden @@ -220,4 +220,10 @@ ( NamedVar "x" ) ) ( Qed Nothing JustificationEmpty ) ) + ( Location + { locFile = "test/examples/proofdefinefunction.tex" + , locLine = 27 + , locColumn = 1 + } + ) ]
\ No newline at end of file diff --git a/test/golden/prooffix/encoding tasks.golden b/test/golden/prooffix/encoding tasks.golden index 0e35e38..744b121 100644 --- a/test/golden/prooffix/encoding tasks.golden +++ b/test/golden/prooffix/encoding tasks.golden @@ -1,4 +1,4 @@ fof(assumetest,conjecture,fx=fx,"test/examples/prooffix.tex 6:5"). ------------------ -fof(assumetest,conjecture,fx=fx,"test/examples/prooffix.tex 6:5"). +fof(assumetest,conjecture,fx=fx,"test/examples/prooffix.tex 7:1"). fof(assumetest1,axiom,fx=fx).
\ No newline at end of file diff --git a/test/golden/prooffix/generating tasks.golden b/test/golden/prooffix/generating tasks.golden index f3a50df..6e1b51f 100644 --- a/test/golden/prooffix/generating tasks.golden +++ b/test/golden/prooffix/generating tasks.golden @@ -52,8 +52,8 @@ , taskConjectureLabel = Marker "assumetest" , taskLocation = Location { locFile = "test/examples/prooffix.tex" - , locLine = 6 - , locColumn = 5 + , locLine = 7 + , locColumn = 1 } , taskConjecture = TermSymbol ( Location diff --git a/test/golden/prooffix/glossing.golden b/test/golden/prooffix/glossing.golden index 104de4f..c63497c 100644 --- a/test/golden/prooffix/glossing.golden +++ b/test/golden/prooffix/glossing.golden @@ -41,6 +41,12 @@ , locColumn = 1 } ) + ( Location + { locFile = "test/examples/prooffix.tex" + , locLine = 7 + , locColumn = 1 + } + ) ( Fix ( Location { locFile = "test/examples/prooffix.tex" @@ -75,7 +81,7 @@ ] ) JustificationEmpty ( Qed - { mpos = Nothing + { mloc = Nothing , by = JustificationEmpty } ) diff --git a/test/golden/prooffix/parsing.golden b/test/golden/prooffix/parsing.golden index 2d0daca..d760e85 100644 --- a/test/golden/prooffix/parsing.golden +++ b/test/golden/prooffix/parsing.golden @@ -83,4 +83,10 @@ ) JustificationEmpty ( Qed Nothing JustificationEmpty ) ) ) + ( Location + { locFile = "test/examples/prooffix.tex" + , locLine = 7 + , locColumn = 1 + } + ) ]
\ No newline at end of file diff --git a/test/golden/russell/encoding tasks.golden b/test/golden/russell/encoding tasks.golden index f1a3d5c..1fb595c 100644 --- a/test/golden/russell/encoding tasks.golden +++ b/test/golden/russell/encoding tasks.golden @@ -15,7 +15,7 @@ fof(no_universal_set2,axiom,![Xx]:(elem(Xx,fR)<=>(elem(Xx,fV)&~elem(Xx,Xx)))). fof(no_universal_set3,axiom,universal_set(fV)). fof(no_universal_set4,axiom,~~?[X0]:universal_set(X0)). ------------------ -fof(no_universal_set,conjecture,$false,"test/examples/russell.tex 15:5"). +fof(no_universal_set,conjecture,$false,"test/examples/russell.tex 16:1"). fof(universal_set,axiom,![XV]:(universal_set(XV)<=>![Xx]:elem(Xx,XV))). fof(no_universal_set1,axiom,$false). fof(no_universal_set2,axiom,elem(fR,fR)<=>~elem(fR,fR)). diff --git a/test/golden/russell/generating tasks.golden b/test/golden/russell/generating tasks.golden index 7c3b0a7..2eb9eed 100644 --- a/test/golden/russell/generating tasks.golden +++ b/test/golden/russell/generating tasks.golden @@ -1099,8 +1099,8 @@ , taskConjectureLabel = Marker "no_universal_set" , taskLocation = Location { locFile = "test/examples/russell.tex" - , locLine = 15 - , locColumn = 5 + , locLine = 16 + , locColumn = 1 } , taskConjecture = PropositionalConstant IsBottom } diff --git a/test/golden/russell/glossing.golden b/test/golden/russell/glossing.golden index f07b604..9b238a3 100644 --- a/test/golden/russell/glossing.golden +++ b/test/golden/russell/glossing.golden @@ -95,6 +95,12 @@ , locColumn = 1 } ) + ( Location + { locFile = "test/examples/russell.tex" + , locLine = 16 + , locColumn = 1 + } + ) ( ByContradiction ( Location { locFile = "test/examples/russell.tex" @@ -233,7 +239,7 @@ } ) ( PropositionalConstant IsBottom ) JustificationEmpty ( Qed - { mpos = Nothing + { mloc = Nothing , by = JustificationEmpty } ) diff --git a/test/golden/russell/parsing.golden b/test/golden/russell/parsing.golden index 73b1081..846e21c 100644 --- a/test/golden/russell/parsing.golden +++ b/test/golden/russell/parsing.golden @@ -288,4 +288,10 @@ ) ) ) + ( Location + { locFile = "test/examples/russell.tex" + , locLine = 16 + , locColumn = 1 + } + ) ]
\ No newline at end of file diff --git a/test/golden/union/encoding tasks.golden b/test/golden/union/encoding tasks.golden index 50b4f3c..34b4eff 100644 --- a/test/golden/union/encoding tasks.golden +++ b/test/golden/union/encoding tasks.golden @@ -13,7 +13,7 @@ fof(union_defn,axiom,![Xa,XA,XB]:(elem(Xa,union(XA,XB))<=>(elem(Xa,XA)|elem(Xa,X fof(ext,axiom,![XA,XB]:(![Xa]:(elem(Xa,XA)<=>elem(Xa,XB))=>XA=XB)). fof(union_assoc1,axiom,![Xa]:(elem(Xa,union(union(fA,fB),fC))=>elem(Xa,union(fA,union(fB,fC))))). ------------------ -fof(union_assoc,conjecture,union(union(fA,fB),fC)=union(fA,union(fB,fC)),"test/examples/union.tex 20:5"). +fof(union_assoc,conjecture,union(union(fA,fB),fC)=union(fA,union(fB,fC)),"test/examples/union.tex 21:1"). fof(union_comm,axiom,![XA,XB]:union(XA,XB)=union(XB,XA)). fof(union_defn,axiom,![Xa,XA,XB]:(elem(Xa,union(XA,XB))<=>(elem(Xa,XA)|elem(Xa,XB)))). fof(ext,axiom,![XA,XB]:(![Xa]:(elem(Xa,XA)<=>elem(Xa,XB))=>XA=XB)). diff --git a/test/golden/union/generating tasks.golden b/test/golden/union/generating tasks.golden index 2b80f20..1e658d8 100644 --- a/test/golden/union/generating tasks.golden +++ b/test/golden/union/generating tasks.golden @@ -1713,8 +1713,8 @@ , taskConjectureLabel = Marker "union_assoc" , taskLocation = Location { locFile = "test/examples/union.tex" - , locLine = 20 - , locColumn = 5 + , locLine = 21 + , locColumn = 1 } , taskConjecture = TermSymbol ( Location diff --git a/test/golden/union/glossing.golden b/test/golden/union/glossing.golden index 8c1b35b..276b3cc 100644 --- a/test/golden/union/glossing.golden +++ b/test/golden/union/glossing.golden @@ -335,6 +335,12 @@ , locColumn = 1 } ) + ( Location + { locFile = "test/examples/union.tex" + , locLine = 21 + , locColumn = 1 + } + ) ( Have ( Location { locFile = "test/examples/union.tex" @@ -626,7 +632,7 @@ ) ) JustificationEmpty ( Qed - { mpos = Nothing + { mloc = Nothing , by = JustificationEmpty } ) diff --git a/test/golden/union/parsing.golden b/test/golden/union/parsing.golden index 5edbb02..8c7ce99 100644 --- a/test/golden/union/parsing.golden +++ b/test/golden/union/parsing.golden @@ -516,4 +516,10 @@ ) JustificationEmpty ( Qed Nothing JustificationEmpty ) ) ) + ( Location + { locFile = "test/examples/union.tex" + , locLine = 21 + , locColumn = 1 + } + ) ]
\ No newline at end of file |