Small fixes and more builtins

src/exec/builtin_definitions/arith.rs

@@ -1,15 +1,12 @@
 use std::rc::Rc;
 
 use crate::{
+    Builtin, DeBrujinAst,
+    exec::builtins::DeBrujinBuiltInAst,
     parse::Constant,
     types::{PrimitiveType, TaggedType, Type, TypeTag},
 };
 
-use super::{
-    DeBrujinAst,
-    builtins::{Builtin, DeBrujinBuiltInAst},
-};
-
 pub struct AddOp;
 struct AddOpNat(usize);
 struct AddOpFloat(f64);
@@ -264,89 +261,3 @@ impl Builtin for MulOpFloat {
         }
     }
 }
-
-pub struct OpCond;
-struct OpCond1(bool);
-struct OpCond2(bool, DeBrujinBuiltInAst);
-
-impl Builtin for OpCond {
-    fn name(&self) -> String {
-        "if".to_string()
-    }
-
-    fn r#type(&self) -> TaggedType {
-        TaggedType::Tagged(
-            TypeTag::Any,
-            "a".to_string(),
-            Box::new(TaggedType::Concrete(Type::arrow(
-                PrimitiveType::Bool,
-                Type::arrow("a", Type::arrow("a", "a")),
-            ))),
-        )
-    }
-
-    fn apply(&self, rhs: DeBrujinBuiltInAst) -> Option<DeBrujinBuiltInAst> {
-        match rhs {
-            DeBrujinBuiltInAst::Constant(Constant::Bool(b)) => {
-                Some(DeBrujinBuiltInAst::Builtin(Rc::new(OpCond1(b))))
-            }
-            _ => None,
-        }
-    }
-}
-
-impl Builtin for OpCond1 {
-    fn name(&self) -> String {
-        format!("if{}1", self.0)
-    }
-
-    fn r#type(&self) -> TaggedType {
-        TaggedType::Tagged(
-            TypeTag::Any,
-            "a".to_string(),
-            Box::new(TaggedType::Concrete(Type::arrow(
-                "a",
-                Type::arrow("a", "a"),
-            ))),
-        )
-    }
-
-    fn to_ast(&self) -> DeBrujinAst {
-        DeBrujinAst::Application(
-            Box::new(DeBrujinAst::FreeVariable("if".to_string())),
-            Box::new(DeBrujinAst::Constant(Constant::Bool(self.0))),
-        )
-    }
-
-    fn apply(&self, rhs: DeBrujinBuiltInAst) -> Option<DeBrujinBuiltInAst> {
-        Some(DeBrujinBuiltInAst::Builtin(Rc::new(OpCond2(self.0, rhs))))
-    }
-}
-
-impl Builtin for OpCond2 {
-    fn name(&self) -> String {
-        format!("if{}2", self.0)
-    }
-
-    fn r#type(&self) -> TaggedType {
-        TaggedType::Tagged(
-            TypeTag::Any,
-            "a".to_string(),
-            Box::new(TaggedType::Concrete(Type::arrow("a", "a"))),
-        )
-    }
-
-    fn to_ast(&self) -> DeBrujinAst {
-        DeBrujinAst::Application(
-            Box::new(DeBrujinAst::Application(
-                Box::new(DeBrujinAst::FreeVariable("if".to_string())),
-                Box::new(DeBrujinAst::Constant(Constant::Bool(self.0))),
-            )),
-            Box::new(self.1.clone().into()),
-        )
-    }
-
-    fn apply(&self, rhs: DeBrujinBuiltInAst) -> Option<DeBrujinBuiltInAst> {
-        Some(if self.0 { self.1.clone() } else { rhs })
-    }
-}

src/exec/builtin_definitions/cmp.rs

