From c4ee47647a5bf1a06ae88ebb9410117c927868ee Mon Sep 17 00:00:00 2001
From: LLLL Colonq <llll@colonq>
Date: Mon, 12 Oct 2026 01:31:00 -0400
Subject: Major refactor, generate relation traits with macros

---
 crates/elfmind/src/character.rs          |  21 ---
 crates/elfmind/src/item.rs               |   6 -
 crates/elfmind/src/knowledge.rs          | 187 +++++++++++----------
 crates/elfmind/src/knowledge/relation.rs | 243 +--------------------------
 crates/elfmind/src/knowledge/traits.rs   | 273 +++++++++++++++++++++++++++++++
 crates/elfmind/src/lib.rs                |   8 +-
 crates/elfmind/src/main.rs               |  49 +++---
 crates/elfmind/src/noun.rs               |  19 +++
 crates/elfmind/src/noun/character.rs     |  41 +++++
 crates/elfmind/src/noun/item.rs          |  20 +++
 crates/elfmind/src/noun/time.rs          |  16 ++
 crates/elfmind/src/time.rs               |   1 -
 12 files changed, 490 insertions(+), 394 deletions(-)
 delete mode 100644 crates/elfmind/src/character.rs
 delete mode 100644 crates/elfmind/src/item.rs
 create mode 100644 crates/elfmind/src/knowledge/traits.rs
 create mode 100644 crates/elfmind/src/noun.rs
 create mode 100644 crates/elfmind/src/noun/character.rs
 create mode 100644 crates/elfmind/src/noun/item.rs
 create mode 100644 crates/elfmind/src/noun/time.rs
 delete mode 100644 crates/elfmind/src/time.rs

(limited to 'crates/elfmind/src')

diff --git a/crates/elfmind/src/character.rs b/crates/elfmind/src/character.rs
deleted file mode 100644
index bb50605..0000000
--- a/crates/elfmind/src/character.rs
+++ /dev/null
@@ -1,21 +0,0 @@
-#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
-pub enum Character {
-    Clonk,
-    Naesten,
-    Jonze,
-    Bobo,
-    Frogrilla,
-    Hynzzy,
-    Orbital,
-    Colin,
-    Meisaka,
-    Ctrl,
-    Antlers,
-    Tyumici,
-    Steeledshield,
-    Creep,
-    Max,
-    Hostile,
-    Owlex,
-    Penguin,
-}
diff --git a/crates/elfmind/src/item.rs b/crates/elfmind/src/item.rs
deleted file mode 100644
index 5b9182d..0000000
--- a/crates/elfmind/src/item.rs
+++ /dev/null
@@ -1,6 +0,0 @@
-#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
-pub enum Item {
-    Apple,
-    BallroomKey,
-    Lumi,
-}
diff --git a/crates/elfmind/src/knowledge.rs b/crates/elfmind/src/knowledge.rs
index a610328..97ff118 100644
--- a/crates/elfmind/src/knowledge.rs
+++ b/crates/elfmind/src/knowledge.rs
@@ -1,86 +1,45 @@
-pub mod relation;
-pub use relation::*;
+pub mod traits; pub use traits::*;
+pub mod relation; pub use relation::*;
 
-use crate::time::*;
-use crate::item::*;
-use crate::character::*;
+pub use crate::noun::*;
 
 use std::collections::{HashMap, HashSet};
+use std::fmt::Display;
 use itertools::Itertools;
+use strum::IntoDiscriminant;
 
 use enum_map::EnumMap;
-use strum::IntoDiscriminant;
 
 #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
