From 36bcec6c91d3192b5c84c96af96961ff6b79f0f0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 9 May 2019 23:35:08 +0200 Subject: Merge Type and Typed --- dhall/src/core/thunk.rs | 2 +- dhall/src/phase/mod.rs | 69 +++++++--------------------------- dhall/src/phase/typecheck.rs | 89 ++++++++++++++++++++------------------------ 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 { @@ -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 { + // 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 { - // TODO: avoid clone - match &self.to_value() { - Value::Const(c) => Some(*c), - _ => None, - } - } - pub fn get_type(&self) -> Result, 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, 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 { - Some(Type(self.0.shift(delta, var)?)) - } -} - impl Shift for Normalized { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { Some(Normalized(self.0.shift(delta, var)?)) @@ -263,12 +234,6 @@ impl Subst for Typed { } } -impl Subst 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 { 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) => { -- cgit v1.2.3