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

feat(library/init/lean,frontends/lean/vm_elaborator): set_option

Browse source
This commit is contained in:
Sebastian Ullrich 2019-01-20 18:14:44 +01:00
parent 88534abccd
commit c22fbb5cde
4 changed files with 103 additions and 56 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
library/init/lean/elaborator.lean
View file

@ -97,6 +97,7 @@ structure local_state :=
(ns_stack : list name := [])
/- The set of active `open` declarations. -/
(open_decls : list open_spec.view := [])
(options : options := options.mk)
/-- An `export` command together with the namespace it was declared in. Opening the namespace activates
the export. -/
@ -118,7 +119,6 @@ structure elaborator_state :=
(expander_cfg : expander.expander_config)
(env : environment := environment.empty)
(ngen : name_generator)
(options : options)
(next_inst_idx : nat := 0)
@[derive monad monad_reader monad_state monad_except]
@ -358,6 +358,7 @@ do cfg ← read,
univs := st.local_state.univs.entries.reverse,
vars := st.local_state.vars.entries.reverse,
include_vars := st.local_state.include_vars.to_list,
options := st.local_state.options,
..st},
match st' with
| some st' := put {
@ -365,6 +366,7 @@ do cfg ← read,
univs := ordered_rbmap.of_list st'.univs,
vars := ordered_rbmap.of_list st'.vars,
include_vars := rbtree.of_list st'.include_vars,
options := st'.options,
},
..st', ..st}
| none := pure (), -- error
@ -813,6 +815,21 @@ def export.elaborate : elaborator :=
def init_quot.elaborate : elaborator :=
λ stx, old_elab_command stx $ expr.mdata (kvmap.set_name {} `command `init_quot) dummy
def set_option.elaborate : elaborator :=
λ stx, do
let v := view «set_option» stx,
let opt := v.opt.val,
st ← get,
let opts := st.local_state.options,
-- TODO(Sebastian): check registered options
let opts := match v.val with
| option_value.view.bool b := opts.set_bool opt (match b with bool_option_value.view.true _ := tt | _ := ff)
| option_value.view.string lit := (match lit.value with
| some s := opts.set_string opt s
| none := opts) -- parser already failed
| option_value.view.num lit := opts.set_nat opt lit.to_nat,
put {st with local_state := {st.local_state with options := opts}}
/-- List of commands: recursively elaborate each command. -/
def no_kind.elaborate : coelaborator := do
stx ← current_command,
@ -886,7 +903,8 @@ def elaborators : rbmap name coelaborator (<) := rbmap.from_list [
(open.name, open.elaborate),
(export.name, export.elaborate),
(check.name, check.elaborate),
(init_quot.name, init_quot.elaborate)
(init_quot.name, init_quot.elaborate),
(set_option.name, set_option.elaborate)
] _
-- TODO: optimize
@ -962,7 +980,7 @@ do
parser_cfg := cfg.initial_parser_cfg,
expander_cfg := {transformers := expander.builtin_transformers, ..cfg},
ngen := ⟨`_ngen.fixme, 0⟩,
options := options.mk},
local_state := {options := options.mk.set_bool `trace.as_messages tt}},
p ← except_t.run $ flip state_t.run st $ flip reader_t.run cfg $ rec_t.run
(commands.elaborate ff max_commands)
(λ _, modify $ λ st, {st with messages := st.messages.add {filename := "foo", pos := ⟨1,0⟩, text := "elaborator.run: out of fuel"}})

14
library/init/lean/parser/command.lean
View file

@ -98,12 +98,24 @@ node! «attribute» [
def init_quot.parser : command_parser :=
node! «init_quot» ["init_quot"]
@[derive parser.has_tokens parser.has_view]
def set_option.parser : command_parser :=
node! «set_option» ["set_option", opt: ident.parser, val: node_choice! option_value {
bool: node_choice! bool_option_value {
true: symbol_or_ident "true",
false: symbol_or_ident "true",
},
string: string_lit.parser,
-- TODO(Sebastian): fractional numbers
num: number.parser,
}]
@[derive has_tokens]
def builtin_command_parsers : list command_parser := [
declaration.parser, variable.parser, variables.parser, namespace.parser, end.parser,
open.parser, section.parser, universe.parser, notation.parser, reserve_notation.parser,
mixfix.parser, reserve_mixfix.parser, check.parser, attribute.parser,
export.parser, include.parser, omit.parser, init_quot.parser]
export.parser, include.parser, omit.parser, init_quot.parser, set_option.parser]
end «command»
def command_parser.run (commands : list command_parser) (p : command_parser)

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

