summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/typecheck.rs602
1 files changed, 248 insertions, 354 deletions
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<S>(c: core::Const) -> Result<core::Const, TypeError<S>> {
+fn axiom<S>(c: Const) -> Result<Const, TypeError<S>> {
+ 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<core::Const, ()> {
+fn rule(a: Const, b: Const) -> Result<Const, ()> {
+ 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<core::Const, ()> {
}
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<S, T>(eL0: Rc<Expr<S, X>>, eR0: Rc<Expr<T, X>>) -> bool
+// Takes normalized expressions as input
+fn prop_equal<S, T>(eL0: &Expr<S, X>, eR0: &Expr<T, X>) -> bool
where
S: ::std::fmt::Debug,
T: ::std::fmt::Debug,
{
+ use dhall_core::Expr::*;
fn go<S, T>(
ctx: &mut Vec<(Label, Label)>,
- el: Rc<Expr<S, X>>,
- er: Rc<Expr<T, X>>,
+ el: &Expr<S, X>,
+ er: &Expr<T, X>,
) -> 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::<S, T>(&mut ctx, normalize(eL0), normalize(eR0))
+ go::<S, T>(&mut ctx, eL0, eR0)
}
-fn op2_type<S, EF>(
- ctx: &Context<Label, Rc<Expr<S, X>>>,
- e: Rc<Expr<S, X>>,
- t: core::Builtin,
- ef: EF,
- l: &Rc<Expr<S, X>>,
- r: &Rc<Expr<S, X>>,
-) -> Result<Expr<S, X>, TypeError<S>>
-where
- S: ::std::fmt::Debug,
- EF: FnOnce(Rc<Expr<S, X>>, Rc<Expr<S, X>>) -> TypeMessage<S>,
-{
- 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<S>(b: Builtin) -> Rc<Expr<S, X>> {
+ 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<Expr<_, _>> = 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<Expr<_, _>> = 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::<Result<_, _>>()?;
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<S>(
+ ctx: &Context<Label, Rc<Expr<S, X>>>,
+ e: Rc<Expr<S, X>>,
+) -> Result<Rc<Expr<S, X>>, TypeError<S>>
+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<S> {
HandlerNotAFunction(Label, Rc<Expr<S, X>>),
NotARecord(Label, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
MissingField(Label, Rc<Expr<S, X>>),
- CantAnd(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
- CantOr(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
- CantEQ(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
- CantNE(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
- CantTextAppend(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
- CantAdd(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
- CantMultiply(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+ BinOpTypeMismatch(BinOp, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
NoDependentLet(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
NoDependentTypes(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
}
@@ -676,11 +570,11 @@ impl<S: fmt::Debug> ::std::error::Error for TypeMessage<S> {
impl<S> fmt::Display for TypeMessage<S> {
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))
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-04 17:16:58 +0000