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

chore(library/init/meta): remove unnecessary primitives

Browse source
This commit is contained in:
Leonardo de Moura 2018-06-05 16:11:30 -07:00
parent 0119926022
commit ab481d7e7b
3 changed files with 5 additions and 206 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
library/init/meta/expr.lean
View file

@ -89,32 +89,11 @@ meta constant expr.lt : expr → expr → bool
meta constant expr.lex_lt : expr → expr → bool
meta constant expr.fold {α : Type} : expr → α → (expr → nat → α → α) → α
meta constant expr.replace : expr → (expr → nat → option expr) → expr
meta constant expr.instantiate_univ_params : expr → list (name × level) → expr
meta constant expr.instantiate_var : expr → expr → expr
meta constant expr.instantiate_vars : expr → list expr → expr
protected meta constant expr.subst : expr elab → expr elab → expr elab
/-- `has_var e` returns true iff e has free variables. -/
meta constant expr.has_bvar_idx : expr → nat → bool
meta constant expr.has_meta_var : expr → bool
/-- `lower_vars e s d` lowers the free variables >= s in `e` by `d`. That is, a free variable `var i` s.t.
`i >= s` is mapped to `var (i-d)`. -/
meta constant expr.lower_vars : expr → nat → nat → expr
/-- Lifts free variables. See `expr.lower_vars` for details. -/
meta constant expr.lift_vars : expr → nat → nat → expr
protected meta constant expr.pos : expr elab → option pos
/-- `copy_pos_info src tgt` copies position information from `src` to `tgt`. -/
meta constant expr.copy_pos_info : expr → expr → expr
meta constant expr.is_internal_cnstr : expr → option uint32
meta constant expr.get_nat_value : expr → option nat
meta constant expr.collect_univ_params : expr → list name
/-- `occurs e t` returns `tt` iff `e` occurs in `t` -/
meta constant expr.occurs : expr → expr → bool
/-- (reflected a) is a special opaque container for a closed `expr` representing `a`.
It can only be obtained via type class inference, which will use the representation

49
library/init/meta/interactive.lean
View file

