summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/normalize.rs84
-rw-r--r--dhall/src/traits/static_type.rs2
-rw-r--r--dhall/src/typecheck.rs68
3 files changed, 78 insertions, 76 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index dbb6d95..7a69bea 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -383,8 +383,8 @@ impl Value {
match self {
Value::Lam(x, t, e) => rc(ExprF::Lam(
x.clone(),
- t.normalize_nf().normalize_to_expr(),
- e.normalize_nf().normalize_to_expr(),
+ t.normalize_to_expr(),
+ e.normalize_to_expr(),
)),
Value::AppliedBuiltin(b, args) => {
let mut e = rc(ExprF::Builtin(*b));
@@ -394,18 +394,18 @@ impl Value {
e
}
Value::OptionalSomeClosure(n) => {
- let a = n.normalize_nf().normalize_to_expr();
+ let a = n.normalize_to_expr();
dhall::subexpr!(λ(x: a) -> Some x)
}
Value::ListConsClosure(n, None) => {
- let a = n.normalize_nf().normalize_to_expr();
+ let a = n.normalize_to_expr();
// Avoid accidental capture of the new `x` variable
let a1 = a.shift0(1, &"x".into());
dhall::subexpr!(λ(x : a) -> λ(xs : List a1) -> [ x ] # xs)
}
Value::ListConsClosure(n, Some(v)) => {
- let v = v.normalize_nf().normalize_to_expr();
- let a = n.normalize_nf().normalize_to_expr();
+ let v = v.normalize_to_expr();
+ let a = n.normalize_to_expr();
// Avoid accidental capture of the new `xs` variable
let v = v.shift0(1, &"xs".into());
dhall::subexpr!(λ(xs : List a) -> [ v ] # xs)
@@ -415,8 +415,8 @@ impl Value {
}
Value::Pi(x, t, e) => rc(ExprF::Pi(
x.clone(),
- t.normalize_nf().normalize_to_expr(),
- e.normalize_nf().normalize_to_expr(),
+ t.normalize_to_expr(),
+ e.normalize_to_expr(),
)),
Value::Var(v) => rc(ExprF::Var(v.clone())),
Value::Const(c) => rc(ExprF::Const(*c)),
@@ -425,41 +425,31 @@ impl Value {
Value::IntegerLit(n) => rc(ExprF::IntegerLit(*n)),
Value::EmptyOptionalLit(n) => rc(ExprF::App(
rc(ExprF::Builtin(Builtin::OptionalNone)),
- n.normalize_nf().normalize_to_expr(),
+ n.normalize_to_expr(),
)),
Value::NEOptionalLit(n) => {
- rc(ExprF::SomeLit(n.normalize_nf().normalize_to_expr()))
+ rc(ExprF::SomeLit(n.normalize_to_expr()))
}
Value::EmptyListLit(n) => {
- rc(ExprF::EmptyListLit(n.normalize_nf().normalize_to_expr()))
+ rc(ExprF::EmptyListLit(n.normalize_to_expr()))
}
Value::NEListLit(elts) => rc(ExprF::NEListLit(
- elts.into_iter()
- .map(|n| n.normalize_nf().normalize_to_expr())
- .collect(),
+ elts.into_iter().map(|n| n.normalize_to_expr()).collect(),
)),
Value::RecordLit(kvs) => rc(ExprF::RecordLit(
kvs.iter()
- .map(|(k, v)| {
- (k.clone(), v.normalize_nf().normalize_to_expr())
- })
+ .map(|(k, v)| (k.clone(), v.normalize_to_expr()))
.collect(),
)),
Value::RecordType(kts) => rc(ExprF::RecordType(
kts.iter()
- .map(|(k, v)| {
- (k.clone(), v.normalize_nf().normalize_to_expr())
- })
+ .map(|(k, v)| (k.clone(), v.normalize_to_expr()))
.collect(),
)),
Value::UnionType(kts) => rc(ExprF::UnionType(
kts.iter()
.map(|(k, v)| {
- (
- k.clone(),
- v.as_ref()
- .map(|v| v.normalize_nf().normalize_to_expr()),
- )
+ (k.clone(), v.as_ref().map(|v| v.normalize_to_expr()))
})
.collect(),
)),
@@ -467,25 +457,17 @@ impl Value {
let kts = kts
.iter()
.map(|(k, v)| {
- (
- k.clone(),
- v.as_ref()
- .map(|v| v.normalize_nf().normalize_to_expr()),
- )
+ (k.clone(), v.as_ref().map(|v| v.normalize_to_expr()))
})
.collect();
rc(ExprF::Field(rc(ExprF::UnionType(kts)), l.clone()))
}
Value::UnionLit(l, v, kts) => rc(ExprF::UnionLit(
l.clone(),
- v.normalize_nf().normalize_to_expr(),
+ v.normalize_to_expr(),
kts.iter()
.map(|(k, v)| {
- (
- k.clone(),
- v.as_ref()
- .map(|v| v.normalize_nf().normalize_to_expr()),
- )
+ (k.clone(), v.as_ref().map(|v| v.normalize_to_expr()))
})
.collect(),
)),
@@ -961,7 +943,10 @@ impl Value {
}
mod thunk {
- use super::{normalize_whnf, InputSubExpr, NormalizationContext, Value};
+ use super::{
+ normalize_whnf, InputSubExpr, NormalizationContext, OutputSubExpr,
+ Value,
+ };
use crate::expr::Typed;
use dhall_core::{Label, V};
use std::cell::{Ref, RefCell};
@@ -1108,6 +1093,10 @@ mod thunk {
Ref::map(self.0.borrow(), ThunkInternal::as_nf)
}
+ pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr {
+ self.normalize_nf().normalize_to_expr()
+ }
+
pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
self.0.borrow().shift(delta, var).into_thunk()
}
@@ -1148,6 +1137,7 @@ impl TypeThunk {
TypeThunk::Type(t)
}
+ // Deprecated
fn normalize(&self) -> TypeThunk {
match self {
TypeThunk::Thunk(th) => TypeThunk::Thunk(th.normalize()),
@@ -1162,6 +1152,18 @@ impl TypeThunk {
}
}
+ pub(crate) fn normalize_nf(&self) -> Value {
+ match self {
+ TypeThunk::Thunk(th) => th.normalize_nf().clone(),
+ // TODO: let's hope for the best with the unwrap
+ TypeThunk::Type(t) => t.normalize_whnf().unwrap().normalize(),
+ }
+ }
+
+ pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr {
+ self.normalize_nf().normalize_to_expr()
+ }
+
fn shift(&self, delta: isize, var: &V<Label>) -> Self {
match self {
TypeThunk::Thunk(th) => TypeThunk::Thunk(th.shift(delta, var)),
@@ -1179,14 +1181,6 @@ impl TypeThunk {
TypeThunk::Type(t) => TypeThunk::Type(t.subst_shift(var, val)),
}
}
-
- pub(crate) fn normalize_nf(&self) -> Value {
- match self {
- TypeThunk::Thunk(th) => th.normalize_nf().clone(),
- // TODO: let's hope for the best with the unwrap
- TypeThunk::Type(t) => t.normalize_whnf().unwrap().normalize(),
- }
- }
}
/// Reduces the imput expression to Value. See doc on `Value` for details.
diff --git a/dhall/src/traits/static_type.rs b/dhall/src/traits/static_type.rs
index 225eb32..8b5acbf 100644
--- a/dhall/src/traits/static_type.rs
+++ b/dhall/src/traits/static_type.rs
@@ -33,7 +33,7 @@ pub trait SimpleStaticType {
}
fn mktype<'a>(x: SubExpr<X, X>) -> SimpleType<'a> {
- SimpleType(x, std::marker::PhantomData)
+ x.into()
}
impl<T: SimpleStaticType> StaticType for T {
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index cdc53a3..e8bc26d 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -66,7 +66,7 @@ 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())?.to_type()
}
_ => Type(TypeInternal::Typed(Box::new(Typed(
Value::Expr(self.0).into_thunk(),
@@ -87,7 +87,7 @@ impl Normalized<'static> {
}
}
impl<'a> Typed<'a> {
- fn normalize_to_type(&self) -> Type<'a> {
+ fn to_type(&self) -> Type<'a> {
match &*self.normalize_whnf() {
Value::Const(c) => Type(TypeInternal::Const(*c)),
_ => Type(TypeInternal::Typed(Box::new(self.clone()))),
@@ -106,6 +106,9 @@ impl<'a> Type<'a> {
pub(crate) fn normalize_whnf(&self) -> Result<Value, TypeError> {
Ok(self.0.normalize_whnf()?)
}
+ fn as_const(&self) -> Option<Const> {
+ self.0.as_const()
+ }
fn internal(&self) -> &TypeInternal<'a> {
&self.0
}
@@ -192,6 +195,12 @@ impl<'a> TypeInternal<'a> {
}
})
}
+ fn as_const(&self) -> Option<Const> {
+ match self {
+ TypeInternal::Const(c) => Some(*c),
+ _ => None,
+ }
+ }
fn whnf(&self) -> Option<std::cell::Ref<Value>> {
match self {
TypeInternal::Typed(e) => Some(e.normalize_whnf()),
@@ -491,8 +500,8 @@ macro_rules! ensure_equal {
// Ensure the provided type has type `Type`
macro_rules! ensure_simple_type {
($x:expr, $err:expr $(,)*) => {{
- match $x.get_type()?.internal() {
- TypeInternal::Const(dhall_core::Const::Type) => {}
+ match $x.get_type()?.as_const() {
+ Some(dhall_core::Const::Type) => {}
_ => return Err($err),
}
}};
@@ -514,8 +523,8 @@ impl TypeIntermediate {
TypeIntermediate::Pi(ctx, x, ta, tb) => {
let ctx2 = ctx.insert_type(x, ta.clone());
- let kA = match ta.get_type()?.internal() {
- TypeInternal::Const(k) => *k,
+ let kA = match ta.get_type()?.as_const() {
+ Some(k) => k,
_ => {
return Err(mkerr(
ctx,
@@ -524,8 +533,8 @@ impl TypeIntermediate {
}
};
- let kB = match tb.get_type()?.internal() {
- TypeInternal::Const(k) => *k,
+ let kB = match tb.get_type()?.as_const() {
+ Some(k) => k,
_ => {
return Err(mkerr(
&ctx2,
@@ -570,9 +579,9 @@ impl TypeIntermediate {
// Check that all types are the same const
let mut k = None;
for (x, t) in kts {
- match (k, t.get_type()?.internal()) {
- (None, TypeInternal::Const(k2)) => k = Some(*k2),
- (Some(k1), TypeInternal::Const(k2)) if k1 == *k2 => {}
+ match (k, t.get_type()?.as_const()) {
+ (None, Some(k2)) => k = Some(k2),
+ (Some(k1), Some(k2)) if k1 == k2 => {}
_ => {
return Err(mkerr(
ctx,
@@ -602,10 +611,9 @@ impl TypeIntermediate {
let mut k = None;
for (x, t) in kts {
if let Some(t) = t {
- match (k, t.get_type()?.internal()) {
- (None, TypeInternal::Const(k2)) => k = Some(*k2),
- (Some(k1), TypeInternal::Const(k2))
- if k1 == *k2 => {}
+ match (k, t.get_type()?.as_const()) {
+ (None, Some(k2)) => k = Some(k2),
+ (Some(k1), Some(k2)) if k1 == k2 => {}
_ => {
return Err(mkerr(
ctx,
@@ -677,7 +685,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)?.to_type())
}
fn builtin_to_type<'a>(b: Builtin) -> Result<Type<'a>, TypeError> {
@@ -713,7 +721,7 @@ fn type_with(
Ok(RetType(
TypeIntermediate::Pi(ctx.clone(), x.clone(), tx, tb)
.typecheck()?
- .normalize_to_type(),
+ .to_type(),
))
}
Pi(x, ta, tb) => {
@@ -813,7 +821,7 @@ fn type_last_layer(
Ok(RetType(tb.subst_shift(&V(x.clone(), 0), &a)))
}
Annot(x, t) => {
- let t = t.normalize_to_type();
+ let t = t.to_type();
ensure_equal!(
&t,
x.get_type()?,
@@ -847,11 +855,11 @@ fn type_last_layer(
Ok(RetType(y.get_type_move()?))
}
EmptyListLit(t) => {
- let t = t.normalize_to_type();
+ let t = t.to_type();
Ok(RetType(
TypeIntermediate::ListType(ctx.clone(), t)
.typecheck()?
- .normalize_to_type(),
+ .to_type(),
))
}
NEListLit(xs) => {
@@ -872,7 +880,7 @@ fn type_last_layer(
Ok(RetType(
TypeIntermediate::ListType(ctx.clone(), t)
.typecheck()?
- .normalize_to_type(),
+ .to_type(),
))
}
SomeLit(x) => {
@@ -880,13 +888,13 @@ fn type_last_layer(
Ok(RetType(
TypeIntermediate::OptionalType(ctx.clone(), t)
.typecheck()?
- .normalize_to_type(),
+ .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.to_type())))
.collect::<Result<_, _>>()?;
Ok(RetTyped(
TypeIntermediate::RecordType(ctx.clone(), kts).typecheck()?,
@@ -900,7 +908,7 @@ fn type_last_layer(
x,
match t {
None => None,
- Some(t) => Some(t.normalize_to_type()),
+ Some(t) => Some(t.to_type()),
},
))
})
@@ -917,7 +925,7 @@ fn type_last_layer(
Ok(RetType(
TypeIntermediate::RecordType(ctx.clone(), kts)
.typecheck()?
- .normalize_to_type(),
+ .to_type(),
))
}
UnionLit(x, v, kvs) => {
@@ -925,7 +933,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.to_type()),
None => None,
};
Ok((x, t))
@@ -936,7 +944,7 @@ fn type_last_layer(
Ok(RetType(
TypeIntermediate::UnionType(ctx.clone(), kts)
.typecheck()?
- .normalize_to_type(),
+ .to_type(),
))
}
Field(r, x) => {
@@ -953,7 +961,7 @@ fn type_last_layer(
},
// TODO: branch here only when r.get_type() is a Const
_ => {
- let r = r.normalize_to_type();
+ let r = r.to_type();
let r_internal = r.internal_whnf();
match r_internal.deref() {
Some(Value::UnionType(kts)) => match kts.get(&x) {
@@ -970,7 +978,7 @@ fn type_last_layer(
r,
)
.typecheck()?
- .normalize_to_type(),
+ .to_type(),
))
},
Some(None) => {
@@ -996,7 +1004,7 @@ fn type_last_layer(
}
// _ => Err(mkerr(NotARecord(
// x,
- // r.normalize_to_type()?.into_normalized()?,
+ // r.to_type()?.into_normalized()?,
// ))),
}
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 04:16:29 +0000