Commit 77392d2d authored by Jeff Smits's avatar Jeff Smits

WIP Set up offset prefetching in term match

parent 45bb8b56
...@@ -72,12 +72,8 @@ impl<'d, 'f : 'd> MutContext<'d, 'f> { ...@@ -72,12 +72,8 @@ impl<'d, 'f : 'd> MutContext<'d, 'f> {
.ok_or_else(|| Error::UndefinedStrategy(strat_name.to_owned())) .ok_or_else(|| Error::UndefinedStrategy(strat_name.to_owned()))
} }
fn get_term_option(&self, term_name: &str) -> Result<Option<ATermRef>> {
Scopes::get_term_option(&self.scopes.borrow(), term_name)
}
pub fn get_term(&self, term_name: &str) -> Result<ATermRef> { pub fn get_term(&self, term_name: &str) -> Result<ATermRef> {
self.get_term_option(term_name).and_then(|o| { Scopes::get_term_option(&self.scopes.borrow(), term_name).and_then(|(_, o)| {
o.ok_or(Error::StrategyFailed) o.ok_or(Error::StrategyFailed)
}) })
} }
...@@ -269,15 +265,20 @@ pub mod Scopes { ...@@ -269,15 +265,20 @@ pub mod Scopes {
use super::*; use super::*;
pub fn get_term_option( pub fn get_term_option(
vec: &Vec<Scope<ATermRef>>, scopes: &Vec<Scope<ATermRef>>,
term_name: &str, term_name: &str,
) -> Result<Option<ATermRef>> { ) -> Result<(usize, Option<ATermRef>)> {
vec.iter() let mut offset = None;
.rev() for (n,scope) in scopes.iter().enumerate().rev() {
.flat_map(|scope| scope.term.get(term_name)) if offset == None && scope.is_overlay {
.cloned() offset = Some(n);
.next() }
.ok_or_else(|| Error::UndefinedVariable(term_name.to_owned())) if let Some(binding) = scope.term.get(term_name) {
let n = offset.unwrap_or(n);
return Ok((n, binding.clone()))
}
}
Err(Error::UndefinedVariable(term_name.to_owned()))
} }
pub fn match_term<'a>( pub fn match_term<'a>(
...@@ -287,31 +288,23 @@ pub mod Scopes { ...@@ -287,31 +288,23 @@ pub mod Scopes {
) -> Result<()> { ) -> Result<()> {
let term = get_term_option(scopes, term_name)?; let term = get_term_option(scopes, term_name)?;
match term { match term {
Some(term) => { (_, Some(term)) => {
if Borrow::<ATerm>::borrow(&term) == current.borrow() { if Borrow::<ATerm>::borrow(&term) == current.borrow() {
return Ok(()); return Ok(());
} else { } else {
return Err(Error::StrategyFailed); return Err(Error::StrategyFailed);
} }
} }
None => { (n, None) => {
for mut scope in scopes.iter_mut().rev() { if let Some(Some(t)) = scopes[n].term.insert(term_name, Some(current.clone())) {
if scope.is_overlay || scope.term.contains_key(term_name) { unreachable!(format!(
if let Some(Some(t)) = scope.term.insert(
term_name,
Some(current.clone()),
)
{
unreachable!(format!(
"match_term: No scope had {}, but we just \ "match_term: No scope had {}, but we just \
replaced {} when we added it?!", replaced {} when we added it?!",
term_name, term_name,
t t
)) ))
} else { } else {
return Ok(()); return Ok(());
}
}
} }
} }
} }
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment