diff --git a/src/parser.rs b/src/parser.rs index 03b7d90..aa2f98f 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -7,6 +7,7 @@ use self::Token::*; pub use crate::term::Notation::*; use crate::term::Term::*; use crate::term::{abs, app, Notation, Term}; +use std::collections::VecDeque; use std::error::Error; use std::fmt; @@ -138,12 +139,12 @@ pub fn tokenize_cla(input: &str) -> Result, ParseError> { #[doc(hidden)] pub fn convert_classic_tokens(tokens: &[CToken]) -> Vec { - _convert_classic_tokens(tokens, &mut Vec::with_capacity(tokens.len()), &mut 0) + _convert_classic_tokens(tokens, &mut VecDeque::with_capacity(tokens.len()), &mut 0) } fn _convert_classic_tokens<'t>( tokens: &'t [CToken], - stack: &mut Vec<&'t str>, + stack: &mut VecDeque<&'t str>, pos: &mut usize, ) -> Vec { let mut output = Vec::with_capacity(tokens.len() - *pos); @@ -153,7 +154,7 @@ fn _convert_classic_tokens<'t>( match *token { CLambda(ref name) => { output.push(Lambda); - stack.push(name); + stack.push_back(name); inner_stack_count += 1; } CLparen => { @@ -170,7 +171,10 @@ fn _convert_classic_tokens<'t>( if let Some(index) = stack.iter().rev().position(|t| t == name) { output.push(Number(index + 1)) } else { - output.push(Number(stack.len() + 1)) + // a new free variable + stack.push_front(name); + // index of the last element + 1 + output.push(Number(stack.len())) } } } @@ -358,6 +362,23 @@ mod tests { ); } + #[test] + fn tokenization_success_classic_with_free_variables() { + let blc_dbr = "12"; + let blc_cla = parse(blc_dbr, DeBruijn).unwrap().to_string(); + + let tokens_cla = tokenize_cla(&blc_cla); + let tokens_dbr = tokenize_dbr(blc_dbr); + + assert!(tokens_cla.is_ok()); + assert!(tokens_dbr.is_ok()); + + assert_eq!( + convert_classic_tokens(&tokens_cla.unwrap()), + tokens_dbr.unwrap() + ); + } + #[test] fn alternative_lambda_parsing() { assert_eq!( diff --git a/tests/parser.rs b/tests/parser.rs new file mode 100644 index 0000000..dca14e9 --- /dev/null +++ b/tests/parser.rs @@ -0,0 +1,33 @@ +use lambda_calculus::{ + parse, + parser::ParseError, + term::Notation::{Classic, DeBruijn}, +}; + +#[test] +fn parse_debruijn_and_classic() -> Result<(), ParseError> { + for (dbr, cla) in [ + ("12", "a b"), + ("λλ21", "λs. λz. s z"), + ( + "λ2134(λ3215(λ4321)3215)2134", + "λx. w x y z (λy. w x y z (λz. w x y z) w x y z) w x y z", + ), + ( + // See: http://alexandria.tue.nl/repository/freearticles/597619.pdf + "λ2(λ421(5(λ4127)λ8))67", + // the free variable list is ..ywzfba + "λx. a (λt. b x t (f (λu. a u t z) λs. w)) w y", + ), + ( + // apply `plus zero one` to `s` and `z` + "(λλλλ42(321))(λλ1)(λλ21)12", + "(λm.λn.λs.λz. m s (n s z)) (λs.λz. z) (λs.λz. s z) s z", + ), + ] { + let term_dbr = parse(dbr, DeBruijn)?; + let term_cla = parse(cla, Classic)?; + assert_eq!(term_dbr, term_cla); + } + Ok(()) +} diff --git a/tests/reduction.rs b/tests/reduction.rs index 91ba3f2..c32ee57 100644 --- a/tests/reduction.rs +++ b/tests/reduction.rs @@ -1,6 +1,7 @@ extern crate lambda_calculus as lambda; use lambda::combinators::{I, O}; +use lambda::parser::ParseError; use lambda::*; use std::thread; @@ -48,6 +49,20 @@ fn reduction_cbv() { assert_eq!(expr, I()); } +#[test] +fn reduction_zero_plus_one() -> Result<(), ParseError> { + let mut expr = parse( + "(λm.λn.λs.λz. m s (n s z)) (λs.λz. z) (λs.λz. s z) s z", + Classic, + )?; + expr.reduce(CBV, 2); + assert_eq!(expr, parse("(λλ(λλ1)2((λλ21)21))12", DeBruijn)?); + expr.reduce(CBV, 6); + assert_eq!(expr, parse("12", DeBruijn)?); + assert_eq!(expr.to_string(), "a b"); + Ok(()) +} + #[test] #[ignore] fn reduction_huge() {