From 06798d622327707ca3f3b42d65fc3d1a25ae3c57 Mon Sep 17 00:00:00 2001 From: Joel Kronqvist Date: Sun, 10 Aug 2025 18:38:49 +0300 Subject: Added term level type literals (for function type signatures) --- src/type/check.rs | 22 ++++++++-------------- src/type/display.rs | 19 ++++++++++--------- src/type/mod.rs | 3 +++ src/type/subst.rs | 1 + 4 files changed, 22 insertions(+), 23 deletions(-) (limited to 'src/type') diff --git a/src/type/check.rs b/src/type/check.rs index 874db58..24c255d 100644 --- a/src/type/check.rs +++ b/src/type/check.rs @@ -67,8 +67,6 @@ impl SExp { /// sexp::{SExp::*, SLeaf::*, util::*}, /// }; /// - /// assert_eq!(Atom(Add).type_check(), Ok(arr(List(vec![Integer, Integer]), Integer))); - /// assert_eq!(Atom(Mul).type_check(), Ok(arr(List(vec![Integer, Integer]), Integer))); /// assert_eq!(Atom(Sub).type_check(), Ok(arr(List(vec![Integer, Integer]), Integer))); /// assert_eq!(Atom(Div).type_check(), Ok(arr(List(vec![Integer, Integer]), Integer))); /// assert_eq!(Atom(Eq) .type_check(), Ok(arr(List(vec![Integer, Integer]), Boolean))); @@ -112,15 +110,6 @@ impl SExp { /// sexp::{SExp::*, SLeaf::*, util::*}, /// }; /// - /// let err = scons(Mul, scons(1, Nil)).type_check(); - /// match err { - /// Err(InvalidArgList { .. }) => (), - /// _ => panic!( - /// "passing only 1 argument to '*' should result in InvalidArgList error, found '{:?}'", - /// err - /// ), - /// }; - /// /// match scons(Sub, scons(1, scons(2, scons(3, Nil)))).type_check() { /// Err(InvalidArgList { .. }) => (), /// _ => panic!( @@ -178,8 +167,8 @@ impl SExp { Atom(Var(name)) => ctx.get(name) .ok_or(UndefinedVariable(name.to_string())) .cloned(), - Atom(Add) => Ok(arr(List(vec![Integer, Integer]), Integer)), // TODO varlen - Atom(Mul) => Ok(arr(List(vec![Integer, Integer]), Integer)), // TODO varlen + Atom(Add) => Ok(arr(vecof(Integer), Integer)), + Atom(Mul) => Ok(arr(vecof(Integer), Integer)), Atom(Sub) => Ok(arr(List(vec![Integer, Integer]), Integer)), Atom(Div) => Ok(arr(List(vec![Integer, Integer]), Integer)), Atom(Eq | Neq | Lt | Gt | Le | Ge) => @@ -197,7 +186,8 @@ impl SExp { )), Atom(Let) => Ok(LetType), Atom(Print) => Ok(arr(vt("_"), List(vec![]))), - + Atom(Ty(_)) => Ok(TypeLit), + Atom(Arr) => Ok(arr(List(vec![TypeLit, TypeLit]), TypeLit)), SCons(op, l) => { @@ -218,6 +208,10 @@ impl SExp { let opertype = (*op).infer_type(ctx.clone())?; let argstype = (*l).infer_list_type(ctx)?; + if opertype == TypeLit && argstype.aka(&vecof(TypeLit)) { + return Ok(TypeLit); + } + let conv_args = match (opertype.clone(), argstype.clone()) { (Arrow(from, _), a) => match a.clone().into_type(&*from) { Ok(s) => Ok(s), diff --git a/src/type/display.rs b/src/type/display.rs index 72e3693..cd60673 100644 --- a/src/type/display.rs +++ b/src/type/display.rs @@ -10,19 +10,20 @@ impl fmt::Display for Type { /// Examples: /// ```rust /// use myslip::r#type::{Type::*, util::*}; - /// assert_eq!(Integer.to_string(), "Int".to_string()); - /// assert_eq!(Boolean.to_string(), "Bool".to_string()); - /// assert_eq!(arr(Integer, Boolean).to_string(), "(Int -> Bool)".to_string()); - /// assert_eq!(List(vec![Integer, Boolean, Integer]).to_string(), "(Int Bool Int)".to_string()); + /// assert_eq!(Integer.to_string(), "int".to_string()); + /// assert_eq!(Boolean.to_string(), "bool".to_string()); + /// assert_eq!(arr(Integer, Boolean).to_string(), "(int -> bool)".to_string()); + /// assert_eq!(List(vec![Integer, Boolean, Integer]).to_string(), "(int bool int)".to_string()); /// ``` fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { - Integer => write!(f, "{}", "Int"), - Boolean => write!(f, "{}", "Bool"), + Integer => write!(f, "{}", "int"), + Boolean => write!(f, "{}", "bool"), QuoteTy => write!(f, "{}", "Quote"), VecType => write!(f, "{}", "Vector"), LetType => write!(f, "{}", "Let"), NilType => write!(f, "()"), + TypeLit => write!(f, "[type literal]"), VecOf(ty) => write!(f, "({} ... {})", *ty, *ty), Arrow(a, b) => write!(f, "({} -> {})", a, b), List(types) => write!( @@ -57,7 +58,7 @@ impl fmt::Display for TypeError { /// expected: arr(VarType("?".to_string()), VarType("?".to_string())), /// found: Integer /// }.to_string(), - /// "invalid operator: '1'\nexpected: '(? -> ?)'\nfound: 'Int'".to_string() + /// "invalid operator: '1'\nexpected: '(? -> ?)'\nfound: 'int'".to_string() /// ); /// assert_eq!( /// InvalidArgList { @@ -65,7 +66,7 @@ impl fmt::Display for TypeError { /// expected: List(vec![Integer, Integer]), /// found: List(vec![Integer, Integer, Integer]), /// }.to_string(), - /// "invalid argument list: '(1 2 3)'\nexpected: '(Int Int)'\nfound: '(Int Int Int)'".to_string() + /// "invalid argument list: '(1 2 3)'\nexpected: '(int int)'\nfound: '(int int int)'".to_string() /// ); /// assert_eq!( /// UnboundGeneric(String::from("?")).to_string(), @@ -76,7 +77,7 @@ impl fmt::Display for TypeError { /// argtype: Integer, /// generictype: arr(VarType("T".to_string()), Integer) /// }.to_string(), - /// "incompatible argument type 'Int' and generic operator type '(T -> Int)'".to_string() + /// "incompatible argument type 'int' and generic operator type '(T -> int)'".to_string() /// ); /// ``` fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { diff --git a/src/type/mod.rs b/src/type/mod.rs index 9c2f89c..c138bba 100644 --- a/src/type/mod.rs +++ b/src/type/mod.rs @@ -17,6 +17,8 @@ pub enum Type { Boolean, + TypeLit, + QuoteTy, //constructor Arrow(Box, Box), @@ -111,6 +113,7 @@ impl Type { VecType => Ok(()), LetType => Ok(()), NilType => Ok(()), + TypeLit => Ok(()), Arrow(a, b) => b.is_concrete().and_then(|_ok| a.is_concrete()), List(v) => { let mut res = Ok(()); diff --git a/src/type/subst.rs b/src/type/subst.rs index ab9d38a..18c9926 100644 --- a/src/type/subst.rs +++ b/src/type/subst.rs @@ -45,6 +45,7 @@ impl Type { VecType => VecType, LetType => LetType, NilType => NilType, + TypeLit => TypeLit, } } -- cgit v1.2.3