Folding over terms, and walking them with a zipper

Term.fold visits a term's nodes; Term.walk visits them through a zipper and can replace them. Both hand each node to the user as its view, the inductive def.term_view V generates, and both take two optional functions: pre, called on reaching a node, before its kids, and post, called on leaving it, after them. Each answers what to do next — descend, skip the kids, stop, and for a walk replace the node — along with the new state.

fold runs in any monad, taking a term apart being pure. walk needs a monad Env lifts into, to rebuild what it replaced under.

Folding

def Cvc.Untyped.foldWith [Ω] {m : Type → Type u_1} {N σ : Type} [Monad m] (present : Term → m N) (t : Term) (init : σ) (pre : N → σ → m (FoldPre σ)) (post : N → σ → m (FoldPost σ)) : m σ

Folds over a term's nodes, presented as present builds them.

What Term.fold and its typed counterpart are built on. Depth-first: each node is entered — pre — then, unless that answered skip, its kids are folded over left to right, and then it is left — post.

Equations

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

def Cvc.Untyped.Term.fold [Ω] {m : Type → Type u_1} {V σ : Type} [Monad m] [TermView V] (t : Term) (init : σ) (pre : Term → V → σ → m (FoldPre σ) := fun (x : Term) (x_1 : V) (s : σ) => pure (FoldPre.descend s)) (post : Term → V → σ → m (FoldPost σ) := fun (x : Term) (x_1 : V) (s : σ) => pure (FoldPost.continue s)) : m σ

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

Each node is handed over with its view. Both functions default to carrying on, so a fold passes only those it needs: pre to act on reaching a node, and to skip its kids; post to act on leaving it, once its kids are done. Runs in any monad.

Equations

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

The zipper

A position in a term: the focus, and the path back to the root. Each node carries a payload P, computed when the zipper reaches it — nothing for the sort-erased Zipper, its sort for the typed one. Nothing about the path is at the type level: an edit replaces the focus by a term of the same sort, so every ancestor keeps its sort.

structure Cvc.Untyped.ZipperOf.Frame [Ω] (P : Type) : Type

One ancestor of the focus, as the path to the root holds it.

• parent : Cvc.Untyped.Term
• payload : P
• parentDirty : Bool
• left : Cvc.Untyped.Terms
• right : List Cvc.Untyped.Term
• dirty : Bool

structure Cvc.Untyped.ZipperOf [Ω] (P : Type) : Type

A position in a term, each node carrying a payload P.

• term : Cvc.Untyped.Term
• payload : P
• dirty : Bool
• path : List (Cvc.Untyped.ZipperOf.Frame P)

def Cvc.Untyped.ZipperOf.ofTerm [Ω] {P : Type} (t : Term) (payload : P) : ZipperOf P

A zipper focused on a term's root.

Equations

• Cvc.Untyped.ZipperOf.ofTerm t payload = { term := t, payload := payload, dirty := false, path := [] }

def Cvc.Untyped.ZipperOf.focus [Ω] {P : Type} (z : ZipperOf P) : Term

The focus.

Equations

• z.focus = Cvc.Untyped.ZipperOf.term✝ z

def Cvc.Untyped.ZipperOf.payloadOf [Ω] {P : Type} (z : ZipperOf P) : P

The focus's payload.

Equations

• z.payloadOf = Cvc.Untyped.ZipperOf.payload✝ z

def Cvc.Untyped.ZipperOf.depth [Ω] {P : Type} (z : ZipperOf P) : Nat

How deep the focus is: 0 at the root.

Equations

• z.depth = (Cvc.Untyped.ZipperOf.path✝ z).length

def Cvc.Untyped.ZipperOf.downWith [Ω] {m : Type → Type u_1} {P : Type} [Monad m] (pay : Term → m P) (z : ZipperOf P) (i : Nat) : m (Option (ZipperOf P))

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

Equations

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

def Cvc.Untyped.ZipperOf.rightWith [Ω] {m : Type → Type u_1} {P : Type} [Monad m] (pay : Term → m P) (z : ZipperOf P) : m (Option (ZipperOf P))

Focuses on the next sibling, if there is one, computing its payload.

Equations

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

def Cvc.Untyped.ZipperOf.leftWith [Ω] {m : Type → Type u_1} {P : Type} [Monad m] (pay : Term → m P) (z : ZipperOf P) : m (Option (ZipperOf P))

Focuses on the previous sibling, if there is one, computing its payload.

Equations

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

def Cvc.Untyped.ZipperOf.up [Ω] {P : Type} (z : ZipperOf P) : Env (Option (ZipperOf P))

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

