New reduction engine that does builtins and beta simulatniously

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<DeBrujinBuiltInAst>;
 }
 
-impl DeBrujinAst {
+impl DeBrujinBuiltInAst {
-    pub fn reduce_builtins(self, builtins: &HashMap<String, Rc<dyn Builtin>>) -> DeBrujinAst {
+    pub(super) fn reduce(self) -> DeBrujinBuiltInAst {
-        self.resolve_builtins(builtins).reduce_builtins().into()
+        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, {:?}",
+                        <DeBrujinBuiltInAst as Into<DeBrujinAst>>::into(a)
+                    ),
+                }
+            }
+            a => a,
+        }
     }
-}
 
-impl DeBrujinBuiltInAst {
+    fn subst_bound(self, depth: usize, subst: DeBrujinBuiltInAst) -> DeBrujinBuiltInAst {
-    fn reduce_builtins(self) -> 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::Application(lhs, rhs) => DeBrujinBuiltInAst::Application(
-                DeBrujinBuiltInAst::Builtin(builtin) => builtin
+                Box::new(lhs.subst_bound(depth, subst.clone())),
-                    .apply(*rhs)
+                Box::new(rhs.subst_bound(depth, subst)),
-                    .expect("the type checker should make sure we can apply")
+            ),
-                    .reduce_builtins(),
+            DeBrujinBuiltInAst::BoundVariable(n) if n == depth => subst,
-                lhs => DeBrujinBuiltInAst::Application(
-                    Box::new(lhs.reduce_builtins()),
-                    Box::new(rhs.reduce_builtins()),
-                )
-                .reduce_builtins(),
-            },
             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<DeBrujinBuiltInAst> for DeBrujinAst {
@@ -95,7 +128,7 @@ impl From<DeBrujinBuiltInAst> 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(),
         }
     }
 }

src/exec/mod.rs

@@ -62,6 +62,12 @@ impl From<DeBrujinAst> for Ast {
 }
 
 impl DeBrujinAst {
+    pub fn reduce(self, builtins: &HashMap<String, Rc<dyn Builtin>>) -> 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,
-        }
-    }
 }

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::Variable("x".to_string())),
-                Box::new(Ast::Constant(Constant::Nat(5))),
-            )),
         )),
         Box::new(Ast::Variable("y".to_string())),
     );
     let dbast: DBAst = input.into();
-    let reduced = dbast.beta_reduce();
+    let reduced = dbast.reduce(&HashMap::new());
-    assert_eq!(
+    assert_eq!(reduced, DBAst::FreeVariable("y".to_string()))
-        reduced,
-        DBAst::Application(
-            Box::new(DBAst::FreeVariable("y".to_string())),
-            Box::new(DBAst::Constant(Constant::Nat(5))),
-        ),
-    )
 }
 
 #[test]
@@ -88,6 +79,57 @@ fn reduce_add() {
     .into();
     let mut builtins: HashMap<String, Rc<dyn Builtin>> = 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<String, Rc<dyn Builtin>> = HashMap::new();
+    builtins.insert("add".to_string(), Rc::new(AddOp));
+    let output = input.reduce(&builtins);
+    assert_eq!(output, DBAst::Constant(Constant::Nat(3)));
+}

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);
-            let ast = ast.reduce_builtins(&builtins);
             let ast: Ast = ast.into();
             println!("{ast} : {typ}")
         }