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

feat(library/init/lean/parser/basic): allow views to specify default value used with opt_param when nested in other views

Browse source
This commit is contained in:
Sebastian Ullrich 2018-09-23 21:53:41 -07:00
parent 07f96e8e09
commit 9a0b1c7a7f
3 changed files with 31 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
library/init/lean/parser/basic.lean
View file

@ -79,6 +79,8 @@ protected class has_view (r : ρ) (α : out_param Type) :=
instance has_view.default (r : ρ) : inhabited (parser.has_view r syntax) :=
⟨{ view := some, review := id }⟩
class has_view_default (r : ρ) (α : out_param Type) [has_view r α] (default : α) := mk {}
abbreviation tysyntax (α : Type) := syntax
class tysyntax.is_view (α : Type) :=
@ -90,6 +92,9 @@ export tysyntax.is_view (view review)
def view_with (α : Type) [tysyntax.is_view α] (stx : syntax) : option α :=
view (stx : tysyntax α)
def review_as (α : Type) [tysyntax.is_view α] (a : α) : syntax :=
review a
def message_of_parsec_message {μ : Type} (cfg : parser_config) (msg : parsec.message μ) : message :=
-- FIXME: translate position
{filename := cfg.filename, pos := ⟨0, 0⟩, text := to_string msg}

10
library/init/lean/parser/token.lean
View file

@ -160,9 +160,17 @@ lift $ try $ do {
pure stx
} <?> repr sym
instance syntax_atom.is_view : tysyntax.is_view syntax_atom :=
{ view := λ stx, match stx with
| syntax.atom atom := some atom
| _ := none,
review := syntax.atom }
instance symbol.tokens (sym lbp) : parser.has_tokens (symbol sym lbp : parser) :=
⟨[⟨sym, lbp, none⟩]⟩
instance symbol.view (sym lbp) : parser.has_view (symbol sym lbp : parser) syntax := default _
instance symbol.view (sym lbp) : parser.has_view (symbol sym lbp : parser) syntax_atom :=
{..syntax_atom.is_view}
instance symbol.view_default (sym lbp) : parser.has_view_default (symbol sym lbp : parser) _
{info := none, val := sym} := ⟨⟩
def number : parser :=
lift $ try $ do {

19
src/frontends/lean/elaborator.cpp
View file

@ -3238,7 +3238,14 @@ expr elaborator::visit_node_macro(expr const & e, optional<expr> const & expecte
if (!inst)
throw elaborator_exception(e, sstream() << "Could not infer instance of parser.has_view for '" << r
<< "'");
struc << "(«" << fname << "» : tysyntax (" << instantiate_mvars(m) << "))\n";
auto m2 = mk_metavar(m, r);
auto defval_inst = m_ctx.mk_class_instance(
mk_app(mk_app(mk_const(name{"lean", "parser", "has_view_default"}), exp, r, m), *inst, m2));
if (defval_inst)
struc << "(«" << fname << "» : tysyntax (" << instantiate_mvars(m) << ") := review ("
<< pp(instantiate_mvars(m2)) << "))\n";
else
struc << "(«" << fname << "» : tysyntax (" << instantiate_mvars(m) << "))\n";
if (i != 0)
stx_pat << ", ";
@ -3319,7 +3326,14 @@ expr elaborator::visit_node_choice_macro(expr const & e, optional<expr> const &
if (!inst)
throw elaborator_exception(e, sstream() << "Could not infer instance of parser.has_view for '" << r
<< "'");
struc << "| " << fname << " : tysyntax (" << instantiate_mvars(m) << ") -> " << macro.to_string() << ".view\n";
auto m2 = mk_metavar(m, r);
auto defval_inst = m_ctx.mk_class_instance(
mk_app(mk_app(mk_const(name{"lean", "parser", "has_view_default"}), exp, r, m), *inst, m2));
if (defval_inst)
struc << "| " << fname << " : opt_param (tysyntax (" << instantiate_mvars(m) << ")) (review ("
<< pp(instantiate_mvars(m2)) << ")) -> " << macro.to_string() << ".view\n";
else
struc << "| " << fname << " : tysyntax (" << instantiate_mvars(m) << ") -> " << macro.to_string() << ".view\n";
view_cases << "| " << i << " := " << macro.to_string() << ".view." << fname << " stx\n";
review_cases << "| " << macro.to_string() << ".view." << fname << " a := "
@ -3339,6 +3353,7 @@ expr elaborator::visit_node_choice_macro(expr const & e, optional<expr> const &
<< " [match v with\n"
<< review_cases.str()
<< "]) }";
trace_elab_detail(tout() << "expansion of node_choice! macro:\n" << struc.str(););
std::istringstream in(struc.str());
parser p(m_env, get_global_ios(), in, "foo");
p.set_imports_parsed();