summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dhall/src/expr.rs7
-rw-r--r--dhall/src/normalize.rs74
-rw-r--r--dhall/src/typecheck.rs137
3 files changed, 94 insertions, 124 deletions
diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index c794324..1ddc4ba 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -44,13 +44,6 @@ pub(crate) struct Typed<'a>(
);
#[derive(Debug, Clone)]
-pub(crate) struct PartiallyNormalized<'a>(
- pub(crate) crate::normalize::Value,
- pub(crate) Option<Type<'static>>,
- pub(crate) PhantomData<&'a ()>,
-);
-
-#[derive(Debug, Clone)]
pub(crate) struct Normalized<'a>(
pub(crate) SubExpr<X, X>,
pub(crate) Option<Type<'static>>,
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 5151790..f15eea4 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, Type, Typed};
+use crate::expr::{Normalized, Type, Typed};
type InputSubExpr = SubExpr<X, Normalized<'static>>;
type OutputSubExpr = SubExpr<X, X>;
@@ -25,37 +25,35 @@ impl<'a> Typed<'a> {
/// leave ill-typed sub-expressions unevaluated.
///
pub fn normalize(self) -> Normalized<'a> {
- self.partially_normalize().normalize()
+ Normalized(self.0.as_whnf().normalize_to_expr(), self.1, self.2)
}
- pub(crate) fn partially_normalize(self) -> PartiallyNormalized<'a> {
- PartiallyNormalized(self.0.as_whnf(), self.1, self.2)
- }
-}
-impl<'a> PartiallyNormalized<'a> {
- pub(crate) fn normalize(self) -> Normalized<'a> {
- Normalized(self.0.normalize_to_expr(), self.1, self.2)
- }
pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
- PartiallyNormalized(
+ Typed(
self.0.shift(delta, var),
self.1.as_ref().map(|x| x.shift(delta, var)),
self.2,
)
}
+
pub(crate) fn subst_shift(
&self,
var: &V<Label>,
- val: &PartiallyNormalized<'static>,
+ val: &Typed<'static>,
) -> Self {
- PartiallyNormalized(
+ Typed(
self.0.subst_shift(var, val),
self.1.as_ref().map(|x| x.subst_shift(var, val)),
self.2,
)
}
- pub(crate) fn into_whnf(self) -> Value {
- self.0
+
+ pub(crate) fn normalize_whnf(&self) -> Value {
+ self.0.as_whnf()
+ }
+
+ pub(crate) fn as_thunk(&self) -> Thunk {
+ self.0.clone()
}
}
@@ -268,13 +266,11 @@ impl EnvItem {
pub(crate) fn subst_shift(
&self,
var: &V<Label>,
- val: &PartiallyNormalized<'static>,
+ val: &Typed<'static>,
) -> Self {
match self {
EnvItem::Thunk(e) => EnvItem::Thunk(e.subst_shift(var, val)),
- EnvItem::Skip(v) if v == var => {
- EnvItem::Thunk(Thunk::from_whnf(val.clone().into_whnf()))
- }
+ EnvItem::Skip(v) if v == var => EnvItem::Thunk(val.as_thunk()),
EnvItem::Skip(v) => EnvItem::Skip(v.shift(-1, var)),
}
}
@@ -331,11 +327,7 @@ impl NormalizationContext {
NormalizationContext(Rc::new(self.0.map(|_, e| e.shift(delta, var))))
}
- fn subst_shift(
- &self,
- var: &V<Label>,
- val: &PartiallyNormalized<'static>,
- ) -> Self {
+ fn subst_shift(&self, var: &V<Label>, val: &Typed<'static>) -> Self {
NormalizationContext(Rc::new(
self.0.map(|_, e| e.subst_shift(var, val)),
))
@@ -377,6 +369,10 @@ pub(crate) enum Value {
}
impl Value {
+ pub(crate) fn into_thunk(self) -> Thunk {
+ Thunk::from_whnf(self)
+ }
+
/// Convert the value back to a (normalized) syntactic expression
pub(crate) fn normalize_to_expr(self) -> OutputSubExpr {
match self {
@@ -585,8 +581,11 @@ impl Value {
pub(crate) fn app(self, val: Value) -> Value {
match (self, val) {
(Value::Lam(x, _, e), val) => {
- let val =
- PartiallyNormalized(val, None, std::marker::PhantomData);
+ let val = Typed(
+ Thunk::from_whnf(val),
+ None,
+ std::marker::PhantomData,
+ );
e.subst_shift(&V(x, 0), &val).as_whnf()
}
(Value::AppliedBuiltin(b, mut args), val) => {
@@ -717,7 +716,7 @@ impl Value {
pub(crate) fn subst_shift(
&self,
var: &V<Label>,
- val: &PartiallyNormalized<'static>,
+ val: &Typed<'static>,
) -> Self {
match self {
Value::Lam(x, t, e) => Value::Lam(
@@ -742,7 +741,7 @@ impl Value {
t.subst_shift(var, val),
e.subst_shift(&var.shift0(1, x), val),
),
- Value::Var(v) if v == var => val.clone().into_whnf(),
+ Value::Var(v) if v == var => val.normalize_whnf(),
Value::Var(v) => Value::Var(v.shift(-1, var)),
Value::Const(c) => Value::Const(*c),
Value::BoolLit(b) => Value::BoolLit(*b),
@@ -814,7 +813,7 @@ impl Value {
mod thunk {
use super::{normalize_whnf, InputSubExpr, NormalizationContext, Value};
- use crate::expr::PartiallyNormalized;
+ use crate::expr::Typed;
use dhall_core::{Label, V};
use std::cell::RefCell;
use std::rc::Rc;
@@ -900,11 +899,7 @@ mod thunk {
}
}
- fn subst_shift(
- &self,
- var: &V<Label>,
- val: &PartiallyNormalized<'static>,
- ) -> Self {
+ fn subst_shift(&self, var: &V<Label>, val: &Typed<'static>) -> Self {
match self {
ThunkInternal::Unnormalized(ctx, e) => {
ThunkInternal::Unnormalized(
@@ -953,7 +948,7 @@ mod thunk {
pub(crate) fn subst_shift(
&self,
var: &V<Label>,
- val: &PartiallyNormalized<'static>,
+ val: &Typed<'static>,
) -> Self {
self.0.borrow().subst_shift(var, val).into_thunk()
}
@@ -1003,7 +998,7 @@ impl TypeThunk {
pub(crate) fn subst_shift(
&self,
var: &V<Label>,
- val: &PartiallyNormalized<'static>,
+ val: &Typed<'static>,
) -> Self {
match self {
TypeThunk::Thunk(th) => TypeThunk::Thunk(th.subst_shift(var, val)),
@@ -1015,12 +1010,7 @@ impl TypeThunk {
match self {
TypeThunk::Thunk(th) => th.as_nf(),
// TODO: let's hope for the best with the unwrap
- TypeThunk::Type(t) => t
- .clone()
- .partially_normalize()
- .unwrap()
- .into_whnf()
- .normalize(),
+ TypeThunk::Type(t) => t.normalize_whnf().unwrap().normalize(),
}
}
}
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 85de42a..f22925a 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -68,8 +68,8 @@ impl<'a> Normalized<'a> {
// TODO: wasteful
type_with(ctx, self.0.embed_absurd())?.normalize_to_type()
}
- _ => Type(TypeInternal::PNzed(Box::new(PartiallyNormalized(
- Value::Expr(self.0),
+ _ => Type(TypeInternal::Typed(Box::new(Typed(
+ Value::Expr(self.0).into_thunk(),
self.1,
self.2,
)))),
@@ -86,11 +86,12 @@ impl Normalized<'static> {
rc(ExprF::Embed(self))
}
}
-impl<'a> PartiallyNormalized<'a> {
+impl<'a> Typed<'a> {
fn normalize_to_type(self) -> Type<'a> {
- match &self.0 {
+ // TODO: avoid cloning Value
+ match &self.normalize_whnf() {
Value::Const(c) => Type(TypeInternal::Const(*c)),
- _ => Type(TypeInternal::PNzed(Box::new(self))),
+ _ => Type(TypeInternal::Typed(Box::new(self))),
}
}
}
@@ -103,18 +104,16 @@ impl<'a> Type<'a> {
pub(crate) fn into_normalized(self) -> Result<Normalized<'a>, TypeError> {
self.0.into_normalized()
}
- fn normalize_whnf(self) -> Result<Value, TypeError> {
+ pub(crate) fn normalize_whnf(&self) -> Result<Value, TypeError> {
self.0.normalize_whnf()
}
- pub(crate) fn partially_normalize(
- self,
- ) -> Result<PartiallyNormalized<'a>, TypeError> {
- self.0.partially_normalize()
+ pub(crate) fn as_typed(&self) -> Result<Typed<'a>, TypeError> {
+ self.0.as_typed()
}
fn internal(&self) -> &TypeInternal<'a> {
&self.0
}
- fn internal_whnf(&self) -> Option<&Value> {
+ fn internal_whnf(&self) -> Option<Value> {
self.0.whnf()
}
pub(crate) fn shift0(&self, delta: isize, label: &Label) -> Self {
@@ -126,7 +125,7 @@ impl<'a> Type<'a> {
pub(crate) fn subst_shift(
&self,
var: &V<Label>,
- val: &PartiallyNormalized<'static>,
+ val: &Typed<'static>,
) -> Self {
Type(self.0.subst_shift(var, val))
}
@@ -172,20 +171,20 @@ pub(crate) enum TypeInternal<'a> {
/// The type of `Sort`
SuperType,
/// This must not contain Const value.
- PNzed(Box<PartiallyNormalized<'a>>),
+ Typed(Box<Typed<'a>>),
}
impl<'a> TypeInternal<'a> {
- pub(crate) fn into_normalized(self) -> Result<Normalized<'a>, TypeError> {
- Ok(self.partially_normalize()?.normalize())
+ pub(crate) fn into_normalized(&self) -> Result<Normalized<'a>, TypeError> {
+ Ok(self.as_typed()?.normalize())
}
- fn normalize_whnf(self) -> Result<Value, TypeError> {
- Ok(self.partially_normalize()?.into_whnf())
+ fn normalize_whnf(&self) -> Result<Value, TypeError> {
+ Ok(self.as_typed()?.normalize_whnf())
}
- fn partially_normalize(self) -> Result<PartiallyNormalized<'a>, TypeError> {
+ fn as_typed(&self) -> Result<Typed<'a>, TypeError> {
Ok(match self {
- TypeInternal::PNzed(e) => *e,
- TypeInternal::Const(c) => const_to_pnormalized(c),
+ TypeInternal::Typed(e) => e.as_ref().clone(),
+ TypeInternal::Const(c) => const_to_typed(*c),
TypeInternal::SuperType => {
return Err(TypeError::new(
&TypecheckContext::new(),
@@ -194,9 +193,10 @@ impl<'a> TypeInternal<'a> {
}
})
}
- fn whnf(&self) -> Option<&Value> {
+ fn whnf(&self) -> Option<Value> {
+ // TODO: return reference
match self {
- TypeInternal::PNzed(e) => Some(&e.0),
+ TypeInternal::Typed(e) => Some(e.normalize_whnf()),
_ => None,
}
}
@@ -206,19 +206,15 @@ impl<'a> TypeInternal<'a> {
fn shift(&self, delta: isize, var: &V<Label>) -> Self {
use TypeInternal::*;
match self {
- PNzed(e) => PNzed(Box::new(e.shift(delta, var))),
+ Typed(e) => Typed(Box::new(e.shift(delta, var))),
Const(c) => Const(*c),
SuperType => SuperType,
}
}
- fn subst_shift(
- &self,
- var: &V<Label>,
- val: &PartiallyNormalized<'static>,
- ) -> Self {
+ fn subst_shift(&self, var: &V<Label>, val: &Typed<'static>) -> Self {
use TypeInternal::*;
match self {
- PNzed(e) => PNzed(Box::new(e.subst_shift(var, val))),
+ Typed(e) => Typed(Box::new(e.subst_shift(var, val))),
Const(c) => Const(*c),
SuperType => SuperType,
}
@@ -252,9 +248,7 @@ impl TypedOrType {
}
fn normalize_to_type(self) -> Type<'static> {
match self {
- TypedOrType::Typed(e) => {
- e.partially_normalize().normalize_to_type()
- }
+ TypedOrType::Typed(e) => e.normalize_to_type(),
TypedOrType::Type(t) => t,
}
}
@@ -270,12 +264,10 @@ impl TypedOrType {
TypedOrType::Type(t) => Ok(t.get_type()?.into_owned()),
}
}
- fn partially_normalize(
- self,
- ) -> Result<PartiallyNormalized<'static>, TypeError> {
+ fn as_typed(&self) -> Result<Typed<'static>, TypeError> {
match self {
- TypedOrType::Typed(e) => Ok(e.partially_normalize()),
- TypedOrType::Type(t) => Ok(t.partially_normalize()?),
+ TypedOrType::Typed(e) => Ok(e.clone()),
+ TypedOrType::Type(t) => Ok(t.as_typed()?),
}
}
}
@@ -442,8 +434,12 @@ where
}
}
-fn const_to_pnormalized<'a>(c: Const) -> PartiallyNormalized<'a> {
- PartiallyNormalized(Value::Const(c), Some(type_of_const(c)), PhantomData)
+fn const_to_typed<'a>(c: Const) -> Typed<'a> {
+ Typed(
+ Value::Const(c).into_thunk(),
+ Some(type_of_const(c)),
+ PhantomData,
+ )
}
fn const_to_type<'a>(c: Const) -> Type<'a> {
@@ -555,7 +551,7 @@ pub(crate) enum TypeIntermediate {
impl TypeIntermediate {
fn typecheck(self) -> Result<TypedOrType, TypeError> {
let mkerr = |ctx, msg| TypeError::new(ctx, msg);
- match &self {
+ let typed = match &self {
TypeIntermediate::Pi(ctx, x, ta, tb) => {
let ctx2 = ctx.insert_type(x, ta.clone());
@@ -600,18 +596,16 @@ impl TypeIntermediate {
}
};
- let pnormalized = PartiallyNormalized(
+ Typed(
Value::Pi(
x.clone(),
TypeThunk::from_type(ta.clone()),
TypeThunk::from_type(tb.clone()),
- ),
+ )
+ .into_thunk(),
Some(const_to_type(k)),
PhantomData,
- );
- Ok(TypedOrType::Type(Type(TypeInternal::PNzed(Box::new(
- pnormalized,
- )))))
+ )
}
TypeIntermediate::RecordType(ctx, kts) => {
// Check that all types are the same const
@@ -634,20 +628,18 @@ impl TypeIntermediate {
// An empty record type has type Type
let k = k.unwrap_or(dhall_core::Const::Type);
- let pnormalized = PartiallyNormalized(
+ Typed(
Value::RecordType(
kts.iter()
.map(|(k, t)| {
(k.clone(), TypeThunk::from_type(t.clone()))
})
.collect(),
- ),
+ )
+ .into_thunk(),
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
@@ -675,7 +667,7 @@ impl TypeIntermediate {
// an union type with only unary variants also has type Type
let k = k.unwrap_or(dhall_core::Const::Type);
- let pnormalized = PartiallyNormalized(
+ Typed(
Value::UnionType(
kts.iter()
.map(|(k, t)| {
@@ -687,28 +679,24 @@ impl TypeIntermediate {
)
})
.collect(),
- ),
+ )
+ .into_thunk(),
Some(const_to_type(k)),
PhantomData,
- );
- Ok(TypedOrType::Type(Type(TypeInternal::PNzed(Box::new(
- pnormalized,
- )))))
+ )
}
TypeIntermediate::ListType(ctx, t) => {
ensure_simple_type!(
t,
mkerr(ctx, InvalidListType(t.clone().into_normalized()?)),
);
- let pnormalized = PartiallyNormalized(
+ Typed(
Value::from_builtin(Builtin::List)
- .app(t.clone().normalize_whnf()?),
+ .app(t.clone().normalize_whnf()?)
+ .into_thunk(),
Some(const_to_type(Const::Type)),
PhantomData,
- );
- Ok(TypedOrType::Type(Type(TypeInternal::PNzed(Box::new(
- pnormalized,
- )))))
+ )
}
TypeIntermediate::OptionalType(ctx, t) => {
ensure_simple_type!(
@@ -718,17 +706,18 @@ impl TypeIntermediate {
InvalidOptionalType(t.clone().into_normalized()?)
),
);
- let pnormalized = PartiallyNormalized(
+ Typed(
Value::from_builtin(Builtin::Optional)
- .app(t.clone().normalize_whnf()?),
+ .app(t.clone().normalize_whnf()?)
+ .into_thunk(),
Some(const_to_type(Const::Type)),
PhantomData,
- );
- Ok(TypedOrType::Type(Type(TypeInternal::PNzed(Box::new(
- pnormalized,
- )))))
+ )
}
- }
+ };
+ Ok(TypedOrType::Type(Type(TypeInternal::Typed(Box::new(
+ typed,
+ )))))
}
}
@@ -867,13 +856,11 @@ fn type_last_layer(
}
_ => return Err(mkerr(NotAFunction(f))),
};
- ensure_equal!(a.get_type()?, tx, {
+ ensure_equal!(a.get_type()?, &tx, {
mkerr(TypeMismatch(f.clone(), tx.clone().into_normalized()?, a))
});
- Ok(RetType(
- tb.subst_shift(&V(x.clone(), 0), &a.partially_normalize()?),
- ))
+ Ok(RetType(tb.subst_shift(&V(x.clone(), 0), &a.as_typed()?)))
}
Annot(x, t) => {
let t = t.normalize_to_type();
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 03:21:55 +0000