]>
Witch of Git - mukan/blob - src/lib.rs
1 use dyn_clone
::{self, DynClone
};
2 use im
::{HashMap
, Vector
};
6 pub use term
::{Term
, Var
};
8 #[derive(Debug, Clone, Default)]
14 impl fmt
::Display
for Subst
{
15 fn fmt(&self, fmt
: &mut fmt
::Formatter
) -> fmt
::Result
{
16 let mut entries
= self.0.iter
();
18 if let Some((k
, v
)) = entries
.next() {
19 write
!(fmt
, "{:?}: {:?}", k
, v
)?
;
21 for (k
, v
) in entries
{
22 write
!(fmt
, ", {:?}: {:?}", k
, v
)?
;
28 impl fmt
::Display
for State
{
29 fn fmt(&self, fmt
: &mut fmt
::Formatter
) -> fmt
::Result
{
30 write
!(fmt
, "#{} {}", self.fresh
, self.subst
)
34 pub fn delay
<G
: Goal
>(thunk
: impl Clone
+ Fn() -> G
+ '
static) -> BoxedGoal
{
35 BoxedGoal
::new(move |state
: State
| thunk().search(state
))
39 pub struct BoxedGoal
{
40 inner
: Box
<dyn Goal
<Stream
= Box
<dyn Iterator
<Item
= State
>>>>,
44 fn new(goal
: impl Goal
+ Clone
+ '
static) -> Self {
46 inner
: Box
::new(BoxGoalInner(goal
)),
51 impl Goal
for BoxedGoal
{
52 type Stream
= Box
<dyn Iterator
<Item
= State
>>;
53 fn search(&self, state
: State
) -> Self::Stream
{
54 self.inner
.search(state
)
59 struct BoxGoalInner
<G
>(G
);
61 impl<G
> Goal
for BoxGoalInner
<G
>
66 type Stream
= Box
<dyn Iterator
<Item
= State
>>;
67 fn search(&self, state
: State
) -> Self::Stream
{
68 Box
::new(self.0.search(state
))
72 pub trait Goal
: DynClone
{
73 type Stream
: Iterator
<Item
= State
>;
74 fn search(&self, state
: State
) -> Self::Stream
;
77 dyn_clone
::clone_trait_object
!(Goal
<Stream
= Box
<dyn Iterator
<Item
= State
>>>);
79 pub fn call_fresh
<G
: Goal
>(block
: impl Clone
+ Fn(Var
) -> G
) -> impl Goal
+ Clone
{
80 move |mut state
: State
| {
81 let var
= Var(state
.fresh
);
83 block(var
).search(state
)
89 (() => $e
:expr
) => { $e
};
90 (($v
:ident $
(, $vs
:ident
)* $
(,)?
) => $e
:expr
) => {
91 call_fresh(move |$v
| $
crate::fresh
!(($
($vs
),*) => $e
))
97 () => { |state
: State
| std
::iter
::once(state
) };
99 ($e
:expr $
(, $es
:expr
)* $
(,)?
) => {
100 and($e
, all
!($
($es
),*))
106 () => { |state
: State
| std
::iter
::empty() };
108 ($e
:expr $
(, $es
:expr
)* $
(,)?
) => {
109 or($e
, any
!($
($es
),*))
113 pub fn eq(u
: impl Into
<Term
>, v
: impl Into
<Term
>) -> impl Goal
+ Clone
{
116 move |state
: State
| state
.un
ify
(u
.clone(), v
.clone()).into
_iter
()
119 pub fn and(u
: impl Goal
+ Clone
, v
: impl Goal
+ Clone
) -> impl Goal
+ Clone
{
120 move |state
: State
| Bind
{
128 pub fn or(u
: impl Goal
+ Clone
, v
: impl Goal
+ Clone
) -> impl Goal
+ Clone
{
129 move |state
: State
| Plus
{
130 a
: u
.search(state
.clone()),
137 pub fn new() -> Self {
141 pub fn with_vars(n
: u32) -> (Vec
<Var
>, Self) {
142 let vars
= (0..n
).map(|v
| Var(v
)).collect();
152 pub fn unify(&self, u
: Term
, v
: Term
) -> Option
<State
> {
153 self.subst
.un
ify
(u
, v
).map(|subst
| State
{
159 pub fn eval(&self, term
: Term
) -> Term
{
160 match self.subst
.walk(term
) {
161 Term
::Pair(u
, v
) => Term
::from((self.eval((*u
).clone()), self.eval((*v
).clone()))),
167 #[derive(Debug, Clone, Default)]
168 struct Subst(HashMap
<Var
, Vector
<Term
>>);
171 fn walk(&self, mut term
: Term
) -> Term
{
172 let mut subst
= self.clone();
175 Term
::Var(var
) => match subst
.0.get_mut(&var
) {
177 term
= vec
.pop_back().unwrap
();
179 subst
.0.remove(&var
);
189 fn extend(&mut self, var
: Var
, term
: Term
) {
190 self.0.entry(var
).or_default().push_back(term
);
193 fn extended(&self, var
: Var
, term
: Term
) -> Self {
194 let mut subst
= self.clone();
195 subst
.extend(var
, term
);
199 fn unify(&self, u
: Term
, v
: Term
) -> Option
<Subst
> {
200 let u
= self.walk(u
);
201 let v
= self.walk(v
);
203 (u
, v
) if u
== v
=> Some(self.clone()),
204 (Term
::Var(u
), term
) => Some(self.clone().extended(u
, term
)),
205 (term
, Term
::Var(v
)) => Some(self.clone().extended(v
, term
)),
206 (Term
::Pair(u0
, u1
), Term
::Pair(v0
, v1
)) => self
207 .un
ify
((*u0
).clone(), (*v0
).clone())
208 .and_then(|s
| s
.un
ify
((*u1
).clone(), (*v1
).clone())),
214 pub fn reify(state
: State
) -> HashMap
<Var
, Term
> {
215 let mut result
= HashMap
::new();
216 for &v
in state
.subst
.0.keys() {
217 let term
= state
.subst
.walk(Term
::Var(v
));
218 result
.insert
(v
, state
.eval(term
));
223 pub fn reify_vars(vars
: &[Var
], state
: State
) -> HashMap
<Var
, Term
> {
224 let mut result
= HashMap
::new();
226 let term
= state
.subst
.walk(Term
::Var(v
));
227 result
.insert
(v
, state
.eval(term
));
232 impl<F
, S
> Goal
for F
234 F
: Clone
+ Fn(State
) -> S
,
235 S
: Iterator
<Item
= State
>,
238 fn search(&self, state
: State
) -> S
{
257 impl<S
, R
, T
> Iterator
for Plus
<S
, R
>
259 S
: Iterator
<Item
= T
>,
260 R
: Iterator
<Item
= T
>,
264 fn next(&mut self) -> Option
<T
> {
266 Which
::A
=> match self.a
.next() {
268 self.which
= Which
::OnlyB
;
272 self.which
= Which
::B
;
276 Which
::B
=> match self.b
.next() {
278 self.which
= Which
::OnlyA
;
282 self.which
= Which
::A
;
286 Which
::OnlyA
=> match self.a
.next() {
288 self.which
= Which
::Done
;
293 Which
::OnlyB
=> match self.b
.next() {
295 self.which
= Which
::Done
;
305 struct Bind
<S
: Iterator
<Item
= State
>, R
: Goal
> {
308 current
: Option
<R
::Stream
>,
312 impl<S
, R
> Iterator
for Bind
<S
, R
>
314 S
: Iterator
<Item
= State
>,
319 fn next(&mut self) -> Option
<Self::Item
> {
323 match &mut self.current
{
325 if let Some(state
) = self.a
.next() {
326 self.current
= Some(self.b
.search(state
));
333 Some(stream
) => match stream
.next() {