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
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139

use std::fmt;
use std::hash::{Hash, Hasher};
use std::mem;

use binder::{Binder, BinderIndex};
use free_var::FreeVar;

/// The [Debruijn index] of the binder that introduced the variable
///
/// For example:
///
/// ```text
/// λx.∀y.λz. x z (y z)
/// λ  ∀  λ   2 0 (1 0)
/// ```
///
/// [Debruijn index]: https://en.wikipedia.org/wiki/De_Bruijn_index
#[derive(Debug, Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Hash)]
pub struct ScopeOffset(pub u32);

impl ScopeOffset {
    /// Move the current Debruijn index into an inner binder
    pub fn succ(self) -> ScopeOffset {
        ScopeOffset(self.0 + 1)
    }

    pub fn pred(self) -> Option<ScopeOffset> {
        match self {
            ScopeOffset(0) => None,
            ScopeOffset(i) => Some(ScopeOffset(i - 1)),
        }
    }
}

impl fmt::Display for ScopeOffset {
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
        fmt::Display::fmt(&self.0, f)
    }
}

/// A variable that can either be free or bound
#[derive(Debug, Clone)]
pub enum Var<N> {
    /// A free variable
    Free(FreeVar<N>),
    /// A variable that is bound by a lambda or pi binder
    Bound(ScopeOffset, BinderIndex, Option<N>),
}

impl<N> Var<N> {
    /// Create a variable from a human-readable string
    pub fn user<T: Into<N>>(ident: T) -> Var<N> {
        Var::Free(FreeVar::user(ident))
    }
}

impl<N> PartialEq for Var<N>
where
    N: PartialEq,
{
    fn eq(&self, other: &Var<N>) -> bool {
        match (self, other) {
            (&Var::Free(ref lhs), &Var::Free(ref rhs)) => lhs == rhs,
            (
                &Var::Bound(scope_offset_lhs, binder_index_lhs, _),
                &Var::Bound(scope_offset_rhs, binder_index_rhs, _),
            ) => scope_offset_lhs == scope_offset_rhs && binder_index_lhs == binder_index_rhs,
            _ => false,
        }
    }
}

impl<N> Eq for Var<N> where N: Eq {}

impl<N> Hash for Var<N>
where
    N: Hash,
{
    fn hash<H: Hasher>(&self, state: &mut H) {
        mem::discriminant(self).hash(state);
        match *self {
            Var::Free(ref free_var) => free_var.hash(state),
            Var::Bound(scope, pattern, _) => {
                scope.hash(state);
                pattern.hash(state);
            },
        }
    }
}

impl<N: fmt::Display> fmt::Display for Var<N> {
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
        match *self {
            Var::Bound(scope_offset, binder_index, None) => {
                write!(f, "@{}.{}", scope_offset, binder_index)
            },
            Var::Bound(scope_offset, binder_index, Some(ref hint)) => {
                write!(f, "{}@{}.{}", hint, scope_offset, binder_index)
            },
            Var::Free(ref free_var) => write!(f, "{}", free_var),
        }
    }
}

impl<N> PartialEq<Binder<N>> for Var<N>
where
    N: PartialEq,
{
    fn eq(&self, other: &Binder<N>) -> bool {
        match self {
            Var::Free(ref lhs) => other == lhs,
            _ => false,
        }
    }
}

impl<N> PartialEq<FreeVar<N>> for Var<N>
where
    N: PartialEq,
{
    fn eq(&self, other: &FreeVar<N>) -> bool {
        match *self {
            Var::Free(ref lhs) => lhs == other,
            _ => false,
        }
    }
}

impl<N> PartialEq<Var<N>> for Binder<N>
where
    N: PartialEq,
{
    fn eq(&self, other: &Var<N>) -> bool {
        match other {
            Var::Free(ref rhs) => self == rhs,
            _ => false,
        }
    }
}