Skip to content

Commit

Permalink
Use result for backward
Browse files Browse the repository at this point in the history
  • Loading branch information
nickdrozd committed Dec 19, 2024
1 parent 9ad06df commit 0b77b7d
Show file tree
Hide file tree
Showing 3 changed files with 36 additions and 22 deletions.
6 changes: 3 additions & 3 deletions src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -53,17 +53,17 @@ mod wrappers {

#[pyfunction]
pub fn py_cant_halt(prog: &str, depth: Depth) -> Option<Step> {
cant_halt(&CompProg::from_str(prog), depth)
cant_halt(&CompProg::from_str(prog), depth).ok()
}

#[pyfunction]
pub fn py_cant_blank(prog: &str, depth: Depth) -> Option<Step> {
cant_blank(&CompProg::from_str(prog), depth)
cant_blank(&CompProg::from_str(prog), depth).ok()
}

#[pyfunction]
pub fn py_cant_spin_out(prog: &str, depth: Depth) -> Option<Step> {
cant_spin_out(&CompProg::from_str(prog), depth)
cant_spin_out(&CompProg::from_str(prog), depth).ok()
}

#[pyfunction]
Expand Down
44 changes: 29 additions & 15 deletions src/reason.rs
Original file line number Diff line number Diff line change
Expand Up @@ -20,15 +20,29 @@ const MAX_STACK_DEPTH: Depth = 46;

/**************************************/

pub fn cant_halt(comp: &CompProg, depth: Depth) -> Option<Step> {
pub enum BackwardError {
Init,
LinRec,
Spinout,
StepLimit,
DepthLimit,
}

use BackwardError::*;

pub type BackwardResult = Result<Step, BackwardError>;

/**************************************/

pub fn cant_halt(comp: &CompProg, depth: Depth) -> BackwardResult {
cant_reach(comp, depth, halt_configs)
}

pub fn cant_blank(comp: &CompProg, depth: Depth) -> Option<Step> {
pub fn cant_blank(comp: &CompProg, depth: Depth) -> BackwardResult {
cant_reach(comp, depth, erase_configs)
}

pub fn cant_spin_out(comp: &CompProg, depth: Depth) -> Option<Step> {
pub fn cant_spin_out(comp: &CompProg, depth: Depth) -> BackwardResult {
cant_reach(comp, depth, zero_reflexive_configs)
}

Expand All @@ -42,11 +56,11 @@ fn cant_reach(
comp: &CompProg,
depth: Depth,
get_configs: impl Fn(&CompProg) -> Configs,
) -> Option<Step> {
) -> BackwardResult {
let mut configs = get_configs(comp);

if configs.is_empty() {
return Some(0);
return Ok(0);
}

let entrypoints = get_entrypoints(comp);
Expand All @@ -71,23 +85,23 @@ fn cant_reach(
let valid_steps = get_valid_steps(&mut configs, &entrypoints)?;

match valid_steps.len() {
0 => return Some(step),
n if MAX_STACK_DEPTH < n => return None,
0 => return Ok(step),
n if MAX_STACK_DEPTH < n => return Err(DepthLimit),
_ => {},
}

configs = step_configs(valid_steps, &mut blanks)?;
}

None
Err(StepLimit)
}

type ValidatedSteps = Vec<(Vec<Instr>, Config)>;

fn get_valid_steps(
configs: &mut Configs,
entrypoints: &Entrypoints,
) -> Option<ValidatedSteps> {
) -> Result<ValidatedSteps, BackwardError> {
let mut checked = ValidatedSteps::new();

for config in configs.drain(..) {
Expand All @@ -106,7 +120,7 @@ fn get_valid_steps(
&& tape.scan == next_color
&& *state == next_state
{
return None;
return Err(Spinout);
}

good_steps.push((next_color, shift, next_state));
Expand All @@ -119,13 +133,13 @@ fn get_valid_steps(
checked.push((good_steps, config));
}

Some(checked)
Ok(checked)
}

fn step_configs(
configs: ValidatedSteps,
blanks: &mut Blanks,
) -> Option<Configs> {
) -> Result<Configs, BackwardError> {
let mut stepped = Configs::new();

for (instrs, config) in configs {
Expand All @@ -138,7 +152,7 @@ fn step_configs(

if tape.blank() {
if state == 0 {
return None;
return Err(Init);
}

if blanks.contains(&state) {
Expand All @@ -159,15 +173,15 @@ fn step_configs(
next_config.recs += 1;

if next_config.recs > 1 {
return None;
return Err(LinRec);
}
}

stepped.push(next_config);
}
}

Some(stepped)
Ok(stepped)
}

/**************************************/
Expand Down
8 changes: 4 additions & 4 deletions src/tree.rs
Original file line number Diff line number Diff line change
Expand Up @@ -298,9 +298,9 @@ fn skip_all(comp: &CompProg, params: Params, halt: bool) -> bool {

incomplete(comp, params, halt)
|| (states >= 4 && !is_connected(comp, states))
|| cant_reach(comp, 1).is_some()
|| cant_reach(comp, 1).is_ok()
|| quick_term_or_rec(comp, 301, true)
|| cant_reach(comp, 256).is_some()
|| cant_reach(comp, 256).is_ok()
|| check_inf(comp, params, opt_block(comp, 300), 306)
|| segment_cant_reach(comp, params, 3).is_some()
}
Expand Down Expand Up @@ -408,7 +408,7 @@ fn assert_reason(params: Params, halt: u8, expected: (u64, u64)) {
build_tree(params, halt_flag, 300, &|prog| {
*access(&visited_count) += 1;

if let Some(__) = cant_reach(prog, 256) {
if let Ok(__) = cant_reach(prog, 256) {
return;
}

Expand Down Expand Up @@ -605,7 +605,7 @@ fn assert_blank(params: Params, expected: (u64, u64)) {

let run = 700;

if cant_blank(prog, 44).is_some()
if cant_blank(prog, 44).is_ok()
|| quick_term_or_rec(prog, run, true)
|| check_inf(prog, params, opt_block(prog, 300), run as u64)
|| !run_prover(&prog.show(Some(params)), run as u64)
Expand Down

0 comments on commit 0b77b7d

Please sign in to comment.