Skip input predicates in completion
This commit is contained in:
parent
a802b9f8fd
commit
33c5245b80
|
@ -58,6 +58,8 @@ impl std::fmt::Debug for crate::Project
|
||||||
crate::project::Block::Whitespace(ref text) => write!(format, "{}", text)?,
|
crate::project::Block::Whitespace(ref text) => write!(format, "{}", text)?,
|
||||||
crate::project::Block::FormulaStatement(ref formula_statement) =>
|
crate::project::Block::FormulaStatement(ref formula_statement) =>
|
||||||
write!(format, "{}", formula_statement.original_text)?,
|
write!(format, "{}", formula_statement.original_text)?,
|
||||||
|
crate::project::Block::InputStatement(ref input_statement) =>
|
||||||
|
write!(format, "{}", input_statement.original_text)?,
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -54,6 +54,18 @@ pub fn is_formula_statement_theorem(formula_statement: &crate::project::FormulaS
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pub fn is_formula_statement_ignored(formula_statement: &crate::project::FormulaStatement,
|
||||||
|
input_predicates: &std::collections::HashSet<foliage::PredicateDeclaration>) -> bool
|
||||||
|
{
|
||||||
|
// Hide completed definitions of input predicates
|
||||||
|
if let crate::project::FormulaStatementKind::Completion(crate::project::CompletionTarget::Predicate(ref predicate_declaration)) = formula_statement.kind
|
||||||
|
{
|
||||||
|
return input_predicates.contains(predicate_declaration);
|
||||||
|
}
|
||||||
|
|
||||||
|
false
|
||||||
|
}
|
||||||
|
|
||||||
fn is_arithmetic_term(term: &foliage::Term) -> bool
|
fn is_arithmetic_term(term: &foliage::Term) -> bool
|
||||||
{
|
{
|
||||||
match term
|
match term
|
||||||
|
@ -129,6 +141,7 @@ fn collect_predicate_declarations_in_project<'a>(project: &'a crate::Project)
|
||||||
{
|
{
|
||||||
crate::project::Block::Whitespace(_) => None,
|
crate::project::Block::Whitespace(_) => None,
|
||||||
crate::project::Block::FormulaStatement(ref formula_statement) => Some(&formula_statement.formula),
|
crate::project::Block::FormulaStatement(ref formula_statement) => Some(&formula_statement.formula),
|
||||||
|
crate::project::Block::InputStatement(_) => None,
|
||||||
});
|
});
|
||||||
|
|
||||||
for formula in formulas
|
for formula in formulas
|
||||||
|
@ -253,11 +266,12 @@ fn collect_symbolic_constants_in_project<'a>(project: &'a crate::Project)
|
||||||
let formulas = project.blocks.iter()
|
let formulas = project.blocks.iter()
|
||||||
.filter_map(
|
.filter_map(
|
||||||
|block|
|
|block|
|
||||||
match block
|
match block
|
||||||
{
|
{
|
||||||
crate::project::Block::Whitespace(_) => None,
|
crate::project::Block::Whitespace(_) => None,
|
||||||
crate::project::Block::FormulaStatement(ref formula_statement) => Some(&formula_statement.formula),
|
crate::project::Block::FormulaStatement(ref formula_statement) => Some(&formula_statement.formula),
|
||||||
});
|
crate::project::Block::InputStatement(_) => None,
|
||||||
|
});
|
||||||
|
|
||||||
for formula in formulas
|
for formula in formulas
|
||||||
{
|
{
|
||||||
|
@ -701,11 +715,19 @@ impl<'a> std::fmt::Debug for ProjectDisplay<'a>
|
||||||
{
|
{
|
||||||
crate::project::Block::Whitespace(_) => None,
|
crate::project::Block::Whitespace(_) => None,
|
||||||
crate::project::Block::FormulaStatement(ref formula_statement) =>
|
crate::project::Block::FormulaStatement(ref formula_statement) =>
|
||||||
|
{
|
||||||
|
if is_formula_statement_ignored(formula_statement, &self.project.input_predicates)
|
||||||
|
{
|
||||||
|
return None;
|
||||||
|
}
|
||||||
|
|
||||||
match is_formula_statement_axiom(&formula_statement, self.proof_direction)
|
match is_formula_statement_axiom(&formula_statement, self.proof_direction)
|
||||||
{
|
{
|
||||||
true => Some(formula_statement),
|
true => Some(formula_statement),
|
||||||
false => None,
|
false => None,
|
||||||
}
|
}
|
||||||
|
},
|
||||||
|
crate::project::Block::InputStatement(_) => None,
|
||||||
});
|
});
|
||||||
|
|
||||||
for axiom in axioms
|
for axiom in axioms
|
||||||
|
|
23
src/main.rs
23
src/main.rs
|
@ -9,10 +9,9 @@ fn reset_proof_results<'a>(project: &'a mut ask_dracula::Project)
|
||||||
{
|
{
|
||||||
for block in &mut project.blocks
|
for block in &mut project.blocks
|
||||||
{
|
{
|
||||||
match block
|
if let ask_dracula::project::Block::FormulaStatement(ref mut formula_statement) = block
|
||||||
{
|
{
|
||||||
ask_dracula::project::Block::Whitespace(_) => (),
|
formula_statement.proven = false;
|
||||||
ask_dracula::project::Block::FormulaStatement(ref mut formula_statement) => formula_statement.proven = false,
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -119,6 +118,8 @@ fn main() -> Result<(), Box<dyn std::error::Error>>
|
||||||
|
|
||||||
reset_proof_results(&mut project);
|
reset_proof_results(&mut project);
|
||||||
|
|
||||||
|
let input_predicates = &project.input_predicates;
|
||||||
|
|
||||||
loop
|
loop
|
||||||
{
|
{
|
||||||
let conjecture = project.blocks.iter()
|
let conjecture = project.blocks.iter()
|
||||||
|
@ -127,11 +128,11 @@ fn main() -> Result<(), Box<dyn std::error::Error>>
|
||||||
|block|
|
|block|
|
||||||
match block
|
match block
|
||||||
{
|
{
|
||||||
ask_dracula::project::Block::Whitespace(_) => None,
|
|
||||||
ask_dracula::project::Block::FormulaStatement(ref formula_statement) => Some(formula_statement),
|
ask_dracula::project::Block::FormulaStatement(ref formula_statement) => Some(formula_statement),
|
||||||
|
_ => None,
|
||||||
}
|
}
|
||||||
)
|
)
|
||||||
.find(|formula_statement| ask_dracula::format_tptp::is_formula_statement_lemma(&formula_statement, proof_direction));
|
.find(|formula_statement| !ask_dracula::format_tptp::is_formula_statement_ignored(&formula_statement, &input_predicates) && ask_dracula::format_tptp::is_formula_statement_lemma(&formula_statement, proof_direction));
|
||||||
|
|
||||||
let conjecture = match conjecture
|
let conjecture = match conjecture
|
||||||
{
|
{
|
||||||
|
@ -142,11 +143,11 @@ fn main() -> Result<(), Box<dyn std::error::Error>>
|
||||||
|block|
|
|block|
|
||||||
match block
|
match block
|
||||||
{
|
{
|
||||||
ask_dracula::project::Block::Whitespace(_) => None,
|
|
||||||
ask_dracula::project::Block::FormulaStatement(ref formula_statement) => Some(formula_statement),
|
ask_dracula::project::Block::FormulaStatement(ref formula_statement) => Some(formula_statement),
|
||||||
|
_ => None,
|
||||||
}
|
}
|
||||||
)
|
)
|
||||||
.find(|formula_statement| ask_dracula::format_tptp::is_formula_statement_theorem(&formula_statement, proof_direction)),
|
.find(|formula_statement| !ask_dracula::format_tptp::is_formula_statement_ignored(&formula_statement, &input_predicates) && ask_dracula::format_tptp::is_formula_statement_theorem(&formula_statement, proof_direction)),
|
||||||
};
|
};
|
||||||
|
|
||||||
let conjecture = match conjecture
|
let conjecture = match conjecture
|
||||||
|
@ -189,11 +190,11 @@ fn main() -> Result<(), Box<dyn std::error::Error>>
|
||||||
|block|
|
|block|
|
||||||
match block
|
match block
|
||||||
{
|
{
|
||||||
ask_dracula::project::Block::Whitespace(_) => None,
|
|
||||||
ask_dracula::project::Block::FormulaStatement(ref mut formula_statement) => Some(formula_statement),
|
ask_dracula::project::Block::FormulaStatement(ref mut formula_statement) => Some(formula_statement),
|
||||||
|
_ => None,
|
||||||
}
|
}
|
||||||
)
|
)
|
||||||
.find(|formula_statement| ask_dracula::format_tptp::is_formula_statement_lemma(&formula_statement, proof_direction));
|
.find(|formula_statement| !ask_dracula::format_tptp::is_formula_statement_ignored(&formula_statement, &input_predicates) && ask_dracula::format_tptp::is_formula_statement_lemma(&formula_statement, proof_direction));
|
||||||
|
|
||||||
let mut conjecture = match conjecture
|
let mut conjecture = match conjecture
|
||||||
{
|
{
|
||||||
|
@ -204,11 +205,11 @@ fn main() -> Result<(), Box<dyn std::error::Error>>
|
||||||
|block|
|
|block|
|
||||||
match block
|
match block
|
||||||
{
|
{
|
||||||
ask_dracula::project::Block::Whitespace(_) => None,
|
|
||||||
ask_dracula::project::Block::FormulaStatement(ref mut formula_statement) => Some(formula_statement),
|
ask_dracula::project::Block::FormulaStatement(ref mut formula_statement) => Some(formula_statement),
|
||||||
|
_ => None,
|
||||||
}
|
}
|
||||||
)
|
)
|
||||||
.find(|formula_statement| ask_dracula::format_tptp::is_formula_statement_theorem(&formula_statement, proof_direction)),
|
.find(|formula_statement| !ask_dracula::format_tptp::is_formula_statement_ignored(&formula_statement, &input_predicates) && ask_dracula::format_tptp::is_formula_statement_theorem(&formula_statement, proof_direction)),
|
||||||
}.unwrap();
|
}.unwrap();
|
||||||
|
|
||||||
conjecture.proven = true;
|
conjecture.proven = true;
|
||||||
|
|
136
src/parse.rs
136
src/parse.rs
|
@ -6,6 +6,7 @@ use nom::
|
||||||
character::complete::digit1,
|
character::complete::digit1,
|
||||||
branch::alt,
|
branch::alt,
|
||||||
bytes::complete::tag,
|
bytes::complete::tag,
|
||||||
|
multi::separated_list,
|
||||||
};
|
};
|
||||||
|
|
||||||
use foliage::parse::whitespace0;
|
use foliage::parse::whitespace0;
|
||||||
|
@ -31,7 +32,7 @@ where
|
||||||
|
|
||||||
fn formula_statement_kind(i: &str) -> IResult<&str, crate::project::FormulaStatementKind>
|
fn formula_statement_kind(i: &str) -> IResult<&str, crate::project::FormulaStatementKind>
|
||||||
{
|
{
|
||||||
let foo = delimited
|
delimited
|
||||||
(
|
(
|
||||||
whitespace0,
|
whitespace0,
|
||||||
alt
|
alt
|
||||||
|
@ -101,9 +102,7 @@ fn formula_statement_kind(i: &str) -> IResult<&str, crate::project::FormulaState
|
||||||
),
|
),
|
||||||
)),
|
)),
|
||||||
whitespace0,
|
whitespace0,
|
||||||
)(i);
|
)(i)
|
||||||
|
|
||||||
foo
|
|
||||||
}
|
}
|
||||||
|
|
||||||
fn formula_statement(i: &str) -> IResult<&str, (crate::project::FormulaStatementKind, foliage::Formula)>
|
fn formula_statement(i: &str) -> IResult<&str, (crate::project::FormulaStatementKind, foliage::Formula)>
|
||||||
|
@ -123,13 +122,84 @@ fn formula_statement(i: &str) -> IResult<&str, (crate::project::FormulaStatement
|
||||||
)(i)
|
)(i)
|
||||||
}
|
}
|
||||||
|
|
||||||
fn formula_statement_enclosed_by_whitespace(i: &str)
|
fn input_statement(i: &str) -> IResult<&str, Vec<crate::project::InputSymbol>>
|
||||||
-> IResult<&str, (&str, (&str, (crate::project::FormulaStatementKind, foliage::Formula)), &str)>
|
{
|
||||||
|
delimited
|
||||||
|
(
|
||||||
|
whitespace0,
|
||||||
|
preceded
|
||||||
|
(
|
||||||
|
pair
|
||||||
|
(
|
||||||
|
tag("input:"),
|
||||||
|
whitespace0,
|
||||||
|
),
|
||||||
|
separated_list
|
||||||
|
(
|
||||||
|
tag(","),
|
||||||
|
delimited
|
||||||
|
(
|
||||||
|
whitespace0,
|
||||||
|
alt
|
||||||
|
((
|
||||||
|
map
|
||||||
|
(
|
||||||
|
pair
|
||||||
|
(
|
||||||
|
terminated
|
||||||
|
(
|
||||||
|
foliage::parse::symbolic_identifier,
|
||||||
|
tag("/"),
|
||||||
|
),
|
||||||
|
digit1,
|
||||||
|
),
|
||||||
|
|(name, arity)|
|
||||||
|
crate::project::InputSymbol::Predicate(
|
||||||
|
foliage::PredicateDeclaration
|
||||||
|
{
|
||||||
|
name: name.to_string(),
|
||||||
|
arity: arity.parse::<usize>().expect("invalid arity"),
|
||||||
|
})
|
||||||
|
),
|
||||||
|
map
|
||||||
|
(
|
||||||
|
foliage::parse::symbolic_identifier,
|
||||||
|
|name|
|
||||||
|
crate::project::InputSymbol::Constant(name.to_string())
|
||||||
|
),
|
||||||
|
)),
|
||||||
|
whitespace0,
|
||||||
|
)
|
||||||
|
)
|
||||||
|
),
|
||||||
|
preceded
|
||||||
|
(
|
||||||
|
whitespace0,
|
||||||
|
tag("."),
|
||||||
|
),
|
||||||
|
)(i)
|
||||||
|
}
|
||||||
|
|
||||||
|
pub enum Statement
|
||||||
|
{
|
||||||
|
Formula(crate::project::FormulaStatementKind, foliage::Formula),
|
||||||
|
Input(Vec<crate::project::InputSymbol>),
|
||||||
|
}
|
||||||
|
|
||||||
|
fn statement_enclosed_by_whitespace(i: &str)
|
||||||
|
-> IResult<&str, (&str, (&str, Statement), &str)>
|
||||||
{
|
{
|
||||||
tuple
|
tuple
|
||||||
((
|
((
|
||||||
recognize(whitespace0),
|
recognize(whitespace0),
|
||||||
recognize_and_keep(formula_statement),
|
recognize_and_keep
|
||||||
|
(
|
||||||
|
alt
|
||||||
|
((
|
||||||
|
map(formula_statement, |(formula_statement_kind, formula)| Statement::Formula(formula_statement_kind, formula)),
|
||||||
|
map(input_statement, |input_symbols| Statement::Input(input_symbols)),
|
||||||
|
))
|
||||||
|
),
|
||||||
recognize(whitespace0),
|
recognize(whitespace0),
|
||||||
))(i)
|
))(i)
|
||||||
}
|
}
|
||||||
|
@ -138,13 +208,15 @@ pub fn project(i: &str) -> IResult<&str, crate::Project>
|
||||||
{
|
{
|
||||||
let mut statement_input = i.clone();
|
let mut statement_input = i.clone();
|
||||||
let mut blocks = Vec::new();
|
let mut blocks = Vec::new();
|
||||||
|
let mut input_constants = std::collections::HashSet::new();
|
||||||
|
let mut input_predicates = std::collections::HashSet::new();
|
||||||
|
|
||||||
loop
|
loop
|
||||||
{
|
{
|
||||||
let i_ = statement_input.clone();
|
let i_ = statement_input.clone();
|
||||||
match formula_statement_enclosed_by_whitespace(i_)
|
match statement_enclosed_by_whitespace(i_)
|
||||||
{
|
{
|
||||||
Ok((i, (whitespace_before, (formula_statement_original_text, (formula_statement_kind, formula)), whitespace_after))) =>
|
Ok((i, (whitespace_before, (statement_original_text, statement), whitespace_after))) =>
|
||||||
{
|
{
|
||||||
// Iteration must always consume input (to prevent infinite loops)
|
// Iteration must always consume input (to prevent infinite loops)
|
||||||
if i == statement_input
|
if i == statement_input
|
||||||
|
@ -157,15 +229,45 @@ pub fn project(i: &str) -> IResult<&str, crate::Project>
|
||||||
blocks.push(crate::project::Block::Whitespace(whitespace_before.to_string()));
|
blocks.push(crate::project::Block::Whitespace(whitespace_before.to_string()));
|
||||||
}
|
}
|
||||||
|
|
||||||
let formula_statement = crate::project::FormulaStatement
|
match statement
|
||||||
{
|
{
|
||||||
kind: formula_statement_kind,
|
Statement::Formula(formula_statement_kind, formula) =>
|
||||||
original_text: formula_statement_original_text.to_string(),
|
{
|
||||||
formula,
|
let formula_statement = crate::project::FormulaStatement
|
||||||
proven: false,
|
{
|
||||||
};
|
kind: formula_statement_kind,
|
||||||
|
original_text: statement_original_text.to_string(),
|
||||||
|
formula,
|
||||||
|
proven: false,
|
||||||
|
};
|
||||||
|
|
||||||
blocks.push(crate::project::Block::FormulaStatement(formula_statement));
|
blocks.push(crate::project::Block::FormulaStatement(formula_statement));
|
||||||
|
},
|
||||||
|
Statement::Input(input_symbols) =>
|
||||||
|
{
|
||||||
|
for input_symbol in input_symbols
|
||||||
|
{
|
||||||
|
match input_symbol
|
||||||
|
{
|
||||||
|
crate::project::InputSymbol::Constant(name) =>
|
||||||
|
{
|
||||||
|
input_constants.insert(name);
|
||||||
|
},
|
||||||
|
crate::project::InputSymbol::Predicate(declaration) =>
|
||||||
|
{
|
||||||
|
input_predicates.insert(declaration);
|
||||||
|
},
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
let input_statement = crate::project::InputStatement
|
||||||
|
{
|
||||||
|
original_text: statement_original_text.to_string(),
|
||||||
|
};
|
||||||
|
|
||||||
|
blocks.push(crate::project::Block::InputStatement(input_statement));
|
||||||
|
},
|
||||||
|
}
|
||||||
|
|
||||||
if !whitespace_after.is_empty()
|
if !whitespace_after.is_empty()
|
||||||
{
|
{
|
||||||
|
@ -191,6 +293,8 @@ pub fn project(i: &str) -> IResult<&str, crate::Project>
|
||||||
let project = crate::Project
|
let project = crate::Project
|
||||||
{
|
{
|
||||||
blocks,
|
blocks,
|
||||||
|
input_constants,
|
||||||
|
input_predicates,
|
||||||
};
|
};
|
||||||
|
|
||||||
Ok((i, project))
|
Ok((i, project))
|
||||||
|
|
|
@ -30,13 +30,27 @@ pub struct FormulaStatement
|
||||||
pub proven: bool,
|
pub proven: bool,
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pub struct InputStatement
|
||||||
|
{
|
||||||
|
pub original_text: String,
|
||||||
|
}
|
||||||
|
|
||||||
|
pub enum InputSymbol
|
||||||
|
{
|
||||||
|
Constant(String),
|
||||||
|
Predicate(foliage::PredicateDeclaration),
|
||||||
|
}
|
||||||
|
|
||||||
pub enum Block
|
pub enum Block
|
||||||
{
|
{
|
||||||
FormulaStatement(FormulaStatement),
|
FormulaStatement(FormulaStatement),
|
||||||
|
InputStatement(InputStatement),
|
||||||
Whitespace(String),
|
Whitespace(String),
|
||||||
}
|
}
|
||||||
|
|
||||||
pub struct Project
|
pub struct Project
|
||||||
{
|
{
|
||||||
pub blocks: Vec<Block>,
|
pub blocks: Vec<Block>,
|
||||||
|
pub input_constants: std::collections::HashSet<String>,
|
||||||
|
pub input_predicates: std::collections::HashSet<foliage::PredicateDeclaration>,
|
||||||
}
|
}
|
||||||
|
|
Loading…
Reference in New Issue