Lean4
/-- Return all encodings of `e` as a `Array Key`. This is used for testing. -/
partial def encodeExprWithEta (e : Expr) (labelledStars : Bool) : MetaM (Array (Array Key)) :=
withReducible do
let entries ← (encodingStepWithEta e true (← mkInitLazyEntry labelledStars)).run { bvars := [] }
let entries := entries.map fun (key, entry) => (#[key], entry)
go entries.toArray #[]
where/-- The main loop for `encodeExpr`. -/
go (todo : Array (Array Key × LazyEntry)) (result : Array (Array Key)) : MetaM (Array (Array Key)) := do
if h : todo.size = 0 then
return result
else -- use an if-then-else instead of if-then-return, so that `go` is tail recursive
let (keys, entry) := todo.back
let todo := todo.pop
match ← evalLazyEntry entry true with
| some xs =>
let rec /-- This variation on `List.fold` ensures that the array `keys`
isn't copied unnecessarily. -/
fold xs todo :=
match xs with
| [] => todo
| (key, entry) :: [] => todo.push (keys.push key, entry)
| (key, entry) :: xs => fold xs (todo.push (keys.push key, entry))
go (fold xs todo) result
| none =>
go todo (result.push keys)
