Replace variable declaration stack with recursive layer implementation

src/error.rs

@@ -1,69 +0,0 @@
-pub type Source = Box<dyn std::error::Error>;
-
-pub enum Kind
-{
-	Logic(&'static str),
-}
-
-pub struct Error
-{
-	pub kind: Kind,
-	pub source: Option<Source>,
-}
-
-impl Error
-{
-	pub(crate) fn new(kind: Kind) -> Self
-	{
-		Self
-		{
-			kind,
-			source: None,
-		}
-	}
-
-	pub(crate) fn with<S: Into<Source>>(mut self, source: S) -> Self
-	{
-		self.source = Some(source.into());
-		self
-	}
-
-	pub(crate) fn new_logic(description: &'static str) -> Self
-	{
-		Self::new(Kind::Logic(description))
-	}
-}
-
-impl std::fmt::Debug for Error
-{
-	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
-	{
-		match &self.kind
-		{
-			Kind::Logic(ref description) => write!(formatter,
-				"logic error, please report to bug tracker ({})", description),
-		}?;
-
-		Ok(())
-	}
-}
-
-impl std::fmt::Display for Error
-{
-	fn fmt(&self, formatter: &mut std::fmt::Formatter) -> std::fmt::Result
-	{
-		write!(formatter, "{:?}", self)
-	}
-}
-
-impl std::error::Error for Error
-{
-	fn source(&self) -> Option<&(dyn std::error::Error + 'static)>
-	{
-		match &self.source
-		{
-			Some(source) => Some(source.as_ref()),
-			None => None,
-		}
-	}
-}

src/lib.rs

@@ -1,10 +1,8 @@
 mod ast;
-mod error;
 pub mod format;
 #[cfg(feature = "parse")]
 pub mod parse;
 mod utils;
 
 pub use ast::*;
-pub use error::Error;
+pub use utils::*;
-pub use utils::VariableDeclarationStack;

src/parse.rs

@@ -14,7 +14,7 @@ pub struct Declarations
 {
 	function_declarations: std::cell::RefCell<crate::FunctionDeclarations>,
 	predicate_declarations: std::cell::RefCell<crate::PredicateDeclarations>,
-	variable_declaration_stack: std::cell::RefCell<crate::VariableDeclarationStack>,
+	free_variable_declarations: crate::FreeVariableDeclarations,
 }
 
 impl Declarations
@@ -25,8 +25,7 @@ impl Declarations
 		{
 			function_declarations: std::cell::RefCell::new(crate::FunctionDeclarations::new()),
 			predicate_declarations: std::cell::RefCell::new(crate::PredicateDeclarations::new()),
-			variable_declaration_stack:
+			free_variable_declarations: crate::FreeVariableDeclarations::new(),
-				std::cell::RefCell::new(crate::VariableDeclarationStack::new()),
 		}
 	}
 }

src/parse/formulas.rs

@@ -11,11 +11,12 @@ use nom::
 
 use super::{Declarations, boolean, word_boundary};
 
-pub fn predicate<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::Predicate>
+pub fn predicate<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
+	-> IResult<&'i str, crate::Predicate>
 {
 	map
 	(
-		|i| crate::parse::terms::function_or_predicate(i, d),
+		|i| crate::parse::terms::function_or_predicate(i, d, v),
 		|(name, arguments)|
 		{
 			let arguments = match arguments
@@ -50,7 +51,8 @@ pub fn predicate<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::Pr
 	)(i)
 }
 
-fn not<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
+fn not<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
+	-> IResult<&'i str, crate::Formula>
 {
 	map
 	(
@@ -61,13 +63,14 @@ fn not<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
 				tag("not"),
 				multispace0,
 			),
-			|i| formula_precedence_2(i, d),
+			|i| formula_precedence_2(i, d, v),
 		),
 		|x| crate::Formula::not(Box::new(x)),
 	)(i)
 }
 
-fn and<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formulas>
+fn and<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
+	-> IResult<&'i str, crate::Formulas>
 {
 	map_res
 	(
@@ -83,7 +86,7 @@ fn and<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formulas>
 				),
 				multispace0,
 			),
-			|i| formula_precedence_2(i, d),
+			|i| formula_precedence_2(i, d, v),
 		),
 		|arguments| -> Result<_, (_, _)>
 		{
@@ -99,7 +102,8 @@ fn and<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formulas>
 	)(i)
 }
 
-fn or<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formulas>
+fn or<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
+	-> IResult<&'i str, crate::Formulas>
 {
 	map_res
 	(
@@ -115,7 +119,7 @@ fn or<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formulas>
 				),
 				multispace0,
 			),
-			|i| formula_precedence_3(i, d),
+			|i| formula_precedence_3(i, d, v),
 		),
 		|arguments| -> Result<_, (_, _)>
 		{
@@ -131,7 +135,9 @@ fn or<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formulas>
 	)(i)
 }
 
