summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/core/thunk.rs2
-rw-r--r--dhall/src/phase/mod.rs69
-rw-r--r--dhall/src/phase/typecheck.rs89
3 files changed, 55 insertions, 105 deletions
diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs
index 0e4f2d5..c65d70e 100644
--- a/dhall/src/core/thunk.rs
+++ b/dhall/src/core/thunk.rs
@@ -198,7 +198,7 @@ impl TypeThunk {
}
pub fn from_type(t: Type) -> TypeThunk {
- TypeThunk(t.to_typed())
+ TypeThunk(t)
}
pub fn normalize_mut(&mut self) {
diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs
index 3d7afb6..63480c5 100644
--- a/dhall/src/phase/mod.rs
+++ b/dhall/src/phase/mod.rs
@@ -49,8 +49,7 @@ pub enum Typed {
#[derive(Debug, Clone)]
pub struct Normalized(Typed);
-#[derive(Debug, Clone, PartialEq, Eq)]
-pub struct Type(Typed);
+pub type Type = Typed;
impl Parsed {
pub fn parse_file(f: &Path) -> Result<Parsed, Error> {
@@ -119,7 +118,7 @@ impl Typed {
Typed::Const(c)
}
pub fn from_value_untyped(v: Value) -> Self {
- Typed::Untyped(Thunk::from_value(v))
+ Typed::from_thunk_untyped(Thunk::from_value(v))
}
pub fn from_normalized_expr_untyped(e: NormalizedSubExpr) -> Self {
Typed::from_thunk_untyped(Thunk::from_normalized_expr(e))
@@ -148,8 +147,19 @@ impl Typed {
pub fn to_type(&self) -> Type {
self.clone().into_type()
}
+ // Deprecated
pub fn into_type(self) -> Type {
- Type(self)
+ self
+ }
+ pub fn to_normalized(&self) -> Normalized {
+ self.clone().normalize()
+ }
+ pub fn as_const(&self) -> Option<Const> {
+ // TODO: avoid clone
+ match &self.to_value() {
+ Value::Const(c) => Some(*c),
+ _ => None,
+ }
}
pub fn normalize_mut(&mut self) {
@@ -171,36 +181,6 @@ impl Typed {
}
}
-impl Type {
- // Deprecated
- pub fn to_normalized(&self) -> Normalized {
- self.0.clone().normalize()
- }
- pub fn to_expr(&self) -> NormalizedSubExpr {
- self.0.to_expr()
- }
- pub fn to_value(&self) -> Value {
- self.0.to_value()
- }
- pub fn to_typed(&self) -> Typed {
- self.0.clone()
- }
- pub fn as_const(&self) -> Option<Const> {
- // TODO: avoid clone
- match &self.to_value() {
- Value::Const(c) => Some(*c),
- _ => None,
- }
- }
- pub fn get_type(&self) -> Result<Cow<'_, Type>, TypeError> {
- self.0.get_type()
- }
-
- pub fn from_const(c: Const) -> Self {
- Type(Typed::from_const(c))
- }
-}
-
impl Normalized {
#[allow(dead_code)]
pub fn to_expr(&self) -> NormalizedSubExpr {
@@ -220,9 +200,6 @@ impl Normalized {
pub fn into_typed(self) -> Typed {
self.0
}
- pub fn get_type(&self) -> Result<Cow<'_, Type>, TypeError> {
- self.0.get_type()
- }
}
impl Shift for Typed {
@@ -238,12 +215,6 @@ impl Shift for Typed {
}
}
-impl Shift for Type {
- fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
- Some(Type(self.0.shift(delta, var)?))
- }
-}
-
impl Shift for Normalized {
fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
Some(Normalized(self.0.shift(delta, var)?))
@@ -263,12 +234,6 @@ impl Subst<Typed> for Typed {
}
}
-impl Subst<Typed> for Type {
- fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
- Type(self.0.subst_shift(var, val))
- }
-}
-
macro_rules! derive_traits_for_wrapper_struct {
($ty:ident) => {
impl std::cmp::PartialEq for $ty {
@@ -306,9 +271,3 @@ impl Display for Typed {
self.to_expr().fmt(f)
}
}
-
-impl Display for Type {
- fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> {
- self.to_normalized().fmt(f)
- }
-}
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index c2d9da3..5caf1d5 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -47,7 +47,7 @@ fn tck_pi_type(
_ => {
return Err(TypeError::new(
ctx,
- InvalidInputType(tx.clone().to_normalized()),
+ InvalidInputType(tx.to_normalized()),
))
}
};
@@ -57,9 +57,7 @@ fn tck_pi_type(
_ => {
return Err(TypeError::new(
&ctx2,
- InvalidOutputType(
- te.clone().to_normalized().get_type()?.to_normalized(),
- ),
+ InvalidOutputType(te.get_type()?.to_normalized()),
))
}
};
@@ -70,8 +68,8 @@ fn tck_pi_type(
return Err(TypeError::new(
ctx,
NoDependentTypes(
- tx.clone().to_normalized(),
- te.clone().to_normalized().get_type()?.to_normalized(),
+ tx.to_normalized(),
+ te.get_type()?.to_normalized(),
),
))
}
@@ -171,7 +169,7 @@ fn tck_list_type(ctx: &TypecheckContext, t: Type) -> Result<Typed, TypeError> {
use crate::error::TypeMessage::*;
ensure_simple_type!(
t,
- TypeError::new(ctx, InvalidListType(t.clone().to_normalized())),
+ TypeError::new(ctx, InvalidListType(t.to_normalized())),
);
Ok(Typed::from_thunk_and_type(
Value::from_builtin(Builtin::List)
@@ -188,7 +186,7 @@ fn tck_optional_type(
use crate::error::TypeMessage::*;
ensure_simple_type!(
t,
- TypeError::new(ctx, InvalidOptionalType(t.clone().to_normalized())),
+ TypeError::new(ctx, InvalidOptionalType(t.to_normalized())),
);
Ok(Typed::from_thunk_and_type(
Value::from_builtin(Builtin::Optional)
@@ -451,11 +449,7 @@ fn type_last_layer(
_ => return Err(mkerr(NotAFunction(f.clone()))),
};
ensure_equal!(a.get_type()?, &tx, {
- mkerr(TypeMismatch(
- f.clone(),
- tx.clone().to_normalized(),
- a.clone(),
- ))
+ mkerr(TypeMismatch(f.clone(), tx.to_normalized(), a.clone()))
});
Ok(RetTypeOnly(tb.subst_shift(&x.into(), &a)))
@@ -671,47 +665,44 @@ 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();
- 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(),
- )))
- }
- };
+ 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))),
+ };
- 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,
+ tx.to_normalized(),
+ variant_type,
+ ))
+ });
- // 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(),
- 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) => {
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 16:03:14 +0000