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.

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

Verify definitions #116

Open
wants to merge 36 commits into
base: main
Choose a base branch
from
Open
Changes from 1 commit
Commits
Show all changes
36 commits
Select commit Hold shift + click to select a range
66383c8
Add function to export theorem dependencies in GraphML format
tirix Jun 4, 2023
efd0db3
Remove unwanted file!
tirix Jun 4, 2023
2d388c2
Fix typo
tirix Jun 4, 2023
43b89d5
Skipping syntactic dependencies
tirix Jun 4, 2023
414fdd7
Definition check and definition graph export
tirix Jun 8, 2023
293fd6e
Clippy and more one more check
tirix Jun 8, 2023
5facc9d
Fmt
tirix Jun 8, 2023
91ed49f
Error handling
tirix Jun 8, 2023
bc0cd3a
Special malformed definition case
tirix Jun 8, 2023
4212498
Clppy
tirix Jun 8, 2023
7fdcbab
organizing the parts that have been done so far
digama0 Jun 10, 2023
1ce90bc
Remove unused diagnostic type
tirix Jun 11, 2023
b0e7f20
refactoring
digama0 Jun 12, 2023
4005a02
check that statements don't use pending defs
digama0 Jun 12, 2023
7e64ac3
check refl, symm, trans
digama0 Jun 12, 2023
fc812fd
Misc comments
tirix Jun 12, 2023
1dbb11a
starting on justification processing
digama0 Jun 12, 2023
eb7f27a
Mention the possible missing definition case
tirix Jun 12, 2023
ecfd2e9
Tests for the definition checker
tirix Jun 12, 2023
7a4a68c
Format
tirix Jun 12, 2023
ec62775
Oops
tirix Jun 12, 2023
8a5f967
Merge branch 'main' into verify_definitions
tirix Jun 12, 2023
d1cf04a
Typo
tirix Jun 12, 2023
b0ec8cc
add free dummy check
digama0 Jun 12, 2023
43c4f60
DV condition for justifications
digama0 Jun 13, 2023
5823b9c
parameter DV check
digama0 Jun 13, 2023
2cd7866
dummy DV check
digama0 Jun 13, 2023
c685f4f
check for definiendum on RHS
digama0 Jun 13, 2023
57a8bca
misnamed axiom/def warnings
digama0 Jun 13, 2023
aa1eae3
Merge branch 'main' into verify_definitions
tirix Jun 22, 2023
d21c13b
Merge branch 'main' into verify_definitions
tirix Jun 22, 2023
1b77b7a
Merge branch 'main' into verify_definitions
tirix Jul 2, 2023
aa4cafc
Merge branch 'main' into verify_definitions
tirix Nov 27, 2023
7011aef
Fix merge
tirix Nov 27, 2023
80490fe
Merge branch 'main' into verify_definitions
digama0 Nov 27, 2023
ca1e4af
Merge branch 'main' into verify_definitions
tirix Jun 1, 2024
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
Prev Previous commit
Next Next commit
Fmt
  • Loading branch information
tirix committed Jun 8, 2023
commit 5facc9dc871778eb231e73adf7a9196dbcf3bbaa
2 changes: 1 addition & 1 deletion src/database.rs
Original file line number Diff line number Diff line change
@@ -751,7 +751,7 @@ impl Database {
}

