anthem-rs/src/input/specification.rs

490 lines
13 KiB
Rust
Raw Normal View History

2020-05-05 19:40:57 +02:00
// TODO: refactor
fn term_assign_variable_declaration_domains<D>(term: &foliage::Term, declarations: &D)
-> Result<(), crate::Error>
where
D: crate::traits::AssignVariableDeclarationDomain,
{
match term
{
foliage::Term::BinaryOperation(binary_operation) =>
{
term_assign_variable_declaration_domains(&binary_operation.left, declarations)?;
term_assign_variable_declaration_domains(&binary_operation.right, declarations)?;
},
foliage::Term::Function(function) =>
for argument in &function.arguments
{
term_assign_variable_declaration_domains(&argument, declarations)?;
},
foliage::Term::UnaryOperation(unary_operation) =>
term_assign_variable_declaration_domains(&unary_operation.argument, declarations)?,
foliage::Term::Variable(variable) =>
{
let domain = match variable.declaration.name.chars().next()
{
Some('X')
| Some('Y')
| Some('Z') => crate::Domain::Program,
Some('I')
| Some('J')
| Some('K')
| Some('L')
| Some('M')
| Some('N') => crate::Domain::Integer,
2020-05-11 02:45:58 +02:00
Some(_) => return Err(
2020-05-05 19:40:57 +02:00
crate::Error::new_variable_name_not_allowed(variable.declaration.name.clone())),
None => unreachable!(),
};
declarations.assign_variable_declaration_domain(&variable.declaration, domain);
},
_ => (),
}
Ok(())
}
fn formula_assign_variable_declaration_domains<D>(formula: &foliage::Formula, declarations: &D)
-> Result<(), crate::Error>
where
D: crate::traits::AssignVariableDeclarationDomain,
{
match formula
{
foliage::Formula::And(arguments)
| foliage::Formula::Or(arguments)
| foliage::Formula::IfAndOnlyIf(arguments) =>
for argument in arguments
{
formula_assign_variable_declaration_domains(&argument, declarations)?;
},
foliage::Formula::Compare(compare) =>
{
term_assign_variable_declaration_domains(&compare.left, declarations)?;
term_assign_variable_declaration_domains(&compare.right, declarations)?;
},
foliage::Formula::Exists(quantified_formula)
| foliage::Formula::ForAll(quantified_formula) =>
formula_assign_variable_declaration_domains(&quantified_formula.argument,
declarations)?,
foliage::Formula::Implies(implies) =>
{
formula_assign_variable_declaration_domains(&implies.antecedent, declarations)?;
formula_assign_variable_declaration_domains(&implies.implication, declarations)?;
}
foliage::Formula::Not(argument) =>
formula_assign_variable_declaration_domains(&argument, declarations)?,
foliage::Formula::Predicate(predicate) =>
for argument in &predicate.arguments
{
term_assign_variable_declaration_domains(&argument, declarations)?;
},
_ => (),
}
Ok(())
}
2020-05-11 03:58:30 +02:00
fn open_formula<'i, D>(input: &'i str, declarations: &D)
-> Result<(foliage::OpenFormula, &'i str), crate::Error>
2020-05-05 19:40:57 +02:00
where
D: foliage::FindOrCreateFunctionDeclaration
+ foliage::FindOrCreatePredicateDeclaration
+ crate::traits::AssignVariableDeclarationDomain,
{
let terminator_position = match input.find('.')
{
None => return Err(crate::Error::new_missing_statement_terminator()),
Some(terminator_position) => terminator_position,
};
let (formula_input, remaining_input) = input.split_at(terminator_position);
let mut remaining_input_characters = remaining_input.chars();
remaining_input_characters.next();
let remaining_input = remaining_input_characters.as_str();
2020-05-11 03:58:30 +02:00
let open_formula = foliage::parse::formula(formula_input, declarations)
2020-05-05 19:40:57 +02:00
.map_err(|error| crate::Error::new_parse_formula(error))?;
2020-05-11 03:58:30 +02:00
formula_assign_variable_declaration_domains(&open_formula.formula, declarations)?;
2020-05-05 19:40:57 +02:00
2020-05-11 03:58:30 +02:00
let open_formula = foliage::OpenFormula
2020-05-05 19:40:57 +02:00
{
2020-05-11 03:58:30 +02:00
free_variable_declarations: open_formula.free_variable_declarations,
formula: open_formula.formula,
2020-05-05 19:40:57 +02:00
};
2020-05-11 03:58:30 +02:00
Ok((open_formula, remaining_input))
2020-05-05 19:40:57 +02:00
}
2020-05-12 05:20:48 +02:00
fn formula<'i, D>(mut input: &'i str, declarations: &D)
2020-05-05 19:40:57 +02:00
-> Result<(foliage::Formula, &'i str), crate::Error>
where
D: foliage::FindOrCreateFunctionDeclaration
+ foliage::FindOrCreatePredicateDeclaration
+ crate::traits::AssignVariableDeclarationDomain,
{
2020-05-12 05:20:48 +02:00
let (open_formula, remaining_input) = open_formula(input, declarations)?;
input = remaining_input;
2020-05-05 19:40:57 +02:00
2020-05-11 03:58:30 +02:00
if !open_formula.free_variable_declarations.is_empty()
2020-05-05 19:40:57 +02:00
{
2020-05-12 05:20:48 +02:00
return Err(crate::Error::new_formula_not_closed(open_formula.free_variable_declarations));
2020-05-05 19:40:57 +02:00
}
2020-05-11 03:58:30 +02:00
Ok((open_formula.formula, input))
2020-05-05 19:40:57 +02:00
}
2020-05-12 05:20:48 +02:00
fn formula_statement_body<'i>(mut input: &'i str, problem: &crate::Problem)
2020-05-05 19:40:57 +02:00
-> Result<(foliage::Formula, &'i str), crate::Error>
{
2020-05-12 06:08:50 +02:00
input = foliage::parse::tokens::trim_start(input);
2020-05-05 19:40:57 +02:00
let mut input_characters = input.chars();
2020-05-12 05:20:48 +02:00
input = match input_characters.next()
2020-05-05 19:40:57 +02:00
{
Some(':') => input_characters.as_str(),
_ => return Err(crate::Error::new_expected_colon()),
};
2020-05-11 04:00:06 +02:00
formula(input, problem)
2020-05-05 19:40:57 +02:00
}
2020-05-12 05:05:49 +02:00
fn domain_specifier<'i>(mut input: &'i str)
2020-05-12 04:51:31 +02:00
-> Result<(Option<crate::Domain>, &'i str), crate::Error>
{
let original_input = input;
2020-05-12 06:08:50 +02:00
input = foliage::parse::tokens::trim_start(input);
2020-05-12 04:51:31 +02:00
if input.starts_with("->")
{
let mut input_characters = input.chars();
input_characters.next();
input_characters.next();
2020-05-12 06:08:50 +02:00
input = foliage::parse::tokens::trim_start(input_characters.as_str());
2020-05-12 04:51:31 +02:00
let (identifier, remaining_input) =
foliage::parse::tokens::identifier(input)
.ok_or_else(|| crate::Error::new_expected_identifier())?;
2020-05-12 05:05:49 +02:00
input = remaining_input;
2020-05-12 04:51:31 +02:00
match identifier
{
"integer" => Ok((Some(crate::Domain::Integer), input)),
"program" => Ok((Some(crate::Domain::Program), input)),
_ => return Err(crate::Error::new_unknown_domain_identifier(identifier.to_string())),
}
}
else
{
Ok((None, original_input))
}
}
2020-05-12 05:05:49 +02:00
fn predicate_arity_specifier<'i>(mut input: &'i str)
-> Result<(Option<usize>, &'i str), crate::Error>
{
let original_input = input;
2020-05-12 06:08:50 +02:00
input = foliage::parse::tokens::trim_start(input);
2020-05-12 05:05:49 +02:00
let mut input_characters = input.chars();
if input_characters.next() == Some('/')
{
2020-05-12 06:08:50 +02:00
input = foliage::parse::tokens::trim_start(input_characters.as_str());
2020-05-12 05:05:49 +02:00
let (arity, remaining_input) = foliage::parse::tokens::number(input)
.map_err(|error| crate::Error::new_parse_predicate_declaration().with(error))?
.ok_or_else(|| crate::Error::new_parse_predicate_declaration())?;
input = remaining_input;
Ok((Some(arity), input))
}
else
{
Ok((None, original_input))
}
}
fn expect_statement_terminator<'i>(mut input: &'i str) -> Result<&'i str, crate::Error>
{
2020-05-12 06:08:50 +02:00
input = foliage::parse::tokens::trim_start(input);
let mut input_characters = input.chars();
if input_characters.next() != Some('.')
{
return Err(crate::Error::new_missing_statement_terminator())
}
input = input_characters.as_str();
Ok(input)
}
2020-05-05 19:40:57 +02:00
fn input_statement_body<'i>(mut input: &'i str, problem: &crate::Problem)
-> Result<&'i str, crate::Error>
{
2020-05-12 06:08:50 +02:00
input = foliage::parse::tokens::trim_start(input);
2020-05-05 19:40:57 +02:00
let mut input_characters = input.chars();
let remaining_input = match input_characters.next()
{
Some(':') => input_characters.as_str(),
_ => return Err(crate::Error::new_expected_colon()),
};
input = remaining_input;
loop
{
2020-05-12 06:08:50 +02:00
input = foliage::parse::tokens::trim_start(input);
2020-05-05 19:40:57 +02:00
let (constant_or_predicate_name, remaining_input) =
foliage::parse::tokens::identifier(input)
.ok_or_else(|| crate::Error::new_expected_identifier())?;
2020-05-12 06:08:50 +02:00
input = foliage::parse::tokens::trim_start(remaining_input);
2020-05-05 19:40:57 +02:00
2020-05-12 05:05:49 +02:00
// Parse input predicate specifiers
if let (Some(arity), remaining_input) = predicate_arity_specifier(input)?
2020-05-05 19:40:57 +02:00
{
2020-05-12 05:05:49 +02:00
input = remaining_input;
2020-05-05 19:40:57 +02:00
2020-05-12 05:05:49 +02:00
let mut input_predicate_declarations =
problem.input_predicate_declarations.borrow_mut();
2020-05-05 19:40:57 +02:00
2020-05-12 05:05:49 +02:00
use foliage::FindOrCreatePredicateDeclaration as _;
2020-05-05 19:40:57 +02:00
2020-05-12 05:05:49 +02:00
let predicate_declaration =
problem.find_or_create_predicate_declaration(constant_or_predicate_name, arity);
2020-05-05 19:40:57 +02:00
2020-05-12 05:05:49 +02:00
input_predicate_declarations.insert(predicate_declaration);
}
// Parse input constant specifiers
else
{
2020-05-12 06:10:52 +02:00
// TODO: detect conflicting domain specifiers (for example: n -> program, n -> integer)
2020-05-12 05:05:49 +02:00
let (domain, remaining_input) = match domain_specifier(input)?
2020-05-05 19:40:57 +02:00
{
2020-05-12 05:05:49 +02:00
(Some(domain), remaining_input) => (domain, remaining_input),
(None, remaining_input) => (crate::Domain::Program, remaining_input),
};
2020-05-12 04:51:31 +02:00
2020-05-12 05:05:49 +02:00
input = remaining_input;
2020-05-06 00:13:43 +02:00
2020-05-12 05:05:49 +02:00
let mut input_constant_declarations =
problem.input_constant_declarations.borrow_mut();
2020-05-05 19:40:57 +02:00
2020-05-12 05:05:49 +02:00
use foliage::FindOrCreateFunctionDeclaration as _;
2020-05-05 19:40:57 +02:00
2020-05-12 05:05:49 +02:00
let constant_declaration =
problem.find_or_create_function_declaration(constant_or_predicate_name, 0);
2020-05-05 19:40:57 +02:00
2020-05-12 05:05:49 +02:00
input_constant_declarations.insert(std::rc::Rc::clone(&constant_declaration));
2020-05-06 00:13:43 +02:00
2020-05-12 05:05:49 +02:00
let mut input_constant_declaration_domains =
problem.input_constant_declaration_domains.borrow_mut();
2020-05-06 00:13:43 +02:00
2020-05-12 05:05:49 +02:00
input_constant_declaration_domains.insert(constant_declaration, domain);
}
2020-05-05 19:40:57 +02:00
2020-05-12 05:05:49 +02:00
let mut input_characters = input.chars();
2020-05-05 19:40:57 +02:00
2020-05-12 05:05:49 +02:00
match input_characters.next()
{
Some(',') => input = input_characters.as_str(),
_ => break,
2020-05-05 19:40:57 +02:00
}
}
expect_statement_terminator(input)
2020-05-05 19:40:57 +02:00
}
fn output_statement_body<'i>(mut input: &'i str, problem: &crate::Problem)
-> Result<&'i str, crate::Error>
{
2020-05-12 06:08:50 +02:00
input = foliage::parse::tokens::trim_start(input);
let mut input_characters = input.chars();
let remaining_input = match input_characters.next()
{
Some(':') => input_characters.as_str(),
_ => return Err(crate::Error::new_expected_colon()),
};
input = remaining_input;
loop
{
2020-05-12 06:08:50 +02:00
input = foliage::parse::tokens::trim_start(input);
let (constant_or_predicate_name, remaining_input) =
foliage::parse::tokens::identifier(input)
.ok_or_else(|| crate::Error::new_expected_identifier())?;
2020-05-12 06:08:50 +02:00
input = foliage::parse::tokens::trim_start(remaining_input);
// Only accept output predicate specifiers
if let (Some(arity), remaining_input) = predicate_arity_specifier(input)?
{
input = remaining_input;
let mut output_predicate_declarations =
problem.output_predicate_declarations.borrow_mut();
use foliage::FindOrCreatePredicateDeclaration as _;
let predicate_declaration =
problem.find_or_create_predicate_declaration(constant_or_predicate_name, arity);
output_predicate_declarations.insert(predicate_declaration);
}
else
{
return Err(crate::Error::new_expected_predicate_specifier());
}
let mut input_characters = input.chars();
match input_characters.next()
{
Some(',') => input = input_characters.as_str(),
_ => break,
}
}
expect_statement_terminator(input)
}
2020-05-05 19:40:57 +02:00
pub(crate) fn parse_specification(mut input: &str, problem: &crate::Problem)
-> Result<(), crate::Error>
{
loop
{
2020-05-12 06:08:50 +02:00
input = foliage::parse::tokens::trim_start(input);
2020-05-05 19:40:57 +02:00
if input.is_empty()
{
return Ok(());
}
let (identifier, remaining_input) = match foliage::parse::tokens::identifier(input)
{
Some(identifier) => identifier,
None => return Err(crate::Error::new_expected_statement()),
};
input = remaining_input;
match identifier
{
"axiom" =>
{
let (formula, remaining_input) = formula_statement_body(input, problem)?;
input = remaining_input;
let statement = crate::problem::Statement::new(
crate::problem::StatementKind::Axiom, formula);
problem.add_statement(crate::problem::SectionKind::Axioms, statement);
continue;
},
"assume" =>
{
let (formula, remaining_input) = formula_statement_body(input, problem)?;
input = remaining_input;
let statement = crate::problem::Statement::new(
crate::problem::StatementKind::Assumption, formula);
problem.add_statement(crate::problem::SectionKind::Assumptions, statement);
continue;
},
"lemma" =>
{
2020-05-12 06:08:50 +02:00
input = foliage::parse::tokens::trim_start(input);
2020-05-05 19:40:57 +02:00
let mut input_characters = input.chars();
let (proof_direction, remaining_input) = match input_characters.next()
{
Some('(') =>
{
// TODO: refactor
2020-05-12 06:08:50 +02:00
input = foliage::parse::tokens::trim_start(input_characters.as_str());
2020-05-05 19:40:57 +02:00
let (proof_direction, remaining_input) = match
foliage::parse::tokens::identifier(input)
{
Some(("forward", remaining_input)) =>
(crate::problem::ProofDirection::Forward, remaining_input),
2020-05-05 19:40:57 +02:00
Some(("backward", remaining_input)) =>
(crate::problem::ProofDirection::Backward, remaining_input),
2020-05-05 19:40:57 +02:00
Some(("both", remaining_input)) =>
(crate::problem::ProofDirection::Both, remaining_input),
2020-05-05 19:40:57 +02:00
Some((identifier, _)) =>
return Err(crate::Error::new_unknown_proof_direction(
identifier.to_string())),
None => (crate::problem::ProofDirection::Both, input),
2020-05-05 19:40:57 +02:00
};
2020-05-12 06:08:50 +02:00
input = foliage::parse::tokens::trim_start(remaining_input);
2020-05-05 19:40:57 +02:00
let mut input_characters = input.chars();
if input_characters.next() != Some(')')
{
return Err(crate::Error::new_unmatched_parenthesis());
}
input = input_characters.as_str();
(proof_direction, input)
},
Some(_)
| None => (crate::problem::ProofDirection::Both, remaining_input),
2020-05-05 19:40:57 +02:00
};
input = remaining_input;
let (formula, remaining_input) = formula_statement_body(input, problem)?;
input = remaining_input;
let statement = crate::problem::Statement::new(
crate::problem::StatementKind::Lemma(proof_direction), formula);
problem.add_statement(crate::problem::SectionKind::Lemmas, statement);
continue;
},
"assert" =>
{
let (formula, remaining_input) = formula_statement_body(input, problem)?;
input = remaining_input;
let statement = crate::problem::Statement::new(
crate::problem::StatementKind::Assertion, formula);
problem.add_statement(crate::problem::SectionKind::Assertions, statement);
continue;
},
"input" => input = input_statement_body(input, problem)?,
"output" => input = output_statement_body(input, problem)?,
2020-05-05 19:40:57 +02:00
identifier => return Err(crate::Error::new_unknown_statement(identifier.to_string())),
}
}
}