michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean/parser): add Find command

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-25 18:31:52 -08:00
parent d44925f943
commit 3673f2ac1d
4 changed files with 69 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

35
src/frontends/lean/parser.cpp
View file

@ -17,6 +17,7 @@ Author: Leonardo de Moura
#include <tuple>
#include <vector>
#include <limits>
#include <regex>
#include "util/flet.h"
#include "util/luaref.h"
#include "util/scoped_map.h"
@ -104,6 +105,7 @@ static name g_push_kwd("Push");
static name g_pop_kwd("Pop");
static name g_scope_kwd("Scope");
static name g_end_scope_kwd("EndScope");
static name g_find_kwd("Find");
static name g_apply("apply");
static name g_done("done");
static name g_back("back");
@ -113,8 +115,8 @@ static list<name> g_tactic_cmds = { g_apply, g_done, g_back, g_abort, g_assumpti
/** \brief Table/List with all builtin command keywords */
static list<name> g_command_keywords = {g_definition_kwd, g_variable_kwd, g_variables_kwd, g_theorem_kwd, g_axiom_kwd, g_universe_kwd, g_eval_kwd,
g_show_kwd, g_check_kwd, g_infix_kwd, g_infixl_kwd, g_infixr_kwd, g_notation_kwd, g_echo_kwd,
g_set_kwd, g_env_kwd, g_options_kwd, g_import_kwd, g_help_kwd, g_coercion_kwd, g_exit_kwd, g_push_kwd, g_pop_kwd,
g_scope_kwd, g_end_scope_kwd};
g_set_kwd, g_env_kwd, g_options_kwd, g_import_kwd, g_help_kwd, g_coercion_kwd, g_exit_kwd, g_push_kwd,
g_pop_kwd, g_scope_kwd, g_end_scope_kwd, g_find_kwd};
// ==========================================
// ==========================================
@ -2295,11 +2297,11 @@ class parser::imp {
<< " Axiom [id] : [type] assert/postulate a new axiom" << endl
<< " Check [expr] type check the given expression" << endl
<< " Definition [id] : [type] := [expr] define a new element" << endl
<< " Theorem [id] : [type] := [expr] define a new theorem" << endl
<< " Echo [string] display the given string" << endl
<< " EndScope end the current scope and import its objects into the parent scope" << endl
<< " Eval [expr] evaluate the given expression" << endl
<< " Exit exit" << endl
<< " Find [regex] display objects whose name match the given regular expression" << endl
<< " Help display this message" << endl
<< " Help Options display available options" << endl
<< " Help Notation describe commands for defining infix, mixfix, postfix operators" << endl
@ -2312,6 +2314,7 @@ class parser::imp {
<< " Show Options show current the set of assigned options" << endl
<< " Show Environment show objects in the environment, if [Num] provided, then show only the last [Num] objects" << endl
<< " Show Environment [num] show the last num objects in the environment" << endl
<< " Theorem [id] : [type] := [expr] define a new theorem" << endl
<< " Variable [id] : [type] declare/postulate an element of the given type" << endl
<< " Universe [id] [level] declare a new universe variable that is >= the given level" << endl;
#if !defined(LEAN_WINDOWS)
@ -2361,6 +2364,30 @@ class parser::imp {
}
}
void parse_find() {
next();
auto p = pos();
std::string pattern = check_string_next("invalid find command, string (regular expression) expected");
try {
std::regex regex(pattern);
auto it = m_env->begin_objects();
auto end = m_env->end_objects();
bool found = false;
io_state tmp_ios(m_io_state);
tmp_ios.set_option(name{"lean", "pp", "definition_value"}, false);
for (; it != end; ++it) {
if (!is_hidden_object(*it) && it->has_name() && it->has_type() && std::regex_match(it->get_name().to_string(), regex)) {
regular(tmp_ios) << *it << endl;
found = true;
}
}
if (!found)
throw parser_error(sstream() << "no object name in the environment matches the regular expression '" << pattern << "'" , p);
} catch (std::regex_error & ex) {
throw parser_error(sstream() << "invalid regular expression '" << pattern << "'" , p);
}
}
/** \brief Parse a Lean command. */
bool parse_command() {
m_elaborator.clear();
@ -2411,6 +2438,8 @@ class parser::imp {
parse_pop();
} else if (cmd_id == g_end_scope_kwd) {
parse_end_scope();
} else if (cmd_id == g_find_kwd) {
parse_find();
} else {
next();
throw parser_error(sstream() << "invalid command '" << cmd_id << "'", m_last_cmd_pos);

31
src/frontends/lean/pp.cpp
View file

@ -57,6 +57,10 @@ Author: Leonardo de Moura
#define LEAN_DEFAULT_PP_ALIAS_MIN_WEIGHT 20
#endif
#ifndef LEAN_DEFAULT_PP_DEFINITION_VALUE
#define LEAN_DEFAULT_PP_DEFINITION_VALUE true
#endif
namespace lean {
static format g_Type_fmt = highlight_builtin(format("Type"));
static format g_eq_fmt = format("==");
@ -86,6 +90,7 @@ static name g_pp_notation {"lean", "pp", "notation"};
static name g_pp_extra_lets {"lean", "pp", "extra_lets"};
static name g_pp_alias_min_weight{"lean", "pp", "alias_min_weight"};
static name g_pp_coercion {"lean", "pp", "coercion"};
static name g_pp_def_value {"lean", "pp", "definition_value"};
RegisterUnsignedOption(g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH, "(lean pretty printer) maximum expression depth, after that it will use ellipsis");
RegisterUnsignedOption(g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS, "(lean pretty printer) maximum number of visited expressions, after that it will use ellipsis");
@ -94,6 +99,7 @@ RegisterBoolOption(g_pp_notation, LEAN_DEFAULT_PP_NOTATION, "(lean pretty print
RegisterBoolOption(g_pp_coercion, LEAN_DEFAULT_PP_COERCION, "(lean pretty printer) display coercions");
RegisterBoolOption(g_pp_extra_lets, LEAN_DEFAULT_PP_EXTRA_LETS, "(lean pretty printer) introduce extra let expressions when displaying shared terms");
RegisterUnsignedOption(g_pp_alias_min_weight, LEAN_DEFAULT_PP_ALIAS_MIN_WEIGHT, "(lean pretty printer) mimimal weight (approx. size) of a term to be considered a shared term");
RegisterBoolOption(g_pp_def_value, LEAN_DEFAULT_PP_DEFINITION_VALUE, "(lean pretty printer) display definition/theorem value (i.e., the actual definition)");
unsigned get_pp_max_depth(options const & opts) { return opts.get_unsigned(g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH); }
unsigned get_pp_max_steps(options const & opts) { return opts.get_unsigned(g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS); }
@ -102,6 +108,7 @@ bool get_pp_notation(options const & opts) { return opts.get_bool(g_
bool get_pp_coercion(options const & opts) { return opts.get_bool(g_pp_coercion, LEAN_DEFAULT_PP_COERCION); }
bool get_pp_extra_lets(options const & opts) { return opts.get_bool(g_pp_extra_lets, LEAN_DEFAULT_PP_EXTRA_LETS); }
unsigned get_pp_alias_min_weight(options const & opts) { return opts.get_unsigned(g_pp_alias_min_weight, LEAN_DEFAULT_PP_ALIAS_MIN_WEIGHT); }
bool get_pp_def_value(options const & opts) { return opts.get_bool(g_pp_def_value, LEAN_DEFAULT_PP_DEFINITION_VALUE); }
// =======================================
// Prefixes for naming aliases (auxiliary local decls)
@ -1231,9 +1238,16 @@ class pp_formatter_cell : public formatter_cell {
format pp_definition(char const * kwd, name const & n, expr const & t, expr const & v, options const & opts) {
unsigned indent = get_pp_indent(opts);
format def = format{highlight_command(format(kwd)), space(), format(n), space(), colon(), space(),
pp(t, opts), space(), g_assign_fmt, line(), pp(v, opts)};
return group(nest(indent, def));
bool def_value = get_pp_def_value(opts);
format def_fmt;
if (def_value) {
def_fmt = format{highlight_command(format(kwd)), space(), format(n), space(), colon(), space(),
pp(t, opts), space(), g_assign_fmt, line(), pp(v, opts)};
} else {
// suppress the actual definition
def_fmt = format{highlight_command(format(kwd)), space(), format(n), space(), colon(), space(), pp(t, opts)};
}
return group(nest(indent, def_fmt));
}
format pp_compact_definition(char const * kwd, name const & n, expr const & t, expr const & v, options const & opts) {
@ -1254,8 +1268,15 @@ class pp_formatter_cell : public formatter_cell {
if (has_implicit_arguments(m_env, n))
implicit_args = &(get_implicit_arguments(m_env, n));
pp_fn fn(m_env, opts);
format def = fn.pp_definition(v, t, implicit_args);
return format{highlight_command(format(kwd)), space(), format(n), def};
format def_fmt;
bool def_value = get_pp_def_value(opts);
if (def_value)
def_fmt = fn.pp_definition(v, t, implicit_args);
else if (implicit_args)
def_fmt = fn.pp_pi_with_implicit_args(t, *implicit_args);
else
def_fmt = format{space(), colon(), space(), pp(t, opts)};
return format{highlight_command(format(kwd)), space(), format(n), def_fmt};
}
}

3
tests/lean/find.lean Normal file
View file

@ -0,0 +1,3 @@
Find ".*ongr.*"
Find "foo"
Find "(ab"

8
tests/lean/find.lean.expected.out Normal file
View file

@ -0,0 +1,8 @@
Set: pp::colors
Set: pp::unicode
Theorem Congr1 {A : (Type U)} {B : A → (Type U)} {f g : Π x : A, B x} (a : A) (H : f == g) : f a == g a
Theorem Congr2 {A : (Type U)} {B : A → (Type U)} {a b : A} (f : Π x : A, B x) (H : a == b) : f a == f b
Theorem Congr {A : (Type U)} {B : A → (Type U)} {f g : Π x : A, B x} {a b : A} (H1 : f == g) (H2 : a == b) :
f a == g b
Error (line: 2, pos: 5) no object name in the environment matches the regular expression 'foo'
Error (line: 3, pos: 5) invalid regular expression '(ab'