From 0dc2f7be84264372fa5c9db86a0fc75ec61435fd Mon Sep 17 00:00:00 2001 From: Avery Date: Thu, 20 Mar 2025 20:12:07 +0100 Subject: [PATCH] New reduction engine that does builtins and beta simulatniously --- src/exec/builtins.rs | 73 ++++++++++++++++++++++++++++++++------------ src/exec/mod.rs | 30 ++++-------------- src/exec/test.rs | 70 +++++++++++++++++++++++++++++++++--------- src/main.rs | 3 +- 4 files changed, 116 insertions(+), 60 deletions(-) diff --git a/src/exec/builtins.rs b/src/exec/builtins.rs index ccd9b3c..31a690b 100644 --- a/src/exec/builtins.rs +++ b/src/exec/builtins.rs @@ -1,4 +1,4 @@ -use std::{collections::HashMap, rc::Rc}; +use std::{collections::HashMap, fmt::Debug, rc::Rc}; use crate::{ parse::Constant, @@ -55,32 +55,65 @@ pub trait Builtin { fn apply(&self, rhs: DeBrujinBuiltInAst) -> Option; } -impl DeBrujinAst { - pub fn reduce_builtins(self, builtins: &HashMap>) -> DeBrujinAst { - self.resolve_builtins(builtins).reduce_builtins().into() +impl DeBrujinBuiltInAst { + pub(super) fn reduce(self) -> DeBrujinBuiltInAst { + match self { + DeBrujinBuiltInAst::Application(lhs, rhs) => { + let lhs = if lhs.is_value() { *lhs } else { lhs.reduce() }; + let rhs = if rhs.is_value() { *rhs } else { rhs.reduce() }; + assert!(lhs.is_value() && rhs.is_value()); + match lhs { + DeBrujinBuiltInAst::Abstraction(_, _, ast) => { + let ast = ast.subst_bound(1, rhs); + if ast.is_value() { ast } else { ast.reduce() } + } + DeBrujinBuiltInAst::Builtin(builtin) => match builtin.apply(rhs.clone()) { + Some(a) => { + if a.is_value() { + a + } else { + a.reduce() + } + } + None => DeBrujinBuiltInAst::Application( + Box::new(DeBrujinBuiltInAst::Builtin(builtin)), + Box::new(rhs), + ), + }, + a => unreachable!( + "We cannot get a variable or constant because of type checking and we cannot get a application because that is not a value, {:?}", + >::into(a) + ), + } + } + a => a, + } } -} -impl DeBrujinBuiltInAst { - fn reduce_builtins(self) -> DeBrujinBuiltInAst { + fn subst_bound(self, depth: usize, subst: DeBrujinBuiltInAst) -> DeBrujinBuiltInAst { match self { DeBrujinBuiltInAst::Abstraction(i, t, ast) => { - DeBrujinBuiltInAst::Abstraction(i, t, Box::new(ast.reduce_builtins())) + DeBrujinBuiltInAst::Abstraction(i, t, Box::new(ast.subst_bound(depth + 1, subst))) } - DeBrujinBuiltInAst::Application(lhs, rhs) => match *lhs { - DeBrujinBuiltInAst::Builtin(builtin) => builtin - .apply(*rhs) - .expect("the type checker should make sure we can apply") - .reduce_builtins(), - lhs => DeBrujinBuiltInAst::Application( - Box::new(lhs.reduce_builtins()), - Box::new(rhs.reduce_builtins()), - ) - .reduce_builtins(), - }, + DeBrujinBuiltInAst::Application(lhs, rhs) => DeBrujinBuiltInAst::Application( + Box::new(lhs.subst_bound(depth, subst.clone())), + Box::new(rhs.subst_bound(depth, subst)), + ), + DeBrujinBuiltInAst::BoundVariable(n) if n == depth => subst, a => a, } } + + fn is_value(&self) -> bool { + match self { + DeBrujinBuiltInAst::Abstraction(_, _, _) => true, + DeBrujinBuiltInAst::Application(_, _) => false, + DeBrujinBuiltInAst::FreeVariable(_) => true, + DeBrujinBuiltInAst::BoundVariable(_) => true, + DeBrujinBuiltInAst::Constant(constant) => true, + DeBrujinBuiltInAst::Builtin(builtin) => true, + } + } } impl From for DeBrujinAst { @@ -95,7 +128,7 @@ impl From for DeBrujinAst { DeBrujinBuiltInAst::FreeVariable(x) => DeBrujinAst::FreeVariable(x), DeBrujinBuiltInAst::BoundVariable(i) => DeBrujinAst::BoundVariable(i), DeBrujinBuiltInAst::Constant(constant) => DeBrujinAst::Constant(constant), - DeBrujinBuiltInAst::Builtin(builtin) => DeBrujinAst::FreeVariable(builtin.name()), + DeBrujinBuiltInAst::Builtin(builtin) => builtin.to_ast(), } } } diff --git a/src/exec/mod.rs b/src/exec/mod.rs index 696e7e4..a6c5303 100644 --- a/src/exec/mod.rs +++ b/src/exec/mod.rs @@ -62,6 +62,12 @@ impl From for Ast { } impl DeBrujinAst { + pub fn reduce(self, builtins: &HashMap>) -> DeBrujinAst { + let ast = self.resolve_builtins(builtins); + let ast = ast.reduce(); + ast.into() + } + // Vec<(usize, String)> as opposed to a HashMap here since we need to mutate // all the keys every time recuse into an Abstraction, which would be suuper // expensive if not impossible with a HashMap @@ -88,28 +94,4 @@ impl DeBrujinAst { DeBrujinAst::Constant(constant) => Ast::Constant(constant), } } - - pub fn beta_reduce(self) -> DeBrujinAst { - match self { - DeBrujinAst::Application(lhs, rhs) => match *lhs { - DeBrujinAst::Abstraction(_, _, ast) => ast.subst_bound(1, *rhs).beta_reduce(), - lhs => DeBrujinAst::Application(Box::new(lhs), rhs), - }, - a => a, - } - } - - fn subst_bound(self, depth: usize, subst: DeBrujinAst) -> DeBrujinAst { - match self { - DeBrujinAst::Abstraction(i, t, ast) => { - DeBrujinAst::Abstraction(i, t, Box::new(ast.subst_bound(depth + 1, subst))) - } - DeBrujinAst::Application(lhs, rhs) => DeBrujinAst::Application( - Box::new(lhs.subst_bound(depth, subst.clone())), - Box::new(rhs.subst_bound(depth, subst)), - ), - DeBrujinAst::BoundVariable(n) if n == depth => subst, - a => a, - } - } } diff --git a/src/exec/test.rs b/src/exec/test.rs index 341f1b2..00b67a8 100644 --- a/src/exec/test.rs +++ b/src/exec/test.rs @@ -3,7 +3,7 @@ use std::{collections::HashMap, rc::Rc}; use crate::{ exec::{DeBrujinAst as DBAst, builtin_definitions::AddOp}, parse::{Ast, Constant}, - types::{PrimitiveType, Type}, + types::{PrimitiveType, TaggedType, Type, TypeTag}, }; use super::builtins::Builtin; @@ -40,22 +40,13 @@ fn de_brujin_beta_reduce() { Box::new(Ast::Abstraction( "x".to_string(), Some(Type::arrow(PrimitiveType::Nat, PrimitiveType::Nat).into()), - Box::new(Ast::Application( - Box::new(Ast::Variable("x".to_string())), - Box::new(Ast::Constant(Constant::Nat(5))), - )), + Box::new(Ast::Variable("x".to_string())), )), Box::new(Ast::Variable("y".to_string())), ); let dbast: DBAst = input.into(); - let reduced = dbast.beta_reduce(); - assert_eq!( - reduced, - DBAst::Application( - Box::new(DBAst::FreeVariable("y".to_string())), - Box::new(DBAst::Constant(Constant::Nat(5))), - ), - ) + let reduced = dbast.reduce(&HashMap::new()); + assert_eq!(reduced, DBAst::FreeVariable("y".to_string())) } #[test] @@ -88,6 +79,57 @@ fn reduce_add() { .into(); let mut builtins: HashMap> = HashMap::new(); builtins.insert("add".to_string(), Rc::new(AddOp)); - let output = input.reduce_builtins(&builtins); + let output = input.reduce(&builtins); assert_eq!(output, DBAst::Constant(Constant::Nat(10))); } + +#[test] +/// (\x:Any a => a -> a.\y:Num a => a. add 1 (x y)) (\x:Any a => a.x) 2 +fn reduce_complex() { + let input: DBAst = Ast::Application( + Box::new(Ast::Application( + Box::new(Ast::Abstraction( + "x".to_string(), + Some(TaggedType::Tagged( + TypeTag::Any, + "a".to_string(), + Box::new(TaggedType::Concrete(Type::arrow("a", "a"))), + )), + Box::new(Ast::Abstraction( + "y".to_string(), + Some(TaggedType::Tagged( + TypeTag::Num, + "a".to_string(), + Box::new(TaggedType::Concrete("a".into())), + )), + Box::new(Ast::Application( + Box::new(Ast::Application( + Box::new(Ast::Variable("add".to_string())), + Box::new(Ast::Constant(Constant::Nat(1))), + )), + Box::new(Ast::Application( + Box::new(Ast::Variable("x".to_string())), + Box::new(Ast::Variable("y".to_string())), + )), + )), + )), + )), + Box::new(Ast::Abstraction( + "x".to_string(), + Some(TaggedType::Tagged( + TypeTag::Any, + "a".to_string(), + Box::new(TaggedType::Concrete("a".into())), + )), + Box::new(Ast::Variable("x".to_string())), + )), + )), + Box::new(Ast::Constant(Constant::Nat(2))), + ) + .into(); + + let mut builtins: HashMap> = HashMap::new(); + builtins.insert("add".to_string(), Rc::new(AddOp)); + let output = input.reduce(&builtins); + assert_eq!(output, DBAst::Constant(Constant::Nat(3))); +} diff --git a/src/main.rs b/src/main.rs index 19b50a9..dacc040 100644 --- a/src/main.rs +++ b/src/main.rs @@ -81,8 +81,7 @@ fn main() { Ok(t) => t, Err(e) => repl_err!("Could not infer type {e:?}"), }; - let ast = ast.beta_reduce(); - let ast = ast.reduce_builtins(&builtins); + let ast = ast.reduce(&builtins); let ast: Ast = ast.into(); println!("{ast} : {typ}") }