From 126da8185d8d71bb85610d9422c2e4b7248fc8ac Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 29 Sep 2022 16:48:13 -0700 Subject: [PATCH] feat: more compact quotations Trying to control the generated code size. --- src/Init/Meta.lean | 45 +++++++++++++++++---- src/Init/Prelude.lean | 38 ++++++++++++++++- tests/lean/ppNotationCode.lean.expected.out | 20 ++++++--- 3 files changed, 89 insertions(+), 14 deletions(-) diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index 83266e9fdc..e733479757 100644 --- a/src/Init/Meta.lean +++ b/src/Init/Meta.lean @@ -937,10 +937,10 @@ export Quote (quote) instance [Quote α k] [CoeHTCT (TSyntax k) (TSyntax [k'])] : Quote α k' := ⟨fun a => quote (k := k) a⟩ instance : Quote Term := ⟨id⟩ -instance : Quote Bool := ⟨fun | true => mkCIdent `Bool.true | false => mkCIdent `Bool.false⟩ +instance : Quote Bool := ⟨fun | true => mkCIdent ``Bool.true | false => mkCIdent ``Bool.false⟩ instance : Quote String strLitKind := ⟨Syntax.mkStrLit⟩ instance : Quote Nat numLitKind := ⟨fun n => Syntax.mkNumLit <| toString n⟩ -instance : Quote Substring := ⟨fun s => Syntax.mkCApp `String.toSubstring #[quote s.toString]⟩ +instance : Quote Substring := ⟨fun s => Syntax.mkCApp ``String.toSubstring' #[quote s.toString]⟩ -- in contrast to `Name.toString`, we can, and want to be, precise here private def getEscapedNameParts? (acc : List String) : Name → Option (List String) @@ -950,10 +950,28 @@ private def getEscapedNameParts? (acc : List String) : Name → Option (List Str getEscapedNameParts? (s::acc) n | Name.num _ _ => none -def quoteNameMk : Name → Term - | Name.anonymous => mkCIdent ``Name.anonymous - | Name.str n s => Syntax.mkCApp ``Name.mkStr #[quoteNameMk n, quote s] - | Name.num n i => Syntax.mkCApp ``Name.mkNum #[quoteNameMk n, quote i] +def quoteNameMk (n : Name) : Term := + if isSimple n 0 then + mkStr n 0 #[] + else + go n +where + isSimple (n : Name) (sz : Nat) : Bool := + match n with + | .anonymous => 0 < sz && sz <= 8 + | .str p _ => isSimple p (sz+1) + | _ => false + + mkStr (n : Name) (sz : Nat) (args : Array Term) : Term := + match n with + | .anonymous => Syntax.mkCApp (Name.mkStr3 "Lean" "Name" ("mkStr" ++ toString sz)) args.reverse + | .str p s => mkStr p (sz+1) (args.push (quote s)) + | _ => unreachable! + + go : Name → Term + | Name.anonymous => mkCIdent ``Name.anonymous + | Name.str n s => Syntax.mkCApp ``Name.mkStr #[go n, quote s] + | Name.num n i => Syntax.mkCApp ``Name.mkNum #[go n, quote i] instance : Quote Name `term where quote n := match getEscapedNameParts? [] n with @@ -971,8 +989,21 @@ private def quoteList [Quote α `term] : List α → Term instance [Quote α `term] : Quote (List α) `term where quote := quoteList +private def quoteArray [Quote α `term] (xs : Array α) : Term := + if xs.size <= 8 then + go 0 #[] + else + Syntax.mkCApp ``List.toArray #[quote xs.toList] +where + go (i : Nat) (args : Array Term) : Term := + if h : i < xs.size then + go (i+1) (args.push (quote xs[i])) + else + Syntax.mkCApp (Name.mkStr2 "Array" ("mkArray" ++ toString xs.size)) args +termination_by go i _ => xs.size - i + instance [Quote α `term] : Quote (Array α) `term where - quote xs := Syntax.mkCApp ``List.toArray #[quote xs.toList] + quote := quoteArray instance Option.hasQuote {α : Type} [Quote α `term] : Quote (Option α) `term where quote diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 69883312b4..de1805737d 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -2341,6 +2341,10 @@ instance (p₁ p₂ : String.Pos) : Decidable (LT.lt p₁ p₂) := startPos := {} stopPos := s.endPos +/-- `String.toSubstring` without `[inline]` annotation. -/ +def String.toSubstring' (s : String) : Substring := + s.toSubstring + /-- This function will cast a value of type `α` to type `β`, and is a no-op in the compiler. This function is **extremely dangerous** because there is no guarantee @@ -3363,7 +3367,39 @@ abbrev mkNum (p : Name) (v : Nat) : Name := Short for `.str .anonymous s`. -/ abbrev mkSimple (s : String) : Name := - mkStr Name.anonymous s + .str .anonymous s + +/-- Make name `s₁` -/ +def mkStr1 (s₁ : String) : Name := + .str .anonymous s₁ + +/-- Make name `s₁.s₂` -/ +def mkStr2 (s₁ s₂ : String) : Name := + .str (.str .anonymous s₁) s₂ + +/-- Make name `s₁.s₂.s₃` -/ +def mkStr3 (s₁ s₂ s₃ : String) : Name := + .str (.str (.str .anonymous s₁) s₂) s₃ + +/-- Make name `s₁.s₂.s₃.s₄` -/ +def mkStr4 (s₁ s₂ s₃ s₄ : String) : Name := + .str (.str (.str (.str .anonymous s₁) s₂) s₃) s₄ + +/-- Make name `s₁.s₂.s₃.s₄.s₅` -/ +def mkStr5 (s₁ s₂ s₃ s₄ s₅ : String) : Name := + .str (.str (.str (.str (.str .anonymous s₁) s₂) s₃) s₄) s₅ + +/-- Make name `s₁.s₂.s₃.s₄.s₅.s₆` -/ +def mkStr6 (s₁ s₂ s₃ s₄ s₅ s₆ : String) : Name := + .str (.str (.str (.str (.str (.str .anonymous s₁) s₂) s₃) s₄) s₅) s₆ + +/-- Make name `s₁.s₂.s₃.s₄.s₅.s₆.s₇` -/ +def mkStr7 (s₁ s₂ s₃ s₄ s₅ s₆ s₇ : String) : Name := + .str (.str (.str (.str (.str (.str (.str .anonymous s₁) s₂) s₃) s₄) s₅) s₆) s₇ + +/-- Make name `s₁.s₂.s₃.s₄.s₅.s₆.s₇.s₈` -/ +def mkStr8 (s₁ s₂ s₃ s₄ s₅ s₆ s₇ s₈ : String) : Name := + .str (.str (.str (.str (.str (.str (.str (.str .anonymous s₁) s₂) s₃) s₄) s₅) s₆) s₇) s₈ /-- (Boolean) equality comparator for names. -/ @[extern "lean_name_eq"] diff --git a/tests/lean/ppNotationCode.lean.expected.out b/tests/lean/ppNotationCode.lean.expected.out index a15f338528..b5f3598855 100644 --- a/tests/lean/ppNotationCode.lean.expected.out +++ b/tests/lean/ppNotationCode.lean.expected.out @@ -17,9 +17,11 @@ pure { 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 + (Array.mkArray2 + (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 (Array.mkArray2 lhs.raw rhs.raw))) }.raw else let discr := x; throw Lean.Macro.Exception.unsupportedSyntax @@ -40,7 +42,10 @@ let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule - pure { raw := Lean.Syntax.node info `«term_+++_» #[lhs.raw, Lean.Syntax.atom info "+++", rhs.raw] }.raw + pure + { raw := + Lean.Syntax.node info `«term_+++_» + (Array.mkArray3 lhs.raw (Lean.Syntax.atom info "+++") rhs.raw) }.raw else let discr := Lean.Syntax.getArg discr 1; throw () @@ -65,8 +70,11 @@ pure { 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 #[] (Lean.TSyntaxArray.raw moreArgs))] }.raw + (Array.mkArray2 + (Lean.Syntax.node info `«term_+++_» + (Array.mkArray3 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;