From 4bfaeda8039acc2a25891a778a51ae7dce1e0d32 Mon Sep 17 00:00:00 2001 From: Jan Tuomi Date: Tue, 23 Nov 2021 20:27:27 +0200 Subject: Get term reduction (without Lazy) seemingly working --- src/builtins.rs | 2 +- src/runtime.rs | 172 ++++++++++++++++++++++++++++++++++++++++++++++++++------ 2 files changed, 157 insertions(+), 17 deletions(-) (limited to 'src') diff --git a/src/builtins.rs b/src/builtins.rs index 46b6ec5..fa029a9 100644 --- a/src/builtins.rs +++ b/src/builtins.rs @@ -21,7 +21,7 @@ pub fn make_identity_function() -> Term { Term::Abstraction(v, Rc::new(Term::Variable(v))) } -pub fn try_builtin_symbol_to_value(symbol: &ast::Symbol) -> Option { +pub fn try_builtin_symbol_to_term(symbol: &ast::Symbol) -> Option { match symbol.as_str() { "true" => Some(make_boolean_true_function()), "false" => Some(make_boolean_false_function()), diff --git a/src/runtime.rs b/src/runtime.rs index 8f2c0e8..8e71eb3 100644 --- a/src/runtime.rs +++ b/src/runtime.rs @@ -14,8 +14,8 @@ pub enum Value { impl fmt::Display for Value { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { - Value::Integer(value) => write!(f, "{} :: Integer", value), - Value::String(value) => write!(f, "{} :: String", value), + Value::Integer(value) => write!(f, "Integer({})", value), + Value::String(value) => write!(f, "String({})", value), } } } @@ -100,6 +100,128 @@ pub fn advance_v() -> usize { // } // } +fn bound_variable_opt_to_string(bound_variable_opt: &Option<(usize, Rc)>) -> String { + match bound_variable_opt { + Some((v, term_rc)) => format!("({}, {})", v, term_rc), + None => String::from("None"), + } +} + +fn substitute_var( + term_rc: Rc, + bound_variable_opt: &Option<(usize, Rc)>, +) -> ReductionResult { + let term = &*term_rc; + match term { + Term::Variable(v) => match bound_variable_opt { + Some((bound_v, bound_term_rc)) => { + if bound_v == v { + Ok((Rc::clone(bound_term_rc), 1)) + } else { + Ok((term_rc, 0)) + } + } + None => Ok((term_rc, 0)), + }, + _ => Err(format!( + "[runtime] non-var term passed to substitute_var: {}", + term_rc + )), + } +} + +type ReductionResult = Result<(Rc, usize), String>; + +fn reduce_term( + symbol_table: &HashMap>, + term_rc: Rc, + bound_variable_opt: &Option<(usize, Rc)>, + resolve_lazy: bool, +) -> ReductionResult { + let term = &*term_rc; + println!( + "[debug] reduce_term with term_rc:\n{}\nbound_variable_opt:\n{}\n", + term_rc, + bound_variable_opt_to_string(bound_variable_opt) + ); + let result = match term { + Term::Primitive(_) => Ok((term_rc, 0)), + Term::Variable(_) => substitute_var(term_rc, bound_variable_opt), + Term::Application(lhs_rc, rhs_rc) => { + let (subst_lhs_rc, lhs_n) = reduce_term( + symbol_table, + Rc::clone(lhs_rc), + bound_variable_opt, + resolve_lazy, + )?; + let (subst_rhs_rc, rhs_n) = reduce_term( + symbol_table, + Rc::clone(rhs_rc), + bound_variable_opt, + resolve_lazy, + )?; + + let subst_n = lhs_n + rhs_n; + + let (result, app_n) = match &*subst_lhs_rc { + Term::Abstraction(abs_v, abs_body_rc) => reduce_term( + symbol_table, + Rc::clone(abs_body_rc), + &Some((*abs_v, subst_rhs_rc)), + resolve_lazy, + ), + _ => Ok(( + Rc::new(Term::Application(subst_lhs_rc, subst_rhs_rc)), + subst_n, + )), + }?; + + Ok((result, app_n + subst_n)) + } + Term::Abstraction(abs_v, body_rc) => { + let (subst_body, subst_n) = reduce_term( + symbol_table, + Rc::clone(body_rc), + bound_variable_opt, + resolve_lazy, + )?; + Ok((Rc::new(Term::Abstraction(*abs_v, subst_body)), subst_n)) + } + // Term::Lazy(symbol) => { + // if resolve_lazy { + // let table_lookup_value = symbol_table.get(symbol); + // if table_lookup_value.is_some() { + // let lookup_rc = table_lookup_value.unwrap(); + // return reduce_term( + // symbol_table, + // lookup_rc.clone(), + // bound_variable_opt, + // resolve_lazy, + // ); + // } + + // let builtin_value = builtins::try_builtin_symbol_to_term(symbol); + // if builtin_value.is_some() { + // let builtin_rc = Rc::new(builtin_value.unwrap()); + // return reduce_term( + // symbol_table, + // builtin_rc.clone(), + // bound_variable_opt, + // resolve_lazy, + // ); + // } + + // panic!("[runtime] symbol {} not defined", symbol); + // } else { + // term_rc + // } + // } + _ => todo!("reduce_term cases"), + }; + // println!("[debug] returning {}\n", result); + result +} + fn process_expr_inner_unary( symbol_table: &HashMap>, inner: &ast::ExpressionInner, @@ -126,7 +248,7 @@ fn process_expr_inner_unary( return Rc::clone(lookup_rc); } - let builtin_value = builtins::try_builtin_symbol_to_value(value); + let builtin_value = builtins::try_builtin_symbol_to_term(value); if builtin_value.is_some() { return Rc::new(builtin_value.unwrap()); } @@ -164,7 +286,7 @@ fn process_expr_inner_binary( lhs_term = Rc::new(Term::Variable(bound_symbol.1)); } else if let Some(lookup) = symbol_table.get(value) { lhs_term = Rc::clone(lookup); - } else if let Some(builtin) = builtins::try_builtin_symbol_to_value(value) { + } else if let Some(builtin) = builtins::try_builtin_symbol_to_term(value) { lhs_term = Rc::new(builtin); } else { lhs_term = Rc::new(Term::Lazy(value.clone())); @@ -198,7 +320,7 @@ fn process_expr( pub fn process(program: &ast::Program) { let mut symbol_table: HashMap> = HashMap::new(); - for (index, statement) in program.iter().enumerate() { + for (_index, statement) in program.iter().enumerate() { match statement { ast::Statement::Definition { symbol, @@ -211,26 +333,44 @@ pub fn process(program: &ast::Program) { .map(|param| (param.clone(), advance_v())) .collect(); - let evaled_expr = process_expr(&symbol_table, expression, &bound_params); - let mut abstracted_expr: Rc = evaled_expr; + let mut term = process_expr(&symbol_table, expression, &bound_params); bound_params.iter().rev().for_each(|(_, v)| { - abstracted_expr = Rc::new(Term::Abstraction(*v, Rc::clone(&abstracted_expr))); + term = Rc::new(Term::Abstraction(*v, Rc::clone(&term))); }); - symbol_table.insert(symbol.clone(), abstracted_expr); + println!("Term:\n{}", term); + symbol_table.insert(symbol.clone(), term); } ast::Statement::Expression(expression) => { println!("[runtime] evaluating free-standing expression"); - let term = process_expr(&symbol_table, expression, &vec![]); - println!("Term:\n{}", term); - // let value = evaluate_term(&symbol_table, term); + let mut term: Rc = process_expr(&symbol_table, expression, &vec![]); + let mut reduction_result: ReductionResult; + loop { + // println!("Term:\n{}", term); + reduction_result = reduce_term(&symbol_table, term.clone(), &None, false); + match reduction_result { + Ok((result_term, substitution_n)) => { + println!("Reduction OK:\n{},\nN: {}\n", result_term, substitution_n); + if substitution_n > 0 { + term = result_term; + } else { + break; + } + } + Err(err_string) => { + println!("Reduction ERR:\n{}\n", err_string) + } + } + } + + println!("Reduction terminated, result:\n{}", term); } } } - println!( - "[runtime] evaluation done, symbol_table state dump: {:#?}", - symbol_table - ); + // println!( + // "[runtime] evaluation done, symbol_table state dump: {:#?}", + // symbol_table + // ); } -- cgit v1.3