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

Expose TermID #207

Merged
merged 3 commits into from
Aug 28, 2023
Merged

Expose TermID #207

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
e9bd5f9
Expose TermID
saulshanabrook Aug 23, 2023
683fa59
Expose usize on term ID
saulshanabrook Aug 23, 2023
42c7d6e
Remove term id wrapper struct
saulshanabrook Aug 23, 2023
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
2 changes: 1 addition & 1 deletion src/lib.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ use index::ColumnIndex;
use instant::{Duration, Instant};
pub use serialize::SerializeConfig;
use sort::*;
pub use termdag::{Term, TermDag};
pub use termdag::{Term, TermDag, TermId};
use thiserror::Error;

use proofs::ProofState;
Expand Down
18 changes: 7 additions & 11 deletions src/termdag.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,7 @@ use crate::{
Symbol,
};

#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug)]
pub struct TermId(usize);
pub type TermId = usize;

/// Like [`Expr`]s but with sharing and deduplication.
///
Expand Down Expand Up @@ -71,7 +70,7 @@ impl TermDag {
///
/// Panics if the id is not valid.
pub fn get(&self, id: TermId) -> Term {
self.nodes[id.0].clone()
self.nodes[id].clone()
}

/// Make and return a [`Term::App`] with the given head symbol and children,
Expand Down Expand Up @@ -110,7 +109,7 @@ impl TermDag {
if self.hashcons.get(node).is_none() {
let idx = self.nodes.len();
self.nodes.push(node.clone());
self.hashcons.insert(node.clone(), TermId(idx));
self.hashcons.insert(node.clone(), idx);
}
}

Expand Down Expand Up @@ -168,7 +167,7 @@ impl TermDag {
// use a stack to avoid stack overflow
let mut stack = vec![id];
while let Some(next) = stack.pop() {
match self.nodes[next.0].clone() {
match self.nodes[next].clone() {
Term::App(name, children) => {
if seen.contains(&next) {
let mut str = String::new();
Expand Down Expand Up @@ -229,11 +228,8 @@ mod tests {
vec![
Term::Var("x".into()),
Term::Var("y".into()),
Term::App("g".into(), vec![0, 1].into_iter().map(TermId).collect()),
Term::App(
"f".into(),
vec![2, 0, 1, 2].into_iter().map(TermId).collect()
),
Term::App("g".into(), vec![0, 1]),
Term::App("f".into(), vec![2, 0, 1, 2]),
]
);
let e2 = td.term_to_expr(&t);
Expand Down Expand Up @@ -261,7 +257,7 @@ mod tests {
fn test_lookup() {
let s = r#"(f (g x y) x y (g x y))"#;
let (td, t) = parse_term(s);
assert_eq!(td.lookup(&t).0, td.size() - 1);
assert_eq!(td.lookup(&t), td.size() - 1);
}

#[test]
Expand Down