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

feat: add Expr helper functions

Browse source
This commit is contained in:
Leonardo de Moura 2019-10-25 16:47:07 -07:00
parent 336caaea63
commit f46db3cc01
4 changed files with 59 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
library/Init/Lean/Expr.lean
View file

@ -84,6 +84,9 @@ args.foldl Expr.app fn
def mkCApp (fn : Name) (args : Array Expr) : Expr :=
mkApp (Expr.const fn []) args
def mkAppRev (fn : Expr) (revArgs : Array Expr) : Expr :=
revArgs.foldr (fun a r => Expr.app r a) fn
namespace Expr
@[extern "lean_expr_hash"]
constant hash (n : @& Expr) : USize := default USize
@ -200,6 +203,15 @@ private def getAppRevArgsAux : Expr → Array Expr → Array Expr
@[inline] def getAppRevArgs (e : Expr) : Array Expr :=
getAppRevArgsAux e (Array.mkEmpty e.getAppNumArgs)
@[specialize] def withAppAux {α} (k : Expr → Array Expr → α) : Expr → Array Expr → Nat → α
| app f a, as, i => withAppAux f (as.set! i a) (i-1)
| f, as, i => k f as
@[inline] def withApp {α} (e : Expr) (k : Expr → Array Expr → α) : α :=
let dummy := Expr.sort Level.zero;
let nargs := e.getAppNumArgs;
withAppAux k e (mkArray nargs dummy) (nargs-1)
def isAppOf (e : Expr) (n : Name) : Bool :=
match e.getAppFn with
| const c _ => c == n
@ -248,22 +260,27 @@ def letName : Expr → Name
/-- Instantiate the loose bound variables in `e` using `subst`.
That is, a loose `Expr.bvar i` is replaced with `subst[i]`. -/
@[extern "lean_expr_instantiate"]
constant instantiate (e : Expr) (subst : Array Expr) : Expr := default _
constant instantiate (e : @& Expr) (subst : @& Array Expr) : Expr := default _
@[extern "lean_expr_instantiate1"]
constant instantiate1 (e : Expr) (subst : Expr) : Expr := default _
constant instantiate1 (e : @& Expr) (subst : @& Expr) : Expr := default _
/-- Similar to instantiate, but `Expr.bvar i` is replaced with `subst[subst.size - i - 1]` -/
@[extern "lean_expr_instantiate_rev"]
constant instantiateRev (e : Expr) (subst : Array Expr) : Expr := default _
constant instantiateRev (e : @& Expr) (subst : @& Array Expr) : Expr := default _
/-- Similar to `instantiate`, but consider only the variables `xs` in the range `[beginIdx, endIdx)`.
Function panics if `beginIdx <= endIdx <= xs.size` does not hold. -/
@[extern "lean_expr_instantiate_range"]
constant instantiateRange (e : @& Expr) (beginIdx endIdx : @& Nat) (xs : Array Expr) : Expr := default _
/-- Replace free variables `xs` with loose bound variables. -/
@[extern "lean_expr_abstract"]
constant abstract (e : Expr) (xs : Array Expr) : Expr := default _
constant abstract (e : @& Expr) (xs : @& Array Expr) : Expr := default _
/-- Similar to `abstract`, but consider only the first `min n xs.size` entries in `xs`. -/
@[extern "lean_expr_abstract_range"]
constant abstractRange (e : Expr) (n : Nat) (xs : Array Expr) : Expr := default _
constant abstractRange (e : @& Expr) (n : @& Nat) (xs : @& Array Expr) : Expr := default _
instance : HasToString Expr :=
⟨Expr.dbgToString⟩

36
src/kernel/instantiate.cpp
View file

