2019-11-07 05:42:42 +01:00
|
|
|
#[derive(Clone, Copy, Eq, Hash, PartialEq)]
|
|
|
|
pub enum ProofDirection
|
|
|
|
{
|
|
|
|
Forward,
|
|
|
|
Backward,
|
|
|
|
}
|
|
|
|
|
2019-11-07 04:20:06 +01:00
|
|
|
#[derive(Eq, Hash, PartialEq)]
|
|
|
|
pub enum CompletionTarget
|
|
|
|
{
|
|
|
|
Predicate(foliage::PredicateDeclaration),
|
|
|
|
Constraint,
|
|
|
|
}
|
|
|
|
|
|
|
|
#[derive(Eq, Hash, PartialEq)]
|
2019-11-07 08:12:26 +01:00
|
|
|
pub enum FormulaStatementKind
|
2019-11-02 02:13:45 +01:00
|
|
|
{
|
|
|
|
Axiom,
|
2019-11-07 04:20:06 +01:00
|
|
|
Completion(CompletionTarget),
|
2019-11-07 05:42:42 +01:00
|
|
|
Lemma(Option<ProofDirection>),
|
2019-11-06 07:18:30 +01:00
|
|
|
Assumption,
|
|
|
|
Assertion,
|
2019-11-02 02:13:45 +01:00
|
|
|
}
|
|
|
|
|
2019-11-07 08:12:26 +01:00
|
|
|
pub struct FormulaStatement
|
2019-11-02 02:13:45 +01:00
|
|
|
{
|
2019-11-07 08:12:26 +01:00
|
|
|
pub kind: FormulaStatementKind,
|
2019-11-06 11:36:51 +01:00
|
|
|
pub original_text: String,
|
2019-11-05 19:44:28 +01:00
|
|
|
pub formula: foliage::Formula,
|
2019-11-07 07:53:50 +01:00
|
|
|
pub proven: bool,
|
2019-11-05 19:44:28 +01:00
|
|
|
}
|
|
|
|
|
2019-11-07 09:17:49 +01:00
|
|
|
pub struct InputStatement
|
|
|
|
{
|
|
|
|
pub original_text: String,
|
|
|
|
}
|
|
|
|
|
2019-11-07 10:14:44 +01:00
|
|
|
#[derive(Eq, Hash, PartialEq)]
|
|
|
|
pub struct InputConstantDeclaration
|
|
|
|
{
|
|
|
|
pub name: String,
|
|
|
|
pub domain: foliage::Domain,
|
|
|
|
}
|
|
|
|
|
2019-11-07 09:17:49 +01:00
|
|
|
pub enum InputSymbol
|
|
|
|
{
|
2019-11-07 10:14:44 +01:00
|
|
|
Constant(InputConstantDeclaration),
|
2019-11-07 09:17:49 +01:00
|
|
|
Predicate(foliage::PredicateDeclaration),
|
|
|
|
}
|
|
|
|
|
2019-11-06 11:36:51 +01:00
|
|
|
pub enum Block
|
2019-11-05 19:44:28 +01:00
|
|
|
{
|
2019-11-07 08:12:26 +01:00
|
|
|
FormulaStatement(FormulaStatement),
|
2019-11-07 09:17:49 +01:00
|
|
|
InputStatement(InputStatement),
|
2019-11-06 11:36:51 +01:00
|
|
|
Whitespace(String),
|
2019-11-05 19:44:28 +01:00
|
|
|
}
|
|
|
|
|
2019-11-06 11:36:51 +01:00
|
|
|
pub struct Project
|
2019-11-05 19:44:28 +01:00
|
|
|
{
|
2019-11-06 11:36:51 +01:00
|
|
|
pub blocks: Vec<Block>,
|
2019-11-07 10:14:44 +01:00
|
|
|
pub input_constants: std::collections::HashSet<InputConstantDeclaration>,
|
2019-11-07 09:17:49 +01:00
|
|
|
pub input_predicates: std::collections::HashSet<foliage::PredicateDeclaration>,
|
2019-11-02 02:13:45 +01:00
|
|
|
}
|