diff options
Diffstat (limited to 'test/golden')
21 files changed, 912 insertions, 214 deletions
diff --git a/test/golden/coord/parsing.golden b/test/golden/coord/parsing.golden index 2c1ca80..f148da6 100644 --- a/test/golden/coord/parsing.golden +++ b/test/golden/coord/parsing.golden @@ -485,12 +485,38 @@ } ) ) -, BlockClaim Proposition +, BlockProof + ( Location + { locFile = "test/examples/coord.tex" + , locLine = 33 + , locColumn = 1 + } + ) + ( Qed + ( Just + ( Location + { locFile = "test/examples/coord.tex" + , locLine = 34 + , locColumn = 5 + } + ) + ) + ( JustificationRef + ( Marker "bar" :| [] ) + ) + ) ( Location { locFile = "test/examples/coord.tex" , locLine = 35 , locColumn = 1 } + ) +, BlockClaim Proposition + ( Location + { locFile = "test/examples/coord.tex" + , locLine = 38 + , locColumn = 1 + } ) Nothing ( Marker "adjs" ) ( Claim [] @@ -503,7 +529,7 @@ ( Adj ( Location { locFile = "test/examples/coord.tex" - , locLine = 36 + , locLine = 39 , locColumn = 12 } ) @@ -516,7 +542,7 @@ [ Adj ( Location { locFile = "test/examples/coord.tex" - , locLine = 36 + , locLine = 39 , locColumn = 20 } ) @@ -531,10 +557,38 @@ } ) ) +, BlockProof + ( Location + { locFile = "test/examples/coord.tex" + , locLine = 41 + , locColumn = 1 + } + ) + ( Qed + ( Just + ( Location + { locFile = "test/examples/coord.tex" + , locLine = 42 + , locColumn = 5 + } + ) + ) + ( JustificationRef + ( Marker "foo" :| + [ Marker "baz" ] + ) + ) + ) + ( Location + { locFile = "test/examples/coord.tex" + , locLine = 43 + , locColumn = 1 + } + ) , BlockClaim Proposition ( Location { locFile = "test/examples/coord.tex" - , locLine = 39 + , locLine = 45 , locColumn = 1 } ) Nothing @@ -548,7 +602,7 @@ [ AdjL ( Location { locFile = "test/examples/coord.tex" - , locLine = 40 + , locLine = 46 , locColumn = 19 } ) @@ -563,7 +617,7 @@ ( Noun ( Location { locFile = "test/examples/coord.tex" - , locLine = 40 + , locLine = 46 , locColumn = 23 } ) @@ -594,7 +648,7 @@ [ AdjL ( Location { locFile = "test/examples/coord.tex" - , locLine = 41 + , locLine = 47 , locColumn = 26 } ) @@ -609,7 +663,7 @@ ( Noun ( Location { locFile = "test/examples/coord.tex" - , locLine = 41 + , locLine = 47 , locColumn = 30 } ) diff --git a/test/golden/coord/tokenizing.golden b/test/golden/coord/tokenizing.golden index 56dac36..252d9ab 100644 --- a/test/golden/coord/tokenizing.golden +++ b/test/golden/coord/tokenizing.golden @@ -151,6 +151,15 @@ , EndEnv "proposition" ] , + [ BeginEnv "proof" + , Word "follows" + , Word "by" + , Ref + ( "bar" :| [] ) + , Symbol "." + , EndEnv "proof" + ] +, [ BeginEnv "proposition" , Label "adjs" , BeginEnv "math" @@ -164,6 +173,15 @@ , EndEnv "proposition" ] , + [ BeginEnv "proof" + , Word "follows" + , Word "by" + , Ref + ( "foo" :| [ "baz" ] ) + , Symbol "." + , EndEnv "proof" + ] +, [ BeginEnv "proposition" , Label "are_nouns" , Word "let" diff --git a/test/golden/datatype/parsing.golden b/test/golden/datatype/parsing.golden index d07b92c..11dd2bc 100644 --- a/test/golden/datatype/parsing.golden +++ b/test/golden/datatype/parsing.golden @@ -88,15 +88,15 @@ , ExprFiniteSet ( Location { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 54 + , locLine = 7 + , locColumn = 20 } ) ( ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 6 - , locColumn = 56 + , locLine = 7 + , locColumn = 22 } ) ( MixfixItem @@ -113,7 +113,7 @@ { datatypeClauseConstructorExpr = ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 7 + , locLine = 8 , locColumn = 17 } ) @@ -133,7 +133,7 @@ , datatypeClauseTargetExpr = ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 7 + , locLine = 8 , locColumn = 34 } ) @@ -149,7 +149,7 @@ , ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 7 + , locLine = 8 , locColumn = 56 } ) @@ -165,7 +165,7 @@ , ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 7 + , locLine = 8 , locColumn = 78 } ) @@ -184,7 +184,7 @@ , BlockClaim Proposition ( Location { locFile = "test/examples/datatype.tex" - , locLine = 10 + , locLine = 11 , locColumn = 1 } ) Nothing @@ -196,7 +196,7 @@ ( ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 11 + , locLine = 12 , locColumn = 6 } ) @@ -210,7 +210,7 @@ ( Relation ( Location { locFile = "test/examples/datatype.tex" - , locLine = 11 + , locLine = 12 , locColumn = 15 } ) @@ -223,7 +223,7 @@ ( ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 11 + , locLine = 12 , locColumn = 19 } ) @@ -238,12 +238,38 @@ } ) ) -, BlockClaim Proposition +, BlockProof ( Location { locFile = "test/examples/datatype.tex" , locLine = 14 , locColumn = 1 } + ) + ( Qed + ( Just + ( Location + { locFile = "test/examples/datatype.tex" + , locLine = 15 + , locColumn = 5 + } + ) + ) + ( JustificationRef + ( Marker "propform_propbot_intro" :| [] ) + ) + ) + ( Location + { locFile = "test/examples/datatype.tex" + , locLine = 16 + , locColumn = 1 + } + ) +, BlockClaim Proposition + ( Location + { locFile = "test/examples/datatype.tex" + , locLine = 18 + , locColumn = 1 + } ) Nothing ( Marker "propform_var_test" ) ( Claim [] @@ -252,7 +278,7 @@ , mloc = Just ( Location { locFile = "test/examples/datatype.tex" - , locLine = 15 + , locLine = 19 , locColumn = 5 } ) @@ -262,7 +288,7 @@ ( ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 15 + , locLine = 19 , locColumn = 9 } ) @@ -276,7 +302,7 @@ ( Relation ( Location { locFile = "test/examples/datatype.tex" - , locLine = 15 + , locLine = 19 , locColumn = 19 } ) @@ -289,14 +315,14 @@ ( ExprFiniteSet ( Location { locFile = "test/examples/datatype.tex" - , locLine = 15 + , locLine = 19 , locColumn = 23 } ) ( ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 15 + , locLine = 19 , locColumn = 25 } ) @@ -316,8 +342,8 @@ ( ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 45 + , locLine = 20 + , locColumn = 10 } ) ( MixfixItem @@ -332,8 +358,8 @@ [ ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 54 + , locLine = 20 + , locColumn = 19 } ) ( MixfixItem @@ -347,8 +373,8 @@ ( Relation ( Location { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 65 + , locLine = 20 + , locColumn = 30 } ) ( RelationSymbol @@ -360,8 +386,8 @@ ( ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 15 - , locColumn = 69 + , locLine = 20 + , locColumn = 34 } ) ( MixfixItem @@ -376,10 +402,36 @@ } ) ) +, BlockProof + ( Location + { locFile = "test/examples/datatype.tex" + , locLine = 22 + , locColumn = 1 + } + ) + ( Qed + ( Just + ( Location + { locFile = "test/examples/datatype.tex" + , locLine = 23 + , locColumn = 5 + } + ) + ) + ( JustificationRef + ( Marker "propform_propvar_intro" :| [] ) + ) + ) + ( Location + { locFile = "test/examples/datatype.tex" + , locLine = 24 + , locColumn = 1 + } + ) , BlockClaim Proposition ( Location { locFile = "test/examples/datatype.tex" - , locLine = 18 + , locLine = 26 , locColumn = 1 } ) Nothing @@ -391,7 +443,7 @@ ( ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 19 + , locLine = 27 , locColumn = 7 } ) @@ -406,7 +458,7 @@ [ ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 19 + , locLine = 27 , locColumn = 7 } ) @@ -419,7 +471,7 @@ , ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 19 + , locLine = 27 , locColumn = 24 } ) @@ -434,7 +486,7 @@ ( Relation ( Location { locFile = "test/examples/datatype.tex" - , locLine = 19 + , locLine = 27 , locColumn = 34 } ) @@ -447,7 +499,7 @@ ( ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 19 + , locLine = 27 , locColumn = 38 } ) @@ -462,10 +514,38 @@ } ) ) +, BlockProof + ( Location + { locFile = "test/examples/datatype.tex" + , locLine = 29 + , locColumn = 1 + } + ) + ( Qed + ( Just + ( Location + { locFile = "test/examples/datatype.tex" + , locLine = 30 + , locColumn = 5 + } + ) + ) + ( JustificationRef + ( Marker "propform_propbot_intro" :| + [ Marker "propform_propto_intro" ] + ) + ) + ) + ( Location + { locFile = "test/examples/datatype.tex" + , locLine = 31 + , locColumn = 1 + } + ) , BlockClaim Proposition ( Location { locFile = "test/examples/datatype.tex" - , locLine = 22 + , locLine = 33 , locColumn = 1 } ) Nothing @@ -477,7 +557,7 @@ ( ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 23 + , locLine = 34 , locColumn = 6 } ) @@ -491,7 +571,7 @@ ( Relation ( Location { locFile = "test/examples/datatype.tex" - , locLine = 23 + , locLine = 34 , locColumn = 15 } ) @@ -504,7 +584,7 @@ ( ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 23 + , locLine = 34 , locColumn = 21 } ) @@ -519,7 +599,7 @@ [ ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 23 + , locLine = 34 , locColumn = 21 } ) @@ -532,7 +612,7 @@ , ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 23 + , locLine = 34 , locColumn = 38 } ) @@ -548,10 +628,36 @@ } ) ) +, BlockProof + ( Location + { locFile = "test/examples/datatype.tex" + , locLine = 36 + , locColumn = 1 + } + ) + ( Qed + ( Just + ( Location + { locFile = "test/examples/datatype.tex" + , locLine = 37 + , locColumn = 5 + } + ) + ) + ( JustificationRef + ( Marker "propform_propbot_propto_distinct" :| [] ) + ) + ) + ( Location + { locFile = "test/examples/datatype.tex" + , locLine = 38 + , locColumn = 1 + } + ) , BlockClaim Proposition ( Location { locFile = "test/examples/datatype.tex" - , locLine = 26 + , locLine = 40 , locColumn = 1 } ) Nothing @@ -562,7 +668,7 @@ , mloc = Just ( Location { locFile = "test/examples/datatype.tex" - , locLine = 27 + , locLine = 41 , locColumn = 5 } ) @@ -572,7 +678,7 @@ ( ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 27 + , locLine = 41 , locColumn = 9 } ) @@ -592,7 +698,7 @@ ( Relation ( Location { locFile = "test/examples/datatype.tex" - , locLine = 27 + , locLine = 41 , locColumn = 21 } ) @@ -605,7 +711,7 @@ ( ExprOp ( Location { locFile = "test/examples/datatype.tex" - , locLine = 27 + , locLine = 41 , locColumn = 23 } ) @@ -633,7 +739,7 @@ ( Relation ( Location { locFile = "test/examples/datatype.tex" - , locLine = 27 + , locLine = 41 , locColumn = 45 } ) @@ -651,4 +757,30 @@ } ) ) +, BlockProof + ( Location + { locFile = "test/examples/datatype.tex" + , locLine = 43 + , locColumn = 1 + } + ) + ( Qed + ( Just + ( Location + { locFile = "test/examples/datatype.tex" + , locLine = 44 + , locColumn = 5 + } + ) + ) + ( JustificationRef + ( Marker "propform_propvar_injective" :| [] ) + ) + ) + ( Location + { locFile = "test/examples/datatype.tex" + , locLine = 45 + , locColumn = 1 + } + ) ]
\ No newline at end of file diff --git a/test/golden/datatype/tokenizing.golden b/test/golden/datatype/tokenizing.golden index 1827a62..90f8274 100644 --- a/test/golden/datatype/tokenizing.golden +++ b/test/golden/datatype/tokenizing.golden @@ -73,6 +73,15 @@ , EndEnv "proposition" ] , + [ BeginEnv "proof" + , Word "follows" + , Word "by" + , Ref + ( "propform_propbot_intro" :| [] ) + , Symbol "." + , EndEnv "proof" + ] +, [ BeginEnv "proposition" , Label "propform_var_test" , Word "if" @@ -97,6 +106,15 @@ , EndEnv "proposition" ] , + [ BeginEnv "proof" + , Word "follows" + , Word "by" + , Ref + ( "propform_propvar_intro" :| [] ) + , Symbol "." + , EndEnv "proof" + ] +, [ BeginEnv "proposition" , Label "propform_imp_test" , BeginEnv "math" @@ -112,6 +130,15 @@ , EndEnv "proposition" ] , + [ BeginEnv "proof" + , Word "follows" + , Word "by" + , Ref + ( "propform_propbot_intro" :| [ "propform_propto_intro" ] ) + , Symbol "." + , EndEnv "proof" + ] +, [ BeginEnv "proposition" , Label "propform_distinct_test" , BeginEnv "math" @@ -127,6 +154,15 @@ , EndEnv "proposition" ] , + [ BeginEnv "proof" + , Word "follows" + , Word "by" + , Ref + ( "propform_propbot_propto_distinct" :| [] ) + , Symbol "." + , EndEnv "proof" + ] +, [ BeginEnv "proposition" , Label "propform_injective_test" , Word "if" @@ -151,4 +187,13 @@ , Symbol "." , EndEnv "proposition" ] +, + [ BeginEnv "proof" + , Word "follows" + , Word "by" + , Ref + ( "propform_propvar_injective" :| [] ) + , Symbol "." + , EndEnv "proof" + ] ]
\ No newline at end of file diff --git a/test/golden/finite-set-terms/parsing.golden b/test/golden/finite-set-terms/parsing.golden index 6d031b4..d351ceb 100644 --- a/test/golden/finite-set-terms/parsing.golden +++ b/test/golden/finite-set-terms/parsing.golden @@ -1,10 +1,58 @@ -[ BlockAxiom +[ BlockSig ( Location { locFile = "test/examples/finite-set-terms.tex" , locLine = 1 , locColumn = 1 } ) Nothing + ( Marker "example_cons" ) [] + ( SignatureSymbolic + ( SymbolPattern + ( MixfixItem + ( TokenCons + ( Command "cons" ) + ( TokenCons InvisibleBraceL + ( HoleCons + ( TokenCons InvisibleBraceR + ( TokenCons InvisibleBraceL + ( HoleCons ( TokenCons InvisibleBraceR End ) ) + ) + ) + ) + ) + ) + ( Marker "cons" ) NonAssoc + ) + [ NamedVar "y" + , NamedVar "X" + ] + ) NounPhrase ( [] ) + ( Noun + ( Location + { locFile = "test/examples/finite-set-terms.tex" + , locLine = 2 + , locColumn = 24 + } + ) + ( LexicalItemSgPl + ( SgPl + { sg = TokenCons + ( Word "set" ) End + , pl = TokenCons + ( Word "sets" ) End + } + ) + ( Marker "set" ) + ) [] + ) ( Nothing ) ( [] ) ( Nothing ) + ) +, BlockAxiom + ( Location + { locFile = "test/examples/finite-set-terms.tex" + , locLine = 5 + , locColumn = 1 + } + ) Nothing ( Marker "cons" ) ( Axiom [] ( StmtConnected @@ -19,7 +67,7 @@ ( Relation ( Location { locFile = "test/examples/finite-set-terms.tex" - , locLine = 2 + , locLine = 6 , locColumn = 7 } ) @@ -32,7 +80,7 @@ ( ExprOp ( Location { locFile = "test/examples/finite-set-terms.tex" - , locLine = 2 + , locLine = 6 , locColumn = 11 } ) @@ -71,7 +119,7 @@ ( Relation ( Location { locFile = "test/examples/finite-set-terms.tex" - , locLine = 2 + , locLine = 6 , locColumn = 31 } ) @@ -95,7 +143,7 @@ ( Relation ( Location { locFile = "test/examples/finite-set-terms.tex" - , locLine = 2 + , locLine = 6 , locColumn = 41 } ) @@ -117,7 +165,7 @@ , BlockDefn ( Location { locFile = "test/examples/finite-set-terms.tex" - , locLine = 5 + , locLine = 9 , locColumn = 1 } ) Nothing @@ -134,14 +182,14 @@ ( ExprFiniteSet ( Location { locFile = "test/examples/finite-set-terms.tex" - , locLine = 6 + , locLine = 10 , locColumn = 14 } ) ( ExprOp ( Location { locFile = "test/examples/finite-set-terms.tex" - , locLine = 6 + , locLine = 10 , locColumn = 16 } ) @@ -157,7 +205,7 @@ , BlockClaim Proposition ( Location { locFile = "test/examples/finite-set-terms.tex" - , locLine = 9 + , locLine = 13 , locColumn = 1 } ) Nothing @@ -169,7 +217,7 @@ ( ExprOp ( Location { locFile = "test/examples/finite-set-terms.tex" - , locLine = 10 + , locLine = 14 , locColumn = 6 } ) @@ -183,7 +231,7 @@ ( Relation ( Location { locFile = "test/examples/finite-set-terms.tex" - , locLine = 10 + , locLine = 14 , locColumn = 15 } ) @@ -196,7 +244,7 @@ ( ExprOp ( Location { locFile = "test/examples/finite-set-terms.tex" - , locLine = 10 + , locLine = 14 , locColumn = 18 } ) diff --git a/test/golden/finite-set-terms/scanning.golden b/test/golden/finite-set-terms/scanning.golden index 5cef8dd..66d57f7 100644 --- a/test/golden/finite-set-terms/scanning.golden +++ b/test/golden/finite-set-terms/scanning.golden @@ -1,5 +1,19 @@ [ ScanFunctionSymbol ( TokenCons + ( Command "cons" ) + ( TokenCons InvisibleBraceL + ( HoleCons + ( TokenCons InvisibleBraceR + ( TokenCons InvisibleBraceL + ( HoleCons ( TokenCons InvisibleBraceR End ) ) + ) + ) + ) + ) + ) + ( Marker "example_cons" ) +, ScanFunctionSymbol + ( TokenCons ( Command "unit" ) End ) ( Marker "unit" ) diff --git a/test/golden/finite-set-terms/tokenizing.golden b/test/golden/finite-set-terms/tokenizing.golden index 200e330..ebe2484 100644 --- a/test/golden/finite-set-terms/tokenizing.golden +++ b/test/golden/finite-set-terms/tokenizing.golden @@ -1,4 +1,22 @@ [ + [ BeginEnv "signature" + , Label "example_cons" + , BeginEnv "math" + , Command "cons" + , InvisibleBraceL + , Variable "y" + , InvisibleBraceR + , InvisibleBraceL + , Variable "X" + , InvisibleBraceR + , EndEnv "math" + , Word "is" + , Word "a" + , Word "set" + , Symbol "." + , EndEnv "signature" + ] +, [ BeginEnv "axiom" , Label "cons" , BeginEnv "math" diff --git a/test/golden/proofdefinefunction/parsing.golden b/test/golden/proofdefinefunction/parsing.golden index 1089d8f..60110a5 100644 --- a/test/golden/proofdefinefunction/parsing.golden +++ b/test/golden/proofdefinefunction/parsing.golden @@ -1,7 +1,55 @@ -[ BlockDefn +[ BlockSig ( Location { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 3 + , locLine = 1 + , locColumn = 1 + } + ) Nothing + ( Marker "example_pair" ) [] + ( SignatureSymbolic + ( SymbolPattern + ( MixfixItem + ( TokenCons + ( Command "pair" ) + ( TokenCons InvisibleBraceL + ( HoleCons + ( TokenCons InvisibleBraceR + ( TokenCons InvisibleBraceL + ( HoleCons ( TokenCons InvisibleBraceR End ) ) + ) + ) + ) + ) + ) + ( Marker "pair" ) NonAssoc + ) + [ NamedVar "x" + , NamedVar "y" + ] + ) NounPhrase ( [] ) + ( Noun + ( Location + { locFile = "test/examples/proofdefinefunction.tex" + , locLine = 2 + , locColumn = 18 + } + ) + ( LexicalItemSgPl + ( SgPl + { sg = TokenCons + ( Word "set" ) End + , pl = TokenCons + ( Word "sets" ) End + } + ) + ( Marker "set" ) + ) [] + ) ( Nothing ) ( [] ) ( Nothing ) + ) +, BlockDefn + ( Location + { locFile = "test/examples/proofdefinefunction.tex" + , locLine = 7 , locColumn = 1 } ) Nothing @@ -34,7 +82,7 @@ , BlockDefn ( Location { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 8 + , locLine = 12 , locColumn = 1 } ) Nothing @@ -59,7 +107,7 @@ , BlockDefn ( Location { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 13 + , locLine = 17 , locColumn = 1 } ) Nothing @@ -70,7 +118,7 @@ ( Adj ( Location { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 14 + , locLine = 18 , locColumn = 12 } ) @@ -91,7 +139,7 @@ ( Relation ( Location { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 14 + , locLine = 18 , locColumn = 31 } ) @@ -111,7 +159,7 @@ , BlockDefn ( Location { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 18 + , locLine = 22 , locColumn = 1 } ) Nothing @@ -122,7 +170,7 @@ ( Noun ( Location { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 19 + , locLine = 23 , locColumn = 14 } ) @@ -147,7 +195,7 @@ ( Relation ( Location { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 19 + , locLine = 23 , locColumn = 29 } ) @@ -167,7 +215,7 @@ , BlockClaim Proposition ( Location { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 22 + , locLine = 26 , locColumn = 1 } ) Nothing @@ -178,7 +226,7 @@ , mloc = Just ( Location { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 23 + , locLine = 27 , locColumn = 5 } ) @@ -191,7 +239,7 @@ ( Relation ( Location { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 23 + , locLine = 27 , locColumn = 10 } ) @@ -215,7 +263,7 @@ ( Relation ( Location { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 23 + , locLine = 27 , locColumn = 25 } ) @@ -236,14 +284,14 @@ , BlockProof ( Location { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 25 + , locLine = 29 , locColumn = 1 } ) ( DefineFunction ( Location { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 26 + , locLine = 30 , locColumn = 5 } ) @@ -259,7 +307,7 @@ ) ( Location { locFile = "test/examples/proofdefinefunction.tex" - , locLine = 27 + , locLine = 31 , locColumn = 1 } ) diff --git a/test/golden/proofdefinefunction/scanning.golden b/test/golden/proofdefinefunction/scanning.golden index fd20405..c49d8f9 100644 --- a/test/golden/proofdefinefunction/scanning.golden +++ b/test/golden/proofdefinefunction/scanning.golden @@ -1,4 +1,14 @@ [ ScanFunctionSymbol + ( TokenCons ParenL + ( HoleCons + ( TokenCons + ( Symbol "," ) + ( HoleCons ( TokenCons ParenR End ) ) + ) + ) + ) + ( Marker "example_pair" ) +, ScanFunctionSymbol ( TokenCons ( Command "apply" ) ( TokenCons InvisibleBraceL diff --git a/test/golden/proofdefinefunction/tokenizing.golden b/test/golden/proofdefinefunction/tokenizing.golden index 63692ab..d479529 100644 --- a/test/golden/proofdefinefunction/tokenizing.golden +++ b/test/golden/proofdefinefunction/tokenizing.golden @@ -1,4 +1,20 @@ [ + [ BeginEnv "signature" + , Label "example_pair" + , BeginEnv "math" + , ParenL + , Variable "x" + , Symbol "," + , Variable "y" + , ParenR + , EndEnv "math" + , Word "is" + , Word "a" + , Word "set" + , Symbol "." + , EndEnv "signature" + ] +, [ BeginEnv "definition" , Label "apply" , BeginEnv "math" diff --git a/test/golden/relation-notation/parsing.golden b/test/golden/relation-notation/parsing.golden index 6c489be..65a7b94 100644 --- a/test/golden/relation-notation/parsing.golden +++ b/test/golden/relation-notation/parsing.golden @@ -1,10 +1,58 @@ -[ BlockClaim Proposition +[ BlockSig ( Location { locFile = "test/examples/relation-notation.tex" , locLine = 1 , locColumn = 1 } ) Nothing + ( Marker "example_pair" ) [] + ( SignatureSymbolic + ( SymbolPattern + ( MixfixItem + ( TokenCons + ( Command "pair" ) + ( TokenCons InvisibleBraceL + ( HoleCons + ( TokenCons InvisibleBraceR + ( TokenCons InvisibleBraceL + ( HoleCons ( TokenCons InvisibleBraceR End ) ) + ) + ) + ) + ) + ) + ( Marker "pair" ) NonAssoc + ) + [ NamedVar "x" + , NamedVar "y" + ] + ) NounPhrase ( [] ) + ( Noun + ( Location + { locFile = "test/examples/relation-notation.tex" + , locLine = 2 + , locColumn = 18 + } + ) + ( LexicalItemSgPl + ( SgPl + { sg = TokenCons + ( Word "set" ) End + , pl = TokenCons + ( Word "sets" ) End + } + ) + ( Marker "set" ) + ) [] + ) ( Nothing ) ( [] ) ( Nothing ) + ) +, BlockClaim Proposition + ( Location + { locFile = "test/examples/relation-notation.tex" + , locLine = 5 + , locColumn = 1 + } + ) Nothing ( Marker "mathrel_notation_test" ) ( Claim [] ( StmtConnected @@ -12,7 +60,7 @@ , mloc = Just ( Location { locFile = "test/examples/relation-notation.tex" - , locLine = 2 + , locLine = 6 , locColumn = 5 } ) @@ -25,7 +73,7 @@ ( RelationExpr ( Location { locFile = "test/examples/relation-notation.tex" - , locLine = 2 + , locLine = 6 , locColumn = 10 } ) @@ -47,7 +95,7 @@ ( RelationExpr ( Location { locFile = "test/examples/relation-notation.tex" - , locLine = 2 + , locLine = 6 , locColumn = 33 } ) diff --git a/test/golden/relation-notation/scanning.golden b/test/golden/relation-notation/scanning.golden index 0637a08..5a6351e 100644 --- a/test/golden/relation-notation/scanning.golden +++ b/test/golden/relation-notation/scanning.golden @@ -1 +1,11 @@ -[]
\ No newline at end of file +[ ScanFunctionSymbol + ( TokenCons ParenL + ( HoleCons + ( TokenCons + ( Symbol "," ) + ( HoleCons ( TokenCons ParenR End ) ) + ) + ) + ) + ( Marker "example_pair" ) +]
\ No newline at end of file diff --git a/test/golden/relation-notation/tokenizing.golden b/test/golden/relation-notation/tokenizing.golden index ae1bda5..84fc828 100644 --- a/test/golden/relation-notation/tokenizing.golden +++ b/test/golden/relation-notation/tokenizing.golden @@ -1,4 +1,20 @@ [ + [ BeginEnv "signature" + , Label "example_pair" + , BeginEnv "math" + , ParenL + , Variable "x" + , Symbol "," + , Variable "y" + , ParenR + , EndEnv "math" + , Word "is" + , Word "a" + , Word "set" + , Symbol "." + , EndEnv "signature" + ] +, [ BeginEnv "proposition" , Label "mathrel_notation_test" , Word "if" diff --git a/test/golden/replace/parsing.golden b/test/golden/replace/parsing.golden index 8bdea69..5ea7cac 100644 --- a/test/golden/replace/parsing.golden +++ b/test/golden/replace/parsing.golden @@ -1,10 +1,106 @@ -[ BlockAxiom +[ BlockSig ( Location { locFile = "test/examples/replace.tex" , locLine = 1 , locColumn = 1 } ) Nothing + ( Marker "example_cons" ) [] + ( SignatureSymbolic + ( SymbolPattern + ( MixfixItem + ( TokenCons + ( Command "cons" ) + ( TokenCons InvisibleBraceL + ( HoleCons + ( TokenCons InvisibleBraceR + ( TokenCons InvisibleBraceL + ( HoleCons ( TokenCons InvisibleBraceR End ) ) + ) + ) + ) + ) + ) + ( Marker "cons" ) NonAssoc + ) + [ NamedVar "y" + , NamedVar "X" + ] + ) NounPhrase ( [] ) + ( Noun + ( Location + { locFile = "test/examples/replace.tex" + , locLine = 2 + , locColumn = 24 + } + ) + ( LexicalItemSgPl + ( SgPl + { sg = TokenCons + ( Word "set" ) End + , pl = TokenCons + ( Word "sets" ) End + } + ) + ( Marker "set" ) + ) [] + ) ( Nothing ) ( [] ) ( Nothing ) + ) +, BlockSig + ( Location + { locFile = "test/examples/replace.tex" + , locLine = 5 + , locColumn = 1 + } + ) Nothing + ( Marker "example_pair" ) [] + ( SignatureSymbolic + ( SymbolPattern + ( MixfixItem + ( TokenCons + ( Command "pair" ) + ( TokenCons InvisibleBraceL + ( HoleCons + ( TokenCons InvisibleBraceR + ( TokenCons InvisibleBraceL + ( HoleCons ( TokenCons InvisibleBraceR End ) ) + ) + ) + ) + ) + ) + ( Marker "pair" ) NonAssoc + ) + [ NamedVar "x" + , NamedVar "y" + ] + ) NounPhrase ( [] ) + ( Noun + ( Location + { locFile = "test/examples/replace.tex" + , locLine = 6 + , locColumn = 18 + } + ) + ( LexicalItemSgPl + ( SgPl + { sg = TokenCons + ( Word "set" ) End + , pl = TokenCons + ( Word "sets" ) End + } + ) + ( Marker "set" ) + ) [] + ) ( Nothing ) ( [] ) ( Nothing ) + ) +, BlockAxiom + ( Location + { locFile = "test/examples/replace.tex" + , locLine = 9 + , locColumn = 1 + } + ) Nothing ( Marker "cons" ) ( Axiom [] ( StmtConnected @@ -19,7 +115,7 @@ ( Relation ( Location { locFile = "test/examples/replace.tex" - , locLine = 2 + , locLine = 10 , locColumn = 7 } ) @@ -32,7 +128,7 @@ ( ExprOp ( Location { locFile = "test/examples/replace.tex" - , locLine = 2 + , locLine = 10 , locColumn = 11 } ) @@ -71,7 +167,7 @@ ( Relation ( Location { locFile = "test/examples/replace.tex" - , locLine = 2 + , locLine = 10 , locColumn = 31 } ) @@ -95,7 +191,7 @@ ( Relation ( Location { locFile = "test/examples/replace.tex" - , locLine = 2 + , locLine = 10 , locColumn = 41 } ) @@ -117,7 +213,7 @@ , BlockDefn ( Location { locFile = "test/examples/replace.tex" - , locLine = 5 + , locLine = 13 , locColumn = 1 } ) Nothing @@ -139,14 +235,14 @@ ( ExprReplace ( Location { locFile = "test/examples/replace.tex" - , locLine = 6 + , locLine = 14 , locColumn = 18 } ) ( ExprOp ( Location { locFile = "test/examples/replace.tex" - , locLine = 6 + , locLine = 14 , locColumn = 21 } ) @@ -188,7 +284,7 @@ , BlockDefn ( Location { locFile = "test/examples/replace.tex" - , locLine = 9 + , locLine = 17 , locColumn = 1 } ) Nothing @@ -205,14 +301,14 @@ ( ExprFiniteSet ( Location { locFile = "test/examples/replace.tex" - , locLine = 10 + , locLine = 18 , locColumn = 14 } ) ( ExprOp ( Location { locFile = "test/examples/replace.tex" - , locLine = 10 + , locLine = 18 , locColumn = 16 } ) @@ -228,7 +324,7 @@ , BlockClaim Proposition ( Location { locFile = "test/examples/replace.tex" - , locLine = 13 + , locLine = 21 , locColumn = 1 } ) Nothing @@ -240,7 +336,7 @@ ( ExprOp ( Location { locFile = "test/examples/replace.tex" - , locLine = 14 + , locLine = 22 , locColumn = 6 } ) @@ -262,7 +358,7 @@ [ ExprOp ( Location { locFile = "test/examples/replace.tex" - , locLine = 14 + , locLine = 22 , locColumn = 7 } ) @@ -275,7 +371,7 @@ , ExprOp ( Location { locFile = "test/examples/replace.tex" - , locLine = 14 + , locLine = 22 , locColumn = 17 } ) @@ -290,7 +386,7 @@ ( Relation ( Location { locFile = "test/examples/replace.tex" - , locLine = 14 + , locLine = 22 , locColumn = 27 } ) @@ -303,7 +399,7 @@ ( ExprOp ( Location { locFile = "test/examples/replace.tex" - , locLine = 14 + , locLine = 22 , locColumn = 31 } ) @@ -318,7 +414,7 @@ [ ExprOp ( Location { locFile = "test/examples/replace.tex" - , locLine = 14 + , locLine = 22 , locColumn = 31 } ) @@ -331,7 +427,7 @@ , ExprOp ( Location { locFile = "test/examples/replace.tex" - , locLine = 14 + , locLine = 22 , locColumn = 42 } ) @@ -350,7 +446,7 @@ , BlockDefn ( Location { locFile = "test/examples/replace.tex" - , locLine = 19 + , locLine = 27 , locColumn = 1 } ) Nothing @@ -371,7 +467,7 @@ ( ExprReplacePred ( Location { locFile = "test/examples/replace.tex" - , locLine = 20 + , locLine = 28 , locColumn = 16 } ) @@ -389,7 +485,7 @@ ( Relation ( Location { locFile = "test/examples/replace.tex" - , locLine = 20 + , locLine = 28 , locColumn = 44 } ) @@ -402,7 +498,7 @@ ( ExprFiniteSet ( Location { locFile = "test/examples/replace.tex" - , locLine = 20 + , locLine = 28 , locColumn = 46 } ) @@ -418,7 +514,7 @@ , BlockClaim Proposition ( Location { locFile = "test/examples/replace.tex" - , locLine = 25 + , locLine = 33 , locColumn = 1 } ) Nothing @@ -430,7 +526,7 @@ ( ExprOp ( Location { locFile = "test/examples/replace.tex" - , locLine = 26 + , locLine = 34 , locColumn = 6 } ) @@ -451,7 +547,7 @@ ( Relation ( Location { locFile = "test/examples/replace.tex" - , locLine = 26 + , locLine = 34 , locColumn = 16 } ) @@ -464,14 +560,14 @@ ( ExprReplace ( Location { locFile = "test/examples/replace.tex" - , locLine = 26 + , locLine = 34 , locColumn = 18 } ) ( ExprOp ( Location { locFile = "test/examples/replace.tex" - , locLine = 26 + , locLine = 34 , locColumn = 21 } ) @@ -513,4 +609,30 @@ } ) ) +, BlockProof + ( Location + { locFile = "test/examples/replace.tex" + , locLine = 36 + , locColumn = 1 + } + ) + ( Qed + ( Just + ( Location + { locFile = "test/examples/replace.tex" + , locLine = 37 + , locColumn = 5 + } + ) + ) + ( JustificationRef + ( Marker "times" :| [] ) + ) + ) + ( Location + { locFile = "test/examples/replace.tex" + , locLine = 38 + , locColumn = 1 + } + ) ]
\ No newline at end of file diff --git a/test/golden/replace/scanning.golden b/test/golden/replace/scanning.golden index a131d69..6d9ffb0 100644 --- a/test/golden/replace/scanning.golden +++ b/test/golden/replace/scanning.golden @@ -1,4 +1,28 @@ [ ScanFunctionSymbol + ( TokenCons + ( Command "cons" ) + ( TokenCons InvisibleBraceL + ( HoleCons + ( TokenCons InvisibleBraceR + ( TokenCons InvisibleBraceL + ( HoleCons ( TokenCons InvisibleBraceR End ) ) + ) + ) + ) + ) + ) + ( Marker "example_cons" ) +, ScanFunctionSymbol + ( TokenCons ParenL + ( HoleCons + ( TokenCons + ( Symbol "," ) + ( HoleCons ( TokenCons ParenR End ) ) + ) + ) + ) + ( Marker "example_pair" ) +, ScanFunctionSymbol ( HoleCons ( TokenCons ( Command "times" ) ( HoleCons End ) diff --git a/test/golden/replace/tokenizing.golden b/test/golden/replace/tokenizing.golden index d32c8ab..06ab46a 100644 --- a/test/golden/replace/tokenizing.golden +++ b/test/golden/replace/tokenizing.golden @@ -1,4 +1,38 @@ [ + [ BeginEnv "signature" + , Label "example_cons" + , BeginEnv "math" + , Command "cons" + , InvisibleBraceL + , Variable "y" + , InvisibleBraceR + , InvisibleBraceL + , Variable "X" + , InvisibleBraceR + , EndEnv "math" + , Word "is" + , Word "a" + , Word "set" + , Symbol "." + , EndEnv "signature" + ] +, + [ BeginEnv "signature" + , Label "example_pair" + , BeginEnv "math" + , ParenL + , Variable "x" + , Symbol "," + , Variable "y" + , ParenR + , EndEnv "math" + , Word "is" + , Word "a" + , Word "set" + , Symbol "." + , EndEnv "signature" + ] +, [ BeginEnv "axiom" , Label "cons" , BeginEnv "math" @@ -138,4 +172,13 @@ , Symbol "." , EndEnv "proposition" ] +, + [ BeginEnv "proof" + , Word "follows" + , Word "by" + , Ref + ( "times" :| [] ) + , Symbol "." + , EndEnv "proof" + ] ]
\ No newline at end of file diff --git a/test/golden/russell/parsing.golden b/test/golden/russell/parsing.golden index 8e680cd..3ab466f 100644 --- a/test/golden/russell/parsing.golden +++ b/test/golden/russell/parsing.golden @@ -266,62 +266,37 @@ ( Location { locFile = "test/examples/russell.tex" , locLine = 14 - , locColumn = 5 + , locColumn = 6 } ) Nothing - ( StmtConnected - { conn = Equivalence - , mloc = Nothing - , stmt1 = StmtFormula - { formula = FormulaChain - ( ChainBase - ( ExprVar - ( NamedVar "R" ) :| [] - ) Positive - ( Relation - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 14 - , locColumn = 12 - } - ) - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) [] - ) - ( ExprVar - ( NamedVar "R" ) :| [] + ( StmtFormula + { formula = FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "R" ) :| [] + ) Positive + ( Relation + ( Location + { locFile = "test/examples/russell.tex" + , locLine = 14 + , locColumn = 7 + } ) + ( RelationSymbol + ( Command "in" ) + ( ParameterArity 0 ) + ( Marker "elem" ) + ) [] ) - } - , stmt2 = StmtFormula - { formula = FormulaChain - ( ChainBase - ( ExprVar - ( NamedVar "R" ) :| [] - ) Negative - ( Relation - ( Location - { locFile = "test/examples/russell.tex" - , locLine = 14 - , locColumn = 29 - } - ) - ( RelationSymbol - ( Command "in" ) - ( ParameterArity 0 ) - ( Marker "elem" ) - ) [] - ) - ( ExprVar - ( NamedVar "R" ) :| [] - ) + ( ExprVar + ( NamedVar "V" ) :| [] ) - } + ) } - ) JustificationEmpty + ) + ( JustificationRef + ( Marker "universal_set" :| [] ) + ) ( Contradiction ( Location { locFile = "test/examples/russell.tex" diff --git a/test/golden/russell/tokenizing.golden b/test/golden/russell/tokenizing.golden index beba3ee..9a739f8 100644 --- a/test/golden/russell/tokenizing.golden +++ b/test/golden/russell/tokenizing.golden @@ -65,19 +65,14 @@ , VisibleBraceR , EndEnv "math" , Symbol "." - , Word "then" , BeginEnv "math" , Variable "R" , Command "in" - , Variable "R" - , EndEnv "math" - , Word "iff" - , BeginEnv "math" - , Variable "R" - , Command "not" - , Command "in" - , Variable "R" + , Variable "V" , EndEnv "math" + , Word "by" + , Ref + ( "universal_set" :| [] ) , Symbol "." , Word "contradiction" , Symbol "." diff --git a/test/golden/union/parsing.golden b/test/golden/union/parsing.golden index 4225bd8..df6361e 100644 --- a/test/golden/union/parsing.golden +++ b/test/golden/union/parsing.golden @@ -1,9 +1,50 @@ -[ BlockAxiom +[ BlockSig ( Location { locFile = "test/examples/union.tex" , locLine = 1 , locColumn = 1 } + ) Nothing + ( Marker "example_union" ) [] + ( SignatureSymbolic + ( SymbolPattern + ( MixfixItem + ( HoleCons + ( TokenCons + ( Command "union" ) ( HoleCons End ) + ) + ) + ( Marker "union" ) LeftAssoc + ) + [ NamedVar "A" + , NamedVar "B" + ] + ) NounPhrase ( [] ) + ( Noun + ( Location + { locFile = "test/examples/union.tex" + , locLine = 2 + , locColumn = 22 + } + ) + ( LexicalItemSgPl + ( SgPl + { sg = TokenCons + ( Word "set" ) End + , pl = TokenCons + ( Word "sets" ) End + } + ) + ( Marker "set" ) + ) [] + ) ( Nothing ) ( [] ) ( Nothing ) + ) +, BlockAxiom + ( Location + { locFile = "test/examples/union.tex" + , locLine = 5 + , locColumn = 1 + } ) ( Just [ Word "extensionality" ] @@ -14,7 +55,7 @@ ( SymbolicQuantified { loc = Location { locFile = "test/examples/union.tex" - , locLine = 2 + , locLine = 6 , locColumn = 13 } , quant = Universally @@ -33,7 +74,7 @@ ( Relation ( Location { locFile = "test/examples/union.tex" - , locLine = 2 + , locLine = 6 , locColumn = 35 } ) @@ -57,7 +98,7 @@ ( Relation ( Location { locFile = "test/examples/union.tex" - , locLine = 2 + , locLine = 6 , locColumn = 48 } ) @@ -85,7 +126,7 @@ ( Relation ( Location { locFile = "test/examples/union.tex" - , locLine = 3 + , locLine = 7 , locColumn = 13 } ) @@ -105,7 +146,7 @@ , BlockAxiom ( Location { locFile = "test/examples/union.tex" - , locLine = 6 + , locLine = 10 , locColumn = 1 } ) Nothing @@ -118,7 +159,7 @@ ( Noun ( Location { locFile = "test/examples/union.tex" - , locLine = 7 + , locLine = 11 , locColumn = 19 } ) @@ -146,7 +187,7 @@ ( Relation ( Location { locFile = "test/examples/union.tex" - , locLine = 8 + , locLine = 12 , locColumn = 7 } ) @@ -159,7 +200,7 @@ ( ExprOp ( Location { locFile = "test/examples/union.tex" - , locLine = 8 + , locLine = 12 , locColumn = 11 } ) @@ -191,7 +232,7 @@ ( Relation ( Location { locFile = "test/examples/union.tex" - , locLine = 8 + , locLine = 12 , locColumn = 28 } ) @@ -215,7 +256,7 @@ ( Relation ( Location { locFile = "test/examples/union.tex" - , locLine = 8 + , locLine = 12 , locColumn = 40 } ) @@ -237,7 +278,7 @@ , BlockClaim Proposition ( Location { locFile = "test/examples/union.tex" - , locLine = 11 + , locLine = 15 , locColumn = 1 } ) Nothing @@ -249,7 +290,7 @@ ( ExprOp ( Location { locFile = "test/examples/union.tex" - , locLine = 12 + , locLine = 16 , locColumn = 6 } ) @@ -270,7 +311,7 @@ ( Relation ( Location { locFile = "test/examples/union.tex" - , locLine = 12 + , locLine = 16 , locColumn = 16 } ) @@ -283,7 +324,7 @@ ( ExprOp ( Location { locFile = "test/examples/union.tex" - , locLine = 12 + , locLine = 16 , locColumn = 18 } ) @@ -308,7 +349,7 @@ , BlockClaim Proposition ( Location { locFile = "test/examples/union.tex" - , locLine = 15 + , locLine = 19 , locColumn = 1 } ) Nothing @@ -320,7 +361,7 @@ ( ExprOp ( Location { locFile = "test/examples/union.tex" - , locLine = 16 + , locLine = 20 , locColumn = 7 } ) @@ -335,7 +376,7 @@ [ ExprOp ( Location { locFile = "test/examples/union.tex" - , locLine = 16 + , locLine = 20 , locColumn = 7 } ) @@ -359,7 +400,7 @@ ( Relation ( Location { locFile = "test/examples/union.tex" - , locLine = 16 + , locLine = 20 , locColumn = 26 } ) @@ -372,7 +413,7 @@ ( ExprOp ( Location { locFile = "test/examples/union.tex" - , locLine = 16 + , locLine = 20 , locColumn = 28 } ) @@ -389,7 +430,7 @@ , ExprOp ( Location { locFile = "test/examples/union.tex" - , locLine = 16 + , locLine = 20 , locColumn = 37 } ) @@ -415,21 +456,21 @@ , BlockProof ( Location { locFile = "test/examples/union.tex" - , locLine = 18 + , locLine = 22 , locColumn = 1 } ) ( Have ( Location { locFile = "test/examples/union.tex" - , locLine = 19 + , locLine = 23 , locColumn = 5 } ) Nothing ( SymbolicQuantified { loc = Location { locFile = "test/examples/union.tex" - , locLine = 19 + , locLine = 23 , locColumn = 5 } , quant = Universally @@ -441,7 +482,7 @@ , mloc = Just ( Location { locFile = "test/examples/union.tex" - , locLine = 19 + , locLine = 23 , locColumn = 25 } ) @@ -454,7 +495,7 @@ ( Relation ( Location { locFile = "test/examples/union.tex" - , locLine = 19 + , locLine = 23 , locColumn = 30 } ) @@ -467,7 +508,7 @@ ( ExprOp ( Location { locFile = "test/examples/union.tex" - , locLine = 19 + , locLine = 23 , locColumn = 35 } ) @@ -482,7 +523,7 @@ [ ExprOp ( Location { locFile = "test/examples/union.tex" - , locLine = 19 + , locLine = 23 , locColumn = 35 } ) @@ -514,7 +555,7 @@ ( Relation ( Location { locFile = "test/examples/union.tex" - , locLine = 19 + , locLine = 23 , locColumn = 63 } ) @@ -527,7 +568,7 @@ ( ExprOp ( Location { locFile = "test/examples/union.tex" - , locLine = 19 + , locLine = 23 , locColumn = 67 } ) @@ -544,7 +585,7 @@ , ExprOp ( Location { locFile = "test/examples/union.tex" - , locLine = 19 + , locLine = 23 , locColumn = 76 } ) @@ -571,14 +612,14 @@ ( Have ( Location { locFile = "test/examples/union.tex" - , locLine = 20 + , locLine = 24 , locColumn = 5 } ) Nothing ( SymbolicQuantified { loc = Location { locFile = "test/examples/union.tex" - , locLine = 20 + , locLine = 24 , locColumn = 5 } , quant = Universally @@ -590,7 +631,7 @@ , mloc = Just ( Location { locFile = "test/examples/union.tex" - , locLine = 20 + , locLine = 24 , locColumn = 25 } ) @@ -603,7 +644,7 @@ ( Relation ( Location { locFile = "test/examples/union.tex" - , locLine = 20 + , locLine = 24 , locColumn = 30 } ) @@ -616,7 +657,7 @@ ( ExprOp ( Location { locFile = "test/examples/union.tex" - , locLine = 20 + , locLine = 24 , locColumn = 34 } ) @@ -633,7 +674,7 @@ , ExprOp ( Location { locFile = "test/examples/union.tex" - , locLine = 20 + , locLine = 24 , locColumn = 43 } ) @@ -663,7 +704,7 @@ ( Relation ( Location { locFile = "test/examples/union.tex" - , locLine = 20 + , locLine = 24 , locColumn = 63 } ) @@ -676,7 +717,7 @@ ( ExprOp ( Location { locFile = "test/examples/union.tex" - , locLine = 20 + , locLine = 24 , locColumn = 68 } ) @@ -691,7 +732,7 @@ [ ExprOp ( Location { locFile = "test/examples/union.tex" - , locLine = 20 + , locLine = 24 , locColumn = 68 } ) @@ -721,7 +762,7 @@ ) ( Location { locFile = "test/examples/union.tex" - , locLine = 21 + , locLine = 25 , locColumn = 1 } ) diff --git a/test/golden/union/scanning.golden b/test/golden/union/scanning.golden index 0637a08..410ced6 100644 --- a/test/golden/union/scanning.golden +++ b/test/golden/union/scanning.golden @@ -1 +1,8 @@ -[]
\ No newline at end of file +[ ScanFunctionSymbol + ( HoleCons + ( TokenCons + ( Command "union" ) ( HoleCons End ) + ) + ) + ( Marker "example_union" ) +]
\ No newline at end of file diff --git a/test/golden/union/tokenizing.golden b/test/golden/union/tokenizing.golden index 1672765..37ce74e 100644 --- a/test/golden/union/tokenizing.golden +++ b/test/golden/union/tokenizing.golden @@ -1,4 +1,18 @@ [ + [ BeginEnv "signature" + , Label "example_union" + , BeginEnv "math" + , Variable "A" + , Command "union" + , Variable "B" + , EndEnv "math" + , Word "is" + , Word "a" + , Word "set" + , Symbol "." + , EndEnv "signature" + ] +, [ BeginEnv "axiom" , BracketL , Word "extensionality" |