More Datalog

5 files changed, 190 insertions, 73 deletions

diff --git a/crates/elfmind/src/knowledge.rs b/crates/elfmind/src/knowledge.rs
index 3b90dee..cbcce28 100644
--- a/crates/elfmind/src/knowledge.rs
+++ b/crates/elfmind/src/knowledge.rs
@@ -1,12 +1,15 @@
-use std::collections::{HashMap, HashSet};
-use itertools::Itertools;
+pub mod relation;
+pub use relation::*;
 
-use enum_map::{Enum, EnumMap};
+use crate::time::*;
+use crate::item::*;
+use crate::character::*;
 
-use crate::item::Item;
-use crate::character::Character;
+use std::collections::{HashMap, HashSet};
+use itertools::Itertools;
 
-type Time = u64;
+use enum_map::EnumMap;
+use strum::IntoDiscriminant;
 
 #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
 pub struct Var { index: u64 }
@@ -100,57 +103,6 @@ impl<T: Clone + TryFrom<Value>> Hole<T> {
     }
 }
 
-#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Enum)]
-pub enum RelationSort {
-    HasItem,
-    UsedItemAt,
-    TimeIs,
-    FriendOf,
-}
-
-#[derive(Debug, Clone, PartialEq, Eq, Hash)]
-pub enum Relation {
-    HasItem(Hole<Character>, Hole<Item>),
-    UsedItemAt(Hole<Character>, Hole<Item>, Hole<Time>),
-    TimeIs(Hole<Time>),
-    FriendOf(Hole<Character>, Hole<Character>),
-}
-impl Relation {
-    pub fn sort(&self) -> RelationSort {
-        match self {
-            Self::HasItem{..} => RelationSort::HasItem,
-            Self::UsedItemAt{..} => RelationSort::UsedItemAt,
-            Self::TimeIs{..} => RelationSort::TimeIs,
-            Self::FriendOf{..} => RelationSort::FriendOf,
-        }
-    }
-    pub fn unify(&self, other: &Self, mut u: Unification) -> Option<Unification> {
-        match (self, other) {
-            (Self::HasItem(c1, i1), Self::HasItem(c2, i2))
-              if u.unify_hole(c1, c2) && u.unify_hole(i1, i2)
-              => Some(u),
-            (Self::UsedItemAt(c1, i1, t1), Self::UsedItemAt(c2, i2, t2))
-              if u.unify_hole(c1, c2) && u.unify_hole(i1, i2) && u.unify_hole(t1, t2)
-              => Some(u),
-            (Self::TimeIs(t1), Self::TimeIs(t2))
-              if u.unify_hole(t1, t2)
-              => Some(u),
-            (Self::FriendOf(x1, y1), Self::FriendOf(x2, y2))
-              if u.unify_hole(x1, x2) && u.unify_hole(y1, y2)
-              => Some(u),
-            _ => None,
-        }
-    }
-    pub fn substitute(&self, u: &Unification) -> Self {
-        match self {
-            Self::HasItem(c, i) => Self::HasItem(c.substitute(u), i.substitute(u)),
-            Self::UsedItemAt(c, i, t) => Self::UsedItemAt(c.substitute(u), i.substitute(u), t.substitute(u)),
-            Self::TimeIs(t) => Self::TimeIs(t.substitute(u)),
-            Self::FriendOf(x, y) => Self::FriendOf(x.substitute(u), y.substitute(u)),
-        }
-    }
-}
-
 #[derive(Debug, Clone)]
 pub struct Rule {
     pub head: Relation,
@@ -169,13 +121,13 @@ impl Rule {
 
 #[derive(Debug, Default, Clone)]
 pub struct Facts {
-    facts: EnumMap<RelationSort, HashSet<Relation>>,
+    facts: EnumMap<RelationDiscriminants, HashSet<Relation>>,
 }
 impl Facts {
     pub fn add(&mut self, f: Relation) -> bool {
-        self.facts[f.sort()].insert(f)
+        self.facts[f.discriminant()].insert(f)
     }
-    pub fn with_sort(&self, s: RelationSort) -> &HashSet<Relation> {
+    pub fn with_sort(&self, s: RelationDiscriminants) -> &HashSet<Relation> {
         &self.facts[s]
     }
 }
@@ -190,7 +142,7 @@ impl Database {
     pub fn add_rule(&mut self, r: Rule) { self.rules.push(r) }
     fn apply_rule(r: &Rule, facts: &mut Facts) -> bool {
         let found: Vec<Unification> = r.body.iter()
-            .map(|r| facts.with_sort(r.sort())).multi_cartesian_product()
+            .map(|r| facts.with_sort(r.discriminant())).multi_cartesian_product()
             .filter_map(|fs| r.unify_body(&fs))
             .collect();
         let mut changed = false;
diff --git a/crates/elfmind/src/knowledge/relation.rs b/crates/elfmind/src/knowledge/relation.rs
new file mode 100644
index 0000000..754bf0f
--- /dev/null
+++ b/crates/elfmind/src/knowledge/relation.rs
@@ -0,0 +1,163 @@
+use super::{Value, Hole, Unification};
+
+use crate::time::*;
+use crate::item::*;
+use crate::character::*;
+
+use enum_map::Enum;
+use strum::EnumDiscriminants;
+
+pub trait Substitutable {
+    fn substitute(&self, u: &Unification) -> Self;
+}
+impl<A: Clone + TryFrom<Value>> Substitutable for Hole<A> {
+    fn substitute(&self, u: &Unification) -> Self {
+        match self {
+            x@Self::Var(v) => if let Some(y) = u.lookup(v) && let Ok(z) = A::try_from(y) {
+                Hole::Val(z)
+            } else {
+                x.clone()
+            }
+            x => x.clone(),
+        }
+    }
+}
+impl<
+    A: Clone + TryFrom<Value>,
+    B: Clone + TryFrom<Value>
+    > Substitutable for (Hole<A>, Hole<B>) {
+    fn substitute(&self, u: &Unification) -> Self {
+        let (a, b) = self;
+        (a.substitute(u), b.substitute(u))
+    }
+}
+impl<
+    A: Clone + TryFrom<Value>,
+    B: Clone + TryFrom<Value>,
+    C: Clone + TryFrom<Value>,
+    > Substitutable for (Hole<A>, Hole<B>, Hole<C>) {
+    fn substitute(&self, u: &Unification) -> Self {
+        let (a, b, c) = self;
+        (a.substitute(u), b.substitute(u), c.substitute(u))
+    }
+}
+impl<
+    A: Clone + TryFrom<Value>,
+    B: Clone + TryFrom<Value>,
+    C: Clone + TryFrom<Value>,
+    D: Clone + TryFrom<Value>,
+    > Substitutable for (Hole<A>, Hole<B>, Hole<C>, Hole<D>) {
+    fn substitute(&self, u: &Unification) -> Self {
+        let (a, b, c, d) = self;
+        (a.substitute(u), b.substitute(u), c.substitute(u), d.substitute(u))
+    }
+}
+impl<
+    A: Clone + TryFrom<Value>,
+    B: Clone + TryFrom<Value>,
+    C: Clone + TryFrom<Value>,
+    D: Clone + TryFrom<Value>,
+    E: Clone + TryFrom<Value>,
+    > Substitutable for (Hole<A>, Hole<B>, Hole<C>, Hole<D>, Hole<E>) {
+    fn substitute(&self, u: &Unification) -> Self {
+        let (a, b, c, d, e) = self;
+        (a.substitute(u), b.substitute(u), c.substitute(u), d.substitute(u), e.substitute(u))
+    }
+}
+
+pub trait Unifiable {
+    fn unify(&self, other: &Self, u: Unification) -> Option<Unification>;
+}
+impl<A> Unifiable for Hole<A> where
+    Value: From<A>, A: Copy, 
+{
+    fn unify(&self, other: &Self, mut u: Unification) -> Option<Unification> {
+        if u.unify_hole(self, other) {
+            Some(u)
+        } else { None }
+    }
+}
+impl<A, B> Unifiable for (Hole<A>, Hole<B>) where
+    Value: From<A>, A: Copy, 
+    Value: From<B>, B: Copy,
+{
+    fn unify(&self, other: &Self, mut u: Unification) -> Option<Unification> {
+        let (a1, b1) = self;
+        let (a2, b2) = other;
+        if u.unify_hole(a1, a2) && u.unify_hole(b1, b2) {
+            Some(u)
+        } else { None }
+    }
+}
+impl<A, B, C> Unifiable for (Hole<A>, Hole<B>, Hole<C>) where
+    Value: From<A>, A: Copy, 
+    Value: From<B>, B: Copy,
+    Value: From<C>, C: Copy,
+{
+    fn unify(&self, other: &Self, mut u: Unification) -> Option<Unification> {
+        let (a1, b1, c1) = self;
+        let (a2, b2, c2) = other;
+        if u.unify_hole(a1, a2) && u.unify_hole(b1, b2) && u.unify_hole(c1, c2) {
+            Some(u)
+        } else { None }
+    }
+}
+impl<A, B, C, D> Unifiable for (Hole<A>, Hole<B>, Hole<C>, Hole<D>) where
+    Value: From<A>, A: Copy, 
+    Value: From<B>, B: Copy,
+    Value: From<C>, C: Copy,
+    Value: From<D>, D: Copy,
+{
+    fn unify(&self, other: &Self, mut u: Unification) -> Option<Unification> {
+        let (a1, b1, c1, d1) = self;
+        let (a2, b2, c2, d2) = other;
+        if u.unify_hole(a1, a2) && u.unify_hole(b1, b2) && u.unify_hole(c1, c2) && u.unify_hole(d1, d2) {
+            Some(u)
+        } else { None }
+    }
+}
+impl<A, B, C, D, E> Unifiable for (Hole<A>, Hole<B>, Hole<C>, Hole<D>, Hole<E>) where
+    Value: From<A>, A: Copy, 
+    Value: From<B>, B: Copy,
+    Value: From<C>, C: Copy,
+    Value: From<D>, D: Copy,
+    Value: From<E>, E: Copy,
+{
+    fn unify(&self, other: &Self, mut u: Unification) -> Option<Unification> {
+        let (a1, b1, c1, d1, e1) = self;
+        let (a2, b2, c2, d2, e2) = other;
+        if u.unify_hole(a1, a2) && u.unify_hole(b1, b2) && u.unify_hole(c1, c2) && u.unify_hole(d1, d2) && u.unify_hole(e1, e2) {
+            Some(u)
+        } else { None }
+    }
+}
+
+#[derive(Debug, Clone, PartialEq, Eq, Hash, EnumDiscriminants)]
+#[strum_discriminants(derive(Enum))]
+pub enum Relation {
+    HasItem((Hole<Character>, Hole<Item>)),
+    UsedItemAt((Hole<Character>, Hole<Item>, Hole<Time>)),
+    TimeIs(Hole<Time>),
+    FriendOf((Hole<Character>, Hole<Character>)),
+}
+impl Substitutable for Relation {
+    fn substitute(&self, u: &Unification) -> Self {
+        match self {
+            Self::HasItem(x) => Self::HasItem(x.substitute(u)),
+            Self::UsedItemAt(x) => Self::UsedItemAt(x.substitute(u)),
+            Self::TimeIs(x) => Self::TimeIs(x.substitute(u)),
+            Self::FriendOf(x) => Self::FriendOf(x.substitute(u)),
+        }
+    }
+}
+impl Unifiable for Relation {
+    fn unify(&self, other: &Self, u: Unification) -> Option<Unification> {
+        match (self, other) {
+            (Self::HasItem(a), Self::HasItem(b)) => a.unify(b, u),
+            (Self::UsedItemAt(a), Self::UsedItemAt(b)) => a.unify(b, u),
+            (Self::TimeIs(a), Self::TimeIs(b)) => a.unify(b, u),
+            (Self::FriendOf(a), Self::FriendOf(b)) => a.unify(b, u),
+            _ => None,
+        }
+    }
+}
diff --git a/crates/elfmind/src/lib.rs b/crates/elfmind/src/lib.rs
index ba9eeb4..30167b4 100644
--- a/crates/elfmind/src/lib.rs
+++ b/crates/elfmind/src/lib.rs
@@ -1,3 +1,4 @@
+pub mod time;
 pub mod item;
 pub mod knowledge;
 // pub mod gadget;
diff --git a/crates/elfmind/src/main.rs b/crates/elfmind/src/main.rs
index 748ca9d..cd811f7 100644
--- a/crates/elfmind/src/main.rs
+++ b/crates/elfmind/src/main.rs
@@ -6,44 +6,44 @@ fn main() {
     let mut db = Database::default();
     db.add_fact(Relation::TimeIs(Hole::Val(6)));
     db.add_fact(Relation::TimeIs(Hole::Val(7)));
-    db.add_fact(Relation::HasItem(Hole::Val(character::Character::Tyumici), Hole::Val(item::Item::Apple)));
-    db.add_fact(Relation::FriendOf(Hole::Val(character::Character::Bobo), Hole::Val(character::Character::Naesten)));
+    db.add_fact(Relation::HasItem((Hole::Val(character::Character::Tyumici), Hole::Val(item::Item::Apple))));
+    db.add_fact(Relation::FriendOf((Hole::Val(character::Character::Bobo), Hole::Val(character::Character::Naesten))));
     let vt = ctx.var("time");
     let vi = ctx.var("item");
     db.add_rule(Rule {
-        head: Relation::UsedItemAt(
+        head: Relation::UsedItemAt((
             Hole::Val(character::Character::Tyumici),
             Hole::Var(vi),
             Hole::Var(vt),
-        ),
+        )),
         body: vec![
             Relation::TimeIs(Hole::Var(vt)),
-            Relation::HasItem(Hole::Val(character::Character::Tyumici), Hole::Var(vi)),
+            Relation::HasItem((Hole::Val(character::Character::Tyumici), Hole::Var(vi))),
         ],
     });
     let vt = ctx.var("time");
     let vc = ctx.var("char");
     db.add_rule(Rule {
-        head: Relation::FriendOf(
+        head: Relation::FriendOf((
             Hole::Val(character::Character::Naesten),
             Hole::Var(vc),
-        ),
+        )),
         body: vec![
             Relation::TimeIs(Hole::Var(vt)),
-            Relation::UsedItemAt(Hole::Var(vc), Hole::Val(item::Item::Apple), Hole::Var(vt)),
+            Relation::UsedItemAt((Hole::Var(vc), Hole::Val(item::Item::Apple), Hole::Var(vt))),
         ],
     });
     let vc1 = ctx.var("char");
     let vc2 = ctx.var("char");
     let vc3 = ctx.var("char");
     db.add_rule(Rule {
-        head: Relation::FriendOf(
+        head: Relation::FriendOf((
             Hole::Var(vc1),
             Hole::Var(vc3),
-        ),
+        )),
         body: vec![
-            Relation::FriendOf(Hole::Var(vc1), Hole::Var(vc2)),
-            Relation::FriendOf(Hole::Var(vc2), Hole::Var(vc3)),
+            Relation::FriendOf((Hole::Var(vc1), Hole::Var(vc2))),
+            Relation::FriendOf((Hole::Var(vc2), Hole::Var(vc3))),
         ],
     });
     db.apply_rules();
diff --git a/crates/elfmind/src/time.rs b/crates/elfmind/src/time.rs
new file mode 100644
index 0000000..5a98630
--- /dev/null
+++ b/crates/elfmind/src/time.rs
@@ -0,0 +1 @@
+pub type Time = u64;