#![feature(non_ascii_idents,
box_syntax,
box_patterns,
fn_traits,
unboxed_closures)]
#[macro_use]
extern crate lalrpop_util;
#[cfg(feature = "wasm")]
extern crate wasm_bindgen;
use std::collections::{HashSet, HashMap};
use std::fmt;
#[cfg(feature = "wasm")]
pub mod wasm;
mod normal;
pub use self::normal::Strategy;
#[macro_use]
mod macros;
mod encode;
#[derive(Clone, PartialEq, Eq)]
pub enum Expression {
Var(Variable),
Abs(Abstraction),
App(Application),
}
#[derive(Clone, Hash, PartialEq, Eq)]
pub struct Variable(pub String, pub Option<String>);
#[derive(Clone, PartialEq, Eq)]
pub struct Abstraction(pub Variable, pub Box<Expression>);
#[derive(Clone, PartialEq, Eq)]
pub struct Application(pub Box<Expression>, pub Box<Expression>);
impl Expression {
pub fn rename(&self, old: &Variable, new: &Variable) -> Self {
dbg!(old, new);
unimplemented!()
}
pub fn variables(&self) -> HashSet<Variable> {
match self {
Expression::Var(v) => set! { v.clone() },
Expression::Abs(Abstraction(id, body)) => {
body.variables().union(&set! { id.clone() }).cloned().collect()
},
Expression::App(Application(e1, e2)) => {
e1.variables().union(&e2.variables()).cloned().collect()
}
}
}
pub fn free_variables(&self) -> HashSet<Variable> {
match self {
Expression::Var(id) => set! { id.clone() },
Expression::Abs(Abstraction(id, body)) => {
body.free_variables()
.difference(&set! { id.clone() })
.cloned()
.collect()
},
Expression::App(Application(e1, e2)) => {
e1.free_variables()
.union(&e2.free_variables())
.cloned()
.collect()
}
}
}
pub fn resolve(&self, env: &HashMap<Variable,Expression>) -> Expression
{
match self {
Expression::Var(id) => {
if let Some(e) = env.get(id) {
e.clone()
} else {
self.clone()
}
},
Expression::Abs(Abstraction(id, box body)) => {
Expression::Abs(Abstraction(id.clone(),
box body.resolve(env)))
},
Expression::App(Application(box e1, box e2)) => {
app!({e1.resolve(env)}, {e2.resolve(env)})
},
}
}
}
impl Expression {
pub fn build_abs(
lambs: usize,
ids: Vec<Variable>,
body: Option<Expression>
)
-> Self
{
let mut abs = body.unwrap_or(var!(""));
let id_count = ids.len();
for i in ids.into_iter().rev() {
abs = Expression::Abs(Abstraction(i, box abs));
}
for l in 0..lambs {
if l == 0 && id_count > 0 { continue; }
abs = Expression::Abs(Abstraction(variable!(""), box abs));
}
abs
}
}
impl fmt::Debug for Expression {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
match self {
Expression::Var(id) => {
write!(f, "{:?}", id)
},
Expression::Abs(Abstraction(id, body)) => {
write!(f, "(λ{:?}.{:?})", id, body)
},
Expression::App(Application(box e1, box e2)) => {
write!(f, "({:?} {:?})", e1, e2)
},
}
}
}
impl fmt::Debug for Variable {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
if let Some(ty) = &self.1 {
write!(f, "{}:{}", self.0, ty)
} else {
write!(f, "{}", self.0)
}
}
}
impl fmt::Display for Expression {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
write!(f, "{:?}", self)
}
}
impl fmt::Display for Variable {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
write!(f, "{:?}", self)
}
}
lalrpop_mod! {
pub parse
}
#[cfg(test)]
mod tests {
use pretty_assertions::assert_eq;
use crate::parse::ExpressionParser;
use super::*;
#[test]
fn variable() {
assert!(ExpressionParser::new().parse(r"x").is_ok());
}
#[test]
fn abstraction() {
assert!(ExpressionParser::new().parse(r"\x.x").is_ok());
assert!(ExpressionParser::new().parse(r"\x. x").is_ok());
assert!(ExpressionParser::new().parse(r"\x.(x)").is_ok());
assert!(ExpressionParser::new().parse(r"\x. (x)").is_ok());
}
#[test]
fn application() {
assert!(ExpressionParser::new().parse(r"x x").is_ok());
assert!(ExpressionParser::new().parse(r"(x y)").is_ok());
assert!(ExpressionParser::new().parse(r"(\x.x y)").is_ok());
}
#[test]
#[ignore]
fn rename() {}
#[test]
#[ignore]
fn variables() {}
#[test]
fn free_variables() {
let parser = ExpressionParser::new();
assert_eq!(set! { variable!(x) },
parser.parse(r"x").unwrap().free_variables());
assert_eq!(set! { },
parser.parse(r"λx.x").unwrap().free_variables());
assert_eq!(set! { variable!(f), variable!(x) },
parser.parse(r"f x").unwrap().free_variables());
assert_eq!(set! { variable!(x), variable!(y) },
parser.parse(r"(λx.(x y)) (λy.(x y))").unwrap().free_variables());
}
#[test]
fn resolve() {
let env = map! {
variable!(n) => 1.into(),
};
assert_eq!(var!(q), var!(q).resolve(&env));
assert_eq!(1u64, var!(n).resolve(&env).into());
}
}