Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

support syntax 'A' 'B' 'C'; command, style #144

Merged
merged 1 commit into from
Oct 18, 2023
Merged

support syntax 'A' 'B' 'C'; command, style #144

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
211 changes: 95 additions & 116 deletions src/grammar.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -424,9 +424,12 @@ impl Grammar {
self.logic_type = nset.lookup_symbol(&logic.value(buf)).unwrap().atom;
self.typecodes.push(self.logic_type);
}
[Keyword(cmd), sort] if cmd.as_ref(buf) == b"syntax" => self
.typecodes
.push(nset.lookup_symbol(&sort.value(buf)).unwrap().atom),
[Keyword(cmd), rest @ ..] if cmd.as_ref(buf) == b"syntax" => {
for sort in rest {
self.typecodes
.push(nset.lookup_symbol(&sort.value(buf)).unwrap().atom)
}
}
_ => {}
}
}
Expand Down Expand Up @@ -517,31 +520,24 @@ impl Grammar {
stype: SymbolType,
add_reduce: ReduceVec,
) -> Result<NodeId, NodeId> {
match self.nodes.get_mut(to_node) {
GrammarNode::Leaf { .. } => {
Err(to_node) // Error: cannot add to a leaf node, `to_node` is the conflicting node
}
GrammarNode::Branch { map } => {
match map.get(&(stype, symbol)) {
Some(prev_node) if prev_node.leaf_label == add_reduce => {
Ok(prev_node.next_node_id)
}
Some(prev_node) => Err(prev_node.next_node_id),
None => {
let new_node_id = self.nodes.create_branch();
// here we have to re-borrow from self after the creation,
// because the previous var_map and cst_map may not be valid pointers anymore
if let GrammarNode::Branch { map } = self.nodes.get_mut(to_node) {
map.insert(
(stype, symbol),
NextNode::new_with_reduce_vec(new_node_id, add_reduce),
);
Ok(new_node_id)
} else {
panic!("Shall not happen!");
}
}
}
let GrammarNode::Branch { map } = self.nodes.get_mut(to_node) else {
return Err(to_node); // Error: cannot add to a leaf node, `to_node` is the conflicting node
};
match map.get(&(stype, symbol)) {
Some(prev_node) if prev_node.leaf_label == add_reduce => Ok(prev_node.next_node_id),
Some(prev_node) => Err(prev_node.next_node_id),
None => {
let new_node_id = self.nodes.create_branch();
// here we have to re-borrow from self after the creation,
// because the previous var_map and cst_map may not be valid pointers anymore
let GrammarNode::Branch { map } = self.nodes.get_mut(to_node) else {
unreachable!();
};
map.insert(
(stype, symbol),
NextNode::new_with_reduce_vec(new_node_id, add_reduce),
);
Ok(new_node_id)
}
}
}
Expand Down Expand Up @@ -574,14 +570,11 @@ impl Grammar {
.lookup_symbol(token_ptr)
.ok_or_else(|| Diagnostic::UndefinedToken(sref.math_span(1), token_ptr.into()))?;
if symbol.stype == SymbolType::Variable {
let from_typecode = match names.lookup_float(token_ptr) {
Some(lookup_float) => lookup_float.typecode_atom,
_ => {
return Err(Diagnostic::VariableMissingFloat(1));
}
let Some(lookup_float) = names.lookup_float(token_ptr) else {
return Err(Diagnostic::VariableMissingFloat(1));
};
self.type_conversions
.push((from_typecode, this_typecode, this_label));
.push((lookup_float.typecode_atom, this_typecode, this_label));
return Ok(()); // we don't need to add the type conversion axiom itself to the grammar (or do we?)
}
}
Expand All @@ -605,14 +598,13 @@ impl Grammar {
.typecode_atom
}
};
match match &tokens.peek() {
Some(_) => self.add_branch_with_reduce(node, atom, symbol.stype, ReduceVec::new()),
None => {
let leaf_node_id = self
.nodes
.create_leaf(Reduce::new(this_label, var_count), this_typecode);
self.add_branch(node, atom, symbol.stype, &NextNode::new(leaf_node_id))
}
match if tokens.peek().is_some() {
self.add_branch_with_reduce(node, atom, symbol.stype, ReduceVec::new())
} else {
let leaf_node_id = self
.nodes
.create_leaf(Reduce::new(this_label, var_count), this_typecode);
self.add_branch(node, atom, symbol.stype, &NextNode::new(leaf_node_id))
} {
Ok(next_node) => {
node = next_node;
Expand Down Expand Up @@ -662,21 +654,19 @@ impl Grammar {
as_str(nset.statement_name(sref))
);

match self.nodes.get_mut(self.root) {
// We ignore the ambiguity in floats, since they are actually frame dependent.
GrammarNode::Branch { map } => {
map.insert(
(SymbolType::Constant, symbol.atom),
NextNode::new(leaf_node),
);
Ok(())
// match cst_map.insert(symbol.atom, NextNode::new(leaf_node)) {
// None => Ok(()),
// Some(_) => Err(self.ambiguous(conflict_node.next_node_id, nset)),
// }
}
GrammarNode::Leaf { .. } => panic!("Root node shall be a branch node!"),
}
let GrammarNode::Branch { map } = self.nodes.get_mut(self.root) else {
unreachable!("Root node must be a branch node!")
};
// We ignore the ambiguity in floats, since they are actually frame dependent.
map.insert(
(SymbolType::Constant, symbol.atom),
NextNode::new(leaf_node),
);
Ok(())
// match cst_map.insert(symbol.atom, NextNode::new(leaf_node)) {
// None => Ok(()),
// Some(_) => Err(self.ambiguous(conflict_node.next_node_id, nset)),
// }
}

/// Handle type conversion:
Expand Down Expand Up @@ -737,16 +727,14 @@ impl Grammar {
}

fn next_var_node(&self, node_id: NodeId, typecode: TypeCode) -> Option<(NodeId, &ReduceVec)> {
match self.nodes.get(node_id) {
GrammarNode::Branch { map } => match map.get(&(SymbolType::Variable, typecode)) {
Some(NextNode {
next_node_id,
leaf_label,
}) => Some((*next_node_id, leaf_label)),
_ => None,
},
GrammarNode::Leaf { .. } => None,
}
let GrammarNode::Branch { map } = self.nodes.get(node_id) else {
return None;
};
let NextNode {
next_node_id,
leaf_label,
} = map.get(&(SymbolType::Variable, typecode))?;
Some((*next_node_id, leaf_label))
}

/// Recursively clone the whole grammar tree starting from `add_from_node_id`
Expand Down Expand Up @@ -1096,65 +1084,56 @@ impl Grammar {
for &(ix, (span, ref command)) in &sref.j_commands {
use CommandToken::*;
let address = StatementAddress::new(sref.id, ix);
if let (Keyword(k), rest) = command
.split_first()
.ok_or((address, Diagnostic::BadCommand(span)))?
{
// 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] => {
let [Keyword(k), ref rest @ ..] = **command else {
return Err((address, Diagnostic::BadCommand(span)));
};
// 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,
);
}
_ => {
for ty in rest {
// 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
.iter()
.position(|t| matches!(t, Keyword(k) if k.as_ref(buf) == b"=>"))
.ok_or((address, Diagnostic::BadCommand(*k)))?; // '=>' not present in 'garden_path' command
let (prefix, shadows) = rest.split_at(split_index);
if let Err(diag) =
self.handle_common_prefixes(prefix, &shadows[1..], buf, db, names)
{
return Err((address, diag));
}
}
// Handle replacement schemes
b"type_conversions" => {
for &(from_typecode, to_typecode, label) in
&self.type_conversions.clone()
{
if let Err(diag) = self.perform_type_conversion(
from_typecode,
to_typecode,
label,
db,
) {
return Err((address, diag));
}
}
},
// Handle Ambiguous prefix commands
b"garden_path" => {
let split_index = rest
.iter()
.position(|t| matches!(t, Keyword(k) if k.as_ref(buf) == b"=>"))
.ok_or((address, Diagnostic::BadCommand(k)))?; // '=>' not present in 'garden_path' command
let (prefix, shadows) = rest.split_at(split_index);
if let Err(diag) =
self.handle_common_prefixes(prefix, &shadows[1..], buf, db, names)
{
return Err((address, diag));
}
_ => {}
}
// Handle replacement schemes
b"type_conversions" => {
for &(from_typecode, to_typecode, label) in &self.type_conversions.clone() {
self.perform_type_conversion(from_typecode, to_typecode, label, db)
.map_err(|diag| (address, diag))?;
}
}
_ => {}
}
}
}
Expand Down
Loading