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

feat(library/init/lean/parser/declaration): implement structure field blocks that go beyond regular binder syntax

Browse source
This commit is contained in:
Sebastian Ullrich 2019-01-15 15:00:34 +01:00
parent 7aa06338c9
commit fc3a0403ab
2 changed files with 27 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
library/init/lean/parser/declaration.lean
View file

@ -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]

12
library/init/lean/parser/term.lean
View file

@ -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]