From fc3a0403abfc32c1afacdab20d82da03b1cd5d8f Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 15 Jan 2019 15:00:34 +0100
Subject: [PATCH] feat(library/init/lean/parser/declaration): implement
 structure field blocks that go beyond regular binder syntax

---
 library/init/lean/parser/declaration.lean | 24 ++++++++++++++++++-----
 library/init/lean/parser/term.lean        | 12 ++++++++----
 2 files changed, 27 insertions(+), 9 deletions(-)

diff --git a/library/init/lean/parser/declaration.lean b/library/init/lean/parser/declaration.lean
index 5d41ece568..d54a8a97f2 100644
--- a/library/init/lean/parser/declaration.lean
+++ b/library/init/lean/parser/declaration.lean
@@ -92,10 +92,24 @@ node! intro_rule [
 ]
 
 @[derive has_tokens has_view]
-def structure_field.parser : command_parser :=
-node_longest_choice! structure_field {
-  local_notation: node! structure_notation ["(", «notation»: notation_like.parser, ")"],
-  field: term.bracketed_binder.parser,
+def struct_binder_content.parser : command_parser :=
+node! struct_binder_content [
+  ids: ident.parser+,
+  infer_mod: infer_modifier.parser?,
+  sig: opt_decl_sig.parser,
+  default: term.binder_default.parser?,
+]
+
+@[derive has_tokens has_view]
+def structure_field_block.parser : command_parser :=
+node_choice! structure_field_block {
+  explicit: node! struct_explicit_binder ["(", content: node_choice! struct_explicit_binder_content {
+    «notation»: command.notation_like.parser,
+    other: struct_binder_content.parser
+  }, right: symbol ")"],
+  implicit: node! struct_implicit_binder ["{", content: struct_binder_content.parser, "}"],
+  strict_implicit: node! strict_implicit_binder ["⦃", content: struct_binder_content.parser, "⦄"],
+  inst_implicit: node! inst_implicit_binder ["[", content: struct_binder_content.parser, "]"],
 }
 
 @[derive has_tokens has_view]
@@ -119,7 +133,7 @@ node! «structure» [
   «extends»: node! «extends» ["extends", parents: sep_by1 term.parser (symbol ",")]?,
   ":=",
   ctor: node! structure_ctor [name: ident.parser, infer_mod: infer_modifier.parser?, "::"]?,
-  fields: structure_field.parser*,
+  field_blocks: structure_field_block.parser*,
 ]
 
 @[derive has_tokens has_view]
diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean
index 6acd894bd5..4fa5edfbb0 100644
--- a/library/init/lean/parser/term.lean
+++ b/library/init/lean/parser/term.lean
@@ -71,15 +71,19 @@ section binder
 def binder_ident.parser : term_parser :=
 node_choice! binder_ident {id: ident.parser, hole: hole.parser}
 
+@[derive has_tokens has_view]
+def binder_default.parser : term_parser :=
+node_choice! binder_default {
+  val: node! binder_default_val [":=", term: term.parser 0],
+  tac: node! binder_default_tac [".", term: term.parser 0],
+}
+
 @[derive has_tokens has_view]
 def binder_content.parser : term_parser :=
 node! binder_content [
   ids: binder_ident.parser+,
   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]
-  }?
+  default: binder_default.parser?
 ]
 
 @[derive has_tokens has_view]