From 42771ef90d9a0e0e7075e45ae7cb4c9299c9709b Mon Sep 17 00:00:00 2001 From: Cassie Jones Date: Mon, 17 Feb 2020 12:41:24 +0100 Subject: [PATCH] Change Subst to store a single mapping for vars The previous implementation stored a Vector of values mapped, and adding new mappings shadowed previous ones. I did it like this because the implementation in the paper used association lists, which has this shadowing effect. But, the implementation in Clojure simply uses a dictionary like I'm using, and after doing these examples without seeing shadowing, I'm convinced that it has the same behavior. During this change, I also ended up changing a bunch of places with cloning to pass references instead, which should cut down on reference counting bookkeeping time. --- src/lib.rs | 98 ++++++++++++++++++++++-------------------------------- 1 file changed, 40 insertions(+), 58 deletions(-) diff --git a/src/lib.rs b/src/lib.rs index 4c84efb..fa56b55 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,5 +1,5 @@ use dyn_clone::{self, DynClone}; -use im::{HashMap, Vector}; +use im::HashMap; use std::fmt; pub mod term; @@ -11,26 +11,6 @@ pub struct State { subst: Subst, } -impl fmt::Display for Subst { - fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result { - let mut entries = self.0.iter(); - write!(fmt, "{{")?; - if let Some((k, v)) = entries.next() { - write!(fmt, "{:?}: {:?}", k, v)?; - } - for (k, v) in entries { - write!(fmt, ", {:?}: {:?}", k, v)?; - } - write!(fmt, "}}") - } -} - -impl fmt::Display for State { - fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result { - write!(fmt, "#{} {}", self.fresh, self.subst) - } -} - pub fn delay(thunk: impl Clone + Fn() -> G + 'static) -> BoxedGoal { BoxedGoal::new(move |state: State| thunk().search(state)) } @@ -113,7 +93,7 @@ macro_rules! any { pub fn eq(u: impl Into, v: impl Into) -> impl Goal + Clone { let u = u.into(); let v = v.into(); - move |state: State| state.unify(u.clone(), v.clone()).into_iter() + move |state: State| state.unify(&u, &v).into_iter() } pub fn and(u: impl Goal + Clone, v: impl Goal + Clone) -> impl Goal + Clone { @@ -149,63 +129,49 @@ impl State { ) } - pub fn unify(&self, u: Term, v: Term) -> Option { + pub fn unify(&self, u: &Term, v: &Term) -> Option { self.subst.unify(u, v).map(|subst| State { fresh: self.fresh, subst, }) } - pub fn eval(&self, term: Term) -> Term { - match self.subst.walk(term) { - Term::Pair(u, v) => Term::from((self.eval((*u).clone()), self.eval((*v).clone()))), - term => term, + pub fn eval(&self, term: &Term) -> Term { + match self.subst.walk(&term) { + Term::Pair(u, v) => Term::from((self.eval(&*u), self.eval(&*v))), + term => term.clone(), } } } #[derive(Debug, Clone, Default)] -struct Subst(HashMap>); +struct Subst(HashMap); impl Subst { - fn walk(&self, mut term: Term) -> Term { - let mut subst = self.clone(); - loop { - match term { - Term::Var(var) => match subst.0.get_mut(&var) { - Some(vec) => { - term = vec.pop_back().unwrap(); - if vec.is_empty() { - subst.0.remove(&var); - } - } - None => return term, - }, - t => return t, + fn walk<'a>(&'a self, mut term: &'a Term) -> &'a Term { + while let Term::Var(var) = term { + match self.0.get(&var) { + Some(t) => term = t, + None => break, } } - } - - fn extend(&mut self, var: Var, term: Term) { - self.0.entry(var).or_default().push_back(term); + term } fn extended(&self, var: Var, term: Term) -> Self { - let mut subst = self.clone(); - subst.extend(var, term); - subst + Subst(self.0.update(var, term)) } - fn unify(&self, u: Term, v: Term) -> Option { - let u = self.walk(u); - let v = self.walk(v); + fn unify(&self, u: &Term, v: &Term) -> Option { + let u = self.walk(&u); + let v = self.walk(&v); match (u, v) { (u, v) if u == v => Some(self.clone()), - (Term::Var(u), term) => Some(self.clone().extended(u, term)), - (term, Term::Var(v)) => Some(self.clone().extended(v, term)), + (Term::Var(u), term) => Some(self.clone().extended(*u, term.clone())), + (term, Term::Var(v)) => Some(self.clone().extended(*v, term.clone())), (Term::Pair(u0, u1), Term::Pair(v0, v1)) => self - .unify((*u0).clone(), (*v0).clone()) - .and_then(|s| s.unify((*u1).clone(), (*v1).clone())), + .unify(&*u0, &*v0) + .and_then(|s| s.unify(&*u1, &*v1)), _ => None, } } @@ -214,7 +180,8 @@ impl Subst { pub fn reify(state: State) -> HashMap { let mut result = HashMap::new(); for &v in state.subst.0.keys() { - let term = state.subst.walk(Term::Var(v)); + let var = Term::Var(v); + let term = state.subst.walk(&var); result.insert(v, state.eval(term)); } result @@ -223,7 +190,8 @@ pub fn reify(state: State) -> HashMap { pub fn reify_vars(vars: &[Var], state: State) -> HashMap { let mut result = HashMap::new(); for &v in vars { - let term = state.subst.walk(Term::Var(v)); + let var = Term::Var(v); + let term = state.subst.walk(&var); result.insert(v, state.eval(term)); } result @@ -340,3 +308,17 @@ where } } } + +impl fmt::Display for Subst { + fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result { + fmt.debug_map() + .entries(self.0.iter().map(|x| (&x.0, &x.1))) + .finish() + } +} + +impl fmt::Display for State { + fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result { + write!(fmt, "#{} {}", self.fresh, self.subst) + } +} -- 2.47.0