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
Show file tree
Hide file tree
Changes from 24 commits
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
14 changes: 14 additions & 0 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

5 changes: 5 additions & 0 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -27,10 +27,15 @@ simple_logger = "1.13"

# Optional dependencies
dot-writer = { version = "0.1.2", optional = true }
xml-rs = { version = "0.8.14", optional = true }

[dev-dependencies]
assert_matches = "1.5"

[features]
default = ["annotate-snippets/color"]
dot = ["dot-writer"]
xml = ["xml-rs"]

[profile]

Expand Down
40 changes: 40 additions & 0 deletions src/database.rs
Original file line number Diff line number Diff line change
Expand Up @@ -98,6 +98,7 @@
//! estimated runtime. This requires an additional argument when queueing.

use crate::as_str;
use crate::defck::DefResult;
use crate::diag;
use crate::diag::Diagnostic;
use crate::export;
Expand Down Expand Up @@ -402,6 +403,7 @@ pub struct Database {
outline: Option<Arc<Outline>>,
grammar: Option<Arc<Grammar>>,
stmt_parse: Option<Arc<StmtParse>>,
definitions: Option<Arc<DefResult>>,
}

impl Default for Database {
Expand Down Expand Up @@ -432,6 +434,7 @@ impl Drop for Database {
Arc::make_mut(&mut self.segments).clear();
self.typesetting = None;
self.outline = None;
self.definitions = None;
});
}
}
Expand All @@ -455,6 +458,7 @@ impl Database {
outline: None,
grammar: None,
stmt_parse: None,
definitions: None,
prev_nameset: None,
prev_scopes: None,
prev_verify: None,
Expand Down Expand Up @@ -499,6 +503,7 @@ impl Database {
self.typesetting = None;
self.outline = None;
self.grammar = None;
self.definitions = None;
});
}

Expand Down Expand Up @@ -745,6 +750,38 @@ impl Database {
)
}

/// Checks all definitions soundness.
pub fn definitions_pass(&mut self) -> &Arc<DefResult> {
if self.definitions.is_none() {
self.stmt_parse_pass();
time(&self.options.clone(), "defck_pass", || {
let parse = self.parse_result();
let mut definitions = DefResult::default();
self.verify_definitions(parse, &mut definitions);
self.definitions = Some(Arc::new(definitions));
})
}
self.definitions_result()
}

/// Returns the results of the definition check pass.
/// Returns `None` if [`Database::definitions_pass`] was not previously called.
#[inline]
#[must_use]
pub const fn try_definitions_result(&self) -> Option<&Arc<DefResult>> {
self.definitions.as_ref()
}

/// Returns the results of the definition check pass.
/// Panics if [`Database::definition_pass`] was not previously called.
#[inline]
#[must_use]
pub fn definitions_result(&self) -> &Arc<DefResult> {
self.try_definitions_result().expect(
"The database has not run `stmt_parse_pass()`. Please ensure it is run before calling depending methods."
)
}

/// A getter method which does not build the outline.
#[inline]
#[must_use]
Expand Down Expand Up @@ -968,6 +1005,9 @@ impl Database {
if let Some(pass) = self.try_typesetting_result() {
diags.extend_from_slice(&pass.diagnostics)
}
if let Some(pass) = self.try_definitions_result() {
diags.extend(pass.diagnostics())
}
diags
}

Expand Down
Loading