Skip to content

Commit

Permalink
Add OR intro-elim and Reiterate event logic
Browse files Browse the repository at this point in the history
  • Loading branch information
@Mroik
Mroik committed May 8, 2024
1 parent 161a1f9 commit 4db1e32
Show file tree
Hide file tree
Showing 2 changed files with 165 additions and 17 deletions.
126 changes: 120 additions & 6 deletions src/app.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,20 +34,24 @@ impl App {
let (title, render_box) = match self.state {
State::AddAssumption => ("Assumption expression", true),
State::AddSubproof => ("Subproof expression", true),
State::AbsurdumState(AbsurdumState::EliminateGetProposition(_)) => {
State::AbsurdumState(AbsurdumState::EliminateGetProposition(_))
| State::OrState(OrState::IntroduceGetProposition(_)) => {
("Expression to introduce", true)
}
State::AbsurdumState(_) => ("Assumption index", true),
State::AndState(AndState::IntroduceGetLeftAssumption)
| State::AndState(AndState::IntroduceGetRightAssumption(_)) => {
("Assumption index to use", true)
}
State::AndState(AndState::EliminateGetAssumption) => {
| State::AndState(AndState::IntroduceGetRightAssumption(_))
| State::OrState(OrState::IntroduceGetAssumption) => ("Assumption index to use", true),
State::AndState(AndState::EliminateGetAssumption)
| State::OrState(OrState::EliminateGetAssumption) => {
("And expression to eliminate", true)
}
State::AndState(AndState::EliminateGetProposition(_)) => {
("And assumption to use", true)
}
State::OrState(OrState::EliminateGetLeftSubproof(_))
| State::OrState(OrState::EliminateGetRightSubproof(_, _)) => ("Subproof to use", true),
State::Reiterate => ("Select proposition to reiterate", true),
_ => ("", false),
};

Expand Down Expand Up @@ -76,10 +80,12 @@ impl App {
State::Noraml => self.listen_normal(&key.code),
State::AddAssumption => self.listen_add_assumption(&key.code),
State::AddSubproof => self.listen_add_subproof(&key.code),
State::Reiterate => self.listen_reiterate(&key.code),
State::IntroduceChoice => self.listen_introduce(&key.code),
State::EliminateChoice => self.listen_eliminate(&key.code),
State::AbsurdumState(_) => self.listen_absurdum(&key.code),
State::AndState(_) => self.listen_and(&key.code),
State::OrState(_) => self.listen_or(&key.code),
_ => todo!(),
}
}
Expand All @@ -90,6 +96,108 @@ impl App {
}
}

fn listen_reiterate(&mut self, code: &KeyCode) {
let handler = |app_context: &mut App| match app_context.expression_buffer.parse() {
Err(_) => {
app_context
.info_buffer
.push_str("The input value is not a valid index");
}
Ok(i) => {
if !app_context.model.reiterate(i) {
app_context.info_buffer.push_str("Invalid index");
app_context.warning = true;
}
app_context.state = State::Noraml;
app_context.reset_expression_box();
}
};
self.handle_expression_box_event(code, handler);
}

fn listen_or(&mut self, code: &KeyCode) {
let handler = |app_context: &mut App| match app_context.state {
State::OrState(OrState::IntroduceGetAssumption) => {
match app_context.expression_buffer.parse() {
Err(_) => {
app_context
.info_buffer
.push_str("The input value is not a valid index");
}
Ok(ass) => {
app_context.state = State::OrState(OrState::IntroduceGetProposition(ass));
app_context.reset_expression_box();
}
}
}
State::OrState(OrState::IntroduceGetProposition(ass)) => {
match parse_expression(&app_context.expression_buffer) {
parser::Result::Failure => app_context
.info_buffer
.push_str("The input expression is not valid"),
parser::Result::Success(ris, _) => {
if !app_context.model.introduce_or(ass, &ris) {
app_context.info_buffer.push_str(
"Select the left or right prop used in the input expression",
);
app_context.warning = true;
}
app_context.state = State::Noraml;
app_context.reset_expression_box();
}
}
}
State::OrState(OrState::EliminateGetAssumption) => {
match app_context.expression_buffer.parse() {
Err(_) => {
app_context
.info_buffer
.push_str("The input value is not a valid index");
}
Ok(ass) => {
app_context.state = State::OrState(OrState::EliminateGetLeftSubproof(ass));
app_context.reset_expression_box();
}
}
}
State::OrState(OrState::EliminateGetLeftSubproof(ass)) => {
match app_context.expression_buffer.parse() {
Err(_) => {
app_context
.info_buffer
.push_str("The input value is not a valid index");
}
Ok(left) => {
app_context.state =
State::OrState(OrState::EliminateGetRightSubproof(ass, left));
app_context.reset_expression_box();
}
}
}
State::OrState(OrState::EliminateGetRightSubproof(ass, left)) => {
match app_context.expression_buffer.parse() {
Err(_) => {
app_context
.info_buffer
.push_str("The input value is not a valid index");
}
Ok(right) => {
if !app_context.model.eliminate_or(ass, left, right) {
app_context
.info_buffer
.push_str("Select the or to eliminate then the 2 subproofs");
app_context.warning = true;
}
app_context.state = State::Noraml;
app_context.reset_expression_box();
}
}
}
_ => (),
};
self.handle_expression_box_event(code, handler);
}

fn listen_and(&mut self, code: &KeyCode) {
let handler = |app_context: &mut App| match app_context.state {
State::AndState(AndState::IntroduceGetLeftAssumption) => {
Expand Down Expand Up @@ -241,6 +349,7 @@ impl App {
self.state = State::AbsurdumState(AbsurdumState::EliminateGetAssumption)
}
KeyCode::Char('n') => self.state = State::AndState(AndState::EliminateGetAssumption),
KeyCode::Char('o') => self.state = State::OrState(OrState::EliminateGetAssumption),
_ => (),
}
}
Expand All @@ -254,6 +363,7 @@ impl App {
KeyCode::Char('n') => {
self.state = State::AndState(AndState::IntroduceGetLeftAssumption)
}
KeyCode::Char('o') => self.state = State::OrState(OrState::IntroduceGetAssumption),
_ => (),
}
}
Expand Down Expand Up @@ -299,6 +409,7 @@ impl App {
KeyCode::Char('a') => self.state = State::AddAssumption,
KeyCode::Char('s') => self.state = State::AddSubproof,
KeyCode::Char('n') => self.model.end_subproof(),
KeyCode::Char('r') => self.state = State::Reiterate,
KeyCode::Char('d') => self.model.delete_last_row(),
KeyCode::Char('q') => self.state = State::Quit,
_ => (),
Expand All @@ -324,7 +435,8 @@ impl App {
}
}
KeyCode::Char(c) => {
self.expression_buffer.push(*c);
self.expression_buffer
.insert(self.expression_cursor as usize, *c);
self.expression_cursor += 1;
}
KeyCode::Esc => {
Expand All @@ -347,6 +459,7 @@ impl App {
"add [a]ssumption",
"add [s]ubproof",
"e[n]d subproof",
"[r]eiterate",
"[d]elete last row",
"[q]uit",
]
Expand All @@ -369,6 +482,7 @@ enum State {
EliminateChoice,
AddAssumption,
AddSubproof,
Reiterate,
AbsurdumState(AbsurdumState),
AndState(AndState),
OrState(OrState),
Expand Down
56 changes: 45 additions & 11 deletions src/fitch.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -123,9 +123,21 @@ impl Display for Fitch {
}
res.push_str(format!("{} | ", i).as_str());

let is_sub = match expression {
FitchComponent::Assumption(_) => true,
_ => false,
};

if is_sub {
res.push('-');
}
for _ in 0..*level {
res.push_str(" ");
}
if is_sub {
res.pop();
}

res.push_str(expression.unwrap().to_string().as_str());
res.push_str("\n");
});
Expand All @@ -145,7 +157,7 @@ impl Fitch {
pub fn add_assumption(&mut self, prop: &Rc<Proposition>) {
self.statements.insert(
self.start_of_deductions,
(0, FitchComponent::Assumption(prop.clone())),
(0, FitchComponent::Deduction(prop.clone())),
);
self.start_of_deductions += 1;
}
Expand Down Expand Up @@ -231,13 +243,21 @@ impl Fitch {
None
}

pub fn reiterate(&mut self, row: usize) {
pub fn reiterate(&mut self, row: usize) -> bool {
if row >= self.statements.len() {
return;
return false;
}

let a = self.statements.get(row).unwrap();
self.statements.push((self.current_level, a.1.clone()));
if a.0 > self.current_level {
return false;
}

self.statements.push((
self.current_level,
FitchComponent::Deduction(a.1.unwrap().clone()),
));
true
}

pub fn introduce_or(&mut self, assum: usize, prop: &Rc<Proposition>) -> bool {
Expand All @@ -246,10 +266,18 @@ impl Fitch {
None => return false,
};

let ris = Proposition::new_or(assum, prop);
self.statements
.push((self.current_level, FitchComponent::Deduction(ris)));
true
match prop.borrow() {
Proposition::Or(left, right) => {
if assum == left || assum == right {
self.statements
.push((self.current_level, FitchComponent::Deduction(prop.clone())));
true
} else {
false
}
}
_ => false,
}
}

// This prolly has some bugs
Expand Down Expand Up @@ -525,11 +553,17 @@ mod tests {
let t0 = Proposition::new_term("A");
let t1 = Proposition::new_term("B");
fitch.add_assumption(&t0);
let ris = fitch.introduce_or(0, &t1);
let mut ris = fitch.introduce_or(0, &Proposition::new_or(&t0, &t1));
assert!(ris);
assert_eq!(
fitch.statements.get(1).unwrap().1.unwrap(),
&Proposition::new_or(&t0, &t1)
);
ris = fitch.introduce_or(0, &Proposition::new_or(&t1, &t0));
assert!(ris);
assert_eq!(
*fitch.statements.get(1).unwrap().1.unwrap(),
Proposition::new_or(&t0, &t1)
fitch.statements.get(2).unwrap().1.unwrap(),
&Proposition::new_or(&t1, &t0)
);
}

Expand Down

0 comments on commit 4db1e32

Please sign in to comment.