Commit a7087602 authored by Jeff Smits's avatar Jeff Smits

Fixed bug in term matching

parent 2d344319
......@@ -44,7 +44,7 @@ impl<'a> MutContext<'a> {
let prim_ref = self.primitives
.iter()
.flat_map(|prims| prims.get(prim_name))
.cloned() // very cheap, so whatever
.cloned() // ATermRef should be very cheap to clone
.next()
.ok_or_else(|| Error::UndefinedPrimitive(prim_name.to_owned()))?;
self.stack_tracer.borrow_mut().push(prim_name.to_owned());
......@@ -69,7 +69,7 @@ impl<'a> MutContext<'a> {
.ok_or(Error::UndefinedStrategy(strat_name.to_owned()))
}
pub fn get_term(&self, term_name: &str) -> Result<ATermRef> {
fn get_term_option(&self, term_name: &str) -> Result<Option<ATermRef>> {
self.scopes
.borrow()
.iter()
......@@ -77,36 +77,56 @@ impl<'a> MutContext<'a> {
.flat_map(|scope| scope.term.get(term_name))
.cloned()
.next()
.unwrap_or(None)
.ok_or(Error::UndefinedVariable(term_name.to_owned()))
}
pub fn get_term(&self, term_name: &str) -> Result<ATermRef> {
self.get_term_option(term_name).and_then(|o| o.ok_or(Error::UninitializedVariable))
}
pub fn match_term(&self, term_name: &str, current: &ATermRef) -> Result<()> {
match self.get_term(term_name) {
Ok(term) => {
let term = self.get_term_option(term_name)?;
match term {
Some(term) => {
if Borrow::<ATerm>::borrow(&term) == current.borrow() {
Ok(())
return Ok(())
} else {
Err(Error::StrategyFailed)
return Err(Error::StrategyFailed)
}
}
Err(Error::UndefinedVariable(_)) => {
if let Some(Some(t)) = self.scopes
.borrow_mut()
.last_mut()
.expect("Variable scope was unexpectedly empty")
.term
.insert(term_name.to_owned(), Some(current.clone())) {
unreachable!(format!("No scope had {}, but we just replaced {} when \
we added it?!",
term_name,
t))
} else {
Ok(())
None => {
for mut scope in self.scopes.borrow_mut().iter_mut().rev() {
if scope.overlay || scope.term.contains_key(term_name) {
if let Some(Some(t)) = scope.term.insert(term_name.to_owned(), Some(current.clone())) {
unreachable!(
format!("match_term: No scope had {}, but we just replaced {} when \
we added it?!", term_name, t))
} else {
return Ok(())
}
}
}
}
Err(e) => Err(e),
}
unreachable!(format!("match_term: First we could find {} unbound, then we couldn't \
anymore?!", term_name))
}
pub fn push_scope(&self, scope: Scope<ATermRef>) {
self.scopes.borrow_mut().push(scope);
}
pub fn apply_overlay(&self) {
let mut scopes = self.scopes.borrow_mut();
let overlay = scopes.pop().expect("apply_overlay: scopes stack unexpectedly empty");
if !overlay.overlay {
unreachable!("apply_overlay: Interpreter bug, scopes stack did not contain an overlay \
at the top")
}
}
pub fn pop_scope(&self) {
let _ = self.scopes.borrow_mut().pop();
}
}
......@@ -140,7 +160,7 @@ impl StackTracer {
impl fmt::Display for StackTracer {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
for (n, name) in self.stack.iter().enumerate() {
if n == self.current_depth-1 {
if n+1 == self.current_depth {
writeln!(f, "{} <==", name)?;
} else {
writeln!(f, "{}", name)?;
......@@ -154,18 +174,31 @@ impl fmt::Display for StackTracer {
pub struct Scope<ATerm> {
pub term: HashMap<String, Option<ATerm>>,
pub strategy: HashMap<String, StrategyDef>,
overlay: bool,
}
impl<ATerm> Scope<ATerm> {
pub fn from_sdefts<I>(sdefts: I) -> Scope<ATerm>
pub fn new<IA, IS>(terms:IA, defs: IS) -> Scope<ATerm>
where IA: IntoIterator<Item=(String,ATerm)>,
IS: IntoIterator<Item=(String,StrategyDef)>
{
Scope {
term: terms.into_iter().map(|(n,a)| (n,Some(a))).collect(),
strategy: defs.into_iter().collect(),
overlay: false,
}
}
pub fn from_defs<I>(defs: I) -> Scope<ATerm>
where I: IntoIterator<Item =StrategyDef>
{
Scope {
term: HashMap::default(),
strategy: sdefts
strategy: defs
.into_iter()
.map(|sdeft| (sdeft.name(), sdeft))
.collect(),
overlay: false,
}
}
......@@ -183,6 +216,15 @@ impl<ATerm> Scope<ATerm> {
result
},
strategy: HashMap::default(),
overlay: false,
}
}
pub fn overlay() -> Scope<ATerm> {
Scope {
term: HashMap::new(),
strategy: HashMap::new(),
overlay: true,
}
}
}
......@@ -16,6 +16,7 @@ pub enum Error {
UndefinedStrategy(String),
UndefinedVariable(String),
UndefinedPrimitive(String),
UninitializedVariable,
StrategyFailed,
UnknownBehaviour(&'static str),
InterpreterExit(i32),
......@@ -31,6 +32,7 @@ impl<'t> error::Error for Error {
Error::UndefinedStrategy(_) => "couldn't find strategy",
Error::UndefinedVariable(_) => "couldn't find variable",
Error::UndefinedPrimitive(_) => "couldn't find primitive",
Error::UninitializedVariable => "variable was used but not bound",
Error::StrategyFailed => "strategy failed",
Error::UnknownBehaviour(_) => "unknown behaviour",
Error::InterpreterExit(_) => "interpreter exit",
......@@ -46,6 +48,7 @@ impl<'t> error::Error for Error {
Error::UndefinedStrategy(_) => None,
Error::UndefinedVariable(_) => None,
Error::UndefinedPrimitive(_) => None,
Error::UninitializedVariable => None,
Error::StrategyFailed => None,
Error::UnknownBehaviour(_) => None,
Error::InterpreterExit(_) => None,
......@@ -63,6 +66,7 @@ impl<'t> fmt::Display for Error {
Error::UndefinedStrategy(ref s) => write!(f, "UndefinedStrategyError: {}", s),
Error::UndefinedVariable(ref s) => write!(f, "UndefinedVariableError: {}", s),
Error::UndefinedPrimitive(ref s) => write!(f, "UndefinedPrimitiveError: {}", s),
Error::UninitializedVariable => write!(f, "Uninitialized variable"),
Error::StrategyFailed => write!(f, "Strategy failed"),
Error::UnknownBehaviour(ref s) => write!(f, "Unknown behaviour for {}", s),
Error::InterpreterExit(i) => write!(f, "Interpreter exited with code {}", i),
......
......@@ -77,7 +77,7 @@ pub fn interpret<'a>(factory: &'a ATermFactory,
.map(|l| b(&l).try_into().and_then(preprocess))
.collect::<Result<_>>()?;
let context = MutContext::new(factory, libs, libraries.prims);
context.scopes.borrow_mut().push(preprocess(program)?);
context.push_scope(preprocess(program)?);
let main = context.get_strategy(strategy)?;
let result = main.eval(&context, Vec::new(), Vec::new(), input);
match result {
......@@ -105,18 +105,14 @@ impl<'a> Eval<'a> for preprocess::Strategy {
match *self {
Let(ref defs, ref body) => {
// TODO: Figure out if sdefts in let need to save a scopes-stack pointer thingy
context
.scopes
.borrow_mut()
.push(context::Scope::from_sdefts(defs.clone()));
context.push_scope(context::Scope::from_defs(defs.clone()));
// Don't unwind scopes stack when fatal error occurred? Then again, why make such a
// failure case faster at the cost of many extra branches for the happy path...
let result = body.eval(context, current);
context.scopes.borrow_mut().pop();
context.pop_scope();
result
}
CallT(ref name, ref sargs, ref targs) => {
println!("Calling {}", name);
let sdeft = context.get_strategy(name)?;
let no_of_scopes = context.scopes.borrow().len();
let sargs = sargs
......@@ -156,12 +152,9 @@ impl<'a> Eval<'a> for preprocess::Strategy {
Match(ref term) => eval_match(context, term, &current).map(|()| current),
Build(ref term) => term.build(context),
Scope(ref fresh_names, ref body) => {
context
.scopes
.borrow_mut()
.push(context::Scope::from_fresh_variables(fresh_names.clone()));
context.push_scope(context::Scope::from_fresh_variables(fresh_names.clone()));
let result = body.eval(context, current);
context.scopes.borrow_mut().pop();
context.pop_scope();
result
}
Seq(ref strat1, ref strat2) => {
......@@ -169,11 +162,20 @@ impl<'a> Eval<'a> for preprocess::Strategy {
strat2.eval(context, current)
}
GuardedLChoice(ref s_if, ref s_then, ref s_else) => {
// TODO: restore unbound variables if s_if binds some
context.push_scope(context::Scope::overlay());
match s_if.eval(context, current.clone()) {
Ok(current) => s_then.eval(context, current),
Err(Error::StrategyFailed) => s_else.eval(context, current),
Err(e) => Err(e),
Ok(current) => {
context.apply_overlay();
s_then.eval(context, current)
},
Err(Error::StrategyFailed) => {
context.pop_scope();
s_else.eval(context, current)
},
Err(e) => {
context.pop_scope();
Err(e)
},
}
}
PrimT(ref name, ref sargs, ref targs) => {
......@@ -200,7 +202,7 @@ impl<'a> Eval<'a> for preprocess::Strategy {
eval_all(strat, context, current)
},
ImportTerm(ref modname) => {
// This primitive really is interwoven with SSL like this :(
// This primitive really is interwoven with SSL :(
use primitives::ssl;
let fd = ssl::fopen(
context,
......
......@@ -35,7 +35,7 @@ pub fn preprocess(program: ctree::Module) -> Result<Scope<ATermRef>> {
// TODO: find nicer way to filter out external strategy definitions
.filter(Result::is_ok)
.collect::<Result<Vec<StrategyDef>>>()?;
Ok(Scope::from_sdefts(defs))
Ok(Scope::from_defs(defs))
}
#[derive(Debug, PartialEq, Eq, Hash, Clone)]
......@@ -67,18 +67,10 @@ impl StrategyDef {
Err(Error::UndefinedStrategy(name.clone()))
} else {
context.stack_tracer.borrow_mut().push(name.clone());
context
.scopes
.borrow_mut()
.push(Scope {
term: targs
.iter()
.cloned()
.zip(actual_targs.into_iter().map(Some))
.collect(),
strategy: sargs.iter().cloned().zip(actual_sargs).collect(),
});
context.push_scope(Scope::new(targs.iter().cloned().zip(actual_targs),
sargs.iter().cloned().zip(actual_sargs)));
let result = body.eval(context, current);
context.pop_scope();
if result.is_ok() {
context.stack_tracer.borrow_mut().pop_on_success();
} else {
......@@ -87,7 +79,7 @@ impl StrategyDef {
result
}
}
StrategyDef::Anonymous {ref argument_of, ref argument_no, ref body, no_of_scopes} => {
StrategyDef::Anonymous {ref body, no_of_scopes, ..} => {
let name = self.name();
if !(actual_sargs.is_empty() && actual_targs.is_empty()) {
Err(Error::UndefinedStrategy(name))
......
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