@@ -0,0 +1,518 @@
+use std::rc::Rc;
+
+use crate::{
+    Builtin, DeBrujinAst,
+    exec::builtins::DeBrujinBuiltInAst,
+    parse::Constant,
+    types::{PrimitiveType, TaggedType, Type, TypeTag},
+};
+
+pub struct LtOp;
+struct LtOpNat(usize);
+struct LtOpFloat(f64);
+
+impl Builtin for LtOp {
+    fn name(&self) -> String {
+        "lt".to_string()
+    }
+
+    fn r#type(&self) -> TaggedType {
+        TaggedType::Tagged(
+            TypeTag::Num,
+            "a".to_string(),
+            Box::new(TaggedType::Concrete(Type::arrow(
+                "a",
+                Type::arrow("a", PrimitiveType::Bool),
+            ))),
+        )
+    }
+
+    fn apply(&self, rhs: DeBrujinBuiltInAst) -> Option<DeBrujinBuiltInAst> {
+        match rhs {
+            DeBrujinBuiltInAst::Constant(Constant::Nat(n)) => {
+                Some(DeBrujinBuiltInAst::Builtin(Rc::new(LtOpNat(n))))
+            }
+            DeBrujinBuiltInAst::Constant(Constant::Float(n)) => {
+                Some(DeBrujinBuiltInAst::Builtin(Rc::new(LtOpFloat(n))))
+            }
+            _ => None,
+        }
+    }
+}
+
+impl Builtin for LtOpNat {
+    fn name(&self) -> String {
+        format!("lt{}", self.0)
+    }
+
+    fn to_ast(&self) -> DeBrujinAst {
+        DeBrujinAst::Application(
+            Box::new(DeBrujinAst::FreeVariable("lt".to_string())),
+            Box::new(DeBrujinAst::Constant(Constant::Nat(self.0))),
+        )
+    }
+
+    fn r#type(&self) -> TaggedType {
+        Type::arrow(PrimitiveType::Nat, PrimitiveType::Bool).into()
+    }
+
+    fn apply(&self, rhs: DeBrujinBuiltInAst) -> Option<DeBrujinBuiltInAst> {
+        match rhs {
+            DeBrujinBuiltInAst::Constant(Constant::Nat(n)) => {
+                Some(DeBrujinBuiltInAst::Constant(Constant::Bool(self.0 < n)))
+            }
+            _ => None,
+        }
+    }
+}
+
+impl Builtin for LtOpFloat {
+    fn name(&self) -> String {
+        format!("lt{}", self.0)
+    }
+
+    fn to_ast(&self) -> DeBrujinAst {
+        DeBrujinAst::Application(
+            Box::new(DeBrujinAst::FreeVariable("lt".to_string())),
+            Box::new(DeBrujinAst::Constant(Constant::Float(self.0))),
+        )
+    }
+
+    fn r#type(&self) -> TaggedType {
+        Type::arrow(PrimitiveType::Float, PrimitiveType::Bool).into()
+    }
+
+    fn apply(&self, rhs: DeBrujinBuiltInAst) -> Option<DeBrujinBuiltInAst> {
+        match rhs {
+            DeBrujinBuiltInAst::Constant(Constant::Float(n)) => {
+                Some(DeBrujinBuiltInAst::Constant(Constant::Bool(self.0 < n)))
+            }
+            _ => None,
+        }
+    }
+}
+
+pub struct LeOp;
+struct LeOpNat(usize);
+struct LeOpFloat(f64);
+
+impl Builtin for LeOp {
+    fn name(&self) -> String {
+        "le".to_string()
+    }
+
+    fn r#type(&self) -> TaggedType {
+        TaggedType::Tagged(
+            TypeTag::Num,
+            "a".to_string(),
+            Box::new(TaggedType::Concrete(Type::arrow(
+                "a",
+                Type::arrow("a", PrimitiveType::Bool),
+            ))),
+        )
+    }
+
+    fn apply(&self, rhs: DeBrujinBuiltInAst) -> Option<DeBrujinBuiltInAst> {
+        match rhs {
+            DeBrujinBuiltInAst::Constant(Constant::Nat(n)) => {
+                Some(DeBrujinBuiltInAst::Builtin(Rc::new(LeOpNat(n))))
+            }
+            DeBrujinBuiltInAst::Constant(Constant::Float(n)) => {
+                Some(DeBrujinBuiltInAst::Builtin(Rc::new(LeOpFloat(n))))
+            }
+            _ => None,
+        }
+    }
+}
+
+impl Builtin for LeOpNat {
+    fn name(&self) -> String {
+        format!("le{}", self.0)
+    }
+
+    fn to_ast(&self) -> DeBrujinAst {
+        DeBrujinAst::Application(
+            Box::new(DeBrujinAst::FreeVariable("le".to_string())),
+            Box::new(DeBrujinAst::Constant(Constant::Nat(self.0))),
+        )
+    }
+
+    fn r#type(&self) -> TaggedType {
+        Type::arrow(PrimitiveType::Nat, PrimitiveType::Bool).into()
+    }
+
+    fn apply(&self, rhs: DeBrujinBuiltInAst) -> Option<DeBrujinBuiltInAst> {
+        match rhs {
+            DeBrujinBuiltInAst::Constant(Constant::Nat(n)) => {
+                Some(DeBrujinBuiltInAst::Constant(Constant::Bool(self.0 <= n)))
+            }
+            _ => None,
+        }
+    }
+}
+
+impl Builtin for LeOpFloat {
+    fn name(&self) -> String {
+        format!("le{}", self.0)
+    }
+
+    fn to_ast(&self) -> DeBrujinAst {
+        DeBrujinAst::Application(
+            Box::new(DeBrujinAst::FreeVariable("le".to_string())),
+            Box::new(DeBrujinAst::Constant(Constant::Float(self.0))),
+        )
+    }
+
+    fn r#type(&self) -> TaggedType {
+        Type::arrow(PrimitiveType::Float, PrimitiveType::Bool).into()
+    }
+
+    fn apply(&self, rhs: DeBrujinBuiltInAst) -> Option<DeBrujinBuiltInAst> {
+        match rhs {
+            DeBrujinBuiltInAst::Constant(Constant::Float(n)) => {
+                Some(DeBrujinBuiltInAst::Constant(Constant::Bool(self.0 <= n)))
+            }
+            _ => None,
+        }
+    }
+}
+
+pub struct GtOp;
+struct GtOpNat(usize);
+struct GtOpFloat(f64);
+
+impl Builtin for GtOp {
+    fn name(&self) -> String {
+        "gt".to_string()
+    }
+
+    fn r#type(&self) -> TaggedType {
+        TaggedType::Tagged(
+            TypeTag::Num,
+            "a".to_string(),
+            Box::new(TaggedType::Concrete(Type::arrow(
+                "a",
+                Type::arrow("a", PrimitiveType::Bool),
+            ))),
+        )
+    }
+
+    fn apply(&self, rhs: DeBrujinBuiltInAst) -> Option<DeBrujinBuiltInAst> {
+        match rhs {
+            DeBrujinBuiltInAst::Constant(Constant::Nat(n)) => {
+                Some(DeBrujinBuiltInAst::Builtin(Rc::new(GtOpNat(n))))
+            }
+            DeBrujinBuiltInAst::Constant(Constant::Float(n)) => {
+                Some(DeBrujinBuiltInAst::Builtin(Rc::new(GtOpFloat(n))))
+            }
+            _ => None,
+        }
+    }
+}
+
+impl Builtin for GtOpNat {
+    fn name(&self) -> String {
+        format!("gt{}", self.0)
+    }
+
+    fn to_ast(&self) -> DeBrujinAst {
+        DeBrujinAst::Application(
+            Box::new(DeBrujinAst::FreeVariable("gt".to_string())),
+            Box::new(DeBrujinAst::Constant(Constant::Nat(self.0))),
+        )
+    }
+
+    fn r#type(&self) -> TaggedType {
+        Type::arrow(PrimitiveType::Nat, PrimitiveType::Bool).into()
+    }
+
+    fn apply(&self, rhs: DeBrujinBuiltInAst) -> Option<DeBrujinBuiltInAst> {
+        match rhs {
+            DeBrujinBuiltInAst::Constant(Constant::Nat(n)) => {
+                Some(DeBrujinBuiltInAst::Constant(Constant::Bool(self.0 > n)))
+            }
+            _ => None,
+        }
+    }
+}
+
+impl Builtin for GtOpFloat {
+    fn name(&self) -> String {
+        format!("gt{}", self.0)
+    }
+
+    fn to_ast(&self) -> DeBrujinAst {
+        DeBrujinAst::Application(
+            Box::new(DeBrujinAst::FreeVariable("gt".to_string())),
+            Box::new(DeBrujinAst::Constant(Constant::Float(self.0))),
+        )
+    }
+
+    fn r#type(&self) -> TaggedType {
+        Type::arrow(PrimitiveType::Float, PrimitiveType::Bool).into()
+    }
+
+    fn apply(&self, rhs: DeBrujinBuiltInAst) -> Option<DeBrujinBuiltInAst> {
+        match rhs {
+            DeBrujinBuiltInAst::Constant(Constant::Float(n)) => {
+                Some(DeBrujinBuiltInAst::Constant(Constant::Bool(self.0 > n)))
+            }
+            _ => None,
+        }
+    }
+}
+
+pub struct GeOp;
+struct GeOpNat(usize);
+struct GeOpFloat(f64);
+
+impl Builtin for GeOp {
+    fn name(&self) -> String {
+        "ge".to_string()
+    }
+
+    fn r#type(&self) -> TaggedType {
+        TaggedType::Tagged(
+            TypeTag::Num,
+            "a".to_string(),
+            Box::new(TaggedType::Concrete(Type::arrow(
+                "a",
+                Type::arrow("a", PrimitiveType::Bool),
+            ))),
+        )
+    }
+
+    fn apply(&self, rhs: DeBrujinBuiltInAst) -> Option<DeBrujinBuiltInAst> {
+        match rhs {
+            DeBrujinBuiltInAst::Constant(Constant::Nat(n)) => {
+                Some(DeBrujinBuiltInAst::Builtin(Rc::new(GeOpNat(n))))
+            }
+            DeBrujinBuiltInAst::Constant(Constant::Float(n)) => {
+                Some(DeBrujinBuiltInAst::Builtin(Rc::new(GeOpFloat(n))))
+            }
+            _ => None,
+        }
+    }
+}
+
+impl Builtin for GeOpNat {
+    fn name(&self) -> String {
+        format!("ge{}", self.0)
+    }
+
+    fn to_ast(&self) -> DeBrujinAst {
+        DeBrujinAst::Application(
+            Box::new(DeBrujinAst::FreeVariable("ge".to_string())),
+            Box::new(DeBrujinAst::Constant(Constant::Nat(self.0))),
+        )
+    }
+
+    fn r#type(&self) -> TaggedType {
+        Type::arrow(PrimitiveType::Nat, PrimitiveType::Bool).into()
+    }
+
+    fn apply(&self, rhs: DeBrujinBuiltInAst) -> Option<DeBrujinBuiltInAst> {
+        match rhs {
+            DeBrujinBuiltInAst::Constant(Constant::Nat(n)) => {
+                Some(DeBrujinBuiltInAst::Constant(Constant::Bool(self.0 >= n)))
+            }
+            _ => None,
+        }
+    }
+}
+
+impl Builtin for GeOpFloat {
+    fn name(&self) -> String {
+        format!("ge{}", self.0)
+    }
+
+    fn to_ast(&self) -> DeBrujinAst {
+        DeBrujinAst::Application(
+            Box::new(DeBrujinAst::FreeVariable("ge".to_string())),
+            Box::new(DeBrujinAst::Constant(Constant::Float(self.0))),
+        )
+    }
+
+    fn r#type(&self) -> TaggedType {
+        Type::arrow(PrimitiveType::Float, PrimitiveType::Bool).into()
+    }
+
+    fn apply(&self, rhs: DeBrujinBuiltInAst) -> Option<DeBrujinBuiltInAst> {
+        match rhs {
+            DeBrujinBuiltInAst::Constant(Constant::Float(n)) => {
+                Some(DeBrujinBuiltInAst::Constant(Constant::Bool(self.0 >= n)))
+            }
+            _ => None,
+        }
+    }
+}
+
+pub struct EqOp;
+struct EqOpNat(usize);
+struct EqOpFloat(f64);
+
+impl Builtin for EqOp {
+    fn name(&self) -> String {
+        "eq".to_string()
+    }
+
+    fn r#type(&self) -> TaggedType {
+        TaggedType::Tagged(
+            TypeTag::Num,
+            "a".to_string(),
+            Box::new(TaggedType::Concrete(Type::arrow(
+                "a",
+                Type::arrow("a", PrimitiveType::Bool),
+            ))),
+        )
+    }
+
+    fn apply(&self, rhs: DeBrujinBuiltInAst) -> Option<DeBrujinBuiltInAst> {
+        match rhs {
+            DeBrujinBuiltInAst::Constant(Constant::Nat(n)) => {
+                Some(DeBrujinBuiltInAst::Builtin(Rc::new(EqOpNat(n))))
+            }
+            DeBrujinBuiltInAst::Constant(Constant::Float(n)) => {
+                Some(DeBrujinBuiltInAst::Builtin(Rc::new(EqOpFloat(n))))
+            }
+            _ => None,
+        }
+    }
+}
+
+impl Builtin for EqOpNat {
+    fn name(&self) -> String {
+        format!("eq{}", self.0)
+    }
+
+    fn to_ast(&self) -> DeBrujinAst {
+        DeBrujinAst::Application(
+            Box::new(DeBrujinAst::FreeVariable("eq".to_string())),
+            Box::new(DeBrujinAst::Constant(Constant::Nat(self.0))),
+        )
+    }
+
+    fn r#type(&self) -> TaggedType {
+        Type::arrow(PrimitiveType::Nat, PrimitiveType::Bool).into()
+    }
+
+    fn apply(&self, rhs: DeBrujinBuiltInAst) -> Option<DeBrujinBuiltInAst> {
+        match rhs {
+            DeBrujinBuiltInAst::Constant(Constant::Nat(n)) => {
+                Some(DeBrujinBuiltInAst::Constant(Constant::Bool(self.0 == n)))
+            }
+            _ => None,
+        }
+    }
+}
+
+impl Builtin for EqOpFloat {
+    fn name(&self) -> String {
+        format!("eq{}", self.0)
+    }
+
+    fn to_ast(&self) -> DeBrujinAst {
+        DeBrujinAst::Application(
+            Box::new(DeBrujinAst::FreeVariable("eq".to_string())),
+            Box::new(DeBrujinAst::Constant(Constant::Float(self.0))),
+        )
+    }
+
+    fn r#type(&self) -> TaggedType {
+        Type::arrow(PrimitiveType::Float, PrimitiveType::Bool).into()
+    }
+
+    fn apply(&self, rhs: DeBrujinBuiltInAst) -> Option<DeBrujinBuiltInAst> {
+        match rhs {
+            DeBrujinBuiltInAst::Constant(Constant::Float(n)) => {
+                Some(DeBrujinBuiltInAst::Constant(Constant::Bool(self.0 == n)))
+            }
+            _ => None,
+        }
+    }
+}
+
+pub struct NeOp;
+struct NeOpNat(usize);
+struct NeOpFloat(f64);
+
+impl Builtin for NeOp {
+    fn name(&self) -> String {
+        "ne".to_string()
+    }
+
+    fn r#type(&self) -> TaggedType {
+        TaggedType::Tagged(
+            TypeTag::Num,
+            "a".to_string(),
+            Box::new(TaggedType::Concrete(Type::arrow(
+                "a",
+                Type::arrow("a", PrimitiveType::Bool),
+            ))),
+        )
+    }
+
+    fn apply(&self, rhs: DeBrujinBuiltInAst) -> Option<DeBrujinBuiltInAst> {
+        match rhs {
+            DeBrujinBuiltInAst::Constant(Constant::Nat(n)) => {
+                Some(DeBrujinBuiltInAst::Builtin(Rc::new(NeOpNat(n))))
+            }
+            DeBrujinBuiltInAst::Constant(Constant::Float(n)) => {
+                Some(DeBrujinBuiltInAst::Builtin(Rc::new(NeOpFloat(n))))
+            }
+            _ => None,
+        }
+    }
+}
+
+impl Builtin for NeOpNat {
+    fn name(&self) -> String {
+        format!("ne{}", self.0)
+    }
+
+    fn to_ast(&self) -> DeBrujinAst {
+        DeBrujinAst::Application(
+            Box::new(DeBrujinAst::FreeVariable("ne".to_string())),
+            Box::new(DeBrujinAst::Constant(Constant::Nat(self.0))),
+        )
+    }
+
+    fn r#type(&self) -> TaggedType {
+        Type::arrow(PrimitiveType::Nat, PrimitiveType::Bool).into()
+    }
+
+    fn apply(&self, rhs: DeBrujinBuiltInAst) -> Option<DeBrujinBuiltInAst> {
+        match rhs {
+            DeBrujinBuiltInAst::Constant(Constant::Nat(n)) => {
+                Some(DeBrujinBuiltInAst::Constant(Constant::Bool(self.0 != n)))
+            }
+            _ => None,
+        }
+    }
+}
+
+impl Builtin for NeOpFloat {
+    fn name(&self) -> String {
+        format!("ne{}", self.0)
+    }
+
+    fn to_ast(&self) -> DeBrujinAst {
+        DeBrujinAst::Application(
+            Box::new(DeBrujinAst::FreeVariable("ne".to_string())),
+            Box::new(DeBrujinAst::Constant(Constant::Float(self.0))),
+        )
+    }
+
+    fn r#type(&self) -> TaggedType {
+        Type::arrow(PrimitiveType::Float, PrimitiveType::Bool).into()
+    }
+
+    fn apply(&self, rhs: DeBrujinBuiltInAst) -> Option<DeBrujinBuiltInAst> {
+        match rhs {
+            DeBrujinBuiltInAst::Constant(Constant::Float(n)) => {
+                Some(DeBrujinBuiltInAst::Constant(Constant::Bool(self.0 != n)))
+            }
+            _ => None,
+        }
+    }
+}

