Allow function inlining in quantifiers

Strata/DL/Lambda/LExprEval.lean

@@ -320,6 +320,64 @@ instance : Traceable EvalProvenance Unit where
 
 /-! ## Expression Evaluation -/
 
+/--
+Recursively expand calls to `inline` factory functions everywhere in `e`,
+including under quantifier and lambda binders.
+
+Background: the main `eval` does not descend into binder bodies — closed
+`.abs`/`.quant` terms are canonical values and the small-step `Step`
+relation has no congruence rule that reduces under them. As a result, an
+`inline` factory call inside `forall x, f(x)` is left untouched.
+
+This helper walks the term structurally and at each `.app` that is a
+fully-applied call to an inline function with a body, replaces it with the
+substituted body. Binders are traversed; bvar lifting during substitution
+is handled by `substFvarsLifting`, so the bvars belonging to outer binders
+are preserved correctly.
+
+Use this as a pre-pass before `eval` when you want inline expansion to
+happen inside quantifiers and lambdas.
+
+`fuel` bounds the number of expansion+recursion steps to ensure
+termination on (mutually) recursive inline functions.
+-/
+def expandInlineCalls (F : @Factory TBase) (fuel : Nat) (e : LExpr TBase.mono)
+    : LExpr TBase.mono :=
+  match fuel with
+  | 0 => e
+  | fuel' + 1 =>
+    match e with
+    | .const _ _ | .op _ _ _ | .bvar _ _ | .fvar _ _ _ => e
+    | .abs m name ty body =>
+      .abs m name ty (expandInlineCalls F fuel' body)
+    | .quant m qk name ty tr body =>
+      .quant m qk name ty
+        (expandInlineCalls F fuel' tr)
+        (expandInlineCalls F fuel' body)
+    | .ite m c t f =>
+      .ite m (expandInlineCalls F fuel' c)
+             (expandInlineCalls F fuel' t)
+             (expandInlineCalls F fuel' f)
+    | .eq m e1 e2 =>
+      .eq m (expandInlineCalls F fuel' e1) (expandInlineCalls F fuel' e2)
+    | .app m e1 e2 =>
+      let e1' := expandInlineCalls F fuel' e1
+      let e2' := expandInlineCalls F fuel' e2
+      let e' : LExpr TBase.mono := .app m e1' e2'
+      match F.callOfLFunc e' with
+      | some (op_expr, args, lfunc) =>
+        if h : lfunc.body.isSome
+            && (lfunc.attr.contains FuncAttr.inline) then
+          let body := lfunc.body.get (Bool.and_eq_true_iff.mp h).1
+          match LFunc.computeTypeSubst lfunc op_expr args with
+          | some tySubst =>
+            let body' := body.applySubst tySubst
+            let new_e := substFvarsLifting body' (lfunc.inputs.keys.zip args)
+            expandInlineCalls F fuel' new_e
+          | none => e'
+        else e'
+      | none => e'
+
 /-- Walk a post-eval expression looking for a stuck redex: a fully-applied
 non-constructor factory function whose arguments are all canonical values.
 Such a call *should* have reduced during `eval` but didn't (e.g. missing `body`

Strata/Languages/Core/CmdEval.lean

@@ -20,6 +20,9 @@ open Std (ToFormat Format format)
 namespace CmdEval
 
 def eval (E : Env) (e : Expression.Expr) : Expression.Expr :=
+  -- Pre-pass: expand inline factory calls under quantifier/lambda binders,
+  -- because `LExpr.eval` does not descend into closed binder bodies.
+  let e := LExpr.expandInlineCalls E.exprEnv.config.factory E.exprEnv.config.fuel e
   LExpr.eval E.exprEnv.config.fuel E.exprEnv e
 
 def updateError (E : Env) (e : EvalError Expression) : Env :=

StrataTest/DL/Lambda/InlineInQuantifierTests.lean

@@ -0,0 +1,74 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+/-
+  Reproducer + verification: inline functions inside quantifier bodies.
+
+  - Confirms the original bug: `LExpr.eval` does not expand an `inline` call
+    inside a `forall` body.
+  - Confirms the fix: `LExpr.expandInlineCalls` correctly expands the call
+    under the binder, and then `LExpr.eval` produces the fully reduced form.
+-/
+module
+
+meta import all Strata.DL.Lambda.LExprEval
+
+meta section
+
+namespace Lambda
+open LExpr LTy.Syntax LExpr.SyntaxMono
+
+private abbrev TP : LExprParams := ⟨Unit, Unit⟩
+private instance : Coe String TP.Identifier where coe s := Identifier.mk s ()
+
+-- inline polyEq<a>(x, y) := ∀ (z : a), z == z
+private def polyEqFns : Array (LFunc TP) :=
+  #[{ name := "polyEq",
+      typeArgs := ["a"],
+      attr := #[.inline],
+      inputs := [("x", mty[%a]), ("y", mty[%a])],
+      output := mty[bool],
+      body := some esM[∀ (%a): (%0 == %0)] }]
+
+private def polyState : LState TP :=
+  { (LState.init : LState TP) with
+    config := { (LState.init : LState TP).config with factory := .ofArray polyEqFns } }
+
+-- Top-level call expands as expected.
+private def topCall    : LExpr TP.mono := esM[(((~polyEq : int → int → bool) #1) #2)]
+private def topExpect  : LExpr TP.mono := esM[∀ (int): (%0 == %0)]
+/-- info: true -/
+#guard_msgs in
+#eval (LExpr.eval 100 polyState topCall) == topExpect
+
+-- Same call wrapped inside a forall: original bug — eval leaves it untouched.
+private def quantCall   : LExpr TP.mono :=
+  esM[∀ (int): (((~polyEq : int → int → bool) %0) %0)]
+private def quantExpect : LExpr TP.mono :=
+  esM[∀ (int): (∀ (int): (%0 == %0))]
+
+/-- info: true -/
+#guard_msgs in
+#eval (LExpr.eval 100 polyState quantCall) == quantCall
+
+/-- info: false -/
+#guard_msgs in
+#eval (LExpr.eval 100 polyState quantCall) == quantExpect
+
+-- Fix: expandInlineCalls descends through the forall and rewrites the call.
+/-- info: true -/
+#guard_msgs in
+#eval (LExpr.expandInlineCalls polyState.config.factory 100 quantCall) == quantExpect
+
+-- And piping the pre-pass before eval also yields the expected form.
+/-- info: true -/
+#guard_msgs in
+#eval
+  (LExpr.eval 100 polyState
+    (LExpr.expandInlineCalls polyState.config.factory 100 quantCall)) == quantExpect
+
+end Lambda
+end