From 287fdce45b44b75b657354e628cc3b6e430ea4cc Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 22 Aug 2018 09:41:25 -0700
Subject: [PATCH] refactor(library/init/lean/parser/reader): remove
 `reader.has_view` default instance

---
 library/init/lean/parser/reader/basic.lean  |  7 ++++---
 library/init/lean/parser/reader/module.lean | 12 ++++++++++++
 library/init/lean/parser/reader/term.lean   |  1 +
 3 files changed, 17 insertions(+), 3 deletions(-)

diff --git a/library/init/lean/parser/reader/basic.lean b/library/init/lean/parser/reader/basic.lean
index 2644e97d8d..62019e2ab9 100644
--- a/library/init/lean/parser/reader/basic.lean
+++ b/library/init/lean/parser/reader/basic.lean
@@ -81,9 +81,8 @@ class reader.has_view (r : reader) (α : out_param Type) :=
 (view : syntax → option α)
 (review : α → syntax)
 
-@[priority 0] instance reader.has_view.default (r) : reader.has_view r syntax :=
-{ view := some,
-  review := id }
+instance reader.has_view.default (r : reader) : inhabited (reader.has_view r syntax) :=
+⟨{ view := some, review := id }⟩
 
 class macro.has_view (m : macro) (α : out_param Type) :=
 (view : syntax → option α)
@@ -258,6 +257,8 @@ def any_of (rs : list reader) : reader :=
     | (r::rs) := (rs.map reader.read).foldl (<|>) r.read),
   tokens := (rs.map reader.tokens).join }
 
+instance any_of.view (rs) : reader.has_view (any_of rs) syntax := default _
+
 /-- Parse a list `[p1, ..., pn]` of readers as `p1 <|> ... <|> pn`.
     The result will be wrapped in a node with the the index of the successful
     parser as the name. -/
diff --git a/library/init/lean/parser/reader/module.lean b/library/init/lean/parser/reader/module.lean
index 28fd2a3a8a..f7ab7e654b 100644
--- a/library/init/lean/parser/reader/module.lean
+++ b/library/init/lean/parser/reader/module.lean
@@ -20,6 +20,14 @@ local postfix `?`:10000 := optional
 local postfix *:10000 := many
 local postfix +:10000 := many1
 
+instance symbol.view (s) : reader.has_view (symbol s) syntax := default _
+instance raw_symbol.view (s) : reader.has_view (raw_symbol s) syntax := default _
+instance number.view : reader.has_view number syntax := default _
+instance ident.view : reader.has_view ident syntax := default _
+instance recurse.view : reader.has_view recurse syntax := default _
+instance with_recurse.view (r) : reader.has_view (with_recurse r) syntax := default _
+
+@[derive reader.has_view]
 def prelude.reader : reader :=
 node! «prelude» ["prelude"]
 
@@ -30,6 +38,7 @@ node! import_path [
   dirups: (raw_symbol ".")*,
   module: ident]
 
+@[derive reader.has_view]
 def import.reader : reader :=
 node! «import» ["import", imports: import_path.reader+]
 
@@ -67,6 +76,8 @@ def quoted_symbol : reader :=
 { read := do (s, info) ← with_source_info $ take_until (= '`'),
    pure $ syntax.atom ⟨info, atomic_val.string s⟩ }
 
+instance quoted_symbol.view : reader.has_view quoted_symbol syntax := default _
+
 @[derive reader.has_view]
 def notation_quoted_symbol.reader : reader :=
 node! notation_quoted_symbol [
@@ -144,6 +155,7 @@ node! «reserve_mixfix» [
   try ["reserve", kind: mixfix.kind.reader],
   sym: notation_symbol.reader]
 
+@[derive reader.has_view]
 def command.reader :=
 with_recurse $ any_of [open.reader, section.reader, universe.reader, notation.reader, reserve_notation.reader,
   mixfix.reader, reserve_mixfix.reader] <?> "command"
diff --git a/library/init/lean/parser/reader/term.lean b/library/init/lean/parser/reader/term.lean
index 234798cee4..63776e290f 100644
--- a/library/init/lean/parser/reader/term.lean
+++ b/library/init/lean/parser/reader/term.lean
@@ -17,6 +17,7 @@ def hole := {macro . name := `hole}
 def hole.reader : reader :=
 node hole [symbol "_"]
 
+@[derive reader.has_view]
 def term.reader :=
 any_of [
   hole.reader