src/exec/builtin_definitions/conditional.rs

@@ -0,0 +1,94 @@
+use std::rc::Rc;
+
+use crate::{
+    Builtin, DeBrujinAst,
+    exec::builtins::DeBrujinBuiltInAst,
+    parse::Constant,
+    types::{PrimitiveType, TaggedType, Type, TypeTag},
+};
+
+pub struct OpCond;
+struct OpCond1(bool);
+struct OpCond2(bool, DeBrujinBuiltInAst);
+
+impl Builtin for OpCond {
+    fn name(&self) -> String {
+        "if".to_string()
+    }
+
+    fn r#type(&self) -> TaggedType {
+        TaggedType::Tagged(
+            TypeTag::Any,
+            "a".to_string(),
+            Box::new(TaggedType::Concrete(Type::arrow(
+                PrimitiveType::Bool,
+                Type::arrow("a", Type::arrow("a", "a")),
+            ))),
+        )
+    }
+
+    fn apply(&self, rhs: DeBrujinBuiltInAst) -> Option<DeBrujinBuiltInAst> {
+        match rhs {
+            DeBrujinBuiltInAst::Constant(Constant::Bool(b)) => {
+                Some(DeBrujinBuiltInAst::Builtin(Rc::new(OpCond1(b))))
+            }
+            _ => None,
+        }
+    }
+}
+
+impl Builtin for OpCond1 {
+    fn name(&self) -> String {
+        format!("if{}1", self.0)
+    }
+
+    fn r#type(&self) -> TaggedType {
+        TaggedType::Tagged(
+            TypeTag::Any,
+            "a".to_string(),
+            Box::new(TaggedType::Concrete(Type::arrow(
+                "a",
+                Type::arrow("a", "a"),
+            ))),
+        )
+    }
+
+    fn to_ast(&self) -> DeBrujinAst {
+        DeBrujinAst::Application(
+            Box::new(DeBrujinAst::FreeVariable("if".to_string())),
+            Box::new(DeBrujinAst::Constant(Constant::Bool(self.0))),
+        )
+    }
+
+    fn apply(&self, rhs: DeBrujinBuiltInAst) -> Option<DeBrujinBuiltInAst> {
+        Some(DeBrujinBuiltInAst::Builtin(Rc::new(OpCond2(self.0, rhs))))
+    }
+}
+
+impl Builtin for OpCond2 {
+    fn name(&self) -> String {
+        format!("if{}2", self.0)
+    }
+
+    fn r#type(&self) -> TaggedType {
+        TaggedType::Tagged(
+            TypeTag::Any,
+            "a".to_string(),
+            Box::new(TaggedType::Concrete(Type::arrow("a", "a"))),
+        )
+    }
+
+    fn to_ast(&self) -> DeBrujinAst {
+        DeBrujinAst::Application(
+            Box::new(DeBrujinAst::Application(
+                Box::new(DeBrujinAst::FreeVariable("if".to_string())),
+                Box::new(DeBrujinAst::Constant(Constant::Bool(self.0))),
+            )),
+            Box::new(self.1.clone().into()),
+        )
+    }
+
+    fn apply(&self, rhs: DeBrujinBuiltInAst) -> Option<DeBrujinBuiltInAst> {
+        Some(if self.0 { self.1.clone() } else { rhs })
+    }
+}

