Expr size

Stream: Is there code for X?

[Damiano Testa]

Dear All,

is there some quantity associated with Expressions that is strictly decreasing on sub-Expressions?

I thought of SizeOf.sizeOf, but I may not be using it correctly. Here is what I have.

import Mathlib.Tactic

open Lean

def Lean.Expr.getExprArgs : Expr → Array Expr
  | app fn arg        => #[fn, arg]
  | lam _ bt bb _     => #[bt, bb]
  | forallE _ bt bb _ => #[bt, bb]
  | letE _ t v b _    => #[t, v, b]
  | mdata _ e         => #[e]
  | proj _ _ e        => #[e]
  | _ => #[]

--  This works for my application, but maybe it already exists?
partial
def Lean.Expr.size (e : Expr) : ℕ := (e.getExprArgs.map size).foldl (· + ·) 1

#eval (Expr.const ``Nat []).size  -- 1
#eval (mkNatLit 1).size  -- 9

--  not generating executable code seems to defeat the purpose for my application
#eval sizeOf (Expr.const ``Nat [])  -- failed to compile, wants 'noncomputable'

Thanks!

[Mario Carneiro]

there is approxDepth, but it is approx because it saturates at 255

[Eric Wieser]

Is the motivation here to use it for termination_by and avoid needing partial on recursive defs elsewhere? Or for sorting reasons?

[Damiano Testa]

My motivation is for sorting reasons: I am working on move_add and I want to successively rewrite a term that cannot containEDIT[be contained in] one of the next ones that I will rewrite.

[Damiano Testa]

So, if I am reordering expressions containing a, b, c to "alphabetical" order, I do not want a reordering on a subexpression that is b + a to mess up the expression b + a + c.

[Damiano Testa]

Mario, given the sizes of the terms in Semirings, I am skeptical that a bound of 255 would be safe enough...

[Damiano Testa]

Btw, depth bound is adding one on each layer, right? That would work for me. The difference with what I have is that it would add 1 to the max of what it sees on the ExprArgs, right?