refactor(library/init/lean/parser/term): factor out opt_type parser

library/init/lean/elaborator.lean

@@ -194,7 +194,7 @@ def to_pexpr : syntax → elaborator_m expr
     let fn_name := `_match_fn,
     fn ← expr.lam fn_name -- TODO: unhygienic
       binder_info.default
-      <$> to_pexpr ((match_type.view.type <$> v.type).get_or_else $ review hole {}),
+      <$> to_pexpr (get_opt_type v.type),
     eqns ← match v.equations with
     | [] := pure [fn $ expr.mdata (kvmap.set_bool {} `no_equation ff) dummy]
     | eqns := (eqns.map sep_by.elem.view.item).mmap $ λ (eqn : match_equation.view), do {

library/init/lean/expander.lean

@@ -210,6 +210,10 @@ def binder_ident_to_ident : binder_ident.view → syntax_ident
 | (binder_ident.view.id id)  := id
 | (binder_ident.view.hole _) := "a"
 
+def get_opt_type : option opt_type.view → syntax
+| none     := review hole {}
+| (some v) := v.type
+
 def expand_bracketed_binder : bracketed_binder.view → transform_m (list simple_binder.view)
 -- local notation: should have been handled by caller, erase
 | (bracketed_binder.view.explicit {content := explicit_binder_content.view.notation _}) := pure []
@@ -227,7 +231,7 @@ def expand_bracketed_binder : bracketed_binder.view → transform_m (list simple
       | inst_implicit_binder_content.view.named bcn :=
         {ids := [bcn.id], type := some {type := bcn.type}})
   | bracketed_binder.view.anonymous_constructor _ := (binder_info.default, {ids := []}) /- unreachable -/),
-  let type := (binder_content_type.view.type <$> bc.type).get_or_else $ review hole {},
+  let type := get_opt_type bc.type,
   type ← match bc.default with
   | none := pure type
   | some (binder_default.view.val bdv) := pure $ mk_app (glob_id `opt_param) [type, bdv.term]

library/init/lean/parser/combinators.lean

@@ -237,6 +237,7 @@ instance coe.tokens {β} (r : parser) [parser.has_tokens r] [has_coe_t parser β
 ⟨tokens r⟩
 instance coe.view {β} (r : parser) [i : parser.has_view α r] [has_coe_t parser β] : parser.has_view α (coe r : β) :=
 {..i}
+instance coe.view_default {β} (d : α) (r : parser) [has_view α r] [parser.has_view_default r α d] [has_coe_t parser β] : parser.has_view_default (coe r : β) α d := ⟨⟩
 
 end combinators
 end parser

library/init/lean/parser/declaration.lean

@@ -56,7 +56,7 @@ node! decl_modifiers [
 def decl_sig.parser : command_parser :=
 node! decl_sig [
   params: term.bracketed_binders.parser,
-  type: node! decl_type [":", type: term.parser]?
+  type: term.opt_type.parser,
 ]
 
 @[derive has_tokens has_view]

library/init/lean/parser/term.lean

@@ -56,6 +56,12 @@ node! hole [hole: symbol "_" max_prec]
 def sort.parser : term_parser :=
 node_choice! sort {"Sort":max_prec, "Type":max_prec}
 
+@[derive has_tokens has_view]
+def opt_type.parser : term_parser :=
+node! opt_type [" : ", type: term.parser 0]?
+
+instance opt_type.view_default : has_view_default opt_type.parser _ none := ⟨⟩
+
 section binder
 @[derive has_tokens has_view]
 def binder_ident.parser : term_parser :=
@@ -65,7 +71,7 @@ node_choice! binder_ident {id: ident.parser, hole: hole.parser}
 def binder_content.parser : term_parser :=
 node! binder_content [
   ids: binder_ident.parser+,
-  type: node! binder_content_type [":", type: term.parser 0]?,
+  type: opt_type.parser,
   default: node_choice! binder_default {
     val: node! binder_default_val [":=", term: term.parser 0],
     tac: node! binder_default_tac [".", term: term.parser 0]
@@ -227,7 +233,7 @@ node! «let» [
       id: ident.parser,
       -- NOTE: after expansion, binders are empty
       binders: bracketed_binder.parser*,
-      type: node! let_type [" : ", type: term.parser]?
+      type: opt_type.parser,
     ],
     pattern: term.parser
   },
@@ -269,7 +275,7 @@ def match.parser : term_parser :=
 node! «match» [
   "match ",
   scrutinees: sep_by1 term.parser (symbol ", ") ff,
-  type: node! match_type [" : ", type: term.parser]?,
+  type: opt_type.parser,
   " with ",
   opt_bar: (symbol " | ")?,
   equations: sep_by1