From e5d9aee00b0c775df1d8e2d8819aeb80dffa73c2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 1 Mar 2019 17:28:19 +0100 Subject: Split abnf_to_pest and dhall into their own crates --- dhall/src/typecheck.rs | 616 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 616 insertions(+) create mode 100644 dhall/src/typecheck.rs (limited to 'dhall/src/typecheck.rs') diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs new file mode 100644 index 0000000..62ff7d2 --- /dev/null +++ b/dhall/src/typecheck.rs @@ -0,0 +1,616 @@ +#![allow(non_snake_case)] +use std::collections::BTreeMap; +use std::collections::HashSet; +use std::fmt; + +use crate::context::Context; +use crate::core; +use crate::core::{Expr, V, X, bx, normalize, shift, subst}; +use crate::core::{pi, app}; +use crate::core::BuiltinType::*; +use crate::core::BuiltinValue::*; +use crate::core::Const::*; +use crate::core::Expr::*; + +use self::TypeMessage::*; + +fn axiom<'i, S: Clone>(c: core::Const) -> Result> { + match c { + Type => Ok(Kind), + Kind => Err(TypeError::new(&Context::new(), &Const(Kind), Untyped)), + } +} + +fn rule(a: core::Const, b: core::Const) -> Result { + match (a, b) { + (Type, Kind) => Err(()), + (Kind, Kind) => Ok(Kind), + (Type, Type) | + (Kind, Type) => Ok(Type), + } +} + +fn match_vars(vl: &V, vr: &V, ctx: &[(&str, &str)]) -> bool { + let xxs = ctx.get(0).map(|x| (x, ctx.split_at(1).1)); + match (vl, vr, xxs) { + (&V(xL, nL), &V(xR, nR), None) => xL == xR && nL == nR, + (&V(xL, 0), &V(xR, 0), Some((&(xL2, xR2), _))) if xL == xL2 && xR == xR2 => true, + (&V(xL, nL), &V(xR, nR), Some((&(xL2, xR2), xs))) => { + let nL2 = if xL == xL2 { nL - 1 } else { nL }; + let nR2 = if xR == xR2 { nR - 1 } else { nR }; + match_vars(&V(xL, nL2), &V(xR, nR2), xs) + } + } +} + +fn prop_equal(eL0: &Expr, eR0: &Expr) -> bool + where S: Clone + ::std::fmt::Debug, + T: Clone + ::std::fmt::Debug +{ + fn go<'i, S, T>(ctx: &mut Vec<(&'i str, &'i str)>, el: &'i Expr<'i, S, X>, er: &'i Expr<'i, T, X>) -> bool + where S: Clone + ::std::fmt::Debug, + T: Clone + ::std::fmt::Debug + { + match (el, er) { + (&Const(Type), &Const(Type)) | + (&Const(Kind), &Const(Kind)) => true, + (&Var(ref vL), &Var(ref vR)) => match_vars(vL, vR, &*ctx), + (&Pi(xL, ref tL, ref bL), &Pi(xR, ref tR, ref bR)) => { + //ctx <- State.get + let eq1 = go(ctx, tL, tR); + if eq1 { + //State.put ((xL, xR):ctx) + ctx.push((xL, xR)); + let eq2 = go(ctx, bL, bR); + //State.put ctx + let _ = ctx.pop(); + eq2 + } else { + false + } + } + (&App(ref fL, ref aL), &App(ref fR, ref aR)) => + if go(ctx, fL, fR) { go(ctx, aL, aR) } else { false }, + (&BuiltinType(a), &BuiltinType(b)) => a == b, + (&Record(ref ktsL0), &Record(ref ktsR0)) => { + if ktsL0.len() != ktsR0.len() { + return false; + } + /* + let go ((kL, tL):ktsL) ((kR, tR):ktsR) + | kL == kR = do + b <- go tL tR + if b + then go ktsL ktsR + else return False + go [] [] = return True + go _ _ = return False + */ + /* + for ((kL, tL), (kR, tR)) in ktsL0.iter().zip(ktsR0.iter()) { + if kL == kR { + if !go(ctx, tL, tR) { + return false; + } + } else { + return false; + } + } + true + */ + !ktsL0.iter().zip(ktsR0.iter()).any(|((kL, tL), (kR, tR))| { + kL != kR || !go(ctx, tL, tR) + }) + } + (&Union(ref ktsL0), &Union(ref ktsR0)) => { + if ktsL0.len() != ktsR0.len() { + return false; + } + /* + let loop ((kL, tL):ktsL) ((kR, tR):ktsR) + | kL == kR = do + b <- go tL tR + if b + then loop ktsL ktsR + else return False + loop [] [] = return True + loop _ _ = return False + loop (Data.Map.toList ktsL0) (Data.Map.toList ktsR0) + */ + !ktsL0.iter().zip(ktsR0.iter()).any(|((kL, tL), (kR, tR))| { + kL != kR || !go(ctx, tL, tR) + }) + } + (_, _) => false, + } + } + let mut ctx = vec![]; + go::(&mut ctx, &normalize(eL0), &normalize(eR0)) +} + +fn op2_type<'i, S, EF>(ctx: &Context<'i, Expr<'i, S, X>>, + e: &Expr<'i, S, X>, + t: core::BuiltinType, + ef: EF, + l: &Expr<'i, S, X>, + r: &Expr<'i, S, X>) + -> Result, TypeError<'i, S>> + where S: Clone + ::std::fmt::Debug + 'i, + EF: FnOnce(Expr<'i, S, X>, Expr<'i, S, X>) -> TypeMessage<'i, S>, +{ + let tl = normalize(&type_with(ctx, l)?); + match tl { + BuiltinType(lt) if lt == t => {} + _ => return Err(TypeError::new(ctx, e, ef((*l).clone(), tl))), + } + + let tr = normalize(&type_with(ctx, r)?); + match tr { + BuiltinType(rt) if rt == t => {} + _ => return Err(TypeError::new(ctx, e, ef((*r).clone(), tr))), + } + + Ok(BuiltinType(t)) +} + +/// Type-check an expression and return the expression'i type if type-checking +/// suceeds or an error if type-checking fails +/// +/// `type_with` does not necessarily normalize the type since full normalization +/// is not necessary for just type-checking. If you actually care about the +/// returned type then you may want to `normalize` it afterwards. +pub fn type_with<'i, S>(ctx: &Context<'i, Expr<'i, S, X>>, + e: &Expr<'i, S, X>) + -> Result, TypeError<'i, S>> + where S: Clone + ::std::fmt::Debug + 'i +{ + match *e { + Const(c) => axiom(c).map(Const), //.map(Cow::Owned), + Var(V(x, n)) => { + ctx.lookup(x, n) + .cloned() + //.map(Cow::Borrowed) + .ok_or_else(|| TypeError::new(ctx, e, UnboundVariable)) + } + Lam(x, ref tA, ref b) => { + let ctx2 = ctx.insert(x, (**tA).clone()).map(|e| core::shift(1, V(x, 0), e)); + let tB = type_with(&ctx2, b)?; + let p = Pi(x, tA.clone(), bx(tB)); + let _ = type_with(ctx, &p)?; + //Ok(Cow::Owned(p)) + Ok(p) + } + Pi(x, ref tA, ref tB) => { + let tA2 = normalize::(&type_with(ctx, tA)?); + let kA = match tA2 { + Const(k) => k, + _ => return Err(TypeError::new(ctx, e, InvalidInputType((**tA).clone()))), + }; + + let ctx2 = ctx.insert(x, (**tA).clone()).map(|e| core::shift(1, V(x, 0), e)); + let tB = normalize(&type_with(&ctx2, tB)?); + let kB = match tB { + Const(k) => k, + _ => return Err(TypeError::new(&ctx2, e, InvalidOutputType(tB))), + }; + + match rule(kA, kB) { + Err(()) => Err(TypeError::new(ctx, e, NoDependentTypes((**tA).clone(), tB))), + Ok(k) => Ok(Const(k)), + } + } + App(ref f, ref a) => { + let tf = normalize(&type_with(ctx, f)?); + let (x, tA, tB) = match tf { + Pi(x, tA, tB) => (x, tA, tB), + _ => return Err(TypeError::new(ctx, e, NotAFunction((**f).clone(), tf))), + }; + let tA2 = type_with(ctx, a)?; + if prop_equal(&tA, &tA2) { + let vx0 = V(x, 0); + let a2 = shift::( 1, vx0, a); + let tB2 = subst(vx0, &a2, &tB); + let tB3 = shift::(-1, vx0, &tB2); + Ok(tB3) + } else { + let nf_A = normalize(&tA); + let nf_A2 = normalize(&tA2); + Err(TypeError::new(ctx, e, TypeMismatch((**f).clone(), nf_A, (**a).clone(), nf_A2))) + } + } + Let(f, ref mt, ref r, ref b) => { + let tR = type_with(ctx, r)?; + let ttR = normalize::(&type_with(ctx, &tR)?); + let kR = match ttR { + Const(k) => k, + // Don't bother to provide a `let`-specific version of this error + // message because this should never happen anyway + _ => return Err(TypeError::new(ctx, e, InvalidInputType(tR))), + }; + + let ctx2 = ctx.insert(f, tR.clone()); + let tB = type_with(&ctx2, b)?; + let ttB = normalize::(&type_with(ctx, &tB)?); + let kB = match ttB { + Const(k) => k, + // Don't bother to provide a `let`-specific version of this error + // message because this should never happen anyway + _ => return Err(TypeError::new(ctx, e, InvalidOutputType(tB))), + }; + + if let Err(()) = rule(kR, kB) { + return Err(TypeError::new(ctx, e, NoDependentLet(tR, tB))); + } + + if let Some(ref t) = *mt { + let nf_t = normalize(t); + let nf_tR = normalize(&tR); + if !prop_equal(&nf_tR, &nf_t) { + return Err(TypeError::new(ctx, e, AnnotMismatch((**r).clone(), nf_t, nf_tR))); + } + } + + Ok(tB) + } + Annot(ref x, ref t) => { + // This is mainly just to check that `t` is not `Kind` + let _ = type_with(ctx, t)?; + + let t2 = type_with(ctx, x)?; + if prop_equal(t, &t2) { + Ok((**t).clone()) + } else { + let nf_t = normalize(t); + let nf_t2 = normalize(&t2); + Err(TypeError::new(ctx, e, AnnotMismatch((**x).clone(), nf_t, nf_t2))) + } + } + BuiltinType(t) => Ok(match t { + List | Optional => pi("_", Const(Type), Const(Type)), + Bool | Natural | Integer | Double | Text => Const(Type), + }), + BoolLit(_) => Ok(BuiltinType(Bool)), + BoolAnd(ref l, ref r) => op2_type(ctx, e, Bool, CantAnd, l, r), + BoolOr(ref l, ref r) => op2_type(ctx, e, Bool, CantOr, l, r), + BoolEQ(ref l, ref r) => op2_type(ctx, e, Bool, CantEQ, l, r), + BoolNE(ref l, ref r) => op2_type(ctx, e, Bool, CantNE, l, r), + BoolIf(ref x, ref y, ref z) => { + let tx = normalize(&type_with(ctx, x)?); + match tx { + BuiltinType(Bool) => {} + _ => return Err(TypeError::new(ctx, e, InvalidPredicate((**x).clone(), tx))), + } + let ty = normalize(&type_with(ctx, y)?); + let tty = normalize(&type_with(ctx, &ty)?); + match tty { + Const(Type) => {} + _ => return Err(TypeError::new(ctx, e, IfBranchMustBeTerm(true, (**y).clone(), ty, tty))), + } + + let tz = normalize(&type_with(ctx, z)?); + let ttz = normalize(&type_with(ctx, &tz)?); + match ttz { + Const(Type) => {} + _ => return Err(TypeError::new(ctx, e, IfBranchMustBeTerm(false, (**z).clone(), tz, ttz))), + } + + if !prop_equal(&ty, &tz) { + return Err(TypeError::new(ctx, e, IfBranchMismatch((**y).clone(), (**z).clone(), ty, tz))); + } + Ok(ty) + } + NaturalLit(_) => Ok(BuiltinType(Natural)), + BuiltinValue(NaturalFold) => + Ok(pi("_", Natural, + pi("natural", Const(Type), + pi("succ", pi("_", "natural", "natural"), + pi("zero", "natural", "natural"))))), + BuiltinValue(NaturalBuild) => + Ok(pi("_", + pi("natural", Const(Type), + pi("succ", pi("_", "natural", "natural"), + pi("zero", "natural", "natural"))), + Natural)), + BuiltinValue(NaturalIsZero) | + BuiltinValue(NaturalEven) | + BuiltinValue(NaturalOdd) => Ok(pi("_", Natural, Bool)), + NaturalPlus(ref l, ref r) => op2_type(ctx, e, Natural, CantAdd, l, r), + NaturalTimes(ref l, ref r) => op2_type(ctx, e, Natural, CantMultiply, l, r), + IntegerLit(_) => Ok(BuiltinType(Integer)), + DoubleLit(_) => Ok(BuiltinType(Double)), + TextLit(_) => Ok(BuiltinType(Text)), + TextAppend(ref l, ref r) => op2_type(ctx, e, Text, CantTextAppend, l, r), + ListLit(ref t, ref xs) => { + let s = normalize::<_, S, _>(&type_with(ctx, t)?); + match s { + Const(Type) => {} + _ => return Err(TypeError::new(ctx, e, InvalidListType((**t).clone()))), + } + for (i, x) in xs.iter().enumerate() { + let t2 = type_with(ctx, x)?; + if !prop_equal(t, &t2) { + let nf_t = normalize(t); + let nf_t2 = normalize(&t2); + return Err(TypeError::new(ctx, e, InvalidListElement(i, nf_t, x.clone(), nf_t2)) ) + } + } + Ok(App(bx(BuiltinType(List)), t.clone())) + } + BuiltinValue(ListBuild) => + Ok(pi("a", Const(Type), + pi("_", + pi("list", Const(Type), + pi("cons", pi("_", "a", pi("_", "list", "list")), + pi("nil", "list", "list"))), + app(List, "a")))), + BuiltinValue(ListFold) => + Ok(pi("a", Const(Type), + pi("_", app(List, "a"), + pi("list", Const(Type), + pi("cons", pi("_", "a", pi("_", "list", "list")), + pi("nil", "list", "list")))))), + BuiltinValue(ListLength) => + Ok(pi("a", Const(Type), pi("_", app(List, "a"), Natural))), + BuiltinValue(ListHead) | + BuiltinValue(ListLast) => + Ok(pi("a", Const(Type), pi("_", app(List, "a"), app(Optional, "a")))), + BuiltinValue(ListIndexed) => { + let mut m = BTreeMap::new(); + m.insert("index", BuiltinType(Natural)); + m.insert("value", Expr::from("a")); + Ok(pi("a", Const(Type), pi("_", app(List, "a"), app(List, Record(m))))) + } + BuiltinValue(ListReverse) => + Ok(pi("a", Const(Type), pi("_", app(List, "a"), app(List, "a")))), + OptionalLit(ref t, ref xs) => { + let s = normalize::<_, S, _>(&type_with(ctx, t)?); + match s { + Const(Type) => {} + _ => return Err(TypeError::new(ctx, e, InvalidOptionalType((**t).clone()))), + } + let n = xs.len(); + if 2 <= n { + return Err(TypeError::new(ctx, e, InvalidOptionalLiteral(n))); + } + for x in xs { + let t2 = type_with(ctx, x)?; + if !prop_equal(t, &t2) { + let nf_t = normalize(t); + let nf_t2 = normalize(&t2); + return Err(TypeError::new(ctx, e, InvalidOptionalElement(nf_t, x.clone(), nf_t2))); + } + } + Ok(App(bx(BuiltinType(Optional)), t.clone())) + } + BuiltinValue(OptionalFold) => + Ok(pi("a", Const(Type), + pi("_", app(Optional, "a"), + pi("optional", Const(Type), + pi("just", pi("_", "a", "optional"), + pi("nothing", "optional", "optional")))))), + Record(ref kts) => { + for (k, t) in kts { + let s = normalize::(&type_with(ctx, t)?); + match s { + Const(Type) => {} + _ => return Err(TypeError::new(ctx, e, InvalidFieldType((*k).to_owned(), (*t).clone()))), + } + } + Ok(Const(Type)) + } + RecordLit(ref kvs) => { + let kts = kvs.iter().map(|(&k, v)| { + let t = type_with(ctx, v)?; + let s = normalize::(&type_with(ctx, &t)?); + match s { + Const(Type) => {} + _ => return Err(TypeError::new(ctx, e, InvalidField((*k).to_owned(), (*v).clone()))), + } + Ok((k, t)) + }).collect::>()?; + Ok(Record(kts)) + } +/* +type_with ctx e@(Union kts ) = do + let process (k, t) = do + s <- fmap Dhall.Core.normalize (type_with ctx t) + case s of + Const Type -> return () + _ -> Left (TypeError ctx e (InvalidAlternativeType k t)) + mapM_ process (Data.Map.toList kts) + return (Const Type) +type_with ctx e@(UnionLit k v kts) = do + case Data.Map.lookup k kts of + Just _ -> Left (TypeError ctx e (DuplicateAlternative k)) + Nothing -> return () + t <- type_with ctx v + let union = Union (Data.Map.insert k t kts) + _ <- type_with ctx union + return union +type_with ctx e@(Combine kvsX kvsY) = do + tKvsX <- fmap Dhall.Core.normalize (type_with ctx kvsX) + ktsX <- case tKvsX of + Record kts -> return kts + _ -> Left (TypeError ctx e (MustCombineARecord kvsX tKvsX)) + + tKvsY <- fmap Dhall.Core.normalize (type_with ctx kvsY) + ktsY <- case tKvsY of + Record kts -> return kts + _ -> Left (TypeError ctx e (MustCombineARecord kvsY tKvsY)) + + let combineTypes ktsL ktsR = do + let ks = + Data.Set.union (Data.Map.keysSet ktsL) (Data.Map.keysSet ktsR) + kts <- forM (toList ks) (\k -> do + case (Data.Map.lookup k ktsL, Data.Map.lookup k ktsR) of + (Just (Record ktsL'), Just (Record ktsR')) -> do + t <- combineTypes ktsL' ktsR' + return (k, t) + (Nothing, Just t) -> do + return (k, t) + (Just t, Nothing) -> do + return (k, t) + _ -> do + Left (TypeError ctx e (FieldCollision k)) ) + return (Record (Data.Map.fromList kts)) + + combineTypes ktsX ktsY +type_with ctx e@(Merge kvsX kvsY t) = do + tKvsX <- fmap Dhall.Core.normalize (type_with ctx kvsX) + ktsX <- case tKvsX of + Record kts -> return kts + _ -> Left (TypeError ctx e (MustMergeARecord kvsX tKvsX)) + let ksX = Data.Map.keysSet ktsX + + tKvsY <- fmap Dhall.Core.normalize (type_with ctx kvsY) + ktsY <- case tKvsY of + Union kts -> return kts + _ -> Left (TypeError ctx e (MustMergeUnion kvsY tKvsY)) + let ksY = Data.Map.keysSet ktsY + + let diffX = Data.Set.difference ksX ksY + let diffY = Data.Set.difference ksY ksX + + if Data.Set.null diffX + then return () + else Left (TypeError ctx e (UnusedHandler diffX)) + + let process (kY, tY) = do + case Data.Map.lookup kY ktsX of + Nothing -> Left (TypeError ctx e (MissingHandler diffY)) + Just tX -> + case tX of + Pi _ tY' t' -> do + if prop_equal tY tY' + then return () + else Left (TypeError ctx e (HandlerInputTypeMismatch kY tY tY')) + if prop_equal t t' + then return () + else Left (TypeError ctx e (HandlerOutputTypeMismatch kY t t')) + _ -> Left (TypeError ctx e (HandlerNotAFunction kY tX)) + mapM_ process (Data.Map.toList ktsY) + return t + */ + Field(ref r, x) => { + let t = normalize(&type_with(ctx, r)?); + match t { + Record(ref kts) => + kts.get(x).cloned().ok_or_else(|| TypeError::new(ctx, e, MissingField(x.to_owned(), t.clone()))), + _ => Err(TypeError::new(ctx, e, NotARecord(x.to_owned(), (**r).clone(), t.clone()))), + } + } + /* +type_with ctx (Note s e' ) = case type_with ctx e' of + Left (TypeError ctx2 (Note s' e'') m) -> Left (TypeError ctx2 (Note s' e'') m) + Left (TypeError ctx2 e'' m) -> Left (TypeError ctx2 (Note s e'') m) + Right r -> Right r +*/ + Embed(p) => match p {}, + _ => panic!("Unimplemented typecheck case: {:?}", e), + } +} + +/// `typeOf` is the same as `type_with` with an empty context, meaning that the +/// expression must be closed (i.e. no free variables), otherwise type-checking +/// will fail. +pub fn type_of<'i, S: Clone + ::std::fmt::Debug + 'i>(e: &Expr<'i, S, X>) -> Result, TypeError<'i, S>> { + let ctx = Context::new(); + type_with(&ctx, e) //.map(|e| e.into_owned()) +} + +/// The specific type error +#[derive(Debug)] +pub enum TypeMessage<'i, S> { + UnboundVariable, + InvalidInputType(Expr<'i, S, X>), + InvalidOutputType(Expr<'i, S, X>), + NotAFunction(Expr<'i, S, X>, Expr<'i, S, X>), + TypeMismatch(Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>), + AnnotMismatch(Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>), + Untyped, + InvalidListElement(usize, Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>), + InvalidListType(Expr<'i, S, X>), + InvalidOptionalElement(Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>), + InvalidOptionalLiteral(usize), + InvalidOptionalType(Expr<'i, S, X>), + InvalidPredicate(Expr<'i, S, X>, Expr<'i, S, X>), + IfBranchMismatch(Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>), + IfBranchMustBeTerm(bool, Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>), + InvalidField(String, Expr<'i, S, X>), + InvalidFieldType(String, Expr<'i, S, X>), + InvalidAlternative(String, Expr<'i, S, X>), + InvalidAlternativeType(String, Expr<'i, S, X>), + DuplicateAlternative(String), + MustCombineARecord(Expr<'i, S, X>, Expr<'i, S, X>), + FieldCollision(String), + MustMergeARecord(Expr<'i, S, X>, Expr<'i, S, X>), + MustMergeUnion(Expr<'i, S, X>, Expr<'i, S, X>), + UnusedHandler(HashSet), + MissingHandler(HashSet), + HandlerInputTypeMismatch(String, Expr<'i, S, X>, Expr<'i, S, X>), + HandlerOutputTypeMismatch(String, Expr<'i, S, X>, Expr<'i, S, X>), + HandlerNotAFunction(String, Expr<'i, S, X>), + NotARecord(String, Expr<'i, S, X>, Expr<'i, S, X>), + MissingField(String, Expr<'i, S, X>), + CantAnd(Expr<'i, S, X>, Expr<'i, S, X>), + CantOr(Expr<'i, S, X>, Expr<'i, S, X>), + CantEQ(Expr<'i, S, X>, Expr<'i, S, X>), + CantNE(Expr<'i, S, X>, Expr<'i, S, X>), + CantTextAppend(Expr<'i, S, X>, Expr<'i, S, X>), + CantAdd(Expr<'i, S, X>, Expr<'i, S, X>), + CantMultiply(Expr<'i, S, X>, Expr<'i, S, X>), + NoDependentLet(Expr<'i, S, X>, Expr<'i, S, X>), + NoDependentTypes(Expr<'i, S, X>, Expr<'i, S, X>), +} + +/// A structured type error that includes context +#[derive(Debug)] +pub struct TypeError<'i, S> { + pub context: Context<'i, Expr<'i, S, X>>, + pub current: Expr<'i, S, X>, + pub type_message: TypeMessage<'i, S>, +} + +impl<'i, S: Clone> TypeError<'i, S> { + pub fn new(context: &Context<'i, Expr<'i, S, X>>, + current: &Expr<'i, S, X>, + type_message: TypeMessage<'i, S>) + -> Self { + TypeError { + context: context.clone(), + current: current.clone(), + type_message: type_message, + } + } +} + +impl<'i, S: fmt::Debug> ::std::error::Error for TypeMessage<'i, S> { + fn description(&self) -> &str { + match *self { + UnboundVariable => "Unbound variable", + InvalidInputType(_) => "Invalid function input", + InvalidOutputType(_) => "Invalid function output", + NotAFunction(_, _) => "Not a function", + TypeMismatch(_, _, _, _) => "Wrong type of function argument", + _ => "Unhandled error", + } + } +} + +impl<'i, S> fmt::Display for TypeMessage<'i, S> { + fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { + match *self { + UnboundVariable => f.write_str(include_str!("errors/UnboundVariable.txt")), + TypeMismatch(ref e0, ref e1, ref e2, ref e3) => { + let template = include_str!("errors/TypeMismatch.txt"); + let s = template + .replace("$txt0", &format!("{}", e0)) + .replace("$txt1", &format!("{}", e1)) + .replace("$txt2", &format!("{}", e2)) + .replace("$txt3", &format!("{}", e3)); + f.write_str(&s) + } + _ => f.write_str("Unhandled error message"), + } + } +} -- cgit v1.2.3