mini_kanren/core/
structure.rs

1//! Logic-aware data structures
2
3use crate::core::logic_variable::{ReifiedVar, Var};
4use crate::core::substitution::Substitution;
5use crate::core::value::Value;
6use std::any::Any;
7use std::rc::Rc;
8use std::sync::Arc;
9
10/// Trait implemented by all logic-compatible types
11pub trait Structure: std::any::Any + std::fmt::Debug {
12    /// Returns `true` if `self` contains a variable that is equivalent
13    /// to `x` when considering substitution `s`.
14    fn occurs<'s>(&self, x: &Var, s: &Substitution<'s>) -> bool;
15
16    /// Attempt to unify `self` with `Value` `v` under substitution `s`.
17    fn unify<'s>(&self, v: &Value, s: Substitution<'s>) -> Option<Substitution<'s>>;
18
19    /// Recursively replace any variables contained in `self` with
20    /// their substituted values.
21    fn walk_star(self: Arc<Self>, s: &Substitution<'_>) -> Value;
22
23    /// Substitute all variables that remain fresh in `self` with reified variables.
24    fn reify_s<'s>(&self, s: Substitution<'s>) -> Substitution<'s>;
25
26    /// Cast to `Any` reference.
27    fn as_any(&self) -> &dyn Any;
28
29    /// Return `true` if `self` is equivalent to `other`.
30    fn eqv(&self, other: &Value) -> bool;
31}
32
33impl Structure for Var {
34    fn occurs<'s>(&self, x: &Var, _s: &Substitution<'s>) -> bool {
35        self == x
36    }
37
38    fn unify<'s>(&self, v: &Value, s: Substitution<'s>) -> Option<Substitution<'s>> {
39        if let Some(var) = v.try_as_var() {
40            if self == &var {
41                return Some(s);
42            }
43        }
44
45        let v = v.clone();
46        s.extend(*self, v)
47    }
48
49    fn walk_star(self: Arc<Self>, _: &Substitution<'_>) -> Value {
50        Value::var(*self)
51    }
52
53    fn reify_s<'s>(&self, s: Substitution<'s>) -> Substitution<'s> {
54        let reified = Value::new(ReifiedVar(s.n_subs()));
55        s.extend(*self, reified).unwrap()
56    }
57
58    fn as_any(&self) -> &dyn Any {
59        self
60    }
61
62    fn eqv(&self, other: &Value) -> bool {
63        other
64            .downcast_ref::<Self>()
65            .map(|v| v == self)
66            .unwrap_or(false)
67    }
68}
69
70impl Structure for ReifiedVar {
71    fn occurs<'s>(&self, _x: &Var, _s: &Substitution<'s>) -> bool {
72        false
73    }
74
75    fn unify<'s>(&self, _v: &Value, _s: Substitution<'s>) -> Option<Substitution<'s>> {
76        unimplemented!()
77    }
78
79    fn walk_star(self: Arc<Self>, _: &Substitution<'_>) -> Value {
80        Value::from_arc(self)
81    }
82
83    fn reify_s<'s>(&self, s: Substitution<'s>) -> Substitution<'s> {
84        s
85    }
86
87    fn as_any(&self) -> &dyn Any {
88        self
89    }
90
91    fn eqv(&self, other: &Value) -> bool {
92        other
93            .downcast_ref::<Self>()
94            .map(|v| v == self)
95            .unwrap_or(false)
96    }
97}
98
99impl Structure for Option<Value> {
100    fn occurs<'s>(&self, x: &Var, s: &Substitution<'s>) -> bool {
101        match self {
102            Some(v) => s.occurs(x, v),
103            None => false,
104        }
105    }
106
107    fn unify<'s>(&self, v: &Value, s: Substitution<'s>) -> Option<Substitution<'s>> {
108        let other = v.downcast_ref::<Self>()?;
109        match (self, other) {
110            (Some(su), Some(sv)) => s.unify(su, sv),
111            (None, None) => Some(s),
112            _ => None,
113        }
114    }
115
116    fn walk_star(self: Arc<Self>, s: &Substitution<'_>) -> Value {
117        match &*self {
118            None => Value::from_arc(self),
119            Some(v) => s.walk_star(v),
120        }
121    }
122
123    fn reify_s<'s>(&self, s: Substitution<'s>) -> Substitution<'s> {
124        match &*self {
125            None => s,
126            Some(v) => s.reify_s(v),
127        }
128    }
129
130    fn as_any(&self) -> &dyn Any {
131        self
132    }
133
134    fn eqv(&self, other: &Value) -> bool {
135        other
136            .downcast_ref::<Self>()
137            .map(|v| v == self)
138            .unwrap_or(false)
139    }
140}
141
142impl<T: 'static + Atomic + PartialEq> Structure for T {
143    fn occurs<'s>(&self, _x: &Var, _s: &Substitution<'s>) -> bool {
144        false
145    }
146
147    fn unify<'s>(&self, v: &Value, s: Substitution<'s>) -> Option<Substitution<'s>> {
148        if self.eqv(v) {
149            Some(s)
150        } else {
151            None
152        }
153    }
154
155    fn walk_star(self: Arc<Self>, _: &Substitution<'_>) -> Value {
156        Value::from_arc(self)
157    }
158
159    fn reify_s<'s>(&self, s: Substitution<'s>) -> Substitution<'s> {
160        s
161    }
162
163    fn as_any(&self) -> &dyn Any {
164        self
165    }
166
167    fn eqv(&self, other: &Value) -> bool {
168        other
169            .downcast_ref::<Self>()
170            .map(|o| o == self)
171            .unwrap_or(false)
172    }
173}
174
175/// Marker trait for types that contain no further values
176pub trait Atomic: std::fmt::Debug {}
177
178impl Atomic for () {}
179
180impl Atomic for bool {}
181
182impl Atomic for u8 {}
183
184impl Atomic for u16 {}
185
186impl Atomic for u32 {}
187
188impl Atomic for u64 {}
189
190impl Atomic for u128 {}
191
192impl Atomic for i8 {}
193
194impl Atomic for i16 {}
195
196impl Atomic for i32 {}
197
198impl Atomic for i64 {}
199
200impl Atomic for i128 {}
201
202impl Atomic for char {}
203
204impl Atomic for f64 {}
205
206impl Atomic for f32 {}
207
208impl Atomic for String {}
209
210impl Atomic for &str {}
211
212impl<T: Atomic> Atomic for Option<T> {}
213impl<T: Atomic> Atomic for Box<T> {}
214impl<T: Atomic> Atomic for Arc<T> {}
215impl<T: Atomic> Atomic for Rc<T> {}
mini_kanren/core/structure.rs

mini_kanren/core/
structure.rs