@ -246,15 +246,7 @@ meta def change (q : parse texpr) : parse (tk "with" *> texpr)? → parse locati
| none (loc.ns [none]) := do e ← i_to_expr q, change_core e none
| none (loc.ns [some h]) := do eq ← i_to_expr q, eh ← get_local h, change_core eq (some eh)
| none _ := fail "change-at does not support multiple locations"
| (some w) l :=
do u ← mk_meta_univ,
ty ← mk_meta_var (sort u),
eq ← i_to_expr ``(%%q : %%ty),
ew ← i_to_expr ``(%%w : %%ty),
let repl := λe : expr, e.replace (λ a n, if a = eq then some ew else none),
l.try_apply
(λh, do e ← infer_type h, change_core (repl e) (some h))
(do g ← target, change_core (repl g) none)
| (some w) l := fail "not implemented yet"
/--
This tactic provides an exact proof term to solve the main goal. If `t` is the goal and `p` is a term of type `u` then `exact p` succeeds if and only if `t` and `u` can be unified.
@ -347,28 +339,6 @@ private meta def generalize_arg_p_aux : pexpr → parser (pexpr × name)
private meta def generalize_arg_p : parser (pexpr × name) :=
with_desc "expr = id" $ parser.pexpr 0 >>= generalize_arg_p_aux
/--
`generalize : e = x` replaces all occurrences of `e` in the target with a new hypothesis `x` of the same type.
`generalize h : e = x` in addition registers the hypothesis `h : e = x`.
-/
meta def generalize (h : parse ident?) (_ : parse $ tk ":") (p : parse generalize_arg_p) : tactic unit :=
propagate_tags $
do let (p, x) := p,
e ← i_to_expr p,
some h ← pure h | tactic.generalize e x >> intro1 >> skip,
tgt ← target,
-- if generalizing fails, fall back to not replacing anything
tgt' ← do {
⟨tgt', _⟩ ← solve_aux tgt (tactic.generalize e x >> target),
to_expr ``(Π x, %%e = x → %%(tgt'.binding_body.lift_vars 0 1))
} <|> to_expr ``(Π x, %%e = x → %%tgt),
t ← assert h tgt',
swap,
exact ``(%%t %%e rfl),
intro x,
intro h
meta def cases_arg_p : parser (option name × pexpr) :=
with_desc "(id :)? expr" $ do
t ← texpr,
@ -413,9 +383,6 @@ For example, given `n : nat` and a goal with a hypothesis `h : P n` and target `
`induction e using r` allows the user to specify the principle of induction that should be used. Here `r` should be a theorem whose result type must be of the form `C t`, where `C` is a bound variable and `t` is a (possibly empty) sequence of bound variables
`induction e generalizing z₁ ... zₙ`, where `z₁ ... zₙ` are variables in the local context, generalizes over `z₁ ... zₙ` before applying the induction but then introduces them in each goal. In other words, the net effect is that each inductive hypothesis is generalized.
`induction h : t` will introduce an equality of the form `h : t = C x y`, asserting that the input term is equal to the current constructor case, to the context.
-/
meta def induction (hp : parse cases_arg_p) (rec_name : parse using_ident) (ids : parse with_ident_list)
(revert : parse $ (tk "generalizing" *> ident*)?) : tactic unit :=
@ -423,10 +390,7 @@ do in_tag ← get_main_tag,
focus1 $ do {
-- process `h : t` case
e ← (match hp with
| (some h, p) := do
x ← get_unused_name,
generalize h () (p, x),
get_local x
| (some h, p) := fail "not implemented yet"
| (none, p) := i_to_expr p),
-- generalize major premise
e ← if e.is_fvar then pure e
@ -517,7 +481,7 @@ match pre with
find_tagged_goal_aux pre
private meta def find_case (goals : list expr) (ty : name) (idx : nat) (num_indices : nat) : option expr → expr → option (expr × expr)
| case e := if e.has_meta_var then match e with
| case e := match e with
| (mvar _ _ _) :=
do case ← case,
guard $ e ∈ goals,
@ -547,7 +511,6 @@ private meta def find_case (goals : list expr) (ty : name) (idx : nat) (num_indi
| (lam _ _ _ e) := find_case case e
| (macro n args) := list.foldl (<|>) none $ args.map (find_case case)
| _ := none
else none
private meta def rename_lams : expr → list name → tactic unit
| (lam n _ _ e) (n'::ns) := (rename n n' >> rename_lams e ns) <|> rename_lams e (n'::ns)
@ -630,11 +593,7 @@ meta def cases : parse cases_arg_p → parse with_ident_list → tactic unit
| (none, p) ids := do
e ← i_to_expr p,
cases_core e ids
| (some h, p) ids := do
x ← get_unused_name,
generalize h () (p, x),
hx ← get_local x,
cases_core hx ids
| (some h, p) ids := fail "not implemented yet"
private meta def try_cases_for_types (type_names : list name) (at_most_one : bool) : tactic unit :=
any_hyp $ λ h, do

141
src/library/vm/vm_expr.cpp
View file

@ -238,59 +238,6 @@ vm_obj expr_fold(vm_obj const &, vm_obj const & e, vm_obj const & a, vm_obj cons
return r;
}
vm_obj expr_replace(vm_obj const & e, vm_obj const & fn) {
expr r = replace(to_expr(e), [&](expr const & o, unsigned d) {
vm_obj new_o = invoke(fn, to_obj(o), mk_vm_nat(d));
if (is_none(new_o))
return none_expr();
else
return some_expr(to_expr(get_some_value(new_o)));
});
return to_obj(r);
}
vm_obj expr_instantiate_univ_params(vm_obj const & e, vm_obj const & nls) {
names ns = to_obj_list<name>(nls, [](vm_obj const & p) {
lean_assert(csize(p) == 2);
return to_name(cfield(p, 0));
} );
levels ls = to_obj_list<level>(nls, [](vm_obj const & p) {
lean_assert(csize(p) == 2);
return to_level(cfield(p, 1));
} );
return to_obj(instantiate_univ_params(to_expr(e), ns, ls));
}
vm_obj expr_instantiate_var(vm_obj const & e, vm_obj const & v) {
return to_obj(instantiate(to_expr(e), to_expr(v)));
}
vm_obj expr_instantiate_vars(vm_obj const & e, vm_obj const & vs) {
buffer<expr> vs_buf;
to_buffer_expr(vs, vs_buf);
return to_obj(instantiate(to_expr(e), vs_buf.size(), vs_buf.data()));
}
vm_obj expr_abstract_local(vm_obj const & e, vm_obj const & n) {
return to_obj(abstract_local(to_expr(e), to_name(n)));
}
static void list_name_to_buffer_local(vm_obj const & o, buffer<expr> & r) {
if (is_simple(o)) {
return;
} else {
expr dummy = mk_Prop();
r.push_back(mk_local(to_name(cfield(o, 0)), dummy));
list_name_to_buffer_local(cfield(o, 1), r);
}
}
vm_obj expr_abstract_locals(vm_obj const & e, vm_obj const & ns) {
buffer<expr> locals;
list_name_to_buffer_local(ns, locals);
return to_obj(abstract_locals(to_expr(e), locals.size(), locals.data()));
}
vm_obj expr_has_bvar_idx(vm_obj const & e, vm_obj const & u) {
if (auto n = try_to_unsigned(u)) {
return mk_vm_bool(has_free_var(to_expr(e), *n));
@ -299,70 +246,11 @@ vm_obj expr_has_bvar_idx(vm_obj const & e, vm_obj const & u) {
}
}
vm_obj expr_has_meta_var(vm_obj const & e) {
return mk_vm_bool(has_metavar(to_expr(e)));
}
vm_obj expr_lift_vars(vm_obj const & e, vm_obj const & n1, vm_obj const & n2) {
auto u1 = try_to_unsigned(n1);
auto u2 = try_to_unsigned(n2);
if (u1 && u2)
return to_obj(lift_free_vars(to_expr(e), *u1, *u2));
else
return e;
}
vm_obj expr_lower_vars(vm_obj const & e, vm_obj const & n1, vm_obj const & n2) {
auto u1 = try_to_unsigned(n1);
auto u2 = try_to_unsigned(n2);
if (u1 && u2)
return to_obj(lower_free_vars(to_expr(e), *u1, *u2));
else
return e;
}
vm_obj expr_hash(vm_obj const & e) {
unsigned r = to_expr(e).hash() % LEAN_VM_MAX_SMALL_NAT;
return mk_vm_simple(r); // make sure it is a simple value
}
vm_obj expr_copy_pos_info(vm_obj const & src, vm_obj const & tgt) {
return to_obj(copy_tag(to_expr(src), copy(to_expr(tgt))));
}
vm_obj expr_is_internal_cnstr(vm_obj const & e) {
auto opt_unsigned = is_internal_cnstr(to_expr(e));
if (opt_unsigned) {
std::cout << *opt_unsigned << std::endl;
vm_obj u = to_obj(*opt_unsigned);
return mk_vm_constructor(1, { u });
} else {
return mk_vm_constructor(0, {});
}
}
vm_obj expr_is_internal_proj(vm_obj const & e) {
auto opt_unsigned = is_internal_proj(to_expr(e));
if (opt_unsigned) {
std::cout << *opt_unsigned << std::endl;
vm_obj u = to_obj(*opt_unsigned);
return mk_vm_constructor(1, { u });
} else {
return mk_vm_constructor(0, {});
}
}
vm_obj expr_is_internal_cases(vm_obj const & e) {
auto opt_unsigned = is_internal_cases(to_expr(e));
if (opt_unsigned) {
std::cout << *opt_unsigned << std::endl;
vm_obj u = to_obj(*opt_unsigned);
return mk_vm_constructor(1, { u });
} else {
return mk_vm_constructor(0, {});
}
}
vm_obj expr_get_nat_value(vm_obj const & o) {
expr e = to_expr(o);
if (is_nat_value(e)) {
@ -405,10 +293,6 @@ vm_obj vm_mk_string_val_ne_proof(vm_obj const & a, vm_obj const & b) {
return to_obj(mk_string_val_ne_proof(to_expr(a), to_expr(b)));
}
vm_obj expr_occurs(vm_obj const & e1, vm_obj const & e2) {
return mk_vm_bool(occurs(to_expr(e1), to_expr(e2)));
}
vm_obj expr_subst(vm_obj const &, vm_obj const & _e1, vm_obj const & _e2) {
expr const & e1 = to_expr(_e1);
expr const & e2 = to_expr(_e2);
@ -439,18 +323,12 @@ vm_obj reflect_string(vm_obj const & s) {
return to_obj(from_string(to_string(s)));
}
vm_obj expr_pos(vm_obj const &, vm_obj const & e) {
if (auto p = get_pos_info(to_expr(e)))
return mk_vm_some(to_obj(*p));
return mk_vm_none();
}
void initialize_vm_expr() {
DECLARE_VM_BUILTIN(name({"expr", "var"}), expr_var_intro);
DECLARE_VM_BUILTIN(name({"expr", "fvar"}), expr_local_const_intro);
DECLARE_VM_BUILTIN(name({"expr", "sort"}), expr_sort_intro);
DECLARE_VM_BUILTIN(name({"expr", "const"}), expr_const_intro);
DECLARE_VM_BUILTIN(name({"expr", "mvar"}), expr_mvar_intro);
DECLARE_VM_BUILTIN(name({"expr", "local_const"}), expr_local_const_intro);
DECLARE_VM_BUILTIN(name({"expr", "app"}), expr_app_intro);
DECLARE_VM_BUILTIN(name({"expr", "lam"}), expr_lam_intro);
DECLARE_VM_BUILTIN(name({"expr", "pi"}), expr_pi_intro);
@ -463,22 +341,9 @@ void initialize_vm_expr() {
DECLARE_VM_BUILTIN(name({"expr", "lt"}), expr_lt);
DECLARE_VM_BUILTIN(name({"expr", "lex_lt"}), expr_lex_lt);
DECLARE_VM_BUILTIN(name({"expr", "fold"}), expr_fold);
DECLARE_VM_BUILTIN(name({"expr", "replace"}), expr_replace);
DECLARE_VM_BUILTIN(name({"expr", "instantiate_univ_params"}), expr_instantiate_univ_params);
DECLARE_VM_BUILTIN(name({"expr", "instantiate_var"}), expr_instantiate_var);
DECLARE_VM_BUILTIN(name({"expr", "instantiate_vars"}), expr_instantiate_vars);
DECLARE_VM_BUILTIN(name({"expr", "subst"}), expr_subst);
DECLARE_VM_BUILTIN(name({"expr", "abstract_local"}), expr_abstract_local);
DECLARE_VM_BUILTIN(name({"expr", "abstract_locals"}), expr_abstract_locals);
DECLARE_VM_BUILTIN(name({"expr", "has_bvar_idx"}), expr_has_bvar_idx);
DECLARE_VM_BUILTIN(name({"expr", "has_meta_var"}), expr_has_meta_var);
DECLARE_VM_BUILTIN(name({"expr", "lift_vars"}), expr_lift_vars);
DECLARE_VM_BUILTIN(name({"expr", "lower_vars"}), expr_lower_vars);
DECLARE_VM_BUILTIN(name({"expr", "hash"}), expr_hash);
DECLARE_VM_BUILTIN(name({"expr", "pos"}), expr_pos);
DECLARE_VM_BUILTIN(name({"expr", "copy_pos_info"}), expr_copy_pos_info);
DECLARE_VM_BUILTIN(name({"expr", "occurs"}), expr_occurs);
DECLARE_VM_BUILTIN(name({"expr", "collect_univ_params"}), expr_collect_univ_params);
DECLARE_VM_CASES_BUILTIN(name({"expr", "cases_on"}), expr_cases_on);
@ -493,10 +358,6 @@ void initialize_vm_expr() {
DECLARE_VM_BUILTIN(name("mk_string_val_ne_proof"), vm_mk_string_val_ne_proof);
DECLARE_VM_BUILTIN(name("expr", "is_annotation"), expr_is_annotation);
// Not sure if we should expose these or what?
DECLARE_VM_BUILTIN(name({"expr", "is_internal_cnstr"}), expr_is_internal_cnstr);
DECLARE_VM_BUILTIN(name({"expr", "get_nat_value"}), expr_get_nat_value);
}
void finalize_vm_expr() {