Rename ScopedFormula to OpenFormula

src/input/specification.rs

@@ -85,8 +85,8 @@ where
 	Ok(())
 }
 
-fn closed_formula<'i, D>(input: &'i str, declarations: &D)
+fn open_formula<'i, D>(input: &'i str, declarations: &D)
-	-> Result<(crate::ScopedFormula, &'i str), crate::Error>
+	-> Result<(foliage::OpenFormula, &'i str), crate::Error>
 where
 	D: foliage::FindOrCreateFunctionDeclaration
 		+ foliage::FindOrCreatePredicateDeclaration
@@ -103,19 +103,18 @@ where
 	remaining_input_characters.next();
 	let remaining_input = remaining_input_characters.as_str();
 
-	let closed_formula = foliage::parse::formula(formula_input, declarations)
+	let open_formula = foliage::parse::formula(formula_input, declarations)
 		.map_err(|error| crate::Error::new_parse_formula(error))?;
 
-	formula_assign_variable_declaration_domains(&closed_formula.formula, declarations)?;
+	formula_assign_variable_declaration_domains(&open_formula.formula, declarations)?;
 
-	// TODO: get rid of ScopedFormula
+	let open_formula = foliage::OpenFormula
-	let scoped_formula = crate::ScopedFormula
 	{
-		free_variable_declarations: closed_formula.free_variable_declarations,
+		free_variable_declarations: open_formula.free_variable_declarations,
-		formula: closed_formula.formula,
+		formula: open_formula.formula,
 	};
 
-	Ok((scoped_formula, remaining_input))
+	Ok((open_formula, remaining_input))
 }
 
 // TODO: rename
@@ -126,15 +125,15 @@ where
 		+ foliage::FindOrCreatePredicateDeclaration
 		+ crate::traits::AssignVariableDeclarationDomain,
 {
-	let (closed_formula, input) = closed_formula(input, declarations)?;
+	let (open_formula, input) = open_formula(input, declarations)?;
 
-	if !closed_formula.free_variable_declarations.is_empty()
+	if !open_formula.free_variable_declarations.is_empty()
 	{
 		// TODO: improve
 		panic!("formula may not contain free variables");
 	}
 
-	Ok((closed_formula.formula, input))
+	Ok((open_formula.formula, input))
 }
 
 fn formula_statement_body<'i>(input: &'i str, problem: &crate::Problem)

src/translate/verify_properties.rs

@@ -8,7 +8,7 @@ use crate::traits::AssignVariableDeclarationDomain as _;
 struct PredicateDefinitions
 {
 	pub parameters: std::rc::Rc<foliage::VariableDeclarations>,
-	pub definitions: Vec<crate::ScopedFormula>,
+	pub definitions: Vec<foliage::OpenFormula>,
 }
 
 type Definitions =
@@ -99,13 +99,13 @@ impl<'p> Translator<'p>
 					let completed_definition =
 						foliage::Formula::if_and_only_if(vec![head_predicate, or]);
 
-					let scoped_formula = crate::ScopedFormula
+					let open_formula = foliage::OpenFormula
 					{
 						free_variable_declarations: predicate_definitions.parameters,
 						formula: completed_definition,
 					};
 
-					crate::universal_closure(scoped_formula)
+					crate::universal_closure(open_formula)
 				},
 				// This predicate has no definitions, so universally falsify it
 				None =>
@@ -130,13 +130,13 @@ impl<'p> Translator<'p>
 
 					let not = foliage::Formula::not(Box::new(head_predicate));
 
-					let scoped_formula = crate::ScopedFormula
+					let open_formula = foliage::OpenFormula
 					{
 						free_variable_declarations: parameters,
 						formula: not,
 					};
 
-					crate::universal_closure(scoped_formula)
+					crate::universal_closure(open_formula)
 				},
 			}
 		};
@@ -255,7 +255,7 @@ impl<'p> Translator<'p>
 					_ => foliage::Formula::and(definition_arguments),
 				};
 
-				let definition = crate::ScopedFormula
+				let definition = foliage::OpenFormula
 				{
 					free_variable_declarations: std::rc::Rc::new(free_variable_declarations),
 					formula: definition,
@@ -286,13 +286,13 @@ impl<'p> Translator<'p>
 					_ => foliage::Formula::not(Box::new(foliage::Formula::and(arguments))),
 				};
 
-				let scoped_formula = crate::ScopedFormula
+				let open_formula = foliage::OpenFormula
 				{
 					free_variable_declarations: std::rc::Rc::new(free_variable_declarations),
 					formula,
 				};
 
-				let integrity_constraint = crate::universal_closure(scoped_formula);
+				let integrity_constraint = crate::universal_closure(open_formula);
 
 				let statement = crate::problem::Statement::new(
 					crate::problem::StatementKind::Program, integrity_constraint)

src/utils.rs

@@ -37,9 +37,3 @@ impl std::fmt::Display for Domain
 		write!(formatter, "{:?}", self)
 	}
 }
-
-pub(crate) struct ScopedFormula
-{
-	pub free_variable_declarations: std::rc::Rc<foliage::VariableDeclarations>,
-	pub formula: foliage::Formula,
-}

src/utils/closures.rs

@@ -1,19 +1,19 @@
-pub(crate) fn existential_closure(scoped_formula: crate::ScopedFormula) -> foliage::Formula
+pub(crate) fn existential_closure(open_formula: foliage::OpenFormula) -> foliage::Formula
 {
-	match scoped_formula.free_variable_declarations.is_empty()
+	match open_formula.free_variable_declarations.is_empty()
 	{
-		true => scoped_formula.formula,
+		true => open_formula.formula,
-		false => foliage::Formula::exists(scoped_formula.free_variable_declarations,
+		false => foliage::Formula::exists(open_formula.free_variable_declarations,
-			Box::new(scoped_formula.formula)),
+			Box::new(open_formula.formula)),
 	}
 }
 
-pub(crate) fn universal_closure(scoped_formula: crate::ScopedFormula) -> foliage::Formula
+pub(crate) fn universal_closure(open_formula: foliage::OpenFormula) -> foliage::Formula
 {
-	match scoped_formula.free_variable_declarations.is_empty()
+	match open_formula.free_variable_declarations.is_empty()
 	{
-		true => scoped_formula.formula,
+		true => open_formula.formula,
-		false => foliage::Formula::for_all(scoped_formula.free_variable_declarations,
+		false => foliage::Formula::for_all(open_formula.free_variable_declarations,
-			Box::new(scoped_formula.formula)),
+			Box::new(open_formula.formula)),
 	}
 }