From 1b8a67353a0167bdafd0b8cc03f5d83464f7af3d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 7 May 2019 12:49:35 +0200 Subject: Unify Type, TypeInternal and Typed --- dhall/src/phase/mod.rs | 131 ++++++++++++------------------------------- dhall/src/phase/typecheck.rs | 28 +++------ dhall/src/tests.rs | 1 - 3 files changed, 43 insertions(+), 117 deletions(-) (limited to 'dhall') diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs index 0faf6dd..c8a8ffd 100644 --- a/dhall/src/phase/mod.rs +++ b/dhall/src/phase/mod.rs @@ -10,7 +10,7 @@ use crate::core::value::{AlphaVar, Value}; use crate::error::{Error, ImportError, TypeError, TypeMessage}; use resolve::ImportRoot; -use typecheck::{const_to_typed, type_of_const}; +use typecheck::type_of_const; pub(crate) mod binary; pub(crate) mod normalize; @@ -32,10 +32,13 @@ pub(crate) struct Resolved(pub(crate) ResolvedSubExpr); /// A typed expression #[derive(Debug, Clone)] pub(crate) enum Typed { - // The `Sort` higher-kinded type; it doesn't have a type - Sort, - // Any other value, along with (optionally) its type + // Any value, along with (optionally) its type Value(Thunk, Option), + // 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 + // even though it doesn't itself have a type. + Const(Const), } /// A normalized expression. @@ -58,14 +61,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) TypeInternal); - -#[derive(Debug, Clone)] -pub(crate) enum TypeInternal { - Const(Const), - /// This must not contain a Const value. - Typed(Box), -} +pub struct Type(pub(crate) Box); impl Parsed { pub fn parse_file(f: &Path) -> Result { @@ -116,7 +112,7 @@ impl Typed { /// leave ill-typed sub-expressions unevaluated. pub fn normalize(self) -> Normalized { match &self { - Typed::Sort => {} + Typed::Const(_) => {} Typed::Value(thunk, _) => { thunk.normalize_nf(); } @@ -130,12 +126,15 @@ impl Typed { pub(crate) fn from_thunk_untyped(th: Thunk) -> Self { Typed::Value(th, None) } + pub(crate) fn from_const(c: Const) -> Self { + Typed::Const(c) + } // TODO: Avoid cloning if possible pub(crate) fn to_value(&self) -> Value { match self { Typed::Value(th, _) => th.to_value(), - Typed::Sort => Value::Const(Const::Sort), + Typed::Const(c) => Value::Const(*c), } } pub(crate) fn to_expr(&self) -> NormalizedSubExpr { @@ -147,17 +146,15 @@ impl Typed { pub(crate) fn to_thunk(&self) -> Thunk { match self { Typed::Value(th, _) => th.clone(), - Typed::Sort => Thunk::from_value(Value::Const(Const::Sort)), + Typed::Const(c) => Thunk::from_value(Value::Const(*c)), } } + // Deprecated pub(crate) fn to_type(&self) -> Type { - match self { - Typed::Sort => Type(TypeInternal::Const(Const::Sort)), - Typed::Value(th, _) => match &*th.as_value() { - Value::Const(c) => Type(TypeInternal::Const(*c)), - _ => Type(TypeInternal::Typed(Box::new(self.clone()))), - }, - } + self.clone().into_type() + } + pub(crate) fn into_type(self) -> Type { + Type(Box::new(self)) } pub(crate) fn get_type(&self) -> Result, TypeError> { @@ -167,23 +164,17 @@ impl Typed { &TypecheckContext::new(), TypeMessage::Untyped, )), - Typed::Sort => { - Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort)) - } + Typed::Const(c) => Ok(Cow::Owned(type_of_const(*c)?)), } } - pub(crate) fn const_sort() -> Self { - Typed::Sort - } - pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Self { match self { Typed::Value(th, t) => Typed::Value( th.shift(delta, var), t.as_ref().map(|x| x.shift(delta, var)), ), - Typed::Sort => Typed::Sort, + Typed::Const(c) => Typed::Const(*c), } } @@ -193,14 +184,14 @@ impl Typed { th.subst_shift(var, val), t.as_ref().map(|x| x.subst_shift(var, val)), ), - Typed::Sort => Typed::Sort, + Typed::Const(c) => Typed::Const(*c), } } } impl Type { pub(crate) fn to_normalized(&self) -> Normalized { - self.0.to_normalized() + self.0.clone().normalize() } pub(crate) fn to_expr(&self) -> NormalizedSubExpr { self.0.to_expr() @@ -209,80 +200,37 @@ impl Type { self.0.to_value() } pub(crate) fn as_const(&self) -> Option { - self.0.as_const() + // TODO: avoid clone + match &self.to_value() { + Value::Const(c) => Some(*c), + _ => None, + } } pub(crate) fn internal_whnf(&self) -> Option { - self.0.whnf() + Some(self.to_value()) } pub(crate) fn get_type(&self) -> Result, TypeError> { self.0.get_type() } pub(crate) fn const_sort() -> Self { - Type(TypeInternal::Const(Const::Sort)) + Type::from_const(Const::Sort) } pub(crate) fn const_kind() -> Self { - Type(TypeInternal::Const(Const::Kind)) + Type::from_const(Const::Kind) } pub(crate) fn const_type() -> Self { - Type(TypeInternal::Const(Const::Type)) - } - - pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Self { - Type(self.0.shift(delta, var)) + Type::from_const(Const::Type) } - pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { - Type(self.0.subst_shift(var, val)) + pub(crate) fn from_const(c: Const) -> Self { + Type(Box::new(Typed::from_const(c))) } -} -impl TypeInternal { - pub(crate) fn to_typed(&self) -> Typed { - match self { - TypeInternal::Typed(e) => e.as_ref().clone(), - TypeInternal::Const(c) => const_to_typed(*c), - } - } - pub(crate) fn to_normalized(&self) -> Normalized { - self.to_typed().normalize() - } - pub(crate) fn to_expr(&self) -> NormalizedSubExpr { - self.to_normalized().to_expr() - } - pub(crate) fn to_value(&self) -> Value { - self.to_typed().to_value() - } - pub(crate) fn get_type(&self) -> Result, TypeError> { - Ok(match self { - TypeInternal::Typed(e) => e.get_type()?, - TypeInternal::Const(c) => Cow::Owned(type_of_const(*c)?), - }) - } - pub(crate) fn as_const(&self) -> Option { - match self { - TypeInternal::Const(c) => Some(*c), - _ => None, - } - } - pub(crate) fn whnf(&self) -> Option { - match self { - TypeInternal::Typed(e) => Some(e.to_value()), - _ => None, - } - } pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Self { - use TypeInternal::*; - match self { - Typed(e) => Typed(Box::new(e.shift(delta, var))), - Const(c) => Const(*c), - } + Type(Box::new(self.0.shift(delta, var))) } pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { - use TypeInternal::*; - match self { - Typed(e) => Typed(Box::new(e.subst_shift(var, val))), - Const(c) => Const(*c), - } + Type(Box::new(self.0.subst_shift(var, val))) } } @@ -349,13 +297,6 @@ impl PartialEq for Typed { } } -impl Eq for TypeInternal {} -impl PartialEq for TypeInternal { - fn eq(&self, other: &Self) -> bool { - self.to_normalized() == other.to_normalized() - } -} - impl Display for Typed { fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> { self.to_expr().fmt(f) diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 42a4540..3e6986f 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -12,7 +12,7 @@ use crate::core::context::{NormalizationContext, TypecheckContext}; use crate::core::thunk::{Thunk, TypeThunk}; use crate::core::value::Value; use crate::error::{TypeError, TypeMessage}; -use crate::phase::{Normalized, Resolved, Type, TypeInternal, Typed}; +use crate::phase::{Normalized, Resolved, Type, Typed}; macro_rules! ensure_equal { ($x:expr, $y:expr, $err:expr $(,)*) => { @@ -97,7 +97,7 @@ impl TypeIntermediate { TypeThunk::from_type(tb.clone()), ) .into_thunk(), - const_to_type(k), + Type::from_const(k), ) } TypeIntermediate::RecordType(ctx, kts) => { @@ -127,7 +127,7 @@ impl TypeIntermediate { .collect(), ) .into_thunk(), - const_to_type(k), + Type::from_const(k), ) } TypeIntermediate::UnionType(ctx, kts) => { @@ -166,7 +166,7 @@ impl TypeIntermediate { .collect(), ) .into_thunk(), - const_to_type(k), + Type::from_const(k), ) } TypeIntermediate::ListType(ctx, t) => { @@ -178,7 +178,7 @@ impl TypeIntermediate { Value::from_builtin(Builtin::List) .app(t.to_value()) .into_thunk(), - const_to_type(Const::Type), + Type::from_const(Const::Type), ) } TypeIntermediate::OptionalType(ctx, t) => { @@ -190,7 +190,7 @@ impl TypeIntermediate { Value::from_builtin(Builtin::Optional) .app(t.to_value()) .into_thunk(), - const_to_type(Const::Type), + Type::from_const(Const::Type), ) } }) @@ -217,20 +217,6 @@ where eL0.borrow().to_value() == eR0.borrow().to_value() } -pub(crate) fn const_to_typed(c: Const) -> Typed { - match c { - Const::Sort => Typed::const_sort(), - _ => Typed::from_thunk_and_type( - Value::Const(c).into_thunk(), - type_of_const(c).unwrap(), - ), - } -} - -fn const_to_type(c: Const) -> Type { - Type(TypeInternal::Const(c)) -} - pub(crate) fn type_of_const(c: Const) -> Result { match c { Const::Type => Ok(Type::const_kind()), @@ -647,7 +633,7 @@ fn type_last_layer( // ))), } } - Const(c) => Ok(RetTyped(const_to_typed(c))), + Const(c) => Ok(RetTyped(Typed::from_const(c))), Builtin(b) => { Ok(RetType(mktype(ctx, rc(type_of_builtin(b)).note_absurd())?)) } diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index 18f6917..4fa1cf5 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -35,7 +35,6 @@ macro_rules! make_spec_test { use crate::error::{Error, Result}; use crate::phase::Parsed; -use crate::traits::DynamicType; use std::path::PathBuf; #[derive(Copy, Clone)] -- cgit v1.2.3