Move ProofDirection type to separate module

This commit is contained in:
Patrick Lühne 2020-05-11 03:46:11 +02:00
parent 7c36c4b239
commit 0d51053b88
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
7 changed files with 81 additions and 79 deletions

View File

@ -1,4 +1,5 @@
pub fn run<P>(program_path: P, specification_path: P, proof_direction: crate::ProofDirection) pub fn run<P>(program_path: P, specification_path: P, proof_direction:
crate::problem::ProofDirection)
where where
P: AsRef<std::path::Path> P: AsRef<std::path::Path>
{ {

View File

@ -349,15 +349,15 @@ pub(crate) fn parse_specification(mut input: &str, problem: &crate::Problem)
foliage::parse::tokens::identifier(input) foliage::parse::tokens::identifier(input)
{ {
Some(("forward", remaining_input)) => Some(("forward", remaining_input)) =>
(crate::ProofDirection::Forward, remaining_input), (crate::problem::ProofDirection::Forward, remaining_input),
Some(("backward", remaining_input)) => Some(("backward", remaining_input)) =>
(crate::ProofDirection::Backward, remaining_input), (crate::problem::ProofDirection::Backward, remaining_input),
Some(("both", remaining_input)) => Some(("both", remaining_input)) =>
(crate::ProofDirection::Both, remaining_input), (crate::problem::ProofDirection::Both, remaining_input),
Some((identifier, _)) => Some((identifier, _)) =>
return Err(crate::Error::new_unknown_proof_direction( return Err(crate::Error::new_unknown_proof_direction(
identifier.to_string())), identifier.to_string())),
None => (crate::ProofDirection::Both, input), None => (crate::problem::ProofDirection::Both, input),
}; };
input = remaining_input.trim_start(); input = remaining_input.trim_start();
@ -374,7 +374,7 @@ pub(crate) fn parse_specification(mut input: &str, problem: &crate::Problem)
(proof_direction, input) (proof_direction, input)
}, },
Some(_) Some(_)
| None => (crate::ProofDirection::Both, remaining_input), | None => (crate::problem::ProofDirection::Both, remaining_input),
}; };
input = remaining_input; input = remaining_input;

View File

@ -12,4 +12,4 @@ mod utils;
pub use error::Error; pub use error::Error;
pub use problem::Problem; pub use problem::Problem;
pub(crate) use utils::*; pub(crate) use utils::*;
pub use utils::{Domain, InputConstantDeclarationDomains, ProofDirection}; pub use utils::{Domain, InputConstantDeclarationDomains};

View File

@ -18,7 +18,7 @@ enum Command
/// Proof direction (forward, backward, both) /// Proof direction (forward, backward, both)
#[structopt(long, default_value = "forward")] #[structopt(long, default_value = "forward")]
proof_direction: anthem::ProofDirection, proof_direction: anthem::problem::ProofDirection,
} }
} }

View File

