From 501cae37e5cca78e5cd4b4b567dc9c505aa70d05 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 29 Jul 2014 13:04:58 -0700
Subject: [PATCH] fix(frontends/lean/parser): bug in check_constant_next (when
invoked inside of a section)
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
src/frontends/lean/parser.cpp | 14 ++++++++++++--
tests/lean/run/opaque_hint_bug.lean | 16 ++++++++++++++++
2 files changed, 28 insertions(+), 2 deletions(-)
create mode 100644 tests/lean/run/opaque_hint_bug.lean
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 9133984c2..8a8b169b3 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -26,6 +26,7 @@ Author: Leonardo de Moura
#include "library/deep_copy.h"
#include "library/module.h"
#include "library/scoped_ext.h"
+#include "library/explicit.h"
#include "library/num.h"
#include "library/string.h"
#include "library/error_handling/error_handling.h"
@@ -876,9 +877,18 @@ name parser::check_constant_next(char const * msg) {
auto p = pos();
name id = check_id_next(msg);
expr e = id_to_expr(id, p);
- if (!is_constant(e))
+
+ if (in_section(m_env) && is_implicit(e)) {
+ e = get_app_fn(get_implicit_arg(e));
+ if (is_explicit(e))
+ e = get_explicit_arg(e);
+ }
+
+ if (is_constant(e)) {
+ return const_name(e);
+ } else {
throw parser_error(msg, p);
- return const_name(e);
+ }
}
expr parser::parse_id() {
diff --git a/tests/lean/run/opaque_hint_bug.lean b/tests/lean/run/opaque_hint_bug.lean
new file mode 100644
index 000000000..4c9fa0840
--- /dev/null
+++ b/tests/lean/run/opaque_hint_bug.lean
@@ -0,0 +1,16 @@
+
+
+inductive list (T : Type) : Type :=
+| nil {} : list T
+| cons : T → list T → list T
+
+
+section
+ variable {T : Type}
+
+ definition concat (s t : list T) : list T
+ := list_rec t (fun x l u, cons x u) s
+
+ opaque_hint (hiding concat)
+
+end
\ No newline at end of file