From d1c97e405230b6616ef834cf38be351e566a228e Mon Sep 17 00:00:00 2001 From: Joel Kronqvist Date: Thu, 21 Aug 2025 12:35:37 +0300 Subject: feat: implemented coproducts according to tests --- src/type/check.rs | 25 ++++++++++++++++++++----- 1 file changed, 20 insertions(+), 5 deletions(-) (limited to 'src/type/check.rs') diff --git a/src/type/check.rs b/src/type/check.rs index 96a4408..5ccd0e7 100644 --- a/src/type/check.rs +++ b/src/type/check.rs @@ -193,8 +193,9 @@ impl SExp { /// let exp = parse_to_ast( /// "(let mysum (coprod Bool 7)) \ /// (case mysum \ - /// ((inl b) (if b 0 1)) \ - /// ((inr x) x))" + /// ((inl b) (case b (true 0) (_ 1))) \ + /// ((inr x) x) \ + /// (_ 0))" /// ).unwrap(); /// assert_eq!( /// exp.type_check(), @@ -300,9 +301,9 @@ impl SExp { vecof(vt("T")), List(vec![VecType, vecof(vt("T"))]) )), - Atom(Coprod) => todo!(), - Atom(Inl) => todo!(), - Atom(Inr) => todo!(), + Atom(Coprod) => Err(OtherError), // TODO + Atom(Inl) => Err(OtherError), // TODO + Atom(Inr) => Err(OtherError), // TODO Atom(Let) => Ok(LetType), Atom(Print) => Ok(arr(vt("_"), NilType)), Atom(Ty(_)) => Ok(TypeLit), @@ -379,6 +380,20 @@ impl SExp { } } + // Coproducts + if **op == Atom(Coprod) { + let mut parts = (**l).clone().parts().into_iter(); + return match (parts.next(), parts.next(), parts.next()) { + (Some(Atom(Ty(ty))), Some(r), None) + => Ok(sumtype(ty, r.infer_type(ctx)?)), + (Some(l), Some(Atom(Ty(ty))), None) + => Ok(sumtype(l.infer_type(ctx)?, ty)), + (Some(l), Some(r), None) + => Err(SumDefNoTypeLiteral(scons(l, r))), + _ => Err(OtherError) + }; + } + // Normal operation let opertype = (*op).infer_type(ctx.clone())?; let argstype = (*l).infer_list_type(ctx)?; -- cgit v1.2.3