diff --git a/GoldbachTm/Tm26/Sim26.lean b/GoldbachTm/Tm26/Sim26.lean index 03bdaf2..5de296e 100644 --- a/GoldbachTm/Tm26/Sim26.lean +++ b/GoldbachTm/Tm26/Sim26.lean @@ -1,15 +1,72 @@ import GoldbachTm.Tm26.TuringMachine26 import GoldbachTm.Basic +set_option maxHeartbeats 0 + open Tm26 -unsafe def foo (cfg : Cfg) : IO Unit := -match (step machine cfg) with -| some cfg => do - IO.println s!"{cfg}" - foo cfg -| none => IO.println s!"halt" +unsafe def foo (cfg : Cfg) (unvisited : List (Fin 26 × Γ)): IO Unit := +do + let unvisited <- pure (List.removeAll unvisited [⟨cfg.q, cfg.Tape.head⟩]) + IO.println s!"{unvisited}" + match (step machine cfg) with + | some cfg => IO.println s!"{cfg}" + foo cfg unvisited + | none => IO.println s!"halt" unsafe def main : List String → IO Unit -| _ => foo (init []) +| _ => foo (init []) [ + ⟨⟨00, by omega⟩, Γ.zero⟩, + ⟨⟨01, by omega⟩, Γ.zero⟩, + ⟨⟨02, by omega⟩, Γ.zero⟩, + ⟨⟨03, by omega⟩, Γ.zero⟩, + ⟨⟨04, by omega⟩, Γ.zero⟩, + ⟨⟨05, by omega⟩, Γ.zero⟩, + ⟨⟨06, by omega⟩, Γ.zero⟩, + ⟨⟨07, by omega⟩, Γ.zero⟩, + ⟨⟨08, by omega⟩, Γ.zero⟩, + ⟨⟨09, by omega⟩, Γ.zero⟩, + ⟨⟨10, by omega⟩, Γ.zero⟩, + ⟨⟨11, by omega⟩, Γ.zero⟩, + ⟨⟨12, by omega⟩, Γ.zero⟩, + ⟨⟨13, by omega⟩, Γ.zero⟩, + ⟨⟨14, by omega⟩, Γ.zero⟩, + ⟨⟨15, by omega⟩, Γ.zero⟩, + ⟨⟨16, by omega⟩, Γ.zero⟩, + ⟨⟨17, by omega⟩, Γ.zero⟩, + ⟨⟨18, by omega⟩, Γ.zero⟩, + ⟨⟨19, by omega⟩, Γ.zero⟩, + ⟨⟨20, by omega⟩, Γ.zero⟩, + ⟨⟨21, by omega⟩, Γ.zero⟩, + ⟨⟨22, by omega⟩, Γ.zero⟩, + ⟨⟨23, by omega⟩, Γ.zero⟩, + ⟨⟨24, by omega⟩, Γ.zero⟩, + ⟨⟨25, by omega⟩, Γ.zero⟩, + ⟨⟨00, by omega⟩, Γ.one⟩, + ⟨⟨01, by omega⟩, Γ.one⟩, + ⟨⟨02, by omega⟩, Γ.one⟩, + ⟨⟨03, by omega⟩, Γ.one⟩, + ⟨⟨04, by omega⟩, Γ.one⟩, + ⟨⟨05, by omega⟩, Γ.one⟩, + ⟨⟨06, by omega⟩, Γ.one⟩, + ⟨⟨07, by omega⟩, Γ.one⟩, + ⟨⟨08, by omega⟩, Γ.one⟩, + ⟨⟨09, by omega⟩, Γ.one⟩, + ⟨⟨10, by omega⟩, Γ.one⟩, + ⟨⟨11, by omega⟩, Γ.one⟩, + ⟨⟨12, by omega⟩, Γ.one⟩, + ⟨⟨13, by omega⟩, Γ.one⟩, + ⟨⟨14, by omega⟩, Γ.one⟩, + ⟨⟨15, by omega⟩, Γ.one⟩, + ⟨⟨16, by omega⟩, Γ.one⟩, + ⟨⟨17, by omega⟩, Γ.one⟩, + ⟨⟨18, by omega⟩, Γ.one⟩, + ⟨⟨19, by omega⟩, Γ.one⟩, + ⟨⟨20, by omega⟩, Γ.one⟩, + ⟨⟨21, by omega⟩, Γ.one⟩, + ⟨⟨22, by omega⟩, Γ.one⟩, + ⟨⟨23, by omega⟩, Γ.one⟩, + ⟨⟨24, by omega⟩, Γ.one⟩, + ⟨⟨25, by omega⟩, Γ.one⟩, +]