08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
54 lines
2.4 KiB
Text
54 lines
2.4 KiB
Text
[Elab.definition.body] «term_+++_» : Lean.TrailingParserDescr :=
|
|
Lean.ParserDescr.trailingNode `«term_+++_» 45 46
|
|
(Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "+++") (Lean.ParserDescr.cat `term 46))
|
|
[Elab.definition.body] «_aux_elab_ppNotationCode___macroRules_term_+++__1» : Lean.Macro :=
|
|
fun x =>
|
|
have __discr := x;
|
|
if __discr.isOfKind `«term_+++_» = true then
|
|
have __discr_1 := __discr.getArg 0;
|
|
have __discr_2 := __discr.getArg 1;
|
|
have __discr := __discr.getArg 2;
|
|
have rhs := { raw := __discr };
|
|
have lhs := { raw := __discr_1 };
|
|
do
|
|
let info ← Lean.MonadRef.mkInfoFromRefPos
|
|
let scp ← Lean.getCurrMacroScope
|
|
let quotCtx ← Lean.MonadQuotation.getContext
|
|
pure
|
|
{
|
|
raw :=
|
|
Lean.Syntax.node2 info `Lean.Parser.Term.app
|
|
(Lean.Syntax.ident info "Nat.add".toRawSubstring' (Lean.addMacroScope quotCtx `Nat.add scp)
|
|
[Lean.Syntax.Preresolved.decl `Nat.add [], Lean.Syntax.Preresolved.namespace `Nat.add])
|
|
(Lean.Syntax.node2 info `null lhs.raw rhs.raw) }.raw
|
|
else
|
|
have __discr := x;
|
|
throw Lean.Macro.Exception.unsupportedSyntax
|
|
[Elab.definition.body] _aux_elab_ppNotationCode___unexpand_Nat_add_1 : Lean.PrettyPrinter.Unexpander :=
|
|
fun x =>
|
|
have __discr := x;
|
|
if __discr.isOfKind `Lean.Parser.Term.app = true then
|
|
have __discr_1 := __discr.getArg 0;
|
|
bif false || __discr_1.isOfKind `ident then
|
|
have __discr_2 := __discr.getArg 1;
|
|
if __discr_2.matchesNull 2 = true then
|
|
have __discr := __discr_2.getArg 0;
|
|
have __discr_3 := __discr_2.getArg 1;
|
|
have rhs := { raw := __discr_3 };
|
|
have lhs := { raw := __discr };
|
|
have f := { raw := __discr_1 };
|
|
Lean.withRef f.raw do
|
|
let info ← Lean.MonadRef.mkInfoFromRefPos
|
|
let _ ← Lean.getCurrMacroScope
|
|
let _ ← Lean.MonadQuotation.getContext
|
|
pure { raw := Lean.Syntax.node3 info `«term_+++_» lhs.raw (Lean.Syntax.atom info "+++") rhs.raw }.raw
|
|
else
|
|
have __discr := __discr.getArg 1;
|
|
throw ()
|
|
else
|
|
have __discr_2 := __discr.getArg 0;
|
|
have __discr := __discr.getArg 1;
|
|
throw ()
|
|
else
|
|
have __discr := x;
|
|
throw ()
|