-fn implies_left_to_right<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
+fn implies_left_to_right<'i, 'v>(i: &'i str, d: &Declarations,
+	v: &'v crate::VariableDeclarationStackLayer)
+	-> IResult<&'i str, crate::Formula>
 {
 	map
 	(
@@ -141,7 +147,7 @@ fn implies_left_to_right<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, c
 			(
 				terminated
 				(
-					|i| formula_precedence_4(i, d),
+					|i| formula_precedence_4(i, d, v),
 					delimited
 					(
 						multispace0,
@@ -150,7 +156,7 @@ fn implies_left_to_right<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, c
 					),
 				)
 			),
-			|i| formula_precedence_4(i, d),
+			|i| formula_precedence_4(i, d, v),
 		),
 		|(arguments, last_argument)| arguments.into_iter().rev().fold(last_argument,
 			|accumulator, argument|
@@ -159,13 +165,15 @@ fn implies_left_to_right<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, c
 	)(i)
 }
 
-fn implies_right_to_left<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
+fn implies_right_to_left<'i, 'v>(i: &'i str, d: &Declarations,
+	v: &'v crate::VariableDeclarationStackLayer)
+	-> IResult<&'i str, crate::Formula>
 {
 	map
 	(
 		pair
 		(
-			|i| formula_precedence_4(i, d),
+			|i| formula_precedence_4(i, d, v),
 			many1
 			(
 				preceded
@@ -176,7 +184,7 @@ fn implies_right_to_left<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, c
 						tag("<-"),
 						multispace0,
 					),
-					|i| formula_precedence_4(i, d),
+					|i| formula_precedence_4(i, d, v),
 				)
 			),
 		),
@@ -187,7 +195,8 @@ fn implies_right_to_left<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, c
 	)(i)
 }
 
-fn if_and_only_if<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formulas>
+fn if_and_only_if<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
+	-> IResult<&'i str, crate::Formulas>
 {
 	map_res
 	(
@@ -199,7 +208,7 @@ fn if_and_only_if<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::F
 				tag("<->"),
 				multispace0,
 			),
-			|i| formula_precedence_5(i, d),
+			|i| formula_precedence_5(i, d, v),
 		),
 		|arguments| -> Result<_, (_, _)>
 		{
@@ -215,8 +224,9 @@ fn if_and_only_if<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::F
 	)(i)
 }
 
-fn quantified_formula<'a, 'b>(i: &'a str, d: &Declarations, keyword: &'b str)
+fn quantified_formula<'i, 'b, 'v>(i: &'i str, d: &Declarations,
-	-> IResult<&'a str, crate::QuantifiedFormula>
+	v: &'v crate::VariableDeclarationStackLayer, keyword: &'b str)
+	-> IResult<&'i str, crate::QuantifiedFormula>
 {
 	preceded
 	(
@@ -259,10 +269,11 @@ fn quantified_formula<'a, 'b>(i: &'a str, d: &Declarations, keyword: &'b str)
 					return Err(nom::Err::Failure((i, nom::error::ErrorKind::Many1)));
 				}
 
-				let _guard = crate::VariableDeclarationStack::push(&d.variable_declaration_stack,
+				let v2 = crate::VariableDeclarationStackLayer::Bound(
-					std::rc::Rc::clone(&variable_declarations));
+					crate::BoundVariableDeclarations::new(v,
+						std::rc::Rc::clone(&variable_declarations)));
 
-				let (i, argument) = formula_precedence_0(i, d)?;
+				let (i, argument) = formula_precedence_0(i, d, &v2)?;
 
 				Ok((i, crate::QuantifiedFormula::new(variable_declarations, Box::new(argument))))
 			}
@@ -270,13 +281,14 @@ fn quantified_formula<'a, 'b>(i: &'a str, d: &Declarations, keyword: &'b str)
 	)(i)
 }
 
-fn compare<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Compare>
+fn compare<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
+	-> IResult<&'i str, crate::Compare>
 {
 	map
 	(
 		tuple
 		((
-			|i| crate::parse::term(i, d),
+			|i| crate::parse::term(i, d, v),
 			delimited
 			(
 				multispace0,
@@ -315,7 +327,7 @@ fn compare<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Compare>
 				)),
 				multispace0,
 			),
-			|i| crate::parse::term(i, d),
+			|i| crate::parse::term(i, d, v),
 		)),
 		|(left, operator, right)|
 		{
@@ -324,17 +336,21 @@ fn compare<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Compare>
 	)(i)
 }
 
-fn exists<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::QuantifiedFormula>
+fn exists<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
+	-> IResult<&'i str, crate::QuantifiedFormula>
 {
-	quantified_formula(i, d, "exists")
+	quantified_formula(i, d, v, "exists")
 }
 
-fn for_all<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::QuantifiedFormula>
+fn for_all<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
+	-> IResult<&'i str, crate::QuantifiedFormula>
 {
-	quantified_formula(i, d, "forall")
+	quantified_formula(i, d, v, "forall")
 }
 
