summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/expr.rs158
-rw-r--r--dhall/src/normalize.rs50
-rw-r--r--dhall/src/tests.rs9
-rw-r--r--dhall/src/traits/deserialize.rs2
-rw-r--r--dhall/src/traits/dynamic_type.rs24
-rw-r--r--dhall/src/traits/static_type.rs8
-rw-r--r--dhall/src/typecheck.rs273
7 files changed, 282 insertions, 242 deletions
diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index a753ffd..4d55f4a 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -1,4 +1,5 @@
use crate::imports::ImportRoot;
+use crate::normalize::{Thunk, Value};
use dhall_core::*;
use std::marker::PhantomData;
@@ -36,23 +37,23 @@ pub(crate) struct Resolved<'a>(
);
derive_other_traits!(Resolved);
+pub(crate) use self::typed::TypedInternal;
+
#[derive(Debug, Clone)]
pub(crate) struct Typed<'a>(
- pub(crate) crate::normalize::Thunk,
- pub(crate) Option<Type<'static>>,
+ pub(crate) TypedInternal,
pub(crate) PhantomData<&'a ()>,
);
#[derive(Debug, Clone)]
pub(crate) struct Normalized<'a>(
- pub(crate) crate::normalize::Thunk,
- pub(crate) Option<Type<'static>>,
+ pub(crate) TypedInternal,
pub(crate) PhantomData<&'a ()>,
);
impl<'a> std::cmp::PartialEq for Normalized<'a> {
fn eq(&self, other: &Self) -> bool {
- self.0.normalize_to_expr() == other.0.normalize_to_expr()
+ self.to_expr() == other.to_expr()
}
}
@@ -60,7 +61,110 @@ impl<'a> std::cmp::Eq for Normalized<'a> {}
impl<'a> std::fmt::Display for Normalized<'a> {
fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> {
- self.0.normalize_to_expr().fmt(f)
+ self.to_expr().fmt(f)
+ }
+}
+
+mod typed {
+ use super::{Type, Typed};
+ use crate::normalize::{Thunk, Value};
+ use crate::typecheck::{
+ TypeError, TypeInternal, TypeMessage, TypecheckContext,
+ };
+ use dhall_core::{Const, Label, SubExpr, V, X};
+ use std::borrow::Cow;
+ use std::marker::PhantomData;
+
+ #[derive(Debug, Clone)]
+ pub(crate) enum TypedInternal {
+ // The `Sort` higher-kinded type doesn't have a type
+ Sort,
+ // Any other value, along with its type
+ Value(Thunk, Option<Type<'static>>),
+ }
+
+ impl TypedInternal {
+ pub(crate) fn from_thunk_and_type(th: Thunk, t: Type<'static>) -> Self {
+ TypedInternal::Value(th, Some(t))
+ }
+
+ pub(crate) fn from_thunk_untyped(th: Thunk) -> Self {
+ TypedInternal::Value(th, None)
+ }
+
+ // TODO: Avoid cloning if possible
+ pub(crate) fn to_value(&self) -> Value {
+ match self {
+ TypedInternal::Value(th, _) => th.normalize_whnf().clone(),
+ TypedInternal::Sort => Value::Const(Const::Sort),
+ }
+ }
+
+ pub(crate) fn to_expr(&self) -> SubExpr<X, X> {
+ self.to_value().normalize_to_expr()
+ }
+
+ pub(crate) fn to_thunk(&self) -> Thunk {
+ match self {
+ TypedInternal::Value(th, _) => th.clone(),
+ TypedInternal::Sort => {
+ Thunk::from_whnf(Value::Const(Const::Sort))
+ }
+ }
+ }
+
+ pub(crate) fn to_type(&self) -> Type<'static> {
+ match self {
+ TypedInternal::Sort => Type(TypeInternal::Const(Const::Sort)),
+ TypedInternal::Value(th, _) => match &*th.normalize_whnf() {
+ Value::Const(c) => Type(TypeInternal::Const(*c)),
+ _ => Type(TypeInternal::Typed(Box::new(Typed(
+ self.clone(),
+ PhantomData,
+ )))),
+ },
+ }
+ }
+
+ pub(crate) fn get_type(
+ &self,
+ ) -> Result<Cow<'_, Type<'static>>, TypeError> {
+ match self {
+ TypedInternal::Value(_, Some(t)) => Ok(Cow::Borrowed(t)),
+ TypedInternal::Value(_, None) => Err(TypeError::new(
+ &TypecheckContext::new(),
+ TypeMessage::Untyped,
+ )),
+ TypedInternal::Sort => Err(TypeError::new(
+ &TypecheckContext::new(),
+ TypeMessage::Sort,
+ )),
+ }
+ }
+
+ pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ match self {
+ TypedInternal::Value(th, t) => TypedInternal::Value(
+ th.shift(delta, var),
+ t.as_ref().map(|x| x.shift(delta, var)),
+ ),
+ TypedInternal::Sort => TypedInternal::Sort,
+ }
+ }
+
+ pub(crate) fn subst_shift(
+ &self,
+ var: &V<Label>,
+ val: &Typed<'static>,
+ ) -> Self {
+ match self {
+ TypedInternal::Value(th, t) => TypedInternal::Value(
+ th.subst_shift(var, val),
+ t.as_ref().map(|x| x.subst_shift(var, val)),
+ ),
+ TypedInternal::Sort => TypedInternal::Sort,
+ }
+ }
}
}
@@ -88,10 +192,7 @@ pub struct Type<'a>(pub(crate) TypeInternal<'a>);
impl<'a> std::fmt::Display for Type<'a> {
fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> {
- match self.0.clone().into_normalized() {
- Ok(e) => e.fmt(f),
- Err(_) => write!(f, "SuperType"),
- }
+ self.to_normalized().fmt(f)
}
}
@@ -115,39 +216,38 @@ impl<'a> From<SubExpr<X, X>> for SimpleType<'a> {
#[doc(hidden)]
impl<'a> From<Normalized<'a>> for Typed<'a> {
fn from(x: Normalized<'a>) -> Typed<'a> {
- Typed(x.0, x.1, x.2)
+ Typed(x.0, x.1)
}
}
impl<'a> Normalized<'a> {
+ pub(crate) fn from_thunk_and_type(th: Thunk, t: Type<'static>) -> Self {
+ Normalized(TypedInternal::from_thunk_and_type(th, t), PhantomData)
+ }
// Deprecated
pub(crate) fn as_expr(&self) -> SubExpr<X, X> {
- self.0.normalize_to_expr()
+ self.0.to_expr()
}
pub(crate) fn to_expr(&self) -> SubExpr<X, X> {
- self.0.normalize_to_expr()
+ self.0.to_expr()
}
- pub(crate) fn to_value(&self) -> crate::normalize::Value {
- self.0.normalize_nf().clone()
+ pub(crate) fn to_value(&self) -> Value {
+ self.0.to_value()
}
#[allow(dead_code)]
pub(crate) fn unnote<'b>(self) -> Normalized<'b> {
- Normalized(self.0, self.1, PhantomData)
+ Normalized(self.0, PhantomData)
}
}
-#[doc(hidden)]
-impl<'a> Type<'a> {
- pub(crate) fn unnote<'b>(self) -> Type<'b> {
- // use TypeInternal::*;
- // Type(match self.0 {
- // Expr(e) => Expr(Box::new(e.unnote())),
- // Pi(ctx, c, x, t, e) => Pi(ctx, c, x, t, e),
- // Const(c) => Const(c),
- // SuperType => SuperType,
- // })
-
- // Yes, this is positively horrible. Please forgive me.
- unsafe { std::mem::transmute::<Type<'a>, Type<'b>>(self) }
+impl<'a> Typed<'a> {
+ pub(crate) fn from_thunk_and_type(th: Thunk, t: Type<'static>) -> Self {
+ Typed(TypedInternal::from_thunk_and_type(th, t), PhantomData)
+ }
+ pub(crate) fn from_thunk_untyped(th: Thunk) -> Self {
+ Typed(TypedInternal::from_thunk_untyped(th), PhantomData)
+ }
+ pub(crate) fn const_sort() -> Self {
+ Typed(TypedInternal::Sort, PhantomData)
}
}
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 390911a..a023d38 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, Type, Typed};
+use crate::expr::{Normalized, Type, Typed, TypedInternal};
type InputSubExpr = SubExpr<X, Normalized<'static>>;
type OutputSubExpr = SubExpr<X, X>;
@@ -25,11 +25,17 @@ impl<'a> Typed<'a> {
/// leave ill-typed sub-expressions unevaluated.
///
pub fn normalize(self) -> Normalized<'a> {
- // TODO: stupid but needed for now
- let thunk = Thunk::from_normalized_expr(self.0.normalize_to_expr());
- // let thunk = self.0;
- thunk.normalize_nf();
- Normalized(thunk, self.1, self.2)
+ let internal = match self.0 {
+ TypedInternal::Sort => TypedInternal::Sort,
+ TypedInternal::Value(thunk, t) => {
+ // TODO: stupid but needed for now
+ let thunk =
+ Thunk::from_normalized_expr(thunk.normalize_to_expr());
+ thunk.normalize_nf();
+ TypedInternal::Value(thunk, t)
+ }
+ };
+ Normalized(internal, self.1)
}
pub(crate) fn shift0(&self, delta: isize, x: &Label) -> Self {
@@ -37,11 +43,7 @@ impl<'a> Typed<'a> {
}
pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
- Typed(
- self.0.shift(delta, var),
- self.1.as_ref().map(|x| x.shift(delta, var)),
- self.2,
- )
+ Typed(self.0.shift(delta, var), self.1)
}
pub(crate) fn subst_shift(
@@ -49,19 +51,15 @@ impl<'a> Typed<'a> {
var: &V<Label>,
val: &Typed<'static>,
) -> Self {
- Typed(
- self.0.subst_shift(var, val),
- self.1.as_ref().map(|x| x.subst_shift(var, val)),
- self.2,
- )
+ Typed(self.0.subst_shift(var, val), self.1)
}
- pub(crate) fn normalize_whnf(&self) -> std::cell::Ref<Value> {
- self.0.normalize_whnf()
+ pub(crate) fn to_value(&self) -> Value {
+ self.0.to_value()
}
- pub(crate) fn as_thunk(&self) -> Thunk {
- self.0.clone()
+ pub(crate) fn to_thunk(&self) -> Thunk {
+ self.0.to_thunk()
}
}
@@ -278,7 +276,7 @@ impl EnvItem {
) -> Self {
match self {
EnvItem::Thunk(e) => EnvItem::Thunk(e.subst_shift(var, val)),
- EnvItem::Skip(v) if v == var => EnvItem::Thunk(val.as_thunk()),
+ EnvItem::Skip(v) if v == var => EnvItem::Thunk(val.to_thunk()),
EnvItem::Skip(v) => EnvItem::Skip(v.shift(-1, var)),
}
}
@@ -695,7 +693,10 @@ impl Value {
match self {
Value::Lam(x, _, e) => {
- let val = Typed(th, None, std::marker::PhantomData);
+ let val = Typed(
+ TypedInternal::Value(th, None),
+ std::marker::PhantomData,
+ );
e.subst_shift(&V(x, 0), &val).normalize_whnf().clone()
}
Value::AppliedBuiltin(b, mut args) => {
@@ -867,7 +868,7 @@ impl Value {
t.subst_shift(var, val),
e.subst_shift(&var.shift0(1, x), &val.shift0(1, x)),
),
- Value::Var(v) if v == var => val.normalize_whnf().clone(),
+ Value::Var(v) if v == var => val.to_value().clone(),
Value::Var(v) => Value::Var(v.shift(-1, var)),
Value::Const(c) => Value::Const(*c),
Value::BoolLit(b) => Value::BoolLit(*b),
@@ -1163,8 +1164,7 @@ 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(),
+ TypeThunk::Type(t) => t.to_value().normalize(),
}
}
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index ebca256..ecd6e43 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -134,15 +134,12 @@ pub fn run_test(
assert_eq_display!(expr, expected);
}
Typecheck => {
- expr.typecheck_with(&expected.into_type()?)?;
+ expr.typecheck_with(&expected.to_type())?;
}
TypeInference => {
let expr = expr.typecheck()?;
- let ty = expr.get_type()?;
- assert_eq_display!(
- ty.as_normalized()?.as_expr(),
- expected.into_type()?.as_normalized()?.as_expr()
- );
+ let ty = expr.get_type()?.into_owned();
+ assert_eq_display!(ty.to_normalized(), expected);
}
Normalization => {
let expr = expr.skip_typecheck().normalize();
diff --git a/dhall/src/traits/deserialize.rs b/dhall/src/traits/deserialize.rs
index 9cc2147..99ca5ee 100644
--- a/dhall/src/traits/deserialize.rs
+++ b/dhall/src/traits/deserialize.rs
@@ -48,6 +48,6 @@ impl<'de: 'a, 'a> Deserialize<'de> for Normalized<'a> {
impl<'de: 'a, 'a> Deserialize<'de> for Type<'a> {
fn from_str(s: &'de str, ty: Option<&Type>) -> Result<Self> {
- Ok(Normalized::from_str(s, ty)?.into_type()?)
+ Ok(Normalized::from_str(s, ty)?.to_type())
}
}
diff --git a/dhall/src/traits/dynamic_type.rs b/dhall/src/traits/dynamic_type.rs
index c15b277..74c2e0a 100644
--- a/dhall/src/traits/dynamic_type.rs
+++ b/dhall/src/traits/dynamic_type.rs
@@ -1,9 +1,7 @@
use crate::expr::*;
use crate::traits::StaticType;
#[allow(unused_imports)]
-use crate::typecheck::{
- type_of_const, TypeError, TypeMessage, TypecheckContext,
-};
+use crate::typecheck::{TypeError, TypeMessage, TypecheckContext};
#[allow(unused_imports)]
use dhall_core::{Const, ExprF};
use std::borrow::Cow;
@@ -20,32 +18,18 @@ impl<T: StaticType> DynamicType for T {
impl<'a> DynamicType for Type<'a> {
fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> {
- Ok(Cow::Owned(
- self.clone().into_normalized()?.get_type()?.into_owned(),
- ))
+ self.get_type()
}
}
impl<'a> DynamicType for Normalized<'a> {
fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> {
- match &self.1 {
- Some(t) => Ok(Cow::Borrowed(t)),
- None => Err(TypeError::new(
- &TypecheckContext::new(),
- TypeMessage::Untyped,
- )),
- }
+ self.0.get_type()
}
}
impl<'a> DynamicType for Typed<'a> {
fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> {
- match &self.1 {
- Some(t) => Ok(Cow::Borrowed(t)),
- None => Err(TypeError::new(
- &TypecheckContext::new(),
- TypeMessage::Untyped,
- )),
- }
+ self.0.get_type()
}
}
diff --git a/dhall/src/traits/static_type.rs b/dhall/src/traits/static_type.rs
index 4dd9961..df6a177 100644
--- a/dhall/src/traits/static_type.rs
+++ b/dhall/src/traits/static_type.rs
@@ -38,15 +38,13 @@ fn mktype<'a>(x: SubExpr<X, X>) -> SimpleType<'a> {
impl<T: SimpleStaticType> StaticType for T {
fn get_static_type() -> Type<'static> {
- crate::expr::Normalized(
+ crate::expr::Normalized::from_thunk_and_type(
crate::normalize::Thunk::from_normalized_expr(
T::get_simple_static_type().into(),
),
- Some(Type::const_type()),
- std::marker::PhantomData,
+ Type::const_type(),
)
- .into_type()
- .unwrap()
+ .to_type()
}
}
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 8afbb2b..582930b 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::collections::BTreeMap;
use std::fmt;
-use std::marker::PhantomData;
use crate::expr::*;
use crate::normalize::{NormalizationContext, Thunk, TypeThunk, Value};
@@ -24,71 +23,52 @@ impl<'a> Resolved<'a> {
ty: &Type,
) -> Result<Typed<'static>, TypeError> {
let expr: SubExpr<_, _> = self.0.unnote();
- let ty: SubExpr<_, _> = ty.clone().unnote().embed()?;
- type_of(dhall::subexpr!(expr: ty))
+ let ty: SubExpr<_, _> = ty.to_expr().embed_absurd();
+ type_of(rc(ExprF::Annot(expr, ty)))
}
/// Pretends this expression has been typechecked. Use with care.
#[allow(dead_code)]
pub fn skip_typecheck(self) -> Typed<'a> {
- Typed(
- Thunk::new(NormalizationContext::new(), self.0.unnote()),
- None,
- PhantomData,
- )
+ Typed::from_thunk_untyped(Thunk::new(
+ NormalizationContext::new(),
+ self.0.unnote(),
+ ))
}
}
+
impl<'a> Typed<'a> {
- fn get_type_move(self) -> Result<Type<'static>, TypeError> {
- self.1.ok_or_else(|| {
- TypeError::new(&TypecheckContext::new(), TypeMessage::Untyped)
- })
+ fn to_type(&self) -> Type<'a> {
+ match &self.to_value() {
+ Value::Const(c) => Type(TypeInternal::Const(*c)),
+ _ => Type(TypeInternal::Typed(Box::new(self.clone()))),
+ }
}
}
+
impl<'a> Normalized<'a> {
fn shift0(&self, delta: isize, label: &Label) -> Self {
self.shift(delta, &V(label.clone(), 0))
}
fn shift(&self, delta: isize, var: &V<Label>) -> Self {
- Normalized(
- self.0.shift(delta, var),
- self.1.as_ref().map(|t| t.shift(delta, var)),
- self.2,
- )
+ Normalized(self.0.shift(delta, var), self.1)
}
- pub(crate) fn into_type(self) -> Result<Type<'a>, TypeError> {
- let typed: Typed = self.into();
- Ok(typed.to_type())
- }
- fn get_type_move(self) -> Result<Type<'static>, TypeError> {
- self.1.ok_or_else(|| {
- TypeError::new(&TypecheckContext::new(), TypeMessage::Untyped)
- })
- }
-}
-impl Normalized<'static> {
- fn embed<N>(self) -> SubExpr<N, Normalized<'static>> {
- rc(ExprF::Embed(self))
- }
-}
-impl<'a> Typed<'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()))),
- }
+ pub(crate) fn to_type(self) -> Type<'a> {
+ self.0.to_type()
}
}
+
impl<'a> Type<'a> {
- pub(crate) fn as_normalized(
- &self,
- ) -> Result<Cow<Normalized<'a>>, TypeError> {
- Ok(Cow::Owned(self.0.clone().into_normalized()?))
+ pub(crate) fn to_normalized(&self) -> Normalized<'a> {
+ self.0.to_normalized()
+ }
+ pub(crate) fn to_expr(&self) -> SubExpr<X, X> {
+ self.0.to_expr()
}
- pub(crate) fn into_normalized(self) -> Result<Normalized<'a>, TypeError> {
- self.0.into_normalized()
+ pub(crate) fn to_value(&self) -> Value {
+ self.0.to_value()
}
- pub(crate) fn normalize_whnf(&self) -> Result<Value, TypeError> {
- Ok(self.0.normalize_whnf()?)
+ pub(crate) fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> {
+ self.0.get_type()
}
fn as_const(&self) -> Option<Const> {
self.0.as_const()
@@ -96,7 +76,7 @@ impl<'a> Type<'a> {
fn internal(&self) -> &TypeInternal<'a> {
&self.0
}
- fn internal_whnf(&self) -> Option<std::cell::Ref<Value>> {
+ fn internal_whnf(&self) -> Option<Value> {
self.0.whnf()
}
pub(crate) fn shift0(&self, delta: isize, label: &Label) -> Self {
@@ -123,14 +103,9 @@ impl<'a> Type<'a> {
Type(TypeInternal::Const(Const::Type))
}
}
-impl Type<'static> {
- fn embed<N>(self) -> Result<SubExpr<N, Normalized<'static>>, TypeError> {
- Ok(self.into_normalized()?.embed())
- }
-}
impl TypeThunk {
- fn normalize_to_type(
+ fn to_type(
&self,
ctx: &TypecheckContext,
) -> Result<Type<'static>, TypeError> {
@@ -138,10 +113,7 @@ impl TypeThunk {
TypeThunk::Type(t) => Ok(t.clone()),
TypeThunk::Thunk(th) => {
// TODO: rule out statically
- mktype(
- ctx,
- th.normalize_whnf().normalize_to_expr().embed_absurd(),
- )
+ mktype(ctx, th.normalize_to_expr().embed_absurd())
}
}
}
@@ -154,29 +126,30 @@ impl TypeThunk {
#[derive(Debug, Clone)]
pub(crate) enum TypeInternal<'a> {
Const(Const),
- /// The type of `Sort`
- SuperType,
- /// This must not contain Const value.
+ /// This must not contain a Const value.
Typed(Box<Typed<'a>>),
}
impl<'a> TypeInternal<'a> {
- pub(crate) fn into_normalized(&self) -> Result<Normalized<'a>, TypeError> {
- Ok(self.as_typed()?.normalize())
+ fn to_typed(&self) -> Typed<'a> {
+ match self {
+ TypeInternal::Typed(e) => e.as_ref().clone(),
+ TypeInternal::Const(c) => const_to_typed(*c),
+ }
+ }
+ fn to_normalized(&self) -> Normalized<'a> {
+ self.to_typed().normalize()
}
- fn normalize_whnf(&self) -> Result<Value, TypeError> {
- Ok(self.as_typed()?.normalize_whnf().clone())
+ fn to_expr(&self) -> SubExpr<X, X> {
+ self.to_normalized().to_expr()
}
- fn as_typed(&self) -> Result<Typed<'a>, TypeError> {
+ fn to_value(&self) -> Value {
+ self.to_typed().to_value().clone()
+ }
+ pub(crate) fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> {
Ok(match self {
- TypeInternal::Typed(e) => e.as_ref().clone(),
- TypeInternal::Const(c) => const_to_typed(*c),
- TypeInternal::SuperType => {
- return Err(TypeError::new(
- &TypecheckContext::new(),
- TypeMessage::Untyped,
- ))
- }
+ TypeInternal::Typed(e) => e.get_type()?,
+ TypeInternal::Const(c) => Cow::Owned(type_of_const(*c)?),
})
}
fn as_const(&self) -> Option<Const> {
@@ -185,9 +158,9 @@ impl<'a> TypeInternal<'a> {
_ => None,
}
}
- fn whnf(&self) -> Option<std::cell::Ref<Value>> {
+ fn whnf(&self) -> Option<Value> {
match self {
- TypeInternal::Typed(e) => Some(e.normalize_whnf()),
+ TypeInternal::Typed(e) => Some(e.to_value()),
_ => None,
}
}
@@ -199,7 +172,6 @@ impl<'a> TypeInternal<'a> {
match self {
Typed(e) => Typed(Box::new(e.shift(delta, var))),
Const(c) => Const(*c),
- SuperType => SuperType,
}
}
fn subst_shift(&self, var: &V<Label>, val: &Typed<'static>) -> Self {
@@ -207,7 +179,6 @@ impl<'a> TypeInternal<'a> {
match self {
Typed(e) => Typed(Box::new(e.subst_shift(var, val))),
Const(c) => Const(*c),
- SuperType => SuperType,
}
}
}
@@ -215,12 +186,7 @@ impl<'a> TypeInternal<'a> {
impl<'a> Eq for TypeInternal<'a> {}
impl<'a> PartialEq for TypeInternal<'a> {
fn eq(&self, other: &Self) -> bool {
- let self_nzed = self.clone().into_normalized();
- let other_nzed = other.clone().into_normalized();
- match (self_nzed, other_nzed) {
- (Ok(x), Ok(y)) => x == y,
- _ => false,
- }
+ self.to_normalized() == other.to_normalized()
}
}
@@ -369,17 +335,14 @@ where
}
}
match (eL0.borrow().internal(), eR0.borrow().internal()) {
- (TypeInternal::SuperType, TypeInternal::SuperType) => true,
- (TypeInternal::SuperType, _) => false,
- (_, TypeInternal::SuperType) => false,
// (TypeInternal::Const(cl), TypeInternal::Const(cr)) => cl == cr,
// (TypeInternal::Expr(l), TypeInternal::Expr(r)) => {
_ => {
let mut ctx = vec![];
go(
&mut ctx,
- &eL0.borrow().as_normalized().unwrap().to_expr(),
- &eR0.borrow().as_normalized().unwrap().to_expr(),
+ &eL0.borrow().to_expr(),
+ &eR0.borrow().to_expr(),
)
}
// _ => false,
@@ -387,22 +350,29 @@ where
}
fn const_to_typed<'a>(c: Const) -> Typed<'a> {
- Typed(
- Value::Const(c).into_thunk(),
- Some(type_of_const(c)),
- PhantomData,
- )
+ match c {
+ Const::Sort => Typed::const_sort(),
+ _ => Typed::from_thunk_and_type(
+ Value::Const(c).into_thunk(),
+ type_of_const(c).unwrap(),
+ ),
+ }
}
fn const_to_type<'a>(c: Const) -> Type<'a> {
Type(TypeInternal::Const(c))
}
-pub(crate) fn type_of_const<'a>(c: Const) -> Type<'a> {
+fn type_of_const<'a>(c: Const) -> Result<Type<'a>, TypeError> {
match c {
- Const::Type => Type::const_kind(),
- Const::Kind => Type::const_sort(),
- Const::Sort => Type(TypeInternal::SuperType),
+ Const::Type => Ok(Type::const_kind()),
+ Const::Kind => Ok(Type::const_sort()),
+ Const::Sort => {
+ return Err(TypeError::new(
+ &TypecheckContext::new(),
+ TypeMessage::Sort,
+ ))
+ }
}
}
@@ -512,7 +482,7 @@ impl TypeIntermediate {
_ => {
return Err(mkerr(
ctx,
- InvalidInputType(ta.clone().into_normalized()?),
+ InvalidInputType(ta.clone().to_normalized()),
))
}
};
@@ -524,9 +494,9 @@ impl TypeIntermediate {
&ctx2,
InvalidOutputType(
tb.clone()
- .into_normalized()?
- .get_type_move()?
- .into_normalized()?,
+ .to_normalized()
+ .get_type()?
+ .to_normalized(),
),
))
}
@@ -538,25 +508,24 @@ impl TypeIntermediate {
return Err(mkerr(
ctx,
NoDependentTypes(
- ta.clone().into_normalized()?,
+ ta.clone().to_normalized(),
tb.clone()
- .into_normalized()?
- .get_type_move()?
- .into_normalized()?,
+ .to_normalized()
+ .get_type()?
+ .to_normalized(),
),
))
}
};
- Typed(
+ Typed::from_thunk_and_type(
Value::Pi(
x.clone(),
TypeThunk::from_type(ta.clone()),
TypeThunk::from_type(tb.clone()),
)
.into_thunk(),
- Some(const_to_type(k)),
- PhantomData,
+ const_to_type(k),
)
}
TypeIntermediate::RecordType(ctx, kts) => {
@@ -577,7 +546,7 @@ impl TypeIntermediate {
// An empty record type has type Type
let k = k.unwrap_or(dhall_core::Const::Type);
- Typed(
+ Typed::from_thunk_and_type(
Value::RecordType(
kts.iter()
.map(|(k, t)| {
@@ -586,8 +555,7 @@ impl TypeIntermediate {
.collect(),
)
.into_thunk(),
- Some(const_to_type(k)),
- PhantomData,
+ const_to_type(k),
)
}
TypeIntermediate::UnionType(ctx, kts) => {
@@ -612,7 +580,7 @@ impl TypeIntermediate {
// an union type with only unary variants also has type Type
let k = k.unwrap_or(dhall_core::Const::Type);
- Typed(
+ Typed::from_thunk_and_type(
Value::UnionType(
kts.iter()
.map(|(k, t)| {
@@ -626,37 +594,31 @@ impl TypeIntermediate {
.collect(),
)
.into_thunk(),
- Some(const_to_type(k)),
- PhantomData,
+ const_to_type(k),
)
}
TypeIntermediate::ListType(ctx, t) => {
ensure_simple_type!(
t,
- mkerr(ctx, InvalidListType(t.clone().into_normalized()?)),
+ mkerr(ctx, InvalidListType(t.clone().to_normalized())),
);
- Typed(
+ Typed::from_thunk_and_type(
Value::from_builtin(Builtin::List)
- .app(t.normalize_whnf()?)
+ .app(t.to_value())
.into_thunk(),
- Some(const_to_type(Const::Type)),
- PhantomData,
+ const_to_type(Const::Type),
)
}
TypeIntermediate::OptionalType(ctx, t) => {
ensure_simple_type!(
t,
- mkerr(
- ctx,
- InvalidOptionalType(t.clone().into_normalized()?)
- ),
+ mkerr(ctx, InvalidOptionalType(t.clone().to_normalized())),
);
- Typed(
+ Typed::from_thunk_and_type(
Value::from_builtin(Builtin::Optional)
- .app(t.normalize_whnf()?)
+ .app(t.to_value())
.into_thunk(),
- Some(const_to_type(Const::Type)),
- PhantomData,
+ const_to_type(Const::Type),
)
}
})
@@ -701,7 +663,7 @@ fn type_with(
let tx = mktype(ctx, t.clone())?;
let ctx2 = ctx.insert_type(x, tx.clone());
let b = type_with(&ctx2, b.clone())?;
- let tb = b.get_type_move()?;
+ let tb = b.get_type()?.into_owned();
Ok(RetType(
TypeIntermediate::Pi(ctx.clone(), x.clone(), tx, tb)
.typecheck()?
@@ -727,7 +689,7 @@ fn type_with(
let v = type_with(ctx, v)?.normalize();
let e = type_with(&ctx.insert_value(x, v.clone()), e.clone())?;
- Ok(RetType(e.get_type_move()?))
+ Ok(RetType(e.get_type()?.into_owned()))
}
OldOptionalLit(None, t) => {
let t = t.clone();
@@ -749,15 +711,13 @@ fn type_with(
),
}?;
Ok(match ret {
- RetExpr(ret) => Typed(
+ RetExpr(ret) => Typed::from_thunk_and_type(
Thunk::new(ctx.to_normalization_ctx(), e),
- Some(mktype(ctx, rc(ret))?),
- PhantomData,
+ mktype(ctx, rc(ret))?,
),
- RetType(typ) => Typed(
+ RetType(typ) => Typed::from_thunk_and_type(
Thunk::new(ctx.to_normalization_ctx(), e),
- Some(typ),
- PhantomData,
+ typ,
),
RetTyped(tt) => tt,
})
@@ -787,7 +747,7 @@ fn type_last_layer(
App(f, a) => {
let tf = f.get_type()?;
let tf_internal = tf.internal_whnf();
- let (x, tx, tb) = match tf_internal.deref() {
+ let (x, tx, tb) = match &tf_internal {
Some(Value::Pi(
x,
TypeThunk::Type(tx),
@@ -799,7 +759,7 @@ fn type_last_layer(
_ => return Err(mkerr(NotAFunction(f.clone()))),
};
ensure_equal!(a.get_type()?, tx, {
- mkerr(TypeMismatch(f.clone(), tx.clone().into_normalized()?, a))
+ mkerr(TypeMismatch(f.clone(), tx.clone().to_normalized(), a))
});
Ok(RetType(tb.subst_shift(&V(x.clone(), 0), &a)))
@@ -809,9 +769,9 @@ fn type_last_layer(
ensure_equal!(
&t,
x.get_type()?,
- mkerr(AnnotMismatch(x, t.into_normalized()?))
+ mkerr(AnnotMismatch(x, t.to_normalized()))
);
- Ok(RetType(x.get_type_move()?))
+ Ok(RetType(x.get_type()?.into_owned()))
}
BoolIf(x, y, z) => {
ensure_equal!(
@@ -836,7 +796,7 @@ fn type_last_layer(
mkerr(IfBranchMismatch(y, z))
);
- Ok(RetType(y.get_type_move()?))
+ Ok(RetType(y.get_type()?.into_owned()))
}
EmptyListLit(t) => {
let t = t.to_type();
@@ -855,12 +815,12 @@ fn type_last_layer(
y.get_type()?,
mkerr(InvalidListElement(
i,
- x.get_type_move()?.into_normalized()?,
+ x.get_type()?.to_normalized(),
y
))
);
}
- let t = x.get_type_move()?;
+ let t = x.get_type()?.into_owned();
Ok(RetType(
TypeIntermediate::ListType(ctx.clone(), t)
.typecheck()?
@@ -868,7 +828,7 @@ fn type_last_layer(
))
}
SomeLit(x) => {
- let t = x.get_type_move()?;
+ let t = x.get_type()?.into_owned();
Ok(RetType(
TypeIntermediate::OptionalType(ctx.clone(), t)
.typecheck()?
@@ -904,7 +864,7 @@ fn type_last_layer(
RecordLit(kvs) => {
let kts = kvs
.into_iter()
- .map(|(x, v)| Ok((x, v.get_type_move()?)))
+ .map(|(x, v)| Ok((x, v.get_type()?.into_owned())))
.collect::<Result<_, _>>()?;
Ok(RetType(
TypeIntermediate::RecordType(ctx.clone(), kts)
@@ -923,7 +883,7 @@ fn type_last_layer(
Ok((x, t))
})
.collect::<Result<_, _>>()?;
- let t = v.get_type_move()?;
+ let t = v.get_type()?.into_owned();
kts.insert(x, Some(t));
Ok(RetType(
TypeIntermediate::UnionType(ctx.clone(), kts)
@@ -934,12 +894,12 @@ fn type_last_layer(
Field(r, x) => {
let tr = r.get_type()?;
let tr_internal = tr.internal_whnf();
- match tr_internal.deref() {
+ match &tr_internal {
Some(Value::RecordType(kts)) => match kts.get(&x) {
Some(tth) => {
let tth = tth.clone();
drop(tr_internal);
- Ok(RetType(tth.normalize_to_type(ctx)?))
+ Ok(RetType(tth.to_type(ctx)?))
},
None => Err(mkerr(MissingRecordField(x, r.clone()))),
},
@@ -947,7 +907,7 @@ fn type_last_layer(
_ => {
let r = r.to_type();
let r_internal = r.internal_whnf();
- match r_internal.deref() {
+ match &r_internal {
Some(Value::UnionType(kts)) => match kts.get(&x) {
// Constructor has type T -> < x: T, ... >
// TODO: use "_" instead of x (i.e. compare types using equivalence in tests)
@@ -958,7 +918,7 @@ fn type_last_layer(
TypeIntermediate::Pi(
ctx.clone(),
x.clone(),
- t.normalize_to_type(ctx)?,
+ t.to_type(ctx)?,
r,
)
.typecheck()?
@@ -973,7 +933,7 @@ fn type_last_layer(
drop(r_internal);
Err(mkerr(MissingUnionField(
x,
- r.into_normalized()?,
+ r.to_normalized(),
)))
},
},
@@ -981,18 +941,18 @@ fn type_last_layer(
drop(r_internal);
Err(mkerr(NotARecord(
x,
- r.into_normalized()?
+ r.to_normalized()
)))
},
}
}
// _ => Err(mkerr(NotARecord(
// x,
- // r.to_type()?.into_normalized()?,
+ // r.to_type()?.to_normalized(),
// ))),
}
}
- Const(c) => Ok(RetType(type_of_const(c))),
+ Const(c) => Ok(RetTyped(const_to_typed(c))),
Builtin(b) => Ok(RetExpr(type_of_builtin(b))),
BoolLit(_) => Ok(RetType(builtin_to_type(Bool)?)),
NaturalLit(_) => Ok(RetType(builtin_to_type(Natural)?)),
@@ -1001,7 +961,7 @@ 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()?.internal_whnf().deref() {
+ match l.get_type()?.internal_whnf() {
Some(Value::AppliedBuiltin(List, _)) => {}
_ => return Err(mkerr(BinOpTypeMismatch(o, l.clone()))),
}
@@ -1045,8 +1005,8 @@ fn type_of(
) -> Result<Typed<'static>, TypeError> {
let ctx = TypecheckContext::new();
let e = type_with(&ctx, e)?;
- // Ensure the inferred type isn't SuperType
- e.get_type()?.as_normalized()?;
+ // Ensure `e` has a type (i.e. `e` is not `Sort`)
+ e.get_type()?;
Ok(e)
}
@@ -1072,6 +1032,7 @@ pub(crate) enum TypeMessage<'a> {
MissingUnionField(Label, Normalized<'a>),
BinOpTypeMismatch(BinOp, Typed<'a>),
NoDependentTypes(Normalized<'a>, Normalized<'a>),
+ Sort,
Unimplemented,
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 18:07:43 +0000