max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: move Lean.quote to LeanInit

Browse source 
cc @Kha
This commit is contained in:
Leonardo de Moura 2020-09-17 07:51:06 -07:00
parent 9d1f2b644f
commit f4aabaecae
2 changed files with 37 additions and 37 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

37
src/Init/LeanInit.lean
View file

@ -762,6 +762,43 @@ def find? (stx : Syntax) (p : Syntax → Bool) : Option Syntax :=
findAux p stx
end Syntax
/-- Reflect a runtime datum back to surface syntax (best-effort). -/
class HasQuote (α : Type) :=
(quote : α → Syntax)
export HasQuote (quote)
instance Syntax.HasQuote : HasQuote Syntax := ⟨id⟩
instance String.HasQuote : HasQuote String := ⟨mkStxStrLit⟩
instance Nat.HasQuote : HasQuote Nat := ⟨fun n => mkStxNumLit $ toString n⟩
instance Substring.HasQuote : HasQuote Substring := ⟨fun s => mkCAppStx `String.toSubstring #[quote s.toString]⟩
private def quoteName : Name → Syntax
| Name.anonymous => mkCIdent `Lean.Name.anonymous
| Name.str n s _ => mkCAppStx `Lean.mkNameStr #[quoteName n, quote s]
| Name.num n i _ => mkCAppStx `Lean.mkNameNum #[quoteName n, quote i]
instance Name.hasQuote : HasQuote Name := ⟨quoteName⟩
instance Prod.hasQuote {α β : Type} [HasQuote α] [HasQuote β] : HasQuote (α × β) :=
⟨fun ⟨a, b⟩ => mkCAppStx `Prod.mk #[quote a, quote b]⟩
private def quoteList {α : Type} [HasQuote α] : List α → Syntax
| [] => mkCIdent `List.nil
| (x::xs) => mkCAppStx `List.cons #[quote x, quoteList xs]
instance List.hasQuote {α : Type} [HasQuote α] : HasQuote (List α) := ⟨quoteList⟩
instance Array.hasQuote {α : Type} [HasQuote α] : HasQuote (Array α) :=
⟨fun xs => mkCAppStx `List.toArray #[quote xs.toList]⟩
private def quoteOption {α : Type} [HasQuote α] : Option α → Syntax
| none => mkIdent `Option.none
| (some x) => mkCAppStx `Option.some #[quote x]
instance Option.hasQuote {α : Type} [HasQuote α] : HasQuote (Option α) := ⟨quoteOption⟩
end Lean
namespace Array

37
src/Lean/Syntax.lean
View file

@ -431,41 +431,4 @@ mkStxStrLit val
def mkStxNumLitAux (val : Nat) : Syntax :=
mkStxNumLit (toString val)
/-- Reflect a runtime datum back to surface syntax (best-effort). -/
class HasQuote (α : Type) :=
(quote : α → Syntax)
export HasQuote (quote)
instance Syntax.HasQuote : HasQuote Syntax := ⟨id⟩
instance String.HasQuote : HasQuote String := ⟨mkStxStrLit⟩
instance Nat.HasQuote : HasQuote Nat := ⟨fun n => mkStxNumLit $ toString n⟩
instance Substring.HasQuote : HasQuote Substring := ⟨fun s => mkCAppStx `String.toSubstring #[quote s.toString]⟩
private def quoteName : Name → Syntax
| Name.anonymous => mkCIdent `Lean.Name.anonymous
| Name.str n s _ => mkCAppStx `Lean.mkNameStr #[quoteName n, quote s]
| Name.num n i _ => mkCAppStx `Lean.mkNameNum #[quoteName n, quote i]
instance Name.hasQuote : HasQuote Name := ⟨quoteName⟩
instance Prod.hasQuote {α β : Type} [HasQuote α] [HasQuote β] : HasQuote (α × β) :=
⟨fun ⟨a, b⟩ => mkCAppStx `Prod.mk #[quote a, quote b]⟩
private def quoteList {α : Type} [HasQuote α] : List α → Syntax
| [] => mkCIdent `List.nil
| (x::xs) => mkCAppStx `List.cons #[quote x, quoteList xs]
instance List.hasQuote {α : Type} [HasQuote α] : HasQuote (List α) := ⟨quoteList⟩
instance Array.hasQuote {α : Type} [HasQuote α] : HasQuote (Array α) :=
⟨fun xs => mkCAppStx `List.toArray #[quote xs.toList]⟩
private def quoteOption {α : Type} [HasQuote α] : Option α → Syntax
| none => mkIdent `Option.none
| (some x) => mkCAppStx `Option.some #[quote x]
instance Option.hasQuote {α : Type} [HasQuote α] : HasQuote (Option α) := ⟨quoteOption⟩
end Lean