#[cfg(test)]
use proptest::strategy::Strategy;
use std::collections::HashSet;
use std::fmt::{self, Display};
use std::ops::{Deref, DerefMut};
use self::Term::*;
pub fn var(name: impl Into<String>) -> Term {
Var(VarName(name.into()))
}
pub fn lam(param: impl Into<String>, body: Term) -> Term {
Lam(VarName(param.into()), Box::new(body))
}
pub fn app(lhs: Term, rhs: Term) -> Term {
App(Box::new(lhs), Box::new(rhs))
}
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
pub enum Term {
Var(VarName),
Lam(VarName, Box<Term>),
App(Box<Term>, Box<Term>),
}
enum TermFormat<'a> {
LParen,
RParen,
Space,
ToFormat(&'a Term),
}
impl Display for Term {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
use self::fmt::Write;
use self::TermFormat::*;
let mut to_format = Vec::with_capacity(7);
to_format.push(ToFormat(self));
while let Some(item) = to_format.pop() {
match item {
LParen => f.write_char('(')?,
RParen => f.write_char(')')?,
Space => f.write_char(' ')?,
ToFormat(term) => match term {
Var(name) => f.write_str(&name)?,
Lam(param, body) => {
write!(f, "λ{}.", ¶m)?;
to_format.push(ToFormat(&**body));
},
App(lhs, rhs) => match (&**lhs, &**rhs) {
(App(_, _), App(_, _)) => {
to_format.push(RParen);
to_format.push(ToFormat(&**rhs));
to_format.push(LParen);
to_format.push(Space);
to_format.push(RParen);
to_format.push(ToFormat(&**lhs));
to_format.push(LParen);
},
(Lam(_, _), App(_, _)) => {
to_format.push(RParen);
to_format.push(ToFormat(&**rhs));
to_format.push(LParen);
to_format.push(Space);
to_format.push(RParen);
to_format.push(ToFormat(&**lhs));
to_format.push(LParen);
},
(Lam(_, _), Lam(_, _)) => {
to_format.push(RParen);
to_format.push(ToFormat(&**rhs));
to_format.push(LParen);
to_format.push(Space);
to_format.push(RParen);
to_format.push(ToFormat(&**lhs));
to_format.push(LParen);
},
(_, App(_, _)) => {
to_format.push(RParen);
to_format.push(ToFormat(&**rhs));
to_format.push(LParen);
to_format.push(Space);
to_format.push(ToFormat(&**lhs));
},
(_, Lam(_, _)) => {
to_format.push(RParen);
to_format.push(ToFormat(&**rhs));
to_format.push(LParen);
to_format.push(Space);
to_format.push(ToFormat(&**lhs));
},
(Lam(_, _), _) => {
to_format.push(ToFormat(&**rhs));
to_format.push(Space);
to_format.push(RParen);
to_format.push(ToFormat(&**lhs));
to_format.push(LParen);
},
(_, _) => {
to_format.push(ToFormat(&**rhs));
to_format.push(Space);
to_format.push(ToFormat(&**lhs));
},
},
},
}
}
Ok(())
}
}
impl<'a> From<&'a Term> for Term {
fn from(expr: &Term) -> Self {
expr.to_owned()
}
}
impl From<VarName> for Term {
fn from(var: VarName) -> Self {
Var(var)
}
}
impl Term {
pub fn free_vars(&self) -> HashSet<&VarName> {
let mut free_vars = HashSet::with_capacity(4);
let mut to_check: Vec<(&Term, HashSet<&VarName>)> = Vec::with_capacity(2);
to_check.push((self, HashSet::with_capacity(4)));
while let Some((term, mut bound_vars)) = to_check.pop() {
match *term {
Var(ref name) => {
if !bound_vars.contains(name) {
free_vars.insert(name);
}
},
Lam(ref param, ref body) => {
bound_vars.insert(param);
to_check.push((&*body, bound_vars));
},
App(ref lhs, ref rhs) => {
to_check.push((&*rhs, bound_vars.clone()));
to_check.push((&*lhs, bound_vars));
},
}
}
free_vars
}
}
#[cfg(test)]
#[allow(dead_code)]
pub fn any_application() -> impl Strategy<Value = Term> {
(any_term(), any_term()).prop_map(|(lhs, rhs)| App(lhs.into(), rhs.into()))
}
#[cfg(test)]
#[allow(dead_code)]
pub fn any_abstraction() -> impl Strategy<Value = Term> {
(any_short_var_name(), any_term()).prop_map(|(param, body)| Lam(param, body.into()))
}
#[cfg(test)]
pub fn any_term() -> impl Strategy<Value = Term> {
any_short_variable().prop_recursive(23, 500, 3, |inner| {
prop_oneof!{
inner.clone(),
(any_short_var_name(), inner.clone()).prop_map(|(param, body)| Lam(param, body.into())),
(inner.clone(), inner.clone()).prop_map(|(lhs, rhs)| App(lhs.into(), rhs.into())),
}
})
}
#[cfg(test)]
#[allow(dead_code)]
pub fn any_variable() -> impl Strategy<Value = Term> {
any_var_name().prop_map(Var)
}
#[cfg(test)]
pub fn any_short_variable() -> impl Strategy<Value = Term> {
any_short_var_name().prop_map(Var)
}
#[derive(Debug, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub struct VarName(pub String);
impl Display for VarName {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
write!(f, "{}", self.0)
}
}
impl Deref for VarName {
type Target = String;
fn deref(&self) -> &<Self as Deref>::Target {
&self.0
}
}
impl DerefMut for VarName {
fn deref_mut(&mut self) -> &mut <Self as Deref>::Target {
&mut self.0
}
}
impl AsRef<str> for VarName {
fn as_ref(&self) -> &str {
&self.0
}
}
impl VarName {
pub fn new(name: impl Into<String>) -> Self {
VarName(name.into())
}
pub fn unwrap(self) -> String {
self.0
}
}
#[cfg(test)]
pub fn any_var_name() -> impl Strategy<Value = VarName> {
any_identifier_().prop_map(VarName)
}
#[cfg(test)]
pub fn any_short_var_name() -> impl Strategy<Value = VarName> {
any_short_identifier_().prop_map(VarName)
}
#[cfg(test)]
pub fn any_identifier() -> impl Strategy<Value = String> {
any_identifier_()
}
#[cfg(test)]
prop_compose! {
fn any_identifier_()(
name in "[A-Za-z0-9][A-Za-z0-9_']*",
) -> String {
name
}
}
#[cfg(test)]
prop_compose! {
fn any_short_identifier_()(
name in "[A-Za-z0-9][A-Za-z0-9_']?",
) -> String {
name
}
}
#[macro_export]
macro_rules! app {
($term1:expr, $($term2:expr),+) => {
{
let mut __term = $term1;
$(__term = $crate::Term::App(Box::new(__term), Box::new($term2));)*
__term
}
}
}
#[cfg(test)]
mod tests;