From 34dfacc10eb8ee7fb9dabcdf03758a5fd6ef73e1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 16 Jun 2014 10:52:12 -0700 Subject: [PATCH] refactor(frontends/lean): Bool does not need to be a reserved keyword Signed-off-by: Leonardo de Moura --- src/frontends/lean/builtin_exprs.cpp | 1 - src/frontends/lean/token_table.cpp | 2 +- src/tests/frontends/lean/scanner.cpp | 4 ++-- tests/lean/run/simple.lean | 1 + tests/lean/run/t1.lean | 1 + tests/lean/t4.lean | 1 + tests/lean/t4.lean.expected.out | 5 +++-- tests/lean/t6.lean | 1 + tests/lean/t7.lean | 1 + tests/lean/t7.lean.expected.out | 2 +- 10 files changed, 12 insertions(+), 7 deletions(-) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 74b2848e99..5c3b3b5a14 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -95,7 +95,6 @@ parse_table init_nud_table() { action Binders(mk_binders_action()); expr x0 = mk_var(0); parse_table r; - r = r.add({transition("Bool", Skip)}, mk_Bool()); r = r.add({transition("_", mk_ext_action(parse_placeholder))}, x0); r = r.add({transition("(", Expr), transition(")", Skip)}, x0); r = r.add({transition("fun", Binders), transition(",", mk_scoped_expr_action(x0))}, x0); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 3d216b13b2..37ef1deb4a 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -58,7 +58,7 @@ token_table init_token_table() { {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec}, {"[", g_max_prec}, {"]", 0}, {".{", 0}, {"Type", g_max_prec}, {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, - {"(*", 0}, {"(--", 0}, {"proof", 0}, {"qed", 0}, {"raw", 0}, {"Bool", g_max_prec}, + {"(*", 0}, {"(--", 0}, {"proof", 0}, {"qed", 0}, {"raw", 0}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}}; char const * commands[] = {"theorem", "axiom", "variable", "definition", "{axiom}", "{variable}", "[variable]", diff --git a/src/tests/frontends/lean/scanner.cpp b/src/tests/frontends/lean/scanner.cpp index 438cda4cb3..2b73102945 100644 --- a/src/tests/frontends/lean/scanner.cpp +++ b/src/tests/frontends/lean/scanner.cpp @@ -129,7 +129,7 @@ static void tst2() { scan("x.name"); scan("x.foo"); check("x.name", {tk::Identifier}); - check("fun (x : Bool), x", {tk::Keyword, tk::Keyword, tk::Identifier, tk::Keyword, tk::Keyword, + check("fun (x : Bool), x", {tk::Keyword, tk::Keyword, tk::Identifier, tk::Keyword, tk::Identifier, tk::Keyword, tk::Keyword, tk::Identifier}); check_name("x10", name("x10")); // check_name("x.10", name(name("x"), 10)); @@ -161,7 +161,7 @@ static void tst2() { scan("0..1"); check("0..1", {tk::Numeral, tk::Keyword, tk::Keyword, tk::Numeral}); scan("theorem a : Bool axiom b : Int"); - check("theorem a : Bool axiom b : Int", {tk::CommandKeyword, tk::Identifier, tk::Keyword, tk::Keyword, + check("theorem a : Bool axiom b : Int", {tk::CommandKeyword, tk::Identifier, tk::Keyword, tk::Identifier, tk::CommandKeyword, tk::Identifier, tk::Keyword, tk::Identifier}); scan("foo \"ttk\\\"\" : Int"); check("foo \"ttk\\\"\" : Int", {tk::Identifier, tk::String, tk::Keyword, tk::Identifier}); diff --git a/tests/lean/run/simple.lean b/tests/lean/run/simple.lean index bb320aba81..e2839e1319 100644 --- a/tests/lean/run/simple.lean +++ b/tests/lean/run/simple.lean @@ -1,3 +1,4 @@ +abbreviation Bool : Type.{1} := Type.{0} section parameter A : Type diff --git a/tests/lean/run/t1.lean b/tests/lean/run/t1.lean index 20e8970074..56019b10f1 100644 --- a/tests/lean/run/t1.lean +++ b/tests/lean/run/t1.lean @@ -1,3 +1,4 @@ +definition Bool : Type.{1} := Type.{0} print raw ((Bool)) print raw Bool print raw fun (x y : Bool), x x diff --git a/tests/lean/t4.lean b/tests/lean/t4.lean index cbfba7f1af..c2b3e7e5fb 100644 --- a/tests/lean/t4.lean +++ b/tests/lean/t4.lean @@ -1,3 +1,4 @@ +definition [inline] Bool : Type.{1} := Type.{0} variable N : Type.{1} check N variable a : N diff --git a/tests/lean/t4.lean.expected.out b/tests/lean/t4.lean.expected.out index ab04626120..a57a678b6e 100644 --- a/tests/lean/t4.lean.expected.out +++ b/tests/lean/t4.lean.expected.out @@ -8,7 +8,7 @@ len.{1} : Pi (A : Type) (n : N) (v : vec.{1} A n), N B -> B : Bool A -> A : Type.{l_1} C : Type.{l_2} -t4.lean:24:6: error: unknown identifier 'A' +t4.lean:25:6: error: unknown identifier 'A' R.{1 0} : Type -> Bool fun (x : N) (y : N), x : N -> N -> N choice N tst.N @@ -18,7 +18,7 @@ foo.M tst.M : Type.{2} foo.M : Type.{3} foo.M : Type.{3} -t4.lean:47:6: error: unknown identifier 'M' +t4.lean:48:6: error: unknown identifier 'M' ok Declarations: tst.M @@ -31,4 +31,5 @@ len vec f foo.M +Bool ------------- diff --git a/tests/lean/t6.lean b/tests/lean/t6.lean index 15608e8657..049a482291 100644 --- a/tests/lean/t6.lean +++ b/tests/lean/t6.lean @@ -1,3 +1,4 @@ +definition Bool : Type.{1} := Type.{0} section {parameter} A : Type -- Mark A as implicit parameter parameter R : A → A → Bool diff --git a/tests/lean/t7.lean b/tests/lean/t7.lean index e9020e8356..eb97630e5c 100644 --- a/tests/lean/t7.lean +++ b/tests/lean/t7.lean @@ -1,3 +1,4 @@ +definition Bool : Type.{1} := Type.{0} variable and : Bool → Bool → Bool section {parameter} A : Type -- Mark A as implicit parameter diff --git a/tests/lean/t7.lean.expected.out b/tests/lean/t7.lean.expected.out index a7a9b68f52..9c2d8b4c0a 100644 --- a/tests/lean/t7.lean.expected.out +++ b/tests/lean/t7.lean.expected.out @@ -2,4 +2,4 @@ id.{2} : Pi {A : Type.{2}} (a : A), A trans.{1} : Pi {A : Type} (R : A -> A -> Bool), Bool symm.{1} : Pi {A : Type} (R : A -> A -> Bool), Bool equivalence.{1} : Pi {A : Type} (R : A -> A -> Bool), Bool -fun {A : Type.{l_1}} (R : A -> A -> Bool), (and (and (private.2020036202.refl.{l_1} A R) (symm.{l_1} A R)) (trans.{l_1} A R)) +fun {A : Type.{l_1}} (R : A -> A -> Bool), (and (and (private.2595647076.refl.{l_1} A R) (symm.{l_1} A R)) (trans.{l_1} A R))