Maintain expression dependencies

[AzizZayed]

I have a use case where I need extracted expressions to keep the same parameter variables when it can.

For example:

(datatype Expr
  (Add Expr Expr)
  (Num i64)
  (Mul Expr Expr)
  (Var String)
)

(let e1 (Var "x"))
(let e2  (Num 1))
(let e3 (Add e1 e2))

(rewrite (Add ?x ?y) (Add ?y ?x))

(run 10)

(extract e3)

For now, (extract e3) will output (Add (Num 1) (Var "x")), but I want it to output (Add e2 e1). Is this possible with egglog currently? If not, how can I replicate this functionality with existing commands?

[yihozhang]

The problem is that let-bound vars like e1 and e2 are not extractable. You can workaround this issue by using nullary functions instead (which are extractable by default)

(datatype Expr
  (Add Expr Expr)
  (Num i64)
  (Mul Expr Expr)
  (Var String)
)

(function e1 () Expr)
(function e2 () Expr)

(union (e1) (Var "x"))
(union (e2)  (Num 1))
(let e3 (Add (e1) (e2)))

(rewrite (Add ?x ?y) (Add ?y ?x))

(run 10)

(extract e3)