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

chore(frontends/lean): use consistent filename convention

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-09-04 09:59:24 -07:00
parent b94ec07b29
commit 9876d07094
6 changed files with 47 additions and 47 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/CMakeLists.txt
View file

@ -5,6 +5,6 @@ server.cpp notation_cmd.cpp calc.cpp
decl_cmds.cpp util.cpp inductive_cmd.cpp elaborator.cpp
dependencies.cpp parser_bindings.cpp begin_end_ext.cpp
class.cpp pp_options.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp
structure_cmd.cpp info_manager.cpp noinfo.cpp extra_info.cpp)
structure_cmd.cpp info_manager.cpp no_info.cpp extra_info.cpp)
target_link_libraries(lean_frontend ${LEAN_LIBS})

36
src/frontends/lean/elaborator.cpp
View file

@ -37,7 +37,7 @@ Author: Leonardo de Moura
#include "frontends/lean/tactic_hint.h"
#include "frontends/lean/info_manager.h"
#include "frontends/lean/elaborator.h"
#include "frontends/lean/noinfo.h"
#include "frontends/lean/no_info.h"
#include "frontends/lean/extra_info.h"
#ifndef LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES
@ -310,7 +310,7 @@ class elaborator {
// this mapping is populated by the 'by tactic-expr' expression.
name_set m_displayed_errors; // set of metavariables that we already reported unsolved/unassigned
bool m_relax_main_opaque; // if true, then treat opaque definitions from the main module as transparent.
bool m_noinfo; // when true, we do not collect information when true, we set is to true whenever we find noinfo annotation.
bool m_no_info; // when true, we do not collect information when true, we set is to true whenever we find no_info annotation.
info_manager m_pre_info_data;
// Auxiliary object to "saving" elaborator state
@ -334,21 +334,21 @@ class elaborator {
/** \brief Auxiliary object for creating backtracking points, and replacing the local scopes. */
struct new_scope {
elaborator & m_main;
bool m_old_noinfo;
bool m_old_no_info;
context::scope_replace m_context_scope;
context::scope_replace m_full_context_scope;
cache m_old_cache;
new_scope(elaborator & e, saved_state const & s, bool noinfo = false):
new_scope(elaborator & e, saved_state const & s, bool no_info = false):
m_main(e),
m_context_scope(e.m_context, s.m_ctx),
m_full_context_scope(e.m_full_context, s.m_full_ctx){
m_old_noinfo = m_main.m_noinfo;
m_main.m_noinfo = noinfo;
m_old_no_info = m_main.m_no_info;
m_main.m_no_info = no_info;
m_old_cache = m_main.m_cache;
m_main.m_cache = s.m_cache;
}
~new_scope() {
m_main.m_noinfo = m_old_noinfo;
m_main.m_no_info = m_old_no_info;
m_main.m_cache = m_old_cache;
}
};
@ -447,8 +447,8 @@ class elaborator {
pre = copy_tag(m_meta, ::lean::mk_app(pre, copy_tag(m_meta, mk_strict_expr_placeholder())));
}
try {
bool noinfo = true;
new_scope s(m_elab, m_state, noinfo);
bool no_info = true;
new_scope s(m_elab, m_state, no_info);
pair<expr, constraint_seq> rcs = m_elab.visit(pre); // use elaborator to create metavariables, levels, etc.
expr r = rcs.first;
buffer<constraint> cs;
@ -525,7 +525,7 @@ public:
m_context(m_ngen, m_mvar2meta, ctx),
m_full_context(m_ngen, m_mvar2meta, ctx) {
m_relax_main_opaque = false;
m_noinfo = false;
m_no_info = false;
m_tc[0] = mk_type_checker_with_hints(env.m_env, m_ngen.mk_child(), false);
m_tc[1] = mk_type_checker_with_hints(env.m_env, m_ngen.mk_child(), true);
}
@ -552,7 +552,7 @@ public:
/** \brief Store the pair (pos(e), type(r)) in the info_data if m_info_manager is available. */
void save_type_data(expr const & e, expr const & r) {
if (!m_noinfo && infom() && pip() && (is_constant(e) || is_local(e) || is_placeholder(e))) {
if (!m_no_info && infom() && pip() && (is_constant(e) || is_local(e) || is_placeholder(e))) {
if (auto p = pip()->get_pos_info(e)) {
expr t = m_tc[m_relax_main_opaque]->infer(r).first;
m_pre_info_data.add_type_info(p->first, p->second, t);
@ -562,7 +562,7 @@ public:
/** \brief Store type information at pos(e) for r if \c e is marked as "extra" in the info_manager */
void save_extra_type_data(expr const & e, expr const & r) {
if (!m_noinfo && infom() && pip()) {
if (!m_no_info && infom() && pip()) {
if (auto p = pip()->get_pos_info(e)) {
expr t = m_tc[m_relax_main_opaque]->infer(r).first;
m_pre_info_data.add_extra_type_info(p->first, p->second, r, t);
@ -572,7 +572,7 @@ public:
/** \brief Auxiliary function for saving information about which overloaded identifier was used by the elaborator. */
void save_identifier_info(expr const & f) {
if (!m_noinfo && infom() && pip() && is_constant(f)) {
if (!m_no_info && infom() && pip() && is_constant(f)) {
if (auto p = pip()->get_pos_info(f))
m_pre_info_data.add_identifier_info(p->first, p->second, const_name(f));
}
@ -580,7 +580,7 @@ public:
/** \brief Store actual term that was synthesized for an explicit placeholders */
void save_synth_data(expr const & e, expr const & r) {
if (!m_noinfo && infom() && pip() && is_placeholder(e)) {
if (!m_no_info && infom() && pip() && is_placeholder(e)) {
if (auto p = pip()->get_pos_info(e))
m_pre_info_data.add_synth_info(p->first, p->second, r);
}
@ -597,7 +597,7 @@ public:
It marks that coercion c was used on e.
*/
void save_coercion_info(expr const & e, expr const & c) {
if (!m_noinfo && infom() && pip()) {
if (!m_no_info && infom() && pip()) {
if (auto p = pip()->get_pos_info(e)) {
expr t = m_tc[m_relax_main_opaque]->infer(c).first;
m_pre_info_data.add_coercion_info(p->first, p->second, c, t);
@ -607,7 +607,7 @@ public:
/** \brief Remove coercion information associated with \c e */
void erase_coercion_info(expr const & e) {
if (!m_noinfo && infom() && pip()) {
if (!m_no_info && infom() && pip()) {
if (auto p = pip()->get_pos_info(e))
m_pre_info_data.erase_coercion_info(p->first, p->second);
}
@ -1214,8 +1214,8 @@ public:
return visit_let_value(e, cs);
} else if (is_by(e)) {
return visit_by(e, none_expr(), cs);
} else if (is_noinfo(e)) {
flet<bool> let(m_noinfo, true);
} else if (is_no_info(e)) {
flet<bool> let(m_no_info, true);
return visit(get_annotation_arg(e), cs);
} else if (is_typed_expr(e)) {
return visit_typed_expr(e, cs);

19
src/frontends/lean/no_info.cpp Normal file
View file

@ -0,0 +1,19 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "frontends/lean/no_info.h"
namespace lean {
name const & get_no_info() {
static name g_no_info("no_info");
static register_annotation_fn g_no_info_annotation(g_no_info);
return g_no_info;
}
static name g_no_info_name = get_no_info(); // force 'no_info' annotation to be registered
expr mk_no_info(expr const & e) { return mk_annotation(get_no_info(), e); }
bool is_no_info(expr const & e) { return is_annotation(e, get_no_info()); }
}

6
src/frontends/lean/noinfo.h → src/frontends/lean/no_info.h
View file

@ -13,7 +13,7 @@ namespace lean {
Whenever the elaborator finds this annotation it does not generate
information for \c e or any subterm of \c e.
*/
expr mk_noinfo(expr const & e);
/** \brief Return true iff \c e is a term annotated with mk_noinfo */
bool is_noinfo(expr const & e);
expr mk_no_info(expr const & e);
/** \brief Return true iff \c e is a term annotated with mk_no_info */
bool is_no_info(expr const & e);
}

19
src/frontends/lean/noinfo.cpp
View file

@ -1,19 +0,0 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "frontends/lean/noinfo.h"
namespace lean {
name const & get_noinfo() {
static name g_noinfo("noinfo");
static register_annotation_fn g_noinfo_annotation(g_noinfo);
return g_noinfo;
}
static name g_noinfo_name = get_noinfo(); // force 'noinfo' annotation to be registered
expr mk_noinfo(expr const & e) { return mk_annotation(get_noinfo(), e); }
bool is_noinfo(expr const & e) { return is_annotation(e, get_noinfo()); }
}

12
src/frontends/lean/parse_table.cpp
View file

@ -11,18 +11,18 @@ Author: Leonardo de Moura
#include "kernel/free_vars.h"
#include "library/kernel_bindings.h"
#include "frontends/lean/parse_table.h"
#include "frontends/lean/noinfo.h"
#include "frontends/lean/no_info.h"
namespace lean {
namespace notation {
/** \brief Annotate subterms of "macro" \c e with noinfo annotation.
/** \brief Annotate subterms of "macro" \c e with no_info annotation.
1- Variables are not annotated.
2- A constant f in a macro (f ...) is not annotated if (root == true).
3- Every other subterm is annotated with noinfo.
3- Every other subterm is annotated with no_info.
*/
static expr annotate_macro_subterms(expr const & e, bool root = true) {
if (is_var(e) || is_noinfo(e))
if (is_var(e) || is_no_info(e))
return e;
if (is_binding(e))
return update_binding(e,
@ -32,7 +32,7 @@ static expr annotate_macro_subterms(expr const & e, bool root = true) {
bool modified = false;
expr const & f = get_app_args(e, args);
expr new_f;
if ((is_constant(f) && root) || is_noinfo(f)) {
if ((is_constant(f) && root) || is_no_info(f)) {
new_f = f;
} else if (is_annotation(f)) {
name const & k = get_annotation_kind(f);
@ -45,7 +45,7 @@ static expr annotate_macro_subterms(expr const & e, bool root = true) {
modified = true;
}
} else {
new_f = mk_noinfo(f);
new_f = mk_no_info(f);
modified = true;
}
for (expr & arg : args) {