diff --git a/src/app.rs b/src/app.rs index f154789..3682490 100644 --- a/src/app.rs +++ b/src/app.rs @@ -100,7 +100,7 @@ impl App { State::NotState(_) => self.listen_not(&key.code), State::ImpliesState(_) => self.listen_implies(&key.code), State::IffState(_) => self.listen_iff(&key.code), - _ => todo!(), + _ => unreachable!(), } } @@ -585,7 +585,12 @@ impl App { .info_buffer .push_str("Expression entered is invalid"), parser::Result::Success(expr, _) => { - app_context.model.add_assumption(&expr); + if !app_context.model.add_assumption(&expr) { + app_context + .info_buffer + .push_str("Delete all deductions before adding assumptions"); + app_context.warning = true; + } app_context.state = State::Noraml; app_context.reset_expression_box(); } diff --git a/src/fitch.rs b/src/fitch.rs index a267ba8..3318682 100644 --- a/src/fitch.rs +++ b/src/fitch.rs @@ -96,11 +96,16 @@ impl Display for Fitch { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { let mut res = String::new(); let mut temp = self.statements.len() as i32 - 1; + if temp == 0 { + temp = 1; + } + let mut max = 0; while temp > 0 { temp /= 10; max += 1; } + self.statements .iter() .enumerate() @@ -138,6 +143,16 @@ impl Display for Fitch { res.push_str(expression.unwrap().to_string().as_str()); res.push('\n'); }); + + for _ in 0..max + 4 { + res.push(' '); + } + + for _ in 0..self.current_level { + res.push_str(" "); + } + + res.push_str("^\n"); write!(f, "{}", res) } } @@ -151,12 +166,15 @@ impl Fitch { } } - pub fn add_assumption(&mut self, prop: &Rc) { - self.statements.insert( - self.start_of_deductions, - (0, FitchComponent::Deduction(prop.clone())), - ); + pub fn add_assumption(&mut self, prop: &Rc) -> bool { + if self.statements.len() > self.start_of_deductions { + return false; + } + + self.statements + .push((0, FitchComponent::Deduction(prop.clone()))); self.start_of_deductions += 1; + true } pub fn add_subproof(&mut self, prop: &Rc) {