diff options
author | Nadrieril | 2019-04-22 23:31:42 +0200 |
---|---|---|
committer | Nadrieril | 2019-04-22 23:31:42 +0200 |
commit | 60df4ed07a752d256888e6b4449a48bfa43cf79f (patch) | |
tree | 16fcd64f6d255f4391477bb9af57b745e8efb82e /dhall/src | |
parent | 53f886c0f5044e4bfe7de756b8c47d992f91b03e (diff) |
Temporarily simplify functions depending on TypeInternal
Diffstat (limited to 'dhall/src')
-rw-r--r-- | dhall/src/expr.rs | 15 | ||||
-rw-r--r-- | dhall/src/traits/dynamic_type.rs | 21 | ||||
-rw-r--r-- | dhall/src/typecheck.rs | 40 |
3 files changed, 35 insertions, 41 deletions
diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs index 1840eba..94093a9 100644 --- a/dhall/src/expr.rs +++ b/dhall/src/expr.rs @@ -136,12 +136,15 @@ impl<'a> Normalized<'a> { #[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())), - Const(c) => Const(c), - SuperType => SuperType, - }) + // use TypeInternal::*; + // Type(match self.0 { + // Expr(e) => Expr(Box::new(e.unnote())), + // Const(c) => Const(c), + // SuperType => SuperType, + // }) + + // Yes, this is positively horrible. Please forgive me. + unsafe { std::mem::transmute::<Type<'a>, Type<'b>>(self) } } } diff --git a/dhall/src/traits/dynamic_type.rs b/dhall/src/traits/dynamic_type.rs index 479bed6..3b34363 100644 --- a/dhall/src/traits/dynamic_type.rs +++ b/dhall/src/traits/dynamic_type.rs @@ -18,15 +18,18 @@ impl<T: StaticType> DynamicType for T { impl<'a> DynamicType for Type<'a> { fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> { - match &self.0 { - TypeInternal::Expr(e) => e.get_type(), - TypeInternal::Const(c) => Ok(Cow::Owned(type_of_const(*c))), - TypeInternal::SuperType => Err(TypeError::new( - &TypecheckContext::new(), - dhall_core::rc(ExprF::Const(Const::Sort)), - TypeMessage::Untyped, - )), - } + Ok(Cow::Owned( + self.clone().into_normalized()?.get_type()?.into_owned(), + )) + // match &self.0 { + // TypeInternal::Expr(e) => e.get_type(), + // TypeInternal::Const(c) => Ok(Cow::Owned(type_of_const(*c))), + // TypeInternal::SuperType => Err(TypeError::new( + // &TypecheckContext::new(), + // dhall_core::rc(ExprF::Const(Const::Sort)), + // TypeMessage::Untyped, + // )), + // } } } diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 19d7eee..37c95c5 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -78,15 +78,16 @@ impl Normalized<'static> { } impl<'a> Type<'a> { fn as_normalized(&self) -> Result<Cow<Normalized<'a>>, TypeError> { - match &self.0 { - TypeInternal::Expr(e) => Ok(Cow::Borrowed(e)), - TypeInternal::Const(c) => Ok(Cow::Owned(const_to_normalized(*c))), - TypeInternal::SuperType => Err(TypeError::new( - &TypecheckContext::new(), - rc(ExprF::Const(Const::Sort)), - TypeMessage::Untyped, - )), - } + Ok(Cow::Owned(self.0.clone().into_normalized()?)) + // match &self.0 { + // TypeInternal::Expr(e) => Ok(Cow::Borrowed(e)), + // TypeInternal::Const(c) => Ok(Cow::Owned(const_to_normalized(*c))), + // TypeInternal::SuperType => Err(TypeError::new( + // &TypecheckContext::new(), + // rc(ExprF::Const(Const::Sort)), + // TypeMessage::Untyped, + // )), + // } } pub(crate) fn into_normalized(self) -> Result<Normalized<'a>, TypeError> { self.0.into_normalized() @@ -427,20 +428,6 @@ macro_rules! ensure_equal { }; } -// Do not use with Const because they will never match -macro_rules! ensure_matches { - ($x:expr, $pat:pat => $branch:expr, $err:expr $(,)*) => { - match $x.unroll_ref()? { - Cow::Borrowed(e) => match e { - $pat => $branch, - _ => return Err($err), - }, - // Can't pattern match because lifetimes - Cow::Owned(_) => return Err($err), - } - }; -} - // Ensure the provided type has type `Type` macro_rules! ensure_simple_type { ($x:expr, $err:expr $(,)*) => {{ @@ -610,10 +597,11 @@ fn type_last_layer( }, App(f, a) => { let tf = f.get_type()?; - let (x, tx, tb) = ensure_matches!(tf, + let tf_expr = tf.unroll_ref()?; + let (x, tx, tb) = match tf_expr.as_ref() { Pi(x, tx, tb) => (x, tx, tb), - mkerr(NotAFunction(f)) - ); + _ => return Err(mkerr(NotAFunction(f))), + }; let tx = mktype(ctx, tx.embed_absurd())?; ensure_equal!(a.get_type()?, &tx, { mkerr(TypeMismatch(f, tx.into_normalized()?, a)) |