diff --git a/src/commands/verify_program.rs b/src/commands/verify_program.rs
index ae2e482..1f35cc9 100644
--- a/src/commands/verify_program.rs
+++ b/src/commands/verify_program.rs
@@ -1,4 +1,5 @@
-pub fn run
(program_path: P, specification_path: P, proof_direction: crate::ProofDirection)
+pub fn run
(program_path: P, specification_path: P, proof_direction:
+ crate::problem::ProofDirection)
where
P: AsRef
{
diff --git a/src/input/specification.rs b/src/input/specification.rs
index db5d67e..e03373a 100644
--- a/src/input/specification.rs
+++ b/src/input/specification.rs
@@ -349,15 +349,15 @@ pub(crate) fn parse_specification(mut input: &str, problem: &crate::Problem)
foliage::parse::tokens::identifier(input)
{
Some(("forward", remaining_input)) =>
- (crate::ProofDirection::Forward, remaining_input),
+ (crate::problem::ProofDirection::Forward, remaining_input),
Some(("backward", remaining_input)) =>
- (crate::ProofDirection::Backward, remaining_input),
+ (crate::problem::ProofDirection::Backward, remaining_input),
Some(("both", remaining_input)) =>
- (crate::ProofDirection::Both, remaining_input),
+ (crate::problem::ProofDirection::Both, remaining_input),
Some((identifier, _)) =>
return Err(crate::Error::new_unknown_proof_direction(
identifier.to_string())),
- None => (crate::ProofDirection::Both, input),
+ None => (crate::problem::ProofDirection::Both, input),
};
input = remaining_input.trim_start();
@@ -374,7 +374,7 @@ pub(crate) fn parse_specification(mut input: &str, problem: &crate::Problem)
(proof_direction, input)
},
Some(_)
- | None => (crate::ProofDirection::Both, remaining_input),
+ | None => (crate::problem::ProofDirection::Both, remaining_input),
};
input = remaining_input;
diff --git a/src/lib.rs b/src/lib.rs
index 1ab2abf..0c0845f 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -12,4 +12,4 @@ mod utils;
pub use error::Error;
pub use problem::Problem;
pub(crate) use utils::*;
-pub use utils::{Domain, InputConstantDeclarationDomains, ProofDirection};
+pub use utils::{Domain, InputConstantDeclarationDomains};
diff --git a/src/main.rs b/src/main.rs
index 752128e..ed5c583 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -18,7 +18,7 @@ enum Command
/// Proof direction (forward, backward, both)
#[structopt(long, default_value = "forward")]
- proof_direction: anthem::ProofDirection,
+ proof_direction: anthem::problem::ProofDirection,
}
}
diff --git a/src/problem.rs b/src/problem.rs
index 6c549b1..91c4419 100644
--- a/src/problem.rs
+++ b/src/problem.rs
@@ -1,5 +1,7 @@
+mod proof_direction;
mod section_kind;
+pub use proof_direction::ProofDirection;
pub use section_kind::SectionKind;
#[derive(Copy, Clone, Eq, PartialEq)]
@@ -8,7 +10,7 @@ pub enum StatementKind
Axiom,
Program,
Assumption,
- Lemma(crate::ProofDirection),
+ Lemma(ProofDirection),
Assertion,
}
@@ -124,10 +126,10 @@ impl Problem
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
- || proof_direction == crate::ProofDirection::Both
+ if proof_direction == ProofDirection::Forward
+ || proof_direction == ProofDirection::Both
{
println!("performing forward proof");
@@ -144,7 +146,7 @@ impl Problem
| StatementKind::Assumption
| StatementKind::Program =>
statement.proof_status = ProofStatus::AssumedProven,
- StatementKind::Lemma(crate::ProofDirection::Backward) =>
+ StatementKind::Lemma(ProofDirection::Backward) =>
statement.proof_status = ProofStatus::Ignored,
_ => statement.proof_status = ProofStatus::ToProveLater,
}
@@ -158,8 +160,8 @@ impl Problem
println!("finished forward proof");
}
- if proof_direction == crate::ProofDirection::Backward
- || proof_direction == crate::ProofDirection::Both
+ if proof_direction == ProofDirection::Backward
+ || proof_direction == ProofDirection::Both
{
println!("performing backward proof");
@@ -176,7 +178,7 @@ impl Problem
| StatementKind::Assumption
| StatementKind::Assertion =>
statement.proof_status = ProofStatus::AssumedProven,
- StatementKind::Lemma(crate::ProofDirection::Forward) =>
+ StatementKind::Lemma(ProofDirection::Forward) =>
statement.proof_status = ProofStatus::Ignored,
_ => statement.proof_status = ProofStatus::ToProveLater,
}
diff --git a/src/problem/proof_direction.rs b/src/problem/proof_direction.rs
new file mode 100644
index 0000000..0f586a9
--- /dev/null
+++ b/src/problem/proof_direction.rs
@@ -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
+ {
+ match s
+ {
+ "forward" => Ok(ProofDirection::Forward),
+ "backward" => Ok(ProofDirection::Backward),
+ "both" => Ok(ProofDirection::Both),
+ _ => Err(InvalidProofDirectionError),
+ }
+ }
+}
diff --git a/src/utils.rs b/src/utils.rs
index 48f07b5..1d73d33 100644
--- a/src/utils.rs
+++ b/src/utils.rs
@@ -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
- {
- match s
- {
- "forward" => Ok(ProofDirection::Forward),
- "backward" => Ok(ProofDirection::Backward),
- "both" => Ok(ProofDirection::Both),
- _ => Err(InvalidProofDirectionError),
- }
- }
-}
-
pub(crate) struct ScopedFormula
{
pub free_variable_declarations: std::rc::Rc,