Skip to content

Commit

Permalink
organizing the parts that have been done so far
Browse files Browse the repository at this point in the history
  • Loading branch information
@digama0
digama0 committed Jun 10, 2023
1 parent 4212498 commit 861ec39
Show file tree
Hide file tree
Showing 2 changed files with 114 additions and 63 deletions.
97 changes: 41 additions & 56 deletions src/defck.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,8 +35,8 @@ pub struct DefResult {
impl DefResult {
/// Returns the definition axiom for the given syntax axiom.
#[must_use]
pub fn definition_for(&self, syntax_axiom: Label) -> Option<&Label> {
self.def_map.get(&syntax_axiom)
pub fn definition_for(&self, syntax_axiom: Label) -> Option<Label> {
self.def_map.get(&syntax_axiom).copied()
}

/// Returns the list of errors that were generated during the definition check pass.
Expand All @@ -54,44 +54,30 @@ impl Database {
// Parses the 'equality', 'primitive', and 'justification' commmands in the database,
// and store the result in the database for future fast access.
fn parse_equality_commands(&self, sset: &SegmentSet, definitions: &mut DefResult) {
let nset = self.name_result();
for sref in sset.segments(..) {
let buf = &**sref.buffer;
for (_, (_, command)) in &sref.j_commands {
use CommandToken::*;
match &**command {
[Keyword(cmd), label, Keyword(from), _reflexivity_law, _commutativity_law, _transitivity_law]
[Keyword(cmd), label, Keyword(from), _reflexivity_law, _symmetry_law, _transitivity_law]
if cmd.as_ref(buf) == b"equality" && from.as_ref(buf) == b"from" =>
{
let equality = self
.name_result()
.lookup_label(label.value(buf))
.unwrap()
.atom;
let equality = nset.lookup_label(label.value(buf)).unwrap().atom;
// TODO check it's a valid equality
definitions.equalities.push(equality);
}
[Keyword(cmd), ..] if cmd.as_ref(buf) == b"primitive" => {
for label in &command[1..] {
let primitive = self
.name_result()
.lookup_label(label.value(buf))
.unwrap()
.atom;
[Keyword(cmd), rest @ ..] if cmd.as_ref(buf) == b"primitive" => {
for label in rest {
let primitive = nset.lookup_label(label.value(buf)).unwrap().atom;
definitions.primitives.push(primitive);
}
}
[Keyword(cmd), justif_label, Keyword(for_), label]
if cmd.as_ref(buf) == b"justification" && for_.as_ref(buf) == b"for" =>
{
let theorem = self
.name_result()
.lookup_label(justif_label.value(buf))
.unwrap()
.atom;
let definition = self
.name_result()
.lookup_label(label.value(buf))
.unwrap()
.atom;
let theorem = nset.lookup_label(justif_label.value(buf)).unwrap().atom;
let definition = nset.lookup_label(label.value(buf)).unwrap().atom;
definitions.justifications.insert(definition, theorem);
}
_ => {}
Expand Down Expand Up @@ -138,6 +124,8 @@ impl Database {
if pending_definitions.len() == 1 {
let syntax_axiom = pending_definitions.remove(0);

// TODO check that the justification matches the definition

// Store the validated definition
definitions.definitions.insert(definition);
definitions.def_map.insert(syntax_axiom, definition);
Expand All @@ -154,40 +142,45 @@ impl Database {
.stmt_parse_result()
.get_formula(&sref)
.ok_or_else(|| Diagnostic::UnknownLabel(sref.label_span()))?;
let equality = &fmla.get_by_path(&[]).unwrap();
if !definitions.equalities.contains(equality) {
let root = fmla.root(self);
let equality = root.label();
if !definitions.equalities.contains(&equality) {
Err(Diagnostic::DefCkNotAnEquality(
names.atom_name(*equality).into(),
names.atom_name(equality).into(),
definitions
.equalities
.iter()
.map(|label| names.atom_name(*label).into())
.map(|&label| names.atom_name(label).into())
.collect(),
))
} else {
let Some(lhs) = root.nth_child(0) else {
return Err(Diagnostic::DefCkMalformedDefinition)
};

let syntax_axiom = lhs.label();
// push the definition to the validated list early, so that later definitions
// aren't as messed up if this check fails
definitions.definitions.insert(definition);
if let Some(prev) = definitions.def_map.insert(syntax_axiom, definition) {
return Err(Diagnostic::DefCkDuplicateDefinition(
names.atom_name(syntax_axiom).into(),
names.lookup_label_by_atom(prev).address,
));
}

// Remove the definition from the pending list
let syntax_axiom = &fmla.get_by_path(&[0]).unwrap();
let result = if let Some(pending_index) =
pending_definitions.iter().position(|x| *x == *syntax_axiom)
if let Some(pending_index) =
pending_definitions.iter().position(|&x| x == syntax_axiom)
{
pending_definitions.swap_remove(pending_index);
Ok(())
} else if let Some(previous_saddr) = definitions
.definition_for(*syntax_axiom)
.map(|a| names.lookup_label_by_atom(*a).address)
{
Err(Diagnostic::DefCkDuplicateDefinition(
names.atom_name(*syntax_axiom).into(),
previous_saddr,
))
} else {
Err(Diagnostic::DefCkMalformedDefinition)
};
return Err(Diagnostic::DefCkMalformedDefinition);
}

// Store the validated definition
definitions.definitions.insert(definition);
definitions.def_map.insert(*syntax_axiom, definition);
result
// TODO definition check

Ok(())
}
}
}
Expand All @@ -198,15 +191,7 @@ impl Database {
self.parse_equality_commands(sset, definitions);
let names = self.name_result();

// Fail the whole check if no equality has been defined
#[allow(clippy::manual_assert)]
if definitions.equalities.is_empty() {
definitions
.diagnostics
.insert(StatementAddress::default(), Diagnostic::DefCkNoEquality);
}

// TODO verify that the reflexivity, associativity, and transivity laws are well-formed
// TODO verify that the reflexivity, symmetry, and transitivity laws are well-formed

let mut pending_definitions = vec![];
for sref in self
Expand Down
80 changes: 73 additions & 7 deletions src/formula.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -203,6 +203,16 @@ impl Formula {
FormulaRef { db, formula: self }
}

/// Augment a formula with a database reference, to produce a [`FormulaRef`].
/// The resulting object implements [`Display`], [`Debug`], and [`IntoIterator`].
#[must_use]
pub const fn root<'a>(&'a self, db: &'a Database) -> SubFormulaRef<'a> {
SubFormulaRef {
node_id: self.root,
f_ref: self.as_ref(db),
}
}

/// Debug only, dumps the internal structure of the formula.
pub fn dump(&self, nset: &Nameset) {
println!(" Root: {}", self.root);
Expand All @@ -223,7 +233,8 @@ impl Formula {

/// Returns the label obtained when following the given path.
/// Each element of the path gives the index of the child to retrieve.
/// For example, the empty
/// For example, the empty path gives the root, and the path `[0, 2]`
/// in `foo(bar(a, b, baz()), d)` gives `baz`.
#[must_use]
pub fn get_by_path(&self, path: &[usize]) -> Option<Label> {
let mut node_id = self.root;
Expand Down Expand Up @@ -462,7 +473,7 @@ impl<'a> Iterator for LabelIter<'a> {
}

/// A [`Formula`] reference in the context of a [`Database`].
/// This allows the values in the [`Formula`] to be resolved,
/// This allows the values in the [`Formula`] to be resolved.
#[derive(Copy, Clone)]
pub struct FormulaRef<'a> {
db: &'a Database,
Expand All @@ -478,8 +489,8 @@ impl<'a> std::ops::Deref for FormulaRef<'a> {
}

impl<'a> FormulaRef<'a> {
/// Convert the formula back to a flat list of symbols
/// This is slow and shall not normally be called except for showing a result to the user.
/// Convert the formula back to a flat list of symbols.
/// This is slow and should not normally be called except for showing a result to the user.
#[must_use]
pub(crate) fn iter(self) -> Flatten<'a> {
let mut f = Flatten {
Expand All @@ -493,7 +504,7 @@ impl<'a> FormulaRef<'a> {
}

/// Returns a copy of this formula with a new root
/// (in the same tree)
/// (in the same tree).
fn to_rerooted(self, new_root: NodeId) -> Formula {
Formula {
root: new_root,
Expand All @@ -504,7 +515,7 @@ impl<'a> FormulaRef<'a> {
}

/// Computes the typecode of the given node
/// according to the corresponding statement
/// according to the corresponding statement.
fn compute_typecode_at(&self, node_id: NodeId) -> TypeCode {
self.db.label_typecode(self.formula.tree[node_id])
}
Expand Down Expand Up @@ -652,7 +663,9 @@ impl<'a> IntoIterator for FormulaRef<'a> {
}
}

struct SubFormulaRef<'a> {
/// A reference to a subformula, usable for tree traversals.
#[derive(Copy, Clone)]
pub struct SubFormulaRef<'a> {
node_id: NodeId,
f_ref: FormulaRef<'a>,
}
Expand All @@ -679,6 +692,59 @@ impl<'a> Debug for SubFormulaRef<'a> {
}
}

impl<'a> SubFormulaRef<'a> {
/// Returns the statement label applied at this tree node.
#[must_use]
pub fn label(&self) -> Label {
self.f_ref.formula.tree[self.node_id]
}

/// Returns an iterator over the list of children of this node.
pub fn children(&self) -> SubFormulaChildren<'a> {
SubFormulaChildren {
iter: self.f_ref.formula.tree.children_iter(self.node_id),
f_ref: self.f_ref,
}
}

/// Returns the `n`th child of this node.
#[must_use]
pub fn nth_child(&self, index: usize) -> Option<Self> {
self.children().nth(index)
}

/// Returns a reference to the subtree obtained when following the given path.
/// Each element of the path gives the index of the child to retrieve.
/// For example, the empty path gives the root, and the path `[0, 2]`
/// in `foo(bar(a, b, baz(c)), d)` gives `baz(c)`.
#[must_use]
pub fn get_by_path(mut self, path: &[usize]) -> Option<Self> {
for &index in path {
self = self.nth_child(index)?;
}
Some(self)
}
}

/// An iterator over the children of a node.
#[must_use]
#[derive(Debug)]
pub struct SubFormulaChildren<'a> {
iter: SiblingIter<'a, Label>,
f_ref: FormulaRef<'a>,
}

impl<'a> Iterator for SubFormulaChildren<'a> {
type Item = SubFormulaRef<'a>;

fn next(&mut self) -> Option<Self::Item> {
Some(SubFormulaRef {
node_id: self.iter.next()?,
f_ref: self.f_ref,
})
}
}

/// An iterator going through each symbol in a formula
#[derive(Debug)]
pub struct Flatten<'a> {
Expand Down

0 comments on commit 861ec39

Please sign in to comment.