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

feat: generalize Expr.abstractRange

Browse source 
It now takes free variables **and** metavariables.
This is the first step to make `mkForallFVars` and `mkLambdaFVars`
more general.
This commit is contained in:
Leonardo de Moura 2022-03-08 18:19:17 -08:00
parent d6b782f811
commit 164f07a5e5
4 changed files with 25 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Expr.lean
View file

@ -757,7 +757,7 @@ constant instantiateRange (e : @& Expr) (beginIdx endIdx : @& Nat) (xs : @& Arra
@[extern "lean_expr_instantiate_rev_range"]
constant instantiateRevRange (e : @& Expr) (beginIdx endIdx : @& Nat) (xs : @& Array Expr) : Expr
/-- Replace free variables `xs` with loose bound variables. -/
/-- Replace free (or meta) variables `xs` with loose bound variables. -/
@[extern "lean_expr_abstract"]
constant abstract (e : @& Expr) (xs : @& Array Expr) : Expr

14
src/kernel/abstract.cpp
View file

@ -39,19 +39,23 @@ expr abstract(expr const & e, name const & n) {
static object * lean_expr_abstract_core(object * e0, size_t n, object * subst) {
lean_assert(n <= lean_array_size(subst));
expr const & e = reinterpret_cast<expr const &>(e0);
if (!has_fvar(e)) {
if (!has_fvar(e) && !has_mvar(e)) {
lean_inc(e0);
return e0;
}
expr r = replace(e, [=](expr const & m, unsigned offset) -> optional<expr> {
if (!has_fvar(m))
return some_expr(m); // expression m does not contain free variables
if (is_fvar(m)) {
if (!has_fvar(m) && !has_mvar(m))
return some_expr(m); // expression m does not contain free/meta variables
bool fv = is_fvar(m);
bool mv = is_mvar(m);
if (fv || mv) {
size_t i = n;
while (i > 0) {
--i;
object * v = lean_array_get_core(subst, i);
if (is_fvar_core(v) && fvar_name_core(v) == fvar_name(m))
if (fv && is_fvar_core(v) && fvar_name_core(v) == fvar_name(m))
return some_expr(mk_bvar(offset + n - i - 1));
if (mv && is_mvar_core(v) && mvar_name_core(v) == mvar_name(m))
return some_expr(mk_bvar(offset + n - i - 1));
}
return none_expr();

2
src/kernel/expr.h
View file

@ -145,6 +145,7 @@ struct expr_pair_eq {
static expr_kind expr_kind_core(object * o) { return static_cast<expr_kind>(cnstr_tag(o)); }
inline bool is_bvar(expr const & e) { return e.kind() == expr_kind::BVar; }
inline bool is_fvar_core(object * o) { return expr_kind_core(o) == expr_kind::FVar; }
inline bool is_mvar_core(object * o) { return expr_kind_core(o) == expr_kind::MVar; }
inline bool is_fvar(expr const & e) { return e.kind() == expr_kind::FVar; }
inline bool is_const(expr const & e) { return e.kind() == expr_kind::Const; }
inline bool is_mvar(expr const & e) { return e.kind() == expr_kind::MVar; }
@ -217,6 +218,7 @@ inline bool is_bvar(expr const & e, unsigned i) { return is_bvar(e)
inline name const & fvar_name_core(object * o) { lean_assert(is_fvar_core(o)); return static_cast<name const &>(cnstr_get_ref(o, 0)); }
inline name const & fvar_name(expr const & e) { lean_assert(is_fvar(e)); return static_cast<name const &>(cnstr_get_ref(e, 0)); }
inline level const & sort_level(expr const & e) { lean_assert(is_sort(e)); return static_cast<level const &>(cnstr_get_ref(e, 0)); }
inline name const & mvar_name_core(object * o) { lean_assert(is_mvar_core(o)); return static_cast<name const &>(cnstr_get_ref(o, 0)); }
inline name const & mvar_name(expr const & e) { lean_assert(is_mvar(e)); return static_cast<name const &>(cnstr_get_ref(e, 0)); }
inline name const & const_name(expr const & e) { lean_assert(is_const(e)); return static_cast<name const &>(cnstr_get_ref(e, 0)); }
inline levels const & const_levels(expr const & e) { lean_assert(is_const(e)); return static_cast<levels const &>(cnstr_get_ref(e, 1)); }

13
tests/lean/run/abstractExpr.lean Normal file
View file

@ -0,0 +1,13 @@
import Lean
open Lean
open Lean.Meta
def test : MetaM Unit := do
let x ← mkFreshExprMVar (mkConst ``Nat)
let y ← mkFreshExprMVar (mkConst ``Nat)
let add := mkConst ``Nat.add
let e := mkApp3 add x (mkNatLit 1) y
IO.println (e.abstract #[x, y])
assert! e.abstract #[x, y] == mkApp3 add (mkBVar 1) (mkNatLit 1) (mkBVar 0)
#eval test