diff options
Diffstat (limited to 'lambda-calcul/rust/src')
| -rw-r--r-- | lambda-calcul/rust/src/ast.rs | 10 | ||||
| -rw-r--r-- | lambda-calcul/rust/src/builtins.rs | 25 | ||||
| -rw-r--r-- | lambda-calcul/rust/src/io.rs | 6 | ||||
| -rw-r--r-- | lambda-calcul/rust/src/lambda.rs | 73 | ||||
| -rw-r--r-- | lambda-calcul/rust/src/web.rs | 18 |
5 files changed, 106 insertions, 26 deletions
diff --git a/lambda-calcul/rust/src/ast.rs b/lambda-calcul/rust/src/ast.rs index bdfb963..2b9bcfc 100644 --- a/lambda-calcul/rust/src/ast.rs +++ b/lambda-calcul/rust/src/ast.rs @@ -14,7 +14,11 @@ pub enum Type { impl Display for Type { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - write!(f, "Type") + match self { + Type::Num => write!(f, "Num"), + Type::Bool => write!(f, "Bool"), + Type::Arr(l, r) => write!(f, "({} -> {})", l, r), + } } } @@ -39,7 +43,7 @@ pub enum Value { // this is unsound as we are not in a dependently typed language // but useful to unify external representation (AST). In theory, // we should separate AST from Terms - Type(Type) + Type(Type), } use Value::*; @@ -76,7 +80,7 @@ impl Display for Value { Value::Lam(var, body) => write!(f, "(lam {} {})", var, body), Value::Def(var, value) => write!(f, "(def {} {})", var, value), Value::Let(var, value, body) => write!(f, "(let ({} {}) {})", var, value, body), - Value::TLam(var,typ, body) => write!(f, "(tlam ({} {}) {})", var, typ, body), + Value::TLam(var, typ, body) => write!(f, "(tlam ({} {}) {})", var, typ, body), Value::Type(typ) => write!(f, ":{}", typ), } } diff --git a/lambda-calcul/rust/src/builtins.rs b/lambda-calcul/rust/src/builtins.rs new file mode 100644 index 0000000..7064c1c --- /dev/null +++ b/lambda-calcul/rust/src/builtins.rs @@ -0,0 +1,25 @@ +use crate::ast::Value; +use std::collections::HashMap; + +pub struct Builtins {} + +impl Builtins { + pub fn new() -> HashMap<String, Value> { + let mut map = HashMap::new(); + map.insert("+".to_string(), Value::Prim("+".to_string())); + map + } +} + +pub fn plus(v: Value) -> Value { + match v { + Num(i) => Lam(gensym(), + } +} + +pub fn builtins(sym: &String) -> Option<Box<dyn Fn(Value) -> Value>> { + match sym.as_str() { + "+" => Some(Box::new(plus)), + _ => None, + } +} diff --git a/lambda-calcul/rust/src/io.rs b/lambda-calcul/rust/src/io.rs index 8c628ba..4e5fb59 100644 --- a/lambda-calcul/rust/src/io.rs +++ b/lambda-calcul/rust/src/io.rs @@ -21,6 +21,7 @@ pub fn eval_file(file_name: &str) -> String { pub fn batch_eval<I: Read, O: Write>(inp: &mut I, outp: &mut O) { let mut env = Environment::new(); + let mut context = Environment::new(); let mut reader = BufReader::new(inp); loop { let mut input = String::new(); @@ -36,7 +37,7 @@ pub fn batch_eval<I: Read, O: Write>(inp: &mut I, outp: &mut O) { let values = parse(&input); let results = values .iter() - .map(|v| eval_whnf(v, &mut env)) + .map(|v| eval_whnf(v, &mut env, &mut context)) .collect::<Vec<Value>>(); for result in results { writeln!(outp, "{}", result).unwrap(); @@ -47,6 +48,7 @@ pub fn batch_eval<I: Read, O: Write>(inp: &mut I, outp: &mut O) { pub fn repl<I: Read, O: Write>(inp: &mut I, outp: &mut O) { let mut env = Environment::new(); + let mut context = Environment::new(); let mut reader = BufReader::new(inp); loop { let mut input = String::new(); @@ -63,7 +65,7 @@ pub fn repl<I: Read, O: Write>(inp: &mut I, outp: &mut O) { let values = parse(&input); let results = values .iter() - .map(|v| eval_whnf(v, &mut env)) + .map(|v| eval_whnf(v, &mut env, &mut context)) .collect::<Vec<Value>>(); for result in results { writeln!(outp, "{}", result).unwrap(); diff --git a/lambda-calcul/rust/src/lambda.rs b/lambda-calcul/rust/src/lambda.rs index ea571fd..80f2d5c 100644 --- a/lambda-calcul/rust/src/lambda.rs +++ b/lambda-calcul/rust/src/lambda.rs @@ -1,3 +1,4 @@ +use log::debug; use proptest::{ arbitrary::any, prelude::*, @@ -50,7 +51,11 @@ impl<'a, T: Clone> Default for Environment<'a, T> { pub fn eval_all(values: &[Value]) -> Vec<Value> { let mut env = Environment::new(); - values.iter().map(|v| eval_whnf(v, &mut env)).collect() + let mut context = Environment::new(); + values + .iter() + .map(|v| eval_whnf(v, &mut env, &mut context)) + .collect() } /// Reduce the given value to weak head normal form using call-by-name @@ -58,8 +63,13 @@ pub fn eval_all(values: &[Value]) -> Vec<Value> { /// /// call-by-name reduces the leftmost outermost redex first, which is /// not under a lambda abstraction. -pub fn eval_whnf(arg: &Value, env: &mut Environment<Value>) -> Value { - match arg { +pub fn eval_whnf( + arg: &Value, + env: &mut Environment<Value>, + context: &mut Environment<Type>, +) -> Value { + debug!("evaluating {}", arg); + let result = match arg { Value::Def(var, value) => { env.bind(var, value); Value::Bool(true) // TODO: return a more meaningful value? @@ -67,19 +77,26 @@ pub fn eval_whnf(arg: &Value, env: &mut Environment<Value>) -> Value { Value::Let(var, value, expr) => { let mut newenv = env.extends(); newenv.bind(var, value); - eval_whnf(expr, &mut newenv) + eval_whnf(expr, &mut newenv, context) } - Value::App(l, r) => match eval_whnf(l, env) { - Value::Lam(v, body) => eval_whnf(&subst(&v, &body, r), env), - Value::Sym(var) => match env.lookup(&var) { - Some(val) => eval_whnf(&Value::App(Box::new(val.clone()), r.clone()), env), - None => arg.clone(), + Value::App(l, r) => match eval_whnf(l, env, context) { + Value::Lam(v, body) => eval_whnf(&subst(&v, &body, r), env, context), + Value::Sym(var) => match var.as_str() { + ":type-of" => type_of(r, context).map(Value::Type).unwrap(), + _ => match env.lookup(&var) { + Some(val) => { + eval_whnf(&Value::App(Box::new(val.clone()), r.clone()), env, context) + } + None => arg.clone(), + }, }, other => Value::App(Box::new(other), r.clone()), }, Value::Sym(var) => env.lookup(var).unwrap_or(arg).clone(), other => other.clone(), - } + }; + debug!("evaluated to {}", result); + result } fn subst(var: &str, body: &Value, e: &Value) -> Value { @@ -234,21 +251,25 @@ fn gen_terms(u: u32) -> impl Strategy<Value = Value> { #[cfg(test)] mod lambda_test { - use crate::{ast::Type, parser::parse}; - use super::{eval_all, eval_whnf, type_of, Environment, Value}; + use crate::{ast::Type, lambda::gen_terms, parser::parse}; + use proptest::{ + prelude::*, + strategy::{Strategy, ValueTree}, + test_runner::TestRunner, + }; fn parse1(string: &str) -> Value { parse(string).pop().unwrap() } fn eval1(value: &Value) -> Value { - eval_whnf(value, &mut Environment::new()) + eval_whnf(value, &mut Environment::new(), &mut Environment::new()) } #[test] fn evaluate_symbol_starting_with_x_returns_same_symbol() { - let sym= "x1xYgddw7"; + let sym = "x1xYgddw7"; let value = parse1(sym); assert_eq!(value, eval1(&value)); @@ -308,6 +329,11 @@ mod lambda_test { } #[test] + fn type_of_returns_type_of_expression() { + let value = parse1("(:type-of 11)"); + assert_eq!(Value::Type(Type::Num), eval1(&value)); + } + #[test] fn defined_symbols_are_evaluated_to_their_definition() { let values = parse("(def foo 12) foo"); assert_eq!(vec![Value::Bool(true), Value::Num(12)], eval_all(&values)); @@ -375,4 +401,23 @@ mod lambda_test { assert_eq!(Type::Arr(Box::new(Type::Num), Box::new(Type::Num)), ty); } + + #[test] + fn any_terms() { + let mut runner = TestRunner::default(); + for i in 0..100 { + let value = any::<u32>() + .prop_flat_map(gen_terms) + .new_tree(&mut runner) + .unwrap() + .current(); + let evaluation = eval1(&value); + println!( + "{} term: {}, evaluation: {}", + value == evaluation, + value, + evaluation + ); + } + } } diff --git a/lambda-calcul/rust/src/web.rs b/lambda-calcul/rust/src/web.rs index 7dae468..7345d0f 100644 --- a/lambda-calcul/rust/src/web.rs +++ b/lambda-calcul/rust/src/web.rs @@ -130,18 +130,18 @@ impl Client { self.generate_exprs() } else { let input = generate_expr(self.grade.into(), &mut self.runner); - let expected = eval_whnf(&input, &mut Environment::new()); + let expected = eval_whnf(&input, &mut Environment::new(), &mut Environment::new()); (vec![input], vec![expected]) } } fn generate_expression_to_type(&mut self) -> (Vec<Value>, Vec<Value>) { let input = - generate_expression_to_type((self.grade - Self::TYPING_GRADE).into(), &mut self.runner); - let expected = type_of_all(&input) - .iter() - .map(|t| Value::Type(t.clone())) - .collect(); + generate_expression_to_type((self.grade - Self::TYPING_GRADE).into(), &mut self.runner) + .into_iter() + .map(|e| Value::App(Box::new(Value::Sym(":type-of".to_string())), Box::new(e))) + .collect::<Vec<_>>(); + let expected = eval_all(&input); (input, expected) } @@ -273,6 +273,7 @@ async fn eval(input: String) -> impl Responder { let exprs = parse_total(&input); match exprs { Ok(exprs) => { + // Occasionally return a random symbol to keep clients on their toes let mut rng = rand::thread_rng(); if rng.gen_range(0..10) <= 2 { return HttpResponse::Ok().body(gensym()); @@ -392,7 +393,10 @@ fn apply_result( ) { let mut client = client_m.lock().unwrap(); let test = client.check_result(&expected, &response); - info!("result for {} = {:?}, expected {:?}", client.url, test, expected); + info!( + "result for {} = {:?}, expected {:?}", + client.url, test, expected + ); client.apply(&test); } |