summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
authorNadrieril2019-04-28 01:03:12 +0200
committerNadrieril2019-04-28 01:03:12 +0200
commita594e3aa376aa4bfef3456d336630f7520f3c28b (patch)
tree77c22d0ba728ac70e7aee1230df00dc4b0333a48 /dhall
parent949da31876c899dc7de295328fb7acc8063cdc7c (diff)
Use PartiallyNormalized throughout typechecking
Diffstat (limited to '')
-rw-r--r--dhall/src/expr.rs3
-rw-r--r--dhall/src/normalize.rs12
-rw-r--r--dhall/src/typecheck.rs173
3 files changed, 95 insertions, 93 deletions
diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index d1729a5..bde4fe0 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -133,9 +133,6 @@ impl<'a> Normalized<'a> {
pub(crate) fn as_expr(&self) -> &SubExpr<X, X> {
&self.0
}
- pub(crate) fn into_expr(self) -> SubExpr<X, X> {
- self.0
- }
#[allow(dead_code)]
pub(crate) fn unnote<'b>(self) -> Normalized<'b> {
Normalized(self.0, self.1, PhantomData)
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 2dc4cab..88a55a1 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -4,7 +4,7 @@ use std::rc::Rc;
use dhall_core::context::Context;
use dhall_core::{
- rc, shift, shift0, Builtin, ExprF, Integer, InterpolatedText,
+ rc, shift, shift0, Builtin, Const, ExprF, Integer, InterpolatedText,
InterpolatedTextContents, Label, Natural, SubExpr, V, X,
};
use dhall_generator as dhall;
@@ -347,6 +347,7 @@ pub(crate) enum WHNF {
NaturalSuccClosure,
Pi(Label, TypeThunk, TypeThunk),
+ Const(Const),
BoolLit(bool),
NaturalLit(Natural),
IntegerLit(Integer),
@@ -406,6 +407,7 @@ impl WHNF {
t.normalize().normalize_to_expr(),
e.normalize().normalize_to_expr(),
)),
+ WHNF::Const(c) => rc(ExprF::Const(c)),
WHNF::BoolLit(b) => rc(ExprF::BoolLit(b)),
WHNF::NaturalLit(n) => rc(ExprF::NaturalLit(n)),
WHNF::IntegerLit(n) => rc(ExprF::IntegerLit(n)),
@@ -494,7 +496,7 @@ impl WHNF {
}
/// Apply to a value
- fn app(self, val: WHNF) -> WHNF {
+ pub(crate) fn app(self, val: WHNF) -> WHNF {
match (self, val) {
(WHNF::Lam(x, _, (ctx, e)), val) => {
let ctx2 = ctx.insert(&x, val);
@@ -531,13 +533,14 @@ impl WHNF {
}
}
- fn from_builtin(b: Builtin) -> WHNF {
+ pub(crate) fn from_builtin(b: Builtin) -> WHNF {
WHNF::AppliedBuiltin(b, vec![])
}
fn shift(&mut self, delta: isize, var: &V<Label>) {
match self {
WHNF::NaturalSuccClosure
+ | WHNF::Const(_)
| WHNF::BoolLit(_)
| WHNF::NaturalLit(_)
| WHNF::IntegerLit(_) => {}
@@ -705,7 +708,8 @@ fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> WHNF {
Thunk::new(ctx.clone(), t.clone()),
(ctx, e.clone()),
),
- ExprF::Builtin(b) => WHNF::AppliedBuiltin(*b, vec![]),
+ ExprF::Builtin(b) => WHNF::from_builtin(*b),
+ ExprF::Const(c) => WHNF::Const(*c),
ExprF::BoolLit(b) => WHNF::BoolLit(*b),
ExprF::NaturalLit(n) => WHNF::NaturalLit(*n),
ExprF::OldOptionalLit(None, e) => {
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 8c3507d..e04bf0d 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -42,16 +42,8 @@ impl<'a> Typed<'a> {
}
}
impl<'a> Normalized<'a> {
- // Expose the outermost constructor
- fn unroll_ref(&self) -> &Expr<X, X> {
- self.as_expr().as_ref()
- }
fn shift0(&self, delta: isize, label: &Label) -> Self {
- Normalized(
- shift0(delta, label, &self.0),
- self.1.as_ref().map(|t| t.shift0(delta, label)),
- self.2,
- )
+ self.shift(delta, &V(label.clone(), 0))
}
fn shift(&self, delta: isize, var: &V<Label>) -> Self {
Normalized(
@@ -71,9 +63,13 @@ impl<'a> Normalized<'a> {
ExprF::Const(c) => Type(TypeInternal::Const(*c)),
ExprF::Pi(_, _, _) | ExprF::RecordType(_) | ExprF::UnionType(_) => {
// TODO: wasteful
- type_with(ctx, self.0.embed_absurd())?.normalize_to_type()?
+ type_with(ctx, self.0.embed_absurd())?.normalize_to_type()
}
- _ => Type(TypeInternal::Expr(Box::new(self))),
+ _ => Type(TypeInternal::PNzed(Box::new(PartiallyNormalized(
+ WHNF::Expr(self.0),
+ self.1,
+ self.2,
+ )))),
})
}
fn get_type_move(self) -> Result<Type<'static>, TypeError> {
@@ -93,19 +89,11 @@ impl Normalized<'static> {
}
}
impl<'a> PartiallyNormalized<'a> {
- fn normalize_to_type(self) -> Result<Type<'a>, TypeError> {
- Ok(match &self.0 {
- WHNF::RecordType(_) | WHNF::UnionType(_) | WHNF::Pi(_, _, _) => {
- Type(TypeInternal::PNzed(Box::new(self)))
- }
- _ => {
- let e = self.normalize();
- match e.0.as_ref() {
- ExprF::Const(c) => Type(TypeInternal::Const(*c)),
- _ => Type(TypeInternal::Expr(Box::new(e))),
- }
- }
- })
+ fn normalize_to_type(self) -> Type<'a> {
+ match &self.0 {
+ WHNF::Const(c) => Type(TypeInternal::Const(*c)),
+ _ => Type(TypeInternal::PNzed(Box::new(self))),
+ }
}
}
impl<'a> Type<'a> {
@@ -117,12 +105,8 @@ impl<'a> Type<'a> {
pub(crate) fn into_normalized(self) -> Result<Normalized<'a>, TypeError> {
self.0.into_normalized()
}
- // Expose the outermost constructor
- fn unroll_ref(&self) -> Result<Cow<Expr<X, X>>, TypeError> {
- match self.as_normalized()? {
- Cow::Borrowed(e) => Ok(Cow::Borrowed(e.unroll_ref())),
- Cow::Owned(e) => Ok(Cow::Owned(e.into_expr().unroll())),
- }
+ fn normalize_whnf(self) -> Result<WHNF, TypeError> {
+ self.0.normalize_whnf()
}
fn internal(&self) -> &TypeInternal<'a> {
&self.0
@@ -136,6 +120,38 @@ impl<'a> Type<'a> {
pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
Type(self.0.shift(delta, var))
}
+ fn subst(
+ self,
+ ctx: &TypecheckContext,
+ x: &Label,
+ val: Normalized<'static>,
+ ) -> Result<Self, TypeError> {
+ let tval = val.get_type()?.into_owned();
+ let ctx_type = ctx.insert_type(x, tval);
+ let ctx_val = ctx.insert_value(x, val);
+
+ let pnzed = match self.0 {
+ TypeInternal::PNzed(e) => e,
+ internal => return Ok(Type(internal)),
+ };
+ let nzed = pnzed.normalize();
+ let pnzed = Typed(nzed.0.embed_absurd(), nzed.1, ctx_val, nzed.2)
+ .normalize_whnf();
+
+ Ok(match &pnzed.0 {
+ WHNF::Expr(e) => {
+ let e = e.clone();
+ match e.as_ref() {
+ ExprF::Pi(_, _, _) | ExprF::RecordType(_) => {
+ type_with(&ctx_type, e.embed_absurd())?
+ .normalize_to_type()
+ }
+ _ => pnzed.normalize_to_type(),
+ }
+ }
+ _ => pnzed.normalize_to_type(),
+ })
+ }
fn const_sort() -> Self {
Type(TypeInternal::Const(Const::Sort))
@@ -174,19 +190,15 @@ impl TypeThunk {
#[derive(Debug, Clone)]
pub(crate) enum TypeInternal<'a> {
Const(Const),
- ListType(Box<Type<'static>>),
- OptionalType(Box<Type<'static>>),
/// The type of `Sort`
SuperType,
- /// This must not contain a value captured by one of the variants above.
- Expr(Box<Normalized<'a>>),
+ /// This must not contain Const value.
PNzed(Box<PartiallyNormalized<'a>>),
}
impl<'a> TypeInternal<'a> {
pub(crate) fn into_normalized(self) -> Result<Normalized<'a>, TypeError> {
Ok(match self {
- TypeInternal::Expr(e) => *e,
TypeInternal::PNzed(e) => e.normalize(),
TypeInternal::Const(c) => const_to_normalized(c),
TypeInternal::SuperType => {
@@ -196,24 +208,12 @@ impl<'a> TypeInternal<'a> {
TypeMessage::Untyped,
))
}
- TypeInternal::ListType(t) => Normalized(
- rc(ExprF::App(
- rc(ExprF::Builtin(Builtin::List)),
- t.into_normalized()?.into_expr(),
- )),
- Some(Type::const_type()),
- PhantomData,
- ),
- TypeInternal::OptionalType(t) => Normalized(
- rc(ExprF::App(
- rc(ExprF::Builtin(Builtin::Optional)),
- t.into_normalized()?.into_expr(),
- )),
- Some(Type::const_type()),
- PhantomData,
- ),
})
}
+ fn normalize_whnf(self) -> Result<WHNF, TypeError> {
+ let typed: Typed = self.into_normalized()?.into();
+ Ok(typed.normalize_whnf().0)
+ }
fn whnf(&self) -> Option<&WHNF> {
match self {
TypeInternal::PNzed(e) => Some(&e.0),
@@ -226,10 +226,7 @@ impl<'a> TypeInternal<'a> {
fn shift(&self, delta: isize, var: &V<Label>) -> Self {
use TypeInternal::*;
match self {
- Expr(e) => Expr(Box::new(e.shift(delta, var))),
PNzed(e) => PNzed(Box::new(e.shift(delta, var))),
- ListType(t) => ListType(Box::new(t.shift(delta, var))),
- OptionalType(t) => OptionalType(Box::new(t.shift(delta, var))),
Const(c) => Const(*c),
SuperType => SuperType,
}
@@ -261,10 +258,10 @@ impl TypedOrType {
TypedOrType::Type(t) => Ok(t.into_normalized()?.into()),
}
}
- fn normalize_to_type(self) -> Result<Type<'static>, TypeError> {
+ fn normalize_to_type(self) -> Type<'static> {
match self {
TypedOrType::Typed(e) => e.normalize_whnf().normalize_to_type(),
- TypedOrType::Type(t) => Ok(t),
+ TypedOrType::Type(t) => t,
}
}
fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> {
@@ -705,8 +702,14 @@ impl TypeIntermediate {
t,
mkerr(ctx, InvalidListType(t.clone().into_normalized()?))?,
);
- Ok(TypedOrType::Type(Type(TypeInternal::ListType(Box::new(
- t.clone(),
+ let pnormalized = PartiallyNormalized(
+ WHNF::from_builtin(Builtin::List)
+ .app(t.clone().normalize_whnf()?),
+ Some(const_to_type(Const::Type)),
+ PhantomData,
+ );
+ Ok(TypedOrType::Type(Type(TypeInternal::PNzed(Box::new(
+ pnormalized,
)))))
}
TypeIntermediate::OptionalType(ctx, t) => {
@@ -717,9 +720,15 @@ impl TypeIntermediate {
InvalidOptionalType(t.clone().into_normalized()?)
)?,
);
- Ok(TypedOrType::Type(Type(TypeInternal::OptionalType(
- Box::new(t.clone()),
- ))))
+ let pnormalized = PartiallyNormalized(
+ WHNF::from_builtin(Builtin::Optional)
+ .app(t.clone().normalize_whnf()?),
+ Some(const_to_type(Const::Type)),
+ PhantomData,
+ );
+ Ok(TypedOrType::Type(Type(TypeInternal::PNzed(Box::new(
+ pnormalized,
+ )))))
}
}
}
@@ -751,7 +760,7 @@ fn mktype(
ctx: &TypecheckContext,
e: SubExpr<X, Normalized<'static>>,
) -> Result<Type<'static>, TypeError> {
- Ok(type_with(ctx, e)?.normalize_to_type()?)
+ Ok(type_with(ctx, e)?.normalize_to_type())
}
fn builtin_to_type<'a>(b: Builtin) -> Result<Type<'a>, TypeError> {
@@ -787,7 +796,7 @@ fn type_with(
Ok(RetType(
TypeIntermediate::Pi(ctx.clone(), x.clone(), tx, tb)
.typecheck()?
- .normalize_to_type()?,
+ .normalize_to_type(),
))
}
Pi(x, ta, tb) => {
@@ -888,15 +897,10 @@ fn type_last_layer(
mkerr(TypeMismatch(f.clone(), tx.clone().into_normalized()?, a))
});
- let ctx2 = ctx.insert_value(x, a.normalize()?);
- let tb: Typed = tb.clone().into_normalized()?.into();
- // Normalize with the updated context
- let tb = Typed(tb.0, tb.1, ctx2, tb.3).normalize();
- // Convert to type with the current context
- Ok(RetType(tb.into_type_ctx(&ctx)?))
+ Ok(RetType(tb.clone().subst(&ctx, x, a.normalize()?)?))
}
Annot(x, t) => {
- let t = t.normalize_to_type()?;
+ let t = t.normalize_to_type();
ensure_equal!(
&t,
x.get_type()?,
@@ -930,11 +934,11 @@ fn type_last_layer(
Ok(RetType(y.get_type_move()?))
}
EmptyListLit(t) => {
- let t = t.normalize_to_type()?;
+ let t = t.normalize_to_type();
Ok(RetType(
TypeIntermediate::ListType(ctx.clone(), t)
.typecheck()?
- .normalize_to_type()?,
+ .normalize_to_type(),
))
}
NEListLit(xs) => {
@@ -955,7 +959,7 @@ fn type_last_layer(
Ok(RetType(
TypeIntermediate::ListType(ctx.clone(), t)
.typecheck()?
- .normalize_to_type()?,
+ .normalize_to_type(),
))
}
SomeLit(x) => {
@@ -963,13 +967,13 @@ fn type_last_layer(
Ok(RetType(
TypeIntermediate::OptionalType(ctx.clone(), t)
.typecheck()?
- .normalize_to_type()?,
+ .normalize_to_type(),
))
}
RecordType(kts) => {
let kts: BTreeMap<_, _> = kts
.into_iter()
- .map(|(x, t)| Ok((x, t.normalize_to_type()?)))
+ .map(|(x, t)| Ok((x, t.normalize_to_type())))
.collect::<Result<_, _>>()?;
Ok(RetTypedOrType(
TypeIntermediate::RecordType(ctx.clone(), kts).typecheck()?,
@@ -983,7 +987,7 @@ fn type_last_layer(
x,
match t {
None => None,
- Some(t) => Some(t.normalize_to_type()?),
+ Some(t) => Some(t.normalize_to_type()),
},
))
})
@@ -1000,7 +1004,7 @@ fn type_last_layer(
Ok(RetType(
TypeIntermediate::RecordType(ctx.clone(), kts)
.typecheck()?
- .normalize_to_type()?,
+ .normalize_to_type(),
))
}
UnionLit(x, v, kvs) => {
@@ -1008,7 +1012,7 @@ fn type_last_layer(
.into_iter()
.map(|(x, v)| {
let t = match v {
- Some(x) => Some(x.normalize_to_type()?),
+ Some(x) => Some(x.normalize_to_type()),
None => None,
};
Ok((x, t))
@@ -1019,7 +1023,7 @@ fn type_last_layer(
Ok(RetType(
TypeIntermediate::UnionType(ctx.clone(), kts)
.typecheck()?
- .normalize_to_type()?,
+ .normalize_to_type(),
))
}
Field(r, x) => match r.get_type()?.internal_whnf() {
@@ -1028,7 +1032,7 @@ fn type_last_layer(
None => Err(mkerr(MissingRecordField(x, r))),
},
_ => {
- let r = r.normalize_to_type()?;
+ let r = r.normalize_to_type();
match r.internal_whnf() {
Some(WHNF::UnionType(kts)) => match kts.get(&x) {
// Constructor has type T -> < x: T, ... >
@@ -1041,7 +1045,7 @@ fn type_last_layer(
r,
)
.typecheck()?
- .normalize_to_type()?,
+ .normalize_to_type(),
)),
Some(None) => Ok(RetType(r)),
None => Err(mkerr(MissingUnionField(
@@ -1066,11 +1070,8 @@ fn type_last_layer(
// TODO: check type of interpolations
TextLit(_) => Ok(RetType(builtin_to_type(Text)?)),
BinOp(o @ ListAppend, l, r) => {
- match l.get_type()?.unroll_ref()?.as_ref() {
- App(f, _) => match f.as_ref() {
- Builtin(List) => {}
- _ => return Err(mkerr(BinOpTypeMismatch(o, l))),
- },
+ match l.get_type()?.internal_whnf() {
+ Some(WHNF::AppliedBuiltin(List, _)) => {}
_ => return Err(mkerr(BinOpTypeMismatch(o, l))),
}