summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
authorNadrieril2019-04-22 00:07:50 +0200
committerNadrieril2019-04-22 00:07:50 +0200
commit316c6ea1c5512bcc9e0a07aa63fd086eb313abc5 (patch)
tree36529717ff0e36a11a1397b171e5e3006dd18d14 /dhall
parentecff0ecd47bb38937fb43e60b8d78ea92e2af01c (diff)
Avoid shift_subst in typecheck
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/normalize.rs16
-rw-r--r--dhall/src/typecheck.rs56
2 files changed, 40 insertions, 32 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index c17ed78..0301e35 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -18,6 +18,20 @@ impl<'a> Typed<'a> {
pub fn normalize(self) -> Normalized<'a> {
Normalized(normalize(self.0), self.1, self.2)
}
+ pub fn normalize_ctx(
+ self,
+ ctx: &crate::typecheck::TypecheckContext,
+ ) -> Normalized<'a> {
+ Normalized(
+ normalize_whnf(
+ NormalizationContext::from_typecheck_ctx(ctx),
+ self.0,
+ )
+ .normalize_to_expr(),
+ self.1,
+ self.2,
+ )
+ }
/// Pretends this expression is normalized. Use with care.
#[allow(dead_code)]
pub fn skip_normalize(self) -> Normalized<'a> {
@@ -279,7 +293,7 @@ impl NormalizationContext {
use crate::typecheck::EnvItem::*;
let mut ctx = Context::new();
for (k, vs) in tc_ctx.0.iter_keys() {
- for v in vs.iter().rev() {
+ for v in vs.iter() {
let new_item = match v {
Type(var, _) => EnvItem::Skip(var.clone()),
Value(e) => EnvItem::Expr(normalize_whnf(
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index e3ec849..e397316 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -3,7 +3,6 @@ use std::borrow::Borrow;
use std::borrow::Cow;
use std::fmt;
use std::marker::PhantomData;
-use std::rc::Rc;
use crate::expr::*;
use crate::traits::DynamicType;
@@ -46,8 +45,11 @@ impl<'a> Normalized<'a> {
self.as_expr().as_ref()
}
fn shift0(&self, delta: isize, label: &Label) -> Self {
- // shift the type too ?
- Normalized(shift0(delta, label, &self.0), self.1.clone(), self.2)
+ Normalized(
+ shift0(delta, label, &self.0),
+ self.1.as_ref().map(|t| t.shift0(delta, label)),
+ self.2,
+ )
}
pub(crate) fn into_type(self) -> Type<'a> {
Type(match self.0.as_ref() {
@@ -164,8 +166,8 @@ impl TypecheckContext {
pub(crate) fn insert_type(&self, x: &Label, t: Type<'static>) -> Self {
TypecheckContext(
self.0
- .insert(x.clone(), EnvItem::Type(V(x.clone(), 0), t))
- .map(|_, e| e.shift0(1, x)),
+ .map(|_, e| e.shift0(1, x))
+ .insert(x.clone(), EnvItem::Type(V(x.clone(), 0), t)),
)
}
pub(crate) fn insert_value(
@@ -173,11 +175,7 @@ impl TypecheckContext {
x: &Label,
t: Normalized<'static>,
) -> Self {
- TypecheckContext(
- self.0
- .insert(x.clone(), EnvItem::Value(t))
- .map(|_, e| e.shift0(1, x)),
- )
+ TypecheckContext(self.0.insert(x.clone(), EnvItem::Value(t)))
}
pub(crate) fn lookup(
&self,
@@ -422,7 +420,7 @@ fn mktype(
ctx: &TypecheckContext,
e: SubExpr<X, Normalized<'static>>,
) -> Result<Type<'static>, TypeError> {
- Ok(type_with(ctx, e)?.normalize().into_type())
+ Ok(type_with(ctx, e)?.normalize_ctx(ctx).into_type())
}
fn into_simple_type<'a>(e: SubExpr<X, X>) -> Type<'a> {
@@ -500,12 +498,8 @@ fn type_with(
v.clone()
};
- let v = type_with(ctx, v)?.normalize();
- let e = type_with(
- ctx,
- // TODO: Use a substitution context
- subst_shift(&V(x.clone(), 0), &v.embed(), e),
- )?;
+ let v = type_with(ctx, v)?.normalize_ctx(ctx);
+ let e = type_with(&ctx.insert_value(x, v.clone()), e.clone())?;
Ok(RetType(e.get_type_move()?))
}
@@ -547,7 +541,7 @@ fn type_last_layer(
Embed(_) => unreachable!(),
Var(var) => match ctx.lookup(&var) {
Some(e) => Ok(RetType(e.into_owned())),
- None => Err(mkerr(UnboundVariable)),
+ None => Err(mkerr(UnboundVariable(var.clone()))),
},
App(f, a) => {
let tf = f.get_type()?;
@@ -562,12 +556,12 @@ fn type_last_layer(
Ok(RetExpr(Let(
x.clone(),
None,
- a.normalize().embed(),
+ a.normalize_ctx(ctx).embed(),
tb.embed_absurd(),
)))
}
Annot(x, t) => {
- let t = t.normalize().into_type();
+ let t = t.normalize_ctx(ctx).into_type();
ensure_equal!(
&t,
x.get_type()?,
@@ -601,7 +595,7 @@ fn type_last_layer(
Ok(RetType(y.get_type_move()?))
}
EmptyListLit(t) => {
- let t = t.normalize().into_type();
+ let t = t.normalize_ctx(ctx).into_type();
ensure_simple_type!(
t,
mkerr(InvalidListType(t.into_normalized()?)),
@@ -632,13 +626,13 @@ fn type_last_layer(
Ok(RetExpr(dhall::expr!(List t)))
}
OldOptionalLit(None, t) => {
- let t = t.normalize().embed();
+ let t = t.normalize_ctx(ctx).embed();
let e = dhall::subexpr!(None t);
Ok(RetType(type_with(ctx, e)?.get_type()?.into_owned()))
}
OldOptionalLit(Some(x), t) => {
- let t = t.normalize().embed();
- let x = x.normalize().embed();
+ let t = t.normalize_ctx(ctx).embed();
+ let x = x.normalize_ctx(ctx).embed();
let e = dhall::subexpr!(Some x : Optional t);
Ok(RetType(type_with(ctx, e)?.get_type()?.into_owned()))
}
@@ -708,7 +702,7 @@ fn type_last_layer(
let mut kts: std::collections::BTreeMap<_, _> = kvs
.into_iter()
.map(|(x, v)| {
- let t = v.map(|x| x.normalize().embed());
+ let t = v.map(|x| x.normalize_ctx(ctx).embed());
Ok((x, t))
})
.collect::<Result<_, _>>()?;
@@ -722,7 +716,7 @@ fn type_last_layer(
None => Err(mkerr(MissingRecordField(x, r))),
},
_ => {
- let r = r.normalize();
+ let r = r.normalize_ctx(ctx);
match r.as_expr().as_ref() {
UnionType(kts) => match kts.get(&x) {
// Constructor has type T -> < x: T, ... >
@@ -803,7 +797,7 @@ fn type_of(
/// The specific type error
#[derive(Debug)]
pub(crate) enum TypeMessage<'a> {
- UnboundVariable,
+ UnboundVariable(V<Label>),
InvalidInputType(Normalized<'a>),
InvalidOutputType(Normalized<'a>),
NotAFunction(Typed<'a>),
@@ -856,7 +850,7 @@ impl From<TypeError> for std::option::NoneError {
impl ::std::error::Error for TypeMessage<'static> {
fn description(&self) -> &str {
match *self {
- UnboundVariable => "Unbound variable",
+ // UnboundVariable => "Unbound variable",
InvalidInputType(_) => "Invalid function input",
InvalidOutputType(_) => "Invalid function output",
NotAFunction(_) => "Not a function",
@@ -869,9 +863,9 @@ impl ::std::error::Error for TypeMessage<'static> {
impl fmt::Display for TypeMessage<'static> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
match self {
- UnboundVariable => {
- f.write_str(include_str!("errors/UnboundVariable.txt"))
- }
+ // UnboundVariable(_) => {
+ // f.write_str(include_str!("errors/UnboundVariable.txt"))
+ // }
TypeMismatch(e0, e1, e2) => {
let template = include_str!("errors/TypeMismatch.txt");
let s = template