-pub struct Var { index: u64 }
-
-#[derive(Debug, Clone, Copy, PartialEq, Eq)]
-pub enum Value {
-    Var(Var),
-    Item(Item),
-    Character(Character),
-    Time(Time),
-}
-impl From<Var> for Value { fn from(x: Var) -> Self {Value::Var(x)} }
-impl From<Item> for Value { fn from(x: Item) -> Self {Value::Item(x)} }
-impl From<Character> for Value { fn from(x: Character) -> Self {Value::Character(x)} }
-impl From<Time> for Value { fn from(x: Time) -> Self {Value::Time(x)} }
-impl TryFrom<Value> for Var {
-    type Error = ();
-    fn try_from(v: Value) -> Result<Self, Self::Error> {
-        if let Value::Var(x) = v { Ok(x) } else { Err(()) }
-    }
-}
-impl TryFrom<Value> for Item {
-    type Error = ();
-    fn try_from(v: Value) -> Result<Self, Self::Error> {
-        if let Value::Item(x) = v { Ok(x) } else { Err(()) }
-    }
-}
-impl TryFrom<Value> for Character {
-    type Error = ();
-    fn try_from(v: Value) -> Result<Self, Self::Error> {
-        if let Value::Character(x) = v { Ok(x) } else { Err(()) }
-    }
-}
-impl TryFrom<Value> for Time {
-    type Error = ();
-    fn try_from(v: Value) -> Result<Self, Self::Error> {
-        if let Value::Time(x) = v { Ok(x) } else { Err(()) }
+pub struct Var(pub u64);
+impl Display for Var {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        write!(f, "v{}", self.0)
     }
 }
 
 #[derive(Debug, Default)]
 pub struct Unification {
-    assignment: HashMap<Var, Value>,
+    assignment: HashMap<Var, Noun>,
 }
 impl Unification {
-    pub fn lookup(&self, v: &Var) -> Option<Value> {
+    pub fn lookup(&self, v: &Var) -> Option<Noun> {
         self.assignment.get(v).cloned()
     }
-    pub fn add(&mut self, v: Var, x: impl Into<Value>) -> bool {
+    pub fn add(&mut self, v: Var, x: impl Into<Noun>) -> bool {
         let y = x.into();
         if let Some(old) = self.assignment.get(&v) {
-            if let Value::Var(v2) = y {
-                self.add(v2, *old)
-            } else if let Value::Var(v2) = old {
-                self.add(*v2, y)
-            } else {
-                *old == y
-            }
+            *old == y
         } else {
             self.assignment.insert(v, y);
             true
         }
     }
-    pub fn unify_hole<A, B>(&mut self, h1: &Hole<A>, h2: &Hole<B>) -> bool
-    where Value: From<A>, Value: From<B>, A: Copy, B: Copy {
-        match (h1, h2) {
-            (Hole::Var(v1), Hole::Var(v2)) =>
-                self.add(*v1, *v2) && self.add(*v2, *v1),
-            (Hole::Val(x1), Hole::Val(x2)) => Value::from(*x1) == Value::from(*x2),
-            (Hole::Var(v1), Hole::Val(x2)) => self.add(*v1, *x2),
-            (Hole::Val(x1), Hole::Var(v2)) => self.add(*v2, *x1),
+    pub fn unify_hole<A, B>(&mut self, h1: &Hole<A>, x2: &B) -> bool
+    where Noun: From<A>, Noun: From<B>, A: Copy, B: Copy {
+        match h1 {
+            Hole::Val(x1) => Noun::from(*x1) == Noun::from(*x2),
+            Hole::Var(v1) => self.add(*v1, *x2),
         }
     }
 }
@@ -90,7 +49,20 @@ pub enum Hole<T> {
     Var(Var),
     Val(T),
 }
-impl<T: Clone + TryFrom<Value>> Hole<T> {
+impl<T: std::fmt::Debug> Display for Hole<T> {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        match self {
+            Self::Var(v) => v.fmt(f),
+            Self::Val(x) => write!(f, "{:?}", x),
+        }
+    }
+}
+impl<A: std::fmt::Debug> DisplayNoun for Hole<A> {
+    fn display_noun(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        write!(f, "{}", self)
+    }
+}
+impl<T: Clone + TryFrom<Noun>> Hole<T> {
     pub fn substitute(&self, u: &Unification) -> Self {
         match self {
             x@Self::Var(v) => if let Some(y) = u.lookup(v) && let Ok(z) = T::try_from(y) {
@@ -105,8 +77,22 @@ impl<T: Clone + TryFrom<Value>> Hole<T> {
 
 #[derive(Debug, Clone)]
 pub struct Rule {
-    pub head: Relation,
-    pub body: Vec<Relation>,
+    pub head: RelationHole,
+    pub body: Vec<RelationHole>,
+}
+impl Display for Rule {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        write!(f, "{} :- ", self.head)?;
+        #[allow(unstable_name_collisions)]
+        for mb in self.body.iter().map(Some).intersperse(None) {
+            if let Some(b) = mb {
+                write!(f, "{}", b)?;
+            } else {
+                write!(f, ", ")?;
+            }
+        }
+        std::fmt::Result::Ok(())
+    }
 }
 impl Rule {
     pub fn unify_body(&self, facts: &[&Relation]) -> Option<Unification> {
@@ -117,12 +103,40 @@ impl Rule {
         }
         Some(u)
     }
+    pub fn canonize(&mut self, mut next: u64) -> u64 {
+        let mut remap = HashMap::new();
+        let mut f = |v| {
+            if let Some(new) = remap.get(&v) {
+                *new
+            } else {
+                let new = Var(next);
+                next += 1;
+                remap.insert(v, new);
+                new
+            }
+        };
+        self.head = self.head.map_variables(&mut f);
+        for b in self.body.iter_mut() {
+            *b = b.map_variables(&mut f);
+        }
+        next
+    }
 }
 
 #[derive(Debug, Default, Clone)]
 pub struct Facts {
     facts: EnumMap<RelationDiscriminants, HashSet<Relation>>,
 }
+impl Display for Facts {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        for (_, s) in self.facts.iter() {
+            for r in s.iter() {
+                write!(f, "{}.\n", r)?;
+            }
+        }
+        std::fmt::Result::Ok(())
+    }
+}
 impl Facts {
     pub fn add(&mut self, f: Relation) -> bool {
         self.facts[f.discriminant()].insert(f)
@@ -148,6 +162,15 @@ pub struct Database {
     facts: Facts,
     rules: Vec<Rule>,
 }
+impl Display for Database {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        write!(f, "{}", self.facts)?;
+        for r in self.rules.iter() {
+            write!(f, "{}.\n", r)?;
+        }
+        std::fmt::Result::Ok(())
+    }
+}
 impl Database {
     pub fn is_known(&self, r: &Relation) -> bool { self.facts.contains(r) }
     pub fn query<'a>(&'a mut self) -> Query<'a> {
@@ -176,16 +199,6 @@ impl<'a> Query<'a> {
     fn apply_rule(&self, r: &Rule, new_facts: &mut Facts, required_facts: QueryFactsToConsider) -> bool {
         // we don't need to consider every possible fact against each body term (naive evaluation)
         // instead, we can limit ourselves to the subset where at least one of the facts is new (semi-naive)
-        // let found: Vec<Unification> = r.body.iter()
-        //     .map(|r| {
-        //         let d = r.discriminant();
-        //         new_facts.with_sort(d).iter()
-        //             .chain(self.facts.with_sort(d).iter())
-        //             .chain(self.db.facts.with_sort(d).iter())
-        //     })
-        //     .multi_cartesian_product()
-        //     .filter_map(|fs| r.unify_body(&fs))
-        //     .collect();
         let mut found = Vec::new();
         // identify which slots of this rule body possibly have new facts to consider
         let changed_slots = r.body.iter()
@@ -216,8 +229,7 @@ impl<'a> Query<'a> {
                         QueryFactsToConsider::Query if i == cs =>
                              self.facts.with_sort(d).iter().chain(empty.iter()),
                         // otherwise, consider all facts - a new fact might be used alongside an unchanged fact!
-                        _ =>
-                            self.facts.with_sort(d).iter().chain(self.db.facts.with_sort(d).iter()),
+                        _ => self.facts.with_sort(d).iter().chain(self.db.facts.with_sort(d).iter()),
                     }
                 })
                 .multi_cartesian_product();
@@ -229,8 +241,10 @@ impl<'a> Query<'a> {
         }
         let mut changed = false;
         for u in found {
-            let new = r.head.substitute(&u);
-            if new.is_concrete() && !self.facts.contains(&new) && !self.db.facts.contains(&new) {
+            if let Some(new) = r.head.substitute(&u).concretize()
+                && !self.facts.contains(&new)
+                && !self.db.facts.contains(&new)
+            {
                 if new_facts.add(new) { changed = true; }
             }
         }
@@ -259,7 +273,8 @@ impl<'a> Query<'a> {
         }
         self
     }
-    pub fn rule(mut self, r: Rule) -> Self {
+    pub fn rule(mut self, mut r: Rule) -> Self {
+        r.canonize(0);
         self.rules.push(r);
         self
     }
@@ -286,21 +301,3 @@ impl<'a> Query<'a> {
         self.db.rules.extend_from_slice(&mut self.rules);
     }
 }
-
-#[derive(Debug, Default)]
-pub struct Context {
-    next_index: u64,
-    var_names: HashMap<Var, String>,
-}
-impl Context {
-    pub fn fresh(&mut self) -> Var {
-        let ret = Var { index: self.next_index };
-        self.next_index += 1;
-        ret
-    }
-    pub fn var(&mut self, nm: &str) -> Var {
-        let ret = self.fresh();
-        self.var_names.insert(ret, nm.to_owned());
-        ret
-    }
-}
diff --git a/crates/elfmind/src/knowledge/relation.rs b/crates/elfmind/src/knowledge/relation.rs
index b738aa1..82c795d 100644
--- a/crates/elfmind/src/knowledge/relation.rs
+++ b/crates/elfmind/src/knowledge/relation.rs
@@ -1,243 +1,14 @@
-use super::{Value, Hole, Unification};
-
-use crate::time::*;
-use crate::item::*;
-use crate::character::*;
+use crate::knowledge::*;
+use crate::noun::*;
 
 use enum_map::Enum;
 use strum::EnumDiscriminants;
 
-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;
-}
-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)]
+#[derive(Debug, Clone, PartialEq, Eq, Hash, EnumDiscriminants, elfmacros::Concrete)]
 #[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 Relation {
-    pub fn is_concrete(&self) -> bool {
-        match self {
-            Self::HasItem(x) => x.concretize().is_some(),
-            Self::UsedItemAt(x) => x.concretize().is_some(),
-            Self::TimeIs(x) => x.concretize().is_some(),
-            Self::FriendOf(x) => x.concretize().is_some(),
-        }
-    }
-}
-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,
-        }
-    }
+    HasItem((CharacterUnmasked, Item)),
+    UsedItemAt((CharacterUnmasked, Item, Time)),
+    TimeIs(Time),
+    FriendOf((CharacterUnmasked, CharacterUnmasked)),
 }
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 }
+    }
+}
diff --git a/crates/elfmind/src/lib.rs b/crates/elfmind/src/lib.rs
index 30167b4..21fbab6 100644
--- a/crates/elfmind/src/lib.rs
+++ b/crates/elfmind/src/lib.rs
@@ -1,6 +1,2 @@
-pub mod time;
-pub mod item;
-pub mod knowledge;
-// pub mod gadget;
-pub mod character;
-// pub mod world;
+pub mod noun; pub use noun::*;
+pub mod knowledge; pub use knowledge::*;
diff --git a/crates/elfmind/src/main.rs b/crates/elfmind/src/main.rs
index 19b8a03..e4cd4cc 100644
--- a/crates/elfmind/src/main.rs
+++ b/crates/elfmind/src/main.rs
@@ -1,51 +1,42 @@
 use elfmind::*;