@ -1,5 +1,7 @@
mod proof_direction;
mod section_kind; mod section_kind;
pub use proof_direction::ProofDirection;
pub use section_kind::SectionKind; pub use section_kind::SectionKind;
#[derive(Copy, Clone, Eq, PartialEq)] #[derive(Copy, Clone, Eq, PartialEq)]
@ -8,7 +10,7 @@ pub enum StatementKind
Axiom, Axiom,
Program, Program,
Assumption, Assumption,
Lemma(crate::ProofDirection), Lemma(ProofDirection),
Assertion, Assertion,
} }
@ -124,10 +126,10 @@ impl Problem
section.push(statement); section.push(statement);
} }
pub fn prove(&self, proof_direction: crate::ProofDirection) -> Result<(), crate::Error> pub fn prove(&self, proof_direction: ProofDirection) -> Result<(), crate::Error>
{ {
if proof_direction == crate::ProofDirection::Forward if proof_direction == ProofDirection::Forward
|| proof_direction == crate::ProofDirection::Both || proof_direction == ProofDirection::Both
{ {
println!("performing forward proof"); println!("performing forward proof");
@ -144,7 +146,7 @@ impl Problem
| StatementKind::Assumption | StatementKind::Assumption
| StatementKind::Program => | StatementKind::Program =>
statement.proof_status = ProofStatus::AssumedProven, statement.proof_status = ProofStatus::AssumedProven,
StatementKind::Lemma(crate::ProofDirection::Backward) => StatementKind::Lemma(ProofDirection::Backward) =>
statement.proof_status = ProofStatus::Ignored, statement.proof_status = ProofStatus::Ignored,
_ => statement.proof_status = ProofStatus::ToProveLater, _ => statement.proof_status = ProofStatus::ToProveLater,
} }
@ -158,8 +160,8 @@ impl Problem
println!("finished forward proof"); println!("finished forward proof");
} }
if proof_direction == crate::ProofDirection::Backward if proof_direction == ProofDirection::Backward
|| proof_direction == crate::ProofDirection::Both || proof_direction == ProofDirection::Both
{ {
println!("performing backward proof"); println!("performing backward proof");
@ -176,7 +178,7 @@ impl Problem
| StatementKind::Assumption | StatementKind::Assumption
| StatementKind::Assertion => | StatementKind::Assertion =>
statement.proof_status = ProofStatus::AssumedProven, statement.proof_status = ProofStatus::AssumedProven,
StatementKind::Lemma(crate::ProofDirection::Forward) => StatementKind::Lemma(ProofDirection::Forward) =>
statement.proof_status = ProofStatus::Ignored, statement.proof_status = ProofStatus::Ignored,
_ => statement.proof_status = ProofStatus::ToProveLater, _ => statement.proof_status = ProofStatus::ToProveLater,
} }

View File

@ -0,0 +1,62 @@
#[derive(Clone, Copy, Eq, Hash, PartialEq)]
pub enum ProofDirection
{
Forward,
Backward,
Both,
}
impl std::fmt::Debug for ProofDirection
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
match self
{
ProofDirection::Forward => write!(formatter, "forward"),
ProofDirection::Backward => write!(formatter, "backward"),
ProofDirection::Both => write!(formatter, "both"),
}
}
}
impl std::fmt::Display for ProofDirection
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(formatter, "{:?}", self)
}
}
pub struct InvalidProofDirectionError;
impl std::fmt::Debug for InvalidProofDirectionError
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(formatter, "invalid proof direction")
}
}
impl std::fmt::Display for InvalidProofDirectionError
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(formatter, "{:?}", self)
}
}
impl std::str::FromStr for ProofDirection
{
type Err = InvalidProofDirectionError;
fn from_str(s: &str) -> Result<Self, Self::Err>
{
match s
{
"forward" => Ok(ProofDirection::Forward),
"backward" => Ok(ProofDirection::Backward),
"both" => Ok(ProofDirection::Both),
_ => Err(InvalidProofDirectionError),
}
}
}

View File

@ -38,69 +38,6 @@ impl std::fmt::Display for Domain
} }
} }
#[derive(Clone, Copy, Eq, Hash, PartialEq)]
pub enum ProofDirection
{
Forward,
Backward,
Both,
}
impl std::fmt::Debug for ProofDirection
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
match self
{
ProofDirection::Forward => write!(formatter, "forward"),
ProofDirection::Backward => write!(formatter, "backward"),
ProofDirection::Both => write!(formatter, "both"),
}
}
}
impl std::fmt::Display for ProofDirection
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(formatter, "{:?}", self)
}
}
pub struct InvalidProofDirectionError;
impl std::fmt::Debug for InvalidProofDirectionError
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(formatter, "invalid proof direction")
}
}
impl std::fmt::Display for InvalidProofDirectionError
{
fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
{
write!(formatter, "{:?}", self)
}
}
impl std::str::FromStr for ProofDirection
{
type Err = InvalidProofDirectionError;
fn from_str(s: &str) -> Result<Self, Self::Err>
{
match s
{
"forward" => Ok(ProofDirection::Forward),
"backward" => Ok(ProofDirection::Backward),
"both" => Ok(ProofDirection::Both),
_ => Err(InvalidProofDirectionError),
}
}
}
pub(crate) struct ScopedFormula pub(crate) struct ScopedFormula
{ {
pub free_variable_declarations: std::rc::Rc<foliage::VariableDeclarations>, pub free_variable_declarations: std::rc::Rc<foliage::VariableDeclarations>,