-fn formula_parenthesized<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
+fn formula_parenthesized<'i, 'v>(i: &'i str, d: &Declarations,
+	v: &'v crate::VariableDeclarationStackLayer)
+	-> IResult<&'i str, crate::Formula>
 {
 	delimited
 	(
@@ -343,7 +359,7 @@ fn formula_parenthesized<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, c
 			tag("("),
 			multispace0,
 		),
-		|i| formula(i, d),
+		|i| formula(i, d, v),
 		preceded
 		(
 			multispace0,
@@ -352,7 +368,9 @@ fn formula_parenthesized<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, c
 	)(i)
 }
 
-fn formula_precedence_0<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
+fn formula_precedence_0<'i, 'v>(i: &'i str, d: &Declarations,
+	v: &'v crate::VariableDeclarationStackLayer)
+	-> IResult<&'i str, crate::Formula>
 {
 	alt
 	((
@@ -363,97 +381,110 @@ fn formula_precedence_0<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, cr
 		),
 		map
 		(
-			|i| predicate(i, d),
+			|i| predicate(i, d, v),
 			crate::Formula::Predicate,
 		),
 		map
 		(
-			|i| compare(i, d),
+			|i| compare(i, d, v),
 			crate::Formula::Compare,
 		),
-		|i| formula_parenthesized(i, d),
+		|i| formula_parenthesized(i, d, v),
 	))(i)
 }
 
-fn formula_precedence_1<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
+fn formula_precedence_1<'i, 'v>(i: &'i str, d: &Declarations,
+	v: &'v crate::VariableDeclarationStackLayer)
+	-> IResult<&'i str, crate::Formula>
 {
 	alt
 	((
 		map
 		(
-			|i| exists(i, d),
+			|i| exists(i, d, v),
 			crate::Formula::Exists,
 		),
 		map
 		(
-			|i| for_all(i, d),
+			|i| for_all(i, d, v),
 			crate::Formula::ForAll,
 		),
-		|i| formula_precedence_0(i, d),
+		|i| formula_precedence_0(i, d, v),
 	))(i)
 }
 
-fn formula_precedence_2<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
+fn formula_precedence_2<'i, 'v>(i: &'i str, d: &Declarations,
+	v: &'v crate::VariableDeclarationStackLayer)
+	-> IResult<&'i str, crate::Formula>
 {
 	alt
 	((
-		|i| not(i, d),
+		|i| not(i, d, v),
-		|i| formula_precedence_1(i, d),
+		|i| formula_precedence_1(i, d, v),
 	))(i)
 }
 
-fn formula_precedence_3<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
+fn formula_precedence_3<'i, 'v>(i: &'i str, d: &Declarations,
+	v: &'v crate::VariableDeclarationStackLayer)
+	-> IResult<&'i str, crate::Formula>
 {
 	alt
 	((
 		map
 		(
-			|i| and(i, d),
+			|i| and(i, d, v),
 			crate::Formula::And,
 		),
-		|i| formula_precedence_2(i, d),
+		|i| formula_precedence_2(i, d, v),
 	))(i)
 }
 
-fn formula_precedence_4<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
+fn formula_precedence_4<'i, 'v>(i: &'i str, d: &Declarations,
+	v: &'v crate::VariableDeclarationStackLayer)
+	-> IResult<&'i str, crate::Formula>
 {
 	alt
 	((
 		map
 		(
-			|i| or(i, d),
+			|i| or(i, d, v),
 			crate::Formula::Or,
 		),
-		|i| formula_precedence_3(i, d),
+		|i| formula_precedence_3(i, d, v),
 	))(i)
 }
 
-fn formula_precedence_5<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
+fn formula_precedence_5<'i, 'v>(i: &'i str, d: &Declarations,
+	v: &'v crate::VariableDeclarationStackLayer)
+	-> IResult<&'i str, crate::Formula>
 {
 	alt
 	((
-		|i| implies_left_to_right(i, d),
+		|i| implies_left_to_right(i, d, v),
-		|i| implies_right_to_left(i, d),
+		|i| implies_right_to_left(i, d, v),
-		|i| formula_precedence_4(i, d),
+		|i| formula_precedence_4(i, d, v),
 	))(i)
 }
 
-fn formula_precedence_6<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
+fn formula_precedence_6<'i, 'v>(i: &'i str, d: &Declarations,
+	v: &'v crate::VariableDeclarationStackLayer)
+	-> IResult<&'i str, crate::Formula>
 {
 	alt
 	((
 		map
 		(
-			|i| if_and_only_if(i, d),
+			|i| if_and_only_if(i, d, v),
 			crate::Formula::IfAndOnlyIf,
 		),
-		|i| formula_precedence_5(i, d),
+		|i| formula_precedence_5(i, d, v),
 	))(i)
 }
 
-pub fn formula<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Formula>
+pub fn formula<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
+	-> IResult<&'i str, crate::Formula>
 {
-	formula_precedence_6(i, d)
+	formula_precedence_6(i, d, v)
 }
 
 #[cfg(test)]
@@ -461,16 +492,18 @@ mod tests
 {
 	use crate::parse::formulas::*;
 	use crate::parse::formulas as original;
-	use crate::{Formula, Term};
+	use crate::{Formula, ImplicationDirection, Term, VariableDeclarationStackLayer};
 
 	fn formula(i: &str) -> Formula
 	{
-		original::formula(i, &Declarations::new()).unwrap().1
+		original::formula(i, &Declarations::new(), &VariableDeclarationStackLayer::free())
+			.unwrap().1
 	}
 
 	fn formula_remainder(i: &str) -> &str
 	{
-		original::formula(i, &Declarations::new()).unwrap().0
+		original::formula(i, &Declarations::new(), &VariableDeclarationStackLayer::free())
+			.unwrap().0
 	}
 
 	fn format_formula(i: &str) -> String
@@ -542,7 +575,8 @@ mod tests
 		assert_eq!(
 			as_predicate(formula_as_and("(p and q and r and s)").remove(3)).declaration.name, "s");
 
-		let formula = |i| original::formula(i, &Declarations::new());
+		let formula = |i| original::formula(i, &Declarations::new(),
+			&VariableDeclarationStackLayer::free());
 
 		// Malformed formulas shouldn’t be accepted
 		assert!(formula("and").is_err());
@@ -582,7 +616,8 @@ mod tests
 		assert_eq!(
 			as_predicate(formula_as_or("(p or q or r or s)").remove(3)).declaration.name, "s");
 
-		let formula = |i| original::formula(i, &Declarations::new());
+		let formula = |i| original::formula(i, &Declarations::new(),
+			&VariableDeclarationStackLayer::free());
 
 		// Malformed formulas shouldn’t be accepted
 		assert!(formula("or").is_err());
@@ -612,13 +647,11 @@ mod tests
 
 		assert_eq!(as_predicate(*formula_as_implies("a -> b").antecedent).declaration.name, "a");
 		assert_eq!(as_predicate(*formula_as_implies("a -> b").implication).declaration.name, "b");
-		assert_eq!(formula_as_implies("a -> b").direction,
+		assert_eq!(formula_as_implies("a -> b").direction, ImplicationDirection::LeftToRight);
-			crate::ImplicationDirection::LeftToRight);
 
 		assert_eq!(as_predicate(*formula_as_implies("a <- b").antecedent).declaration.name, "b");
 		assert_eq!(as_predicate(*formula_as_implies("a <- b").implication).declaration.name, "a");
-		assert_eq!(formula_as_implies("a <- b").direction,
+		assert_eq!(formula_as_implies("a <- b").direction, ImplicationDirection::RightToLeft);
-			crate::ImplicationDirection::RightToLeft);
 
 		assert_eq!(format_formula("(a -> b -> c)"), "a -> b -> c");
 		assert_eq!(format_formula("(a -> (b -> c))"), "a -> b -> c");
@@ -628,8 +661,10 @@ mod tests
 	#[test]
 	fn parse_predicate()
 	{
-		let predicate = |i| original::predicate(i, &Declarations::new()).unwrap().1;
+		let predicate = |i| original::predicate(i, &Declarations::new(),
-		let predicate_remainder = |i| original::predicate(i, &Declarations::new()).unwrap().0;
+			&VariableDeclarationStackLayer::free()).unwrap().1;
+		let predicate_remainder = |i| original::predicate(i, &Declarations::new(),
+			&VariableDeclarationStackLayer::free()).unwrap().0;
 
 		assert_eq!(predicate("s").declaration.name, "s");
 		assert_eq!(predicate("s").declaration.arity, 0);
@@ -655,20 +690,23 @@ mod tests
 	#[test]
 	fn parse_exists_primitive()
 	{
-		assert_eq!(exists("exists X (p(X, Y, X, Y)), rest", &Declarations::new())
+		let exists = |i| original::exists(i, &Declarations::new(),
+			&VariableDeclarationStackLayer::free());
+
+		assert_eq!(exists("exists X (p(X, Y, X, Y)), rest")
 			.map(|(i, x)| (i, x.parameters.len())),
 			Ok((", rest", 1)));
-		assert_eq!(exists("exists X p(X, Y, X, Y), rest", &Declarations::new())
+		assert_eq!(exists("exists X p(X, Y, X, Y), rest")
 			.map(|(i, x)| (i, x.parameters.len())),
 			Ok((", rest", 1)));
-		assert!(exists("exists (p(X, Y, X, Y)), rest", &Declarations::new()).is_err());
+		assert!(exists("exists (p(X, Y, X, Y)), rest").is_err());
-		assert!(exists("exists X, rest", &Declarations::new()).is_err());
+		assert!(exists("exists X, rest").is_err());
-		assert!(exists("exists X (), rest", &Declarations::new()).is_err());
+		assert!(exists("exists X (), rest").is_err());
-		assert!(exists("exists X (, true), rest", &Declarations::new()).is_err());
+		assert!(exists("exists X (, true), rest").is_err());
-		assert!(exists("exists X (true, ), rest", &Declarations::new()).is_err());
+		assert!(exists("exists X (true, ), rest").is_err());
-		assert!(exists("exists X (true false), rest", &Declarations::new()).is_err());
+		assert!(exists("exists X (true false), rest").is_err());
-		assert!(exists("exists X (true), rest", &Declarations::new()).is_ok());
+		assert!(exists("exists X (true), rest").is_ok());
-		assert!(exists("exists X p(X), rest", &Declarations::new()).is_ok());
+		assert!(exists("exists X p(X), rest").is_ok());
 	}
 
 	#[test]

src/parse/terms.rs

@@ -12,7 +12,8 @@ use nom::
 use super::{Declarations, boolean, function_or_predicate_name, integer, special_integer, string,
 	variable_name};
 
-fn negative<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::Term>
+fn negative<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
+	-> IResult<&'i str, crate::Term>
 {
 	map
 	(
@@ -23,7 +24,7 @@ fn negative<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::Term>
 				tag("-"),
 				multispace0,
 			),
-			|i| term_precedence_1(i, d),
+			|i| term_precedence_1(i, d, v),
 		),
 		|x| match x
 		{
@@ -36,7 +37,8 @@ fn negative<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::Term>
 	)(i)
 }
 
-fn absolute_value<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::Term>
+fn absolute_value<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
+	-> IResult<&'i str, crate::Term>
 {
 	map
 	(
@@ -47,7 +49,7 @@ fn absolute_value<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::T
 				tag("|"),
 				multispace0,
 			),
-			|i| term(i, d),
+			|i| term(i, d, v),
 			preceded
 			(
 				multispace0,
@@ -58,7 +60,8 @@ fn absolute_value<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::T
 	)(i)
 }
 
-pub(crate) fn function_or_predicate<'i>(i: &'i str, d: &Declarations)
+pub(crate) fn function_or_predicate<'i, 'v>(i: &'i str, d: &Declarations,
+	v: &'v crate::VariableDeclarationStackLayer)
 	-> IResult<&'i str, (&'i str, Option<crate::Terms>)>
 {
 	pair
@@ -82,7 +85,7 @@ pub(crate) fn function_or_predicate<'i>(i: &'i str, d: &Declarations)
 						tag(","),
 						multispace0,
 					),
-					|i| term(i, d),
+					|i| term(i, d, v),
 				),
 				preceded
 				(
@@ -94,11 +97,12 @@ pub(crate) fn function_or_predicate<'i>(i: &'i str, d: &Declarations)
 	)(i)
 }
 
-fn function<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::Function>
+fn function<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
+	-> IResult<&'i str, crate::Function>
 {
 	map
 	(
-		|i| function_or_predicate(i, d),
+		|i| function_or_predicate(i, d, v),
 		|(name, arguments)|
 		{
 			let arguments = match arguments
@@ -142,23 +146,24 @@ pub(crate) fn variable_declaration(i: &str) -> IResult<&str, crate::VariableDecl
 	)(i)
 }
 
-fn variable<'i>(i: &'i str, d: &Declarations) -> IResult<&'i str, crate::Variable>
+fn variable<'i, 'v>(i: &'i str, v: &'v crate::VariableDeclarationStackLayer)
+	-> IResult<&'i str, crate::Variable>
 {
 	map
 	(
 		variable_name,
 		|name|
 		{
-			let mut variable_declaration_stack = d.variable_declaration_stack.borrow_mut();
+			let declaration = v.find_or_create(name);
-
-			let declaration = variable_declaration_stack.find_or_create(name);
 
 			crate::Variable::new(declaration)
 		},
 	)(i)
 }
 
-fn term_parenthesized<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term>
+fn term_parenthesized<'i, 'v>(i: &'i str, d: &Declarations,
+	v: &'v crate::VariableDeclarationStackLayer)
+	-> IResult<&'i str, crate::Term>
 {
 	delimited
 	(
@@ -167,7 +172,7 @@ fn term_parenthesized<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crat
 			tag("("),
 			multispace0,
 		),
-		|i| term(i, d),
+		|i| term(i, d, v),
 		preceded
 		(
 			multispace0,
@@ -176,7 +181,9 @@ fn term_parenthesized<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crat
 	)(i)
 }
 
-fn term_precedence_0<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term>
+fn term_precedence_0<'i, 'v>(i: &'i str, d: &Declarations,
+	v: &'v crate::VariableDeclarationStackLayer)
+	-> IResult<&'i str, crate::Term>
 {
 	alt
 	((
@@ -197,7 +204,7 @@ fn term_precedence_0<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate
 		),
 		map
 		(
-			|i| function(i, d),
+			|i| function(i, d, v),
 			crate::Term::Function,
 		),
 		map
@@ -207,24 +214,28 @@ fn term_precedence_0<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate
 		),
 		map
 		(
-			|i| variable(i, d),
+			|i| variable(i, v),
 			crate::Term::Variable,
 		),
-		|i| absolute_value(i, d),
+		|i| absolute_value(i, d, v),
-		|i| term_parenthesized(i, d),
+		|i| term_parenthesized(i, d, v),
 	))(i)
 }
 
-fn term_precedence_1<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term>
+fn term_precedence_1<'i, 'v>(i: &'i str, d: &Declarations,
+	v: &'v crate::VariableDeclarationStackLayer)
+	-> IResult<&'i str, crate::Term>
 {
 	alt
 	((
-		|i| negative(i, d),
+		|i| negative(i, d, v),
-		|i| term_precedence_0(i, d),
+		|i| term_precedence_0(i, d, v),
 	))(i)
 }
 
-fn term_precedence_2<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term>
+fn term_precedence_2<'i, 'v>(i: &'i str, d: &Declarations,
+	v: &'v crate::VariableDeclarationStackLayer)
+	-> IResult<&'i str, crate::Term>
 {
 	alt
 	((
@@ -236,7 +247,7 @@ fn term_precedence_2<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate
 				(
 					terminated
 					(
-						|i| term_precedence_1(i, d),
+						|i| term_precedence_1(i, d, v),
 						delimited
 						(
 							multispace0,
@@ -245,17 +256,19 @@ fn term_precedence_2<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate
 						),
 					)
 				),
-				|i| term_precedence_1(i, d),
+				|i| term_precedence_1(i, d, v),
 			),
 			|(arguments, last_argument)| arguments.into_iter().rev().fold(last_argument,
 				|accumulator, argument|
 					crate::Term::exponentiate(Box::new(argument), Box::new(accumulator))),
 		),
-		|i| term_precedence_1(i, d),
+		|i| term_precedence_1(i, d, v),
 	))(i)
 }
 
-fn term_precedence_3<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term>
+fn term_precedence_3<'i, 'v>(i: &'i str, d: &Declarations,
+	v: &'v crate::VariableDeclarationStackLayer)
+	-> IResult<&'i str, crate::Term>
 {
 	alt
 	((
@@ -263,7 +276,7 @@ fn term_precedence_3<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate
 		(
 			pair
 			(
-				|i| term_precedence_2(i, d),
+				|i| term_precedence_2(i, d, v),
 				many1
 				(
 					pair
@@ -279,7 +292,7 @@ fn term_precedence_3<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate
 							)),
 							multispace0,
 						),
-						|i| term_precedence_2(i, d),
+						|i| term_precedence_2(i, d, v),
 					)
 				),
 			),
@@ -294,11 +307,12 @@ fn term_precedence_3<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate
 					_ => panic!("test"),
 				})
 		),
-		|i| term_precedence_2(i, d),
+		|i| term_precedence_2(i, d, v),
 	))(i)
 }
 
