From f63734cba490b80cbb14284fab4e0b680c8cfaa5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 4 Oct 2022 17:14:48 -0700 Subject: [PATCH] chore: unexpanders for `Name.mkStr*` and `Array.mkArray*` closes #1675 --- src/Init/NotationExtra.lean | 64 +++++++++++++++++++ tests/lean/1321.lean.expected.out | 5 +- tests/lean/586.lean.expected.out | 2 +- tests/lean/macroResolveName.lean.expected.out | 4 +- tests/lean/ppNotationCode.lean.expected.out | 42 +++++------- .../syntaxInNamespacesAndPP.lean.expected.out | 5 +- 6 files changed, 88 insertions(+), 34 deletions(-) diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean index 0f92f53238..a79ad63bd0 100644 --- a/src/Init/NotationExtra.lean +++ b/src/Init/NotationExtra.lean @@ -210,6 +210,70 @@ syntax (name := calcTactic) "calc" ppLine withPosition(calcStep) ppLine withPosi | `($_ $array $index) => `($array[$index]?) | _ => throw () +@[appUnexpander Name.mkStr1] def unexpandMkStr1 : Lean.PrettyPrinter.Unexpander + | `($(_) $a:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a.getString}"] + | _ => throw () + +@[appUnexpander Name.mkStr2] def unexpandMkStr2 : Lean.PrettyPrinter.Unexpander + | `($(_) $a1:str $a2:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}"] + | _ => throw () + +@[appUnexpander Name.mkStr3] def unexpandMkStr3 : Lean.PrettyPrinter.Unexpander + | `($(_) $a1:str $a2:str $a3:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}"] + | _ => throw () + +@[appUnexpander Name.mkStr4] def unexpandMkStr4 : Lean.PrettyPrinter.Unexpander + | `($(_) $a1:str $a2:str $a3:str $a4:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}.{a4.getString}"] + | _ => throw () + +@[appUnexpander Name.mkStr5] def unexpandMkStr5 : Lean.PrettyPrinter.Unexpander + | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}.{a4.getString}.{a5.getString}"] + | _ => throw () + +@[appUnexpander Name.mkStr6] def unexpandMkStr6 : Lean.PrettyPrinter.Unexpander + | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}.{a4.getString}.{a5.getString}.{a6.getString}"] + | _ => throw () + +@[appUnexpander Name.mkStr7] def unexpandMkStr7 : Lean.PrettyPrinter.Unexpander + | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str $a7:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}.{a4.getString}.{a5.getString}.{a6.getString}.{a7.getString}"] + | _ => throw () + +@[appUnexpander Name.mkStr8] def unexpandMkStr8 : Lean.PrettyPrinter.Unexpander + | `($(_) $a1:str $a2:str $a3:str $a4:str $a5:str $a6:str $a7:str $a8:str) => return mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit s!"`{a1.getString}.{a2.getString}.{a3.getString}.{a4.getString}.{a5.getString}.{a6.getString}.{a7.getString}.{a8.getString}"] + | _ => throw () + +@[appUnexpander Array.mkArray1] def unexpandMkArray1 : Lean.PrettyPrinter.Unexpander + | `($(_) $a1) => `(#[$a1]) + | _ => throw () + +@[appUnexpander Array.mkArray2] def unexpandMkArray2 : Lean.PrettyPrinter.Unexpander + | `($(_) $a1 $a2) => `(#[$a1, $a2]) + | _ => throw () + +@[appUnexpander Array.mkArray3] def unexpandMkArray3 : Lean.PrettyPrinter.Unexpander + | `($(_) $a1 $a2 $a3) => `(#[$a1, $a2, $a3]) + | _ => throw () + +@[appUnexpander Array.mkArray4] def unexpandMkArray4 : Lean.PrettyPrinter.Unexpander + | `($(_) $a1 $a2 $a3 $a4) => `(#[$a1, $a2, $a3, $a4]) + | _ => throw () + +@[appUnexpander Array.mkArray5] def unexpandMkArray5 : Lean.PrettyPrinter.Unexpander + | `($(_) $a1 $a2 $a3 $a4 $a5) => `(#[$a1, $a2, $a3, $a4, $a5]) + | _ => throw () + +@[appUnexpander Array.mkArray6] def unexpandMkArray6 : Lean.PrettyPrinter.Unexpander + | `($(_) $a1 $a2 $a3 $a4 $a5 $a6) => `(#[$a1, $a2, $a3, $a4, $a5, $a6]) + | _ => throw () + +@[appUnexpander Array.mkArray7] def unexpandMkArray7 : Lean.PrettyPrinter.Unexpander + | `($(_) $a1 $a2 $a3 $a4 $a5 $a6 $a7) => `(#[$a1, $a2, $a3, $a4, $a5, $a6, $a7]) + | _ => throw () + +@[appUnexpander Array.mkArray8] def unexpandMkArray8 : Lean.PrettyPrinter.Unexpander + | `($(_) $a1 $a2 $a3 $a4 $a5 $a6 $a7 $a8) => `(#[$a1, $a2, $a3, $a4, $a5, $a6, $a7, $a8]) + | _ => throw () + /-- Apply function extensionality and introduce new hypotheses. The tactic `funext` will keep applying new the `funext` lemma until the goal target is not reducible to diff --git a/tests/lean/1321.lean.expected.out b/tests/lean/1321.lean.expected.out index 6edf9db8b6..2b81ffa6ba 100644 --- a/tests/lean/1321.lean.expected.out +++ b/tests/lean/1321.lean.expected.out @@ -1,5 +1,4 @@ @[reducible] def fooParser : Lean.ParserDescr := -Lean.ParserDescr.node (Lean.Name.mkStr1 "fooParser") 1022 - (Lean.ParserDescr.binary (Lean.Name.mkStr1 "andthen") (Lean.ParserDescr.symbol "foo") - (Lean.ParserDescr.cat (Lean.Name.mkStr1 "term") 0)) +Lean.ParserDescr.node `fooParser 1022 + (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "foo") (Lean.ParserDescr.cat `term 0)) 5 + 1 : Nat diff --git a/tests/lean/586.lean.expected.out b/tests/lean/586.lean.expected.out index 41b43a182d..4ff6ac93cd 100644 --- a/tests/lean/586.lean.expected.out +++ b/tests/lean/586.lean.expected.out @@ -1,4 +1,4 @@ Nat.zero : Nat -Lean.Name.mkStr2 "Nat" "succ" : Lean.Name +`Nat.succ : Lean.Name 586.lean:13:0-13:3: error: unknown identifier 'zero✝' 586.lean:13:0-13:3: error: unknown constant 'succ✝' diff --git a/tests/lean/macroResolveName.lean.expected.out b/tests/lean/macroResolveName.lean.expected.out index 500c425dcc..736f51c7b1 100644 --- a/tests/lean/macroResolveName.lean.expected.out +++ b/tests/lean/macroResolveName.lean.expected.out @@ -1,2 +1,2 @@ -[Name.mkStr2 "Lean" "Macro"] : List Name -[(Lean.Name.mkStr2 "Nat" "succ", [])] : List (Lean.Name × List ?m) +[`Lean.Macro] : List Name +[(`Nat.succ, [])] : List (Lean.Name × List ?m) diff --git a/tests/lean/ppNotationCode.lean.expected.out b/tests/lean/ppNotationCode.lean.expected.out index 989a8dad87..0520b04388 100644 --- a/tests/lean/ppNotationCode.lean.expected.out +++ b/tests/lean/ppNotationCode.lean.expected.out @@ -1,11 +1,10 @@ [Elab.definition.body] «term_+++_» : Lean.TrailingParserDescr := - Lean.ParserDescr.trailingNode (Lean.Name.mkStr1 "term_+++_") 45 46 - (Lean.ParserDescr.binary (Lean.Name.mkStr1 "andthen") (Lean.ParserDescr.symbol "+++") - (Lean.ParserDescr.cat (Lean.Name.mkStr1 "term") 46)) + Lean.ParserDescr.trailingNode `term_+++_ 45 46 + (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "+++") (Lean.ParserDescr.cat `term 46)) [Elab.definition.body] «_aux_ppNotationCode___macroRules_term_+++__1» : Lean.Macro := fun x => let discr := x; - if Lean.Syntax.isOfKind discr (Lean.Name.mkStr1 "term_+++_") = true then + if Lean.Syntax.isOfKind discr `term_+++_ = true then let discr_1 := Lean.Syntax.getArg discr 0; let discr_2 := Lean.Syntax.getArg discr 1; let discr := Lean.Syntax.getArg discr 2; @@ -17,22 +16,20 @@ let mainModule ← Lean.getMainModule pure { raw := - Lean.Syntax.node info (Lean.Name.mkStr4 "Lean" "Parser" "Term" "app") - (Array.mkArray2 - (Lean.Syntax.ident info (String.toSubstring' "Nat.add") - (Lean.addMacroScope mainModule (Lean.Name.mkStr2 "Nat" "add") scp) - [Lean.Syntax.Preresolved.decl (Lean.Name.mkStr2 "Nat" "add") [], - Lean.Syntax.Preresolved.namespace (Lean.Name.mkStr2 "Nat" "add")]) - (Lean.Syntax.node info (Lean.Name.mkStr1 "null") (Array.mkArray2 lhs.raw rhs.raw))) }.raw + Lean.Syntax.node info `Lean.Parser.Term.app + #[Lean.Syntax.ident info (String.toSubstring' "Nat.add") + (Lean.addMacroScope mainModule `Nat.add scp) + [Lean.Syntax.Preresolved.decl `Nat.add [], Lean.Syntax.Preresolved.namespace `Nat.add], + Lean.Syntax.node info `null #[lhs.raw, rhs.raw]] }.raw else let discr := x; throw Lean.Macro.Exception.unsupportedSyntax [Elab.definition.body] _aux_ppNotationCode___unexpand_Nat_add_1 : Lean.PrettyPrinter.Unexpander := fun x => let discr := x; - if Lean.Syntax.isOfKind discr (Lean.Name.mkStr4 "Lean" "Parser" "Term" "app") = true then + if Lean.Syntax.isOfKind discr `Lean.Parser.Term.app = true then let discr_1 := Lean.Syntax.getArg discr 0; - bif false || Lean.Syntax.isOfKind discr_1 (Lean.Name.mkStr1 "ident") then + bif false || Lean.Syntax.isOfKind discr_1 `ident then let discr_2 := Lean.Syntax.getArg discr 1; if Lean.Syntax.matchesNull discr_2 2 = true then let discr := Lean.Syntax.getArg discr_2 0; @@ -44,18 +41,15 @@ let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule - pure - { raw := - Lean.Syntax.node info (Lean.Name.mkStr1 "term_+++_") - (Array.mkArray3 lhs.raw (Lean.Syntax.atom info "+++") rhs.raw) }.raw + pure { raw := Lean.Syntax.node info `term_+++_ #[lhs.raw, Lean.Syntax.atom info "+++", rhs.raw] }.raw else let discr := Lean.Syntax.getArg discr 1; throw () else let discr_2 := Lean.Syntax.getArg discr 0; - if Lean.Syntax.isOfKind discr_2 (Lean.Name.mkStr4 "Lean" "Parser" "Term" "app") = true then + if Lean.Syntax.isOfKind discr_2 `Lean.Parser.Term.app = true then let discr_3 := Lean.Syntax.getArg discr_2 0; - bif false || Lean.Syntax.isOfKind discr_3 (Lean.Name.mkStr1 "ident") then + bif false || Lean.Syntax.isOfKind discr_3 `ident then let discr_4 := Lean.Syntax.getArg discr_2 1; if Lean.Syntax.matchesNull discr_4 2 = true then let discr_5 := Lean.Syntax.getArg discr_4 0; @@ -71,12 +65,10 @@ let _ ← Lean.getMainModule pure { raw := - Lean.Syntax.node info (Lean.Name.mkStr4 "Lean" "Parser" "Term" "app") - (Array.mkArray2 - (Lean.Syntax.node info (Lean.Name.mkStr1 "term_+++_") - (Array.mkArray3 lhs.raw (Lean.Syntax.atom info "+++") rhs.raw)) - (Lean.Syntax.node info (Lean.Name.mkStr1 "null") - (Array.append Array.mkArray0 (Lean.TSyntaxArray.raw moreArgs)))) }.raw + Lean.Syntax.node info `Lean.Parser.Term.app + #[Lean.Syntax.node info `term_+++_ #[lhs.raw, Lean.Syntax.atom info "+++", rhs.raw], + Lean.Syntax.node info `null + (Array.append Array.mkArray0 (Lean.TSyntaxArray.raw moreArgs))] }.raw else let discr_5 := Lean.Syntax.getArg discr_2 1; let discr := Lean.Syntax.getArg discr 1; diff --git a/tests/lean/syntaxInNamespacesAndPP.lean.expected.out b/tests/lean/syntaxInNamespacesAndPP.lean.expected.out index 504c2eadf5..47aa41c141 100644 --- a/tests/lean/syntaxInNamespacesAndPP.lean.expected.out +++ b/tests/lean/syntaxInNamespacesAndPP.lean.expected.out @@ -1,6 +1,5 @@ true : Bool true : Bool def Bla.bla : Lean.ParserDescr := -Lean.ParserDescr.node (Lean.Name.mkStr2 "Bla" "bla") 1022 - (Lean.ParserDescr.binary (Lean.Name.mkStr1 "andthen") (Lean.ParserDescr.symbol "bla") - (Lean.ParserDescr.cat (Lean.Name.mkStr1 "term") 0)) +Lean.ParserDescr.node `Bla.bla 1022 + (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "bla") (Lean.ParserDescr.cat `term 0))