Skip to content

Commit

Permalink
grammar bugfixes
Browse files Browse the repository at this point in the history
  • Loading branch information
@digama0
digama0 committed Sep 29, 2023
1 parent a86a122 commit 925b106
Show file tree
Hide file tree
Showing 3 changed files with 125 additions and 96 deletions.
4 changes: 2 additions & 2 deletions src/formula.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -753,14 +753,14 @@ impl<'a> Debug for FormulaRef<'a> {
}
}

#[derive(Default)]
/// A utility to build a formula.
#[derive(Default, Debug)]
pub(crate) struct FormulaBuilder {
stack: Vec<NodeId>,
variables: Bitset,
tree: Tree<Label>,
}

/// A utility to build a formula.
impl FormulaBuilder {
pub(crate) fn from_formula(fmla: Formula) -> Self {
let stack = vec![fmla.root];
Expand Down
181 changes: 87 additions & 94 deletions src/grammar.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -416,18 +416,20 @@ impl Grammar {
let buf = &**sref.buffer;
for (_, (_, command)) in &sref.j_commands {
use CommandToken::*;
match &**command {
[Keyword(cmd), sort, Keyword(as_), logic]
if cmd.as_ref(buf) == b"syntax" && as_.as_ref(buf) == b"as" =>
{
let [Keyword(cmd), rest @ ..] = &**command else { continue };
let b"syntax" = cmd.as_ref(buf) else { continue };
match rest {
[sort, Keyword(as_), logic] if as_.as_ref(buf) == b"as" => {
self.provable_type = nset.lookup_symbol(&sort.value(buf)).unwrap().atom;
self.logic_type = nset.lookup_symbol(&logic.value(buf)).unwrap().atom;
self.typecodes.push(self.logic_type);
self.typecodes.push(self.provable_type);
}
_ => {
for sort in rest {
self.typecodes
.push(nset.lookup_symbol(&sort.value(buf)).unwrap().atom)
}
}
[Keyword(cmd), sort] if cmd.as_ref(buf) == b"syntax" => self
.typecodes
.push(nset.lookup_symbol(&sort.value(buf)).unwrap().atom),
_ => {}
}
}
}
Expand Down Expand Up @@ -1090,7 +1092,6 @@ impl Grammar {
db: &Database,
names: &mut NameReader<'_>,
) -> Result<(), (StatementAddress, Diagnostic)> {
let nset = db.name_result();
for sref in db.parse_result().segments(..) {
let buf = &**sref.buffer;
for &(ix, (span, ref command)) in &sref.j_commands {
Expand All @@ -1102,29 +1103,6 @@ impl Grammar {
{
// Empty parser command
match k.as_ref(buf) {
b"syntax" => match rest {
[ty, Keyword(as_), code] if as_.as_ref(buf) == b"as" => {
// syntax '|-' as 'wff';
self.provable_type = nset
.lookup_symbol(&ty.value(buf))
.ok_or((address, undefined_cmd(ty, buf)))?
.atom;
self.typecodes.push(
nset.lookup_symbol(&code.value(buf))
.ok_or((address, undefined_cmd(code, buf)))?
.atom,
);
}
[ty] => {
// syntax 'setvar';
self.typecodes.push(
nset.lookup_symbol(&ty.value(buf))
.ok_or((address, undefined_cmd(ty, buf)))?
.atom,
);
}
_ => {}
},
// Handle Ambiguous prefix commands
b"garden_path" => {
let split_index = rest
Expand Down Expand Up @@ -1218,77 +1196,92 @@ impl Grammar {
// We found a leaf: REDUCE
Self::do_reduce(&mut formula_builder, reduce, nset);

if e.expected_typecodes.contains(&typecode) {
// We found an expected typecode, pop from the stack and continue
if let Some(popped) = stack.pop() {
e = popped;
debug!(
" ++ Finished parsing formula, found typecode {:?}, back to {}",
as_str(nset.atom_name(typecode)),
e.node_id
);
let map = self.get_branch(e.node_id);
match map.get(&(SymbolType::Variable, typecode)) {
Some(NextNode {
next_node_id,
leaf_label,
}) => {
// Found a sub-formula: First optionally REDUCE and continue
for &reduce in leaf_label {
Self::do_reduce(&mut formula_builder, reduce, nset);
loop {
if e.expected_typecodes.contains(&typecode) {
// We found an expected typecode, pop from the stack and continue
if let Some(popped) = stack.pop() {
e = popped;
debug!(
" ++ Finished parsing formula, found typecode {:?}, back to {}",
as_str(nset.atom_name(typecode)),
e.node_id
);
let map = self.get_branch(e.node_id);
match map.get(&(SymbolType::Variable, typecode)) {
Some(NextNode {
next_node_id,
leaf_label,
}) => {
// Found a sub-formula: First optionally REDUCE and continue
for &reduce in leaf_label {
Self::do_reduce(&mut formula_builder, reduce, nset);
}

e.node_id = *next_node_id;
debug!(" Next Node: {:?}", e.node_id);
}
None => {
debug!("TODO");
}

e.node_id = *next_node_id;
debug!(" Next Node: {:?}", e.node_id);
}
None => {
debug!("TODO");
} else if symbol_enum.peek().is_none() {
// We popped the last element from the stack and we are at the end of the math string, success
if typecode == self.logic_type && convert_to_provable {
typecode = self.provable_type;
}
}
} else if symbol_enum.peek().is_none() {
// We popped the last element from the stack and we are at the end of the math string, success
if typecode == self.logic_type && convert_to_provable {
typecode = self.provable_type;
}
return Ok(formula_builder.build(typecode));
} else {
// There are still symbols to parse, continue from root
let (next_node_id, leaf_label) = self
.next_var_node(self.root, typecode)
.ok_or(StmtParseError::UnparseableStatement(last_token.span))?;
for &reduce in leaf_label {
Self::do_reduce(&mut formula_builder, reduce, nset);
}
e.node_id = next_node_id;
}
} else {
// We have parsed everything but did not obtain an expected typecode, try a type conversion.
if symbol_enum.peek().is_none() {
for (from_typecode, to_typecode, label) in &self.type_conversions {
if *from_typecode == typecode
&& e.expected_typecodes.contains(to_typecode)
{
let reduce = Reduce::new(*label, 1);
return Ok(formula_builder.build(typecode));
} else {
// There are still symbols to parse, continue from root
let (next_node_id, leaf_label) = self
.next_var_node(self.root, typecode)
.ok_or(StmtParseError::UnparseableStatement(last_token.span))?;
for &reduce in leaf_label {
Self::do_reduce(&mut formula_builder, reduce, nset);
let typecode =
if *to_typecode == self.logic_type && convert_to_provable {
self.provable_type
} else {
*to_typecode
};
return Ok(formula_builder.build(typecode));
}
e.node_id = next_node_id;
}
break;
}
// // We have parsed everything but did not obtain an expected typecode, try a type conversion.
// if symbol_enum.peek().is_none() {
// for (from_typecode, to_typecode, label) in &self.type_conversions {
// if *from_typecode == typecode
// && e.expected_typecodes.contains(to_typecode)
// {
// let reduce = Reduce::new(*label, 1);
// Self::do_reduce(&mut formula_builder, reduce, nset);
// let typecode =
// if *to_typecode == self.logic_type && convert_to_provable {
// self.provable_type
// } else {
// *to_typecode
// };
// return Ok(formula_builder.build(typecode));
// }
// }
// }
// We have not found the expected typecode, continue from root
debug!(" ++ Wrong type obtained, continue.");
let (next_node_id, leaf_label) = self
.next_var_node(self.root, typecode)
.ok_or(StmtParseError::UnparseableStatement(last_token.span))?;
for &reduce in leaf_label {
Self::do_reduce(&mut formula_builder, reduce, nset);
if let Some((next_node_id, leaf_label)) =
self.next_var_node(self.root, typecode)
{
for &reduce in leaf_label {
Self::do_reduce(&mut formula_builder, reduce, nset);
}
e.node_id = next_node_id;
break;
}
e.node_id = next_node_id;

// We did not obtain an expected typecode, try a type conversion.
debug!(" ++ Can't shift, try a type conversion.");
let (_, to, label) = self
.type_conversions
.iter()
.find(|(from, _, _)| *from == typecode)
.ok_or(StmtParseError::UnparseableStatement(last_token.span))?;
let reduce = Reduce::new(*label, 1);
Self::do_reduce(&mut formula_builder, reduce, nset);
typecode = *to;
}
}
GrammarNode::Branch { ref map } => {
Expand Down
36 changes: 36 additions & 0 deletions src/grammar_tests.rs
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
use std::sync::Arc;

use simple_logger::SimpleLogger;

use crate::as_str;
use crate::database::Database;
use crate::database::DbOptions;
Expand Down Expand Up @@ -329,6 +331,40 @@ macro_rules! grammar_test {
};
}

const ISSUE_135: &[u8] = b"
$c = class wff setvar -> ( ) |- + [ ] $.
$( $j syntax 'setvar' 'class' 'wff'; syntax '|-' as 'wff'; $)
$v x A B ph ps $.
vx $f setvar x $.
wph $f wff ph $.
wps $f wff ps $.
cA $f class A $.
cB $f class B $.
cv $a class x $.
wn $a wff [ A ] $.
wceq $a wff A = B $.
wi $a wff ( ph -> ps ) $.
cdif $a class ( A + B ) $.
ax1 $a |- [ x ] $.
ax2 $a |- ( x = x -> ph ) $.
";

#[test]
fn test_issue_135() {
SimpleLogger::new().without_timestamps().init().unwrap();
let mut db = mkdb(ISSUE_135);
let stmt_parse = db.stmt_parse_pass().clone();
let sref = db.statement(b"ax1").unwrap();
let formula = stmt_parse.get_formula(&sref).unwrap();
assert_eq!(formula.as_ref(&db).as_sexpr(), "(wn (cv vx))");
let sref = db.statement(b"ax2").unwrap();
let formula = stmt_parse.get_formula(&sref).unwrap();

Check failure on line 361 in src/grammar_tests.rs

View workflow job for this annotation

GitHub Actions / Rebuild and test (ubuntu-20.04, stable) 

called `Option::unwrap()` on a `None` value

Check failure on line 361 in src/grammar_tests.rs

View workflow job for this annotation

GitHub Actions / Rebuild and test (ubuntu-latest, stable) 

called `Option::unwrap()` on a `None` value

Check failure on line 361 in src/grammar_tests.rs

View workflow job for this annotation

GitHub Actions / Rebuild and test (ubuntu-20.04, stable) 

called `Option::unwrap()` on a `None` value

Check failure on line 361 in src/grammar_tests.rs

View workflow job for this annotation

GitHub Actions / Rebuild and test (ubuntu-latest, stable) 

called `Option::unwrap()` on a `None` value
assert_eq!(
formula.as_ref(&db).as_sexpr(),
"(wi (wceq (cv vx) (cv vx)) wph)"
);
}

grammar_test!(
test_missing_float,
b"$c setvar $. $v x $. vx $a setvar x $.",
Expand Down

0 comments on commit 925b106

Please sign in to comment.