What a traversal does next

The answers a traversal's pre and post functions give, shared by everything that folds or walks: the terms of both layers (Cvc.Untyped.Term.fold, Cvc.Typed.Term.walk, …) and proofs (Cvc.Untyped.Solver.Proof.fold, …). Each carries the new state, and says whether to descend, skip, stop, or — for a walk — replace the node.

inductive Cvc.FoldPre (σ : Type) : Type

What a fold does on reaching a node, before its kids.

• descend {σ : Type} (s : σ) : FoldPre σ

  Visit the kids.

• skip {σ : Type} (s : σ) : FoldPre σ

  Do not visit the kids; the node is still left, post and all.

• stop {σ : Type} (s : σ) : FoldPre σ

  End the fold.

inductive Cvc.FoldPost (σ : Type) : Type

What a fold does on leaving a node, after its kids.

• continue {σ : Type} (s : σ) : FoldPost σ

  Carry on.

• stop {σ : Type} (s : σ) : FoldPost σ

  End the fold.

inductive Cvc.WalkPre (σ R : Type) : Type

What a walk does on reaching a node, before its kids. R is what replaces the node.

• descend {σ R : Type} (s : σ) : WalkPre σ R

  Visit the kids.

• skip {σ R : Type} (s : σ) : WalkPre σ R

  Do not visit the kids; the node is still left, post and all.

• replace {σ R : Type} (t : R) (s : σ) : WalkPre σ R

  Replace the node, without visiting the replacement; it is then left.

• replaceAndRevisit {σ R : Type} (t : R) (s : σ) : WalkPre σ R

  Replace the node and visit the replacement, from pre.

• stop {σ R : Type} (s : σ) : WalkPre σ R

  End the walk, keeping every replacement made.

inductive Cvc.WalkPost (σ R : Type) : Type

What a walk does on leaving a node, after its kids. R is what replaces the node.

• continue {σ R : Type} (s : σ) : WalkPost σ R

  Carry on.

• replace {σ R : Type} (t : R) (s : σ) : WalkPost σ R

  Replace the node, and carry on.

• replaceAndRevisit {σ R : Type} (t : R) (s : σ) : WalkPost σ R

  Replace the node and visit the replacement, from pre.

• stop {σ R : Type} (s : σ) : WalkPost σ R

  End the walk, keeping every replacement made.

def Cvc.WalkPre.map {R R' σ : Type} (f : R → R') : WalkPre σ R → WalkPre σ R'

The same step, its replacement mapped.

Equations

• Cvc.WalkPre.map f (Cvc.WalkPre.descend s) = Cvc.WalkPre.descend s
• Cvc.WalkPre.map f (Cvc.WalkPre.skip s) = Cvc.WalkPre.skip s
• Cvc.WalkPre.map f (Cvc.WalkPre.replace t s) = Cvc.WalkPre.replace (f t) s
• Cvc.WalkPre.map f (Cvc.WalkPre.replaceAndRevisit t s) = Cvc.WalkPre.replaceAndRevisit (f t) s
• Cvc.WalkPre.map f (Cvc.WalkPre.stop s) = Cvc.WalkPre.stop s

def Cvc.WalkPost.map {R R' σ : Type} (f : R → R') : WalkPost σ R → WalkPost σ R'

The same step, its replacement mapped.

Equations

• Cvc.WalkPost.map f (Cvc.WalkPost.continue s) = Cvc.WalkPost.continue s
• Cvc.WalkPost.map f (Cvc.WalkPost.replace t s) = Cvc.WalkPost.replace (f t) s
• Cvc.WalkPost.map f (Cvc.WalkPost.replaceAndRevisit t s) = Cvc.WalkPost.replaceAndRevisit (f t) s
• Cvc.WalkPost.map f (Cvc.WalkPost.stop s) = Cvc.WalkPost.stop s