summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/expr.rs11
-rw-r--r--dhall/src/tests.rs9
-rw-r--r--dhall/src/traits/deserialize.rs2
-rw-r--r--dhall/src/traits/static_type.rs1
-rw-r--r--dhall/src/typecheck.rs135
5 files changed, 118 insertions, 40 deletions
diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index 94093a9..1c3ec53 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -139,6 +139,7 @@ impl<'a> Type<'a> {
// 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,
// })
@@ -150,6 +151,14 @@ impl<'a> Type<'a> {
impl<'a> SimpleType<'a> {
pub(crate) fn into_type(self) -> Type<'a> {
- Normalized(self.0, Some(Type::const_type()), PhantomData).into_type()
+ self.into_type_ctx(&crate::typecheck::TypecheckContext::new())
+ }
+ pub(crate) fn into_type_ctx(
+ self,
+ ctx: &crate::typecheck::TypecheckContext,
+ ) -> Type<'a> {
+ Normalized(self.0, Some(Type::const_type()), PhantomData)
+ .into_type_ctx(ctx)
+ .unwrap()
}
}
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index c945b23..4d8fabd 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -71,7 +71,7 @@ pub fn run_test_with_bigger_stack(
) -> std::result::Result<(), String> {
// Many tests stack overflow in debug mode
let base_path: String = base_path.to_string();
- stacker::grow(4 * 1024 * 1024, move || {
+ stacker::grow(6 * 1024 * 1024, move || {
run_test(&base_path, feature, status)
.map_err(|e| e.to_string())
.map(|_| ())
@@ -135,12 +135,15 @@ pub fn run_test(
assert_eq_display!(expr, expected);
}
Typecheck => {
- expr.typecheck_with(&expected.into_type())?;
+ expr.typecheck_with(&expected.into_type()?)?;
}
TypeInference => {
let expr = expr.typecheck()?;
let ty = expr.get_type()?;
- assert_eq_display!(ty.as_ref(), &expected.into_type());
+ assert_eq_display!(
+ ty.as_normalized()?.as_expr(),
+ expected.into_type()?.as_normalized()?.as_expr()
+ );
}
Normalization => {
let expr = expr.skip_typecheck().normalize();
diff --git a/dhall/src/traits/deserialize.rs b/dhall/src/traits/deserialize.rs
index 43eb2ac..9cc2147 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)?.into_type()?)
}
}
diff --git a/dhall/src/traits/static_type.rs b/dhall/src/traits/static_type.rs
index e92ce78..225eb32 100644
--- a/dhall/src/traits/static_type.rs
+++ b/dhall/src/traits/static_type.rs
@@ -44,6 +44,7 @@ impl<T: SimpleStaticType> StaticType for T {
std::marker::PhantomData,
)
.into_type()
+ .unwrap()
}
}
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 6fb7cac..38b3d68 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -32,8 +32,11 @@ impl<'a> Resolved<'a> {
}
}
impl<'a> Typed<'a> {
- fn normalize_to_type(self) -> Type<'a> {
- self.normalize().into_type()
+ fn normalize_to_type(
+ self,
+ ctx: &TypecheckContext,
+ ) -> Result<Type<'a>, TypeError> {
+ Ok(self.normalize().into_type_ctx(ctx)?)
}
fn get_type_move(self) -> Result<Type<'static>, TypeError> {
let (expr, ty) = (self.0, self.1);
@@ -54,11 +57,21 @@ impl<'a> Normalized<'a> {
self.2,
)
}
- pub(crate) fn into_type(self) -> Type<'a> {
- Type(match self.0.as_ref() {
+ pub(crate) fn into_type(self) -> Result<Type<'a>, TypeError> {
+ self.into_type_ctx(&TypecheckContext::new())
+ }
+ pub(crate) fn into_type_ctx(
+ self,
+ ctx: &TypecheckContext,
+ ) -> Result<Type<'a>, TypeError> {
+ Ok(Type(match self.0.as_ref() {
ExprF::Const(c) => TypeInternal::Const(*c),
+ ExprF::Pi(_, _, _) => {
+ return Ok(type_with(ctx, self.0.embed_absurd())?
+ .normalize_to_type(ctx)?)
+ }
_ => TypeInternal::Expr(Box::new(self)),
- })
+ }))
}
fn get_type_move(self) -> Result<Type<'static>, TypeError> {
let (expr, ty) = (self.0, self.1);
@@ -77,7 +90,9 @@ impl Normalized<'static> {
}
}
impl<'a> Type<'a> {
- fn as_normalized(&self) -> Result<Cow<Normalized<'a>>, TypeError> {
+ pub(crate) fn as_normalized(
+ &self,
+ ) -> Result<Cow<Normalized<'a>>, TypeError> {
Ok(Cow::Owned(self.0.clone().into_normalized()?))
// match &self.0 {
// TypeInternal::Expr(e) => Ok(Cow::Borrowed(e)),
@@ -106,6 +121,13 @@ impl<'a> Type<'a> {
use TypeInternal::*;
Type(match &self.0 {
Expr(e) => Expr(Box::new(e.shift0(delta, label))),
+ Pi(ctx, c, x, t, e) => Pi(
+ ctx.clone(),
+ *c,
+ x.clone(),
+ Box::new(t.shift0(delta, label)),
+ Box::new(e.shift0(delta, label)),
+ ),
Const(c) => Const(*c),
SuperType => SuperType,
})
@@ -134,6 +156,13 @@ impl Type<'static> {
#[derive(Debug, Clone, PartialEq, Eq)]
pub(crate) enum TypeInternal<'a> {
Const(Const),
+ Pi(
+ TypecheckContext,
+ Const,
+ Label,
+ Box<Type<'static>>,
+ Box<Type<'static>>,
+ ),
/// The type of `Sort`
SuperType,
/// This must not contain a value captured by one of the variants above.
@@ -144,6 +173,17 @@ impl<'a> TypeInternal<'a> {
pub(crate) fn into_normalized(self) -> Result<Normalized<'a>, TypeError> {
match self {
TypeInternal::Expr(e) => Ok(*e),
+ TypeInternal::Pi(ctx, c, x, t, e) => Ok(Typed(
+ rc(ExprF::Pi(
+ x,
+ t.into_normalized()?.embed(),
+ e.into_normalized()?.embed(),
+ )),
+ Some(const_to_type(c)),
+ ctx,
+ PhantomData,
+ )
+ .normalize()),
TypeInternal::Const(c) => Ok(const_to_normalized(c)),
TypeInternal::SuperType => Err(TypeError::new(
&TypecheckContext::new(),
@@ -156,13 +196,32 @@ impl<'a> TypeInternal<'a> {
#[derive(Debug, Clone)]
pub(crate) enum TypedImproved {
- // Pi(TypecheckContext, Const, Label, Type<'static>, Type<'static>),
+ Pi(TypecheckContext, Const, Label, Type<'static>, Type<'static>),
Expr(Typed<'static>),
}
impl TypedImproved {
fn into_typed(self) -> Result<Typed<'static>, TypeError> {
match self {
+ TypedImproved::Pi(ctx, c, x, t, e) => Ok(Typed(
+ rc(ExprF::Pi(
+ x,
+ t.into_normalized()?.embed(),
+ e.into_normalized()?.embed(),
+ )),
+ Some(const_to_type(c)),
+ ctx,
+ PhantomData,
+ )),
+ TypedImproved::Expr(e) => Ok(e),
+ }
+ }
+ fn normalize_to_type(
+ self,
+ ctx: &TypecheckContext,
+ ) -> Result<Type<'static>, TypeError> {
+ match self {
+ TypedImproved::Expr(e) => Ok(e.normalize_to_type(ctx)?),
// TypedImproved::Pi(ctx, c, x, t, e) => Ok(Typed(
// rc(ExprF::Pi(
// x,
@@ -172,12 +231,14 @@ impl TypedImproved {
// Some(const_to_type(c)),
// ctx,
// PhantomData,
- // )),
- TypedImproved::Expr(e) => Ok(e),
+ // )
+ // .normalize()
+ // .into_type()?),
+ TypedImproved::Pi(ctx, c, x, t, e) => {
+ Ok(Type(TypeInternal::Pi(ctx, c, x, Box::new(t), Box::new(e))))
+ }
}
- }
- fn normalize_to_type(self) -> Result<Type<'static>, TypeError> {
- Ok(self.into_typed()?.normalize_to_type())
+ // Ok(self.into_typed()?.normalize_to_type())
}
fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> {
Ok(Cow::Owned(self.clone().get_type_move()?))
@@ -332,12 +393,19 @@ where
}
match (&eL0.borrow().0, &eR0.borrow().0) {
(TypeInternal::SuperType, TypeInternal::SuperType) => true,
- (TypeInternal::Const(cl), TypeInternal::Const(cr)) => cl == cr,
- (TypeInternal::Expr(l), TypeInternal::Expr(r)) => {
+ (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, l.as_expr(), r.as_expr())
+ go(
+ &mut ctx,
+ eL0.borrow().as_normalized().unwrap().as_expr(),
+ eR0.borrow().as_normalized().unwrap().as_expr(),
+ )
}
- _ => false,
+ // _ => false,
}
}
@@ -465,15 +533,15 @@ 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)?.normalize_to_type(ctx)?)
}
-fn into_simple_type<'a>(e: SubExpr<X, X>) -> Type<'a> {
- SimpleType(e, PhantomData).into_type()
+fn into_simple_type<'a>(ctx: &TypecheckContext, e: SubExpr<X, X>) -> Type<'a> {
+ SimpleType(e, PhantomData).into_type_ctx(ctx)
}
fn simple_type_from_builtin<'a>(b: Builtin) -> Type<'a> {
- into_simple_type(rc(ExprF::Builtin(b)))
+ into_simple_type(&TypecheckContext::new(), rc(ExprF::Builtin(b)))
}
/// Intermediary return type
@@ -540,8 +608,8 @@ fn type_with(
}
};
- // return Ok(TypedImproved::Pi(ctx.clone(), k, x.clone(), ta, tb));
- Ok(RetExpr(Const(k)))
+ return Ok(TypedImproved::Pi(ctx.clone(), k, x.clone(), ta, tb));
+ // Ok(RetExpr(Const(k)))
}
Let(x, t, v, e) => {
let v = if let Some(t) = t {
@@ -560,9 +628,8 @@ fn type_with(
_ => type_last_layer(
ctx,
// Typecheck recursively all subexpressions
- e.as_ref().traverse_ref_simple(|e| {
- Ok(type_with(ctx, e.clone())?)
- })?,
+ e.as_ref()
+ .traverse_ref_simple(|e| Ok(type_with(ctx, e.clone())?))?,
e.clone(),
),
}?;
@@ -608,25 +675,23 @@ fn type_last_layer(
None => Err(mkerr(UnboundVariable(var.clone()))),
},
App(f, a) => {
- let tf = f.get_type()?;
- let tf_expr = tf.unroll_ref()?;
- let (x, tx, tb) = match tf_expr.as_ref() {
- Pi(x, tx, tb) => (x, tx, tb),
+ let tf = f.get_type()?.into_owned();
+ let (x, tx, tb) = match tf.0 {
+ TypeInternal::Pi(_, _, x, tx, tb) => (x, tx, tb),
_ => return Err(mkerr(NotAFunction(f))),
};
- let tx = mktype(ctx, tx.embed_absurd())?;
- ensure_equal!(a.get_type()?, &tx, {
+ ensure_equal!(a.get_type()?, tx.as_ref(), {
mkerr(TypeMismatch(f, tx.into_normalized()?, a))
});
Ok(RetExpr(Let(
x.clone(),
None,
a.normalize()?.embed(),
- tb.embed_absurd(),
+ tb.into_normalized()?.into_expr().embed_absurd(),
)))
}
Annot(x, t) => {
- let t = t.normalize_to_type()?;
+ let t = t.normalize_to_type(ctx)?;
ensure_equal!(
&t,
x.get_type()?,
@@ -660,7 +725,7 @@ fn type_last_layer(
Ok(RetType(y.get_type_move()?))
}
EmptyListLit(t) => {
- let t = t.normalize_to_type()?;
+ let t = t.normalize_to_type(ctx)?;
ensure_simple_type!(
t,
mkerr(InvalidListType(t.into_normalized()?)),
@@ -788,7 +853,7 @@ fn type_last_layer(
None => Err(mkerr(MissingRecordField(x, r))),
},
_ => {
- let r = r.normalize_to_type()?;
+ let r = r.normalize_to_type(ctx)?;
match r.as_normalized()?.as_expr().as_ref() {
UnionType(kts) => match kts.get(&x) {
// Constructor has type T -> < x: T, ... >
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-28 21:10:50 +0000