/-
Copyright (c) 2022 E.W.Ayers. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: E.W.Ayers
-/

import Lean
import Mathlib.Lean.Expr.Basic

/-!
# Traversal functions for expressions.
-/

namespace Lean.Expr

/-- Maps `f` on each immediate child of the given expression. -/
def 
traverseChildren: {M : Type → Type ?u.8} → [inst : Applicative M] → (Expr → M Expr) → Expr → M Expr
traverseChildren [
Applicative: (Type ?u.9 → Type ?u.8) → Type (max(?u.9+1)?u.8)
Applicative 
M: ?m.5
M] (
f: Expr → M Expr
f : 
Expr: Type
Expr → 
M: ?m.5
M 
Expr: Type
Expr) : 
Expr: Type
Expr → 
M: ?m.5
M 
Expr: Type
Expr
  | 
e: Expr
e@(
forallE: Name → Expr → Expr → BinderInfo → Expr
forallE _ 
d: Expr
d 
b: Expr
b _) => 
pure: {f : Type ?u.127 → Type ?u.126} → [self : Pure f] → {α : Type ?u.127} → α → f α
pure 
e: Expr
e.
updateForallE!: Expr → Expr → Expr → Expr
updateForallE! <*> 
f: Expr → M Expr
f 
d: Expr
d <*> 
f: Expr → M Expr
f 
b: Expr
b
  | 
e: Expr
e@(
lam: Name → Expr → Expr → BinderInfo → Expr
lam _ 
d: Expr
d 
b: Expr
b _)     => 
pure: {f : Type ?u.292 → Type ?u.291} → [self : Pure f] → {α : Type ?u.292} → α → f α
pure 
e: Expr
e.
updateLambdaE!: Expr → Expr → Expr → Expr
updateLambdaE! <*> 
f: Expr → M Expr
f 
d: Expr
d <*> 
f: Expr → M Expr
f 
b: Expr
b
  | 
e: Expr
e@(
mdata: MData → Expr → Expr
mdata _ 
b: Expr
b)       => 
e: Expr
e.
updateMData!: Expr → Expr → Expr
updateMData! <$> 
f: Expr → M Expr
f 
b: Expr
b
  | 
e: Expr
e@(
letE: Name → Expr → Expr → Expr → Bool → Expr
letE _ 
t: Expr
t 
v: Expr
v 
b: Expr
b _)  => 
pure: {f : Type ?u.523 → Type ?u.522} → [self : Pure f] → {α : Type ?u.523} → α → f α
pure 
e: Expr
e.
updateLet!: Expr → Expr → Expr → Expr → Expr
updateLet! <*> 
f: Expr → M Expr
f 
t: Expr
t <*> 
f: Expr → M Expr
f 
v: Expr
v <*> 
f: Expr → M Expr
f 
b: Expr
b
  | 
e: Expr
e@(
app: Expr → Expr → Expr
app 
l: Expr
l 
r: Expr
r)         => 
pure: {f : Type ?u.645 → Type ?u.644} → [self : Pure f] → {α : Type ?u.645} → α → f α
pure 
e: Expr
e.
updateApp!: Expr → Expr → Expr → Expr
updateApp! <*> 
f: Expr → M Expr
f 
l: Expr
l <*> 
f: Expr → M Expr
f 
r: Expr
r
  | 
e: Expr
e@(
proj: Name → Nat → Expr → Expr
proj _ _ 
b: Expr
b)      => 
e: Expr
e.
updateProj!: Expr → Expr → Expr
updateProj! <$> 
f: Expr → M Expr
f 
b: Expr
b
  | 
e: Expr
e                   => 
pure: {f : Type ?u.752 → Type ?u.751} → [self : Pure f] → {α : Type ?u.752} → α → f α
pure 
e: Expr
e

/-- `e.foldlM f a` folds the monadic function `f` over the subterms of the expression `e`,
with initial value `a`. -/
def 
foldlM: {α : Type} → {m : Type → Type ?u.2094} → [inst : Monad m] → (α → Expr → m α) → α → Expr → m α
foldlM {
α: Type
α : 
Type: Type 1
Type} {
m: ?m.2091
m} [
Monad: (Type ?u.2095 → Type ?u.2094) → Type (max(?u.2095+1)?u.2094)
Monad 
m: ?m.2091
m] (
f: α → Expr → m α
f : 
α: Type
α → 
Expr: Type
Expr → 
m: ?m.2091
m 
α: Type
α) (
x: α
x : 
α: Type
α) (
e: Expr
e : 
Expr: Type
Expr) : 
m: ?m.2091
m 
α: Type
α :=
Prod.snd: {α : Type ?u.2133} → {β : Type ?u.2132} → α × β → β
Prod.snd <$> (
StateT.run: {σ : Type ?u.2144} → {m : Type ?u.2144 → Type ?u.2143} → {α : Type ?u.2144} → StateT σ m α → σ → m (α × σ)
StateT.run (
e: Expr
e.
traverseChildren: {M : Type → Type ?u.2149} → [inst : Applicative M] → (Expr → M Expr) → Expr → M Expr
traverseChildren $ fun 
e': ?m.2170
e' =>
    
Functor.mapConst: {f : Type ?u.2173 → Type ?u.2172} → [self : Functor f] → {α β : Type ?u.2173} → α → f β → f α
Functor.mapConst 
e': ?m.2170
e' (
get: {σ : outParam (Type ?u.2257)} → {m : Type ?u.2257 → Type ?u.2256} → [self : MonadState σ m] → m σ
get >>= 
monadLift: {m : Type ?u.2337 → Type ?u.2336} →
  {n : Type ?u.2337 → Type ?u.2335} → [self : MonadLiftT m n] → {α : Type ?u.2337} → m α → n α
monadLift ∘ 
flip: {α : Sort ?u.2373} → {β : Sort ?u.2372} → {φ : Sort ?u.2371} → (α → β → φ) → β → α → φ
flip 
f: α → Expr → m α
f 
e': ?m.2170
e' >>= 
set: {σ : semiOutParam (Type ?u.2412)} → {m : Type ?u.2412 → Type ?u.2411} → [self : MonadStateOf σ m] → σ → m PUnit
set)) 
x: α
x : 
m: Type → Type ?u.2094
m 
_: Type
_)

end Lean.Expr