From 64a5d0f240a6dda2eed422be614f68de7eb7da79 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 19 Sep 2018 16:00:04 -0700
Subject: [PATCH] refactor(library/init/lean/parser): has_tokens default

---
 library/init/lean/parser/basic.lean       | 5 ++++-
 library/init/lean/parser/combinators.lean | 2 +-
 library/init/lean/parser/level.lean       | 2 +-
 library/init/lean/parser/term.lean        | 2 +-
 library/init/lean/parser/token.lean       | 8 ++++----
 5 files changed, 11 insertions(+), 8 deletions(-)

diff --git a/library/init/lean/parser/basic.lean b/library/init/lean/parser/basic.lean
index 1347c07449..2d3a14704b 100644
--- a/library/init/lean/parser/basic.lean
+++ b/library/init/lean/parser/basic.lean
@@ -63,8 +63,11 @@ f (f a)
 def tokens (r : ρ) [has_tokens r] :=
 donotinline (has_tokens.tokens r)
 
+instance has_tokens.inhabited (r : ρ) : inhabited (has_tokens r) :=
+⟨⟨[]⟩⟩
+
 instance list.nil.tokens : parser.has_tokens ([] : list ρ) :=
-⟨[]⟩
+default _
 instance list.cons.tokens (r : ρ) (rs : list ρ) [parser.has_tokens r] [parser.has_tokens rs] :
   parser.has_tokens (r::rs) :=
 ⟨tokens r ++ tokens rs⟩
diff --git a/library/init/lean/parser/combinators.lean b/library/init/lean/parser/combinators.lean
index 1287815414..9e8415fd6b 100644
--- a/library/init/lean/parser/combinators.lean
+++ b/library/init/lean/parser/combinators.lean
@@ -210,7 +210,7 @@ instance dbg.view (r  : parser) (l) [i : parser.has_view r α] : parser.has_view
 {..i}
 
 instance recurse.tokens (α δ m a) [monad_rec α δ m] : parser.has_tokens (recurse a : m δ) :=
-⟨[]⟩ -- recursive use should not contribute any new tokens
+default _ -- recursive use should not contribute any new tokens
 instance recurse.view (α δ m a) [monad_rec α δ m] : parser.has_view (recurse a : m δ) syntax := default _
 
 def with_recurse {α : Type} (init : α) (r : α → rec_t α syntax m syntax) : parser :=
diff --git a/library/init/lean/parser/level.lean b/library/init/lean/parser/level.lean
index d0a1297281..394d1e92f1 100644
--- a/library/init/lean/parser/level.lean
+++ b/library/init/lean/parser/level.lean
@@ -24,7 +24,7 @@ abbreviation trailing_level_parser := trailing_level_parser_m syntax
 
 /-- Access leading term -/
 def get_leading : trailing_level_parser := read
-instance : has_tokens get_leading := ⟨[]⟩
+instance : has_tokens get_leading := default _
 instance : has_view get_leading syntax := default _
 
 @[derive parser.has_tokens parser.has_view]
diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean
index ca59d3c68e..20dc3b5fa9 100644
--- a/library/init/lean/parser/term.lean
+++ b/library/init/lean/parser/term.lean
@@ -33,7 +33,7 @@ node! term.ident [id: ident.parser, univ: monad_lift ident_univ_spec.parser?]
 namespace term
 /-- Access leading term -/
 def get_leading : trailing_term_parser := read
-instance : has_tokens get_leading := ⟨[]⟩
+instance : has_tokens get_leading := default _
 instance : has_view get_leading syntax := default _
 
 @[derive parser.has_tokens parser.has_view]
diff --git a/library/init/lean/parser/token.lean b/library/init/lean/parser/token.lean
index 605b4dd12f..ccc04a500f 100644
--- a/library/init/lean/parser/token.lean
+++ b/library/init/lean/parser/token.lean
@@ -84,7 +84,7 @@ try $ do
   (ss, info) ← with_source_info (as_substring p) trailing_ws,
   pure $ syntax.atom ⟨info, ss.to_string⟩
 
-instance raw.tokens {α} (p : m α) (t) : parser.has_tokens (raw p t : parser) := ⟨[]⟩
+instance raw.tokens {α} (p : m α) (t) : parser.has_tokens (raw p t : parser) := default _
 instance raw.view {α} (p : m α) (t) : parser.has_view (raw p t : parser) syntax := default _
 
 end
@@ -171,7 +171,7 @@ lift $ try $ do {
   pure stx
 } <?> "number"
 
-instance number.tokens : parser.has_tokens (number : parser) := ⟨[]⟩
+instance number.tokens : parser.has_tokens (number : parser) := default _
 instance number.view : parser.has_view (number : parser) syntax := default _
 
 def ident.parser : parser :=
@@ -181,7 +181,7 @@ lift $ try $ do {
   pure stx
 } <?> "identifier"
 
-instance ident.parser.tokens : parser.has_tokens (ident.parser : parser) := ⟨[]⟩
+instance ident.parser.tokens : parser.has_tokens (ident.parser : parser) := default _
 instance ident.parser.view : parser.has_view (ident.parser : parser) syntax := default _
 
 /-- Check if the following token is the symbol _or_ identifier `sym`. Useful for
@@ -208,7 +208,7 @@ lift $ try $ do
   pure stx
 
 instance symbol_or_ident.tokens (sym) : parser.has_tokens (symbol_or_ident sym : parser) :=
-⟨[]⟩
+default _
 instance symbol_or_ident.view (sym) : parser.has_view (symbol_or_ident sym : parser) syntax := default _
 
 end «parser»