From d6e5c277e061d61b793286fb0ff2100cf203df89 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 18 Mar 2019 02:08:26 +0100 Subject: Improve ergonomics of typechecking --- dhall/src/typecheck.rs | 602 ++++++++++++++++++++----------------------------- 1 file changed, 248 insertions(+), 354 deletions(-) (limited to 'dhall/src/typecheck.rs') diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 15629a9..26ab360 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -5,24 +5,24 @@ use std::fmt; use std::rc::Rc; use crate::normalize::normalize; +use dhall_core; use dhall_core::context::Context; -use dhall_core::core; -use dhall_core::core::Builtin::*; -use dhall_core::core::Const::*; -use dhall_core::core::Expr::*; -use dhall_core::core::{bx, rc, shift, subst, Expr, Label, V, X}; +use dhall_core::*; use dhall_generator::dhall_expr; use self::TypeMessage::*; -fn axiom(c: core::Const) -> Result> { +fn axiom(c: Const) -> Result> { + use dhall_core::Const::*; + use dhall_core::Expr::*; match c { Type => Ok(Kind), Kind => Err(TypeError::new(&Context::new(), rc(Const(Kind)), Untyped)), } } -fn rule(a: &core::Const, b: &core::Const) -> Result { +fn rule(a: Const, b: Const) -> Result { + use dhall_core::Const::*; match (a, b) { (Type, Kind) => Err(()), (Kind, Kind) => Ok(Kind), @@ -31,46 +31,51 @@ fn rule(a: &core::Const, b: &core::Const) -> Result { } fn match_vars(vl: &V, vr: &V, ctx: &[(Label, Label)]) -> bool { - let xxs: Option<(&(Label, Label), &[(Label, Label)])> = ctx.split_first(); - 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.clone(), nL2), &V(xR.clone(), nR2), xs) + let mut vl = vl.clone(); + let mut vr = vr.clone(); + let mut ctx = ctx.to_vec(); + ctx.reverse(); + while let Some((xL2, xR2)) = &ctx.pop() { + match (&vl, &vr) { + (V(xL, 0), V(xR, 0)) if xL == xL2 && xR == xR2 => return true, + (V(xL, nL), V(xR, nR)) => { + let nL2 = if xL == xL2 { nL - 1 } else { *nL }; + let nR2 = if xR == xR2 { nR - 1 } else { *nR }; + vl = V(xL.clone(), nL2); + vr = V(xR.clone(), nR2); + } } } + vl == vr } -fn prop_equal(eL0: Rc>, eR0: Rc>) -> bool +// Takes normalized expressions as input +fn prop_equal(eL0: &Expr, eR0: &Expr) -> bool where S: ::std::fmt::Debug, T: ::std::fmt::Debug, { + use dhall_core::Expr::*; fn go( ctx: &mut Vec<(Label, Label)>, - el: Rc>, - er: Rc>, + el: &Expr, + er: &Expr, ) -> bool where S: ::std::fmt::Debug, T: ::std::fmt::Debug, { - match (el.as_ref(), er.as_ref()) { - (&Const(Type), &Const(Type)) | (&Const(Kind), &Const(Kind)) => true, + match (el, er) { + (&Const(a), &Const(b)) => a == b, + (&Builtin(a), &Builtin(b)) => a == b, (&Var(ref vL), &Var(ref vR)) => match_vars(vL, vR, ctx), (&Pi(ref xL, ref tL, ref bL), &Pi(ref xR, ref tR, ref bR)) => { //ctx <- State.get - let eq1 = go(ctx, Rc::clone(tL), Rc::clone(tR)); + let eq1 = go(ctx, tL.as_ref(), tR.as_ref()); if eq1 { //State.put ((xL, xR):ctx) ctx.push((xL.clone(), xR.clone())); - let eq2 = go(ctx, Rc::clone(bL), Rc::clone(bR)); + let eq2 = go(ctx, bL.as_ref(), bR.as_ref()); //State.put ctx let _ = ctx.pop(); eq2 @@ -79,96 +84,100 @@ where } } (&App(ref fL, ref aL), &App(ref fR, ref aR)) => { - if go(ctx, Rc::clone(fL), Rc::clone(fR)) { - aL.iter() + go(ctx, fL.as_ref(), fR.as_ref()) + && aL.len() == aR.len() + && aL + .iter() .zip(aR.iter()) - .all(|(aL, aR)| go(ctx, Rc::clone(aL), Rc::clone(aR))) - } else { - false - } + .all(|(aL, aR)| go(ctx, aL.as_ref(), aR.as_ref())) } - (&Builtin(a), &Builtin(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, Rc::clone(tL), Rc::clone(tR)) - }) + ktsL0.len() == ktsR0.len() + && ktsL0.iter().zip(ktsR0.iter()).all( + |((kL, tL), (kR, tR))| { + kL == kR && go(ctx, tL.as_ref(), tR.as_ref()) + }, + ) } (&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, Rc::clone(tL), Rc::clone(tR)) - }) + ktsL0.len() == ktsR0.len() + && ktsL0.iter().zip(ktsR0.iter()).all( + |((kL, tL), (kR, tR))| { + kL == kR && go(ctx, tL.as_ref(), tR.as_ref()) + }, + ) } (_, _) => false, } } let mut ctx = vec![]; - go::(&mut ctx, normalize(eL0), normalize(eR0)) + go::(&mut ctx, eL0, eR0) } -fn op2_type( - ctx: &Context>>, - e: Rc>, - t: core::Builtin, - ef: EF, - l: &Rc>, - r: &Rc>, -) -> Result, TypeError> -where - S: ::std::fmt::Debug, - EF: FnOnce(Rc>, Rc>) -> TypeMessage, -{ - let tl = normalize(type_with(ctx, l.clone())?); - match *tl { - Builtin(lt) if lt == t => {} - _ => return Err(TypeError::new(ctx, e, ef(l.clone(), tl))), - } - - let tr = normalize(type_with(ctx, r.clone())?); - match *tr { - Builtin(rt) if rt == t => {} - _ => return Err(TypeError::new(ctx, e, ef(r.clone(), tr))), +fn type_of_builtin(b: Builtin) -> Rc> { + use dhall_core::Builtin::*; + use dhall_core::Const::*; + use dhall_core::Expr::*; + match b { + Bool | Natural | Integer | Double | Text => dhall_expr!(Type), + List | Optional => dhall_expr!( + Type -> Type + ), + NaturalFold => dhall_expr!( + Natural -> + forall (natural: Type) -> + forall (succ: natural -> natural) -> + forall (zero: natural) -> + natural + ), + NaturalBuild => dhall_expr!( + (forall (natural: Type) -> + forall (succ: natural -> natural) -> + forall (zero: natural) -> + natural) -> + Natural + ), + NaturalIsZero | NaturalEven | NaturalOdd => dhall_expr!( + Natural -> Bool + ), + ListBuild => dhall_expr!( + forall (a: Type) -> + (forall (list: Type) -> + forall (cons: a -> list -> list) -> + forall (nil: list) -> + list) -> + List a + ), + ListFold => dhall_expr!( + forall (a: Type) -> + List a -> + forall (list: Type) -> + forall (cons: a -> list -> list) -> + forall (nil: list) -> + list + ), + ListLength => dhall_expr!(forall (a: Type) -> List a -> Natural), + ListHead | ListLast => { + dhall_expr!(forall (a: Type) -> List a -> Optional a) + } + ListIndexed => dhall_expr!( + forall (a: Type) -> + List a -> + List { index: Natural, value: a } + ), + ListReverse => dhall_expr!( + forall (a: Type) -> List a -> List a + ), + OptionalFold => dhall_expr!( + forall (a: Type) -> + Optional a -> + forall (optional: Type) -> + forall (just: a -> optional) -> + forall (nothing: optional) -> + optional + ), + _ => panic!("Unimplemented typecheck case: {:?}", b), } - - Ok(Builtin(t)) } /// Type-check an expression and return the expression'i type if type-checking @@ -185,17 +194,31 @@ where S: ::std::fmt::Debug, { use dhall_core::BinOp::*; + use dhall_core::Builtin::*; + use dhall_core::Const::*; use dhall_core::Expr; + use dhall_core::Expr::*; let mkerr = |msg: TypeMessage<_>| TypeError::new(ctx, e.clone(), msg); - match *e { - Const(c) => axiom(c).map(Const), - Var(V(ref x, n)) => { + let ensure_const = |x: &SubExpr<_, _>, msg: TypeMessage<_>| match x.as_ref() + { + Const(k) => Ok(*k), + _ => Err(mkerr(msg)), + }; + let ensure_is_type = + |x: SubExpr<_, _>, msg: TypeMessage<_>| match x.as_ref() { + Const(Type) => Ok(()), + _ => Err(mkerr(msg)), + }; + + match e.as_ref() { + Const(c) => axiom(*c).map(Const), + Var(V(x, n)) => { return ctx - .lookup(x, n) + .lookup(x, *n) .cloned() .ok_or_else(|| mkerr(UnboundVariable)) } - Lam(ref x, ref tA, ref b) => { + Lam(x, tA, b) => { let ctx2 = ctx .insert(x.clone(), tA.clone()) .map(|e| shift(1, &V(x.clone(), 0), e)); @@ -204,21 +227,16 @@ where let _ = type_with(ctx, p.clone())?; return Ok(p); } - Pi(ref x, ref tA, ref tB) => { - let tA2 = normalize(type_with(ctx, tA.clone())?); - let kA = match tA2.as_ref() { - Const(k) => k, - _ => { - return Err(mkerr(InvalidInputType(tA.clone()))); - } - }; + Pi(x, tA, tB) => { + let tA2 = normalized_type_with(ctx, tA.clone())?; + let kA = ensure_const(&tA2, InvalidInputType(tA.clone()))?; let ctx2 = ctx .insert(x.clone(), tA.clone()) .map(|e| shift(1, &V(x.clone(), 0), e)); - let tB = normalize(type_with(&ctx2, tB.clone())?); + let tB = normalized_type_with(&ctx2, tB.clone())?; let kB = match tB.as_ref() { - Const(k) => k, + Const(k) => *k, _ => { return Err(TypeError::new( &ctx2, @@ -230,19 +248,19 @@ where match rule(kA, kB) { Err(()) => Err(mkerr(NoDependentTypes(tA.clone(), tB))), - Ok(k) => Ok(Const(k)), + Ok(_) => Ok(Const(kB)), } } - App(ref f, ref args) => { + App(f, args) => { // Recurse on args let (a, tf) = match args.split_last() { None => return type_with(ctx, f.clone()), Some((a, args)) => ( a, - normalize(type_with( + normalized_type_with( ctx, rc(App(f.clone(), args.to_vec())), - )?), + )?, ), }; let (x, tA, tB) = match tf.as_ref() { @@ -251,116 +269,79 @@ where return Err(mkerr(NotAFunction(f.clone(), tf))); } }; - let tA2 = type_with(ctx, a.clone())?; - if prop_equal(tA.clone(), tA2.clone()) { + let tA = normalize(Rc::clone(tA)); + let tA2 = normalized_type_with(ctx, a.clone())?; + if prop_equal(tA.as_ref(), tA2.as_ref()) { let vx0 = &V(x.clone(), 0); let a2 = shift(1, vx0, a); let tB2 = subst(vx0, &a2, &tB); let tB3 = shift(-1, vx0, &tB2); return Ok(tB3); } else { - let nf_A = normalize(tA.clone()); - let nf_A2 = normalize(tA2); - Err(mkerr(TypeMismatch(f.clone(), nf_A, a.clone(), nf_A2))) + Err(mkerr(TypeMismatch(f.clone(), tA, a.clone(), tA2))) } } - Let(ref f, ref mt, ref r, ref b) => { - let tR = type_with(ctx, r.clone())?; - let ttR = normalize(type_with(ctx, tR.clone())?); - let kR = match ttR.as_ref() { - Const(k) => k, - // Don't bother to provide a `let`-specific version of this error - // message because this should never happen anyway - _ => return Err(mkerr(InvalidInputType(tR))), + Let(f, mt, r, b) => { + let r = if let Some(t) = mt { + rc(Annot(Rc::clone(r), Rc::clone(t))) + } else { + Rc::clone(r) }; + let tR = type_with(ctx, r)?; + let ttR = normalized_type_with(ctx, tR.clone())?; + // Don't bother to provide a `let`-specific version of this error + // message because this should never happen anyway + let kR = ensure_const(&ttR, InvalidInputType(tR.clone()))?; + let ctx2 = ctx.insert(f.clone(), tR.clone()); let tB = type_with(&ctx2, b.clone())?; - let ttB = normalize(type_with(ctx, tB.clone())?); - let kB = match ttB.as_ref() { - Const(k) => k, - // Don't bother to provide a `let`-specific version of this error - // message because this should never happen anyway - _ => return Err(mkerr(InvalidOutputType(tB))), - }; + let ttB = normalized_type_with(ctx, tB.clone())?; + // Don't bother to provide a `let`-specific version of this error + // message because this should never happen anyway + let kB = ensure_const(&ttB, InvalidOutputType(tB.clone()))?; if let Err(()) = rule(kR, kB) { return Err(mkerr(NoDependentLet(tR, tB))); } - if let Some(ref t) = *mt { - let nf_t = normalize(t.clone()); - let nf_tR = normalize(tR); - if !prop_equal(nf_tR.clone(), nf_t.clone()) { - return Err(mkerr(AnnotMismatch(r.clone(), nf_t, nf_tR))); - } - } - return Ok(tB); } - Annot(ref x, ref t) => { + Annot(x, t) => { // This is mainly just to check that `t` is not `Kind` let _ = type_with(ctx, t.clone())?; - let t2 = type_with(ctx, x.clone())?; - if prop_equal(t.clone(), t2.clone()) { + let t2 = normalized_type_with(ctx, x.clone())?; + let t = normalize(t.clone()); + if prop_equal(t.as_ref(), t2.as_ref()) { return Ok(t.clone()); } else { - let nf_t = normalize(t.clone()); - let nf_t2 = normalize(t2); - Err(mkerr(AnnotMismatch(x.clone(), nf_t, nf_t2))) + Err(mkerr(AnnotMismatch(x.clone(), t, t2))) } } - BoolLit(_) => Ok(Builtin(Bool)), - BinOp(BoolAnd, ref l, ref r) => { - op2_type(ctx, e.clone(), Bool, CantAnd, l, r) - } - BinOp(BoolOr, ref l, ref r) => { - op2_type(ctx, e.clone(), Bool, CantOr, l, r) - } - BinOp(BoolEQ, ref l, ref r) => { - op2_type(ctx, e.clone(), Bool, CantEQ, l, r) - } - BinOp(BoolNE, ref l, ref r) => { - op2_type(ctx, e.clone(), Bool, CantNE, l, r) - } - BoolIf(ref x, ref y, ref z) => { - let tx = normalize(type_with(ctx, x.clone())?); + BoolIf(x, y, z) => { + let tx = normalized_type_with(ctx, x.clone())?; match tx.as_ref() { Builtin(Bool) => {} _ => { return Err(mkerr(InvalidPredicate(x.clone(), tx))); } } - let ty = normalize(type_with(ctx, y.clone())?); - let tty = normalize(type_with(ctx, ty.clone())?); - match tty.as_ref() { - Const(Type) => {} - _ => { - return Err(mkerr(IfBranchMustBeTerm( - true, - y.clone(), - ty, - tty, - ))); - } - } + let ty = normalized_type_with(ctx, y.clone())?; + let tty = normalized_type_with(ctx, ty.clone())?; + ensure_is_type( + tty.clone(), + IfBranchMustBeTerm(true, y.clone(), ty.clone(), tty.clone()), + )?; - let tz = normalize(type_with(ctx, z.clone())?); - let ttz = normalize(type_with(ctx, tz.clone())?); - match ttz.as_ref() { - Const(Type) => {} - _ => { - return Err(mkerr(IfBranchMustBeTerm( - false, - z.clone(), - tz, - ttz, - ))); - } - } + let tz = normalized_type_with(ctx, z.clone())?; + let ttz = normalized_type_with(ctx, tz.clone())?; + ensure_is_type( + ttz.clone(), + IfBranchMustBeTerm(false, z.clone(), tz.clone(), ttz.clone()), + )?; - if !prop_equal(ty.clone(), tz.clone()) { + if !prop_equal(ty.as_ref(), tz.as_ref()) { return Err(mkerr(IfBranchMismatch( y.clone(), z.clone(), @@ -370,43 +351,7 @@ where } return Ok(ty); } - NaturalLit(_) => Ok(Builtin(Natural)), - Builtin(NaturalFold) => { - return Ok(dhall_expr!( - Natural -> - forall (natural: Type) -> - forall (succ: natural -> natural) -> - forall (zero: natural) -> - natural - )) - } - Builtin(NaturalBuild) => { - return Ok(dhall_expr!( - (forall (natural: Type) -> - forall (succ: natural -> natural) -> - forall (zero: natural) -> - natural) -> - Natural - )) - } - Builtin(NaturalIsZero) | Builtin(NaturalEven) | Builtin(NaturalOdd) => { - return Ok(dhall_expr!( - Natural -> Bool - )) - } - BinOp(NaturalPlus, ref l, ref r) => { - op2_type(ctx, e.clone(), Natural, CantAdd, l, r) - } - BinOp(NaturalTimes, ref l, ref r) => { - op2_type(ctx, e.clone(), Natural, CantMultiply, l, r) - } - IntegerLit(_) => Ok(Builtin(Integer)), - DoubleLit(_) => Ok(Builtin(Double)), - TextLit(_) => Ok(Builtin(Text)), - BinOp(TextAppend, ref l, ref r) => { - op2_type(ctx, e.clone(), Text, CantTextAppend, l, r) - } - ListLit(ref t, ref xs) => { + ListLit(t, xs) => { let mut iter = xs.iter().enumerate(); let t: Rc> = match t { Some(t) => t.clone(), @@ -416,65 +361,18 @@ where } }; - let s = normalize(type_with(ctx, t.clone())?); - match s.as_ref() { - Const(Type) => {} - _ => return Err(mkerr(InvalidListType(t))), - } + let s = normalized_type_with(ctx, t.clone())?; + ensure_is_type(s, InvalidListType(t.clone()))?; + let t = normalize(t); for (i, x) in iter { - let t2 = type_with(ctx, x.clone())?; - if !prop_equal(t.clone(), t2.clone()) { - let nf_t = normalize(t); - let nf_t2 = normalize(t2); - return Err(mkerr(InvalidListElement( - i, - nf_t, - x.clone(), - nf_t2, - ))); + let t2 = normalized_type_with(ctx, x.clone())?; + if !prop_equal(t.as_ref(), t2.as_ref()) { + return Err(mkerr(InvalidListElement(i, t, x.clone(), t2))); } } return Ok(dhall_expr!(List t)); } - Builtin(ListBuild) => { - return Ok(dhall_expr!( - forall (a: Type) -> - (forall (list: Type) -> - forall (cons: a -> list -> list) -> - forall (nil: list) -> - list) -> - List a - )) - } - Builtin(ListFold) => { - return Ok(dhall_expr!( - forall (a: Type) -> - List a -> - forall (list: Type) -> - forall (cons: a -> list -> list) -> - forall (nil: list) -> - list - )) - } - Builtin(ListLength) => { - return Ok(dhall_expr!(forall (a: Type) -> List a -> Natural)) - } - Builtin(ListHead) | Builtin(ListLast) => { - return Ok(dhall_expr!(forall (a: Type) -> List a -> Optional a)) - } - Builtin(ListIndexed) => { - return Ok(dhall_expr!( - forall (a: Type) -> - List a -> - List { index: Natural, value: a } - )) - } - Builtin(ListReverse) => { - return Ok(dhall_expr!( - forall (a: Type) -> List a -> List a - )) - } - OptionalLit(ref t, ref xs) => { + OptionalLit(t, xs) => { let mut iter = xs.iter(); let t: Rc> = match t { Some(t) => t.clone(), @@ -484,83 +382,44 @@ where } }; - let s = normalize(type_with(ctx, t.clone())?); - match s.as_ref() { - Const(Type) => {} - _ => { - return Err(mkerr(InvalidOptionalType(t))); - } - } + let s = normalized_type_with(ctx, t.clone())?; + ensure_is_type(s, InvalidOptionalType(t.clone()))?; + let t = normalize(t); for x in iter { - let t2 = type_with(ctx, x.clone())?; - if !prop_equal(t.clone(), t2.clone()) { - let nf_t = normalize(t); - let nf_t2 = normalize(t2); + let t2 = normalized_type_with(ctx, x.clone())?; + if !prop_equal(t.as_ref(), t2.as_ref()) { return Err(mkerr(InvalidOptionalElement( - nf_t, + t, x.clone(), - nf_t2, + t2, ))); } } return Ok(dhall_expr!(Optional t)); } - Builtin(OptionalFold) => { - return Ok(dhall_expr!( - forall (a: Type) -> - Optional a -> - forall (optional: Type) -> - forall (just: a -> optional) -> - forall (nothing: optional) -> - optional - )) - } - Builtin(List) | Builtin(Optional) => { - return Ok(dhall_expr!( - Type -> Type - )) - } - Builtin(Bool) | Builtin(Natural) | Builtin(Integer) - | Builtin(Double) | Builtin(Text) => Ok(Const(Type)), - Record(ref kts) => { + Record(kts) => { for (k, t) in kts { - let s = normalize(type_with(ctx, t.clone())?); - match s.as_ref() { - Const(Type) => {} - _ => { - return Err(mkerr(InvalidFieldType( - k.clone(), - t.clone(), - ))); - } - } + let s = normalized_type_with(ctx, t.clone())?; + ensure_is_type(s, InvalidFieldType(k.clone(), t.clone()))?; } Ok(Const(Type)) } - RecordLit(ref kvs) => { + RecordLit(kvs) => { let kts = kvs .iter() .map(|(k, v)| { let t = type_with(ctx, v.clone())?; - let s = normalize(type_with(ctx, t.clone())?); - match s.as_ref() { - Const(Type) => {} - _ => { - return Err(mkerr(InvalidField( - k.clone(), - v.clone(), - ))); - } - } + let s = normalized_type_with(ctx, t.clone())?; + ensure_is_type(s, InvalidField(k.clone(), v.clone()))?; Ok((k.clone(), t)) }) .collect::>()?; Ok(Record(kts)) } - Field(ref r, ref x) => { - let t = normalize(type_with(ctx, r.clone())?); + Field(r, x) => { + let t = normalized_type_with(ctx, r.clone())?; match t.as_ref() { - Record(ref kts) => { + Record(kts) => { return kts.get(x).cloned().ok_or_else(|| { mkerr(MissingField(x.clone(), t.clone())) }) @@ -568,12 +427,53 @@ where _ => Err(mkerr(NotARecord(x.clone(), r.clone(), t.clone()))), } } - Embed(p) => match p {}, + Builtin(b) => return Ok(type_of_builtin(*b)), + BoolLit(_) => Ok(Builtin(Bool)), + NaturalLit(_) => Ok(Builtin(Natural)), + IntegerLit(_) => Ok(Builtin(Integer)), + DoubleLit(_) => Ok(Builtin(Double)), + TextLit(_) => Ok(Builtin(Text)), + BinOp(o, l, r) => { + let t = match o { + BoolAnd => Bool, + BoolOr => Bool, + BoolEQ => Bool, + BoolNE => Bool, + NaturalPlus => Natural, + NaturalTimes => Natural, + TextAppend => Text, + _ => panic!("Unimplemented typecheck case: {:?}", e), + }; + let tl = normalized_type_with(ctx, l.clone())?; + match tl.as_ref() { + Builtin(lt) if *lt == t => {} + _ => return Err(mkerr(BinOpTypeMismatch(*o, l.clone(), tl))), + } + + let tr = normalized_type_with(ctx, r.clone())?; + match tr.as_ref() { + Builtin(rt) if *rt == t => {} + _ => return Err(mkerr(BinOpTypeMismatch(*o, r.clone(), tr))), + } + + Ok(Builtin(t)) + } + Embed(p) => match *p {}, _ => panic!("Unimplemented typecheck case: {:?}", e), } .map(rc) } +pub fn normalized_type_with( + ctx: &Context>>, + e: Rc>, +) -> Result>, TypeError> +where + S: ::std::fmt::Debug, +{ + Ok(normalize(type_with(ctx, 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. @@ -628,13 +528,7 @@ pub enum TypeMessage { HandlerNotAFunction(Label, Rc>), NotARecord(Label, Rc>, Rc>), MissingField(Label, Rc>), - CantAnd(Rc>, Rc>), - CantOr(Rc>, Rc>), - CantEQ(Rc>, Rc>), - CantNE(Rc>, Rc>), - CantTextAppend(Rc>, Rc>), - CantAdd(Rc>, Rc>), - CantMultiply(Rc>, Rc>), + BinOpTypeMismatch(BinOp, Rc>, Rc>), NoDependentLet(Rc>, Rc>), NoDependentTypes(Rc>, Rc>), } @@ -676,11 +570,11 @@ impl ::std::error::Error for TypeMessage { impl fmt::Display for TypeMessage { fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { - match *self { + match self { UnboundVariable => { f.write_str(include_str!("errors/UnboundVariable.txt")) } - TypeMismatch(ref e0, ref e1, ref e2, ref e3) => { + TypeMismatch(e0, e1, e2, e3) => { let template = include_str!("errors/TypeMismatch.txt"); let s = template .replace("$txt0", &format!("{}", e0)) -- cgit v1.2.3