@ -299,7 +299,7 @@ def string_lit.parser : parser :=
lift $ try $ do {
it ← left_over,
stx ← token,
some _ ← pure $ try_view string_lit stx | error "" (dlist.singleton "number") it,
some _ ← pure $ try_view string_lit stx | error "" (dlist.singleton "string") it,
pure stx
} <?> "string"
@ -307,6 +307,12 @@ instance string_lit.parser.tokens : parser.has_tokens (string_lit.parser : parse
instance string_lit.parser.view : parser.has_view string_lit.view (string_lit.parser : parser) :=
{..string_lit.has_view}
def string_lit.view.value (lit : string_lit.view) : option string := do
atom ← lit.val,
except.ok s ← pure $ parsec.parse (parse_string_literal : parsec' _) atom.val
| failure,
pure s
def ident.parser : parser :=
lift $ try $ do {
it ← left_over,

113
src/frontends/lean/vm_elaborator.cpp
View file

@ -29,6 +29,7 @@ Lean interface to the old elaborator/elaboration parts of the parser
#include "frontends/lean/inductive_cmds.h"
#include "frontends/lean/structure_cmd.h"
#include "frontends/lean/util.h"
#include "frontends/lean/pp.h"
namespace lean {
struct resolve_names_fn : public replace_visitor {
@ -593,16 +594,16 @@ options to_options(vm_obj o) {
for (auto const & kv : m) {
switch (kv.snd().kind()) {
case data_value_kind::Bool:
opts.update(kv.fst(), kv.snd().get_bool());
opts = opts.update(kv.fst(), kv.snd().get_bool());
break;
case data_value_kind::Name:
opts.update(kv.fst(), kv.snd().get_name());
opts = opts.update(kv.fst(), kv.snd().get_name());
break;
case data_value_kind::Nat:
opts.update(kv.fst(), kv.snd().get_nat().get_small_value());
opts = opts.update(kv.fst(), kv.snd().get_nat().get_small_value());
break;
case data_value_kind::String:
opts.update(kv.fst(), kv.snd().get_string());
opts = opts.update(kv.fst(), kv.snd().get_string());
break;
}
}
@ -657,11 +658,8 @@ vm_obj to_obj(message_log const & log) {
vm_obj vm_elaborate_command(vm_obj const & vm_filename, vm_obj const & vm_cmd, vm_obj const & vm_st) {
auto vm_e = cfield(vm_st, 0);
auto env = to_env(vm_e);
io_state const & ios = get_dummy_ios();
auto filename = to_string(vm_filename);
std::stringstream in;
parser p(env, ios, in, filename);
auto s = p.mk_snapshot();
auto ngen = to_name_generator(cfield(vm_st, 1));
auto vm_lds = cfield(vm_st, 2);
local_level_decls lds;
@ -688,58 +686,71 @@ vm_obj vm_elaborate_command(vm_obj const & vm_filename, vm_obj const & vm_cmd, v
}
auto includes = to_name_set(cfield(vm_st, 4));
auto options = to_options(cfield(vm_st, 5));
p.reset(snapshot(p.env(), ngen, lds, eds, lvars, vars, includes, options, true, false,
parser_scope_stack(), to_unsigned(cfield(vm_st, 6)), pos_info {1, 0}));
auto ns = to_name(cfield(vm_st, 7));
p.set_env(set_namespace(env, ns));
auto cmd = to_expr(vm_cmd);
auto pos = get_pos(cmd).value_or(pos_info {1, 0});
message_log log;
scope_message_log _(log);
vm_obj vm_out = mk_vm_none();
try {
elaborate_command(p, cmd);
s = p.mk_snapshot();
{
scope_message_log scope3(log);
io_state ios(options, mk_pretty_formatter_factory());
ios.set_regular_channel(ios.get_diagnostic_channel_ptr());
scope_global_ios scope_ios(ios);
type_context_old tc(env, options);
scope_trace_env scope(env, options, tc);
scope_traces_as_messages scope2(filename, pos);
// sort levels by reverse insertion order. ugh.
rb_map<unsigned, name, unsigned_rev_cmp> new_lds;
s->m_lds.for_each([&](name const & n, level const &) {
new_lds.insert(s->m_lds.find_idx(n), n);
});
new_lds.for_each([&](unsigned const &, name const & n) {
auto vm_n = to_obj(n);
auto vm_ld = mk_vm_constructor(0, vm_n, mk_vm_constructor(4, vm_n));
vm_lds = mk_vm_constructor(1, vm_ld, vm_lds);
});
parser p(env, ios, in, filename);
auto s = p.mk_snapshot();
p.reset(snapshot(p.env(), ngen, lds, eds, lvars, vars, includes, options, true, false,
parser_scope_stack(), to_unsigned(cfield(vm_st, 6)), pos_info{1, 0}));
auto ns = to_name(cfield(vm_st, 7));
p.set_env(set_namespace(env, ns));
for (auto const & ed : s->m_eds.get_entries()) {
if (!is_local_p(ed.second)) {
// obsolete local ref, ignore
continue;
try {
elaborate_command(p, cmd);
s = p.mk_snapshot();
// sort levels by reverse insertion order. ugh.
rb_map<unsigned, name, unsigned_rev_cmp> new_lds;
s->m_lds.for_each([&](name const & n, level const &) {
new_lds.insert(s->m_lds.find_idx(n), n);
});
new_lds.for_each([&](unsigned const &, name const & n) {
auto vm_n = to_obj(n);
auto vm_ld = mk_vm_constructor(0, vm_n, mk_vm_constructor(4, vm_n));
vm_lds = mk_vm_constructor(1, vm_ld, vm_lds);
});
for (auto const & ed : s->m_eds.get_entries()) {
if (!is_local_p(ed.second)) {
// obsolete local ref, ignore
continue;
}
auto vm_ed = mk_vm_constructor(0, to_obj(ed.first), mk_vm_constructor(0,
to_obj(local_name_p(ed.second)),
mk_vm_external(new vm_expr(
local_type_p(ed.second))),
to_obj(local_info_p(ed.second))));
vm_eds = mk_vm_constructor(1, vm_ed, vm_eds);
}
auto vm_ed = mk_vm_constructor(0, to_obj(ed.first), mk_vm_constructor(0,
to_obj(local_name_p(ed.second)),
mk_vm_external(new vm_expr(local_type_p(ed.second))),
to_obj(local_info_p(ed.second))));
vm_eds = mk_vm_constructor(1, vm_ed, vm_eds);
}
auto vm_st2 = mk_vm_constructor(0, {
mk_vm_external(new vm_env(p.env())),
to_obj(s->m_ngen),
vm_lds,
vm_eds,
cfield(vm_st, 4),
cfield(vm_st, 5),
cfield(vm_st, 6),
cfield(vm_st, 7)
});
vm_out = mk_vm_some(vm_st2);
} catch (exception & e) {
message_builder builder(env, ios, filename, get_pos_info_provider()->get_pos_info_or_some(cmd),
message_severity::ERROR);
builder.set_exception(e);
builder.report();
auto vm_st2 = mk_vm_constructor(0, {
mk_vm_external(new vm_env(p.env())),
to_obj(s->m_ngen),
vm_lds,
vm_eds,
cfield(vm_st, 4),
cfield(vm_st, 5),
cfield(vm_st, 6),
cfield(vm_st, 7)
});
vm_out = mk_vm_some(vm_st2);
} catch (exception & e) {
message_builder builder(env, ios, filename, pos, message_severity::ERROR);
builder.set_exception(e);
builder.report();
}
}
return mk_vm_constructor(0, vm_out, to_obj(log));
}