From 9f69cfd65bc6800af886f2d8c0f79cd5cd3cea9c Mon Sep 17 00:00:00 2001 From: Avery Date: Thu, 20 Mar 2025 20:56:53 +0100 Subject: [PATCH] Small fixes and more builtins --- .../arith.rs} | 93 +--- src/exec/builtin_definitions/cmp.rs | 518 ++++++++++++++++++ src/exec/builtin_definitions/conditional.rs | 94 ++++ src/exec/builtin_definitions/mod.rs | 26 + src/inference/mod.rs | 1 + src/inference/unification.rs | 2 +- src/main.rs | 9 +- src/types/mod.rs | 4 +- 8 files changed, 647 insertions(+), 100 deletions(-) rename src/exec/{builtin_definitions.rs => builtin_definitions/arith.rs} (74%) create mode 100644 src/exec/builtin_definitions/cmp.rs create mode 100644 src/exec/builtin_definitions/conditional.rs create mode 100644 src/exec/builtin_definitions/mod.rs diff --git a/src/exec/builtin_definitions.rs b/src/exec/builtin_definitions/arith.rs similarity index 74% rename from src/exec/builtin_definitions.rs rename to src/exec/builtin_definitions/arith.rs index 2188661..b429df9 100644 --- a/src/exec/builtin_definitions.rs +++ b/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 { - 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 { - 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 { - Some(if self.0 { self.1.clone() } else { rhs }) - } -} diff --git a/src/exec/builtin_definitions/cmp.rs b/src/exec/builtin_definitions/cmp.rs new file mode 100644 index 0000000..59e04bd --- /dev/null +++ b/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 { + 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 { + 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 { + 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 { + 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 { + 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 { + 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 { + 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 { + 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 { + 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 { + 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 { + 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 { + 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 { + 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 { + 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 { + 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 { + 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 { + 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 { + match rhs { + DeBrujinBuiltInAst::Constant(Constant::Float(n)) => { + Some(DeBrujinBuiltInAst::Constant(Constant::Bool(self.0 != n))) + } + _ => None, + } + } +} diff --git a/src/exec/builtin_definitions/conditional.rs b/src/exec/builtin_definitions/conditional.rs new file mode 100644 index 0000000..590f40d --- /dev/null +++ b/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 { + 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 { + 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 { + Some(if self.0 { self.1.clone() } else { rhs }) + } +} diff --git a/src/exec/builtin_definitions/mod.rs b/src/exec/builtin_definitions/mod.rs new file mode 100644 index 0000000..58a2bc8 --- /dev/null +++ b/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> { + let mut builtins: HashMap> = 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 +} diff --git a/src/inference/mod.rs b/src/inference/mod.rs index 9d9d394..5dc838c 100644 --- a/src/inference/mod.rs +++ b/src/inference/mod.rs @@ -17,4 +17,5 @@ pub enum InferError { DoesNotFitTag(TypeTag, TaggedType), ConfilictingBind, ConfilictingTags, + UnusableConstraint, } diff --git a/src/inference/unification.rs b/src/inference/unification.rs index 9362dce..9f58e68 100644 --- a/src/inference/unification.rs +++ b/src/inference/unification.rs @@ -207,7 +207,7 @@ pub(super) fn step_2(mut eq_constraints: Constraints) -> Result> = HashMap::new(); - 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 builtins = builtin::all_builtins(); let mut gamma = HashMap::new(); for (k, v) in &builtins { gamma.insert(k.clone(), v.r#type()); diff --git a/src/types/mod.rs b/src/types/mod.rs index 0e31d18..73a4075 100644 --- a/src/types/mod.rs +++ b/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, }