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 --- src/typecheck.rs | 616 ------------------------------------------------------- 1 file changed, 616 deletions(-) delete mode 100644 src/typecheck.rs (limited to 'src/typecheck.rs') diff --git a/src/typecheck.rs b/src/typecheck.rs deleted file mode 100644 index 62ff7d2..0000000 --- a/src/typecheck.rs +++ /dev/null @@ -1,616 +0,0 @@ -#![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