@ -56,13 +56,12 @@ extern "C" object * lean_expr_instantiate1(object * a0, object * e0) {
return r.steal();
}
extern "C" object * lean_expr_instantiate(object * a0, object * subst) {
static object * lean_expr_instantiate_core(object * a0, size_t n, object** subst) {
expr const & a = reinterpret_cast<expr const &>(a0);
if (!has_loose_bvars(a)) {
if (!has_loose_bvars(a) || n == 0) {
lean_inc(a0);
return a0;
}
size_t n = lean_array_size(subst);
expr r = replace(a, [=](expr const & m, unsigned offset) -> optional<expr> {
if (offset >= get_loose_bvar_range(m))
return some_expr(m); // expression m does not contain loose bound variables with idx >= offset
@ -71,8 +70,8 @@ extern "C" object * lean_expr_instantiate(object * a0, object * subst) {
if (vidx >= offset) {
size_t h = offset + n;
if (h < offset /* overflow, h is bigger than any vidx */ || (vidx.is_small() && vidx.get_small_value() < h)) {
expr v(lean_array_get_core(subst, vidx.get_small_value() - offset), true);
return some_expr(lift_loose_bvars(v, offset));
object * v = subst[vidx.get_small_value() - offset];
return some_expr(lift_loose_bvars(TO_REF(expr, v), offset));
} else {
return some_expr(mk_bvar(vidx - nat::of_size_t(n)));
}
@ -83,6 +82,24 @@ extern "C" object * lean_expr_instantiate(object * a0, object * subst) {
return r.steal();
}
extern "C" object * lean_expr_instantiate(object * a, object * subst) {
return lean_expr_instantiate_core(a, lean_array_size(subst), lean_array_cptr(subst));
}
extern "C" object * lean_expr_instantiate_range(object * a, object * begin, object * end, object * subst) {
if (!lean_is_scalar(begin) || !lean_is_scalar(end)) {
lean_panic("invalid range for Expr.instantiateRange");
} else {
usize sz = lean_array_size(subst);
usize b = lean_unbox(begin);
usize e = lean_unbox(end);
if (b > e || e > sz) {
lean_panic("invalid range for Expr.instantiateRange");
}
return lean_expr_instantiate_core(a, e - b, lean_array_cptr(subst) + b);
}
}
expr instantiate_rev(expr const & a, unsigned n, expr const * subst) {
if (!has_loose_bvars(a))
return a;
@ -104,13 +121,14 @@ expr instantiate_rev(expr const & a, unsigned n, expr const * subst) {
});
}
extern "C" object * lean_expr_instantiate_rev(object * a0, object * subst) {
extern "C" object * lean_expr_instantiate_rev(object * a0, object * subst0) {
expr const & a = reinterpret_cast<expr const &>(a0);
if (!has_loose_bvars(a)) {
lean_inc(a0);
return a0;
}
size_t n = lean_array_size(subst);
size_t n = lean_array_size(subst0);
object ** subst = lean_array_cptr(subst0);
expr r = replace(a, [=](expr const & m, unsigned offset) -> optional<expr> {
if (offset >= get_loose_bvar_range(m))
return some_expr(m); // expression m does not contain loose bound variables with idx >= offset
@ -119,8 +137,8 @@ extern "C" object * lean_expr_instantiate_rev(object * a0, object * subst) {
if (vidx >= offset) {
size_t h = offset + n;
if (h < offset /* overflow, h is bigger than any vidx */ || (vidx.is_small() && vidx.get_small_value() < h)) {
expr v(lean_array_get_core(subst, n - (vidx.get_small_value() - offset) - 1), true);
return some_expr(lift_loose_bvars(v, offset));
object * v = subst[n - (vidx.get_small_value() - offset) - 1];
return some_expr(lift_loose_bvars(TO_REF(expr, v), offset));
} else {
return some_expr(mk_bvar(vidx - nat::of_size_t(n)));
}

13
tests/lean/inst.lean
View file

@ -9,11 +9,14 @@ let y := Expr.bvar 1;
let t := Expr.app (Expr.app (Expr.app f x) y) x;
let a := mkConst `a;
let b := Expr.app f (mkConst `b);
IO.println t.dbgToString;
IO.println (t.instantiate [a, b].toArray).dbgToString;
IO.println (t.instantiateRev [a, b].toArray).dbgToString;
IO.println (t.instantiate [a].toArray).dbgToString;
IO.println (t.instantiate1 a).dbgToString;
let c := mkConst `c;
IO.println t;
IO.println (t.instantiate #[a, b]);
IO.println (t.instantiateRange 0 2 #[a, b]);
IO.println (t.instantiateRange 2 4 #[c, c, a, b, c]);
IO.println (t.instantiateRev #[a, b]);
IO.println (t.instantiate #[a]);
IO.println (t.instantiate1 a);
pure ()
#eval tst

2
tests/lean/inst.lean.expected.out
View file

@ -1,5 +1,7 @@
f #0 #1 #0
f a (f b) a
f a (f b) a
f a (f b) a
f (f b) a (f b)
f a #0 a
f a #0 a