-fn term_precedence_4<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term>
+fn term_precedence_4<'i, 'v>(i: &'i str, d: &Declarations,
+	v: &'v crate::VariableDeclarationStackLayer) -> IResult<&'i str, crate::Term>
 {
 	alt
 	((
@@ -306,7 +320,7 @@ fn term_precedence_4<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate
 		(
 			pair
 			(
-				|i| term_precedence_3(i, d),
+				|i| term_precedence_3(i, d, v),
 				many1
 				(
 					pair
@@ -321,7 +335,7 @@ fn term_precedence_4<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate
 							)),
 							multispace0,
 						),
-						|i| term_precedence_3(i, d),
+						|i| term_precedence_3(i, d, v),
 					)
 				),
 			),
@@ -335,13 +349,14 @@ fn term_precedence_4<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate
 					_ => panic!("test"),
 				})
 		),
-		|i| term_precedence_3(i, d),
+		|i| term_precedence_3(i, d, v),
 	))(i)
 }
 
-pub fn term<'a>(i: &'a str, d: &Declarations) -> IResult<&'a str, crate::Term>
+pub fn term<'i, 'v>(i: &'i str, d: &Declarations, v: &'v crate::VariableDeclarationStackLayer)
+	-> IResult<&'i str, crate::Term>
 {
-	term_precedence_4(i, d)
+	term_precedence_4(i, d, v)
 }
 
 #[cfg(test)]
