diff --git a/src/lib.rs b/src/lib.rs index 4a042060..d866d86f 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -53,17 +53,17 @@ mod wrappers { #[pyfunction] pub fn py_cant_halt(prog: &str, depth: Depth) -> Option { - 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 { - 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 { - cant_spin_out(&CompProg::from_str(prog), depth) + cant_spin_out(&CompProg::from_str(prog), depth).ok() } #[pyfunction] diff --git a/src/reason.rs b/src/reason.rs index 9a27cebd..fceb3c80 100644 --- a/src/reason.rs +++ b/src/reason.rs @@ -20,15 +20,29 @@ const MAX_STACK_DEPTH: Depth = 46; /**************************************/ -pub fn cant_halt(comp: &CompProg, depth: Depth) -> Option { +pub enum BackwardError { + Init, + LinRec, + Spinout, + StepLimit, + DepthLimit, +} + +use BackwardError::*; + +pub type BackwardResult = Result; + +/**************************************/ + +pub fn cant_halt(comp: &CompProg, depth: Depth) -> BackwardResult { cant_reach(comp, depth, halt_configs) } -pub fn cant_blank(comp: &CompProg, depth: Depth) -> Option { +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 { +pub fn cant_spin_out(comp: &CompProg, depth: Depth) -> BackwardResult { cant_reach(comp, depth, zero_reflexive_configs) } @@ -42,11 +56,11 @@ fn cant_reach( comp: &CompProg, depth: Depth, get_configs: impl Fn(&CompProg) -> Configs, -) -> Option { +) -> BackwardResult { let mut configs = get_configs(comp); if configs.is_empty() { - return Some(0); + return Ok(0); } let entrypoints = get_entrypoints(comp); @@ -71,15 +85,15 @@ 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, Config)>; @@ -87,7 +101,7 @@ type ValidatedSteps = Vec<(Vec, Config)>; fn get_valid_steps( configs: &mut Configs, entrypoints: &Entrypoints, -) -> Option { +) -> Result { let mut checked = ValidatedSteps::new(); for config in configs.drain(..) { @@ -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)); @@ -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 { +) -> Result { let mut stepped = Configs::new(); for (instrs, config) in configs { @@ -138,7 +152,7 @@ fn step_configs( if tape.blank() { if state == 0 { - return None; + return Err(Init); } if blanks.contains(&state) { @@ -159,7 +173,7 @@ fn step_configs( next_config.recs += 1; if next_config.recs > 1 { - return None; + return Err(LinRec); } } @@ -167,7 +181,7 @@ fn step_configs( } } - Some(stepped) + Ok(stepped) } /**************************************/ diff --git a/src/tree.rs b/src/tree.rs index 1ad0a0a9..e4008bd2 100644 --- a/src/tree.rs +++ b/src/tree.rs @@ -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() } @@ -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; } @@ -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)