diff options
Diffstat (limited to 'src/type')
| -rw-r--r-- | src/type/case.rs | 18 | ||||
| -rw-r--r-- | src/type/check.rs | 43 | ||||
| -rw-r--r-- | src/type/display.rs | 1 | ||||
| -rw-r--r-- | src/type/mod.rs | 5 | ||||
| -rw-r--r-- | src/type/subst.rs | 2 | ||||
| -rw-r--r-- | src/type/util.rs | 4 |
6 files changed, 72 insertions, 1 deletions
diff --git a/src/type/case.rs b/src/type/case.rs index c53bbd0..d8871af 100644 --- a/src/type/case.rs +++ b/src/type/case.rs @@ -324,4 +324,22 @@ mod tests { Ok(vec![]) ); } + + #[test] + fn test_sumtype_match() { + assert_eq!( + scons(Inl, scons(var("x"), Nil)).matches_type(&sumtype(Integer, Boolean)), + Ok(vec![("x".to_string(), Integer)]) + ); + assert_eq!( + scons(Inr, scons(var("x"), Nil)).matches_type(&sumtype(Integer, Boolean)), + Ok(vec![("x".to_string(), Boolean)]) + ); + assert!( + scons(Inl, scons(True, Nil)).matches_type(&sumtype(Integer, Boolean)).is_err() + ); + assert!( + scons(Inr, scons(1, Nil)).matches_type(&sumtype(Integer, Boolean)).is_err() + ); + } } diff --git a/src/type/check.rs b/src/type/check.rs index c0f4b1f..96a4408 100644 --- a/src/type/check.rs +++ b/src/type/check.rs @@ -60,6 +60,25 @@ impl SExp { /// ``` /// ...so please don't ask what their type is. /// + /// **Sum types** + /// + /// Instantiation types: + /// ```rust + /// use myslip::{ + /// r#type::{*, Type::*, TypeError::*, util::*}, + /// sexp::{SExp::*, SLeaf::*, util::*}, + /// }; + /// assert_eq!( + /// scons(Coprod, scons(7, scons(Ty(Boolean), Nil))).type_check(), + /// Ok(sumtype(Integer, Boolean)) + /// ); + /// assert_eq!( + /// scons(Coprod, scons(Ty(Boolean), scons(False, Nil))).type_check(), + /// Ok(sumtype(Boolean, Boolean)) + /// ); + /// ``` + /// Destructuring is tested in the tests of case. + /// /// Some common operators get arrow types: /// ```rust /// use myslip::{ @@ -161,7 +180,28 @@ impl SExp { /// Ok(Integer) /// ); /// ``` + /// + /// Here's a test on pattern matching on sum types: + /// ```rust + /// use myslip::{ + /// r#type::{*, Type::*, TypeError::*, util::*}, + /// sexp::{SExp::*, SLeaf::*, util::*}, + /// parse::parsetree::parse_to_ast + /// }; /// + /// fn main() { + /// let exp = parse_to_ast( + /// "(let mysum (coprod Bool 7)) \ + /// (case mysum \ + /// ((inl b) (if b 0 1)) \ + /// ((inr x) x))" + /// ).unwrap(); + /// assert_eq!( + /// exp.type_check(), + /// Ok(Integer) + /// ); + /// } + /// ``` /// /// Though perhaps the most important task of the type system /// is to increase safety by being able to warn about errors @@ -260,6 +300,9 @@ impl SExp { vecof(vt("T")), List(vec![VecType, vecof(vt("T"))]) )), + Atom(Coprod) => todo!(), + Atom(Inl) => todo!(), + Atom(Inr) => todo!(), Atom(Let) => Ok(LetType), Atom(Print) => Ok(arr(vt("_"), NilType)), Atom(Ty(_)) => Ok(TypeLit), diff --git a/src/type/display.rs b/src/type/display.rs index a2f4b58..99394df 100644 --- a/src/type/display.rs +++ b/src/type/display.rs @@ -35,6 +35,7 @@ impl fmt::Display for Type { TypeLit => write!(f, "Type"), VecOf(ty) => write!(f, "({} ...)", *ty), Arrow(a, b) => write!(f, "({} -> {})", a, b), + SumType(a,b)=> write!(f, "(Sum {} {})", a, b), List(types) => write!( f, "({})", diff --git a/src/type/mod.rs b/src/type/mod.rs index bfe0055..c726001 100644 --- a/src/type/mod.rs +++ b/src/type/mod.rs @@ -31,6 +31,8 @@ pub enum Type { VecOf(Box<Type>), VecType, // constructor + SumType(Box<Type>, Box<Type>), + LetType, /// Type for generics @@ -156,7 +158,8 @@ impl Type { LetType => Ok(()), NilType => Ok(()), TypeLit => Ok(()), - Arrow(a, b) => b.is_concrete().and_then(|_ok| a.is_concrete()), + Arrow(a, b) => b.is_concrete().and_then(|_ok| a.is_concrete()), + SumType(a, b) => b.is_concrete().and_then(|_ok| a.is_concrete()), List(v) => { let mut res = Ok(()); for t in v { diff --git a/src/type/subst.rs b/src/type/subst.rs index 18c9926..fd45005 100644 --- a/src/type/subst.rs +++ b/src/type/subst.rs @@ -27,6 +27,8 @@ impl Type { Arrow(a, b) => arr((*a).subst(name, value), (*b).subst(name, value)), + SumType(a, b) => sumtype((*a).subst(name, value), (*b).subst(name, value)), + List(v) => List( v.into_iter() .map(|t| t.subst(name, value)) diff --git a/src/type/util.rs b/src/type/util.rs index 04b4ee6..0ea1e4d 100644 --- a/src/type/util.rs +++ b/src/type/util.rs @@ -6,6 +6,10 @@ pub fn arr(a: impl Into<Box<Type>>, b: impl Into<Box<Type>>) -> Type { Arrow(a.into(), b.into()) } +pub fn sumtype(a: impl Into<Box<Type>>, b: impl Into<Box<Type>>) -> Type { + SumType(a.into(), b.into()) +} + pub fn vt(name: &str) -> Type { VarType(name.to_string()) } |