@@ -349,11 +364,11 @@ mod tests
 {
 	use crate::parse::terms::*;
 	use crate::parse::terms as original;
-	use crate::{Term, VariableDeclaration, VariableDeclarationStack};
+	use crate::{Term, VariableDeclaration, VariableDeclarationStackLayer};
 
 	fn term(i: &str) -> Term
 	{
-		original::term(i, &Declarations::new()).unwrap().1
+		original::term(i, &Declarations::new(), &VariableDeclarationStackLayer::free()).unwrap().1
 	}
 
 	fn format_term(i: &str) -> String
@@ -650,7 +665,8 @@ mod tests
 	#[test]
 	fn parse_bounds()
 	{
-		let term = |i| original::term(i, &Declarations::new()).unwrap().0;
+		let term = |i| original::term(i, &Declarations::new(),
+			&VariableDeclarationStackLayer::free()).unwrap().0;
 
 		assert_eq!(term("1 ** 2 ** 3, rest"), ", rest");
 		assert_eq!(term("1 * 2 * 3, rest"), ", rest");
@@ -700,8 +716,10 @@ mod tests
 	#[test]
 	fn parse_function_primitive()
 	{
-		let function = |i| original::function(i, &Declarations::new()).unwrap().1;
+		let function = |i| original::function(i, &Declarations::new(),
-		let function_remainder = |i| original::function(i, &Declarations::new()).unwrap().0;
+			&VariableDeclarationStackLayer::free()).unwrap().1;
+		let function_remainder = |i| original::function(i, &Declarations::new(),
+			&VariableDeclarationStackLayer::free()).unwrap().0;
 
 		assert_eq!(function("s").declaration.name, "s");
 		assert_eq!(function("s").declaration.arity, 0);
@@ -752,8 +770,9 @@ mod tests
 	#[test]
 	fn parse_variable_primitive()
 	{
-		let variable = |i| original::variable(i, &Declarations::new()).unwrap().1;
+		let variable = |i| original::variable(i, &VariableDeclarationStackLayer::free()).unwrap().1;
-		let variable_remainder = |i| original::variable(i, &Declarations::new()).unwrap().0;
+		let variable_remainder = |i| original::variable(i,
+			&VariableDeclarationStackLayer::free()).unwrap().0;
 
 		assert_eq!(variable("X Rest").declaration.name, "X");
 		assert_eq!(variable_remainder("X Rest"), " Rest");
@@ -762,7 +781,7 @@ mod tests
 		assert_eq!(variable("Variable_123 Rest").declaration.name, "Variable_123");
 		assert_eq!(variable_remainder("Variable_123 Rest"), " Rest");
 
-		let variable = |i| original::variable(i, &Declarations::new());
+		let variable = |i| original::variable(i, &VariableDeclarationStackLayer::free());
 
 		assert!(variable("0 Rest").is_err());
 		assert!(variable("123_Asd Rest").is_err());
@@ -781,15 +800,10 @@ mod tests
 		let layer_3 = new_variable_declarations(&["E", "F", "Y"]);
 		let layer_4 = new_variable_declarations(&["G", "H", "X"]);
 
-		let variable_declaration_stack = VariableDeclarationStack::new();
+		let v_0 = VariableDeclarationStackLayer::free();
-
+		let variable = |i| original::variable(i, &v_0).unwrap().1;
-		let mut declarations = Declarations::new();
-		declarations.variable_declaration_stack =
-			std::cell::RefCell::new(variable_declaration_stack);
-
-		let variable = |i| original::variable(i, &declarations).unwrap().1;
 		let number_of_free_variable_declarations =
-			|| declarations.variable_declaration_stack.borrow().free_variable_declarations.len();
+			|| v_0.free_variable_declarations_do(|x| x.len());
 
 		let x1 = variable("X");
 		assert_eq!(number_of_free_variable_declarations(), 1);
@@ -801,8 +815,8 @@ mod tests
 		assert_ne!(x1.declaration, y1.declaration);
 		assert_ne!(x2.declaration, y1.declaration);
 
-		let _guard
+		let v_1 = VariableDeclarationStackLayer::bound(&v_0, layer_1);
-			= VariableDeclarationStack::push(&declarations.variable_declaration_stack, layer_1);
+		let variable = |i| original::variable(i, &v_1).unwrap().1;
 
 		let x3 = variable("X");
 		assert_eq!(number_of_free_variable_declarations(), 2);
@@ -817,8 +831,8 @@ mod tests
 		assert_eq!(number_of_free_variable_declarations(), 2);
 		assert_eq!(y1.declaration, y2.declaration);
 
-		let _guard
+		let v_2 = VariableDeclarationStackLayer::bound(&v_1, layer_2);
-			= VariableDeclarationStack::push(&declarations.variable_declaration_stack, layer_2);
+		let variable = |i| original::variable(i, &v_2).unwrap().1;
 
 		let x5 = variable("X");
 		assert_eq!(number_of_free_variable_declarations(), 2);
@@ -831,8 +845,8 @@ mod tests
 		assert_eq!(number_of_free_variable_declarations(), 2);
 		assert_eq!(a1.declaration, a2.declaration);
 
-		let _guard
+		let v_3 = VariableDeclarationStackLayer::bound(&v_2, layer_3);
-			= VariableDeclarationStack::push(&declarations.variable_declaration_stack, layer_3);
+		let variable = |i| original::variable(i, &v_3).unwrap().1;
 
 		let x7 = variable("X");
 		assert_eq!(number_of_free_variable_declarations(), 2);
@@ -841,8 +855,8 @@ mod tests
 		assert_eq!(number_of_free_variable_declarations(), 2);
 		assert_ne!(y2.declaration, y3.declaration);
 
-		let _guard
+		let v_4 = VariableDeclarationStackLayer::bound(&v_3, layer_4);
-			= VariableDeclarationStack::push(&declarations.variable_declaration_stack, layer_4);
+		let variable = |i| original::variable(i, &v_4).unwrap().1;
 
 		let x8 = variable("X");
 		assert_eq!(number_of_free_variable_declarations(), 2);

src/utils.rs

@@ -15,98 +15,133 @@ pub trait FindVariableDeclaration
 	fn find_variable_declaration(&self, name: &str) -> std::rc::Rc<crate::VariableDeclaration>;
 }
 
-pub struct VariableDeclarationStack
+pub struct FreeVariableDeclarations
 {
-	pub free_variable_declarations: crate::VariableDeclarations,
+	variable_declarations: std::cell::RefCell<crate::VariableDeclarations>,
-	bound_variable_declaration_stack: Vec<std::rc::Rc<crate::VariableDeclarations>>,
 }
 
-impl VariableDeclarationStack
+impl FreeVariableDeclarations
 {
 	pub fn new() -> Self
 	{
 		Self
 		{
-			free_variable_declarations: crate::VariableDeclarations::new(),
+			variable_declarations: std::cell::RefCell::new(vec![]),
-			bound_variable_declaration_stack: vec![],
 		}
 	}
+}
+
+pub struct BoundVariableDeclarations<'p>
+{
+	parent: &'p VariableDeclarationStackLayer<'p>,
+	variable_declarations: std::rc::Rc<crate::VariableDeclarations>,
+}
+
+impl<'p> BoundVariableDeclarations<'p>
+{
+	pub fn new(parent: &'p VariableDeclarationStackLayer<'p>,
+		variable_declarations: std::rc::Rc<crate::VariableDeclarations>) -> Self
+	{
+		Self
+		{
+			parent,
+			variable_declarations,
+		}
+	}
+}
+
+pub enum VariableDeclarationStackLayer<'p>
+{
+	Free(FreeVariableDeclarations),
+	Bound(BoundVariableDeclarations<'p>),
+}
+
+impl<'p> VariableDeclarationStackLayer<'p>
+{
+	pub fn free() -> Self
+	{
+		Self::Free(FreeVariableDeclarations::new())
+	}
+
+	pub fn bound(parent: &'p VariableDeclarationStackLayer<'p>,
+		variable_declarations: std::rc::Rc<crate::VariableDeclarations>) -> Self
+	{
+		Self::Bound(BoundVariableDeclarations::new(parent, variable_declarations))
+	}
 
 	pub fn find(&self, variable_name: &str) -> Option<std::rc::Rc<crate::VariableDeclaration>>
 	{
-		for variable_declarations in self.bound_variable_declaration_stack.iter().rev()
+		match self
 		{
-			if let Some(variable_declaration) = variable_declarations.iter()
+			VariableDeclarationStackLayer::Free(free) =>
-				.find(|x| x.name == variable_name)
 			{
-				return Some(std::rc::Rc::clone(&variable_declaration));
+				if let Some(variable_declaration) = free.variable_declarations.borrow().iter()
-			}
+					.find(|x| x.name == variable_name)
-		}
+				{
+					return Some(std::rc::Rc::clone(&variable_declaration));
+				}
 
-		if let Some(variable_declaration) = self.free_variable_declarations.iter()
+				None
-			.find(|x| x.name == variable_name)
+			},
-		{
+			VariableDeclarationStackLayer::Bound(bound) =>
-			return Some(std::rc::Rc::clone(&variable_declaration));
+			{
-		}
+				if let Some(variable_declaration) = bound.variable_declarations.iter()
+					.find(|x| x.name == variable_name)
+				{
+					return Some(std::rc::Rc::clone(&variable_declaration));
+				}
 
-		None
+				bound.parent.find(variable_name)
-	}
+			},
-
-	pub fn find_or_create(&mut self, variable_name: &str) -> std::rc::Rc<crate::VariableDeclaration>
-	{
-		if let Some(variable_declaration) = self.find(variable_name)
-		{
-			return variable_declaration;
-		}
-
-		let variable_declaration = crate::VariableDeclaration
-		{
-			name: variable_name.to_owned(),
-		};
-		let variable_declaration = std::rc::Rc::new(variable_declaration);
-
-		self.free_variable_declarations.push(std::rc::Rc::clone(&variable_declaration));
-
-		variable_declaration
-	}
-
-	pub fn is_empty(&self) -> bool
-	{
-		self.free_variable_declarations.is_empty()
-			&& self.bound_variable_declaration_stack.is_empty()
-	}
-
-	pub fn push<'v>(variable_declaration_stack: &'v std::cell::RefCell<VariableDeclarationStack>,
-		bound_variable_declarations: std::rc::Rc<crate::VariableDeclarations>)
-		-> VariableDeclarationStackGuard
-	{
-		variable_declaration_stack.borrow_mut()
-			.bound_variable_declaration_stack.push(bound_variable_declarations);
-
-		VariableDeclarationStackGuard
-		{
-			variable_declaration_stack: variable_declaration_stack,
 		}
 	}
 
-	pub(self) fn pop(&mut self)
+	pub fn find_or_create(&self, variable_name: &str) -> std::rc::Rc<crate::VariableDeclaration>
 	{
-		if let None = self.bound_variable_declaration_stack.pop()
+		match self
 		{
-			unreachable!()
+			VariableDeclarationStackLayer::Free(free) =>
+			{
+				if let Some(variable_declaration) = free.variable_declarations.borrow().iter()
+					.find(|x| x.name == variable_name)
+				{
+					return std::rc::Rc::clone(&variable_declaration);
+				}
+
+				let variable_declaration = crate::VariableDeclaration
+				{
+					name: variable_name.to_owned(),
+				};
+				let variable_declaration = std::rc::Rc::new(variable_declaration);
+
+				free.variable_declarations.borrow_mut()
+					.push(std::rc::Rc::clone(&variable_declaration));
+
+				variable_declaration
+			},
+			VariableDeclarationStackLayer::Bound(bound) =>
+			{
+				if let Some(variable_declaration) = bound.variable_declarations.iter()
+					.find(|x| x.name == variable_name)
+				{
+					return std::rc::Rc::clone(&variable_declaration);
+				}
+
+				bound.parent.find_or_create(variable_name)
+			},
+		}
+	}
+
+	#[cfg(test)]
+	pub fn free_variable_declarations_do<F, G>(&self, f: F) -> G
+	where
+		F: Fn(&crate::VariableDeclarations) -> G
+	{
+		match self
+		{
+			VariableDeclarationStackLayer::Free(free) => f(&free.variable_declarations.borrow()),
+			VariableDeclarationStackLayer::Bound(bound)
+				=> bound.parent.free_variable_declarations_do(f),
 		}
 	}
 }
-
-pub struct VariableDeclarationStackGuard<'v>
-{
-	variable_declaration_stack: &'v std::cell::RefCell<VariableDeclarationStack>,
-}
-
-impl<'v> Drop for VariableDeclarationStackGuard<'v>
-{
-	fn drop(&mut self)
-	{
-		self.variable_declaration_stack.borrow_mut().pop();
-	}
-}