From f46db3cc013c2880e0f165ca2995cda72fa8e834 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 25 Oct 2019 16:47:07 -0700 Subject: [PATCH] feat: add `Expr` helper functions --- library/Init/Lean/Expr.lean | 27 ++++++++++++++++++----- src/kernel/instantiate.cpp | 36 +++++++++++++++++++++++-------- tests/lean/inst.lean | 13 ++++++----- tests/lean/inst.lean.expected.out | 2 ++ 4 files changed, 59 insertions(+), 19 deletions(-) diff --git a/library/Init/Lean/Expr.lean b/library/Init/Lean/Expr.lean index e9a893356c..45c99c9f25 100644 --- a/library/Init/Lean/Expr.lean +++ b/library/Init/Lean/Expr.lean @@ -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⟩ diff --git a/src/kernel/instantiate.cpp b/src/kernel/instantiate.cpp index aa4c5cabda..908c97cf86 100644 --- a/src/kernel/instantiate.cpp +++ b/src/kernel/instantiate.cpp @@ -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(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 { 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(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 { 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))); } diff --git a/tests/lean/inst.lean b/tests/lean/inst.lean index f80bedefe5..f8e77050ec 100644 --- a/tests/lean/inst.lean +++ b/tests/lean/inst.lean @@ -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 diff --git a/tests/lean/inst.lean.expected.out b/tests/lean/inst.lean.expected.out index c6a92db396..e3589f2ffd 100644 --- a/tests/lean/inst.lean.expected.out +++ b/tests/lean/inst.lean.expected.out @@ -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