Skip to content

Commit

Permalink
Add reason-specific machine
Browse files Browse the repository at this point in the history
  • Loading branch information
nickdrozd committed Nov 16, 2023
1 parent 6217673 commit 1a6492f
Show file tree
Hide file tree
Showing 2 changed files with 71 additions and 18 deletions.
22 changes: 8 additions & 14 deletions tm/machine.py
Original file line number Diff line number Diff line change
Expand Up @@ -116,24 +116,18 @@ def show_tape(


class QuickMachine(BasicMachine):
def run(self,
sim_lim: int = 100_000_000,
*,
state: State = 0,
tape: Tape | None = None,
) -> Self:
def run(self, sim_lim: int = 100_000_000) -> Self:
comp = self.comp

if tape is None:
tape = Tape.init()

self.tape = tape
self.tape = tape = Tape.init()

self.blanks = {}

step: int = 0

for cycle in range(sim_lim):
state: State = 0

for cycle in range(sim_lim): # no-branch

if (instr := comp[state, tape.scan]) is None:
self.undfnd = step, (state, tape.scan)
Expand All @@ -151,7 +145,7 @@ def run(self,

step += stepped

if (state := next_state) == -1:
if (state := next_state) == -1: # no-cover
self.halted = step
break

Expand All @@ -162,12 +156,12 @@ def run(self,

self.blanks[state] = step

if state == 0:
if state == 0: # no-cover
self.infrul = True
break

else:
self.xlimit = step
self.xlimit = step # no-cover

self.steps = step
self.cycles = cycle
Expand Down
67 changes: 63 additions & 4 deletions tm/reason.py
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,13 @@
from typing import TYPE_CHECKING
from collections import defaultdict

from tm.parse import tcompile
from tm.program import Program
from tm.machine import QuickMachine as BasicMachine
from tm.lin_rec import History, HeadTape

if TYPE_CHECKING:
from typing import Self

from collections.abc import Callable, Iterator

from tm.program import State, Slot
Expand All @@ -16,16 +18,14 @@

Config = tuple[int, State, HeadTape]

GetResult = Callable[[BasicMachine], int | None]


class BackwardReasoner(Program):
@property
def cant_halt(self) -> bool:
def get_result(machine: BasicMachine) -> int | None:
final: int | None
if (und := machine.undfnd):
final = und[0]
final = und
machine.undfnd = None
else:
final = machine.halted
Expand Down Expand Up @@ -203,3 +203,62 @@ def cant_blank(prog: str) -> bool:

def cant_spin_out(prog: str) -> bool:
return BackwardReasoner(prog).cant_spin_out

########################################

class BasicMachine:
blanks: dict[State, int]

halted: int | None = None
spnout: int | None = None
undfnd: int | None = None

def __init__(self, prog: str):
self.comp = tcompile(prog)

def run(self,
*,
sim_lim: int,
state: State,
tape: HeadTape,
) -> Self:
comp = self.comp

self.blanks = {}

step: int = 0

for _ in range(sim_lim):

if (instr := comp[state, tape.scan]) is None:
self.undfnd = step
break

color, shift, next_state = instr

if (same := state == next_state) and tape.at_edge(shift):
self.spnout = step
break

stepped = tape.step(shift, color, same)

step += stepped

if (state := next_state) == -1:
self.halted = step
break

if not color and tape.blank:
if state in self.blanks: # no-cover
break

self.blanks[state] = step

if state == 0:
break

return self


if TYPE_CHECKING:
GetResult = Callable[[BasicMachine], int | None]

0 comments on commit 1a6492f

Please sign in to comment.