summaryrefslogtreecommitdiff
path: root/test/golden/replace
diff options
context:
space:
mode:
Diffstat (limited to 'test/golden/replace')
-rw-r--r--test/golden/replace/parsing.golden178
-rw-r--r--test/golden/replace/scanning.golden24
-rw-r--r--test/golden/replace/tokenizing.golden43
3 files changed, 217 insertions, 28 deletions
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
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-06 19:24:52 +0000