From df7ab0a6f091391bd693890f505f6a1694e2fe91 Mon Sep 17 00:00:00 2001 From: Cassie Jones Date: Mon, 17 Feb 2020 00:06:21 +0100 Subject: [PATCH] What a horrible night to have an initial commit This implements MicroKanren in Rust, based on the original paper: http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf It's also informative to look at the "microLogic" implementation in Clojure, which inspired the slightly cleaner unification style and provides some ideas for what the extension points might need to be in the future: https://mullr.github.io/micrologic/literate.html This implementation is based around a "goal" trait, which can be asked to search for solutions in a given state, producing a stream of new states. Unlike the implementations above, we use Rust's Iterator trait to implement the state streams. This might need to change in order to enable "unproductive" steps in searching to be interleaved with other searches. Potentially we should just change the iterator to use Iterator where Step values are Pending or Sat(State). Goal is implemented for F: Fn(State) -> impl Iterator, which means that you can write searches with functions. A goal that wants to prove "true" would look like: |state: State| std::iter::once(state) and a goal to prove "false" would look like: |state: State| std::iter::empty() The functions and() and or() construct larger goals out of their sub-goals, although they have more complicated implementations in order to provide somewhat fair search. The and() goal constructor currently doesn't produce a fair search, because if the second goal ever produces infinite streams, then the first goal won't get a chance to advance. This can be fixed, although it will involve allocation. The delay() constructor is needed in order to produce recursive procedures. It takes a thunk that produces a goal, and invokes it only when it's first searched. Without this, recursive goals would continually construct larger and larger goals forever. The Rust implementation needs an additional consideration here: we have to box the output Goal type. Most of the goal constructors return `impl Goal` which gives an opaque type that incorporates its contents, including its code. If you wrote a recursive procedure which directly incorporated itself without a box in-between, it would have to have a type which contained its own type, which means an infinite type. This boxing issue is also what ended up complicating the Clone code. Goals often need to be cloned, because they need to be able to be used again and again during search, repeatedly constructing the derived goals, but if we want a boxed goal that obscures the specific type, then we needed to use `Box`, and so since Clone trait isn't object-safe, it can't be used as a bound on Goal, and thus we need `Goal: DynClone` so that the `Box` can implement Clone, and also we need a to write Goal + Clone in lots of places because we need both bounds. Some of the constructors use Into in order to make writing programs with the terms more convenient. Tuples become pair terms, integers become literal terms, and variables are wrapped. --- .gitignore | 1 + Cargo.lock | 75 ++++++++++ Cargo.toml | 11 ++ src/lib.rs | 399 ++++++++++++++++++++++++++++++++++++++++++++++++++++ src/main.rs | 91 ++++++++++++ 5 files changed, 577 insertions(+) create mode 100644 .gitignore create mode 100644 Cargo.lock create mode 100644 Cargo.toml create mode 100644 src/lib.rs create mode 100644 src/main.rs diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..ea8c4bf --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +/target diff --git a/Cargo.lock b/Cargo.lock new file mode 100644 index 0000000..5714bfb --- /dev/null +++ b/Cargo.lock @@ -0,0 +1,75 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +[[package]] +name = "bitmaps" +version = "2.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "81e039a80914325b37fde728ef7693c212f0ac913d5599607d7b95a9484aae0b" +dependencies = [ + "typenum", +] + +[[package]] +name = "dyn-clone" +version = "1.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b3ec9c7fb9a2ce708751c98e31ccbae74b6ab194f5c8e30cfb7ed62e38b70866" + +[[package]] +name = "im" +version = "14.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e302bf26ba21de289e808230f80fe799fd371268d853783ee7f844c7cb5704b7" +dependencies = [ + "bitmaps", + "rand_core", + "rand_xoshiro", + "sized-chunks", + "typenum", + "version_check", +] + +[[package]] +name = "mukan" +version = "0.1.0" +dependencies = [ + "dyn-clone", + "im", +] + +[[package]] +name = "rand_core" +version = "0.5.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "90bde5296fc891b0cef12a6d03ddccc162ce7b2aff54160af9338f8d40df6d19" + +[[package]] +name = "rand_xoshiro" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a9fcdd2e881d02f1d9390ae47ad8e5696a9e4be7b547a1da2afbc61973217004" +dependencies = [ + "rand_core", +] + +[[package]] +name = "sized-chunks" +version = "0.5.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6f59f81ec9833a580d2448e958d16bd872637798f3ab300b693c48f136fb76ff" +dependencies = [ + "bitmaps", + "typenum", +] + +[[package]] +name = "typenum" +version = "1.11.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6d2783fe2d6b8c1101136184eb41be8b1ad379e4657050b8aaff0c79ee7575f9" + +[[package]] +name = "version_check" +version = "0.9.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "078775d0255232fb988e6fccf26ddc9d1ac274299aaedcedce21c6f72cc533ce" diff --git a/Cargo.toml b/Cargo.toml new file mode 100644 index 0000000..0c638f3 --- /dev/null +++ b/Cargo.toml @@ -0,0 +1,11 @@ +[package] +name = "mukan" +version = "0.1.0" +authors = ["Cassie Jones "] +edition = "2018" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] +im = "14.2" +dyn-clone = "1.0" diff --git a/src/lib.rs b/src/lib.rs new file mode 100644 index 0000000..ad587d1 --- /dev/null +++ b/src/lib.rs @@ -0,0 +1,399 @@ +use dyn_clone::{self, DynClone}; +use im::{HashMap, Vector}; +use std::{fmt, sync::Arc}; + +#[derive(Clone, Copy, PartialEq, Eq, Hash)] +pub struct Var(u32); + +#[derive(Clone, PartialEq)] +pub enum Term { + Var(Var), + Pair(Arc, Arc), + Lit(i32), +} + +impl From<&Term> for Term { + fn from(term: &Term) -> Term { + term.clone() + } +} + +impl From for Term { + fn from(i: i32) -> Term { + Term::Lit(i) + } +} + +impl From for Term { + fn from(var: Var) -> Term { + Term::Var(var) + } +} + +impl fmt::Display for Term { + fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result { + match self { + Term::Var(v) => write!(fmt, "{:?}", v), + Term::Pair(l, r) => write!(fmt, "({}, {})", *l, *r), + Term::Lit(i) => write!(fmt, "{}", i), + } + } +} + +impl fmt::Debug for Term { + fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result { + write!(fmt, "{}", self) + } +} + +impl fmt::Debug for Var { + fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result { + write!(fmt, "x{}", self.0) + } +} + +impl From<(T, U)> for Term +where + T: Into, + U: Into, +{ + fn from((t, u): (T, U)) -> Term { + Term::Pair(Arc::new(t.into()), Arc::new(u.into())) + } +} + +#[derive(Debug, Clone, Default)] +pub struct State { + fresh: u32, + 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)) +} + +#[derive(Clone)] +pub struct BoxedGoal { + inner: Box>>>, +} + +impl BoxedGoal { + fn new(goal: impl Goal + Clone + 'static) -> Self { + BoxedGoal { + inner: Box::new(BoxGoalInner(goal)), + } + } +} + +impl Goal for BoxedGoal { + type Stream = Box>; + fn search(&self, state: State) -> Self::Stream { + self.inner.search(state) + } +} + +#[derive(Clone)] +struct BoxGoalInner(G); + +impl Goal for BoxGoalInner +where + G: Goal + Clone, + G::Stream: 'static, +{ + type Stream = Box>; + fn search(&self, state: State) -> Self::Stream { + Box::new(self.0.search(state)) + } +} + +pub trait Goal: DynClone { + type Stream: Iterator; + fn search(&self, state: State) -> Self::Stream; +} + +dyn_clone::clone_trait_object!(Goal>>); + +pub fn call_fresh(block: impl Clone + Fn(Var) -> G) -> impl Goal + Clone { + move |mut state: State| { + let var = Var(state.fresh); + state.fresh += 1; + block(var).search(state) + } +} + +#[macro_export] +macro_rules! fresh { + (() => $e:expr) => { $e }; + (($v:ident $(, $vs:ident)* $(,)?) => $e:expr) => { + call_fresh(move |$v| $crate::fresh!(($($vs),*) => $e)) + }; +} + +#[macro_export] +macro_rules! all { + () => { |state: State| std::iter::once(state) }; + ($e:expr) => { $e }; + ($e:expr $(, $es:expr)* $(,)?) => { + and($e, all!($($es),*)) + } +} + +#[macro_export] +macro_rules! any { + () => { |state: State| std::iter::empty() }; + ($e:expr) => { $e }; + ($e:expr $(, $es:expr)* $(,)?) => { + or($e, any!($($es),*)) + } +} + +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() +} + +pub fn and(u: impl Goal + Clone, v: impl Goal + Clone) -> impl Goal + Clone { + move |state: State| Bind { + a: u.search(state), + b: v.clone(), + current: None, + done: false, + } +} + +pub fn or(u: impl Goal + Clone, v: impl Goal + Clone) -> impl Goal + Clone { + move |state: State| Plus { + a: u.search(state.clone()), + b: v.search(state), + which: Which::A, + } +} + +impl State { + pub fn new() -> Self { + Self::default() + } + + pub fn with_vars(n: u32) -> (Vec, Self) { + let vars = (0..n).map(|v| Var(v)).collect(); + ( + vars, + Self { + fresh: n + 1, + ..Default::default() + }, + ) + } + + 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, + } + } +} + +#[derive(Debug, Clone, Default)] +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 extend(&mut self, var: Var, term: Term) { + self.0.entry(var).or_default().push_back(term); + } + + fn extended(&self, var: Var, term: Term) -> Self { + let mut subst = self.clone(); + subst.extend(var, term); + subst + } + + 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::Pair(u0, u1), Term::Pair(v0, v1)) => self + .unify((*u0).clone(), (*v0).clone()) + .and_then(|s| s.unify((*u1).clone(), (*v1).clone())), + _ => None, + } + } +} + +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)); + result.insert(v, state.eval(term)); + } + result +} + +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)); + result.insert(v, state.eval(term)); + } + result +} + +impl Goal for F +where + F: Clone + Fn(State) -> S, + S: Iterator, +{ + type Stream = S; + fn search(&self, state: State) -> S { + self(state) + } +} + +enum Which { + A, + B, + OnlyA, + OnlyB, + Done, +} + +struct Plus { + a: S, + b: R, + which: Which, +} + +impl Iterator for Plus +where + S: Iterator, + R: Iterator, + T: fmt::Display, +{ + type Item = T; + fn next(&mut self) -> Option { + match self.which { + Which::A => match self.a.next() { + None => { + self.which = Which::OnlyB; + self.next() + } + item => { + self.which = Which::B; + item + } + }, + Which::B => match self.b.next() { + None => { + self.which = Which::OnlyA; + self.next() + } + item => { + self.which = Which::A; + item + } + }, + Which::OnlyA => match self.a.next() { + None => { + self.which = Which::Done; + None + } + item => item, + }, + Which::OnlyB => match self.b.next() { + None => { + self.which = Which::Done; + None + } + item => item, + }, + Which::Done => None, + } + } +} + +struct Bind, R: Goal> { + a: S, + b: R, + current: Option, + done: bool, +} + +impl Iterator for Bind +where + S: Iterator, + R: Goal, +{ + type Item = State; + + fn next(&mut self) -> Option { + if self.done { + return None; + } + match &mut self.current { + None => { + if let Some(state) = self.a.next() { + self.current = Some(self.b.search(state)); + self.next() + } else { + self.done = true; + None + } + } + Some(stream) => match stream.next() { + None => { + self.current = None; + self.next() + } + item => item, + }, + } + } +} diff --git a/src/main.rs b/src/main.rs new file mode 100644 index 0000000..190cb77 --- /dev/null +++ b/src/main.rs @@ -0,0 +1,91 @@ +use mukan::{all, and, call_fresh, delay, eq, fresh, or, reify, reify_vars, Goal, State, Term}; + +fn main() { + println!("Part 1"); + let term = call_fresh(|a| call_fresh(move |b| or(and(eq(a, b), eq(a, 1)), eq(b, 2)))); + for soln in term.search(State::new()) { + println!("{:?}", reify(soln)); + } + + println!("Part 2"); + let term = fresh!((p, a, b, c, d) => { + all! { + eq(p, (a, b)), + eq((a, b), (c, d)), + eq((a, b), (b, c)), + eq(d, 413), + } + }); + for soln in term.search(State::new()) { + println!("{:?}", reify(soln)); + } + + println!("Part 3"); + let term = fresh!((a, b) => eq(a, b)); + for soln in term.search(State::new()) { + println!("{:?}", reify(soln)); + } + + println!("Peano"); + fn peano(n: impl Into) -> impl Goal + Clone { + let n = n.into(); + or( + eq(n.clone(), 0), + fresh!((r) => and(eq(n.clone(), (1, r)), delay(move || peano(r)))), + ) + } + let term = fresh!((n) => peano(n)); + for soln in term.search(State::new()).take(5) { + println!("{:?}", reify(soln)); + } + + fn make_nat(n: u32) -> Term { + if n == 0 { + 0.into() + } else { + (1, make_nat(n - 1)).into() + } + } + + fn less(n: impl Into, m: impl Into) -> impl Goal + Clone { + let n = n.into(); + let m = m.into(); + or( + eq((1, n.clone()), m.clone()), + fresh!((x) => all! { + eq(m.clone(), (1, x)), + { + let n = n.clone(); + delay(move || less(n.clone(), x.clone())) + } + }), + ) + } + + fn sums_to(n: impl Into, m: impl Into, s: impl Into) -> impl Goal + Clone { + let n = n.into(); + let m = m.into(); + let s = s.into(); + or( + and(eq(n.clone(), 0), eq(m.clone(), s.clone())), + fresh!((x) => all! { + eq(n.clone(), (1, x)), + { + let m = m.clone(); + let s = s.clone(); + delay(move || all! { + less(m.clone(), s.clone()), + sums_to(x, (1, m.clone()), s.clone()), + }) + } + }), + ) + } + + println!("Peano addition!"); + let (vars, state) = State::with_vars(2); + let term = sums_to(vars[0], vars[1], make_nat(10)); + for soln in term.search(state) { + println!("= {:?}", reify_vars(&vars, soln)); + } +} -- 2.47.0