Equations

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

partial def Cvc.Untyped.ZipperOf.root [Ω] {P : Type} (z : ZipperOf P) : Env Term

The whole term, with every replacement made.

def Cvc.Untyped.ZipperOf.replaceUnchecked [Ω] {P : Type} (z : ZipperOf P) (t : Term) : ZipperOf P

Replaces the focus, unchecked: the replacement must have the focus's sort.

Equations

• z.replaceUnchecked t = { term := t, payload := Cvc.Untyped.ZipperOf.payload✝ z, dirty := true, path := Cvc.Untyped.ZipperOf.path✝ z }

def Cvc.Untyped.ZipperOf.walkWith [Ω] {m : Type → Type u_1} {P σ : Type} [Monad m] [MonadLiftT Env m] (pay : Term → m P) (z₀ : ZipperOf P) (init : σ) (pre : ZipperOf P → σ → m (WalkPre σ Term)) (post : ZipperOf P → σ → m (WalkPost σ Term)) : m (Term × σ)

Walks a term's nodes through a zipper, presented as the functions see fit.

What Term.walk and its typed counterpart are built on. Depth-first: pre on reaching a node, then — unless it skipped, replaced or stopped — its kids, then post on leaving it. A replacement is unchecked; a stop keeps every replacement made. Answers the rebuilt term and the final state.

Equations

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

The sort-erased zipper

@[reducible, inline]

abbrev Cvc.Untyped.Zipper [Ω] : Type

A position in a sort-erased term.

Equations

• Cvc.Untyped.Zipper = Cvc.Untyped.ZipperOf Unit

def Cvc.Untyped.ZipperOf.ofTermErased [Ω] (t : Term) : Zipper

A sort-erased zipper focused on a term's root.

Equations

• Cvc.Untyped.ZipperOf.ofTermErased t = Cvc.Untyped.ZipperOf.ofTerm t ()

def Cvc.Untyped.ZipperOf.view [Ω] {V : Type} [TermView V] (z : Zipper) : V

The focus's view.

Equations

• Cvc.Untyped.ZipperOf.view z = Cvc.Untyped.TermView.viewOf (Cvc.Untyped.ZipperOf.focus z)

def Cvc.Untyped.ZipperOf.down [Ω] (z : Zipper) (i : Nat) : Option Zipper

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

Equations

• Cvc.Untyped.ZipperOf.down z i = (Cvc.Untyped.ZipperOf.downWith (fun (x : Cvc.Untyped.Term) => pure ()) z i).run

def Cvc.Untyped.ZipperOf.right [Ω] (z : Zipper) : Option Zipper

Focuses on the next sibling, if there is one.

Equations

• Cvc.Untyped.ZipperOf.right z = (Cvc.Untyped.ZipperOf.rightWith (fun (x : Cvc.Untyped.Term) => pure ()) z).run

def Cvc.Untyped.ZipperOf.left [Ω] (z : Zipper) : Option Zipper

Focuses on the previous sibling, if there is one.

Equations

• Cvc.Untyped.ZipperOf.left z = (Cvc.Untyped.ZipperOf.leftWith (fun (x : Cvc.Untyped.Term) => pure ()) z).run

def Cvc.Untyped.checkSameSort [Ω] (old new : Term) : Env Unit

Fails unless a replacement has the sort of what it replaces.

Equations

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

def Cvc.Untyped.ZipperOf.replace [Ω] (z : Zipper) (t : Term) : Env Zipper

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

Equations

• Cvc.Untyped.ZipperOf.replace z t = do Cvc.Untyped.checkSameSort (Cvc.Untyped.ZipperOf.focus z) t pure (Cvc.Untyped.ZipperOf.replaceUnchecked z t)

def Cvc.Untyped.Term.walk [Ω] {m : Type → Type u_1} {V σ : Type} [Monad m] [MonadLiftT Env m] [TermView V] (t : Term) (init : σ) (pre : Zipper → V → σ → m (WalkPre σ Term) := fun (x : Zipper) (x_1 : V) (s : σ) => pure (WalkPre.descend s)) (post : Zipper → V → σ → m (WalkPost σ Term) := fun (x : Zipper) (x_1 : V) (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 two optional functions, each handed the zipper focused on the node — so it sees the node's context too — and its view, and answering whether to replace it. A replacement must have the sort of the node it replaces, which is checked. post sees a node rebuilt with its replaced kids. Answers the rebuilt term with the final state, stop included.

Runs in any monad Env lifts into, since rebuilding a term needs Env.

Equations

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