feat: more compact quotations
Trying to control the generated code size.
This commit is contained in:
Leonardo de Moura
parent
b4454902c1
commit
126da8185d
3 changed files with 89 additions and 14 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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"]
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue