summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dhall/src/core/thunk.rs59
-rw-r--r--dhall/src/phase/mod.rs41
-rw-r--r--dhall/src/phase/typecheck.rs165
3 files changed, 108 insertions, 157 deletions
diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs
index eed8685..2d4c34d 100644
--- a/dhall/src/core/thunk.rs
+++ b/dhall/src/core/thunk.rs
@@ -4,14 +4,11 @@ use std::rc::Rc;
use dhall_syntax::{ExprF, X};
use crate::core::context::NormalizationContext;
-use crate::core::context::TypecheckContext;
use crate::core::value::Value;
use crate::core::var::{AlphaVar, Shift, Subst};
-use crate::error::TypeError;
use crate::phase::normalize::{
apply_any, normalize_one_layer, normalize_whnf, InputSubExpr, OutputSubExpr,
};
-use crate::phase::typecheck::mktype;
use crate::phase::{Type, Typed};
#[derive(Debug, Clone, Copy)]
@@ -45,10 +42,7 @@ pub struct Thunk(Rc<RefCell<ThunkInternal>>);
/// A thunk in type position. Can optionally store a Type from the typechecking phase to preserve
/// type information through the normalization phase.
#[derive(Debug, Clone)]
-pub(crate) enum TypeThunk {
- Thunk(Thunk),
- Type(Type),
-}
+pub(crate) struct TypeThunk(Typed);
impl ThunkInternal {
fn into_thunk(self) -> Thunk {
@@ -181,10 +175,6 @@ impl Thunk {
self.as_value().clone()
}
- pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr {
- self.normalize_to_expr_maybe_alpha(false)
- }
-
pub(crate) fn normalize_to_expr_maybe_alpha(
&self,
alpha: bool,
@@ -207,52 +197,31 @@ impl TypeThunk {
}
pub(crate) fn from_thunk(th: Thunk) -> TypeThunk {
- TypeThunk::Thunk(th)
+ TypeThunk(Typed::from_thunk_untyped(th))
}
pub(crate) fn from_type(t: Type) -> TypeThunk {
- TypeThunk::Type(t)
+ TypeThunk(t.to_typed())
}
pub(crate) fn normalize_mut(&mut self) {
- match self {
- TypeThunk::Thunk(th) => th.normalize_mut(),
- TypeThunk::Type(_) => {}
- }
+ self.0.normalize_mut()
}
pub(crate) fn normalize_nf(&self) -> Value {
- match self {
- TypeThunk::Thunk(th) => th.normalize_nf().clone(),
- TypeThunk::Type(t) => t.to_value().normalize(),
- }
+ self.0.to_value().normalize()
}
pub(crate) fn to_value(&self) -> Value {
- match self {
- TypeThunk::Thunk(th) => th.to_value(),
- TypeThunk::Type(t) => t.to_value(),
- }
+ self.0.to_value()
}
pub(crate) fn to_thunk(&self) -> Thunk {
- match self {
- TypeThunk::Thunk(th) => th.clone(),
- TypeThunk::Type(t) => t.to_thunk(),
- }
+ self.0.to_thunk()
}
- pub(crate) fn to_type(
- &self,
- ctx: &TypecheckContext,
- ) -> Result<Type, TypeError> {
- match self {
- TypeThunk::Type(t) => Ok(t.clone()),
- TypeThunk::Thunk(th) => {
- // TODO: rule out statically
- mktype(ctx, th.normalize_to_expr().absurd())
- }
- }
+ pub(crate) fn to_type(&self) -> Type {
+ self.0.to_type()
}
pub(crate) fn normalize_to_expr_maybe_alpha(
@@ -291,10 +260,7 @@ impl Shift for ThunkInternal {
impl Shift for TypeThunk {
fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
- Some(match self {
- TypeThunk::Thunk(th) => TypeThunk::Thunk(th.shift(delta, var)?),
- TypeThunk::Type(t) => TypeThunk::Type(t.shift(delta, var)?),
- })
+ Some(TypeThunk(self.0.shift(delta, var)?))
}
}
@@ -333,10 +299,7 @@ impl Subst<Typed> for ThunkInternal {
impl Subst<Typed> for TypeThunk {
fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
- match self {
- TypeThunk::Thunk(th) => TypeThunk::Thunk(th.subst_shift(var, val)),
- TypeThunk::Type(t) => TypeThunk::Type(t.subst_shift(var, val)),
- }
+ TypeThunk(self.0.subst_shift(var, val))
}
}
diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs
index 50103a0..351bbf0 100644
--- a/dhall/src/phase/mod.rs
+++ b/dhall/src/phase/mod.rs
@@ -34,7 +34,7 @@ pub(crate) struct Resolved(pub(crate) ResolvedSubExpr);
#[derive(Debug, Clone)]
pub(crate) enum Typed {
// Any value, along with (optionally) its type
- Value(Thunk, Option<Type>),
+ Value(Thunk, Option<Box<Type>>),
// One of the base higher-kinded typed.
// Used to avoid storing the same tower ot Type->Kind->Sort
// over and over again. Also enables having Sort as a type
@@ -62,7 +62,7 @@ pub struct SimpleType(pub(crate) NormalizedSubExpr);
/// This includes [SimpleType]s but also higher-kinded expressions like
/// `Type`, `Kind` and `{ x: Type }`.
#[derive(Debug, Clone, PartialEq, Eq)]
-pub struct Type(pub(crate) Box<Typed>);
+pub struct Type(pub(crate) Typed);
impl Parsed {
pub fn parse_file(f: &Path) -> Result<Parsed, Error> {
@@ -122,7 +122,7 @@ impl Typed {
}
pub(crate) fn from_thunk_and_type(th: Thunk, t: Type) -> Self {
- Typed::Value(th, Some(t))
+ Typed::Value(th, Some(Box::new(t)))
}
pub(crate) fn from_thunk_untyped(th: Thunk) -> Self {
Typed::Value(th, None)
@@ -155,7 +155,14 @@ impl Typed {
self.clone().into_type()
}
pub(crate) fn into_type(self) -> Type {
- Type(Box::new(self))
+ Type(self)
+ }
+
+ pub(crate) fn normalize_mut(&mut self) {
+ match self {
+ Typed::Value(th, _) => th.normalize_mut(),
+ Typed::Const(_) => {}
+ }
}
pub(crate) fn get_type(&self) -> Result<Cow<'_, Type>, TypeError> {
@@ -180,11 +187,8 @@ impl Type {
pub(crate) fn to_value(&self) -> Value {
self.0.to_value()
}
- pub(crate) fn to_thunk(&self) -> Thunk {
- self.0.to_thunk()
- }
pub(crate) fn to_typed(&self) -> Typed {
- self.0.as_ref().clone()
+ self.0.clone()
}
pub(crate) fn as_const(&self) -> Option<Const> {
// TODO: avoid clone
@@ -193,24 +197,15 @@ impl Type {
_ => None,
}
}
- pub(crate) fn internal_whnf(&self) -> Option<Value> {
- Some(self.to_value())
- }
pub(crate) fn get_type(&self) -> Result<Cow<'_, Type>, TypeError> {
self.0.get_type()
}
- pub(crate) fn const_sort() -> Self {
- Type::from_const(Const::Sort)
- }
- pub(crate) fn const_kind() -> Self {
- Type::from_const(Const::Kind)
- }
pub(crate) fn const_type() -> Self {
Type::from_const(Const::Type)
}
pub(crate) fn from_const(c: Const) -> Self {
- Type(Box::new(Typed::from_const(c)))
+ Type(Typed::from_const(c))
}
}
@@ -242,7 +237,9 @@ impl Shift for Typed {
Some(match self {
Typed::Value(th, t) => Typed::Value(
th.shift(delta, var)?,
- t.as_ref().map(|x| Ok(x.shift(delta, var)?)).transpose()?,
+ t.as_ref()
+ .map(|x| Ok(Box::new(x.shift(delta, var)?)))
+ .transpose()?,
),
Typed::Const(c) => Typed::Const(*c),
})
@@ -251,7 +248,7 @@ impl Shift for Typed {
impl Shift for Type {
fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
- Some(Type(Box::new(self.0.shift(delta, var)?)))
+ Some(Type(self.0.shift(delta, var)?))
}
}
@@ -266,7 +263,7 @@ impl Subst<Typed> for Typed {
match self {
Typed::Value(th, t) => Typed::Value(
th.subst_shift(var, val),
- t.as_ref().map(|x| x.subst_shift(var, val)),
+ t.as_ref().map(|x| Box::new(x.subst_shift(var, val))),
),
Typed::Const(c) => Typed::Const(*c),
}
@@ -275,7 +272,7 @@ impl Subst<Typed> for Typed {
impl Subst<Typed> for Type {
fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
- Type(Box::new(self.0.subst_shift(var, val)))
+ Type(self.0.subst_shift(var, val))
}
}
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 99876c0..e1dffb0 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -220,8 +220,8 @@ where
pub(crate) fn type_of_const(c: Const) -> Result<Type, TypeError> {
match c {
- Const::Type => Ok(Type::const_kind()),
- Const::Kind => Ok(Type::const_sort()),
+ Const::Type => Ok(Type::from_const(Const::Kind)),
+ Const::Kind => Ok(Type::from_const(Const::Sort)),
Const::Sort => {
return Err(TypeError::new(
&TypecheckContext::new(),
@@ -331,9 +331,9 @@ pub(crate) fn builtin_to_type(b: Builtin) -> Result<Type, TypeError> {
/// Intermediary return type
enum Ret {
/// Returns the contained value as is
- RetTyped(Typed),
+ RetWhole(Typed),
/// Use the contained Type as the type of the input expression
- RetType(Type),
+ RetTypeOnly(Type),
}
/// Type-check an expression and return the expression alongside its type if type-checking
@@ -411,14 +411,14 @@ fn type_with(
)?;
let ret = type_last_layer(ctx, &expr)?;
match ret {
- RetType(typ) => {
+ RetTypeOnly(typ) => {
let expr = expr.map_ref_simple(|typed| typed.to_thunk());
Typed::from_thunk_and_type(
Thunk::from_partial_expr(expr),
typ,
)
}
- RetTyped(tt) => tt,
+ RetWhole(tt) => tt,
}
}
})
@@ -446,19 +446,11 @@ fn type_last_layer(
| Var(_) => unreachable!(),
App(f, a) => {
let tf = f.get_type()?;
- let tf_internal = tf.internal_whnf();
- let (x, tx, tb) = match &tf_internal {
- Some(Value::Pi(
- x,
- TypeThunk::Type(tx),
- TypeThunk::Type(tb),
- )) => (x, tx, tb),
- Some(Value::Pi(_, _, _)) => {
- panic!("ICE: this should not have happened")
- }
+ let (x, tx, tb) = match &tf.to_value() {
+ Value::Pi(x, tx, tb) => (x.clone(), tx.to_type(), tb.to_type()),
_ => return Err(mkerr(NotAFunction(f.clone()))),
};
- ensure_equal!(a.get_type()?, tx, {
+ ensure_equal!(a.get_type()?, &tx, {
mkerr(TypeMismatch(
f.clone(),
tx.clone().to_normalized(),
@@ -466,7 +458,7 @@ fn type_last_layer(
))
});
- Ok(RetType(tb.subst_shift(&x.into(), &a)))
+ Ok(RetTypeOnly(tb.subst_shift(&x.into(), &a)))
}
Annot(x, t) => {
let t = t.to_type();
@@ -475,7 +467,7 @@ fn type_last_layer(
x.get_type()?,
mkerr(AnnotMismatch(x.clone(), t.to_normalized()))
);
- Ok(RetType(x.get_type()?.into_owned()))
+ Ok(RetTypeOnly(x.get_type()?.into_owned()))
}
BoolIf(x, y, z) => {
ensure_equal!(
@@ -500,11 +492,11 @@ fn type_last_layer(
mkerr(IfBranchMismatch(y.clone(), z.clone()))
);
- Ok(RetType(y.get_type()?.into_owned()))
+ Ok(RetTypeOnly(y.get_type()?.into_owned()))
}
EmptyListLit(t) => {
let t = t.to_type();
- Ok(RetType(tck_list_type(ctx, t)?.to_type()))
+ Ok(RetTypeOnly(tck_list_type(ctx, t)?.to_type()))
}
NEListLit(xs) => {
let mut iter = xs.iter().enumerate();
@@ -521,22 +513,22 @@ fn type_last_layer(
);
}
let t = x.get_type()?.into_owned();
- Ok(RetType(tck_list_type(ctx, t)?.to_type()))
+ Ok(RetTypeOnly(tck_list_type(ctx, t)?.to_type()))
}
SomeLit(x) => {
let t = x.get_type()?.into_owned();
- Ok(RetType(tck_optional_type(ctx, t)?.to_type()))
+ Ok(RetTypeOnly(tck_optional_type(ctx, t)?.to_type()))
}
- RecordType(kts) => Ok(RetTyped(tck_record_type(
+ RecordType(kts) => Ok(RetWhole(tck_record_type(
ctx,
kts.iter().map(|(x, t)| Ok((x.clone(), t.to_type()))),
)?)),
- UnionType(kts) => Ok(RetTyped(tck_union_type(
+ UnionType(kts) => Ok(RetWhole(tck_union_type(
ctx,
kts.iter()
.map(|(x, t)| Ok((x.clone(), t.as_ref().map(|t| t.to_type())))),
)?)),
- RecordLit(kvs) => Ok(RetType(
+ RecordLit(kvs) => Ok(RetTypeOnly(
tck_record_type(
ctx,
kvs.iter()
@@ -551,13 +543,13 @@ fn type_last_layer(
.map(|(x, v)| Ok((x.clone(), v.as_ref().map(|v| v.to_type()))));
let t = v.get_type()?.into_owned();
let kts = kts.chain(once(Ok((x.clone(), Some(t)))));
- Ok(RetType(tck_union_type(ctx, kts)?.to_type()))
+ Ok(RetTypeOnly(tck_union_type(ctx, kts)?.to_type()))
}
Field(r, x) => {
- match &r.get_type()?.internal_whnf() {
- Some(Value::RecordType(kts)) => match kts.get(&x) {
+ match &r.get_type()?.to_value() {
+ Value::RecordType(kts) => match kts.get(&x) {
Some(tth) => {
- Ok(RetType(tth.to_type(ctx)?))
+ Ok(RetTypeOnly(tth.to_type()))
},
None => Err(mkerr(MissingRecordField(x.clone(),
r.clone()))),
@@ -565,22 +557,22 @@ fn type_last_layer(
// TODO: branch here only when r.get_type() is a Const
_ => {
let r = r.to_type();
- match &r.internal_whnf() {
- Some(Value::UnionType(kts)) => match kts.get(&x) {
+ match &r.to_value() {
+ Value::UnionType(kts) => match kts.get(&x) {
// Constructor has type T -> < x: T, ... >
Some(Some(t)) => {
// TODO: avoid capture
- Ok(RetType(
+ Ok(RetTypeOnly(
tck_pi_type(
ctx,
"_".into(),
- t.to_type(ctx)?,
+ t.to_type(),
r.clone(),
)?.to_type()
))
},
Some(None) => {
- Ok(RetType(r.clone()))
+ Ok(RetTypeOnly(r.clone()))
},
None => {
Err(mkerr(MissingUnionField(
@@ -603,14 +595,14 @@ fn type_last_layer(
// ))),
}
}
- Const(c) => Ok(RetTyped(Typed::from_const(*c))),
+ Const(c) => Ok(RetWhole(Typed::from_const(*c))),
Builtin(b) => {
- Ok(RetType(mktype(ctx, rc(type_of_builtin(*b)).absurd())?))
+ Ok(RetTypeOnly(mktype(ctx, rc(type_of_builtin(*b)).absurd())?))
}
- BoolLit(_) => Ok(RetType(builtin_to_type(Bool)?)),
- NaturalLit(_) => Ok(RetType(builtin_to_type(Natural)?)),
- IntegerLit(_) => Ok(RetType(builtin_to_type(Integer)?)),
- DoubleLit(_) => Ok(RetType(builtin_to_type(Double)?)),
+ BoolLit(_) => Ok(RetTypeOnly(builtin_to_type(Bool)?)),
+ NaturalLit(_) => Ok(RetTypeOnly(builtin_to_type(Natural)?)),
+ IntegerLit(_) => Ok(RetTypeOnly(builtin_to_type(Integer)?)),
+ DoubleLit(_) => Ok(RetTypeOnly(builtin_to_type(Double)?)),
TextLit(interpolated) => {
let text_type = builtin_to_type(Text)?;
for contents in interpolated.iter() {
@@ -623,11 +615,11 @@ fn type_last_layer(
);
}
}
- Ok(RetType(text_type))
+ Ok(RetTypeOnly(text_type))
}
BinOp(o @ ListAppend, l, r) => {
- match l.get_type()?.internal_whnf() {
- Some(Value::AppliedBuiltin(List, _)) => {}
+ match l.get_type()?.to_value() {
+ Value::AppliedBuiltin(List, _) => {}
_ => return Err(mkerr(BinOpTypeMismatch(*o, l.clone()))),
}
@@ -637,7 +629,7 @@ fn type_last_layer(
mkerr(BinOpTypeMismatch(*o, r.clone()))
);
- Ok(RetType(l.get_type()?.into_owned()))
+ Ok(RetTypeOnly(l.get_type()?.into_owned()))
}
BinOp(o, l, r) => {
let t = builtin_to_type(match o {
@@ -664,7 +656,7 @@ fn type_last_layer(
mkerr(BinOpTypeMismatch(*o, r.clone()))
);
- Ok(RetType(t))
+ Ok(RetTypeOnly(t))
}
Merge(record, union, type_annot) => {
let handlers = match record.get_type()?.to_value() {
@@ -679,48 +671,47 @@ fn type_last_layer(
let mut inferred_type = None;
for (x, handler) in handlers.iter() {
- let handler_return_type = match variants.get(x) {
- // Union alternative with type
- Some(Some(variant_type)) => {
- let variant_type = variant_type.to_type(ctx)?;
- let handler_type = handler.to_type(ctx)?;
- let (x, tx, tb) = match &handler_type.to_value() {
- Value::Pi(x, tx, tb) => {
- (x.clone(), tx.to_type(ctx)?, tb.to_type(ctx)?)
- }
- _ => {
- return Err(mkerr(NotAFunction(
- handler_type.to_typed(),
- )))
- }
- };
+ let handler_return_type =
+ match variants.get(x) {
+ // Union alternative with type
+ Some(Some(variant_type)) => {
+ let variant_type = variant_type.to_type();
+ let handler_type = handler.to_type();
+ let (x, tx, tb) = match &handler_type.to_value() {
+ Value::Pi(x, tx, tb) => {
+ (x.clone(), tx.to_type(), tb.to_type())
+ }
+ _ => {
+ return Err(mkerr(NotAFunction(
+ handler_type.to_typed(),
+ )))
+ }
+ };
- ensure_equal!(&variant_type, &tx, {
- mkerr(TypeMismatch(
- handler_type.to_typed(),
- tx.clone().to_normalized(),
- variant_type.to_typed(),
- ))
- });
+ ensure_equal!(&variant_type, &tx, {
+ mkerr(TypeMismatch(
+ handler_type.to_typed(),
+ tx.clone().to_normalized(),
+ variant_type.to_typed(),
+ ))
+ });
- // Extract `tb` from under the `x` binder. Fails is `x` was free in `tb`.
- match tb.over_binder(x) {
- Some(x) => x,
- None => {
- return Err(mkerr(
+ // Extract `tb` from under the `x` binder. Fails is `x` was free in `tb`.
+ match tb.over_binder(x) {
+ Some(x) => x,
+ None => return Err(mkerr(
MergeHandlerReturnTypeMustNotBeDependent,
- ))
+ )),
}
}
- }
- // Union alternative without type
- Some(None) => handler.to_type(ctx)?,
- None => {
- return Err(mkerr(MergeHandlerMissingVariant(
- x.clone(),
- )))
- }
- };
+ // Union alternative without type
+ Some(None) => handler.to_type(),
+ None => {
+ return Err(mkerr(MergeHandlerMissingVariant(
+ x.clone(),
+ )))
+ }
+ };
match &inferred_type {
None => inferred_type = Some(handler_return_type),
Some(t) => {
@@ -742,10 +733,10 @@ fn type_last_layer(
(Some(ref t1), Some(t2)) => {
let t2 = t2.to_type();
ensure_equal!(t1, &t2, mkerr(MergeAnnotMismatch));
- Ok(RetType(t2))
+ Ok(RetTypeOnly(t2))
}
- (Some(t), None) => Ok(RetType(t)),
- (None, Some(t)) => Ok(RetType(t.to_type())),
+ (Some(t), None) => Ok(RetTypeOnly(t)),
+ (None, Some(t)) => Ok(RetTypeOnly(t.to_type())),
(None, None) => return Err(mkerr(MergeEmptyNeedsAnnotation)),
}
}
@@ -764,7 +755,7 @@ fn type_last_layer(
};
}
- Ok(RetType(
+ Ok(RetTypeOnly(
Typed::from_thunk_and_type(
Value::RecordType(new_kts).into_thunk(),
trecord.get_type()?.into_owned(),
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 01:24:42 +0000