Example.lean

/-
Executable non-vacuity checks.

The theorems in this development are universally quantified, so they would also
hold of a degenerate model in which nothing ever happens.  These examples run
the *published* LMR machinery -- `Scaffold.append`, path-named targets, the
tree unfolding -- on concrete inputs and check the decoded result against a
hand-computed answer, so a degenerate definition would be visible here.

Everything is closed by `decide` or `rfl`, i.e. by kernel computation.
-/

import FPRDTransfer.RealtimeTransfer

namespace FPRD
namespace Examples

/-! ### A one-stack machine that records its input -/

/-- Push every input symbol onto the single stack. -/
def recorder : StackMachine Bool Unit Bool 1 where
  step := fun _ x _ => ((), fun _ => .push x)
  init := ()
  accept := fun _ => true

/-- The stack holds the input reversed, top first. -/
example : (recorder.run [true, false, false]).stacks 0 = [false, false, true] := by decide

/-- The compiled scaffolding automaton appends one node per input symbol. -/
example : ((compile recorder).run [true, false, false]).2.top = 3 := by decide

/-- Decoding the compiled scaffold reproduces the stack.  This exercises
`Scaffold.append`, target resolution by port word, and `decode`. -/
example :
    decode ((compile recorder).run [true, false, false]).2 0
      ((compile recorder).run [true, false, false]).2.top = [false, false, true] := by
  rw [decode_eq_decodeAux]; decide

/-! ### A one-stack machine that pops -/

/-- Push on `true`, pop on `false`.  Exercises the `pop` port word `[j, j]`,
including popping the empty stack. -/
def pusher : StackMachine Bool Unit Bool 1 where
  step := fun _ x _ => ((), fun _ => if x then .push true else .pop)
  init := ()
  accept := fun _ => true

/-- Popping an empty stack is a no-op, and the encoding agrees.  This is the
case `CleanEmpty` exists to protect: the first `false` pops an empty stack. -/
example : (pusher.run [false, true, true, false]).stacks 0 = [true] := by decide

example :
    decode ((compile pusher).run [false, true, true, false]).2 0
      ((compile pusher).run [false, true, true, false]).2.top = [true] := by
  rw [decode_eq_decodeAux]; decide

/-- A longer alternation through three consecutive empty-stack pops.  The
generated empty tops have missing same-stack ports; the example checks the
decoded result without claiming that this run realizes the more general stale
history excluded by `CleanEmpty`. -/
example :
    decode ((compile pusher).run [true, false, false, false, true]).2 0
      ((compile pusher).run [true, false, false, false, true]).2.top = [true] := by
  rw [decode_eq_decodeAux]; decide

/-! ### A one-tape machine through the zipper -/

/-- Write the input symbol and move right, forever. -/
def copier : MultiTapeMachine Bool Unit (Option Bool) 1 where
  blank := none
  step := fun _ x _ => ((), fun _ => (some x, .right))
  init := ()
  accept := fun _ => true

/-- The tape's left half is the input reversed; the head sits on a blank. -/
example : ((copier.run [true, false, true]).tapes 0).left
    = [some true, some false, some true] := by decide

example : ((copier.run [true, false, true]).tapes 0).cur = none := by decide

/-- The scaffold compiled through the zipper decodes to the same tape half.
Degree is `2 * 1 = 2`, distance `2`, three nodes for three symbols. -/
example :
    decode ((compile copier.toStack).run [true, false, true]).2 (leftIdx 0)
      ((compile copier.toStack).run [true, false, true]).2.top
      = [some true, some false, some true] := by
  rw [decode_eq_decodeAux]; decide

example : ((compile copier.toStack).run [true, false, true]).2.top = 3 := by decide

/-- The right half stays empty: a blank is read there, not a recorded cell. -/
example :
    decode ((compile copier.toStack).run [true, false, true]).2 (rightIdx 0)
      ((compile copier.toStack).run [true, false, true]).2.top = [] := by
  rw [decode_eq_decodeAux]; decide

end Examples
end FPRD