summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dhall/src/normalize.rs21
-rw-r--r--dhall/src/typecheck.rs79
2 files changed, 68 insertions, 32 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 9c62923..9ca890e 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -9,7 +9,7 @@ use dhall_core::{
};
use dhall_generator as dhall;
-use crate::expr::{Normalized, PartiallyNormalized, Typed};
+use crate::expr::{Normalized, PartiallyNormalized, Type, Typed};
type InputSubExpr = SubExpr<X, Normalized<'static>>;
type OutputSubExpr = SubExpr<X, X>;
@@ -365,7 +365,7 @@ pub(crate) enum WHNF {
impl WHNF {
/// Convert the value back to a (normalized) syntactic expression
- fn normalize_to_expr(self) -> OutputSubExpr {
+ pub(crate) fn normalize_to_expr(self) -> OutputSubExpr {
match self {
WHNF::Lam(x, t, (ctx, e)) => {
let ctx2 = ctx.skip(&x);
@@ -615,7 +615,7 @@ impl Thunk {
Thunk::Normalized(Box::new(v))
}
- fn normalize(self) -> WHNF {
+ pub(crate) fn normalize(self) -> WHNF {
match self {
Thunk::Normalized(v) => *v,
Thunk::Unnormalized(ctx, e) => normalize_whnf(ctx, e),
@@ -634,7 +634,7 @@ impl Thunk {
#[derive(Debug, Clone)]
pub(crate) enum TypeThunk {
Thunk(Thunk),
- // Type(Type<'static>),
+ Type(Type<'static>),
}
impl TypeThunk {
@@ -646,6 +646,10 @@ impl TypeThunk {
TypeThunk::Thunk(th)
}
+ pub(crate) fn from_type(t: Type<'static>) -> Self {
+ TypeThunk::Type(t)
+ }
+
fn from_whnf(v: WHNF) -> Self {
TypeThunk::from_thunk(Thunk::from_whnf(v))
}
@@ -653,12 +657,21 @@ impl TypeThunk {
fn normalize(self) -> WHNF {
match self {
TypeThunk::Thunk(th) => th.normalize(),
+ // TODO: let's hope for the best with the unwraps
+ TypeThunk::Type(t) => normalize_whnf(
+ NormalizationContext::new(),
+ t.into_normalized().unwrap().0.embed_absurd(),
+ ),
}
}
fn shift(&mut self, delta: isize, var: &V<Label>) {
match self {
TypeThunk::Thunk(th) => th.shift(delta, var),
+ TypeThunk::Type(t) => {
+ let shifted = t.shift(delta, var);
+ std::mem::replace(t, shifted);
+ }
}
}
}
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 2c3a36f..9e985e4 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -6,6 +6,7 @@ use std::fmt;
use std::marker::PhantomData;
use crate::expr::*;
+use crate::normalize::{TypeThunk, WHNF};
use crate::traits::DynamicType;
use dhall_core;
use dhall_core::context::Context;
@@ -113,10 +114,13 @@ impl<'a> Type<'a> {
fn into_internal(self) -> TypeInternal<'a> {
self.0
}
- fn shift0(&self, delta: isize, label: &Label) -> Self {
+ fn internal_whnf(&self) -> Option<&WHNF> {
+ self.0.whnf()
+ }
+ pub(crate) fn shift0(&self, delta: isize, label: &Label) -> Self {
Type(self.0.shift0(delta, label))
}
- fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
Type(self.0.shift(delta, var))
}
@@ -136,6 +140,20 @@ impl Type<'static> {
}
}
+impl TypeThunk {
+ fn normalize_to_type(
+ self,
+ ctx: &TypecheckContext,
+ ) -> Result<Type<'static>, TypeError> {
+ match self {
+ TypeThunk::Type(t) => Ok(t),
+ TypeThunk::Thunk(th) => {
+ mktype(ctx, th.normalize().normalize_to_expr().embed_absurd())
+ }
+ }
+ }
+}
+
/// A semantic type. This is partially redundant with `dhall_core::Expr`, on purpose. `TypeInternal` should
/// be limited to syntactic expressions: either written by the user or meant to be printed.
/// The rule is the following: we must _not_ construct values of type `Expr` while typechecking,
@@ -144,7 +162,6 @@ impl Type<'static> {
pub(crate) enum TypeInternal<'a> {
Const(Const),
Pi(Const, Label, Box<Type<'static>>, Box<Type<'static>>),
- RecordType(Const, BTreeMap<Label, Type<'static>>),
UnionType(Const, BTreeMap<Label, Option<Type<'static>>>),
ListType(Box<Type<'static>>),
OptionalType(Box<Type<'static>>),
@@ -152,12 +169,14 @@ pub(crate) enum TypeInternal<'a> {
SuperType,
/// This must not contain a value captured by one of the variants above.
Expr(Box<Normalized<'a>>),
+ 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 => {
return Err(TypeError::new(
@@ -175,13 +194,6 @@ impl<'a> TypeInternal<'a> {
Some(const_to_type(c)),
PhantomData,
),
- TypeInternal::RecordType(c, kts) => Normalized(
- rc(ExprF::RecordType(kts).traverse_ref_simple(|e| {
- Ok(e.clone().into_normalized()?.into_expr())
- })?),
- Some(const_to_type(c)),
- PhantomData,
- ),
TypeInternal::UnionType(c, kts) => Normalized(
rc(ExprF::UnionType(kts).traverse_ref_simple(|e| {
Ok(e.clone().into_normalized()?.into_expr())
@@ -207,6 +219,12 @@ impl<'a> TypeInternal<'a> {
),
})
}
+ fn whnf(&self) -> Option<&WHNF> {
+ match self {
+ TypeInternal::PNzed(e) => Some(&e.0),
+ _ => None,
+ }
+ }
fn shift0(&self, delta: isize, label: &Label) -> Self {
self.shift(delta, &V(label.clone(), 0))
}
@@ -214,18 +232,13 @@ impl<'a> TypeInternal<'a> {
use TypeInternal::*;
match self {
Expr(e) => Expr(Box::new(e.shift(delta, var))),
+ PNzed(e) => PNzed(Box::new(e.shift(delta, var))),
Pi(c, x, t, e) => Pi(
*c,
x.clone(),
Box::new(t.shift(delta, var)),
Box::new(e.shift(delta, &var.shift0(1, x))),
),
- RecordType(c, kts) => RecordType(
- *c,
- kts.iter()
- .map(|(k, v)| (k.clone(), v.shift(delta, var)))
- .collect(),
- ),
UnionType(c, kts) => UnionType(
*c,
kts.iter()
@@ -642,10 +655,20 @@ impl TypeIntermediate {
// An empty record type has type Type
let k = k.unwrap_or(dhall_core::Const::Type);
- Ok(TypedOrType::Type(Type(TypeInternal::RecordType(
- k,
- kts.clone(),
- ))))
+ let pnormalized = PartiallyNormalized(
+ WHNF::RecordType(
+ kts.iter()
+ .map(|(k, t)| {
+ (k.clone(), TypeThunk::from_type(t.clone()))
+ })
+ .collect(),
+ ),
+ Some(const_to_type(k)),
+ PhantomData,
+ );
+ Ok(TypedOrType::Type(Type(TypeInternal::PNzed(Box::new(
+ pnormalized,
+ )))))
}
TypeIntermediate::UnionType(ctx, kts) => {
// Check that all types are the same const
@@ -998,12 +1021,12 @@ fn type_last_layer(
.normalize_to_type()?,
))
}
- Field(r, x) => match r.get_type()?.internal() {
- TypeInternal::RecordType(_, kts) => match kts.get(&x) {
- Some(t) => Ok(RetType(t.clone())),
+ Field(r, x) => match r.get_type()?.internal_whnf() {
+ Some(WHNF::RecordType(kts)) => match kts.get(&x) {
+ Some(tth) => Ok(RetType(tth.clone().normalize_to_type(ctx)?)),
None => Err(mkerr(MissingRecordField(x, r))),
},
- TypeInternal::Const(_) => {
+ _ => {
let r = r.normalize_to_type()?;
match r.internal() {
TypeInternal::UnionType(_, kts) => match kts.get(&x) {
@@ -1028,10 +1051,10 @@ fn type_last_layer(
_ => Err(mkerr(NotARecord(x, r.into_normalized()?))),
}
}
- _ => Err(mkerr(NotARecord(
- x,
- r.normalize_to_type()?.into_normalized()?,
- ))),
+ // _ => Err(mkerr(NotARecord(
+ // x,
+ // r.normalize_to_type()?.into_normalized()?,
+ // ))),
},
Const(c) => Ok(RetType(type_of_const(c))),
Builtin(b) => Ok(RetExpr(type_of_builtin(b))),
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 16:15:08 +0000