Folding over typed terms, and walking them with a zipper

Term.fold visits a term's nodes; Term.walk visits them through a zipper — a position in the term, which can move and replace what it is on — and can replace them. Both hand each node to the user as its view at its sort — through ViewFamily, which def.term_view V instantiates — and both take four optional functions: pre and post for a node whose sort a Typ describes, called on reaching it and on leaving it, and prePlain and postPlain for any other node — a constructor at the head of an application, a quantifier's variable list, a term of a parametric datatype. Every node is visited, by one pair or the other.

Both run in a monad Env lifts into. Presenting a node reads its sort, which the library does in Env, and a walk rebuilds what it replaced under, which goes through the term manager.

The order and the steps are those of Cvc.Untyped.Traverse. A typed node's replacement is a term of its sort, so it cannot be ill-sorted, while a plain node's is checked.

Folding

def Cvc.Typed.Term.fold [Ω] {m : Type → Type u_1} {V : Typ → Type} {ρ σ : Type} [Monad m] [MonadLiftT Env m] [ViewFamily V] (t : Term ρ) (init : σ) (pre : {τ : Typ} → Term τ.Denote → V τ → σ → m (FoldPre σ) := fun {τ : Typ} (x : Term τ.Denote) (x_1 : V τ) (s : σ) => pure (FoldPre.descend s)) (post : {τ : Typ} → Term τ.Denote → V τ → σ → m (FoldPost σ) := fun {τ : Typ} (x : Term τ.Denote) (x_1 : V τ) (s : σ) => pure (FoldPost.continue s)) (prePlain : Untyped.Term → σ → m (FoldPre σ) := fun (x : Untyped.Term) (s : σ) => pure (FoldPre.descend s)) (postPlain : Untyped.Term → σ → m (FoldPost σ) := fun (x : Untyped.Term) (s : σ) => pure (FoldPost.continue s)) : m σ

Folds over a term's nodes, in depth-first order, with early exit.

Each node is entered — pre, or prePlain if no Typ describes its sort — then, unless that answered skip, its kids are folded over left to right, and then it is left — post or postPlain. pre and post take the node at its sort, with its view, so matching on the view refines the sort. Every function defaults to carrying on, so a fold passes only those it needs.

Equations

• One or more equations did not get rendered due to their size.

The zipper

A position in a Term ρ, indexed by the root's Lean type and by the focus's sort: some τ if a Typ describes it, none otherwise. Nothing about the path is at the type level. An edit replaces the focus by a term of the same sort — statically for replace, checked for replacePlain — so every ancestor keeps its sort and root answers a Term ρ. Moving answers a Zipper.Any, the sort of where it lands being read off the term.

structure Cvc.Typed.Zipper [Ω] (ρ : Type) (s : Option Typ) : Type

A position in a Term ρ, focused on a node whose sort is s.

• raw : Cvc.Untyped.ZipperOf (Option Cvc.Typ)

@[reducible, inline]

abbrev Cvc.Typed.Zipper.Any [Ω] (ρ : Type) : Type

A zipper at whatever sort its focus has.

Equations

• Cvc.Typed.Zipper.Any ρ = ((s : Option Cvc.Typ) × Cvc.Typed.Zipper ρ s)

@[reducible, inline]

abbrev Cvc.Typed.Zipper.Focus [Ω] : Option Typ → Type

What the focus is, by its sort: a typed term, or a sort-erased one.

Equations

• Cvc.Typed.Zipper.Focus (some τ) = Cvc.Typed.Term τ.Denote
• Cvc.Typed.Zipper.Focus none = Cvc.Untyped.Term

def Cvc.Typed.Zipper.ofTerm [Ω] {ρ : Type} (t : Term ρ) : Env (Any ρ)

A zipper focused on a term's root.

Equations

• Cvc.Typed.Zipper.ofTerm t = do let __do_lift ← Cvc.Typed.View.typOf? t.erase pure (Cvc.Typed.Zipper.ofRaw✝ (Cvc.Untyped.ZipperOf.ofTerm t.erase __do_lift))

def Cvc.Typed.Zipper.focus [Ω] {ρ : Type} {s : Option Typ} : Zipper ρ s → Focus s

The focus.

Equations

• Cvc.Typed.Zipper.focus = fun (z : Cvc.Typed.Zipper ρ (some τ)) => Cvc.Typed.View.reindex (Cvc.Typed.Zipper.raw✝ z).focus
• Cvc.Typed.Zipper.focus = fun (z : Cvc.Typed.Zipper ρ none) => (Cvc.Typed.Zipper.raw✝ z).focus

def Cvc.Typed.Zipper.relaxedFocus [Ω] {ρ : Type} {s : Option Typ} (z : Zipper ρ s) : Untyped.Term

The focus, sort-erased.

Equations

• z.relaxedFocus = (Cvc.Typed.Zipper.raw✝ z).focus

def Cvc.Typed.Zipper.view [Ω] {V : Typ → Type} {ρ : Type} {τ : Typ} [ViewFamily V] (z : Zipper ρ (some τ)) : Env (V τ)

The focus's view.

Equations

• z.view = Cvc.Typed.ViewFamily.viewOf τ z.focus

