Skip to content

Commit

Permalink
Rename {ContextPool,LocalPool}::storage for clarity
Browse files Browse the repository at this point in the history
  • Loading branch information
bpandreotti committed Aug 11, 2023
1 parent 4d2a059 commit 9b762cc
Show file tree
Hide file tree
Showing 3 changed files with 28 additions and 30 deletions.
38 changes: 19 additions & 19 deletions carcara/src/ast/pool/advanced.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ use std::sync::{Arc, RwLock};

pub struct ContextPool {
pub(crate) global_pool: Arc<PrimitivePool>,
pub(crate) storage: Arc<RwLock<PrimitivePool>>,
pub(crate) inner: Arc<RwLock<PrimitivePool>>,
}

impl Default for ContextPool {
Expand All @@ -18,21 +18,21 @@ impl ContextPool {
pub fn new() -> Self {
Self {
global_pool: Arc::new(PrimitivePool::new()),
storage: Arc::new(RwLock::new(PrimitivePool::new())),
inner: Arc::new(RwLock::new(PrimitivePool::new())),
}
}

pub fn from_global(global_pool: &Arc<PrimitivePool>) -> Self {
Self {
global_pool: global_pool.clone(),
storage: Arc::new(RwLock::new(PrimitivePool::new())),
inner: Arc::new(RwLock::new(PrimitivePool::new())),
}
}

pub fn from_previous(ctx_pool: &Self) -> Self {
Self {
global_pool: ctx_pool.global_pool.clone(),
storage: ctx_pool.storage.clone(),
inner: ctx_pool.inner.clone(),
}
}
}
Expand All @@ -48,11 +48,11 @@ impl TermPool for ContextPool {

fn add(&mut self, term: Term) -> Rc<Term> {
// If the global pool has the term
if let Some(entry) = self.global_pool.terms.get(&term) {
if let Some(entry) = self.global_pool.storage.get(&term) {
return entry.clone();
}
let mut ctx_guard = self.storage.write().unwrap();
let term = ctx_guard.terms.add(term);
let mut ctx_guard = self.inner.write().unwrap();
let term = ctx_guard.storage.add(term);
ctx_guard.compute_sort(&term);
term
}
Expand All @@ -63,12 +63,12 @@ impl TermPool for ContextPool {
}
// A sort inserted by context
else {
self.storage.read().unwrap().sorts_cache[term].clone()
self.inner.read().unwrap().sorts_cache[term].clone()
}
}

fn free_vars(&mut self, term: &Rc<Term>) -> AHashSet<Rc<Term>> {
self.storage
self.inner
.write()
.unwrap()
.free_vars_with_priorities(term, [&self.global_pool])
Expand All @@ -79,7 +79,7 @@ impl TermPool for ContextPool {

pub struct LocalPool {
pub(crate) ctx_pool: ContextPool,
pub(crate) storage: PrimitivePool,
pub(crate) inner: PrimitivePool,
}

impl Default for LocalPool {
Expand All @@ -92,7 +92,7 @@ impl LocalPool {
pub fn new() -> Self {
Self {
ctx_pool: ContextPool::new(),
storage: PrimitivePool::new(),
inner: PrimitivePool::new(),
}
}

Expand All @@ -101,7 +101,7 @@ impl LocalPool {
pub fn from_previous(ctx_pool: &ContextPool) -> Self {
Self {
ctx_pool: ContextPool::from_previous(ctx_pool),
storage: PrimitivePool::new(),
inner: PrimitivePool::new(),
}
}
}
Expand All @@ -117,14 +117,14 @@ impl TermPool for LocalPool {

fn add(&mut self, term: Term) -> Rc<Term> {
// If there is a constant pool and has the term
if let Some(entry) = self.ctx_pool.global_pool.terms.get(&term) {
if let Some(entry) = self.ctx_pool.global_pool.storage.get(&term) {
entry.clone()
}
// If this term was inserted by the context
else if let Some(entry) = self.ctx_pool.storage.read().unwrap().terms.get(&term) {
else if let Some(entry) = self.ctx_pool.inner.read().unwrap().storage.get(&term) {
entry.clone()
} else {
self.storage.add(term)
self.inner.add(term)
}
}

Expand All @@ -133,19 +133,19 @@ impl TermPool for LocalPool {
sort.clone()
}
// A sort inserted by context
else if let Some(entry) = self.ctx_pool.storage.read().unwrap().terms.get(term) {
else if let Some(entry) = self.ctx_pool.inner.read().unwrap().storage.get(term) {
entry.clone()
} else {
self.storage.sorts_cache[term].clone()
self.inner.sorts_cache[term].clone()
}
}

fn free_vars(&mut self, term: &Rc<Term>) -> AHashSet<Rc<Term>> {
self.storage.free_vars_with_priorities(
self.inner.free_vars_with_priorities(
term,
[
&self.ctx_pool.global_pool,
&self.ctx_pool.storage.read().unwrap(),
&self.ctx_pool.inner.read().unwrap(),
],
)
}
Expand Down
18 changes: 8 additions & 10 deletions carcara/src/ast/pool/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -52,8 +52,7 @@ pub trait TermPool {
/// This struct also provides other utility methods, like computing the sort of a term (see
/// [`PrimitivePool::sort`]) or its free variables (see [`PrimitivePool::free_vars`]).
pub struct PrimitivePool {
/// A map of the terms in the pool.
pub(crate) terms: Storage,
pub(crate) storage: Storage,
pub(crate) free_vars_cache: AHashMap<Rc<Term>, AHashSet<Rc<Term>>>,
pub(crate) sorts_cache: AHashMap<Rc<Term>, Rc<Term>>,
pub(crate) bool_true: Rc<Term>,
Expand All @@ -70,19 +69,19 @@ impl PrimitivePool {
/// Constructs a new `TermPool`. This new pool will already contain the boolean constants `true`
/// and `false`, as well as the `Bool` sort.
pub fn new() -> Self {
let mut terms = Storage::new();
let mut storage = Storage::new();
let mut sorts_cache = AHashMap::new();
let bool_sort = terms.add(Term::Sort(Sort::Bool));
let bool_sort = storage.add(Term::Sort(Sort::Bool));

let [bool_true, bool_false] =
["true", "false"].map(|b| terms.add(Term::new_var(b, bool_sort.clone())));
["true", "false"].map(|b| storage.add(Term::new_var(b, bool_sort.clone())));

sorts_cache.insert(bool_false.clone(), bool_sort.clone());
sorts_cache.insert(bool_true.clone(), bool_sort.clone());
sorts_cache.insert(bool_sort.clone(), bool_sort);

Self {
terms,
storage,
free_vars_cache: AHashMap::new(),
sorts_cache,
bool_true,
Expand Down Expand Up @@ -154,7 +153,7 @@ impl PrimitivePool {
Sort::Function(result)
}
};
let sort = self.terms.add(Term::Sort(result));
let sort = self.storage.add(Term::Sort(result));
self.sorts_cache.insert(term.clone(), sort);
self.sorts_cache[term].clone()
}
Expand All @@ -166,11 +165,10 @@ impl PrimitivePool {
) -> Rc<Term> {
for p in prior_pools {
// If this prior pool has the term
if let Some(entry) = p.terms.get(&term) {
if let Some(entry) = p.storage.get(&term) {
return entry.clone();
}
}

self.add(term)
}

Expand Down Expand Up @@ -263,7 +261,7 @@ impl TermPool for PrimitivePool {
}

fn add(&mut self, term: Term) -> Rc<Term> {
let term = self.terms.add(term);
let term = self.storage.add(term);
self.compute_sort(&term);
term
}
Expand Down
2 changes: 1 addition & 1 deletion carcara/src/parser/tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -94,7 +94,7 @@ fn test_hash_consing() {
.into_iter()
.collect::<AHashSet<&str>>();

let pool_terms = pool.terms.into_vec();
let pool_terms = pool.storage.into_vec();
assert_eq!(pool_terms.len(), expected.len());
for got in pool_terms {
let formatted: &str = &format!("{}", got);
Expand Down

0 comments on commit 9b762cc

Please sign in to comment.