From 25736256e696b51d6fe288398ccc3c52ec583b32 Mon Sep 17 00:00:00 2001 From: Tobias Stolzmann Date: Wed, 22 Nov 2023 23:13:28 +0100 Subject: [PATCH] Move UnboxedFormula in a separate module for convenience features --- src/convenience/mod.rs | 1 + src/convenience/unbox/fol.rs | 51 ++++++++++++++++++++++++ src/convenience/unbox/mod.rs | 44 +++++++++++++++++++++ src/main.rs | 1 + src/simplifying/fol/ht.rs | 5 ++- src/syntax_tree/fol.rs | 77 ------------------------------------ 6 files changed, 101 insertions(+), 78 deletions(-) create mode 100644 src/convenience/mod.rs create mode 100644 src/convenience/unbox/fol.rs create mode 100644 src/convenience/unbox/mod.rs diff --git a/src/convenience/mod.rs b/src/convenience/mod.rs new file mode 100644 index 00000000..4fa2c769 --- /dev/null +++ b/src/convenience/mod.rs @@ -0,0 +1 @@ +pub mod unbox; diff --git a/src/convenience/unbox/fol.rs b/src/convenience/unbox/fol.rs new file mode 100644 index 00000000..db70cb51 --- /dev/null +++ b/src/convenience/unbox/fol.rs @@ -0,0 +1,51 @@ +use crate::syntax_tree::fol::{ + AtomicFormula, BinaryConnective, Formula, Quantification, UnaryConnective, +}; + +pub enum UnboxedFormula { + AtomicFormula(AtomicFormula), + UnaryFormula { + connective: UnaryConnective, + formula: Formula, + }, + BinaryFormula { + connective: BinaryConnective, + lhs: Formula, + rhs: Formula, + }, + QuantifiedFormula { + quantification: Quantification, + formula: Formula, + }, +} + +impl UnboxedFormula { + pub fn rebox(self) -> Formula { + match self { + Self::AtomicFormula(f) => Formula::AtomicFormula(f), + Self::UnaryFormula { + connective, + formula, + } => Formula::UnaryFormula { + connective, + formula: Box::new(formula), + }, + Self::BinaryFormula { + connective, + lhs, + rhs, + } => Formula::BinaryFormula { + connective, + lhs: Box::new(lhs), + rhs: Box::new(rhs), + }, + Self::QuantifiedFormula { + quantification, + formula, + } => Formula::QuantifiedFormula { + quantification, + formula: Box::new(formula), + }, + } + } +} diff --git a/src/convenience/unbox/mod.rs b/src/convenience/unbox/mod.rs new file mode 100644 index 00000000..cc2c3c6b --- /dev/null +++ b/src/convenience/unbox/mod.rs @@ -0,0 +1,44 @@ +use crate::syntax_tree::fol::Formula; + +use self::fol::UnboxedFormula; + +pub mod fol; + +pub trait Unbox { + type Unboxed; + + fn unbox(self) -> Self::Unboxed; +} + +impl Unbox for Formula { + type Unboxed = UnboxedFormula; + + fn unbox(self) -> UnboxedFormula { + match self { + Self::AtomicFormula(f) => UnboxedFormula::AtomicFormula(f), + Self::UnaryFormula { + connective, + formula, + } => UnboxedFormula::UnaryFormula { + connective, + formula: *formula, + }, + Self::BinaryFormula { + connective, + lhs, + rhs, + } => UnboxedFormula::BinaryFormula { + connective, + lhs: *lhs, + rhs: *rhs, + }, + Self::QuantifiedFormula { + quantification, + formula, + } => UnboxedFormula::QuantifiedFormula { + quantification, + formula: *formula, + }, + } + } +} diff --git a/src/main.rs b/src/main.rs index 8c515fa9..800eca80 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1,3 +1,4 @@ +pub mod convenience; pub mod formatting; pub mod parsing; pub mod simplifying; diff --git a/src/simplifying/fol/ht.rs b/src/simplifying/fol/ht.rs index 8073903f..2f48be4d 100644 --- a/src/simplifying/fol/ht.rs +++ b/src/simplifying/fol/ht.rs @@ -1,4 +1,7 @@ -use crate::syntax_tree::fol::{AtomicFormula, BinaryConnective, Formula, UnboxedFormula}; +use crate::{ + convenience::unbox::{fol::UnboxedFormula, Unbox as _}, + syntax_tree::fol::{AtomicFormula, BinaryConnective, Formula}, +}; pub fn simplify(formula: Formula) -> Formula { simplify_outer(match formula { diff --git a/src/syntax_tree/fol.rs b/src/syntax_tree/fol.rs index d9c7dadd..dc805d41 100644 --- a/src/syntax_tree/fol.rs +++ b/src/syntax_tree/fol.rs @@ -259,83 +259,6 @@ impl Formula { Formula::QuantifiedFormula { formula, .. } => formula.variables(), } } - - pub fn unbox(self) -> UnboxedFormula { - match self { - Self::AtomicFormula(f) => UnboxedFormula::AtomicFormula(f), - Self::UnaryFormula { - connective, - formula, - } => UnboxedFormula::UnaryFormula { - connective, - formula: *formula, - }, - Self::BinaryFormula { - connective, - lhs, - rhs, - } => UnboxedFormula::BinaryFormula { - connective, - lhs: *lhs, - rhs: *rhs, - }, - Self::QuantifiedFormula { - quantification, - formula, - } => UnboxedFormula::QuantifiedFormula { - quantification, - formula: *formula, - }, - } - } -} - -pub enum UnboxedFormula { - AtomicFormula(AtomicFormula), - UnaryFormula { - connective: UnaryConnective, - formula: Formula, - }, - BinaryFormula { - connective: BinaryConnective, - lhs: Formula, - rhs: Formula, - }, - QuantifiedFormula { - quantification: Quantification, - formula: Formula, - }, -} - -impl UnboxedFormula { - pub fn rebox(self) -> Formula { - match self { - Self::AtomicFormula(f) => Formula::AtomicFormula(f), - Self::UnaryFormula { - connective, - formula, - } => Formula::UnaryFormula { - connective, - formula: Box::new(formula), - }, - Self::BinaryFormula { - connective, - lhs, - rhs, - } => Formula::BinaryFormula { - connective, - lhs: Box::new(lhs), - rhs: Box::new(rhs), - }, - Self::QuantifiedFormula { - quantification, - formula, - } => Formula::QuantifiedFormula { - quantification, - formula: Box::new(formula), - }, - } - } } #[derive(Clone, Debug, Eq, PartialEq, Hash)]