max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor(library/placeholder,library/init/lean/elaborator): encode pexpr placeholders as anonymous mvars

Browse source
This commit is contained in:
Sebastian Ullrich 2018-12-21 15:47:07 +01:00
parent 5757792345
commit 23c83d7e06
2 changed files with 7 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/lean/elaborator.lean
View file

@ -152,7 +152,7 @@ def to_level : syntax → elaborator_m level
st ← get,
match fn.kind with
| some level.leading := (match view level.leading stx, args with
| level.leading.view.hole _, [] := pure $ level.mvar "u" -- TODO(Sebastian): name?
| level.leading.view.hole _, [] := pure $ level.mvar name.anonymous
| level.leading.view.lit lit, [] := pure $ level.of_nat lit.to_nat
| level.leading.view.var id, [] := let id := mangle_ident id in (match st.local_state.univs.find id with
| some _ := pure $ level.param id
@ -204,7 +204,7 @@ def to_pexpr : syntax → elaborator_m expr
let v := view anonymous_constructor stx,
p ← to_pexpr $ mk_app (review hole {}) (v.args.map sep_by.elem.view.item),
pure $ expr.mk_annotation `anonymous_constructor p
| @hole := pure $ expr.const "_" [] -- TODO
| @hole := pure $ expr.mvar name.anonymous dummy
| @«have» := do
let v := view «have» stx,
let id := (mangle_ident <$> opt_ident.view.id <$> v.id).get_or_else `this,

20
src/library/placeholder.cpp
View file

@ -20,29 +20,19 @@ void finalize_placeholder() {
delete g_placeholder_name;
}
LEAN_THREAD_VALUE(unsigned, g_placeholder_id, 0);
static unsigned next_placeholder_id() {
unsigned r = g_placeholder_id;
g_placeholder_id++;
return r;
}
level mk_level_placeholder() { return mk_univ_param(name(*g_placeholder_name, next_placeholder_id())); }
level mk_level_placeholder() { return mk_univ_mvar(name()); }
expr mk_expr_placeholder() {
name n(*g_placeholder_name, next_placeholder_id());
return mk_constant(n);
return mk_mvar(name(), mk_Prop());
}
static bool is_placeholder(name const & n) {
if (n.is_atomic())
return false;
name const & p = n.get_prefix();
return p == *g_placeholder_name;
return n.is_anonymous();
}
bool is_placeholder(level const & e) { return is_param(e) && is_placeholder(param_id(e)); }
bool is_placeholder(level const & e) { return is_mvar(e) && is_placeholder(mvar_id(e)); }
bool is_placeholder(expr const & e) {
expr e2 = unwrap_pos(e);
return is_constant(e2) && is_placeholder(const_name(e2));
return is_mvar(e2) && is_placeholder(mvar_name(e2));
}
bool has_placeholder(level const & l) {