From 09ff5f929853cc2ba1a1ed7ddb20566cd8fe021d Mon Sep 17 00:00:00 2001 From: LLLL Colonq Date: Fri, 11 Sep 2026 15:47:34 -0400 Subject: More Datalog --- crates/elfmind/src/knowledge/relation.rs | 163 +++++++++++++++++++++++++++++++ 1 file changed, 163 insertions(+) create mode 100644 crates/elfmind/src/knowledge/relation.rs (limited to 'crates/elfmind/src/knowledge') 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> Substitutable for Hole { + 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, + B: Clone + TryFrom + > Substitutable for (Hole, Hole) { + fn substitute(&self, u: &Unification) -> Self { + let (a, b) = self; + (a.substitute(u), b.substitute(u)) + } +} +impl< + A: Clone + TryFrom, + B: Clone + TryFrom, + C: Clone + TryFrom, + > Substitutable for (Hole, Hole, Hole) { + fn substitute(&self, u: &Unification) -> Self { + let (a, b, c) = self; + (a.substitute(u), b.substitute(u), c.substitute(u)) + } +} +impl< + A: Clone + TryFrom, + B: Clone + TryFrom, + C: Clone + TryFrom, + D: Clone + TryFrom, + > Substitutable for (Hole, Hole, Hole, Hole) { + 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, + B: Clone + TryFrom, + C: Clone + TryFrom, + D: Clone + TryFrom, + E: Clone + TryFrom, + > Substitutable for (Hole, Hole, Hole, Hole, Hole) { + 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; +} +impl Unifiable for Hole where + Value: From, A: Copy, +{ + fn unify(&self, other: &Self, mut u: Unification) -> Option { + if u.unify_hole(self, other) { + Some(u) + } else { None } + } +} +impl Unifiable for (Hole, Hole) where + Value: From, A: Copy, + Value: From, B: Copy, +{ + fn unify(&self, other: &Self, mut u: Unification) -> Option { + let (a1, b1) = self; + let (a2, b2) = other; + if u.unify_hole(a1, a2) && u.unify_hole(b1, b2) { + Some(u) + } else { None } + } +} +impl Unifiable for (Hole, Hole, Hole) where + Value: From, A: Copy, + Value: From, B: Copy, + Value: From, C: Copy, +{ + fn unify(&self, other: &Self, mut u: Unification) -> Option { + 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 Unifiable for (Hole, Hole, Hole, Hole) where + Value: From, A: Copy, + Value: From, B: Copy, + Value: From, C: Copy, + Value: From, D: Copy, +{ + fn unify(&self, other: &Self, mut u: Unification) -> Option { + 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 Unifiable for (Hole, Hole, Hole, Hole, Hole) where + Value: From, A: Copy, + Value: From, B: Copy, + Value: From, C: Copy, + Value: From, D: Copy, + Value: From, E: Copy, +{ + fn unify(&self, other: &Self, mut u: Unification) -> Option { + 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, Hole)), + UsedItemAt((Hole, Hole, Hole