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

Add parse_expr. Add more tests.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-17 18:35:50 -07:00
parent 685aeae43a
commit 06f1b2a7db
3 changed files with 50 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
src/frontend/parser.cpp
View file

@ -40,7 +40,7 @@ struct parser_fn {
typedef std::unordered_map<name, expr, name_hash, name_eq> builtins;
frontend m_frontend;
scanner m_scanner;
std::ostream & m_err;
std::ostream * m_err;
scanner::token m_curr;
bool m_use_exceptions;
bool m_found_errors;
@ -84,7 +84,7 @@ struct parser_fn {
m_builtins["Int"] = Int;
}
parser_fn(frontend & fe, std::istream & in, std::ostream & err, bool use_exceptions):
parser_fn(frontend & fe, std::istream & in, std::ostream * err, bool use_exceptions):
m_frontend(fe),
m_scanner(in),
m_err(err),
@ -369,7 +369,8 @@ struct parser_fn {
}
void error(char const * msg, unsigned line, unsigned pos) {
m_err << "Error (line: " << line << ", pos: " << pos << ") " << msg << std::endl;
lean_assert(m_err);
(*m_err) << "Error (line: " << line << ", pos: " << pos << ") " << msg << std::endl;
}
void error(char const * msg) {
@ -403,8 +404,20 @@ struct parser_fn {
}
}
}
expr parse_expr_main() {
try {
return parse_expr();
} catch (parser_error & ex) {
throw parser_exception(ex.what(), m_scanner.get_line(), m_scanner.get_pos());
}
}
};
bool parse_commands(frontend & fe, std::istream & in, std::ostream & err, bool use_exceptions) {
return parser_fn(fe, in, err, use_exceptions).parse_commands();
return parser_fn(fe, in, &err, use_exceptions).parse_commands();
}
expr parse_expr(frontend const & fe, std::istream & in) {
return parser_fn(const_cast<frontend&>(fe), in, nullptr, true).parse_expr_main();
}
}

1
src/frontend/parser.h
View file

@ -10,4 +10,5 @@ Author: Leonardo de Moura
namespace lean {
bool parse_commands(frontend & fe, std::istream & in, std::ostream & err = std::cerr, bool use_exceptions = false);
expr parse_expr(frontend const & fe, std::istream & in);
}

36
src/tests/frontend/parser.cpp
View file

@ -5,15 +5,17 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <sstream>
#include "builtin.h"
#include "parser.h"
#include "pp.h"
#include "printer.h"
#include "exception.h"
#include "test.h"
using namespace lean;
static void parse(frontend & fe, char const * msg) {
static void parse(frontend & fe, char const * str) {
frontend child = fe.mk_child();
std::istringstream in(msg);
std::istringstream in(str);
if (parse_commands(child, in)) {
formatter fmt = mk_pp_formatter(child);
std::for_each(child.begin_local_objects(),
@ -27,11 +29,37 @@ static void parse(frontend & fe, char const * msg) {
static void tst1() {
frontend fe;
parse(fe,
"Variable x : Bool Variable y : Bool Axiom H : x && y || x => x");
parse(fe, "Variable x : Bool Variable y : Bool Axiom H : x && y || x => x");
}
static void check(frontend const & fe, char const * str, expr const & expected) {
std::istringstream in(str);
try {
expr got = parse_expr(fe, in);
lean_assert(expected == got);
} catch (exception &) {
lean_unreachable();
}
}
static void tst2() {
frontend fe;
fe.add_var("x", Bool);
fe.add_var("y", Bool);
fe.add_var("z", Bool);
expr x = Const("x"); expr y = Const("y"); expr z = Const("z");
check(fe, "x && y", And(x, y));
check(fe, "x && y || z", Or(And(x, y), z));
check(fe, "x || y && z", Or(x, And(y, z)));
check(fe, "x || y || x && z", Or(x, Or(y, And(x, z))));
check(fe, "x || y || x && z => x && y", Implies(Or(x, Or(y, And(x, z))), And(x, y)));
check(fe, "x ∨ y ∨ x ∧ z ⇒ x ∧ y", Implies(Or(x, Or(y, And(x, z))), And(x, y)));
check(fe, "x⇒y⇒z⇒x", Implies(x, Implies(y, Implies(z, x))));
check(fe, "x=>y=>z=>x", Implies(x, Implies(y, Implies(z, x))));
}
int main() {
tst1();
tst2();
return has_violations() ? 1 : 0;
}