summaryrefslogtreecommitdiff
path: root/crates/elfmind/src/knowledge/traits.rs
diff options
context:
space:
mode:
Diffstat (limited to 'crates/elfmind/src/knowledge/traits.rs')
-rw-r--r--crates/elfmind/src/knowledge/traits.rs273
1 files changed, 273 insertions, 0 deletions
diff --git a/crates/elfmind/src/knowledge/traits.rs b/crates/elfmind/src/knowledge/traits.rs
new file mode 100644
index 0000000..6db9250
--- /dev/null
+++ b/crates/elfmind/src/knowledge/traits.rs
@@ -0,0 +1,273 @@
+use crate::knowledge::*;
+
+pub trait DisplayNoun {
+ fn display_noun(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result;
+}
+
+pub trait DisplayTuple {
+ fn display_tuple(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result;
+}
+impl<A: DisplayNoun> DisplayTuple for A {
+ // display any single noun as a 1-tuple
+ fn display_tuple(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+ write!(f, "(")?;
+ self.display_noun(f)?;
+ write!(f, ")")
+ }
+}
+impl<A: DisplayNoun, B: DisplayNoun> DisplayTuple for (A, B) {
+ fn display_tuple(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+ write!(f, "(")?;
+ self.0.display_noun(f)?; write!(f, ", ")?;
+ self.1.display_noun(f)?;
+ write!(f, ")")
+ }
+}
+impl<A: DisplayNoun, B: DisplayNoun, C: DisplayNoun> DisplayTuple for (A, B, C) {
+ fn display_tuple(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+ write!(f, "(")?;
+ self.0.display_noun(f)?; write!(f, ", ")?;
+ self.1.display_noun(f)?; write!(f, ", ")?;
+ self.2.display_noun(f)?;
+ write!(f, ")")
+ }
+}
+impl<A: DisplayNoun, B: DisplayNoun, C: DisplayNoun, D: DisplayNoun> DisplayTuple for (A, B, C, D) {
+ fn display_tuple(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+ write!(f, "(")?;
+ self.0.display_noun(f)?; write!(f, ", ")?;
+ self.1.display_noun(f)?; write!(f, ", ")?;
+ self.2.display_noun(f)?; write!(f, ", ")?;
+ self.3.display_noun(f)?;
+ write!(f, ")")
+ }
+}
+impl<A: DisplayNoun, B: DisplayNoun, C: DisplayNoun, D: DisplayNoun, E: DisplayNoun> DisplayTuple for (A, B, C, D, E) {
+ fn display_tuple(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+ write!(f, "(")?;
+ self.0.display_noun(f)?; write!(f, ", ")?;
+ self.1.display_noun(f)?; write!(f, ", ")?;
+ self.2.display_noun(f)?; write!(f, ", ")?;
+ self.3.display_noun(f)?; write!(f, ", ")?;
+ self.4.display_noun(f)?;
+ write!(f, ")")
+ }
+}
+
+pub trait Concretizable {
+ type Concrete;
+ fn concretize(&self) -> Option<Self::Concrete>;
+}
+impl<A: Clone> Concretizable for Hole<A> {
+ type Concrete = A;
+ fn concretize(&self) -> Option<Self::Concrete> {
+ match self {
+ Self::Val(x) => Some(x.clone()),
+ _ => None,
+ }
+ }
+}
+impl<
+ A: Clone,
+ B: Clone,
+ > Concretizable for (Hole<A>, Hole<B>) {
+ type Concrete = (A, B);
+ fn concretize(&self) -> Option<Self::Concrete> {
+ let a = self.0.concretize()?;
+ let b = self.1.concretize()?;
+ Some((a, b))
+ }
+}
+impl<
+ A: Clone,
+ B: Clone,
+ C: Clone,
+ > Concretizable for (Hole<A>, Hole<B>, Hole<C>) {
+ type Concrete = (A, B, C);
+ fn concretize(&self) -> Option<Self::Concrete> {
+ let a = self.0.concretize()?;
+ let b = self.1.concretize()?;
+ let c = self.2.concretize()?;
+ Some((a, b, c))
+ }
+}
+impl<
+ A: Clone,
+ B: Clone,
+ C: Clone,
+ D: Clone,
+ > Concretizable for (Hole<A>, Hole<B>, Hole<C>, Hole<D>) {
+ type Concrete = (A, B, C, D);
+ fn concretize(&self) -> Option<Self::Concrete> {
+ let a = self.0.concretize()?;
+ let b = self.1.concretize()?;
+ let c = self.2.concretize()?;
+ let d = self.3.concretize()?;
+ Some((a, b, c, d))
+ }
+}
+impl<
+ A: Clone,
+ B: Clone,
+ C: Clone,
+ D: Clone,
+ E: Clone,
+ > Concretizable for (Hole<A>, Hole<B>, Hole<C>, Hole<D>, Hole<E>) {
+ type Concrete = (A, B, C, D, E);
+ fn concretize(&self) -> Option<Self::Concrete> {
+ let a = self.0.concretize()?;
+ let b = self.1.concretize()?;
+ let c = self.2.concretize()?;
+ let d = self.3.concretize()?;
+ let e = self.4.concretize()?;
+ Some((a, b, c, d, e))
+ }
+}
+
+pub trait Substitutable {
+ fn substitute(&self, u: &Unification) -> Self;
+ fn map_variables<F>(&self, f: &mut F) -> Self where F: FnMut(Var) -> Var;
+}
+impl<A: Clone + TryFrom<Noun>> 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(),
+ }
+ }
+ fn map_variables<F>(&self, f: &mut F) -> Self where F: FnMut(Var) -> Var {
+ match self {
+ Self::Var(v) => Self::Var(f(*v)),
+ x => x.clone(),
+ }
+ }
+}
+impl<
+ A: Clone + TryFrom<Noun>,
+ B: Clone + TryFrom<Noun>
+ > Substitutable for (Hole<A>, Hole<B>) {
+ fn substitute(&self, u: &Unification) -> Self {
+ let (a, b) = self;
+ (a.substitute(u), b.substitute(u))
+ }
+ fn map_variables<F>(&self, f: &mut F) -> Self where F: FnMut(Var) -> Var {
+ let (a, b) = self;
+ (a.map_variables(f), b.map_variables(f))
+ }
+}
+impl<
+ A: Clone + TryFrom<Noun>,
+ B: Clone + TryFrom<Noun>,
+ C: Clone + TryFrom<Noun>,
+ > 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))
+ }
+ fn map_variables<F>(&self, f: &mut F) -> Self where F: FnMut(Var) -> Var {
+ let (a, b, c) = self;
+ (a.map_variables(f), b.map_variables(f), c.map_variables(f))
+ }
+}
+impl<
+ A: Clone + TryFrom<Noun>,
+ B: Clone + TryFrom<Noun>,
+ C: Clone + TryFrom<Noun>,
+ D: Clone + TryFrom<Noun>,
+ > 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))
+ }
+ fn map_variables<F>(&self, f: &mut F) -> Self where F: FnMut(Var) -> Var {
+ let (a, b, c, d) = self;
+ (a.map_variables(f), b.map_variables(f), c.map_variables(f), d.map_variables(f))
+ }
+}
+impl<
+ A: Clone + TryFrom<Noun>,
+ B: Clone + TryFrom<Noun>,
+ C: Clone + TryFrom<Noun>,
+ D: Clone + TryFrom<Noun>,
+ E: Clone + TryFrom<Noun>,
+ > 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))
+ }
+ fn map_variables<F>(&self, f: &mut F) -> Self where F: FnMut(Var) -> Var {
+ let (a, b, c, d, e) = self;
+ (a.map_variables(f), b.map_variables(f), c.map_variables(f), d.map_variables(f), e.map_variables(f))
+ }
+}
+
+pub trait Unifiable: Concretizable {
+ fn unify(&self, other: &Self::Concrete, u: Unification) -> Option<Unification>;
+}
+impl<A> Unifiable for Hole<A> where
+ Noun: From<A>, A: Copy,
+{
+ fn unify(&self, other: &Self::Concrete, 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
+ Noun: From<A>, A: Copy,
+ Noun: From<B>, B: Copy,
+{
+ fn unify(&self, other: &Self::Concrete, 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
+ Noun: From<A>, A: Copy,
+ Noun: From<B>, B: Copy,
+ Noun: From<C>, C: Copy,
+{
+ fn unify(&self, other: &Self::Concrete, 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
+ Noun: From<A>, A: Copy,
+ Noun: From<B>, B: Copy,
+ Noun: From<C>, C: Copy,
+ Noun: From<D>, D: Copy,
+{
+ fn unify(&self, other: &Self::Concrete, 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
+ Noun: From<A>, A: Copy,
+ Noun: From<B>, B: Copy,
+ Noun: From<C>, C: Copy,
+ Noun: From<D>, D: Copy,
+ Noun: From<E>, E: Copy,
+{
+ fn unify(&self, other: &Self::Concrete, 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 }
+ }
+}
generated by cgit v1.3.1 (git 2.54.0) at 2026-10-31 08:41:59 +0000