/// Checks all definitions soundness.
pub fn definitions_pass(&mut self)-> &Arc<DefResult> {
pub fn definitions_pass(&mut self) -> &Arc<DefResult> {
if self.definitions.is_none() {
self.stmt_parse_pass();
time(&self.options.clone(), "defck_pass", || {
109 changes: 80 additions & 29 deletions src/defck.rs
Original file line number Diff line number Diff line change
@@ -14,10 +14,10 @@
use std::collections::{HashMap, HashSet};
use std::sync::Arc;

use crate::statement::CommandToken;
use crate::{StatementType, Database, StatementRef, Label, as_str};
use crate::diag::Diagnostic;
use crate::segment_set::SegmentSet;
use crate::statement::CommandToken;
use crate::{as_str, Database, Label, StatementRef, StatementType};

/// Information related to definitions in the database.
///
@@ -39,9 +39,9 @@ impl DefResult {
}

impl Database {
// Parses the 'equality', 'primitive', and 'justification' commmands in the 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 ) {
fn parse_equality_commands(&self, sset: &SegmentSet, definitions: &mut DefResult) {
for sref in sset.segments(..) {
let buf = &**sref.buffer;
for (_, (_, command)) in &sref.j_commands {
@@ -50,26 +50,49 @@ impl Database {
[Keyword(cmd), label, Keyword(from), _reflexivity_law, _commutativity_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;
println!("Found equality {label}: {equality:?}", label = as_str(label.value(buf)), equality = equality);
let equality = self
.name_result()
.lookup_label(label.value(buf))
.unwrap()
.atom;
println!(
"Found equality {label}: {equality:?}",
label = as_str(label.value(buf)),
equality = equality
);
definitions.equalities.push(equality);
}
[Keyword(cmd), ..]
if cmd.as_ref(buf) == b"primitive" =>
{
for label in &command[1..]
{
println!("Found primitive {label:?}", label = as_str(label.value(buf)));
let primitive = self.name_result().lookup_label(label.value(buf)).unwrap().atom;
[Keyword(cmd), ..] if cmd.as_ref(buf) == b"primitive" => {
for label in &command[1..] {
println!(
"Found primitive {label:?}",
label = as_str(label.value(buf))
);
let primitive = self
.name_result()
.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" =>
{
println!("Found justification for {label:?}", label = as_str(label.value(buf)));
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;
println!(
"Found justification for {label:?}",
label = as_str(label.value(buf))
);
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;
definitions.justifications.insert(definition, theorem);
}
_ => {}
@@ -79,7 +102,11 @@ impl Database {
}

/// Verify that definitions meet set.mm/iset.mm conventions;
pub(crate) fn verify_definitions(&self, sset: &Arc<SegmentSet>, definitions : &mut DefResult) -> Result<(),Diagnostic> {
pub(crate) fn verify_definitions(
&self,
sset: &Arc<SegmentSet>,
definitions: &mut DefResult,
) -> Result<(), Diagnostic> {
self.parse_equality_commands(sset, definitions);
let names = self.name_result();

@@ -92,26 +119,38 @@ impl Database {
// TODO verify that the reflexivity, associativity, and transivity laws are well-formed

let mut pending_definitions = vec![];
for sref in self.statements().filter(|stmt| stmt.statement_type() == StatementType::Axiom) {
for sref in self
.statements()
.filter(|stmt| stmt.statement_type() == StatementType::Axiom)
{
println!("Checking {label:?}", label = as_str(sref.label()));
if names.get_atom(sref.math_at(0).slice) != self.grammar_result().provable_typecode() {
// Non-provable typecodes are syntax axioms.
// TODO Check that the axiom label does _not_ start with `df-`.
let syntax_axiom = names.lookup_label(sref.label()).ok_or_else(|| Diagnostic::UnknownLabel(sref.label_span()))?.atom;
if !definitions.primitives.contains(&syntax_axiom) {
let syntax_axiom = names
.lookup_label(sref.label())
.ok_or_else(|| Diagnostic::UnknownLabel(sref.label_span()))?
.atom;
if !definitions.primitives.contains(&syntax_axiom) {
// This syntax axiom is in need of a definition
pending_definitions.push(syntax_axiom);
}

} else if pending_definitions.is_empty() {
// No definition to check, this is a regular axiom
// TODO Check that the axiom label starts with `ax-`.
println!("Regular axiom: {label}", label = as_str(sref.label()));
} else {
println!("Definition: {label} ({count} pending)", label = as_str(sref.label()), count=pending_definitions.len());
println!(
"Definition: {label} ({count} pending)",
label = as_str(sref.label()),
count = pending_definitions.len()
);
// TODO Check that the definition label starts with `df-`.

let definition = names.lookup_label(sref.label()).ok_or_else(|| Diagnostic::UnknownLabel(sref.label_span()))?.atom;
let definition = names
.lookup_label(sref.label())
.ok_or_else(|| Diagnostic::UnknownLabel(sref.label_span()))?
.atom;
if definitions.justifications.contains_key(&definition) {
// Skip definitional check for definitions having a justification.
//
@@ -130,21 +169,32 @@ impl Database {
}
} else {
// Check that the top level of the definition is an equality
let fmla = self.stmt_parse_result().get_formula(&sref).ok_or_else(|| Diagnostic::UnknownLabel(sref.label_span()))?;
let fmla = self
.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) {
// TODO - This fails at ~ax-hilex in set.mm.
// panic!("Definition's top level syntax is {equality:?}, which is not an equality", equality=equality);
println!("Skipping {label} because it's not a definition", label = as_str(sref.label()));
println!(
"Skipping {label} because it's not a definition",
label = as_str(sref.label())
);
continue;
}

let syntax_axiom = &fmla.get_by_path(&[0]).unwrap();
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);
} else {
//panic!("Definition {label} found for unknown syntax axiom {syntax_axiom:?}", label = as_str(sref.label()));
println!("Skipping {label} because its definiendum has not been found.", label = as_str(sref.label()));
println!(
"Skipping {label} because its definiendum has not been found.",
label = as_str(sref.label())
);
}

println!("Checked {label} OK", label = as_str(sref.label()));
@@ -155,7 +205,8 @@ impl Database {
}
}
}
assert!(pending_definitions.is_empty(), "Some syntax axioms like {label:?} don't have definitions.", label = &pending_definitions[0]);
// TODO - This fails because of `~cmesy`
//assert!(pending_definitions.is_empty(), "Some syntax axioms like {label} don't have definitions.", label = as_str(self.name_result().atom_name(pending_definitions[0])));

Ok(())
}
@@ -168,4 +219,4 @@ impl Database {
self.definitions_result().definitions.contains(&label)
}
}
}
}
10 changes: 7 additions & 3 deletions src/export_deps.rs
Original file line number Diff line number Diff line change
@@ -60,7 +60,6 @@ impl Database {
})
}


/// Writes down all definition dependencies in a `GraphML` file format to the given writer.
pub fn export_graphml_defs(&mut self, out: &mut impl std::io::Write) -> Result<(), Diagnostic> {
self.definitions_pass();
@@ -82,11 +81,16 @@ impl Database {
writer.write(XmlEvent::end_element())?; // node

println!("Writing {label}", label = as_str(label));
let fmla = self.stmt_parse_result().get_formula(&sref).ok_or_else(|| Diagnostic::UnknownLabel(sref.label_span()))?;
let fmla = self
.stmt_parse_result()
.get_formula(&sref)
.ok_or_else(|| Diagnostic::UnknownLabel(sref.label_span()))?;
if let Some(definiens_fmla) = fmla.sub_formula_by_path(&[1]) {
for (syntax_axiom, is_var) in definiens_fmla.labels_iter() {
if !is_var {
if let Some(definition_axiom) = self.definitions_result().definition_for(syntax_axiom) {
if let Some(definition_axiom) =
self.definitions_result().definition_for(syntax_axiom)
{
let def_label = self.name_result().atom_name(*definition_axiom);
writer.write(
XmlEvent::start_element("edge")