src/exec/builtin_definitions/mod.rs

@@ -0,0 +1,26 @@
+mod arith;
+mod cmp;
+mod conditional;
+
+use std::{collections::HashMap, rc::Rc};
+
+pub use arith::{AddOp, MulOp, SubOp};
+pub use cmp::{EqOp, GeOp, GtOp, LeOp, LtOp, NeOp};
+pub use conditional::OpCond;
+
+use super::Builtin;
+
+pub fn all_builtins() -> HashMap<String, Rc<dyn Builtin>> {
+    let mut builtins: HashMap<String, Rc<dyn Builtin>> = HashMap::new();
+    builtins.insert("add".to_string(), Rc::new(AddOp));
+    builtins.insert("sub".to_string(), Rc::new(SubOp));
+    builtins.insert("mul".to_string(), Rc::new(MulOp));
+    builtins.insert("if".to_string(), Rc::new(OpCond));
+    builtins.insert("ge".to_string(), Rc::new(GeOp));
+    builtins.insert("gt".to_string(), Rc::new(GtOp));
+    builtins.insert("le".to_string(), Rc::new(LeOp));
+    builtins.insert("lt".to_string(), Rc::new(LtOp));
+    builtins.insert("eq".to_string(), Rc::new(EqOp));
+    builtins.insert("ne".to_string(), Rc::new(NeOp));
+    builtins
+}