-use knowledge::*;
 
 fn main() {
-    let mut ctx = Context::default();
     let mut db = Database::default();
     db.query()
-        .fact(Relation::HasItem((Hole::Val(character::Character::Tyumici), Hole::Val(item::Item::Apple))))
-        .fact(Relation::FriendOf((Hole::Val(character::Character::Bobo), Hole::Val(character::Character::Naesten))))
+        .fact(Relation::HasItem((CharacterUnmasked::Assagioli, Item::Apple)))
+        .fact(Relation::FriendOf((CharacterUnmasked::Bombieri, CharacterUnmasked::Cagliostro)))
         .learn();
-    let vt = ctx.var("time");
-    let vi = ctx.var("item");
     db.query().rule(Rule {
-        head: Relation::UsedItemAt((
-            Hole::Val(character::Character::Tyumici),
-            Hole::Var(vi),
-            Hole::Var(vt),
+        head: RelationHole::UsedItemAt((
+            Hole::Val(CharacterUnmasked::Assagioli),
+            Hole::Var(Var(0)),
+            Hole::Var(Var(1)),
         )),
         body: vec![
-            Relation::TimeIs(Hole::Var(vt)),
-            Relation::HasItem((Hole::Val(character::Character::Tyumici), Hole::Var(vi))),
+            RelationHole::TimeIs(Hole::Var(Var(1))),
+            RelationHole::HasItem((Hole::Val(CharacterUnmasked::Assagioli), Hole::Var(Var(0)))),
         ],
     }).learn();
-    let vt = ctx.var("time");
-    let vc = ctx.var("char");
     db.query().rule(Rule {
-        head: Relation::FriendOf((
-            Hole::Val(character::Character::Naesten),
-            Hole::Var(vc),
+        head: RelationHole::FriendOf((
+            Hole::Val(CharacterUnmasked::Cagliostro),
+            Hole::Var(Var(0)),
         )),
         body: vec![
-            Relation::TimeIs(Hole::Var(vt)),
-            Relation::UsedItemAt((Hole::Var(vc), Hole::Val(item::Item::Apple), Hole::Var(vt))),
+            RelationHole::TimeIs(Hole::Var(Var(1))),
+            RelationHole::UsedItemAt((Hole::Var(Var(0)), Hole::Val(Item::Apple), Hole::Var(Var(1)))),
         ],
     }).learn();
-    let vc1 = ctx.var("char");
-    let vc2 = ctx.var("char");
-    let vc3 = ctx.var("char");
     db.query().rule(Rule {
-        head: Relation::FriendOf((
-            Hole::Var(vc1),
-            Hole::Var(vc3),
+        head: RelationHole::FriendOf((
+            Hole::Var(Var(0)),
+            Hole::Var(Var(2)),
         )),
         body: vec![
-            Relation::FriendOf((Hole::Var(vc1), Hole::Var(vc2))),
-            Relation::FriendOf((Hole::Var(vc2), Hole::Var(vc3))),
+            RelationHole::FriendOf((Hole::Var(Var(0)), Hole::Var(Var(1)))),
+            RelationHole::FriendOf((Hole::Var(Var(1)), Hole::Var(Var(2)))),
         ],
     }).learn();
-    println!("{:#?}", db.query().fact(Relation::TimeIs(Hole::Val(8))).ask());
-        
+    println!("{}", db);
+    println!("{}", db.query().fact(Relation::TimeIs(8)).fact(Relation::TimeIs(9)).ask());
 }
diff --git a/crates/elfmind/src/noun.rs b/crates/elfmind/src/noun.rs
new file mode 100644
index 0000000..b09dff3
--- /dev/null
+++ b/crates/elfmind/src/noun.rs
@@ -0,0 +1,19 @@
+pub mod character; pub use character::*;
+pub mod item; pub use item::*;
+pub mod time; pub use time::*;
+
+#[derive(Debug, Clone, Copy, PartialEq, Eq)]
+pub enum Noun {
+    Item(Item),
+    CharacterUnmasked(CharacterUnmasked),
+    Time(Time),
+}
+impl std::fmt::Display for Noun {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        match self {
+            Self::Item(x) => write!(f, "{:?}", x),
+            Self::CharacterUnmasked(x) => write!(f, "{:?}", x),
+            Self::Time(x) => write!(f, "{:?}", x),
+        }
+    }
+}
diff --git a/crates/elfmind/src/noun/character.rs b/crates/elfmind/src/noun/character.rs
new file mode 100644
index 0000000..e6029c0
--- /dev/null
+++ b/crates/elfmind/src/noun/character.rs
@@ -0,0 +1,41 @@
+use crate::knowledge::*;
+
+#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
+pub enum CharacterUnmasked {
+    Assagioli,
+    Bombieri,
+    Cagliostro,
+    Divini,
+    Eustachi,
+    Fracastoro,
+    Grimaldi,
+    Human,
+}
+impl From<CharacterUnmasked> for Noun { fn from(x: CharacterUnmasked) -> Self {Noun::CharacterUnmasked(x)} }
+impl TryFrom<Noun> for CharacterUnmasked {
+    type Error = ();
+    fn try_from(v: Noun) -> Result<Self, Self::Error> {
+        if let Noun::CharacterUnmasked(x) = v { Ok(x) } else { Err(()) }
+    }
+}
+impl DisplayNoun for CharacterUnmasked {
+    fn display_noun(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        write!(f, "{:?}", self)
+    }
+}
+
+#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
+pub enum CharacterMasked {
+    Dragon,
+    Tiger,
+    Rooster,
+    Rabbit,
+    Dog,
+    Horse,
+    Monkey,
+    Ox,
+    Goat,
+    Snake,
+    Rat,
+    Pig,
+}
diff --git a/crates/elfmind/src/noun/item.rs b/crates/elfmind/src/noun/item.rs
new file mode 100644
index 0000000..8ab58d3
--- /dev/null
+++ b/crates/elfmind/src/noun/item.rs
@@ -0,0 +1,20 @@
+use crate::knowledge::*;
+
+#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
+pub enum Item {
+    Apple,
+    BallroomKey,
+    Lumi,
+}
+impl From<Item> for Noun { fn from(x: Item) -> Self {Noun::Item(x)} }
+impl TryFrom<Noun> for Item {
+    type Error = ();
+    fn try_from(v: Noun) -> Result<Self, Self::Error> {
+        if let Noun::Item(x) = v { Ok(x) } else { Err(()) }
+    }
+}
+impl DisplayNoun for Item {
+    fn display_noun(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        write!(f, "{:?}", self)
+    }
+}
diff --git a/crates/elfmind/src/noun/time.rs b/crates/elfmind/src/noun/time.rs
new file mode 100644
index 0000000..1a69da5
--- /dev/null
+++ b/crates/elfmind/src/noun/time.rs
@@ -0,0 +1,16 @@
+use crate::knowledge::*;
+
+pub type Time = u64;
+
+impl From<Time> for Noun { fn from(x: Time) -> Self {Noun::Time(x)} }
+impl TryFrom<Noun> for Time {
+    type Error = ();
+    fn try_from(v: Noun) -> Result<Self, Self::Error> {
+        if let Noun::Time(x) = v { Ok(x) } else { Err(()) }
+    }
+}
+impl DisplayNoun for Time {
+    fn display_noun(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        write!(f, "{:?}", self)
+    }
+}
diff --git a/crates/elfmind/src/time.rs b/crates/elfmind/src/time.rs
deleted file mode 100644
index 5a98630..0000000
--- a/crates/elfmind/src/time.rs
+++ /dev/null
@@ -1 +0,0 @@
-pub type Time = u64;
-- 
cgit v1.3.1