diff options
71 files changed, 660 insertions, 660 deletions
diff --git a/source/Report/Location.hs b/source/Report/Location.hs index a159fa3..59e6e83 100644 --- a/source/Report/Location.hs +++ b/source/Report/Location.hs @@ -3,7 +3,7 @@ module Report.Location where import Base -import Text.Megaparsec.Pos (SourcePos, sourceName, sourceLine, unPos) +import Text.Megaparsec.Pos (SourcePos (sourceColumn), sourceName, sourceLine, unPos) import Data.Text qualified as Text data Location = Location @@ -17,7 +17,7 @@ fromSourcePos :: SourcePos -> Location fromSourcePos pos = Location { locFile = sourceName pos , locLine = unPos (sourceLine pos) - , locColumn = unPos (sourceLine pos) + , locColumn = unPos (sourceColumn pos) } prettyLocation :: Location -> String diff --git a/test/golden/abbr/encoding tasks.golden b/test/golden/abbr/encoding tasks.golden index 285f433..cfb8848 100644 --- a/test/golden/abbr/encoding tasks.golden +++ b/test/golden/abbr/encoding tasks.golden @@ -1,24 +1,24 @@ -fof(dummy_abbr_test_adj,conjecture,~?[Xy]:elem(Xy,fx)=>~?[Xy]:elem(Xy,fx),"test/examples/abbr.tex 5:5"). +fof(dummy_abbr_test_adj,conjecture,~?[Xy]:elem(Xy,fx)=>~?[Xy]:elem(Xy,fx),"test/examples/abbr.tex 5:1"). ------------------ -fof(dummy_abbr_test_noun,conjecture,![Xx]:Xx=Xx,"test/examples/abbr.tex 15:15"). +fof(dummy_abbr_test_noun,conjecture,![Xx]:Xx=Xx,"test/examples/abbr.tex 15:1"). fof(dummy_abbr_test_adj,axiom,![Xx]:(~?[Xy]:elem(Xy,Xx)=>~?[Xy]:elem(Xy,Xx))). ------------------ -fof(dummy_abbr_test_verb,conjecture,fx=fy=>fx=fy,"test/examples/abbr.tex 25:25"). +fof(dummy_abbr_test_verb,conjecture,fx=fy=>fx=fy,"test/examples/abbr.tex 25:1"). fof(dummy_abbr_test_noun,axiom,![Xx]:Xx=Xx). fof(dummy_abbr_test_adj,axiom,![Xx]:(~?[Xy]:elem(Xy,Xx)=>~?[Xy]:elem(Xy,Xx))). ------------------ -fof(abbr_test_notin,conjecture,~elem(fx,fy)=>~elem(fx,fy),"test/examples/abbr.tex 31:31"). +fof(abbr_test_notin,conjecture,~elem(fx,fy)=>~elem(fx,fy),"test/examples/abbr.tex 31:1"). fof(dummy_abbr_test_verb,axiom,![Xx,Xy]:(Xx=Xy=>Xx=Xy)). fof(dummy_abbr_test_noun,axiom,![Xx]:Xx=Xx). fof(dummy_abbr_test_adj,axiom,![Xx]:(~?[Xy]:elem(Xy,Xx)=>~?[Xy]:elem(Xy,Xx))). ------------------ -fof(abbr_test_elementof_is_in,conjecture,elem(fx,fy)=>elem(fx,fy),"test/examples/abbr.tex 37:37"). +fof(abbr_test_elementof_is_in,conjecture,elem(fx,fy)=>elem(fx,fy),"test/examples/abbr.tex 37:1"). fof(abbr_test_notin,axiom,![Xx,Xy]:(~elem(Xx,Xy)=>~elem(Xx,Xy))). fof(dummy_abbr_test_verb,axiom,![Xx,Xy]:(Xx=Xy=>Xx=Xy)). fof(dummy_abbr_test_noun,axiom,![Xx]:Xx=Xx). fof(dummy_abbr_test_adj,axiom,![Xx]:(~?[Xy]:elem(Xy,Xx)=>~?[Xy]:elem(Xy,Xx))). ------------------ -fof(abbr_test_equals_is_eq,conjecture,fx=fy=>fx=fy,"test/examples/abbr.tex 43:43"). +fof(abbr_test_equals_is_eq,conjecture,fx=fy=>fx=fy,"test/examples/abbr.tex 43:1"). fof(abbr_test_elementof_is_in,axiom,![Xx,Xy]:(elem(Xx,Xy)=>elem(Xx,Xy))). fof(abbr_test_notin,axiom,![Xx,Xy]:(~elem(Xx,Xy)=>~elem(Xx,Xy))). fof(dummy_abbr_test_verb,axiom,![Xx,Xy]:(Xx=Xy=>Xx=Xy)). diff --git a/test/golden/abbr/generating tasks.golden b/test/golden/abbr/generating tasks.golden index 8993ce4..6148e48 100644 --- a/test/golden/abbr/generating tasks.golden +++ b/test/golden/abbr/generating tasks.golden @@ -5,14 +5,14 @@ , taskLocation = Location { locFile = "test/examples/abbr.tex" , locLine = 5 - , locColumn = 5 + , locColumn = 1 } , taskConjecture = Connected Implication ( Not ( Location { locFile = "test/examples/abbr.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 35 } ) ( Quantified Existentially @@ -48,7 +48,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 35 } ) ( Quantified Existentially @@ -93,7 +93,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 35 } ) ( Quantified Existentially @@ -131,7 +131,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 35 } ) ( Quantified Existentially @@ -173,7 +173,7 @@ , taskLocation = Location { locFile = "test/examples/abbr.tex" , locLine = 15 - , locColumn = 15 + , locColumn = 1 } , taskConjecture = Quantified Universally ( Scope @@ -241,7 +241,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 35 } ) ( Quantified Existentially @@ -279,7 +279,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 35 } ) ( Quantified Existentially @@ -321,7 +321,7 @@ , taskLocation = Location { locFile = "test/examples/abbr.tex" , locLine = 25 - , locColumn = 25 + , locColumn = 1 } , taskConjecture = Connected Implication ( TermSymbol @@ -453,7 +453,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 35 } ) ( Quantified Existentially @@ -491,7 +491,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 35 } ) ( Quantified Existentially @@ -533,7 +533,7 @@ , taskLocation = Location { locFile = "test/examples/abbr.tex" , locLine = 31 - , locColumn = 31 + , locColumn = 1 } , taskConjecture = Connected Implication ( Not @@ -749,7 +749,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 35 } ) ( Quantified Existentially @@ -787,7 +787,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 35 } ) ( Quantified Existentially @@ -829,7 +829,7 @@ , taskLocation = Location { locFile = "test/examples/abbr.tex" , locLine = 37 - , locColumn = 37 + , locColumn = 1 } , taskConjecture = Connected Implication ( TermSymbol @@ -1081,7 +1081,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 35 } ) ( Quantified Existentially @@ -1119,7 +1119,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 35 } ) ( Quantified Existentially @@ -1161,7 +1161,7 @@ , taskLocation = Location { locFile = "test/examples/abbr.tex" , locLine = 43 - , locColumn = 43 + , locColumn = 1 } , taskConjecture = Connected Implication ( TermSymbol diff --git a/test/golden/abbr/glossing.golden b/test/golden/abbr/glossing.golden index 3122f56..cab9799 100644 --- a/test/golden/abbr/glossing.golden +++ b/test/golden/abbr/glossing.golden @@ -19,7 +19,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 35 } ) ( Quantified Existentially @@ -57,7 +57,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 5 - , locColumn = 5 + , locColumn = 1 } ) ( Marker "dummy_abbr_test_adj" ) @@ -67,7 +67,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 6 - , locColumn = 6 + , locColumn = 14 } ) ( SymbolPredicate @@ -85,7 +85,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 6 - , locColumn = 6 + , locColumn = 33 } ) ( SymbolPredicate @@ -105,7 +105,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 11 - , locColumn = 11 + , locColumn = 1 } ) ( Marker "function" ) @@ -150,7 +150,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 15 - , locColumn = 15 + , locColumn = 1 } ) ( Marker "dummy_abbr_test_noun" ) @@ -192,7 +192,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 21 - , locColumn = 21 + , locColumn = 1 } ) ( Marker "converges" ) @@ -243,7 +243,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 25 - , locColumn = 25 + , locColumn = 1 } ) ( Marker "dummy_abbr_test_verb" ) @@ -253,7 +253,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 26 - , locColumn = 26 + , locColumn = 12 } ) ( SymbolPredicate @@ -307,7 +307,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 31 - , locColumn = 31 + , locColumn = 1 } ) ( Marker "abbr_test_notin" ) @@ -363,7 +363,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 37 - , locColumn = 37 + , locColumn = 1 } ) ( Marker "abbr_test_elementof_is_in" ) @@ -427,7 +427,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 43 - , locColumn = 43 + , locColumn = 1 } ) ( Marker "abbr_test_equals_is_eq" ) @@ -437,7 +437,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 44 - , locColumn = 44 + , locColumn = 12 } ) ( SymbolPredicate diff --git a/test/golden/abbr/parsing.golden b/test/golden/abbr/parsing.golden index 61a4b6b..d793ca8 100644 --- a/test/golden/abbr/parsing.golden +++ b/test/golden/abbr/parsing.golden @@ -12,7 +12,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 12 } ) [ Just @@ -23,13 +23,13 @@ { pos = Location { locFile = "test/examples/abbr.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 35 } , stmt = SymbolicQuantified { pos = Location { locFile = "test/examples/abbr.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 35 } , quant = Existentially , xs = NamedVar "y" :| [] @@ -39,7 +39,7 @@ { pos = Location { locFile = "test/examples/abbr.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 52 } , formula = FormulaChain ( ChainBase @@ -62,7 +62,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 5 - , locColumn = 5 + , locColumn = 1 } ) ( Marker "dummy_abbr_test_adj" ) @@ -73,7 +73,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 6 - , locColumn = 6 + , locColumn = 4 } ) , stmt1 = StmtVerbPhrase @@ -81,7 +81,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 6 - , locColumn = 6 + , locColumn = 7 } ) ( ExprVar @@ -92,7 +92,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 6 - , locColumn = 6 + , locColumn = 14 } ) [ Just @@ -105,7 +105,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 6 - , locColumn = 6 + , locColumn = 26 } ) ( ExprVar @@ -116,7 +116,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 6 - , locColumn = 6 + , locColumn = 33 } ) [ Just @@ -131,7 +131,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 11 - , locColumn = 11 + , locColumn = 1 } ) ( Marker "function" ) @@ -154,7 +154,7 @@ { pos = Location { locFile = "test/examples/abbr.tex" , locLine = 12 - , locColumn = 12 + , locColumn = 27 } , formula = FormulaChain ( ChainBase @@ -175,7 +175,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 15 - , locColumn = 15 + , locColumn = 1 } ) ( Marker "dummy_abbr_test_noun" ) @@ -184,7 +184,7 @@ { pos = Location { locFile = "test/examples/abbr.tex" , locLine = 16 - , locColumn = 16 + , locColumn = 5 } , quant = Universally , xs = NamedVar "x" :| [] @@ -194,13 +194,13 @@ { pos = Location { locFile = "test/examples/abbr.tex" , locLine = 16 - , locColumn = 16 + , locColumn = 25 } , args = TermExpr ( Location { locFile = "test/examples/abbr.tex" , locLine = 16 - , locColumn = 16 + , locColumn = 25 } ) ( ExprVar @@ -228,7 +228,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 21 - , locColumn = 21 + , locColumn = 1 } ) ( Marker "converges" ) @@ -238,7 +238,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 22 - , locColumn = 22 + , locColumn = 9 } ) ( SgPl @@ -264,7 +264,7 @@ { pos = Location { locFile = "test/examples/abbr.tex" , locLine = 22 - , locColumn = 22 + , locColumn = 30 } , formula = FormulaChain ( ChainBase @@ -285,7 +285,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 25 - , locColumn = 25 + , locColumn = 1 } ) ( Marker "dummy_abbr_test_verb" ) @@ -296,7 +296,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 26 - , locColumn = 26 + , locColumn = 5 } ) , stmt1 = StmtVerbPhrase @@ -304,7 +304,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 26 - , locColumn = 26 + , locColumn = 8 } ) ( ExprVar @@ -315,7 +315,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 26 - , locColumn = 26 + , locColumn = 12 } ) ( SgPl @@ -339,7 +339,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 26 - , locColumn = 26 + , locColumn = 25 } ) ( ExprVar @@ -352,7 +352,7 @@ { pos = Location { locFile = "test/examples/abbr.tex" , locLine = 26 - , locColumn = 26 + , locColumn = 35 } , formula = FormulaChain ( ChainBase @@ -374,7 +374,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 31 - , locColumn = 31 + , locColumn = 1 } ) ( Marker "abbr_test_notin" ) @@ -385,14 +385,14 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 32 - , locColumn = 32 + , locColumn = 4 } ) , stmt1 = StmtFormula { pos = Location { locFile = "test/examples/abbr.tex" , locLine = 32 - , locColumn = 32 + , locColumn = 7 } , formula = FormulaChain ( ChainBase @@ -411,7 +411,7 @@ { pos = Location { locFile = "test/examples/abbr.tex" , locLine = 32 - , locColumn = 32 + , locColumn = 25 } , formula = FormulaChain ( ChainBase @@ -433,7 +433,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 37 - , locColumn = 37 + , locColumn = 1 } ) ( Marker "abbr_test_elementof_is_in" ) @@ -444,20 +444,20 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 38 - , locColumn = 38 + , locColumn = 5 } ) , stmt1 = StmtNoun { pos = Location { locFile = "test/examples/abbr.tex" , locLine = 38 - , locColumn = 38 + , locColumn = 8 } , args = TermExpr ( Location { locFile = "test/examples/abbr.tex" , locLine = 38 - , locColumn = 38 + , locColumn = 8 } ) ( ExprVar @@ -486,7 +486,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 38 - , locColumn = 38 + , locColumn = 29 } ) ( ExprVar @@ -499,7 +499,7 @@ { pos = Location { locFile = "test/examples/abbr.tex" , locLine = 38 - , locColumn = 38 + , locColumn = 39 } , formula = FormulaChain ( ChainBase @@ -521,7 +521,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 43 - , locColumn = 43 + , locColumn = 1 } ) ( Marker "abbr_test_equals_is_eq" ) @@ -532,7 +532,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 44 - , locColumn = 44 + , locColumn = 5 } ) , stmt1 = StmtVerbPhrase @@ -540,7 +540,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 44 - , locColumn = 44 + , locColumn = 8 } ) ( ExprVar @@ -551,7 +551,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 44 - , locColumn = 44 + , locColumn = 12 } ) ( SgPl @@ -571,7 +571,7 @@ ( Location { locFile = "test/examples/abbr.tex" , locLine = 44 - , locColumn = 44 + , locColumn = 19 } ) ( ExprVar @@ -584,7 +584,7 @@ { pos = Location { locFile = "test/examples/abbr.tex" , locLine = 44 - , locColumn = 44 + , locColumn = 29 } , formula = FormulaChain ( ChainBase diff --git a/test/golden/byRef/encoding tasks.golden b/test/golden/byRef/encoding tasks.golden index a021d00..3038289 100644 --- a/test/golden/byRef/encoding tasks.golden +++ b/test/golden/byRef/encoding tasks.golden @@ -1,21 +1,21 @@ fof(prop1,conjecture,fa=fa,"test/examples/byRef.tex 1:1"). ------------------ -fof(prop2,conjecture,fb=fb,"test/examples/byRef.tex 5:5"). +fof(prop2,conjecture,fb=fb,"test/examples/byRef.tex 5:1"). fof(prop1,axiom,![Xa]:Xa=Xa). ------------------ -fof(prop3,conjecture,fc=fc,"test/examples/byRef.tex 13:13"). +fof(prop3,conjecture,fc=fc,"test/examples/byRef.tex 13:5"). fof(prop1,axiom,![Xa]:Xa=Xa). ------------------ -fof(prop4,conjecture,![Xd]:Xd=Xd,"test/examples/byRef.tex 20:20"). +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:20"). +fof(prop4,conjecture,fe=fe,"test/examples/byRef.tex 20:5"). fof(prop3,axiom,![Xc]:Xc=Xc). fof(prop2,axiom,![Xb]:Xb=Xb). fof(prop1,axiom,![Xa]:Xa=Xa). fof(prop41,axiom,![Xd]:Xd=Xd). ------------------ -fof(prop5,conjecture,ff=ff,"test/examples/byRef.tex 23:23"). +fof(prop5,conjecture,ff=ff,"test/examples/byRef.tex 23:1"). fof(prop4,axiom,![Xe]:Xe=Xe). fof(prop3,axiom,![Xc]:Xc=Xc). fof(prop2,axiom,![Xb]:Xb=Xb). diff --git a/test/golden/byRef/generating tasks.golden b/test/golden/byRef/generating tasks.golden index 70404a5..e707cec 100644 --- a/test/golden/byRef/generating tasks.golden +++ b/test/golden/byRef/generating tasks.golden @@ -61,7 +61,7 @@ , taskLocation = Location { locFile = "test/examples/byRef.tex" , locLine = 5 - , locColumn = 5 + , locColumn = 1 } , taskConjecture = TermSymbol ( Location @@ -117,7 +117,7 @@ , taskLocation = Location { locFile = "test/examples/byRef.tex" , locLine = 13 - , locColumn = 13 + , locColumn = 5 } , taskConjecture = TermSymbol ( Location @@ -173,7 +173,7 @@ , taskLocation = Location { locFile = "test/examples/byRef.tex" , locLine = 20 - , locColumn = 20 + , locColumn = 5 } , taskConjecture = Quantified Universally ( Scope @@ -321,7 +321,7 @@ , taskLocation = Location { locFile = "test/examples/byRef.tex" , locLine = 20 - , locColumn = 20 + , locColumn = 5 } , taskConjecture = TermSymbol ( Location @@ -461,7 +461,7 @@ , taskLocation = Location { locFile = "test/examples/byRef.tex" , locLine = 23 - , locColumn = 23 + , locColumn = 1 } , taskConjecture = TermSymbol ( Location diff --git a/test/golden/byRef/glossing.golden b/test/golden/byRef/glossing.golden index 62334c8..38204d8 100644 --- a/test/golden/byRef/glossing.golden +++ b/test/golden/byRef/glossing.golden @@ -30,7 +30,7 @@ ( Location { locFile = "test/examples/byRef.tex" , locLine = 5 - , locColumn = 5 + , locColumn = 1 } ) ( Marker "prop2" ) @@ -58,7 +58,7 @@ ( Location { locFile = "test/examples/byRef.tex" , locLine = 9 - , locColumn = 9 + , locColumn = 1 } ) ( Marker "prop3" ) @@ -86,7 +86,7 @@ ( Location { locFile = "test/examples/byRef.tex" , locLine = 12 - , locColumn = 12 + , locColumn = 1 } ) ( Qed @@ -94,7 +94,7 @@ ( Location { locFile = "test/examples/byRef.tex" , locLine = 13 - , locColumn = 13 + , locColumn = 5 } ) , by = JustificationRef @@ -105,7 +105,7 @@ ( Location { locFile = "test/examples/byRef.tex" , locLine = 16 - , locColumn = 16 + , locColumn = 1 } ) ( Marker "prop4" ) @@ -133,14 +133,14 @@ ( Location { locFile = "test/examples/byRef.tex" , locLine = 19 - , locColumn = 19 + , locColumn = 1 } ) ( Have ( Location { locFile = "test/examples/byRef.tex" , locLine = 20 - , locColumn = 20 + , locColumn = 5 } ) ( Quantified Universally @@ -182,7 +182,7 @@ ( Location { locFile = "test/examples/byRef.tex" , locLine = 23 - , locColumn = 23 + , locColumn = 1 } ) ( Marker "prop5" ) diff --git a/test/golden/byRef/parsing.golden b/test/golden/byRef/parsing.golden index 06cd8fa..de15f45 100644 --- a/test/golden/byRef/parsing.golden +++ b/test/golden/byRef/parsing.golden @@ -11,7 +11,7 @@ { pos = Location { locFile = "test/examples/byRef.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 5 } , formula = FormulaChain ( ChainBase @@ -32,7 +32,7 @@ ( Location { locFile = "test/examples/byRef.tex" , locLine = 5 - , locColumn = 5 + , locColumn = 1 } ) ( Marker "prop2" ) @@ -41,7 +41,7 @@ { pos = Location { locFile = "test/examples/byRef.tex" , locLine = 6 - , locColumn = 6 + , locColumn = 5 } , formula = FormulaChain ( ChainBase @@ -62,7 +62,7 @@ ( Location { locFile = "test/examples/byRef.tex" , locLine = 9 - , locColumn = 9 + , locColumn = 1 } ) ( Marker "prop3" ) @@ -71,7 +71,7 @@ { pos = Location { locFile = "test/examples/byRef.tex" , locLine = 10 - , locColumn = 10 + , locColumn = 5 } , formula = FormulaChain ( ChainBase @@ -92,7 +92,7 @@ ( Location { locFile = "test/examples/byRef.tex" , locLine = 12 - , locColumn = 12 + , locColumn = 1 } ) ( Qed @@ -100,7 +100,7 @@ ( Location { locFile = "test/examples/byRef.tex" , locLine = 13 - , locColumn = 13 + , locColumn = 5 } ) ) @@ -112,7 +112,7 @@ ( Location { locFile = "test/examples/byRef.tex" , locLine = 16 - , locColumn = 16 + , locColumn = 1 } ) ( Marker "prop4" ) @@ -121,7 +121,7 @@ { pos = Location { locFile = "test/examples/byRef.tex" , locLine = 17 - , locColumn = 17 + , locColumn = 5 } , formula = FormulaChain ( ChainBase @@ -142,21 +142,21 @@ ( Location { locFile = "test/examples/byRef.tex" , locLine = 19 - , locColumn = 19 + , locColumn = 1 } ) ( Have ( Location { locFile = "test/examples/byRef.tex" , locLine = 20 - , locColumn = 20 + , locColumn = 5 } ) Nothing ( SymbolicQuantified { pos = Location { locFile = "test/examples/byRef.tex" , locLine = 20 - , locColumn = 20 + , locColumn = 5 } , quant = Universally , xs = NamedVar "d" :| [] @@ -166,7 +166,7 @@ { pos = Location { locFile = "test/examples/byRef.tex" , locLine = 20 - , locColumn = 20 + , locColumn = 25 } , formula = FormulaChain ( ChainBase @@ -191,7 +191,7 @@ ( Location { locFile = "test/examples/byRef.tex" , locLine = 23 - , locColumn = 23 + , locColumn = 1 } ) ( Marker "prop5" ) @@ -200,7 +200,7 @@ { pos = Location { locFile = "test/examples/byRef.tex" , locLine = 24 - , locColumn = 24 + , locColumn = 5 } , formula = FormulaChain ( ChainBase diff --git a/test/golden/calc/encoding tasks.golden b/test/golden/calc/encoding tasks.golden index ecc4596..ec9a6eb 100644 --- a/test/golden/calc/encoding tasks.golden +++ b/test/golden/calc/encoding tasks.golden @@ -1,29 +1,29 @@ fof(trivial,conjecture,fx=fx,"test/examples/calc.tex 1:1"). ------------------ -fof(irrelevant,conjecture,fz=fz,"test/examples/calc.tex 5:5"). +fof(irrelevant,conjecture,fz=fz,"test/examples/calc.tex 5:1"). fof(trivial,axiom,![Xx]:Xx=Xx). ------------------ -fof(alsotrivial,conjecture,fy=fy,"test/examples/calc.tex 13:13"). +fof(alsotrivial,conjecture,fy=fy,"test/examples/calc.tex 13:5"). fof(irrelevant,axiom,![Xz]:Xz=Xz). fof(trivial,axiom,![Xx]:Xx=Xx). ------------------ -fof(alsotrivial,conjecture,fy=fy,"test/examples/calc.tex 13:13"). +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:13"). +fof(alsotrivial,conjecture,fy=fy,"test/examples/calc.tex 13:5"). fof(irrelevant,axiom,![Xz]:Xz=Xz). fof(trivial,axiom,![Xx]:Xx=Xx). fof(alsotrivial1,axiom,fy=fy). ------------------ -fof(trivial_biconditionals,conjecture,fy=fy,"test/examples/calc.tex 26:26"). +fof(trivial_biconditionals,conjecture,fy=fy,"test/examples/calc.tex 26:5"). fof(alsotrivial,axiom,![Xy]:Xy=Xy). fof(irrelevant,axiom,![Xz]:Xz=Xz). fof(trivial,axiom,![Xx]:Xx=Xx). ------------------ -fof(trivial_biconditionals,conjecture,fy=fy,"test/examples/calc.tex 26:26"). +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:26"). +fof(trivial_biconditionals,conjecture,fy=fy,"test/examples/calc.tex 26:5"). 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 8f7d2d8..abe8f45 100644 --- a/test/golden/calc/generating tasks.golden +++ b/test/golden/calc/generating tasks.golden @@ -61,7 +61,7 @@ , taskLocation = Location { locFile = "test/examples/calc.tex" , locLine = 5 - , locColumn = 5 + , locColumn = 1 } , taskConjecture = TermSymbol ( Location @@ -145,7 +145,7 @@ , taskLocation = Location { locFile = "test/examples/calc.tex" , locLine = 13 - , locColumn = 13 + , locColumn = 5 } , taskConjecture = TermSymbol ( Location @@ -201,7 +201,7 @@ , taskLocation = Location { locFile = "test/examples/calc.tex" , locLine = 13 - , locColumn = 13 + , locColumn = 5 } , taskConjecture = TermSymbol ( Location @@ -305,7 +305,7 @@ , taskLocation = Location { locFile = "test/examples/calc.tex" , locLine = 13 - , locColumn = 13 + , locColumn = 5 } , taskConjecture = TermSymbol ( Location @@ -417,7 +417,7 @@ , taskLocation = Location { locFile = "test/examples/calc.tex" , locLine = 26 - , locColumn = 26 + , locColumn = 5 } , taskConjecture = TermSymbol ( Location @@ -473,7 +473,7 @@ , taskLocation = Location { locFile = "test/examples/calc.tex" , locLine = 26 - , locColumn = 26 + , locColumn = 5 } , taskConjecture = TermSymbol ( Location @@ -625,7 +625,7 @@ , taskLocation = Location { locFile = "test/examples/calc.tex" , locLine = 26 - , locColumn = 26 + , locColumn = 5 } , taskConjecture = TermSymbol ( Location diff --git a/test/golden/calc/glossing.golden b/test/golden/calc/glossing.golden index 245cfc5..185b815 100644 --- a/test/golden/calc/glossing.golden +++ b/test/golden/calc/glossing.golden @@ -30,7 +30,7 @@ ( Location { locFile = "test/examples/calc.tex" , locLine = 5 - , locColumn = 5 + , locColumn = 1 } ) ( Marker "irrelevant" ) @@ -58,7 +58,7 @@ ( Location { locFile = "test/examples/calc.tex" , locLine = 9 - , locColumn = 9 + , locColumn = 1 } ) ( Marker "alsotrivial" ) @@ -86,14 +86,14 @@ ( Location { locFile = "test/examples/calc.tex" , locLine = 12 - , locColumn = 12 + , locColumn = 1 } ) ( Calc ( Location { locFile = "test/examples/calc.tex" , locLine = 13 - , locColumn = 13 + , locColumn = 5 } ) CalcUnquantified ( Equation @@ -124,7 +124,7 @@ ( Location { locFile = "test/examples/calc.tex" , locLine = 22 - , locColumn = 22 + , locColumn = 1 } ) ( Marker "trivial_biconditionals" ) @@ -152,14 +152,14 @@ ( Location { locFile = "test/examples/calc.tex" , locLine = 25 - , locColumn = 25 + , locColumn = 1 } ) ( Calc ( Location { locFile = "test/examples/calc.tex" , locLine = 26 - , locColumn = 26 + , locColumn = 5 } ) CalcUnquantified ( Biconditionals diff --git a/test/golden/calc/parsing.golden b/test/golden/calc/parsing.golden index 5094abc..749f903 100644 --- a/test/golden/calc/parsing.golden +++ b/test/golden/calc/parsing.golden @@ -11,7 +11,7 @@ { pos = Location { locFile = "test/examples/calc.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 5 } , formula = FormulaChain ( ChainBase @@ -32,7 +32,7 @@ ( Location { locFile = "test/examples/calc.tex" , locLine = 5 - , locColumn = 5 + , locColumn = 1 } ) ( Marker "irrelevant" ) @@ -41,7 +41,7 @@ { pos = Location { locFile = "test/examples/calc.tex" , locLine = 6 - , locColumn = 6 + , locColumn = 5 } , formula = FormulaChain ( ChainBase @@ -62,7 +62,7 @@ ( Location { locFile = "test/examples/calc.tex" , locLine = 9 - , locColumn = 9 + , locColumn = 1 } ) ( Marker "alsotrivial" ) @@ -71,7 +71,7 @@ { pos = Location { locFile = "test/examples/calc.tex" , locLine = 10 - , locColumn = 10 + , locColumn = 5 } , formula = FormulaChain ( ChainBase @@ -92,14 +92,14 @@ ( Location { locFile = "test/examples/calc.tex" , locLine = 12 - , locColumn = 12 + , locColumn = 1 } ) ( Calc ( Location { locFile = "test/examples/calc.tex" , locLine = 13 - , locColumn = 13 + , locColumn = 5 } ) Nothing ( Equation @@ -125,7 +125,7 @@ ( Location { locFile = "test/examples/calc.tex" , locLine = 22 - , locColumn = 22 + , locColumn = 1 } ) ( Marker "trivial_biconditionals" ) @@ -134,7 +134,7 @@ { pos = Location { locFile = "test/examples/calc.tex" , locLine = 23 - , locColumn = 23 + , locColumn = 5 } , formula = FormulaChain ( ChainBase @@ -155,14 +155,14 @@ ( Location { locFile = "test/examples/calc.tex" , locLine = 25 - , locColumn = 25 + , locColumn = 1 } ) ( Calc ( Location { locFile = "test/examples/calc.tex" , locLine = 26 - , locColumn = 26 + , locColumn = 5 } ) Nothing ( Biconditionals diff --git a/test/golden/coord/encoding tasks.golden b/test/golden/coord/encoding tasks.golden index 06268a7..4b38cd9 100644 --- a/test/golden/coord/encoding tasks.golden +++ b/test/golden/coord/encoding tasks.golden @@ -1,11 +1,11 @@ -fof(nouns,conjecture,fx=fx,"test/examples/coord.tex 13:13"). +fof(nouns,conjecture,fx=fx,"test/examples/coord.tex 13:1"). fof(baz,axiom,![Xx]:(baz(Xx)<=>Xx=Xx)). fof(foo,axiom,![Xx]:(foo(Xx)<=>Xx=Xx)). fof(bar,axiom,![Xx]:(bar(Xx)<=>Xx=Xx)). fof(nouns1,axiom,bar(fy)). fof(nouns2,axiom,bar(fx)). ------------------ -fof(adj_nouns,conjecture,fx=fx,"test/examples/coord.tex 18:18"). +fof(adj_nouns,conjecture,fx=fx,"test/examples/coord.tex 18:1"). fof(nouns,axiom,![Xx,Xy]:((bar(Xx)&bar(Xy))=>Xx=Xx)). fof(baz,axiom,![Xx]:(baz(Xx)<=>Xx=Xx)). fof(foo,axiom,![Xx]:(foo(Xx)<=>Xx=Xx)). @@ -13,7 +13,7 @@ fof(bar,axiom,![Xx]:(bar(Xx)<=>Xx=Xx)). fof(adj_nouns1,axiom,bar(fy)&foo(fy)). fof(adj_nouns2,axiom,bar(fx)&foo(fx)). ------------------ -fof(nouns_suchthat,conjecture,fx=fx,"test/examples/coord.tex 24:24"). +fof(nouns_suchthat,conjecture,fx=fx,"test/examples/coord.tex 24:1"). fof(adj_nouns,axiom,![Xx,Xy]:((bar(Xx)&foo(Xx)&bar(Xy)&foo(Xy))=>Xx=Xx)). fof(nouns,axiom,![Xx,Xy]:((bar(Xx)&bar(Xy))=>Xx=Xx)). fof(baz,axiom,![Xx]:(baz(Xx)<=>Xx=Xx)). @@ -23,7 +23,7 @@ fof(nouns_suchthat1,axiom,bar(fy)). fof(nouns_suchthat2,axiom,bar(fx)). fof(nouns_suchthat3,axiom,foo(fx)&baz(fy)). ------------------ -fof(noun_verb,conjecture,fx=fy<=>(bar(fx)&fx=fy),"test/examples/coord.tex 30:30"). +fof(noun_verb,conjecture,fx=fy<=>(bar(fx)&fx=fy),"test/examples/coord.tex 30:1"). fof(nouns_suchthat,axiom,![Xx,Xy]:((foo(Xx)&baz(Xy)&bar(Xx)&bar(Xy))=>Xx=Xx)). fof(adj_nouns,axiom,![Xx,Xy]:((bar(Xx)&foo(Xx)&bar(Xy)&foo(Xy))=>Xx=Xx)). fof(nouns,axiom,![Xx,Xy]:((bar(Xx)&bar(Xy))=>Xx=Xx)). @@ -31,7 +31,7 @@ fof(baz,axiom,![Xx]:(baz(Xx)<=>Xx=Xx)). fof(foo,axiom,![Xx]:(foo(Xx)<=>Xx=Xx)). fof(bar,axiom,![Xx]:(bar(Xx)<=>Xx=Xx)). ------------------ -fof(adjs,conjecture,foo(fx)&baz(fx),"test/examples/coord.tex 35:35"). +fof(adjs,conjecture,foo(fx)&baz(fx),"test/examples/coord.tex 35:1"). fof(noun_verb,axiom,![Xx,Xy]:(Xx=Xy<=>(bar(Xx)&Xx=Xy))). fof(nouns_suchthat,axiom,![Xx,Xy]:((foo(Xx)&baz(Xy)&bar(Xx)&bar(Xy))=>Xx=Xx)). fof(adj_nouns,axiom,![Xx,Xy]:((bar(Xx)&foo(Xx)&bar(Xy)&foo(Xy))=>Xx=Xx)). @@ -40,7 +40,7 @@ fof(baz,axiom,![Xx]:(baz(Xx)<=>Xx=Xx)). fof(foo,axiom,![Xx]:(foo(Xx)<=>Xx=Xx)). fof(bar,axiom,![Xx]:(bar(Xx)<=>Xx=Xx)). ------------------ -fof(are_nouns,conjecture,bar(fx)&foo(fx)&bar(fy)&foo(fy),"test/examples/coord.tex 39:39"). +fof(are_nouns,conjecture,bar(fx)&foo(fx)&bar(fy)&foo(fy),"test/examples/coord.tex 39:1"). fof(adjs,axiom,![Xx]:(foo(Xx)&baz(Xx))). fof(noun_verb,axiom,![Xx,Xy]:(Xx=Xy<=>(bar(Xx)&Xx=Xy))). fof(nouns_suchthat,axiom,![Xx,Xy]:((foo(Xx)&baz(Xy)&bar(Xx)&bar(Xy))=>Xx=Xx)). diff --git a/test/golden/coord/generating tasks.golden b/test/golden/coord/generating tasks.golden index a4b60ff..9a653ca 100644 --- a/test/golden/coord/generating tasks.golden +++ b/test/golden/coord/generating tasks.golden @@ -10,7 +10,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 9 - , locColumn = 9 + , locColumn = 1 } ) ( SymbolPredicate @@ -72,7 +72,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 5 - , locColumn = 5 + , locColumn = 1 } ) ( SymbolPredicate @@ -256,7 +256,7 @@ , taskLocation = Location { locFile = "test/examples/coord.tex" , locLine = 13 - , locColumn = 13 + , locColumn = 1 } , taskConjecture = TermSymbol ( Location @@ -376,7 +376,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 9 - , locColumn = 9 + , locColumn = 1 } ) ( SymbolPredicate @@ -438,7 +438,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 5 - , locColumn = 5 + , locColumn = 1 } ) ( SymbolPredicate @@ -662,7 +662,7 @@ , taskLocation = Location { locFile = "test/examples/coord.tex" , locLine = 18 - , locColumn = 18 + , locColumn = 1 } , taskConjecture = TermSymbol ( Location @@ -914,7 +914,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 9 - , locColumn = 9 + , locColumn = 1 } ) ( SymbolPredicate @@ -976,7 +976,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 5 - , locColumn = 5 + , locColumn = 1 } ) ( SymbolPredicate @@ -1162,7 +1162,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 25 - , locColumn = 25 + , locColumn = 41 } ) ( SymbolPredicate @@ -1180,7 +1180,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 25 - , locColumn = 25 + , locColumn = 56 } ) ( SymbolPredicate @@ -1200,7 +1200,7 @@ , taskLocation = Location { locFile = "test/examples/coord.tex" , locLine = 24 - , locColumn = 24 + , locColumn = 1 } , taskConjecture = TermSymbol ( Location @@ -1235,7 +1235,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 25 - , locColumn = 25 + , locColumn = 41 } ) ( SymbolPredicate @@ -1255,7 +1255,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 25 - , locColumn = 25 + , locColumn = 56 } ) ( SymbolPredicate @@ -1584,7 +1584,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 9 - , locColumn = 9 + , locColumn = 1 } ) ( SymbolPredicate @@ -1646,7 +1646,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 5 - , locColumn = 5 + , locColumn = 1 } ) ( SymbolPredicate @@ -1774,7 +1774,7 @@ , taskLocation = Location { locFile = "test/examples/coord.tex" , locLine = 30 - , locColumn = 30 + , locColumn = 1 } , taskConjecture = Connected Equivalence ( TermSymbol @@ -1939,7 +1939,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 25 - , locColumn = 25 + , locColumn = 41 } ) ( SymbolPredicate @@ -1959,7 +1959,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 25 - , locColumn = 25 + , locColumn = 56 } ) ( SymbolPredicate @@ -2288,7 +2288,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 9 - , locColumn = 9 + , locColumn = 1 } ) ( SymbolPredicate @@ -2350,7 +2350,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 5 - , locColumn = 5 + , locColumn = 1 } ) ( SymbolPredicate @@ -2478,14 +2478,14 @@ , taskLocation = Location { locFile = "test/examples/coord.tex" , locLine = 35 - , locColumn = 35 + , locColumn = 1 } , taskConjecture = Connected Conjunction ( TermSymbol ( Location { locFile = "test/examples/coord.tex" , locLine = 36 - , locColumn = 36 + , locColumn = 12 } ) ( SymbolPredicate @@ -2503,7 +2503,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 36 - , locColumn = 36 + , locColumn = 20 } ) ( SymbolPredicate @@ -2530,7 +2530,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 36 - , locColumn = 36 + , locColumn = 12 } ) ( SymbolPredicate @@ -2550,7 +2550,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 36 - , locColumn = 36 + , locColumn = 20 } ) ( SymbolPredicate @@ -2663,7 +2663,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 25 - , locColumn = 25 + , locColumn = 41 } ) ( SymbolPredicate @@ -2683,7 +2683,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 25 - , locColumn = 25 + , locColumn = 56 } ) ( SymbolPredicate @@ -3012,7 +3012,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 9 - , locColumn = 9 + , locColumn = 1 } ) ( SymbolPredicate @@ -3074,7 +3074,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 5 - , locColumn = 5 + , locColumn = 1 } ) ( SymbolPredicate @@ -3230,7 +3230,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 40 - , locColumn = 40 + , locColumn = 19 } ) ( SymbolPredicate @@ -3278,7 +3278,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 40 - , locColumn = 40 + , locColumn = 19 } ) ( SymbolPredicate @@ -3298,7 +3298,7 @@ , taskLocation = Location { locFile = "test/examples/coord.tex" , locLine = 39 - , locColumn = 39 + , locColumn = 1 } , taskConjecture = Connected Conjunction ( Connected Conjunction @@ -3332,7 +3332,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 41 - , locColumn = 41 + , locColumn = 26 } ) ( SymbolPredicate @@ -3378,7 +3378,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 41 - , locColumn = 41 + , locColumn = 26 } ) ( SymbolPredicate diff --git a/test/golden/coord/glossing.golden b/test/golden/coord/glossing.golden index a344173..34ea297 100644 --- a/test/golden/coord/glossing.golden +++ b/test/golden/coord/glossing.golden @@ -44,7 +44,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 5 - , locColumn = 5 + , locColumn = 1 } ) ( Marker "foo" ) @@ -78,7 +78,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 9 - , locColumn = 9 + , locColumn = 1 } ) ( Marker "baz" ) @@ -112,7 +112,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 13 - , locColumn = 13 + , locColumn = 1 } ) ( Marker "nouns" ) @@ -195,7 +195,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 18 - , locColumn = 18 + , locColumn = 1 } ) ( Marker "adj_nouns" ) @@ -318,7 +318,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 24 - , locColumn = 24 + , locColumn = 1 } ) ( Marker "nouns_suchthat" ) @@ -329,7 +329,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 25 - , locColumn = 25 + , locColumn = 41 } ) ( SymbolPredicate @@ -347,7 +347,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 25 - , locColumn = 25 + , locColumn = 56 } ) ( SymbolPredicate @@ -440,7 +440,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 30 - , locColumn = 30 + , locColumn = 1 } ) ( Marker "noun_verb" ) @@ -516,7 +516,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 35 - , locColumn = 35 + , locColumn = 1 } ) ( Marker "adjs" ) @@ -526,7 +526,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 36 - , locColumn = 36 + , locColumn = 12 } ) ( SymbolPredicate @@ -544,7 +544,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 36 - , locColumn = 36 + , locColumn = 20 } ) ( SymbolPredicate @@ -564,7 +564,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 39 - , locColumn = 39 + , locColumn = 1 } ) ( Marker "are_nouns" ) @@ -601,7 +601,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 40 - , locColumn = 40 + , locColumn = 19 } ) ( SymbolPredicate @@ -648,7 +648,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 40 - , locColumn = 40 + , locColumn = 19 } ) ( SymbolPredicate @@ -696,7 +696,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 41 - , locColumn = 41 + , locColumn = 26 } ) ( SymbolPredicate @@ -742,7 +742,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 41 - , locColumn = 41 + , locColumn = 26 } ) ( SymbolPredicate diff --git a/test/golden/coord/parsing.golden b/test/golden/coord/parsing.golden index 5ee8706..9eb576a 100644 --- a/test/golden/coord/parsing.golden +++ b/test/golden/coord/parsing.golden @@ -27,7 +27,7 @@ { pos = Location { locFile = "test/examples/coord.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 22 } , formula = FormulaChain ( ChainBase @@ -48,7 +48,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 5 - , locColumn = 5 + , locColumn = 1 } ) ( Marker "foo" ) @@ -59,7 +59,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 6 - , locColumn = 6 + , locColumn = 12 } ) [ Just @@ -71,7 +71,7 @@ { pos = Location { locFile = "test/examples/coord.tex" , locLine = 6 - , locColumn = 6 + , locColumn = 20 } , formula = FormulaChain ( ChainBase @@ -92,7 +92,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 9 - , locColumn = 9 + , locColumn = 1 } ) ( Marker "baz" ) @@ -103,7 +103,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 10 - , locColumn = 10 + , locColumn = 12 } ) [ Just @@ -115,7 +115,7 @@ { pos = Location { locFile = "test/examples/coord.tex" , locLine = 10 - , locColumn = 10 + , locColumn = 20 } , formula = FormulaChain ( ChainBase @@ -136,7 +136,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 13 - , locColumn = 13 + , locColumn = 1 } ) ( Marker "nouns" ) @@ -163,7 +163,7 @@ { pos = Location { locFile = "test/examples/coord.tex" , locLine = 15 - , locColumn = 15 + , locColumn = 10 } , formula = FormulaChain ( ChainBase @@ -184,7 +184,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 18 - , locColumn = 18 + , locColumn = 1 } ) ( Marker "adj_nouns" ) @@ -224,7 +224,7 @@ { pos = Location { locFile = "test/examples/coord.tex" , locLine = 20 - , locColumn = 20 + , locColumn = 10 } , formula = FormulaChain ( ChainBase @@ -245,7 +245,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 24 - , locColumn = 24 + , locColumn = 1 } ) ( Marker "nouns_suchthat" ) @@ -276,7 +276,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 25 - , locColumn = 25 + , locColumn = 34 } ) ( ExprVar @@ -287,7 +287,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 25 - , locColumn = 25 + , locColumn = 41 } ) [ Just @@ -300,7 +300,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 25 - , locColumn = 25 + , locColumn = 49 } ) ( ExprVar @@ -311,7 +311,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 25 - , locColumn = 25 + , locColumn = 56 } ) [ Just @@ -327,7 +327,7 @@ { pos = Location { locFile = "test/examples/coord.tex" , locLine = 26 - , locColumn = 26 + , locColumn = 10 } , formula = FormulaChain ( ChainBase @@ -348,7 +348,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 30 - , locColumn = 30 + , locColumn = 1 } ) ( Marker "noun_verb" ) @@ -360,7 +360,7 @@ { pos = Location { locFile = "test/examples/coord.tex" , locLine = 31 - , locColumn = 31 + , locColumn = 5 } , formula = FormulaChain ( ChainBase @@ -379,13 +379,13 @@ { pos = Location { locFile = "test/examples/coord.tex" , locLine = 31 - , locColumn = 31 + , locColumn = 17 } , args = TermExpr ( Location { locFile = "test/examples/coord.tex" , locLine = 31 - , locColumn = 31 + , locColumn = 17 } ) ( ExprVar @@ -410,7 +410,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 31 - , locColumn = 31 + , locColumn = 30 } ) [ Just @@ -423,7 +423,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 31 - , locColumn = 31 + , locColumn = 39 } ) ( ExprVar @@ -440,7 +440,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 35 - , locColumn = 35 + , locColumn = 1 } ) ( Marker "adjs" ) @@ -450,7 +450,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 36 - , locColumn = 36 + , locColumn = 5 } ) ( ExprVar @@ -461,7 +461,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 36 - , locColumn = 36 + , locColumn = 12 } ) [ Just @@ -471,7 +471,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 36 - , locColumn = 36 + , locColumn = 20 } ) [ Just @@ -486,7 +486,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 39 - , locColumn = 39 + , locColumn = 1 } ) ( Marker "are_nouns" ) @@ -500,7 +500,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 40 - , locColumn = 40 + , locColumn = 19 } ) [ Just @@ -526,13 +526,13 @@ { pos = Location { locFile = "test/examples/coord.tex" , locLine = 41 - , locColumn = 41 + , locColumn = 10 } , args = TermExpr ( Location { locFile = "test/examples/coord.tex" , locLine = 41 - , locColumn = 41 + , locColumn = 10 } ) ( ExprVar @@ -542,7 +542,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 41 - , locColumn = 41 + , locColumn = 18 } ) ( ExprVar @@ -555,7 +555,7 @@ ( Location { locFile = "test/examples/coord.tex" , locLine = 41 - , locColumn = 41 + , locColumn = 26 } ) [ Just diff --git a/test/golden/finite-set-terms/encoding tasks.golden b/test/golden/finite-set-terms/encoding tasks.golden index 5489a03..92f5a68 100644 --- a/test/golden/finite-set-terms/encoding tasks.golden +++ b/test/golden/finite-set-terms/encoding tasks.golden @@ -1,3 +1,3 @@ -fof(emptyset_in_unit,conjecture,elem(emptyset,unit),"test/examples/finite-set-terms.tex 9:9"). +fof(emptyset_in_unit,conjecture,elem(emptyset,unit),"test/examples/finite-set-terms.tex 9:1"). fof(unit,axiom,![Xany]:(elem(Xany,unit)<=>(elem(Xany,emptyset)|Xany=emptyset))). fof(cons,axiom,![Xx,Xy,XX]:(elem(Xx,cons(Xy,XX))<=>(Xx=Xy|elem(Xx,XX)))).
\ No newline at end of file diff --git a/test/golden/finite-set-terms/generating tasks.golden b/test/golden/finite-set-terms/generating tasks.golden index f5a1d1a..cc16d1a 100644 --- a/test/golden/finite-set-terms/generating tasks.golden +++ b/test/golden/finite-set-terms/generating tasks.golden @@ -26,7 +26,7 @@ ( Location { locFile = "test/examples/finite-set-terms.tex" , locLine = 5 - , locColumn = 5 + , locColumn = 1 } ) ( SymbolMixfix @@ -71,7 +71,7 @@ ( Location { locFile = "test/examples/finite-set-terms.tex" , locLine = 5 - , locColumn = 5 + , locColumn = 1 } ) ( SymbolPredicate @@ -205,7 +205,7 @@ , taskLocation = Location { locFile = "test/examples/finite-set-terms.tex" , locLine = 9 - , locColumn = 9 + , locColumn = 1 } , taskConjecture = TermSymbol ( Location diff --git a/test/golden/finite-set-terms/glossing.golden b/test/golden/finite-set-terms/glossing.golden index 939995e..5003c82 100644 --- a/test/golden/finite-set-terms/glossing.golden +++ b/test/golden/finite-set-terms/glossing.golden @@ -91,7 +91,7 @@ ( Location { locFile = "test/examples/finite-set-terms.tex" , locLine = 5 - , locColumn = 5 + , locColumn = 1 } ) ( Marker "unit" ) @@ -148,7 +148,7 @@ ( Location { locFile = "test/examples/finite-set-terms.tex" , locLine = 9 - , locColumn = 9 + , locColumn = 1 } ) ( Marker "emptyset_in_unit" ) diff --git a/test/golden/finite-set-terms/parsing.golden b/test/golden/finite-set-terms/parsing.golden index 3cfc5c4..83f3c72 100644 --- a/test/golden/finite-set-terms/parsing.golden +++ b/test/golden/finite-set-terms/parsing.golden @@ -14,7 +14,7 @@ { pos = Location { locFile = "test/examples/finite-set-terms.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 5 } , formula = FormulaChain ( ChainBase @@ -49,7 +49,7 @@ { pos = Location { locFile = "test/examples/finite-set-terms.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 28 } , formula = FormulaChain ( ChainBase @@ -68,7 +68,7 @@ { pos = Location { locFile = "test/examples/finite-set-terms.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 39 } , formula = FormulaChain ( ChainBase @@ -91,7 +91,7 @@ ( Location { locFile = "test/examples/finite-set-terms.tex" , locLine = 5 - , locColumn = 5 + , locColumn = 1 } ) ( Marker "unit" ) @@ -113,7 +113,7 @@ ( Location { locFile = "test/examples/finite-set-terms.tex" , locLine = 9 - , locColumn = 9 + , locColumn = 1 } ) ( Marker "emptyset_in_unit" ) @@ -122,7 +122,7 @@ { pos = Location { locFile = "test/examples/finite-set-terms.tex" , locLine = 10 - , locColumn = 10 + , locColumn = 5 } , formula = FormulaChain ( ChainBase diff --git a/test/golden/formula/encoding tasks.golden b/test/golden/formula/encoding tasks.golden index 85b286f..3e030cb 100644 --- a/test/golden/formula/encoding tasks.golden +++ b/test/golden/formula/encoding tasks.golden @@ -1,8 +1,8 @@ fof(formula_test_forall,conjecture,![Xx,Xy]:(Xx=Xx&Xy=Xy),"test/examples/formula.tex 1:1"). ------------------ -fof(formula_test_exists,conjecture,?[Xx,Xy]:Xx=Xy,"test/examples/formula.tex 5:5"). +fof(formula_test_exists,conjecture,?[Xx,Xy]:Xx=Xy,"test/examples/formula.tex 5:1"). fof(formula_test_forall,axiom,![Xx,Xy]:(Xx=Xx&Xy=Xy)). ------------------ -fof(formula_test_not_exists,conjecture,?[Xx,Xy]:Xx=Xy<=>~?[Xx]:Xx!=Xx,"test/examples/formula.tex 9:9"). +fof(formula_test_not_exists,conjecture,?[Xx,Xy]:Xx=Xy<=>~?[Xx]:Xx!=Xx,"test/examples/formula.tex 9:1"). fof(formula_test_exists,axiom,?[Xx,Xy]:Xx=Xy). fof(formula_test_forall,axiom,![Xx,Xy]:(Xx=Xx&Xy=Xy)).
\ No newline at end of file diff --git a/test/golden/formula/generating tasks.golden b/test/golden/formula/generating tasks.golden index 253c302..2800b00 100644 --- a/test/golden/formula/generating tasks.golden +++ b/test/golden/formula/generating tasks.golden @@ -117,7 +117,7 @@ , taskLocation = Location { locFile = "test/examples/formula.tex" , locLine = 5 - , locColumn = 5 + , locColumn = 1 } , taskConjecture = Quantified Existentially ( Scope @@ -233,7 +233,7 @@ , taskLocation = Location { locFile = "test/examples/formula.tex" , locLine = 9 - , locColumn = 9 + , locColumn = 1 } , taskConjecture = Connected Equivalence ( Quantified Existentially @@ -266,7 +266,7 @@ ( Location { locFile = "test/examples/formula.tex" , locLine = 10 - , locColumn = 10 + , locColumn = 42 } ) ( Quantified Existentially diff --git a/test/golden/formula/glossing.golden b/test/golden/formula/glossing.golden index 9fe50a3..96c3630 100644 --- a/test/golden/formula/glossing.golden +++ b/test/golden/formula/glossing.golden @@ -62,7 +62,7 @@ ( Location { locFile = "test/examples/formula.tex" , locLine = 5 - , locColumn = 5 + , locColumn = 1 } ) ( Marker "formula_test_exists" ) @@ -98,7 +98,7 @@ ( Location { locFile = "test/examples/formula.tex" , locLine = 9 - , locColumn = 9 + , locColumn = 1 } ) ( Marker "formula_test_not_exists" ) @@ -134,7 +134,7 @@ ( Location { locFile = "test/examples/formula.tex" , locLine = 10 - , locColumn = 10 + , locColumn = 42 } ) ( Quantified Existentially diff --git a/test/golden/formula/parsing.golden b/test/golden/formula/parsing.golden index e3a6f82..ffaec8e 100644 --- a/test/golden/formula/parsing.golden +++ b/test/golden/formula/parsing.golden @@ -11,7 +11,7 @@ { pos = Location { locFile = "test/examples/formula.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 5 } , formula = FormulaQuantified Universally ( NamedVar "x" :| @@ -52,7 +52,7 @@ ( Location { locFile = "test/examples/formula.tex" , locLine = 5 - , locColumn = 5 + , locColumn = 1 } ) ( Marker "formula_test_exists" ) @@ -61,7 +61,7 @@ { pos = Location { locFile = "test/examples/formula.tex" , locLine = 6 - , locColumn = 6 + , locColumn = 5 } , formula = FormulaQuantified Existentially ( NamedVar "x" :| @@ -87,7 +87,7 @@ ( Location { locFile = "test/examples/formula.tex" , locLine = 9 - , locColumn = 9 + , locColumn = 1 } ) ( Marker "formula_test_not_exists" ) @@ -99,7 +99,7 @@ { pos = Location { locFile = "test/examples/formula.tex" , locLine = 10 - , locColumn = 10 + , locColumn = 5 } , formula = FormulaQuantified Existentially ( NamedVar "x" :| @@ -123,13 +123,13 @@ { pos = Location { locFile = "test/examples/formula.tex" , locLine = 10 - , locColumn = 10 + , locColumn = 42 } , stmt = StmtFormula { pos = Location { locFile = "test/examples/formula.tex" , locLine = 10 - , locColumn = 10 + , locColumn = 46 } , formula = FormulaQuantified Existentially ( NamedVar "x" :| [] ) Unbounded diff --git a/test/golden/geometry/encoding tasks.golden b/test/golden/geometry/encoding tasks.golden index 8fa267b..87c0a56 100644 --- a/test/golden/geometry/encoding tasks.golden +++ b/test/golden/geometry/encoding tasks.golden @@ -1,4 +1,4 @@ -fof(cong_refl,conjecture,'Cong'(fa,fb,fa,fb),"test/examples/geometry.tex 82:82"). +fof(cong_refl,conjecture,'Cong'(fa,fb,fa,fb),"test/examples/geometry.tex 82:1"). fof(upperdim,axiom,![Xx,Xy,Xz,Xu,Xv]:((point(Xx)&point(Xy)&point(Xz)&point(Xu)&point(Xv))=>(('Cong'(Xx,Xu,Xx,Xv)&'Cong'(Xy,Xu,Xy,Xv)&'Cong'(Xz,Xu,Xz,Xv)&Xu!=Xv)=>collinear(Xx,Xy,Xz)))). fof(innerpasch,axiom,![Xx,Xy,Xz,Xu,Xv,Xw]:((point(Xx)&point(Xy)&point(Xz)&point(Xu)&point(Xv)&point(Xw))=>(('Betw'(Xx,Xu,Xz)&'Betw'(Xy,Xv,Xz))=>?[Xw]:(point(Xw)&'Betw'(Xu,Xw,Xy)&'Betw'(Xv,Xw,Xx))))). fof(betw_id,axiom,![Xa,Xb]:((point(Xa)&point(Xb))=>('Betw'(Xa,Xb,Xa)=>Xa=Xb))). @@ -12,7 +12,7 @@ fof(collinear,axiom,![Xa,Xb,Xc]:(collinear(Xa,Xb,Xc)<=>('Betw'(Xa,Xb,Xc)|'Betw'( fof(cong_refl1,axiom,point(fb)). fof(cong_refl2,axiom,point(fa)). ------------------ -fof(cong_sym,conjecture,'Cong'(fc,fd,fa,fb),"test/examples/geometry.tex 88:88"). +fof(cong_sym,conjecture,'Cong'(fc,fd,fa,fb),"test/examples/geometry.tex 88:1"). fof(cong_refl,axiom,![Xa,Xb]:((point(Xa)&point(Xb))=>'Cong'(Xa,Xb,Xa,Xb))). fof(upperdim,axiom,![Xx,Xy,Xz,Xu,Xv]:((point(Xx)&point(Xy)&point(Xz)&point(Xu)&point(Xv))=>(('Cong'(Xx,Xu,Xx,Xv)&'Cong'(Xy,Xu,Xy,Xv)&'Cong'(Xz,Xu,Xz,Xv)&Xu!=Xv)=>collinear(Xx,Xy,Xz)))). fof(innerpasch,axiom,![Xx,Xy,Xz,Xu,Xv,Xw]:((point(Xx)&point(Xy)&point(Xz)&point(Xu)&point(Xv)&point(Xw))=>(('Betw'(Xx,Xu,Xz)&'Betw'(Xy,Xv,Xz))=>?[Xw]:(point(Xw)&'Betw'(Xu,Xw,Xy)&'Betw'(Xv,Xw,Xx))))). @@ -30,7 +30,7 @@ fof(cong_sym3,axiom,point(fc)). fof(cong_sym4,axiom,point(fb)). fof(cong_sym5,axiom,point(fa)). ------------------ -fof(cong_transitive,conjecture,('Cong'(fa,fb,fc,fd)&'Cong'(fc,fd,fe,ff))=>'Cong'(fa,fb,fe,ff),"test/examples/geometry.tex 95:95"). +fof(cong_transitive,conjecture,('Cong'(fa,fb,fc,fd)&'Cong'(fc,fd,fe,ff))=>'Cong'(fa,fb,fe,ff),"test/examples/geometry.tex 95:1"). fof(cong_sym,axiom,![Xa,Xb,Xc,Xd]:((point(Xa)&point(Xb)&point(Xc)&point(Xd)&'Cong'(Xa,Xb,Xc,Xd))=>'Cong'(Xc,Xd,Xa,Xb))). fof(cong_refl,axiom,![Xa,Xb]:((point(Xa)&point(Xb))=>'Cong'(Xa,Xb,Xa,Xb))). fof(upperdim,axiom,![Xx,Xy,Xz,Xu,Xv]:((point(Xx)&point(Xy)&point(Xz)&point(Xu)&point(Xv))=>(('Cong'(Xx,Xu,Xx,Xv)&'Cong'(Xy,Xu,Xy,Xv)&'Cong'(Xz,Xu,Xz,Xv)&Xu!=Xv)=>collinear(Xx,Xy,Xz)))). @@ -50,7 +50,7 @@ fof(cong_transitive4,axiom,point(fc)). fof(cong_transitive5,axiom,point(fb)). fof(cong_transitive6,axiom,point(fa)). ------------------ -fof(cong_shuffle_left,conjecture,'Cong'(fa,fb,fc,fd)=>'Cong'(fb,fa,fc,fd),"test/examples/geometry.tex 102:102"). +fof(cong_shuffle_left,conjecture,'Cong'(fa,fb,fc,fd)=>'Cong'(fb,fa,fc,fd),"test/examples/geometry.tex 102:1"). fof(cong_transitive,axiom,![Xa,Xb,Xc,Xd,Xe,Xf]:((point(Xa)&point(Xb)&point(Xc)&point(Xd)&point(Xe)&point(Xf))=>(('Cong'(Xa,Xb,Xc,Xd)&'Cong'(Xc,Xd,Xe,Xf))=>'Cong'(Xa,Xb,Xe,Xf)))). fof(cong_sym,axiom,![Xa,Xb,Xc,Xd]:((point(Xa)&point(Xb)&point(Xc)&point(Xd)&'Cong'(Xa,Xb,Xc,Xd))=>'Cong'(Xc,Xd,Xa,Xb))). fof(cong_refl,axiom,![Xa,Xb]:((point(Xa)&point(Xb))=>'Cong'(Xa,Xb,Xa,Xb))). @@ -69,7 +69,7 @@ fof(cong_shuffle_left2,axiom,point(fc)). fof(cong_shuffle_left3,axiom,point(fb)). fof(cong_shuffle_left4,axiom,point(fa)). ------------------ -fof(cong_shuffle_right,conjecture,'Cong'(fa,fb,fc,fd)=>'Cong'(fb,fa,fd,fc),"test/examples/geometry.tex 109:109"). +fof(cong_shuffle_right,conjecture,'Cong'(fa,fb,fc,fd)=>'Cong'(fb,fa,fd,fc),"test/examples/geometry.tex 109:1"). fof(cong_shuffle_left,axiom,![Xa,Xb,Xc,Xd]:((point(Xa)&point(Xb)&point(Xc)&point(Xd))=>('Cong'(Xa,Xb,Xc,Xd)=>'Cong'(Xb,Xa,Xc,Xd)))). fof(cong_transitive,axiom,![Xa,Xb,Xc,Xd,Xe,Xf]:((point(Xa)&point(Xb)&point(Xc)&point(Xd)&point(Xe)&point(Xf))=>(('Cong'(Xa,Xb,Xc,Xd)&'Cong'(Xc,Xd,Xe,Xf))=>'Cong'(Xa,Xb,Xe,Xf)))). fof(cong_sym,axiom,![Xa,Xb,Xc,Xd]:((point(Xa)&point(Xb)&point(Xc)&point(Xd)&'Cong'(Xa,Xb,Xc,Xd))=>'Cong'(Xc,Xd,Xa,Xb))). @@ -89,7 +89,7 @@ fof(cong_shuffle_right2,axiom,point(fc)). fof(cong_shuffle_right3,axiom,point(fb)). fof(cong_shuffle_right4,axiom,point(fa)). ------------------ -fof(cong_zero,conjecture,'Cong'(fa,fa,fb,fb),"test/examples/geometry.tex 116:116"). +fof(cong_zero,conjecture,'Cong'(fa,fa,fb,fb),"test/examples/geometry.tex 116:1"). fof(cong_shuffle_right,axiom,![Xa,Xb,Xc,Xd]:((point(Xa)&point(Xb)&point(Xc)&point(Xd))=>('Cong'(Xa,Xb,Xc,Xd)=>'Cong'(Xb,Xa,Xd,Xc)))). fof(cong_shuffle_left,axiom,![Xa,Xb,Xc,Xd]:((point(Xa)&point(Xb)&point(Xc)&point(Xd))=>('Cong'(Xa,Xb,Xc,Xd)=>'Cong'(Xb,Xa,Xc,Xd)))). fof(cong_transitive,axiom,![Xa,Xb,Xc,Xd,Xe,Xf]:((point(Xa)&point(Xb)&point(Xc)&point(Xd)&point(Xe)&point(Xf))=>(('Cong'(Xa,Xb,Xc,Xd)&'Cong'(Xc,Xd,Xe,Xf))=>'Cong'(Xa,Xb,Xe,Xf)))). diff --git a/test/golden/geometry/generating tasks.golden b/test/golden/geometry/generating tasks.golden index ea503b7..89a3ea5 100644 --- a/test/golden/geometry/generating tasks.golden +++ b/test/golden/geometry/generating tasks.golden @@ -271,7 +271,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 70 - , locColumn = 70 + , locColumn = 17 } ) ( SymbolPredicate @@ -1349,7 +1349,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 26 - , locColumn = 26 + , locColumn = 1 } ) ( SymbolPredicate @@ -2444,7 +2444,7 @@ , taskLocation = Location { locFile = "test/examples/geometry.tex" , locLine = 82 - , locColumn = 82 + , locColumn = 1 } , taskConjecture = TermSymbol ( Location @@ -2833,7 +2833,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 70 - , locColumn = 70 + , locColumn = 17 } ) ( SymbolPredicate @@ -3911,7 +3911,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 26 - , locColumn = 26 + , locColumn = 1 } ) ( SymbolPredicate @@ -5084,7 +5084,7 @@ , taskLocation = Location { locFile = "test/examples/geometry.tex" , locLine = 88 - , locColumn = 88 + , locColumn = 1 } , taskConjecture = TermSymbol ( Location @@ -5657,7 +5657,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 70 - , locColumn = 70 + , locColumn = 17 } ) ( SymbolPredicate @@ -6735,7 +6735,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 26 - , locColumn = 26 + , locColumn = 1 } ) ( SymbolPredicate @@ -7942,7 +7942,7 @@ , taskLocation = Location { locFile = "test/examples/geometry.tex" , locLine = 95 - , locColumn = 95 + , locColumn = 1 } , taskConjecture = Connected Implication ( Connected Conjunction @@ -8833,7 +8833,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 70 - , locColumn = 70 + , locColumn = 17 } ) ( SymbolPredicate @@ -9911,7 +9911,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 26 - , locColumn = 26 + , locColumn = 1 } ) ( SymbolPredicate @@ -11062,7 +11062,7 @@ , taskLocation = Location { locFile = "test/examples/geometry.tex" , locLine = 102 - , locColumn = 102 + , locColumn = 1 } , taskConjecture = Connected Implication ( TermSymbol @@ -12115,7 +12115,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 70 - , locColumn = 70 + , locColumn = 17 } ) ( SymbolPredicate @@ -13193,7 +13193,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 26 - , locColumn = 26 + , locColumn = 1 } ) ( SymbolPredicate @@ -14344,7 +14344,7 @@ , taskLocation = Location { locFile = "test/examples/geometry.tex" , locLine = 109 - , locColumn = 109 + , locColumn = 1 } , taskConjecture = Connected Implication ( TermSymbol @@ -15581,7 +15581,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 70 - , locColumn = 70 + , locColumn = 17 } ) ( SymbolPredicate @@ -16659,7 +16659,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 26 - , locColumn = 26 + , locColumn = 1 } ) ( SymbolPredicate @@ -17754,7 +17754,7 @@ , taskLocation = Location { locFile = "test/examples/geometry.tex" , locLine = 116 - , locColumn = 116 + , locColumn = 1 } , taskConjecture = TermSymbol ( Location diff --git a/test/golden/geometry/glossing.golden b/test/golden/geometry/glossing.golden index 8f60934..b816c15 100644 --- a/test/golden/geometry/glossing.golden +++ b/test/golden/geometry/glossing.golden @@ -86,7 +86,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 5 - , locColumn = 5 + , locColumn = 1 } ) ( Marker "cong_refl_swap" ) @@ -171,7 +171,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 10 - , locColumn = 10 + , locColumn = 1 } ) ( Marker "cong_pseudotransitive" ) @@ -354,7 +354,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 15 - , locColumn = 15 + , locColumn = 1 } ) ( Marker "cong_id" ) @@ -486,7 +486,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 21 - , locColumn = 21 + , locColumn = 1 } ) ( Marker "segment_construction" ) @@ -594,7 +594,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 26 - , locColumn = 26 + , locColumn = 1 } ) ( Marker "ofs" ) @@ -958,7 +958,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 39 - , locColumn = 39 + , locColumn = 1 } ) ( Marker "five_segment" ) @@ -1255,7 +1255,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 46 - , locColumn = 46 + , locColumn = 1 } ) ( Marker "betw_id" ) @@ -1358,7 +1358,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 52 - , locColumn = 52 + , locColumn = 1 } ) ( Marker "innerpasch" ) @@ -1663,7 +1663,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 66 - , locColumn = 66 + , locColumn = 1 } ) ( Marker "upperdim" ) @@ -1893,7 +1893,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 70 - , locColumn = 70 + , locColumn = 17 } ) ( SymbolPredicate @@ -1923,7 +1923,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 82 - , locColumn = 82 + , locColumn = 1 } ) ( Marker "cong_refl" ) @@ -2008,7 +2008,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 88 - , locColumn = 88 + , locColumn = 1 } ) ( Marker "cong_sym" ) @@ -2168,7 +2168,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 95 - , locColumn = 95 + , locColumn = 1 } ) ( Marker "cong_transitive" ) @@ -2405,7 +2405,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 102 - , locColumn = 102 + , locColumn = 1 } ) ( Marker "cong_shuffle_left" ) @@ -2566,7 +2566,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 109 - , locColumn = 109 + , locColumn = 1 } ) ( Marker "cong_shuffle_right" ) @@ -2727,7 +2727,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 116 - , locColumn = 116 + , locColumn = 1 } ) ( Marker "cong_zero" ) diff --git a/test/golden/geometry/parsing.golden b/test/golden/geometry/parsing.golden index e9719a7..3e05667 100644 --- a/test/golden/geometry/parsing.golden +++ b/test/golden/geometry/parsing.golden @@ -13,7 +13,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 12 } ) [ Just @@ -37,7 +37,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 43 } , formula = FormulaPredicate ( PrefixPredicate "Betw" 3 ) @@ -57,7 +57,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 63 } , formula = FormulaPredicate ( PrefixPredicate "Betw" 3 ) @@ -74,7 +74,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 83 } , formula = FormulaPredicate ( PrefixPredicate "Betw" 3 ) @@ -95,7 +95,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 5 - , locColumn = 5 + , locColumn = 1 } ) ( Marker "cong_refl_swap" ) @@ -122,7 +122,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 7 - , locColumn = 7 + , locColumn = 10 } , formula = FormulaPredicate ( PrefixPredicate "Cong" 4 ) @@ -143,7 +143,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 10 - , locColumn = 10 + , locColumn = 1 } ) ( Marker "cong_pseudotransitive" ) @@ -175,7 +175,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 12 - , locColumn = 12 + , locColumn = 5 } ) , stmt1 = StmtConnected @@ -185,7 +185,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 12 - , locColumn = 12 + , locColumn = 8 } , formula = FormulaPredicate ( PrefixPredicate "Cong" 4 ) @@ -204,7 +204,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 12 - , locColumn = 12 + , locColumn = 32 } , formula = FormulaPredicate ( PrefixPredicate "Cong" 4 ) @@ -224,7 +224,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 12 - , locColumn = 12 + , locColumn = 57 } , formula = FormulaPredicate ( PrefixPredicate "Cong" 4 ) @@ -246,7 +246,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 15 - , locColumn = 15 + , locColumn = 1 } ) ( Marker "cong_id" ) @@ -277,14 +277,14 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 17 - , locColumn = 17 + , locColumn = 5 } ) , stmt1 = StmtFormula { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 17 - , locColumn = 17 + , locColumn = 8 } , formula = FormulaPredicate ( PrefixPredicate "Cong" 4 ) @@ -303,7 +303,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 17 - , locColumn = 17 + , locColumn = 33 } , formula = FormulaChain ( ChainBase @@ -325,7 +325,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 21 - , locColumn = 21 + , locColumn = 1 } ) ( Marker "segment_construction" ) @@ -334,7 +334,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 22 - , locColumn = 22 + , locColumn = 5 } , np = NounPhrase ( [] ) ( Noun @@ -361,7 +361,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 22 - , locColumn = 22 + , locColumn = 40 } , formula = FormulaPredicate ( PrefixPredicate "Betw" 3 ) @@ -378,7 +378,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 22 - , locColumn = 22 + , locColumn = 61 } , formula = FormulaPredicate ( PrefixPredicate "Cong" 4 ) @@ -403,7 +403,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 26 - , locColumn = 26 + , locColumn = 1 } ) ( Marker "ofs" ) @@ -453,7 +453,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 29 - , locColumn = 29 + , locColumn = 5 } , formula = Connected Conjunction ( FormulaPredicate @@ -483,7 +483,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 32 - , locColumn = 32 + , locColumn = 5 } , formula = Connected Conjunction ( Connected Conjunction @@ -550,7 +550,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 39 - , locColumn = 39 + , locColumn = 1 } ) ( Marker "five_segment" ) @@ -586,7 +586,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 41 - , locColumn = 41 + , locColumn = 5 } ) , stmt1 = StmtConnected @@ -596,7 +596,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 41 - , locColumn = 41 + , locColumn = 8 } , formula = FormulaPredicate ( PrefixPredicate "OFS" 8 ) @@ -623,7 +623,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 42 - , locColumn = 42 + , locColumn = 5 } , formula = FormulaChain ( ChainBase @@ -643,7 +643,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 42 - , locColumn = 42 + , locColumn = 21 } , formula = FormulaPredicate ( PrefixPredicate "Cong" 4 ) @@ -665,7 +665,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 46 - , locColumn = 46 + , locColumn = 1 } ) ( Marker "betw_id" ) @@ -694,14 +694,14 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 48 - , locColumn = 48 + , locColumn = 5 } ) , stmt1 = StmtFormula { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 48 - , locColumn = 48 + , locColumn = 8 } , formula = FormulaPredicate ( PrefixPredicate "Betw" 3 ) @@ -718,7 +718,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 48 - , locColumn = 48 + , locColumn = 30 } , formula = FormulaChain ( ChainBase @@ -740,7 +740,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 52 - , locColumn = 52 + , locColumn = 1 } ) ( Marker "innerpasch" ) @@ -774,7 +774,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 54 - , locColumn = 54 + , locColumn = 5 } ) , stmt1 = StmtConnected @@ -784,7 +784,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 54 - , locColumn = 54 + , locColumn = 8 } , formula = FormulaPredicate ( PrefixPredicate "Betw" 3 ) @@ -801,7 +801,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 54 - , locColumn = 54 + , locColumn = 29 } , formula = FormulaPredicate ( PrefixPredicate "Betw" 3 ) @@ -819,7 +819,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 54 - , locColumn = 54 + , locColumn = 51 } , np = NounPhrase ( [] ) ( Noun @@ -846,7 +846,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 55 - , locColumn = 55 + , locColumn = 15 } , formula = FormulaPredicate ( PrefixPredicate "Betw" 3 ) @@ -863,7 +863,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 55 - , locColumn = 55 + , locColumn = 36 } , formula = FormulaPredicate ( PrefixPredicate "Betw" 3 ) @@ -887,7 +887,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 66 - , locColumn = 66 + , locColumn = 1 } ) ( Marker "upperdim" ) @@ -920,7 +920,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 68 - , locColumn = 68 + , locColumn = 5 } ) , stmt1 = StmtConnected @@ -930,7 +930,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 68 - , locColumn = 68 + , locColumn = 8 } , formula = FormulaPredicate ( PrefixPredicate "Cong" 4 ) @@ -952,7 +952,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 68 - , locColumn = 68 + , locColumn = 32 } , formula = FormulaPredicate ( PrefixPredicate "Cong" 4 ) @@ -974,7 +974,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 69 - , locColumn = 69 + , locColumn = 9 } , formula = FormulaPredicate ( PrefixPredicate "Cong" 4 ) @@ -993,7 +993,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 69 - , locColumn = 69 + , locColumn = 33 } , formula = FormulaChain ( ChainBase @@ -1016,7 +1016,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 70 - , locColumn = 70 + , locColumn = 10 } ) ( ExprVar @@ -1027,7 +1027,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 70 - , locColumn = 70 + , locColumn = 17 } ) [ Just @@ -1043,7 +1043,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 70 - , locColumn = 70 + , locColumn = 32 } ) ( ExprVar @@ -1053,7 +1053,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 70 - , locColumn = 70 + , locColumn = 40 } ) ( ExprVar @@ -1069,7 +1069,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 82 - , locColumn = 82 + , locColumn = 1 } ) ( Marker "cong_refl" ) @@ -1096,7 +1096,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 84 - , locColumn = 84 + , locColumn = 10 } , formula = FormulaPredicate ( PrefixPredicate "Cong" 4 ) @@ -1117,7 +1117,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 88 - , locColumn = 88 + , locColumn = 1 } ) ( Marker "cong_sym" ) @@ -1147,7 +1147,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 90 - , locColumn = 90 + , locColumn = 13 } , formula = FormulaPredicate ( PrefixPredicate "Cong" 4 ) @@ -1168,7 +1168,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 91 - , locColumn = 91 + , locColumn = 10 } , formula = FormulaPredicate ( PrefixPredicate "Cong" 4 ) @@ -1189,7 +1189,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 95 - , locColumn = 95 + , locColumn = 1 } ) ( Marker "cong_transitive" ) @@ -1223,7 +1223,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 97 - , locColumn = 97 + , locColumn = 5 } ) , stmt1 = StmtConnected @@ -1233,7 +1233,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 97 - , locColumn = 97 + , locColumn = 8 } , formula = FormulaPredicate ( PrefixPredicate "Cong" 4 ) @@ -1252,7 +1252,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 97 - , locColumn = 97 + , locColumn = 32 } , formula = FormulaPredicate ( PrefixPredicate "Cong" 4 ) @@ -1272,7 +1272,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 98 - , locColumn = 98 + , locColumn = 10 } , formula = FormulaPredicate ( PrefixPredicate "Cong" 4 ) @@ -1294,7 +1294,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 102 - , locColumn = 102 + , locColumn = 1 } ) ( Marker "cong_shuffle_left" ) @@ -1326,14 +1326,14 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 104 - , locColumn = 104 + , locColumn = 5 } ) , stmt1 = StmtFormula { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 104 - , locColumn = 104 + , locColumn = 8 } , formula = FormulaPredicate ( PrefixPredicate "Cong" 4 ) @@ -1352,7 +1352,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 105 - , locColumn = 105 + , locColumn = 10 } , formula = FormulaPredicate ( PrefixPredicate "Cong" 4 ) @@ -1374,7 +1374,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 109 - , locColumn = 109 + , locColumn = 1 } ) ( Marker "cong_shuffle_right" ) @@ -1406,14 +1406,14 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 111 - , locColumn = 111 + , locColumn = 5 } ) , stmt1 = StmtFormula { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 111 - , locColumn = 111 + , locColumn = 8 } , formula = FormulaPredicate ( PrefixPredicate "Cong" 4 ) @@ -1432,7 +1432,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 112 - , locColumn = 112 + , locColumn = 10 } , formula = FormulaPredicate ( PrefixPredicate "Cong" 4 ) @@ -1454,7 +1454,7 @@ ( Location { locFile = "test/examples/geometry.tex" , locLine = 116 - , locColumn = 116 + , locColumn = 1 } ) ( Marker "cong_zero" ) @@ -1481,7 +1481,7 @@ { pos = Location { locFile = "test/examples/geometry.tex" , locLine = 118 - , locColumn = 118 + , locColumn = 10 } , formula = FormulaPredicate ( PrefixPredicate "Cong" 4 ) diff --git a/test/golden/indefinite-terms/encoding tasks.golden b/test/golden/indefinite-terms/encoding tasks.golden index 1f81e53..cffcf35 100644 --- a/test/golden/indefinite-terms/encoding tasks.golden +++ b/test/golden/indefinite-terms/encoding tasks.golden @@ -1,3 +1,3 @@ fof(indefinite_test_forall,conjecture,$true,"test/examples/indefinite-terms.tex 1:1"). ------------------ -fof(indefinite_test_exists,conjecture,$true,"test/examples/indefinite-terms.tex 5:5").
\ No newline at end of file +fof(indefinite_test_exists,conjecture,$true,"test/examples/indefinite-terms.tex 5:1").
\ No newline at end of file diff --git a/test/golden/indefinite-terms/generating tasks.golden b/test/golden/indefinite-terms/generating tasks.golden index 26e5533..e9e294c 100644 --- a/test/golden/indefinite-terms/generating tasks.golden +++ b/test/golden/indefinite-terms/generating tasks.golden @@ -16,7 +16,7 @@ , taskLocation = Location { locFile = "test/examples/indefinite-terms.tex" , locLine = 5 - , locColumn = 5 + , locColumn = 1 } , taskConjecture = PropositionalConstant IsTop } diff --git a/test/golden/indefinite-terms/glossing.golden b/test/golden/indefinite-terms/glossing.golden index 2ea8045..3cab448 100644 --- a/test/golden/indefinite-terms/glossing.golden +++ b/test/golden/indefinite-terms/glossing.golden @@ -17,7 +17,7 @@ ( Location { locFile = "test/examples/indefinite-terms.tex" , locLine = 5 - , locColumn = 5 + , locColumn = 1 } ) ( Marker "indefinite_test_exists" ) diff --git a/test/golden/indefinite-terms/parsing.golden b/test/golden/indefinite-terms/parsing.golden index ba53617..af4322c 100644 --- a/test/golden/indefinite-terms/parsing.golden +++ b/test/golden/indefinite-terms/parsing.golden @@ -11,13 +11,13 @@ { pos = Location { locFile = "test/examples/indefinite-terms.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 5 } , args = TermQuantified Universally ( Location { locFile = "test/examples/indefinite-terms.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 5 } ) NounPhrase ( [] ) ( Noun @@ -54,7 +54,7 @@ ( Location { locFile = "test/examples/indefinite-terms.tex" , locLine = 5 - , locColumn = 5 + , locColumn = 1 } ) ( Marker "indefinite_test_exists" ) @@ -63,13 +63,13 @@ { pos = Location { locFile = "test/examples/indefinite-terms.tex" , locLine = 6 - , locColumn = 6 + , locColumn = 5 } , args = TermQuantified Existentially ( Location { locFile = "test/examples/indefinite-terms.tex" , locLine = 6 - , locColumn = 6 + , locColumn = 5 } ) NounPhrase ( [] ) ( Noun diff --git a/test/golden/inductive/encoding tasks.golden b/test/golden/inductive/encoding tasks.golden index f1dc059..ea369fd 100644 --- a/test/golden/inductive/encoding tasks.golden +++ b/test/golden/inductive/encoding tasks.golden @@ -1,4 +1,4 @@ -fof(fin,conjecture,elem(emptyset,pow(fA)),"test/examples/inductive.tex 31:31"). +fof(fin,conjecture,elem(emptyset,pow(fA)),"test/examples/inductive.tex 31:1"). fof(lmao,axiom,![Xx]:elem(Xx,emptyset)). fof(preimg,axiom,![XR,XA]:preimg(XR,XA)=emptyset). fof(fld,axiom,![XR]:fld(XR)=emptyset). @@ -7,7 +7,7 @@ fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). fof(pow,axiom,![XA]:pow(XA)=emptyset). fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)). ------------------ -fof(fin,conjecture,(elem(fa,fA)&elem(fB,pow(fA)))=>elem(cons(fa,fB),pow(fA)),"test/examples/inductive.tex 31:31"). +fof(fin,conjecture,(elem(fa,fA)&elem(fB,pow(fA)))=>elem(cons(fa,fB),pow(fA)),"test/examples/inductive.tex 31:1"). fof(lmao,axiom,![Xx]:elem(Xx,emptyset)). fof(preimg,axiom,![XR,XA]:preimg(XR,XA)=emptyset). fof(fld,axiom,![XR]:fld(XR)=emptyset). @@ -16,7 +16,7 @@ fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). fof(pow,axiom,![XA]:pow(XA)=emptyset). fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)). ------------------ -fof(fin_mono,conjecture,subseteq(fin(fA),fin(fB)),"test/examples/inductive.tex 39:39"). +fof(fin_mono,conjecture,subseteq(fin(fA),fin(fB)),"test/examples/inductive.tex 39:1"). fof(fin,axiom,![Xa,XA,XB]:((elem(Xa,XA)&elem(XB,fin(XA)))=>elem(cons(Xa,XB),fin(XA)))). fof(fin,axiom,![XA]:elem(emptyset,fin(XA))). fof(fin,axiom,![XA]:subseteq(fin(XA),pow(XA))). @@ -29,7 +29,7 @@ fof(pow,axiom,![XA]:pow(XA)=emptyset). fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)). fof(fin_mono1,axiom,subseteq(fA,fB)). ------------------ -fof(tracl,conjecture,elem(fw,fR)=>elem(fw,times(fld(fR),fld(fR))),"test/examples/inductive.tex 45:45"). +fof(tracl,conjecture,elem(fw,fR)=>elem(fw,times(fld(fR),fld(fR))),"test/examples/inductive.tex 45:1"). fof(fin_mono,axiom,![XA,XB]:(subseteq(XA,XB)=>subseteq(fin(XA),fin(XB)))). fof(fin,axiom,![Xa,XA,XB]:((elem(Xa,XA)&elem(XB,fin(XA)))=>elem(cons(Xa,XB),fin(XA)))). fof(fin,axiom,![XA]:elem(emptyset,fin(XA))). @@ -42,7 +42,7 @@ fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). fof(pow,axiom,![XA]:pow(XA)=emptyset). fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)). ------------------ -fof(tracl,conjecture,(elem(pair(fa,fb),times(fld(fR),fld(fR)))&elem(pair(fb,fc),fR))=>elem(pair(fa,fc),times(fld(fR),fld(fR))),"test/examples/inductive.tex 45:45"). +fof(tracl,conjecture,(elem(pair(fa,fb),times(fld(fR),fld(fR)))&elem(pair(fb,fc),fR))=>elem(pair(fa,fc),times(fld(fR),fld(fR))),"test/examples/inductive.tex 45:1"). fof(fin_mono,axiom,![XA,XB]:(subseteq(XA,XB)=>subseteq(fin(XA),fin(XB)))). fof(fin,axiom,![Xa,XA,XB]:((elem(Xa,XA)&elem(XB,fin(XA)))=>elem(cons(Xa,XB),fin(XA)))). fof(fin,axiom,![XA]:elem(emptyset,fin(XA))). @@ -55,7 +55,7 @@ fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). fof(pow,axiom,![XA]:pow(XA)=emptyset). fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)). ------------------ -fof(quasirefltracl,conjecture,elem(fa,fld(fR))=>elem(pair(fa,fa),times(fld(fR),fld(fR))),"test/examples/inductive.tex 53:53"). +fof(quasirefltracl,conjecture,elem(fa,fld(fR))=>elem(pair(fa,fa),times(fld(fR),fld(fR))),"test/examples/inductive.tex 53:1"). fof(tracl,axiom,![Xa,Xb,XR,Xc]:((elem(pair(Xa,Xb),tracl(XR))&elem(pair(Xb,Xc),XR))=>elem(pair(Xa,Xc),tracl(XR)))). fof(tracl,axiom,![Xw,XR]:(elem(Xw,XR)=>elem(Xw,tracl(XR)))). fof(tracl,axiom,![XR]:subseteq(tracl(XR),times(fld(XR),fld(XR)))). @@ -71,7 +71,7 @@ fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). fof(pow,axiom,![XA]:pow(XA)=emptyset). fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)). ------------------ -fof(quasirefltracl,conjecture,(elem(pair(fa,fb),times(fld(fR),fld(fR)))&elem(pair(fb,fc),fR))=>elem(pair(fa,fc),times(fld(fR),fld(fR))),"test/examples/inductive.tex 53:53"). +fof(quasirefltracl,conjecture,(elem(pair(fa,fb),times(fld(fR),fld(fR)))&elem(pair(fb,fc),fR))=>elem(pair(fa,fc),times(fld(fR),fld(fR))),"test/examples/inductive.tex 53:1"). fof(tracl,axiom,![Xa,Xb,XR,Xc]:((elem(pair(Xa,Xb),tracl(XR))&elem(pair(Xb,Xc),XR))=>elem(pair(Xa,Xc),tracl(XR)))). fof(tracl,axiom,![Xw,XR]:(elem(Xw,XR)=>elem(Xw,tracl(XR)))). fof(tracl,axiom,![XR]:subseteq(tracl(XR),times(fld(XR),fld(XR)))). @@ -87,7 +87,7 @@ fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). fof(pow,axiom,![XA]:pow(XA)=emptyset). fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)). ------------------ -fof(refltracl,conjecture,elem(fa,fA)=>elem(pair(fa,fa),times(fA,fA)),"test/examples/inductive.tex 61:61"). +fof(refltracl,conjecture,elem(fa,fA)=>elem(pair(fa,fa),times(fA,fA)),"test/examples/inductive.tex 61:1"). fof(quasirefltracl,axiom,![Xa,Xb,XR,Xc]:((elem(pair(Xa,Xb),quasirefltracl(XR))&elem(pair(Xb,Xc),XR))=>elem(pair(Xa,Xc),quasirefltracl(XR)))). fof(quasirefltracl,axiom,![Xa,XR]:(elem(Xa,fld(XR))=>elem(pair(Xa,Xa),quasirefltracl(XR)))). fof(quasirefltracl,axiom,![XR]:subseteq(quasirefltracl(XR),times(fld(XR),fld(XR)))). @@ -106,7 +106,7 @@ fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). fof(pow,axiom,![XA]:pow(XA)=emptyset). fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)). ------------------ -fof(refltracl,conjecture,(elem(pair(fa,fb),times(fA,fA))&elem(pair(fb,fc),fR))=>elem(pair(fa,fc),times(fA,fA)),"test/examples/inductive.tex 61:61"). +fof(refltracl,conjecture,(elem(pair(fa,fb),times(fA,fA))&elem(pair(fb,fc),fR))=>elem(pair(fa,fc),times(fA,fA)),"test/examples/inductive.tex 61:1"). fof(quasirefltracl,axiom,![Xa,Xb,XR,Xc]:((elem(pair(Xa,Xb),quasirefltracl(XR))&elem(pair(Xb,Xc),XR))=>elem(pair(Xa,Xc),quasirefltracl(XR)))). fof(quasirefltracl,axiom,![Xa,XR]:(elem(Xa,fld(XR))=>elem(pair(Xa,Xa),quasirefltracl(XR)))). fof(quasirefltracl,axiom,![XR]:subseteq(quasirefltracl(XR),times(fld(XR),fld(XR)))). @@ -125,7 +125,7 @@ fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). fof(pow,axiom,![XA]:pow(XA)=emptyset). fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)). ------------------ -fof(acc,conjecture,![Xxa,Xxb]:(subseteq(Xxa,Xxb)=>subseteq(pow(Xxa),pow(Xxb))),"test/examples/inductive.tex 69:69"). +fof(acc,conjecture,![Xxa,Xxb]:(subseteq(Xxa,Xxb)=>subseteq(pow(Xxa),pow(Xxb))),"test/examples/inductive.tex 69:1"). fof(refltracl,axiom,![Xa,Xb,XA,XR,Xc]:((elem(pair(Xa,Xb),refltracl(XA,XR))&elem(pair(Xb,Xc),XR))=>elem(pair(Xa,Xc),refltracl(XA,XR)))). fof(refltracl,axiom,![Xa,XA,XR]:(elem(Xa,XA)=>elem(pair(Xa,Xa),refltracl(XA,XR)))). fof(refltracl,axiom,![XA,XR]:subseteq(refltracl(XA,XR),times(XA,XA))). @@ -147,7 +147,7 @@ fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). fof(pow,axiom,![XA]:pow(XA)=emptyset). fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)). ------------------ -fof(acc,conjecture,(elem(fa,fld(fR))&elem(preimg(fR,cons(fa,emptyset)),pow(fld(fR))))=>elem(fa,fld(fR)),"test/examples/inductive.tex 69:69"). +fof(acc,conjecture,(elem(fa,fld(fR))&elem(preimg(fR,cons(fa,emptyset)),pow(fld(fR))))=>elem(fa,fld(fR)),"test/examples/inductive.tex 69:1"). fof(refltracl,axiom,![Xa,Xb,XA,XR,Xc]:((elem(pair(Xa,Xb),refltracl(XA,XR))&elem(pair(Xb,Xc),XR))=>elem(pair(Xa,Xc),refltracl(XA,XR)))). fof(refltracl,axiom,![Xa,XA,XR]:(elem(Xa,XA)=>elem(pair(Xa,Xa),refltracl(XA,XR)))). fof(refltracl,axiom,![XA,XR]:subseteq(refltracl(XA,XR),times(XA,XA))). diff --git a/test/golden/inductive/generating tasks.golden b/test/golden/inductive/generating tasks.golden index b312a58..df7fa15 100644 --- a/test/golden/inductive/generating tasks.golden +++ b/test/golden/inductive/generating tasks.golden @@ -323,7 +323,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 3 - , locColumn = 3 + , locColumn = 1 } ) ( SymbolPredicate @@ -383,7 +383,7 @@ , taskLocation = Location { locFile = "test/examples/inductive.tex" , locLine = 31 - , locColumn = 31 + , locColumn = 1 } , taskConjecture = TermSymbol ( Location @@ -754,7 +754,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 3 - , locColumn = 3 + , locColumn = 1 } ) ( SymbolPredicate @@ -814,7 +814,7 @@ , taskLocation = Location { locFile = "test/examples/inductive.tex" , locLine = 31 - , locColumn = 31 + , locColumn = 1 } , taskConjecture = Connected Implication ( Connected Conjunction @@ -1495,7 +1495,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 3 - , locColumn = 3 + , locColumn = 1 } ) ( SymbolPredicate @@ -1575,7 +1575,7 @@ , taskLocation = Location { locFile = "test/examples/inductive.tex" , locLine = 39 - , locColumn = 39 + , locColumn = 1 } , taskConjecture = TermSymbol ( Location @@ -2279,7 +2279,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 3 - , locColumn = 3 + , locColumn = 1 } ) ( SymbolPredicate @@ -2339,7 +2339,7 @@ , taskLocation = Location { locFile = "test/examples/inductive.tex" , locLine = 45 - , locColumn = 45 + , locColumn = 1 } , taskConjecture = Connected Implication ( TermSymbol @@ -3080,7 +3080,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 3 - , locColumn = 3 + , locColumn = 1 } ) ( SymbolPredicate @@ -3140,7 +3140,7 @@ , taskLocation = Location { locFile = "test/examples/inductive.tex" , locLine = 45 - , locColumn = 45 + , locColumn = 1 } , taskConjecture = Connected Implication ( Connected Conjunction @@ -4353,7 +4353,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 3 - , locColumn = 3 + , locColumn = 1 } ) ( SymbolPredicate @@ -4413,7 +4413,7 @@ , taskLocation = Location { locFile = "test/examples/inductive.tex" , locLine = 53 - , locColumn = 53 + , locColumn = 1 } , taskConjecture = Connected Implication ( TermSymbol @@ -5531,7 +5531,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 3 - , locColumn = 3 + , locColumn = 1 } ) ( SymbolPredicate @@ -5591,7 +5591,7 @@ , taskLocation = Location { locFile = "test/examples/inductive.tex" , locLine = 53 - , locColumn = 53 + , locColumn = 1 } , taskConjecture = Connected Implication ( Connected Conjunction @@ -7183,7 +7183,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 3 - , locColumn = 3 + , locColumn = 1 } ) ( SymbolPredicate @@ -7243,7 +7243,7 @@ , taskLocation = Location { locFile = "test/examples/inductive.tex" , locLine = 61 - , locColumn = 61 + , locColumn = 1 } , taskConjecture = Connected Implication ( TermSymbol @@ -8692,7 +8692,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 3 - , locColumn = 3 + , locColumn = 1 } ) ( SymbolPredicate @@ -8752,7 +8752,7 @@ , taskLocation = Location { locFile = "test/examples/inductive.tex" , locLine = 61 - , locColumn = 61 + , locColumn = 1 } , taskConjecture = Connected Implication ( Connected Conjunction @@ -10639,7 +10639,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 3 - , locColumn = 3 + , locColumn = 1 } ) ( SymbolPredicate @@ -10699,7 +10699,7 @@ , taskLocation = Location { locFile = "test/examples/inductive.tex" , locLine = 69 - , locColumn = 69 + , locColumn = 1 } , taskConjecture = Quantified Universally ( Scope @@ -12513,7 +12513,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 3 - , locColumn = 3 + , locColumn = 1 } ) ( SymbolPredicate @@ -12573,7 +12573,7 @@ , taskLocation = Location { locFile = "test/examples/inductive.tex" , locLine = 69 - , locColumn = 69 + , locColumn = 1 } , taskConjecture = Connected Implication ( Connected Conjunction diff --git a/test/golden/inductive/glossing.golden b/test/golden/inductive/glossing.golden index b5b0874..638a333 100644 --- a/test/golden/inductive/glossing.golden +++ b/test/golden/inductive/glossing.golden @@ -2,7 +2,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 3 - , locColumn = 3 + , locColumn = 1 } ) ( Marker "subseteq" ) @@ -36,7 +36,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 7 - , locColumn = 7 + , locColumn = 1 } ) ( Marker "pow" ) @@ -66,7 +66,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 11 - , locColumn = 11 + , locColumn = 1 } ) ( Marker "cons" ) @@ -101,7 +101,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 15 - , locColumn = 15 + , locColumn = 1 } ) ( Marker "times" ) @@ -132,7 +132,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 19 - , locColumn = 19 + , locColumn = 1 } ) ( Marker "fld" ) @@ -162,7 +162,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 23 - , locColumn = 23 + , locColumn = 1 } ) ( Marker "preimg" ) @@ -197,7 +197,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 27 - , locColumn = 27 + , locColumn = 1 } ) ( Marker "lmao" ) @@ -235,7 +235,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 31 - , locColumn = 31 + , locColumn = 1 } ) ( Marker "fin" ) @@ -428,7 +428,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 39 - , locColumn = 39 + , locColumn = 1 } ) ( Marker "fin_mono" ) @@ -510,7 +510,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 45 - , locColumn = 45 + , locColumn = 1 } ) ( Marker "tracl" ) @@ -786,7 +786,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 53 - , locColumn = 53 + , locColumn = 1 } ) ( Marker "quasirefltracl" ) @@ -1099,7 +1099,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 61 - , locColumn = 61 + , locColumn = 1 } ) ( Marker "refltracl" ) @@ -1384,7 +1384,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 69 - , locColumn = 69 + , locColumn = 1 } ) ( Marker "acc" ) diff --git a/test/golden/inductive/parsing.golden b/test/golden/inductive/parsing.golden index 0e7acd7..1690a6b 100644 --- a/test/golden/inductive/parsing.golden +++ b/test/golden/inductive/parsing.golden @@ -2,7 +2,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 3 - , locColumn = 3 + , locColumn = 1 } ) ( Marker "subseteq" ) @@ -16,7 +16,7 @@ { pos = Location { locFile = "test/examples/inductive.tex" , locLine = 4 - , locColumn = 4 + , locColumn = 24 } , formula = FormulaChain ( ChainBase @@ -37,7 +37,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 7 - , locColumn = 7 + , locColumn = 1 } ) ( Marker "pow" ) @@ -61,7 +61,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 11 - , locColumn = 11 + , locColumn = 1 } ) ( Marker "cons" ) @@ -90,7 +90,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 15 - , locColumn = 15 + , locColumn = 1 } ) ( Marker "times" ) @@ -115,7 +115,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 19 - , locColumn = 19 + , locColumn = 1 } ) ( Marker "fld" ) @@ -139,7 +139,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 23 - , locColumn = 23 + , locColumn = 1 } ) ( Marker "preimg" ) @@ -168,7 +168,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 27 - , locColumn = 27 + , locColumn = 1 } ) ( Marker "lmao" ) @@ -177,7 +177,7 @@ { pos = Location { locFile = "test/examples/inductive.tex" , locLine = 28 - , locColumn = 28 + , locColumn = 5 } , formula = FormulaChain ( ChainBase @@ -200,7 +200,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 31 - , locColumn = 31 + , locColumn = 1 } ) ( Marker "fin" ) @@ -324,7 +324,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 39 - , locColumn = 39 + , locColumn = 1 } ) ( Marker "fin_mono" ) @@ -351,7 +351,7 @@ { pos = Location { locFile = "test/examples/inductive.tex" , locLine = 41 - , locColumn = 41 + , locColumn = 13 } , formula = FormulaChain ( ChainBase @@ -372,7 +372,7 @@ { pos = Location { locFile = "test/examples/inductive.tex" , locLine = 42 - , locColumn = 42 + , locColumn = 10 } , formula = FormulaChain ( ChainBase @@ -409,7 +409,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 45 - , locColumn = 45 + , locColumn = 1 } ) ( Marker "tracl" ) @@ -587,7 +587,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 53 - , locColumn = 53 + , locColumn = 1 } ) ( Marker "quasirefltracl" ) @@ -786,7 +786,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 61 - , locColumn = 61 + , locColumn = 1 } ) ( Marker "refltracl" ) @@ -981,7 +981,7 @@ ( Location { locFile = "test/examples/inductive.tex" , locLine = 69 - , locColumn = 69 + , locColumn = 1 } ) ( Marker "acc" ) diff --git a/test/golden/no-reflexive-set/encoding tasks.golden b/test/golden/no-reflexive-set/encoding tasks.golden index 1c4e757..a1a001d 100644 --- a/test/golden/no-reflexive-set/encoding tasks.golden +++ b/test/golden/no-reflexive-set/encoding tasks.golden @@ -1,2 +1,2 @@ -fof(in_irrefl,conjecture,~elem(fA,fA),"test/examples/no-reflexive-set.tex 10:10"). +fof(in_irrefl,conjecture,~elem(fA,fA),"test/examples/no-reflexive-set.tex 10:5"). fof(in_irrefl1,axiom,![XIndAntecedent]:(elem(XIndAntecedent,fA)=>~elem(XIndAntecedent,XIndAntecedent))).
\ No newline at end of file diff --git a/test/golden/no-reflexive-set/generating tasks.golden b/test/golden/no-reflexive-set/generating tasks.golden index a1fcaac..9cb9636 100644 --- a/test/golden/no-reflexive-set/generating tasks.golden +++ b/test/golden/no-reflexive-set/generating tasks.golden @@ -68,7 +68,7 @@ , taskLocation = Location { locFile = "test/examples/no-reflexive-set.tex" , locLine = 10 - , locColumn = 10 + , locColumn = 5 } , taskConjecture = Not ( Location diff --git a/test/golden/no-reflexive-set/glossing.golden b/test/golden/no-reflexive-set/glossing.golden index 67d4e4d..fc60015 100644 --- a/test/golden/no-reflexive-set/glossing.golden +++ b/test/golden/no-reflexive-set/glossing.golden @@ -48,14 +48,14 @@ ( Location { locFile = "test/examples/no-reflexive-set.tex" , locLine = 4 - , locColumn = 4 + , locColumn = 1 } ) ( BySetInduction ( Location { locFile = "test/examples/no-reflexive-set.tex" , locLine = 4 - , locColumn = 4 + , locColumn = 21 } ) Nothing ( Qed @@ -63,7 +63,7 @@ ( Location { locFile = "test/examples/no-reflexive-set.tex" , locLine = 10 - , locColumn = 10 + , locColumn = 5 } ) , by = JustificationEmpty diff --git a/test/golden/no-reflexive-set/parsing.golden b/test/golden/no-reflexive-set/parsing.golden index 7ad4f12..b529ae8 100644 --- a/test/golden/no-reflexive-set/parsing.golden +++ b/test/golden/no-reflexive-set/parsing.golden @@ -11,7 +11,7 @@ { pos = Location { locFile = "test/examples/no-reflexive-set.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 5 } , qp = QuantPhrase Universally NounPhrase ( [] ) ( Noun @@ -34,7 +34,7 @@ { pos = Location { locFile = "test/examples/no-reflexive-set.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 30 } , formula = FormulaChain ( ChainBase @@ -56,14 +56,14 @@ ( Location { locFile = "test/examples/no-reflexive-set.tex" , locLine = 4 - , locColumn = 4 + , locColumn = 1 } ) ( BySetInduction ( Location { locFile = "test/examples/no-reflexive-set.tex" , locLine = 4 - , locColumn = 4 + , locColumn = 21 } ) Nothing ( Qed @@ -71,7 +71,7 @@ ( Location { locFile = "test/examples/no-reflexive-set.tex" , locLine = 10 - , locColumn = 10 + , locColumn = 5 } ) ) JustificationEmpty diff --git a/test/golden/proofassume/encoding tasks.golden b/test/golden/proofassume/encoding tasks.golden index d5775b7..16c4a45 100644 --- a/test/golden/proofassume/encoding tasks.golden +++ b/test/golden/proofassume/encoding tasks.golden @@ -1,16 +1,16 @@ -fof(assumetest,conjecture,elem(fx,fy),"test/examples/proofassume.tex 6:6"). +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:6"). +fof(assumetest,conjecture,elem(fx,fy),"test/examples/proofassume.tex 6:5"). fof(assumetest1,axiom,elem(fx,fy)). fof(assumetest2,axiom,elem(fx,fy)). ------------------ -fof(assumetesttwo,conjecture,elem(fx,fy),"test/examples/proofassume.tex 15:15"). +fof(assumetesttwo,conjecture,elem(fx,fy),"test/examples/proofassume.tex 15:5"). 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:15"). +fof(assumetesttwo,conjecture,elem(fx,fy),"test/examples/proofassume.tex 15:5"). 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 8b2db53..9098694 100644 --- a/test/golden/proofassume/generating tasks.golden +++ b/test/golden/proofassume/generating tasks.golden @@ -26,7 +26,7 @@ , taskLocation = Location { locFile = "test/examples/proofassume.tex" , locLine = 6 - , locColumn = 6 + , locColumn = 5 } , taskConjecture = TermSymbol ( Location @@ -94,7 +94,7 @@ , taskLocation = Location { locFile = "test/examples/proofassume.tex" , locLine = 6 - , locColumn = 6 + , locColumn = 5 } , taskConjecture = TermSymbol ( Location @@ -214,7 +214,7 @@ , taskLocation = Location { locFile = "test/examples/proofassume.tex" , locLine = 15 - , locColumn = 15 + , locColumn = 5 } , taskConjecture = TermSymbol ( Location @@ -354,7 +354,7 @@ , taskLocation = Location { locFile = "test/examples/proofassume.tex" , locLine = 15 - , locColumn = 15 + , locColumn = 5 } , taskConjecture = TermSymbol ( Location diff --git a/test/golden/proofassume/glossing.golden b/test/golden/proofassume/glossing.golden index a8e23f4..7ce9761 100644 --- a/test/golden/proofassume/glossing.golden +++ b/test/golden/proofassume/glossing.golden @@ -50,7 +50,7 @@ ( Location { locFile = "test/examples/proofassume.tex" , locLine = 4 - , locColumn = 4 + , locColumn = 1 } ) ( Assume @@ -82,7 +82,7 @@ ( Location { locFile = "test/examples/proofassume.tex" , locLine = 6 - , locColumn = 6 + , locColumn = 5 } ) ( TermSymbol @@ -114,7 +114,7 @@ ( Location { locFile = "test/examples/proofassume.tex" , locLine = 9 - , locColumn = 9 + , locColumn = 1 } ) ( Marker "assumetesttwo" ) @@ -182,14 +182,14 @@ ( Location { locFile = "test/examples/proofassume.tex" , locLine = 12 - , locColumn = 12 + , locColumn = 1 } ) ( Assume ( Location { locFile = "test/examples/proofassume.tex" , locLine = 13 - , locColumn = 13 + , locColumn = 5 } ) ( TermSymbol @@ -214,7 +214,7 @@ ( Location { locFile = "test/examples/proofassume.tex" , locLine = 14 - , locColumn = 14 + , locColumn = 5 } ) ( TermSymbol @@ -239,7 +239,7 @@ ( Location { locFile = "test/examples/proofassume.tex" , locLine = 15 - , locColumn = 15 + , locColumn = 5 } ) ( TermSymbol diff --git a/test/golden/proofassume/parsing.golden b/test/golden/proofassume/parsing.golden index 65c07bc..1b7837f 100644 --- a/test/golden/proofassume/parsing.golden +++ b/test/golden/proofassume/parsing.golden @@ -13,14 +13,14 @@ ( Location { locFile = "test/examples/proofassume.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 5 } ) , stmt1 = StmtFormula { pos = Location { locFile = "test/examples/proofassume.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 8 } , formula = FormulaChain ( ChainBase @@ -39,7 +39,7 @@ { pos = Location { locFile = "test/examples/proofassume.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 23 } , formula = FormulaChain ( ChainBase @@ -61,7 +61,7 @@ ( Location { locFile = "test/examples/proofassume.tex" , locLine = 4 - , locColumn = 4 + , locColumn = 1 } ) ( Assume @@ -75,7 +75,7 @@ { pos = Location { locFile = "test/examples/proofassume.tex" , locLine = 5 - , locColumn = 5 + , locColumn = 12 } , formula = FormulaChain ( ChainBase @@ -95,14 +95,14 @@ ( Location { locFile = "test/examples/proofassume.tex" , locLine = 6 - , locColumn = 6 + , locColumn = 5 } ) Nothing ( StmtFormula { pos = Location { locFile = "test/examples/proofassume.tex" , locLine = 6 - , locColumn = 6 + , locColumn = 10 } , formula = FormulaChain ( ChainBase @@ -124,7 +124,7 @@ ( Location { locFile = "test/examples/proofassume.tex" , locLine = 9 - , locColumn = 9 + , locColumn = 1 } ) ( Marker "assumetesttwo" ) @@ -135,7 +135,7 @@ ( Location { locFile = "test/examples/proofassume.tex" , locLine = 10 - , locColumn = 10 + , locColumn = 5 } ) , stmt1 = StmtConnected @@ -145,7 +145,7 @@ { pos = Location { locFile = "test/examples/proofassume.tex" , locLine = 10 - , locColumn = 10 + , locColumn = 8 } , formula = FormulaChain ( ChainBase @@ -164,7 +164,7 @@ { pos = Location { locFile = "test/examples/proofassume.tex" , locLine = 10 - , locColumn = 10 + , locColumn = 21 } , formula = FormulaChain ( ChainBase @@ -184,7 +184,7 @@ { pos = Location { locFile = "test/examples/proofassume.tex" , locLine = 10 - , locColumn = 10 + , locColumn = 36 } , formula = FormulaChain ( ChainBase @@ -206,21 +206,21 @@ ( Location { locFile = "test/examples/proofassume.tex" , locLine = 12 - , locColumn = 12 + , locColumn = 1 } ) ( Assume ( Location { locFile = "test/examples/proofassume.tex" , locLine = 13 - , locColumn = 13 + , locColumn = 5 } ) ( StmtFormula { pos = Location { locFile = "test/examples/proofassume.tex" , locLine = 13 - , locColumn = 13 + , locColumn = 12 } , formula = FormulaChain ( ChainBase @@ -240,14 +240,14 @@ ( Location { locFile = "test/examples/proofassume.tex" , locLine = 14 - , locColumn = 14 + , locColumn = 5 } ) ( StmtFormula { pos = Location { locFile = "test/examples/proofassume.tex" , locLine = 14 - , locColumn = 14 + , locColumn = 12 } , formula = FormulaChain ( ChainBase @@ -267,14 +267,14 @@ ( Location { locFile = "test/examples/proofassume.tex" , locLine = 15 - , locColumn = 15 + , locColumn = 5 } ) Nothing ( StmtFormula { pos = Location { locFile = "test/examples/proofassume.tex" , locLine = 15 - , locColumn = 15 + , locColumn = 10 } , formula = FormulaChain ( ChainBase diff --git a/test/golden/proofdefinefunction/encoding tasks.golden b/test/golden/proofdefinefunction/encoding tasks.golden index 2a885c8..1f1de12 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:26"). +fof(definefunctiontest,conjecture,elem(fx,fy)=>elem(fx,fy),"test/examples/proofdefinefunction.tex 26:5"). 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 e18eeaa..32276cc 100644 --- a/test/golden/proofdefinefunction/generating tasks.golden +++ b/test/golden/proofdefinefunction/generating tasks.golden @@ -10,7 +10,7 @@ ( Location { locFile = "test/examples/proofdefinefunction.tex" , locLine = 18 - , locColumn = 18 + , locColumn = 1 } ) ( SymbolPredicate @@ -80,7 +80,7 @@ ( Location { locFile = "test/examples/proofdefinefunction.tex" , locLine = 13 - , locColumn = 13 + , locColumn = 1 } ) ( SymbolPredicate @@ -234,7 +234,7 @@ ( Location { locFile = "test/examples/proofdefinefunction.tex" , locLine = 26 - , locColumn = 26 + , locColumn = 5 } ) ( SymbolPredicate @@ -262,7 +262,7 @@ ( Location { locFile = "test/examples/proofdefinefunction.tex" , locLine = 26 - , locColumn = 26 + , locColumn = 5 } ) ( SymbolPredicate @@ -361,7 +361,7 @@ ( Location { locFile = "test/examples/proofdefinefunction.tex" , locLine = 26 - , locColumn = 26 + , locColumn = 5 } ) ( SymbolPredicate @@ -396,7 +396,7 @@ , taskLocation = Location { locFile = "test/examples/proofdefinefunction.tex" , locLine = 26 - , locColumn = 26 + , locColumn = 5 } , taskConjecture = Connected Implication ( TermSymbol diff --git a/test/golden/proofdefinefunction/glossing.golden b/test/golden/proofdefinefunction/glossing.golden index e3e8181..4886067 100644 --- a/test/golden/proofdefinefunction/glossing.golden +++ b/test/golden/proofdefinefunction/glossing.golden @@ -2,7 +2,7 @@ ( Location { locFile = "test/examples/proofdefinefunction.tex" , locLine = 3 - , locColumn = 3 + , locColumn = 1 } ) ( Marker "apply" ) @@ -27,7 +27,7 @@ ( Location { locFile = "test/examples/proofdefinefunction.tex" , locLine = 8 - , locColumn = 8 + , locColumn = 1 } ) ( Marker "dom" ) @@ -47,7 +47,7 @@ ( Location { locFile = "test/examples/proofdefinefunction.tex" , locLine = 13 - , locColumn = 13 + , locColumn = 1 } ) ( Marker "rightunique" ) @@ -81,7 +81,7 @@ ( Location { locFile = "test/examples/proofdefinefunction.tex" , locLine = 18 - , locColumn = 18 + , locColumn = 1 } ) ( Marker "relation" ) @@ -123,7 +123,7 @@ ( Location { locFile = "test/examples/proofdefinefunction.tex" , locLine = 22 - , locColumn = 22 + , locColumn = 1 } ) ( Marker "definefunctiontest" ) @@ -171,14 +171,14 @@ ( Location { locFile = "test/examples/proofdefinefunction.tex" , locLine = 25 - , locColumn = 25 + , locColumn = 1 } ) ( DefineFunction ( Location { locFile = "test/examples/proofdefinefunction.tex" , locLine = 26 - , locColumn = 26 + , locColumn = 5 } ) ( NamedVar "f" ) diff --git a/test/golden/proofdefinefunction/parsing.golden b/test/golden/proofdefinefunction/parsing.golden index ed1f2ed..de3f9a8 100644 --- a/test/golden/proofdefinefunction/parsing.golden +++ b/test/golden/proofdefinefunction/parsing.golden @@ -2,7 +2,7 @@ ( Location { locFile = "test/examples/proofdefinefunction.tex" , locLine = 3 - , locColumn = 3 + , locColumn = 1 } ) ( Marker "apply" ) @@ -29,7 +29,7 @@ ( Location { locFile = "test/examples/proofdefinefunction.tex" , locLine = 8 - , locColumn = 8 + , locColumn = 1 } ) ( Marker "dom" ) @@ -51,7 +51,7 @@ ( Location { locFile = "test/examples/proofdefinefunction.tex" , locLine = 13 - , locColumn = 13 + , locColumn = 1 } ) ( Marker "rightunique" ) @@ -62,7 +62,7 @@ ( Location { locFile = "test/examples/proofdefinefunction.tex" , locLine = 14 - , locColumn = 14 + , locColumn = 12 } ) [ Just @@ -74,7 +74,7 @@ { pos = Location { locFile = "test/examples/proofdefinefunction.tex" , locLine = 14 - , locColumn = 14 + , locColumn = 29 } , formula = FormulaChain ( ChainBase @@ -95,7 +95,7 @@ ( Location { locFile = "test/examples/proofdefinefunction.tex" , locLine = 18 - , locColumn = 18 + , locColumn = 1 } ) ( Marker "relation" ) @@ -120,7 +120,7 @@ { pos = Location { locFile = "test/examples/proofdefinefunction.tex" , locLine = 19 - , locColumn = 19 + , locColumn = 27 } , formula = FormulaChain ( ChainBase @@ -141,7 +141,7 @@ ( Location { locFile = "test/examples/proofdefinefunction.tex" , locLine = 22 - , locColumn = 22 + , locColumn = 1 } ) ( Marker "definefunctiontest" ) @@ -152,14 +152,14 @@ ( Location { locFile = "test/examples/proofdefinefunction.tex" , locLine = 23 - , locColumn = 23 + , locColumn = 5 } ) , stmt1 = StmtFormula { pos = Location { locFile = "test/examples/proofdefinefunction.tex" , locLine = 23 - , locColumn = 23 + , locColumn = 8 } , formula = FormulaChain ( ChainBase @@ -200,14 +200,14 @@ ( Location { locFile = "test/examples/proofdefinefunction.tex" , locLine = 25 - , locColumn = 25 + , locColumn = 1 } ) ( DefineFunction ( Location { locFile = "test/examples/proofdefinefunction.tex" , locLine = 26 - , locColumn = 26 + , locColumn = 5 } ) ( NamedVar "f" ) diff --git a/test/golden/prooffix/encoding tasks.golden b/test/golden/prooffix/encoding tasks.golden index be0943b..0e35e38 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:6"). +fof(assumetest,conjecture,fx=fx,"test/examples/prooffix.tex 6:5"). ------------------ -fof(assumetest,conjecture,fx=fx,"test/examples/prooffix.tex 6:6"). +fof(assumetest,conjecture,fx=fx,"test/examples/prooffix.tex 6:5"). 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 12d6a42..f3a50df 100644 --- a/test/golden/prooffix/generating tasks.golden +++ b/test/golden/prooffix/generating tasks.golden @@ -5,7 +5,7 @@ , taskLocation = Location { locFile = "test/examples/prooffix.tex" , locLine = 6 - , locColumn = 6 + , locColumn = 5 } , taskConjecture = TermSymbol ( Location @@ -53,7 +53,7 @@ , taskLocation = Location { locFile = "test/examples/prooffix.tex" , locLine = 6 - , locColumn = 6 + , locColumn = 5 } , taskConjecture = TermSymbol ( Location diff --git a/test/golden/prooffix/glossing.golden b/test/golden/prooffix/glossing.golden index 177abd6..104de4f 100644 --- a/test/golden/prooffix/glossing.golden +++ b/test/golden/prooffix/glossing.golden @@ -38,7 +38,7 @@ ( Location { locFile = "test/examples/prooffix.tex" , locLine = 4 - , locColumn = 4 + , locColumn = 1 } ) ( Fix @@ -53,7 +53,7 @@ ( Location { locFile = "test/examples/prooffix.tex" , locLine = 6 - , locColumn = 6 + , locColumn = 5 } ) ( TermSymbol diff --git a/test/golden/prooffix/parsing.golden b/test/golden/prooffix/parsing.golden index 52a0b62..2d0daca 100644 --- a/test/golden/prooffix/parsing.golden +++ b/test/golden/prooffix/parsing.golden @@ -11,7 +11,7 @@ { pos = Location { locFile = "test/examples/prooffix.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 5 } , quant = Universally , xs = NamedVar "x" :| [] @@ -21,7 +21,7 @@ { pos = Location { locFile = "test/examples/prooffix.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 25 } , formula = FormulaChain ( ChainBase @@ -43,7 +43,7 @@ ( Location { locFile = "test/examples/prooffix.tex" , locLine = 4 - , locColumn = 4 + , locColumn = 1 } ) ( FixSymbolic @@ -58,14 +58,14 @@ ( Location { locFile = "test/examples/prooffix.tex" , locLine = 6 - , locColumn = 6 + , locColumn = 5 } ) Nothing ( StmtFormula { pos = Location { locFile = "test/examples/prooffix.tex" , locLine = 6 - , locColumn = 6 + , locColumn = 10 } , formula = FormulaChain ( ChainBase diff --git a/test/golden/relation-notation/parsing.golden b/test/golden/relation-notation/parsing.golden index e28fa2c..1693f6d 100644 --- a/test/golden/relation-notation/parsing.golden +++ b/test/golden/relation-notation/parsing.golden @@ -13,14 +13,14 @@ ( Location { locFile = "test/examples/relation-notation.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 5 } ) , stmt1 = StmtFormula { pos = Location { locFile = "test/examples/relation-notation.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 8 } , formula = FormulaChain ( ChainBase @@ -41,7 +41,7 @@ { pos = Location { locFile = "test/examples/relation-notation.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 31 } , formula = FormulaChain ( ChainBase diff --git a/test/golden/relparam/encoding tasks.golden b/test/golden/relparam/encoding tasks.golden index 10f1e81..c75daf4 100644 --- a/test/golden/relparam/encoding tasks.golden +++ b/test/golden/relparam/encoding tasks.golden @@ -1,4 +1,4 @@ -fof(dummy_abbr_test,conjecture,![Xx]:Xx=Xx,"test/examples/relparam.tex 6:6"). +fof(dummy_abbr_test,conjecture,![Xx]:Xx=Xx,"test/examples/relparam.tex 6:1"). ------------------ -fof(dummy_defn_test,conjecture,![Xx]:Xx=Xx,"test/examples/relparam.tex 15:15"). +fof(dummy_defn_test,conjecture,![Xx]:Xx=Xx,"test/examples/relparam.tex 15:1"). fof(dummy_abbr_test,axiom,![Xx]:Xx=Xx).
\ No newline at end of file diff --git a/test/golden/relparam/generating tasks.golden b/test/golden/relparam/generating tasks.golden index b2610b7..7342487 100644 --- a/test/golden/relparam/generating tasks.golden +++ b/test/golden/relparam/generating tasks.golden @@ -5,7 +5,7 @@ , taskLocation = Location { locFile = "test/examples/relparam.tex" , locLine = 6 - , locColumn = 6 + , locColumn = 1 } , taskConjecture = Quantified Universally ( Scope @@ -69,7 +69,7 @@ , taskLocation = Location { locFile = "test/examples/relparam.tex" , locLine = 15 - , locColumn = 15 + , locColumn = 1 } , taskConjecture = Quantified Universally ( Scope diff --git a/test/golden/relparam/glossing.golden b/test/golden/relparam/glossing.golden index 349e54c..fcc1d05 100644 --- a/test/golden/relparam/glossing.golden +++ b/test/golden/relparam/glossing.golden @@ -2,7 +2,7 @@ ( Location { locFile = "test/examples/relparam.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 1 } ) ( Marker "abbr_equal" ) @@ -37,7 +37,7 @@ ( Location { locFile = "test/examples/relparam.tex" , locLine = 6 - , locColumn = 6 + , locColumn = 1 } ) ( Marker "dummy_abbr_test" ) @@ -79,7 +79,7 @@ ( Location { locFile = "test/examples/relparam.tex" , locLine = 11 - , locColumn = 11 + , locColumn = 1 } ) ( Marker "defn_equals" ) @@ -114,7 +114,7 @@ ( Location { locFile = "test/examples/relparam.tex" , locLine = 15 - , locColumn = 15 + , locColumn = 1 } ) ( Marker "dummy_defn_test" ) diff --git a/test/golden/relparam/parsing.golden b/test/golden/relparam/parsing.golden index efab8d7..d4bacbd 100644 --- a/test/golden/relparam/parsing.golden +++ b/test/golden/relparam/parsing.golden @@ -2,7 +2,7 @@ ( Location { locFile = "test/examples/relparam.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 1 } ) ( Marker "abbr_equal" ) @@ -15,7 +15,7 @@ { pos = Location { locFile = "test/examples/relparam.tex" , locLine = 3 - , locColumn = 3 + , locColumn = 24 } , formula = FormulaChain ( ChainBase @@ -36,7 +36,7 @@ ( Location { locFile = "test/examples/relparam.tex" , locLine = 6 - , locColumn = 6 + , locColumn = 1 } ) ( Marker "dummy_abbr_test" ) @@ -45,7 +45,7 @@ { pos = Location { locFile = "test/examples/relparam.tex" , locLine = 7 - , locColumn = 7 + , locColumn = 5 } , quant = Universally , xs = NamedVar "x" :| [] @@ -55,7 +55,7 @@ { pos = Location { locFile = "test/examples/relparam.tex" , locLine = 7 - , locColumn = 7 + , locColumn = 25 } , formula = FormulaChain ( ChainBase @@ -80,7 +80,7 @@ ( Location { locFile = "test/examples/relparam.tex" , locLine = 11 - , locColumn = 11 + , locColumn = 1 } ) ( Marker "defn_equals" ) @@ -93,7 +93,7 @@ { pos = Location { locFile = "test/examples/relparam.tex" , locLine = 12 - , locColumn = 12 + , locColumn = 25 } , formula = FormulaChain ( ChainBase @@ -114,7 +114,7 @@ ( Location { locFile = "test/examples/relparam.tex" , locLine = 15 - , locColumn = 15 + , locColumn = 1 } ) ( Marker "dummy_defn_test" ) @@ -123,7 +123,7 @@ { pos = Location { locFile = "test/examples/relparam.tex" , locLine = 16 - , locColumn = 16 + , locColumn = 5 } , quant = Universally , xs = NamedVar "x" :| [] @@ -133,7 +133,7 @@ { pos = Location { locFile = "test/examples/relparam.tex" , locLine = 16 - , locColumn = 16 + , locColumn = 25 } , formula = FormulaChain ( ChainBase diff --git a/test/golden/replace/encoding tasks.golden b/test/golden/replace/encoding tasks.golden index aabe60b..6bca2ea 100644 --- a/test/golden/replace/encoding tasks.golden +++ b/test/golden/replace/encoding tasks.golden @@ -1,15 +1,15 @@ -fof(pair_emptyset_in_times_unit,conjecture,elem(pair(emptyset,emptyset),times(unit,unit)),"test/examples/replace.tex 13:13"). +fof(pair_emptyset_in_times_unit,conjecture,elem(pair(emptyset,emptyset),times(unit,unit)),"test/examples/replace.tex 13:1"). fof(unit,axiom,![Xany]:(elem(Xany,unit)<=>(elem(Xany,emptyset)|Xany=emptyset))). fof(times,axiom,![XA,XB]:![Xfrv]:(elem(Xfrv,times(XA,XB))<=>?[Xa,Xb]:(elem(Xa,XA)&elem(Xb,XB)&pair(Xa,Xb)=Xfrv))). fof(cons,axiom,![Xx,Xy,XX]:(elem(Xx,cons(Xy,XX))<=>(Xx=Xy|elem(Xx,XX)))). ------------------ -fof(suc,conjecture,![X0]:(elem(X0,fa)=>![X1,X2]:((X1=cons(X0,emptyset)&X2=cons(X0,emptyset))=>X1=X2)),"test/examples/replace.tex 19:19"). +fof(suc,conjecture,![X0]:(elem(X0,fa)=>![X1,X2]:((X1=cons(X0,emptyset)&X2=cons(X0,emptyset))=>X1=X2)),"test/examples/replace.tex 19:1"). fof(pair_emptyset_in_times_unit,axiom,elem(pair(emptyset,emptyset),times(unit,unit))). fof(unit,axiom,![Xany]:(elem(Xany,unit)<=>(elem(Xany,emptyset)|Xany=emptyset))). fof(times,axiom,![XA,XB]:![Xfrv]:(elem(Xfrv,times(XA,XB))<=>?[Xa,Xb]:(elem(Xa,XA)&elem(Xb,XB)&pair(Xa,Xb)=Xfrv))). fof(cons,axiom,![Xx,Xy,XX]:(elem(Xx,cons(Xy,XX))<=>(Xx=Xy|elem(Xx,XX)))). ------------------ -fof(times_replacement_test,conjecture,![Xfrv]:(elem(Xfrv,times(fA,fB))<=>?[Xa,Xb]:(elem(Xa,fA)&elem(Xb,fB)&pair(Xa,Xb)=Xfrv)),"test/examples/replace.tex 25:25"). +fof(times_replacement_test,conjecture,![Xfrv]:(elem(Xfrv,times(fA,fB))<=>?[Xa,Xb]:(elem(Xa,fA)&elem(Xb,fB)&pair(Xa,Xb)=Xfrv)),"test/examples/replace.tex 25:1"). fof(suc,axiom,![X1,Xa]:(elem(X1,suc(Xa))<=>?[X0]:(elem(X0,Xa)&X1=cons(X0,emptyset)))). fof(pair_emptyset_in_times_unit,axiom,elem(pair(emptyset,emptyset),times(unit,unit))). fof(unit,axiom,![Xany]:(elem(Xany,unit)<=>(elem(Xany,emptyset)|Xany=emptyset))). diff --git a/test/golden/replace/generating tasks.golden b/test/golden/replace/generating tasks.golden index 85b3ead..2fb7035 100644 --- a/test/golden/replace/generating tasks.golden +++ b/test/golden/replace/generating tasks.golden @@ -26,7 +26,7 @@ ( Location { locFile = "test/examples/replace.tex" , locLine = 9 - , locColumn = 9 + , locColumn = 1 } ) ( SymbolMixfix @@ -71,7 +71,7 @@ ( Location { locFile = "test/examples/replace.tex" , locLine = 9 - , locColumn = 9 + , locColumn = 1 } ) ( SymbolPredicate @@ -383,7 +383,7 @@ , taskLocation = Location { locFile = "test/examples/replace.tex" , locLine = 13 - , locColumn = 13 + , locColumn = 1 } , taskConjecture = TermSymbol ( Location @@ -607,7 +607,7 @@ ( Location { locFile = "test/examples/replace.tex" , locLine = 9 - , locColumn = 9 + , locColumn = 1 } ) ( SymbolMixfix @@ -652,7 +652,7 @@ ( Location { locFile = "test/examples/replace.tex" , locLine = 9 - , locColumn = 9 + , locColumn = 1 } ) ( SymbolPredicate @@ -964,7 +964,7 @@ , taskLocation = Location { locFile = "test/examples/replace.tex" , locLine = 19 - , locColumn = 19 + , locColumn = 1 } , taskConjecture = Quantified Universally ( Scope @@ -1401,7 +1401,7 @@ ( Location { locFile = "test/examples/replace.tex" , locLine = 9 - , locColumn = 9 + , locColumn = 1 } ) ( SymbolMixfix @@ -1446,7 +1446,7 @@ ( Location { locFile = "test/examples/replace.tex" , locLine = 9 - , locColumn = 9 + , locColumn = 1 } ) ( SymbolPredicate @@ -1758,7 +1758,7 @@ , taskLocation = Location { locFile = "test/examples/replace.tex" , locLine = 25 - , locColumn = 25 + , locColumn = 1 } , taskConjecture = Quantified Universally ( Scope diff --git a/test/golden/replace/glossing.golden b/test/golden/replace/glossing.golden index 5825e0e..c0999c9 100644 --- a/test/golden/replace/glossing.golden +++ b/test/golden/replace/glossing.golden @@ -91,7 +91,7 @@ ( Location { locFile = "test/examples/replace.tex" , locLine = 5 - , locColumn = 5 + , locColumn = 1 } ) ( Marker "times" ) @@ -154,7 +154,7 @@ ( Location { locFile = "test/examples/replace.tex" , locLine = 9 - , locColumn = 9 + , locColumn = 1 } ) ( Marker "unit" ) @@ -211,7 +211,7 @@ ( Location { locFile = "test/examples/replace.tex" , locLine = 13 - , locColumn = 13 + , locColumn = 1 } ) ( Marker "pair_emptyset_in_times_unit" ) @@ -317,7 +317,7 @@ ( Location { locFile = "test/examples/replace.tex" , locLine = 19 - , locColumn = 19 + , locColumn = 1 } ) ( Marker "suc" ) @@ -390,7 +390,7 @@ ( Location { locFile = "test/examples/replace.tex" , locLine = 25 - , locColumn = 25 + , locColumn = 1 } ) ( Marker "times_replacement_test" ) diff --git a/test/golden/replace/parsing.golden b/test/golden/replace/parsing.golden index 5be5a51..4d919e4 100644 --- a/test/golden/replace/parsing.golden +++ b/test/golden/replace/parsing.golden @@ -14,7 +14,7 @@ { pos = Location { locFile = "test/examples/replace.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 5 } , formula = FormulaChain ( ChainBase @@ -49,7 +49,7 @@ { pos = Location { locFile = "test/examples/replace.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 28 } , formula = FormulaChain ( ChainBase @@ -68,7 +68,7 @@ { pos = Location { locFile = "test/examples/replace.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 39 } , formula = FormulaChain ( ChainBase @@ -91,7 +91,7 @@ ( Location { locFile = "test/examples/replace.tex" , locLine = 5 - , locColumn = 5 + , locColumn = 1 } ) ( Marker "times" ) @@ -141,7 +141,7 @@ ( Location { locFile = "test/examples/replace.tex" , locLine = 9 - , locColumn = 9 + , locColumn = 1 } ) ( Marker "unit" ) @@ -163,7 +163,7 @@ ( Location { locFile = "test/examples/replace.tex" , locLine = 13 - , locColumn = 13 + , locColumn = 1 } ) ( Marker "pair_emptyset_in_times_unit" ) @@ -172,7 +172,7 @@ { pos = Location { locFile = "test/examples/replace.tex" , locLine = 14 - , locColumn = 14 + , locColumn = 5 } , formula = FormulaChain ( ChainBase @@ -223,7 +223,7 @@ ( Location { locFile = "test/examples/replace.tex" , locLine = 19 - , locColumn = 19 + , locColumn = 1 } ) ( Marker "suc" ) @@ -271,7 +271,7 @@ ( Location { locFile = "test/examples/replace.tex" , locLine = 25 - , locColumn = 25 + , locColumn = 1 } ) ( Marker "times_replacement_test" ) @@ -280,7 +280,7 @@ { pos = Location { locFile = "test/examples/replace.tex" , locLine = 26 - , locColumn = 26 + , locColumn = 5 } , formula = FormulaChain ( ChainBase diff --git a/test/golden/russell/encoding tasks.golden b/test/golden/russell/encoding tasks.golden index 69a8891..f1a3d5c 100644 --- a/test/golden/russell/encoding tasks.golden +++ b/test/golden/russell/encoding tasks.golden @@ -1,21 +1,21 @@ -fof(no_universal_set,conjecture,?[XV]:universal_set(XV),"test/examples/russell.tex 12:12"). +fof(no_universal_set,conjecture,?[XV]:universal_set(XV),"test/examples/russell.tex 12:5"). fof(universal_set,axiom,![XV]:(universal_set(XV)<=>![Xx]:elem(Xx,XV))). fof(no_universal_set1,axiom,~~?[X0]:universal_set(X0)). ------------------ -fof(no_universal_set,conjecture,elem(fR,fR)<=>~elem(fR,fR),"test/examples/russell.tex 14:14"). +fof(no_universal_set,conjecture,elem(fR,fR)<=>~elem(fR,fR),"test/examples/russell.tex 14:5"). fof(universal_set,axiom,![XV]:(universal_set(XV)<=>![Xx]:elem(Xx,XV))). fof(no_universal_set1,axiom,![Xx]:(elem(Xx,fR)<=>(elem(Xx,fV)&~elem(Xx,Xx)))). fof(no_universal_set2,axiom,universal_set(fV)). fof(no_universal_set3,axiom,~~?[X0]:universal_set(X0)). ------------------ -fof(no_universal_set,conjecture,$false,"test/examples/russell.tex 15:15"). +fof(no_universal_set,conjecture,$false,"test/examples/russell.tex 15:5"). fof(universal_set,axiom,![XV]:(universal_set(XV)<=>![Xx]:elem(Xx,XV))). fof(no_universal_set1,axiom,elem(fR,fR)<=>~elem(fR,fR)). 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:15"). +fof(no_universal_set,conjecture,$false,"test/examples/russell.tex 15:5"). 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 e02b945..7c3b0a7 100644 --- a/test/golden/russell/generating tasks.golden +++ b/test/golden/russell/generating tasks.golden @@ -4,7 +4,7 @@ ( Location { locFile = "test/examples/russell.tex" , locLine = 8 - , locColumn = 8 + , locColumn = 18 } ) ( Quantified Existentially @@ -14,7 +14,7 @@ ( Location { locFile = "test/examples/russell.tex" , locLine = 8 - , locColumn = 8 + , locColumn = 21 } ) ( SymbolPredicate @@ -107,14 +107,14 @@ ( Location { locFile = "test/examples/russell.tex" , locLine = 11 - , locColumn = 11 + , locColumn = 5 } ) ( Not ( Location { locFile = "test/examples/russell.tex" , locLine = 8 - , locColumn = 8 + , locColumn = 18 } ) ( Quantified Existentially @@ -123,7 +123,7 @@ ( Location { locFile = "test/examples/russell.tex" , locLine = 8 - , locColumn = 8 + , locColumn = 21 } ) ( SymbolPredicate @@ -148,7 +148,7 @@ , taskLocation = Location { locFile = "test/examples/russell.tex" , locLine = 12 - , locColumn = 12 + , locColumn = 5 } , taskConjecture = Quantified Existentially ( Scope @@ -180,7 +180,7 @@ ( Location { locFile = "test/examples/russell.tex" , locLine = 8 - , locColumn = 8 + , locColumn = 18 } ) ( Quantified Existentially @@ -190,7 +190,7 @@ ( Location { locFile = "test/examples/russell.tex" , locLine = 8 - , locColumn = 8 + , locColumn = 21 } ) ( SymbolPredicate @@ -391,14 +391,14 @@ ( Location { locFile = "test/examples/russell.tex" , locLine = 11 - , locColumn = 11 + , locColumn = 5 } ) ( Not ( Location { locFile = "test/examples/russell.tex" , locLine = 8 - , locColumn = 8 + , locColumn = 18 } ) ( Quantified Existentially @@ -407,7 +407,7 @@ ( Location { locFile = "test/examples/russell.tex" , locLine = 8 - , locColumn = 8 + , locColumn = 21 } ) ( SymbolPredicate @@ -432,7 +432,7 @@ , taskLocation = Location { locFile = "test/examples/russell.tex" , locLine = 14 - , locColumn = 14 + , locColumn = 5 } , taskConjecture = Connected Equivalence ( TermSymbol @@ -486,7 +486,7 @@ ( Location { locFile = "test/examples/russell.tex" , locLine = 8 - , locColumn = 8 + , locColumn = 18 } ) ( Quantified Existentially @@ -496,7 +496,7 @@ ( Location { locFile = "test/examples/russell.tex" , locLine = 8 - , locColumn = 8 + , locColumn = 21 } ) ( SymbolPredicate @@ -745,14 +745,14 @@ ( Location { locFile = "test/examples/russell.tex" , locLine = 11 - , locColumn = 11 + , locColumn = 5 } ) ( Not ( Location { locFile = "test/examples/russell.tex" , locLine = 8 - , locColumn = 8 + , locColumn = 18 } ) ( Quantified Existentially @@ -761,7 +761,7 @@ ( Location { locFile = "test/examples/russell.tex" , locLine = 8 - , locColumn = 8 + , locColumn = 21 } ) ( SymbolPredicate @@ -786,7 +786,7 @@ , taskLocation = Location { locFile = "test/examples/russell.tex" , locLine = 15 - , locColumn = 15 + , locColumn = 5 } , taskConjecture = PropositionalConstant IsBottom } @@ -796,7 +796,7 @@ ( Location { locFile = "test/examples/russell.tex" , locLine = 8 - , locColumn = 8 + , locColumn = 18 } ) ( Quantified Existentially @@ -806,7 +806,7 @@ ( Location { locFile = "test/examples/russell.tex" , locLine = 8 - , locColumn = 8 + , locColumn = 21 } ) ( SymbolPredicate @@ -1059,14 +1059,14 @@ ( Location { locFile = "test/examples/russell.tex" , locLine = 11 - , locColumn = 11 + , locColumn = 5 } ) ( Not ( Location { locFile = "test/examples/russell.tex" , locLine = 8 - , locColumn = 8 + , locColumn = 18 } ) ( Quantified Existentially @@ -1075,7 +1075,7 @@ ( Location { locFile = "test/examples/russell.tex" , locLine = 8 - , locColumn = 8 + , locColumn = 21 } ) ( SymbolPredicate @@ -1100,7 +1100,7 @@ , taskLocation = Location { locFile = "test/examples/russell.tex" , locLine = 15 - , locColumn = 15 + , locColumn = 5 } , taskConjecture = PropositionalConstant IsBottom } diff --git a/test/golden/russell/glossing.golden b/test/golden/russell/glossing.golden index 2749294..f07b604 100644 --- a/test/golden/russell/glossing.golden +++ b/test/golden/russell/glossing.golden @@ -48,7 +48,7 @@ ( Location { locFile = "test/examples/russell.tex" , locLine = 7 - , locColumn = 7 + , locColumn = 1 } ) ( Marker "no_universal_set" ) @@ -57,7 +57,7 @@ ( Location { locFile = "test/examples/russell.tex" , locLine = 8 - , locColumn = 8 + , locColumn = 18 } ) ( Quantified Existentially @@ -67,7 +67,7 @@ ( Location { locFile = "test/examples/russell.tex" , locLine = 8 - , locColumn = 8 + , locColumn = 21 } ) ( SymbolPredicate @@ -92,21 +92,21 @@ ( Location { locFile = "test/examples/russell.tex" , locLine = 10 - , locColumn = 10 + , locColumn = 1 } ) ( ByContradiction ( Location { locFile = "test/examples/russell.tex" , locLine = 11 - , locColumn = 11 + , locColumn = 5 } ) ( Take ( Location { locFile = "test/examples/russell.tex" , locLine = 12 - , locColumn = 12 + , locColumn = 5 } ) ( NamedVar "V" :| [] ) @@ -134,7 +134,7 @@ ( Location { locFile = "test/examples/russell.tex" , locLine = 13 - , locColumn = 13 + , locColumn = 5 } ) ( NamedVar "R" ) @@ -176,7 +176,7 @@ ( Location { locFile = "test/examples/russell.tex" , locLine = 14 - , locColumn = 14 + , locColumn = 5 } ) ( Connected Equivalence @@ -229,7 +229,7 @@ ( Location { locFile = "test/examples/russell.tex" , locLine = 15 - , locColumn = 15 + , locColumn = 5 } ) ( PropositionalConstant IsBottom ) JustificationEmpty ( Qed diff --git a/test/golden/russell/parsing.golden b/test/golden/russell/parsing.golden index e7a04b5..73b1081 100644 --- a/test/golden/russell/parsing.golden +++ b/test/golden/russell/parsing.golden @@ -28,7 +28,7 @@ ( Location { locFile = "test/examples/russell.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 18 } ) [ Just @@ -40,7 +40,7 @@ { pos = Location { locFile = "test/examples/russell.tex" , locLine = 4 - , locColumn = 4 + , locColumn = 5 } , qp = QuantPhrase Universally NounPhrase ( [] ) ( Noun @@ -63,7 +63,7 @@ { pos = Location { locFile = "test/examples/russell.tex" , locLine = 4 - , locColumn = 4 + , locColumn = 30 } , formula = FormulaChain ( ChainBase @@ -85,7 +85,7 @@ ( Location { locFile = "test/examples/russell.tex" , locLine = 7 - , locColumn = 7 + , locColumn = 1 } ) ( Marker "no_universal_set" ) @@ -94,13 +94,13 @@ { pos = Location { locFile = "test/examples/russell.tex" , locLine = 8 - , locColumn = 8 + , locColumn = 18 } , stmt = StmtExists { pos = Location { locFile = "test/examples/russell.tex" , locLine = 8 - , locColumn = 8 + , locColumn = 18 } , np = NounPhrase ( @@ -108,7 +108,7 @@ ( Location { locFile = "test/examples/russell.tex" , locLine = 8 - , locColumn = 8 + , locColumn = 21 } ) [ Just @@ -137,21 +137,21 @@ ( Location { locFile = "test/examples/russell.tex" , locLine = 10 - , locColumn = 10 + , locColumn = 1 } ) ( ByContradiction ( Location { locFile = "test/examples/russell.tex" , locLine = 11 - , locColumn = 11 + , locColumn = 5 } ) ( TakeNoun ( Location { locFile = "test/examples/russell.tex" , locLine = 12 - , locColumn = 12 + , locColumn = 5 } ) NounPhrase ( @@ -187,7 +187,7 @@ ( Location { locFile = "test/examples/russell.tex" , locLine = 13 - , locColumn = 13 + , locColumn = 5 } ) ( NamedVar "R" ) @@ -221,7 +221,7 @@ ( Location { locFile = "test/examples/russell.tex" , locLine = 14 - , locColumn = 14 + , locColumn = 5 } ) Nothing ( StmtConnected @@ -231,7 +231,7 @@ { pos = Location { locFile = "test/examples/russell.tex" , locLine = 14 - , locColumn = 14 + , locColumn = 10 } , formula = FormulaChain ( ChainBase @@ -250,7 +250,7 @@ { pos = Location { locFile = "test/examples/russell.tex" , locLine = 14 - , locColumn = 14 + , locColumn = 23 } , formula = FormulaChain ( ChainBase @@ -271,14 +271,14 @@ ( Location { locFile = "test/examples/russell.tex" , locLine = 15 - , locColumn = 15 + , locColumn = 5 } ) Nothing ( StmtFormula { pos = Location { locFile = "test/examples/russell.tex" , locLine = 15 - , locColumn = 15 + , locColumn = 5 } , formula = PropositionalConstant IsBottom } diff --git a/test/golden/separation/parsing.golden b/test/golden/separation/parsing.golden index 3aea94c..9ef21c9 100644 --- a/test/golden/separation/parsing.golden +++ b/test/golden/separation/parsing.golden @@ -11,7 +11,7 @@ { pos = Location { locFile = "test/examples/separation.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 5 } , formula = FormulaChain ( ChainBase diff --git a/test/golden/union/encoding tasks.golden b/test/golden/union/encoding tasks.golden index 3141305..50b4f3c 100644 --- a/test/golden/union/encoding tasks.golden +++ b/test/golden/union/encoding tasks.golden @@ -1,19 +1,19 @@ -fof(union_comm,conjecture,union(fA,fB)=union(fB,fA),"test/examples/union.tex 11:11"). +fof(union_comm,conjecture,union(fA,fB)=union(fB,fA),"test/examples/union.tex 11:1"). 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)). ------------------ -fof(union_assoc,conjecture,![Xa]:(elem(Xa,union(union(fA,fB),fC))=>elem(Xa,union(fA,union(fB,fC)))),"test/examples/union.tex 19:19"). +fof(union_assoc,conjecture,![Xa]:(elem(Xa,union(union(fA,fB),fC))=>elem(Xa,union(fA,union(fB,fC)))),"test/examples/union.tex 19:5"). 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)). ------------------ -fof(union_assoc,conjecture,![Xa]:(elem(Xa,union(fA,union(fB,fC)))=>elem(Xa,union(union(fA,fB),fC))),"test/examples/union.tex 20:20"). +fof(union_assoc,conjecture,![Xa]:(elem(Xa,union(fA,union(fB,fC)))=>elem(Xa,union(union(fA,fB),fC))),"test/examples/union.tex 20:5"). 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)). 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:20"). +fof(union_assoc,conjecture,union(union(fA,fB),fC)=union(fA,union(fB,fC)),"test/examples/union.tex 20:5"). 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 cbfe70b..2b80f20 100644 --- a/test/golden/union/generating tasks.golden +++ b/test/golden/union/generating tasks.golden @@ -189,7 +189,7 @@ , taskLocation = Location { locFile = "test/examples/union.tex" , locLine = 11 - , locColumn = 11 + , locColumn = 1 } , taskConjecture = TermSymbol ( Location @@ -500,7 +500,7 @@ , taskLocation = Location { locFile = "test/examples/union.tex" , locLine = 19 - , locColumn = 19 + , locColumn = 5 } , taskConjecture = Quantified Universally ( Scope @@ -1037,7 +1037,7 @@ , taskLocation = Location { locFile = "test/examples/union.tex" , locLine = 20 - , locColumn = 20 + , locColumn = 5 } , taskConjecture = Quantified Universally ( Scope @@ -1714,7 +1714,7 @@ , taskLocation = Location { locFile = "test/examples/union.tex" , locLine = 20 - , locColumn = 20 + , locColumn = 5 } , taskConjecture = TermSymbol ( Location diff --git a/test/golden/union/glossing.golden b/test/golden/union/glossing.golden index 4a44287..8c1b35b 100644 --- a/test/golden/union/glossing.golden +++ b/test/golden/union/glossing.golden @@ -86,7 +86,7 @@ ( Location { locFile = "test/examples/union.tex" , locLine = 6 - , locColumn = 6 + , locColumn = 1 } ) ( Marker "union_defn" ) @@ -174,7 +174,7 @@ ( Location { locFile = "test/examples/union.tex" , locLine = 11 - , locColumn = 11 + , locColumn = 1 } ) ( Marker "union_comm" ) @@ -236,7 +236,7 @@ ( Location { locFile = "test/examples/union.tex" , locLine = 15 - , locColumn = 15 + , locColumn = 1 } ) ( Marker "union_assoc" ) @@ -332,14 +332,14 @@ ( Location { locFile = "test/examples/union.tex" , locLine = 18 - , locColumn = 18 + , locColumn = 1 } ) ( Have ( Location { locFile = "test/examples/union.tex" , locLine = 19 - , locColumn = 19 + , locColumn = 5 } ) ( Quantified Universally @@ -484,7 +484,7 @@ ( Location { locFile = "test/examples/union.tex" , locLine = 20 - , locColumn = 20 + , locColumn = 5 } ) ( Quantified Universally diff --git a/test/golden/union/parsing.golden b/test/golden/union/parsing.golden index 532b837..5edbb02 100644 --- a/test/golden/union/parsing.golden +++ b/test/golden/union/parsing.golden @@ -12,7 +12,7 @@ { pos = Location { locFile = "test/examples/union.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 13 } , quant = Universally , xs = NamedVar "a" :| [] @@ -25,7 +25,7 @@ { pos = Location { locFile = "test/examples/union.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 33 } , formula = FormulaChain ( ChainBase @@ -44,7 +44,7 @@ { pos = Location { locFile = "test/examples/union.tex" , locLine = 2 - , locColumn = 2 + , locColumn = 46 } , formula = FormulaChain ( ChainBase @@ -67,7 +67,7 @@ { pos = Location { locFile = "test/examples/union.tex" , locLine = 3 - , locColumn = 3 + , locColumn = 10 } , formula = FormulaChain ( ChainBase @@ -88,7 +88,7 @@ ( Location { locFile = "test/examples/union.tex" , locLine = 6 - , locColumn = 6 + , locColumn = 1 } ) ( Marker "union_defn" ) @@ -118,7 +118,7 @@ { pos = Location { locFile = "test/examples/union.tex" , locLine = 8 - , locColumn = 8 + , locColumn = 5 } , formula = FormulaChain ( ChainBase @@ -149,7 +149,7 @@ { pos = Location { locFile = "test/examples/union.tex" , locLine = 8 - , locColumn = 8 + , locColumn = 26 } , formula = FormulaChain ( ChainBase @@ -168,7 +168,7 @@ { pos = Location { locFile = "test/examples/union.tex" , locLine = 8 - , locColumn = 8 + , locColumn = 38 } , formula = FormulaChain ( ChainBase @@ -191,7 +191,7 @@ ( Location { locFile = "test/examples/union.tex" , locLine = 11 - , locColumn = 11 + , locColumn = 1 } ) ( Marker "union_comm" ) @@ -200,7 +200,7 @@ { pos = Location { locFile = "test/examples/union.tex" , locLine = 12 - , locColumn = 12 + , locColumn = 5 } , formula = FormulaChain ( ChainBase @@ -239,7 +239,7 @@ ( Location { locFile = "test/examples/union.tex" , locLine = 15 - , locColumn = 15 + , locColumn = 1 } ) ( Marker "union_assoc" ) @@ -248,7 +248,7 @@ { pos = Location { locFile = "test/examples/union.tex" , locLine = 16 - , locColumn = 16 + , locColumn = 5 } , formula = FormulaChain ( ChainBase @@ -305,21 +305,21 @@ ( Location { locFile = "test/examples/union.tex" , locLine = 18 - , locColumn = 18 + , locColumn = 1 } ) ( Have ( Location { locFile = "test/examples/union.tex" , locLine = 19 - , locColumn = 19 + , locColumn = 5 } ) Nothing ( SymbolicQuantified { pos = Location { locFile = "test/examples/union.tex" , locLine = 19 - , locColumn = 19 + , locColumn = 5 } , quant = Universally , xs = NamedVar "a" :| [] @@ -331,14 +331,14 @@ ( Location { locFile = "test/examples/union.tex" , locLine = 19 - , locColumn = 19 + , locColumn = 25 } ) , stmt1 = StmtFormula { pos = Location { locFile = "test/examples/union.tex" , locLine = 19 - , locColumn = 19 + , locColumn = 28 } , formula = FormulaChain ( ChainBase @@ -375,7 +375,7 @@ { pos = Location { locFile = "test/examples/union.tex" , locLine = 19 - , locColumn = 19 + , locColumn = 61 } , formula = FormulaChain ( ChainBase @@ -415,14 +415,14 @@ ( Location { locFile = "test/examples/union.tex" , locLine = 20 - , locColumn = 20 + , locColumn = 5 } ) Nothing ( SymbolicQuantified { pos = Location { locFile = "test/examples/union.tex" , locLine = 20 - , locColumn = 20 + , locColumn = 5 } , quant = Universally , xs = NamedVar "a" :| [] @@ -434,14 +434,14 @@ ( Location { locFile = "test/examples/union.tex" , locLine = 20 - , locColumn = 20 + , locColumn = 25 } ) , stmt1 = StmtFormula { pos = Location { locFile = "test/examples/union.tex" , locLine = 20 - , locColumn = 20 + , locColumn = 28 } , formula = FormulaChain ( ChainBase @@ -478,7 +478,7 @@ { pos = Location { locFile = "test/examples/union.tex" , locLine = 20 - , locColumn = 20 + , locColumn = 61 } , formula = FormulaChain ( ChainBase |