feat(frontends/lean): use nice names for meta-variables when executing check c
and c
is a constant
This commit is contained in:
parent
51125c1577
commit
db25f933b0
4 changed files with 33 additions and 1 deletions
|
@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
||||||
Author: Leonardo de Moura
|
Author: Leonardo de Moura
|
||||||
*/
|
*/
|
||||||
#include <algorithm>
|
#include <algorithm>
|
||||||
|
#include <string>
|
||||||
#include "util/sstream.h"
|
#include "util/sstream.h"
|
||||||
#include "util/sexpr/option_declarations.h"
|
#include "util/sexpr/option_declarations.h"
|
||||||
#include "kernel/type_checker.h"
|
#include "kernel/type_checker.h"
|
||||||
|
@ -181,6 +182,27 @@ environment end_scoped_cmd(parser & p) {
|
||||||
/** \brief Auxiliary function for check/eval */
|
/** \brief Auxiliary function for check/eval */
|
||||||
static std::tuple<expr, level_param_names> parse_local_expr(parser & p) {
|
static std::tuple<expr, level_param_names> parse_local_expr(parser & p) {
|
||||||
expr e = p.parse_expr();
|
expr e = p.parse_expr();
|
||||||
|
environment const & env = p.env();
|
||||||
|
if (is_constant(e) && !const_levels(e)) {
|
||||||
|
// manually elaborate simple constant using nicer names for meta-variables
|
||||||
|
if (auto decl = env.find(const_name(e))) {
|
||||||
|
levels ls = param_names_to_levels(decl->get_univ_params());
|
||||||
|
e = mk_constant(const_name(e), ls);
|
||||||
|
expr type = instantiate_type_univ_params(*decl, ls);
|
||||||
|
while (true) {
|
||||||
|
if (!is_pi(type))
|
||||||
|
break;
|
||||||
|
if (is_explicit(binding_info(type)))
|
||||||
|
break;
|
||||||
|
std::string q("?");
|
||||||
|
q += binding_name(type).to_string();
|
||||||
|
expr m = mk_local(name(q.c_str()), binding_domain(type));
|
||||||
|
type = instantiate(binding_body(type), m);
|
||||||
|
e = mk_app(e, m);
|
||||||
|
}
|
||||||
|
return std::make_tuple(e, decl->get_univ_params());
|
||||||
|
}
|
||||||
|
}
|
||||||
list<expr> ctx = p.locals_to_context();
|
list<expr> ctx = p.locals_to_context();
|
||||||
level_param_names new_ls;
|
level_param_names new_ls;
|
||||||
std::tie(e, new_ls) = p.elaborate_relaxed(e, ctx);
|
std::tie(e, new_ls) = p.elaborate_relaxed(e, ctx);
|
||||||
|
|
6
tests/lean/check.lean
Normal file
6
tests/lean/check.lean
Normal file
|
@ -0,0 +1,6 @@
|
||||||
|
import logic
|
||||||
|
|
||||||
|
check and.intro
|
||||||
|
check or.elim
|
||||||
|
check eq
|
||||||
|
check eq.rec
|
4
tests/lean/check.lean.expected.out
Normal file
4
tests/lean/check.lean.expected.out
Normal file
|
@ -0,0 +1,4 @@
|
||||||
|
and.intro : ?a → ?b → ?a ∧ ?b
|
||||||
|
or.elim : ?a ∨ ?b → (?a → ?c) → (?b → ?c) → ?c
|
||||||
|
eq : ?A → ?A → Prop
|
||||||
|
eq.rec : ?C ?a → (Π {a : ?A}, ?a = a → ?C a)
|
|
@ -9,5 +9,5 @@ Type.{1} : Type.{2}
|
||||||
-- BEGINWAIT
|
-- BEGINWAIT
|
||||||
-- ENDWAIT
|
-- ENDWAIT
|
||||||
-- BEGINEVAL
|
-- BEGINEVAL
|
||||||
tst.foo.{l_1 l_2} : ?M_1 → ?M_2 → ?M_1
|
tst.foo.{l_1 l_2} : ?A → ?B → ?A
|
||||||
-- ENDEVAL
|
-- ENDEVAL
|
||||||
|
|
Loading…
Add table
Reference in a new issue