def Cvc.Typed.Zipper.depth [Ω] {ρ : Type} {s : Option Typ} (z : Zipper ρ s) : Nat

How deep the focus is: 0 at the root.

Equations

• z.depth = (Cvc.Typed.Zipper.raw✝ z).depth

def Cvc.Typed.Zipper.down [Ω] {ρ : Type} {s : Option Typ} (z : Zipper ρ s) (i : Nat) : Env (Option (Any ρ))

Focuses on the i-th kid, if there is one.

Equations

• z.down i = do let __do_lift ← Cvc.Untyped.ZipperOf.downWith Cvc.Typed.View.typOf? (Cvc.Typed.Zipper.raw✝ z) i pure (Option.map Cvc.Typed.Zipper.ofRaw✝ __do_lift)

def Cvc.Typed.Zipper.right [Ω] {ρ : Type} {s : Option Typ} (z : Zipper ρ s) : Env (Option (Any ρ))

Focuses on the next sibling, if there is one.

Equations

• z.right = do let __do_lift ← Cvc.Untyped.ZipperOf.rightWith Cvc.Typed.View.typOf? (Cvc.Typed.Zipper.raw✝ z) pure (Option.map Cvc.Typed.Zipper.ofRaw✝ __do_lift)

def Cvc.Typed.Zipper.left [Ω] {ρ : Type} {s : Option Typ} (z : Zipper ρ s) : Env (Option (Any ρ))

Focuses on the previous sibling, if there is one.

Equations

• z.left = do let __do_lift ← Cvc.Untyped.ZipperOf.leftWith Cvc.Typed.View.typOf? (Cvc.Typed.Zipper.raw✝ z) pure (Option.map Cvc.Typed.Zipper.ofRaw✝ __do_lift)

def Cvc.Typed.Zipper.up [Ω] {ρ : Type} {s : Option Typ} (z : Zipper ρ s) : Env (Option (Any ρ))

Focuses on the parent, if there is one, rebuilding it if anything below it was replaced.

Equations

• z.up = do let __do_lift ← (Cvc.Typed.Zipper.raw✝ z).up pure (Option.map Cvc.Typed.Zipper.ofRaw✝ __do_lift)

def Cvc.Typed.Zipper.root [Ω] {ρ : Type} {s : Option Typ} (z : Zipper ρ s) : Env (Term ρ)

The whole term, with every replacement made.

Equations

• z.root = do let __do_lift ← (Cvc.Typed.Zipper.raw✝ z).root pure (Cvc.Typed.View.reindex __do_lift)

def Cvc.Typed.Zipper.replace [Ω] {ρ : Type} {τ : Typ} (z : Zipper ρ (some τ)) (t : Term τ.Denote) : Zipper ρ (some τ)

Replaces the focus by a term of its sort.

Equations

• z.replace t = { raw := (Cvc.Typed.Zipper.raw✝ z).replaceUnchecked t.erase }

def Cvc.Typed.Zipper.replacePlain [Ω] {ρ : Type} (z : Zipper ρ none) (t : Untyped.Term) : Env (Zipper ρ none)

Replaces a sort-erased focus, checking that the replacement has the focus's sort.

Equations

• z.replacePlain t = do Cvc.Untyped.checkSameSort (Cvc.Typed.Zipper.raw✝ z).focus t pure { raw := (Cvc.Typed.Zipper.raw✝ z).replaceUnchecked t }

def Cvc.Typed.Zipper.Any.root [Ω] {ρ : Type} (z : Any ρ) : Env (Term ρ)

The whole term, with every replacement made.

Equations

• z.root = z.snd.root

Walking

def Cvc.Typed.Term.walk [Ω] {m : Type → Type u_1} {V : Typ → Type} {ρ σ : Type} [Monad m] [MonadLiftT Env m] [ViewFamily V] (t : Term ρ) (init : σ) (pre : {τ : Typ} → Zipper ρ (some τ) → V τ → σ → m (WalkPre σ (Term τ.Denote)) := fun {τ : Typ} (x : Zipper ρ (some τ)) (x_1 : V τ) (s : σ) => pure (WalkPre.descend s)) (post : {τ : Typ} → Zipper ρ (some τ) → V τ → σ → m (WalkPost σ (Term τ.Denote)) := fun {τ : Typ} (x : Zipper ρ (some τ)) (x_1 : V τ) (s : σ) => pure (WalkPost.continue s)) (prePlain : Zipper ρ none → σ → m (WalkPre σ Untyped.Term) := fun (x : Zipper ρ none) (s : σ) => pure (WalkPre.descend s)) (postPlain : Zipper ρ none → σ → m (WalkPost σ Untyped.Term) := fun (x : Zipper ρ none) (s : σ) => pure (WalkPost.continue s)) : m (Term ρ × σ)

Walks a term's nodes through a zipper, in depth-first order, replacing some.

The same order as Term.fold, and the same four functions, each handed the zipper focused on the node — so it sees the node's context too — and answering whether to replace it. A typed node's replacement is a term of its sort; a plain node's is checked against its sort. post sees a node rebuilt with its replaced kids. Answers the rebuilt term with the final state, stop included.

Equations

• One or more equations did not get rendered due to their size.