1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104

use crate::domains::DomainType;
use crate::state::State;
use std::fmt::Debug;
use std::rc::Rc;

/** How compatible values are matched with each other.

See
[Unification](https://en.wikipedia.org/wiki/Unification_(computer_science))
for a formal and probably more correct definition. This will attempt to
describe unification as implemented (and understood by the author).

The simplest example of unification looks like equality or variable
assignment. In `x=1`, if the variable `x` is unbound, the statement succeeds
and `x` is considered equal to `1`. `1=1` is also valid, though slightly
silly. Unification does not care about direction, so `1=x` is equally valid
and has the same effect.

A follow-up assertion that `x=2` would fail, because `x` is already bound to
`1`.

Unifying structures containing other types of values can get interesting
very fast. Unifying a free (unbound) variable with a structure simply binds
that variable to the entire structure (e.g. `x=(1,2)`). However, binding two
compatible structures with each other allows binding to values inside the
structures. In `(x,2)=(1,2)`, the `x` in the first structure is bound to the
`1` in the second.

Arbitrarily nested structures can be unified by recursively applying this
simple pattern matching.

For simple types, unification is essentially the same thing as equality (and
implementations are provided for these simplest cases). The general pattern
for structures is to define a way to match up their component parts and
recursively attempt to unify them.

# Implementation

Default implementations are provided for most primitive types and some
collections. You can also implement it for your own types.

TODO: Create a derive macro
```
use canrun::{State, DomainType, UnifyIn};
use std::rc::Rc;

#[derive(PartialEq, Debug)]
struct MyType;

impl<'a, D> UnifyIn<'a, D> for MyType
where
    // The domain must be constrained to
    // those that contain yur type
    D: DomainType<'a, Self>
{
    fn unify_resolved(
        state: State<'a, D>,
        a: Rc<Self>,
        b: Rc<Self>
    ) -> Option<State<'a, D>> {
        if a == b { Some(state) } else { None }
    }
}
# fn main() {}
```
Because the trait is parameterized with a [domain](crate::domains), you
should be able to implement UnifyIn for third-party types without running
into the orphan trait rule, so long as you don't conflict with an existing
implementation.
```
# // Just a random foreign type to make this an accurate doctest.
# // I'm pretty sure no one will want to unify this for real :)
# use std::convert::Infallible as SomeForeignType;
use canrun::{State, DomainType, UnifyIn};
use std::rc::Rc;

canrun::domain! {
    MyDomain {
        SomeForeignType
    }
}

impl<'a> UnifyIn<'a, MyDomain> for SomeForeignType {
    // ...
#    fn unify_resolved(
#        state: State<'a, MyDomain>,
#        a: Rc<Self>,
#        b: Rc<Self>
#    ) -> Option<State<'a, MyDomain>> {
#        if a == b { Some(state) } else { None }
#    }
}
# fn main() {}
```
*/
pub trait UnifyIn<'a, D: DomainType<'a, Self>>: Sized + Debug {
    /** Attempt to unify two fully resolved values.

    This function accepts `Rc<T>`s to simplify the borrow checking. The
    `Option<_>` allows recursive unification of structures that hold
    additional values.
    */
    fn unify_resolved(state: State<'a, D>, a: Rc<Self>, b: Rc<Self>) -> Option<State<'a, D>>;
}