src/inference/mod.rs

@@ -17,4 +17,5 @@ pub enum InferError {
     DoesNotFitTag(TypeTag, TaggedType),
     ConfilictingBind,
     ConfilictingTags,
+    UnusableConstraint,
 }

src/inference/unification.rs

@@ -207,7 +207,7 @@ pub(super) fn step_2(mut eq_constraints: Constraints<Type>) -> Result<Option<Sub
             eq_constraints.insert(s_rhs, t_rhs);
             step_2(eq_constraints)
         } else {
-            panic!()
+            Err(InferError::UnusableConstraint)
         }
     } else {
         Ok(None)

src/main.rs

@@ -1,11 +1,10 @@
 use std::{
     collections::{HashMap, hash_map},
     io::{Write, stdin, stdout},
-    rc::Rc,
 };
 
 use stlc_type_inference::{
-    Ast, Builtin, DeBrujinAst, builtin, infer_type_uni, parse_ast_str, parse_type_str,
+    Ast, DeBrujinAst, builtin, infer_type_uni, parse_ast_str, parse_type_str,
 };
 
 macro_rules! repl_err {
@@ -18,11 +17,7 @@ macro_rules! repl_err {
 }
 
 fn main() {
-    let mut builtins: HashMap<String, Rc<dyn Builtin>> = HashMap::new();
+    let builtins = builtin::all_builtins();
-    builtins.insert("add".to_string(), Rc::new(builtin::AddOp));
-    builtins.insert("sub".to_string(), Rc::new(builtin::SubOp));
-    builtins.insert("mul".to_string(), Rc::new(builtin::MulOp));
-    builtins.insert("if".to_string(), Rc::new(builtin::OpCond));
     let mut gamma = HashMap::new();
     for (k, v) in &builtins {
         gamma.insert(k.clone(), v.r#type());

src/types/mod.rs

@@ -257,7 +257,9 @@ impl Type {
             Type::Variable(_) => true,
             Type::Primitive(primitive_type) => matches!(
                 (primitive_type, tag),
-                (_, TypeTag::Any) | (PrimitiveType::Nat, TypeTag::Num)
+                (_, TypeTag::Any)
+                    | (PrimitiveType::Nat, TypeTag::Num)
+                    | (PrimitiveType::Float, TypeTag::Num)
             ),
             Type::Arrow(_, _) => false,
         }