wip

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⟩,
+]