summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
authorNadrieril2019-04-22 23:31:42 +0200
committerNadrieril2019-04-22 23:31:42 +0200
commit60df4ed07a752d256888e6b4449a48bfa43cf79f (patch)
tree16fcd64f6d255f4391477bb9af57b745e8efb82e /dhall
parent53f886c0f5044e4bfe7de756b8c47d992f91b03e (diff)
Temporarily simplify functions depending on TypeInternal
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/expr.rs15
-rw-r--r--dhall/src/traits/dynamic_type.rs21
-rw-r--r--dhall/src/typecheck.rs40
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))