Skip to content

Commit

Permalink
Move UnboxedFormula in a separate module for convenience features
Browse files Browse the repository at this point in the history
  • Loading branch information
teiesti authored and ZachJHansen committed Nov 23, 2023
1 parent 6f0e915 commit 2573625
Show file tree
Hide file tree
Showing 6 changed files with 101 additions and 78 deletions.
1 change: 1 addition & 0 deletions src/convenience/mod.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
pub mod unbox;
51 changes: 51 additions & 0 deletions src/convenience/unbox/fol.rs
Original file line number Diff line number Diff line change
@@ -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),
},
}
}
}
44 changes: 44 additions & 0 deletions src/convenience/unbox/mod.rs
Original file line number Diff line number Diff line change
@@ -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,
},
}
}
}
1 change: 1 addition & 0 deletions src/main.rs
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
pub mod convenience;
pub mod formatting;
pub mod parsing;
pub mod simplifying;
Expand Down
5 changes: 4 additions & 1 deletion src/simplifying/fol/ht.rs
Original file line number Diff line number Diff line change
@@ -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 {
Expand Down
77 changes: 0 additions & 77 deletions src/syntax_tree/fol.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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)]
Expand Down

0 comments on commit 2573625

Please sign in to comment.