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

feat(frontends/lean): remove feature that in declarations such as (A B : Type), forced A and B to be in the same universe

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-12 15:00:32 -07:00
parent 562926e7ad
commit 60ab6d3bd8
6 changed files with 33 additions and 45 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
library/standard/data/pair.lean
View file

@ -7,12 +7,11 @@
import logic.classes.inhabited logic.connectives.eq
namespace pair
inductive pair (A : Type) (B : Type) : Type :=
inductive pair (A B : Type) : Type :=
| mk_pair : A → B → pair A B
section thms
parameter {A : Type}
parameter {B : Type}
parameters {A B : Type}
definition fst [inline] (p : pair A B) := pair_rec (λ x y, x) p
definition snd [inline] (p : pair A B) := pair_rec (λ x y, y) p

4
library/standard/data/sum.lean
View file

@ -7,12 +7,12 @@
import logic.connectives.prop
namespace sum
inductive sum (A : Type) (B : Type) : Type :=
inductive sum (A B : Type) : Type :=
| inl : A → sum A B
| inr : B → sum A B
infixr `+`:25 := sum
theorem induction_on {A : Type} {B : Type} {C : Prop} (s : A + B) (H1 : A → C) (H2 : B → C) : C :=
theorem induction_on {A B : Type} {C : Prop} (s : A + B) (H1 : A → C) (H2 : B → C) : C :=
sum_rec H1 H2 s
end sum

2
library/standard/logic/axioms/funext.lean
View file

@ -12,7 +12,7 @@ axiom funext : ∀ {A : Type} {B : A → Type} {f g : Π x, B x} (H : ∀ x, f x
namespace function
section
parameters {A : Type} {B : Type} {C : Type} {D : Type}
parameters {A B C D: Type}
theorem compose_assoc (f : C → D) (g : B → C) (h : A → B) : (f ∘ g) ∘ h = f ∘ (g ∘ h) :=
funext (take x, refl _)

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

@ -346,14 +346,19 @@ static environment variables_cmd(parser & p) {
expr type = p.parse_expr();
p.parse_close_binder_info(bi);
level_param_names ls = to_level_param_names(collect_univ_params(type));
level_param_names new_ls;
list<expr> ctx = locals_to_context(type, p);
std::tie(type, new_ls) = p.elaborate_type(type, ctx);
update_section_local_levels(p, new_ls);
ls = append(ls, new_ls);
for (auto id : ids)
env = declare_var(p, env, id, ls, type, false, bi, pos);
if (!p.curr_is_token(g_lparen) && !p.curr_is_token(g_lcurly) && !p.curr_is_token(g_ldcurly) && !p.curr_is_token(g_lbracket))
for (auto id : ids) {
// Hack: to make sure we get different universe parameters for each parameter.
// Alternative: elaborate once and copy types replacing universes in new_ls.
level_param_names new_ls;
expr new_type;
std::tie(new_type, new_ls) = p.elaborate_type(type, ctx);
update_section_local_levels(p, new_ls);
new_ls = append(ls, new_ls);
env = declare_var(p, env, id, new_ls, new_type, false, bi, pos);
}
if (!p.curr_is_token(g_lparen) && !p.curr_is_token(g_lcurly) &&
!p.curr_is_token(g_ldcurly) && !p.curr_is_token(g_lbracket))
break;
}
return env;

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

@ -291,8 +291,6 @@ class elaborator {
name_generator m_ngen;
type_checker_ptr m_tc[2];
substitution m_subst;
expr_map<expr> m_cache; // (pointer equality) cache for Type and Constants (this is a trick to make sure we get the
// same universe metavariable for different occurrences of the same Type/Constant
mvar2meta m_mvar2meta; // mapping from metavariable ?m to the (?m l_1 ... l_n) where [l_1 ... l_n] are the local constants
// representing the context where ?m was created.
context m_context; // current local context: a list of local constants
@ -916,14 +914,7 @@ public:
}
expr visit_sort(expr const & e) {
auto it = m_cache.find(e);
if (it != m_cache.end()) {
return it->second;
} else {
expr r = update_sort(e, replace_univ_placeholder(sort_level(e)));
m_cache.insert(mk_pair(e, r));
return r;
}
return update_sort(e, replace_univ_placeholder(sort_level(e)));
}
expr visit_macro(expr const & e) {
@ -963,27 +954,20 @@ public:
}
expr visit_constant(expr const & e) {
auto it = m_cache.find(e);
if (it != m_cache.end()) {
return it->second;
} else {
declaration d = m_env.get(const_name(e));
buffer<level> ls;
for (level const & l : const_levels(e))
ls.push_back(replace_univ_placeholder(l));
unsigned num_univ_params = length(d.get_univ_params());
if (num_univ_params < ls.size())
throw_kernel_exception(m_env, sstream() << "incorrect number of universe levels parameters for '"
<< const_name(e) << "', #" << num_univ_params
<< " expected, #" << ls.size() << " provided");
// "fill" with meta universe parameters
for (unsigned i = ls.size(); i < num_univ_params; i++)
ls.push_back(mk_meta_univ(m_ngen.next()));
lean_assert(num_univ_params == ls.size());
expr r = update_constant(e, to_list(ls.begin(), ls.end()));
m_cache.insert(mk_pair(e, r));
return r;
}
declaration d = m_env.get(const_name(e));
buffer<level> ls;
for (level const & l : const_levels(e))
ls.push_back(replace_univ_placeholder(l));
unsigned num_univ_params = length(d.get_univ_params());
if (num_univ_params < ls.size())
throw_kernel_exception(m_env, sstream() << "incorrect number of universe levels parameters for '"
<< const_name(e) << "', #" << num_univ_params
<< " expected, #" << ls.size() << " provided");
// "fill" with meta universe parameters
for (unsigned i = ls.size(); i < num_univ_params; i++)
ls.push_back(mk_meta_univ(m_ngen.next()));
lean_assert(num_univ_params == ls.size());
return update_constant(e, to_list(ls.begin(), ls.end()));
}
/** \brief Make sure \c e is a type. If it is not, then try to apply coercions. */

2
tests/lean/run/coe5.lean
View file

@ -36,5 +36,5 @@ namespace setoid
| mk_foo : Π (s1 s2 : setoid) (s3 s4 : setoid), morphism2 s1 s2 → morphism2 s3 s4 → my_struct
check my_struct
definition tst2 : Type.{4} := my_struct.{1 2}
definition tst2 : Type.{4} := my_struct.{1 2 1 2}
end setoid