]>
Witch of Git - mukan/blob - src/lib.rs
1 use dyn_clone
::{self, DynClone
};
6 pub use term
::{Term
, Var
};
8 #[derive(Debug, Clone, Default)]
14 pub fn delay
<G
: Goal
>(thunk
: impl Clone
+ Fn() -> G
+ '
static) -> BoxedGoal
{
15 BoxedGoal
::new(move |state
: State
| thunk().search(state
))
19 pub struct BoxedGoal
{
20 inner
: Box
<dyn Goal
<Stream
= Box
<dyn Iterator
<Item
= State
>>>>,
24 fn new(goal
: impl Goal
+ Clone
+ '
static) -> Self {
26 inner
: Box
::new(BoxGoalInner(goal
)),
31 impl Goal
for BoxedGoal
{
32 type Stream
= Box
<dyn Iterator
<Item
= State
>>;
33 fn search(&self, state
: State
) -> Self::Stream
{
34 self.inner
.search(state
)
39 struct BoxGoalInner
<G
>(G
);
41 impl<G
> Goal
for BoxGoalInner
<G
>
46 type Stream
= Box
<dyn Iterator
<Item
= State
>>;
47 fn search(&self, state
: State
) -> Self::Stream
{
48 Box
::new(self.0.search(state
))
52 pub trait Goal
: DynClone
{
53 type Stream
: Iterator
<Item
= State
>;
54 fn search(&self, state
: State
) -> Self::Stream
;
57 dyn_clone
::clone_trait_object
!(Goal
<Stream
= Box
<dyn Iterator
<Item
= State
>>>);
59 pub fn call_fresh
<G
: Goal
>(block
: impl Clone
+ Fn(Var
) -> G
) -> impl Goal
+ Clone
{
60 move |mut state
: State
| {
61 let var
= Var(state
.fresh
);
63 block(var
).search(state
)
69 (() => $e
:expr
) => { $e
};
70 (($v
:ident $
(, $vs
:ident
)* $
(,)?
) => $e
:expr
) => {
71 call_fresh(move |$v
| $
crate::fresh
!(($
($vs
),*) => $e
))
77 () => { |state
: State
| std
::iter
::once(state
) };
79 ($e
:expr $
(, $es
:expr
)* $
(,)?
) => {
80 and($e
, all
!($
($es
),*))
86 () => { |state
: State
| std
::iter
::empty() };
88 ($e
:expr $
(, $es
:expr
)* $
(,)?
) => {
89 or($e
, any
!($
($es
),*))
93 pub fn eq(u
: impl Into
<Term
>, v
: impl Into
<Term
>) -> impl Goal
+ Clone
{
96 move |state
: State
| state
.un
ify
(&u
, &v
).into
_iter
()
99 pub fn and(u
: impl Goal
+ Clone
, v
: impl Goal
+ Clone
) -> impl Goal
+ Clone
{
100 move |state
: State
| Bind
{
108 pub fn or(u
: impl Goal
+ Clone
, v
: impl Goal
+ Clone
) -> impl Goal
+ Clone
{
109 move |state
: State
| Plus
{
110 a
: u
.search(state
.clone()),
117 pub fn new() -> Self {
121 pub fn with_vars(n
: u32) -> (Vec
<Var
>, Self) {
122 let vars
= (0..n
).map(|v
| Var(v
)).collect();
132 pub fn unify(&self, u
: &Term
, v
: &Term
) -> Option
<State
> {
133 self.subst
.un
ify
(u
, v
).map(|subst
| State
{
139 pub fn eval(&self, term
: &Term
) -> Term
{
140 match self.subst
.walk(&term
) {
141 Term
::Pair(u
, v
) => Term
::from((self.eval(&*u
), self.eval(&*v
))),
142 term
=> term
.clone(),
147 #[derive(Debug, Clone, Default)]
148 struct Subst(HashMap
<Var
, Term
>);
151 fn walk
<'a
>(&'a
self, mut term
: &'a Term
) -> &'a Term
{
152 while let Term
::Var(var
) = term
{
153 match self.0.get(&var
) {
161 fn extended(&self, var
: Var
, term
: Term
) -> Self {
162 Subst(self.0.update
(var
, term
))
165 fn unify(&self, u
: &Term
, v
: &Term
) -> Option
<Subst
> {
166 let u
= self.walk(&u
);
167 let v
= self.walk(&v
);
169 (u
, v
) if u
== v
=> Some(self.clone()),
170 (Term
::Var(u
), term
) => Some(self.clone().extended(*u
, term
.clone())),
171 (term
, Term
::Var(v
)) => Some(self.clone().extended(*v
, term
.clone())),
172 (Term
::Pair(u0
, u1
), Term
::Pair(v0
, v1
)) => self
174 .and_then(|s
| s
.un
ify
(&*u1
, &*v1
)),
180 pub fn reify(state
: State
) -> HashMap
<Var
, Term
> {
181 let mut result
= HashMap
::new();
182 for &v
in state
.subst
.0.keys() {
183 let var
= Term
::Var(v
);
184 let term
= state
.subst
.walk(&var
);
185 result
.insert
(v
, state
.eval(term
));
190 pub fn reify_vars(vars
: &[Var
], state
: State
) -> HashMap
<Var
, Term
> {
191 let mut result
= HashMap
::new();
193 let var
= Term
::Var(v
);
194 let term
= state
.subst
.walk(&var
);
195 result
.insert
(v
, state
.eval(term
));
200 impl<F
, S
> Goal
for F
202 F
: Clone
+ Fn(State
) -> S
,
203 S
: Iterator
<Item
= State
>,
206 fn search(&self, state
: State
) -> S
{
225 impl<S
, R
, T
> Iterator
for Plus
<S
, R
>
227 S
: Iterator
<Item
= T
>,
228 R
: Iterator
<Item
= T
>,
232 fn next(&mut self) -> Option
<T
> {
234 Which
::A
=> match self.a
.next() {
236 self.which
= Which
::OnlyB
;
240 self.which
= Which
::B
;
244 Which
::B
=> match self.b
.next() {
246 self.which
= Which
::OnlyA
;
250 self.which
= Which
::A
;
254 Which
::OnlyA
=> match self.a
.next() {
256 self.which
= Which
::Done
;
261 Which
::OnlyB
=> match self.b
.next() {
263 self.which
= Which
::Done
;
273 struct Bind
<S
: Iterator
<Item
= State
>, R
: Goal
> {
276 current
: Option
<R
::Stream
>,
280 impl<S
, R
> Iterator
for Bind
<S
, R
>
282 S
: Iterator
<Item
= State
>,
287 fn next(&mut self) -> Option
<Self::Item
> {
291 match &mut self.current
{
293 if let Some(state
) = self.a
.next() {
294 self.current
= Some(self.b
.search(state
));
301 Some(stream
) => match stream
.next() {
312 impl fmt
::Display
for Subst
{
313 fn fmt(&self, fmt
: &mut fmt
::Formatter
) -> fmt
::Result
{
315 .entries(self.0.iter
().map(|x
| (&x
.0, &x
.1)))
320 impl fmt
::Display
for State
{
321 fn fmt(&self, fmt
: &mut fmt
::Formatter
) -> fmt
::Result
{
322 write
!(fmt
, "#{} {}", self.fresh
, self.subst
)