From 12c662d1dfaf20443d5e897212f2ac1490dee7cf Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 9 May 2019 18:51:37 +0200 Subject: Reduce the distance between Type and Typed --- dhall/src/core/thunk.rs | 59 +++------------- dhall/src/phase/mod.rs | 41 +++++------ dhall/src/phase/typecheck.rs | 165 ++++++++++++++++++++----------------------- 3 files changed, 108 insertions(+), 157 deletions(-) diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs index eed8685..2d4c34d 100644 --- a/dhall/src/core/thunk.rs +++ b/dhall/src/core/thunk.rs @@ -4,14 +4,11 @@ use std::rc::Rc; use dhall_syntax::{ExprF, X}; use crate::core::context::NormalizationContext; -use crate::core::context::TypecheckContext; use crate::core::value::Value; use crate::core::var::{AlphaVar, Shift, Subst}; -use crate::error::TypeError; use crate::phase::normalize::{ apply_any, normalize_one_layer, normalize_whnf, InputSubExpr, OutputSubExpr, }; -use crate::phase::typecheck::mktype; use crate::phase::{Type, Typed}; #[derive(Debug, Clone, Copy)] @@ -45,10 +42,7 @@ pub struct Thunk(Rc>); /// A thunk in type position. Can optionally store a Type from the typechecking phase to preserve /// type information through the normalization phase. #[derive(Debug, Clone)] -pub(crate) enum TypeThunk { - Thunk(Thunk), - Type(Type), -} +pub(crate) struct TypeThunk(Typed); impl ThunkInternal { fn into_thunk(self) -> Thunk { @@ -181,10 +175,6 @@ impl Thunk { self.as_value().clone() } - pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr { - self.normalize_to_expr_maybe_alpha(false) - } - pub(crate) fn normalize_to_expr_maybe_alpha( &self, alpha: bool, @@ -207,52 +197,31 @@ impl TypeThunk { } pub(crate) fn from_thunk(th: Thunk) -> TypeThunk { - TypeThunk::Thunk(th) + TypeThunk(Typed::from_thunk_untyped(th)) } pub(crate) fn from_type(t: Type) -> TypeThunk { - TypeThunk::Type(t) + TypeThunk(t.to_typed()) } pub(crate) fn normalize_mut(&mut self) { - match self { - TypeThunk::Thunk(th) => th.normalize_mut(), - TypeThunk::Type(_) => {} - } + self.0.normalize_mut() } pub(crate) fn normalize_nf(&self) -> Value { - match self { - TypeThunk::Thunk(th) => th.normalize_nf().clone(), - TypeThunk::Type(t) => t.to_value().normalize(), - } + self.0.to_value().normalize() } pub(crate) fn to_value(&self) -> Value { - match self { - TypeThunk::Thunk(th) => th.to_value(), - TypeThunk::Type(t) => t.to_value(), - } + self.0.to_value() } pub(crate) fn to_thunk(&self) -> Thunk { - match self { - TypeThunk::Thunk(th) => th.clone(), - TypeThunk::Type(t) => t.to_thunk(), - } + self.0.to_thunk() } - pub(crate) fn to_type( - &self, - ctx: &TypecheckContext, - ) -> Result { - match self { - TypeThunk::Type(t) => Ok(t.clone()), - TypeThunk::Thunk(th) => { - // TODO: rule out statically - mktype(ctx, th.normalize_to_expr().absurd()) - } - } + pub(crate) fn to_type(&self) -> Type { + self.0.to_type() } pub(crate) fn normalize_to_expr_maybe_alpha( @@ -291,10 +260,7 @@ impl Shift for ThunkInternal { impl Shift for TypeThunk { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(match self { - TypeThunk::Thunk(th) => TypeThunk::Thunk(th.shift(delta, var)?), - TypeThunk::Type(t) => TypeThunk::Type(t.shift(delta, var)?), - }) + Some(TypeThunk(self.0.shift(delta, var)?)) } } @@ -333,10 +299,7 @@ impl Subst for ThunkInternal { impl Subst for TypeThunk { fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { - match self { - TypeThunk::Thunk(th) => TypeThunk::Thunk(th.subst_shift(var, val)), - TypeThunk::Type(t) => TypeThunk::Type(t.subst_shift(var, val)), - } + TypeThunk(self.0.subst_shift(var, val)) } } diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs index 50103a0..351bbf0 100644 --- a/dhall/src/phase/mod.rs +++ b/dhall/src/phase/mod.rs @@ -34,7 +34,7 @@ pub(crate) struct Resolved(pub(crate) ResolvedSubExpr); #[derive(Debug, Clone)] pub(crate) enum Typed { // Any value, along with (optionally) its type - Value(Thunk, Option), + 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 @@ -62,7 +62,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) Box); +pub struct Type(pub(crate) Typed); impl Parsed { pub fn parse_file(f: &Path) -> Result { @@ -122,7 +122,7 @@ impl Typed { } pub(crate) fn from_thunk_and_type(th: Thunk, t: Type) -> Self { - Typed::Value(th, Some(t)) + Typed::Value(th, Some(Box::new(t))) } pub(crate) fn from_thunk_untyped(th: Thunk) -> Self { Typed::Value(th, None) @@ -155,7 +155,14 @@ impl Typed { self.clone().into_type() } pub(crate) fn into_type(self) -> Type { - Type(Box::new(self)) + Type(self) + } + + pub(crate) fn normalize_mut(&mut self) { + match self { + Typed::Value(th, _) => th.normalize_mut(), + Typed::Const(_) => {} + } } pub(crate) fn get_type(&self) -> Result, TypeError> { @@ -180,11 +187,8 @@ impl Type { pub(crate) fn to_value(&self) -> Value { self.0.to_value() } - pub(crate) fn to_thunk(&self) -> Thunk { - self.0.to_thunk() - } pub(crate) fn to_typed(&self) -> Typed { - self.0.as_ref().clone() + self.0.clone() } pub(crate) fn as_const(&self) -> Option { // TODO: avoid clone @@ -193,24 +197,15 @@ impl Type { _ => None, } } - pub(crate) fn internal_whnf(&self) -> Option { - Some(self.to_value()) - } pub(crate) fn get_type(&self) -> Result, TypeError> { self.0.get_type() } - pub(crate) fn const_sort() -> Self { - Type::from_const(Const::Sort) - } - pub(crate) fn const_kind() -> Self { - Type::from_const(Const::Kind) - } pub(crate) fn const_type() -> Self { Type::from_const(Const::Type) } pub(crate) fn from_const(c: Const) -> Self { - Type(Box::new(Typed::from_const(c))) + Type(Typed::from_const(c)) } } @@ -242,7 +237,9 @@ impl Shift for Typed { Some(match self { Typed::Value(th, t) => Typed::Value( th.shift(delta, var)?, - t.as_ref().map(|x| Ok(x.shift(delta, var)?)).transpose()?, + t.as_ref() + .map(|x| Ok(Box::new(x.shift(delta, var)?))) + .transpose()?, ), Typed::Const(c) => Typed::Const(*c), }) @@ -251,7 +248,7 @@ impl Shift for Typed { impl Shift for Type { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(Type(Box::new(self.0.shift(delta, var)?))) + Some(Type(self.0.shift(delta, var)?)) } } @@ -266,7 +263,7 @@ impl Subst for Typed { match self { Typed::Value(th, t) => Typed::Value( th.subst_shift(var, val), - t.as_ref().map(|x| x.subst_shift(var, val)), + t.as_ref().map(|x| Box::new(x.subst_shift(var, val))), ), Typed::Const(c) => Typed::Const(*c), } @@ -275,7 +272,7 @@ impl Subst for Typed { impl Subst for Type { fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { - Type(Box::new(self.0.subst_shift(var, val))) + Type(self.0.subst_shift(var, val)) } } diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 99876c0..e1dffb0 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -220,8 +220,8 @@ where pub(crate) fn type_of_const(c: Const) -> Result { match c { - Const::Type => Ok(Type::const_kind()), - Const::Kind => Ok(Type::const_sort()), + Const::Type => Ok(Type::from_const(Const::Kind)), + Const::Kind => Ok(Type::from_const(Const::Sort)), Const::Sort => { return Err(TypeError::new( &TypecheckContext::new(), @@ -331,9 +331,9 @@ pub(crate) fn builtin_to_type(b: Builtin) -> Result { /// Intermediary return type enum Ret { /// Returns the contained value as is - RetTyped(Typed), + RetWhole(Typed), /// Use the contained Type as the type of the input expression - RetType(Type), + RetTypeOnly(Type), } /// Type-check an expression and return the expression alongside its type if type-checking @@ -411,14 +411,14 @@ fn type_with( )?; let ret = type_last_layer(ctx, &expr)?; match ret { - RetType(typ) => { + RetTypeOnly(typ) => { let expr = expr.map_ref_simple(|typed| typed.to_thunk()); Typed::from_thunk_and_type( Thunk::from_partial_expr(expr), typ, ) } - RetTyped(tt) => tt, + RetWhole(tt) => tt, } } }) @@ -446,19 +446,11 @@ fn type_last_layer( | Var(_) => unreachable!(), App(f, a) => { let tf = f.get_type()?; - let tf_internal = tf.internal_whnf(); - let (x, tx, tb) = match &tf_internal { - Some(Value::Pi( - x, - TypeThunk::Type(tx), - TypeThunk::Type(tb), - )) => (x, tx, tb), - Some(Value::Pi(_, _, _)) => { - panic!("ICE: this should not have happened") - } + let (x, tx, tb) = match &tf.to_value() { + Value::Pi(x, tx, tb) => (x.clone(), tx.to_type(), tb.to_type()), _ => return Err(mkerr(NotAFunction(f.clone()))), }; - ensure_equal!(a.get_type()?, tx, { + ensure_equal!(a.get_type()?, &tx, { mkerr(TypeMismatch( f.clone(), tx.clone().to_normalized(), @@ -466,7 +458,7 @@ fn type_last_layer( )) }); - Ok(RetType(tb.subst_shift(&x.into(), &a))) + Ok(RetTypeOnly(tb.subst_shift(&x.into(), &a))) } Annot(x, t) => { let t = t.to_type(); @@ -475,7 +467,7 @@ fn type_last_layer( x.get_type()?, mkerr(AnnotMismatch(x.clone(), t.to_normalized())) ); - Ok(RetType(x.get_type()?.into_owned())) + Ok(RetTypeOnly(x.get_type()?.into_owned())) } BoolIf(x, y, z) => { ensure_equal!( @@ -500,11 +492,11 @@ fn type_last_layer( mkerr(IfBranchMismatch(y.clone(), z.clone())) ); - Ok(RetType(y.get_type()?.into_owned())) + Ok(RetTypeOnly(y.get_type()?.into_owned())) } EmptyListLit(t) => { let t = t.to_type(); - Ok(RetType(tck_list_type(ctx, t)?.to_type())) + Ok(RetTypeOnly(tck_list_type(ctx, t)?.to_type())) } NEListLit(xs) => { let mut iter = xs.iter().enumerate(); @@ -521,22 +513,22 @@ fn type_last_layer( ); } let t = x.get_type()?.into_owned(); - Ok(RetType(tck_list_type(ctx, t)?.to_type())) + Ok(RetTypeOnly(tck_list_type(ctx, t)?.to_type())) } SomeLit(x) => { let t = x.get_type()?.into_owned(); - Ok(RetType(tck_optional_type(ctx, t)?.to_type())) + Ok(RetTypeOnly(tck_optional_type(ctx, t)?.to_type())) } - RecordType(kts) => Ok(RetTyped(tck_record_type( + RecordType(kts) => Ok(RetWhole(tck_record_type( ctx, kts.iter().map(|(x, t)| Ok((x.clone(), t.to_type()))), )?)), - UnionType(kts) => Ok(RetTyped(tck_union_type( + UnionType(kts) => Ok(RetWhole(tck_union_type( ctx, kts.iter() .map(|(x, t)| Ok((x.clone(), t.as_ref().map(|t| t.to_type())))), )?)), - RecordLit(kvs) => Ok(RetType( + RecordLit(kvs) => Ok(RetTypeOnly( tck_record_type( ctx, kvs.iter() @@ -551,13 +543,13 @@ fn type_last_layer( .map(|(x, v)| Ok((x.clone(), v.as_ref().map(|v| v.to_type())))); let t = v.get_type()?.into_owned(); let kts = kts.chain(once(Ok((x.clone(), Some(t))))); - Ok(RetType(tck_union_type(ctx, kts)?.to_type())) + Ok(RetTypeOnly(tck_union_type(ctx, kts)?.to_type())) } Field(r, x) => { - match &r.get_type()?.internal_whnf() { - Some(Value::RecordType(kts)) => match kts.get(&x) { + match &r.get_type()?.to_value() { + Value::RecordType(kts) => match kts.get(&x) { Some(tth) => { - Ok(RetType(tth.to_type(ctx)?)) + Ok(RetTypeOnly(tth.to_type())) }, None => Err(mkerr(MissingRecordField(x.clone(), r.clone()))), @@ -565,22 +557,22 @@ fn type_last_layer( // TODO: branch here only when r.get_type() is a Const _ => { let r = r.to_type(); - match &r.internal_whnf() { - Some(Value::UnionType(kts)) => match kts.get(&x) { + match &r.to_value() { + Value::UnionType(kts) => match kts.get(&x) { // Constructor has type T -> < x: T, ... > Some(Some(t)) => { // TODO: avoid capture - Ok(RetType( + Ok(RetTypeOnly( tck_pi_type( ctx, "_".into(), - t.to_type(ctx)?, + t.to_type(), r.clone(), )?.to_type() )) }, Some(None) => { - Ok(RetType(r.clone())) + Ok(RetTypeOnly(r.clone())) }, None => { Err(mkerr(MissingUnionField( @@ -603,14 +595,14 @@ fn type_last_layer( // ))), } } - Const(c) => Ok(RetTyped(Typed::from_const(*c))), + Const(c) => Ok(RetWhole(Typed::from_const(*c))), Builtin(b) => { - Ok(RetType(mktype(ctx, rc(type_of_builtin(*b)).absurd())?)) + Ok(RetTypeOnly(mktype(ctx, rc(type_of_builtin(*b)).absurd())?)) } - BoolLit(_) => Ok(RetType(builtin_to_type(Bool)?)), - NaturalLit(_) => Ok(RetType(builtin_to_type(Natural)?)), - IntegerLit(_) => Ok(RetType(builtin_to_type(Integer)?)), - DoubleLit(_) => Ok(RetType(builtin_to_type(Double)?)), + BoolLit(_) => Ok(RetTypeOnly(builtin_to_type(Bool)?)), + NaturalLit(_) => Ok(RetTypeOnly(builtin_to_type(Natural)?)), + IntegerLit(_) => Ok(RetTypeOnly(builtin_to_type(Integer)?)), + DoubleLit(_) => Ok(RetTypeOnly(builtin_to_type(Double)?)), TextLit(interpolated) => { let text_type = builtin_to_type(Text)?; for contents in interpolated.iter() { @@ -623,11 +615,11 @@ fn type_last_layer( ); } } - Ok(RetType(text_type)) + Ok(RetTypeOnly(text_type)) } BinOp(o @ ListAppend, l, r) => { - match l.get_type()?.internal_whnf() { - Some(Value::AppliedBuiltin(List, _)) => {} + match l.get_type()?.to_value() { + Value::AppliedBuiltin(List, _) => {} _ => return Err(mkerr(BinOpTypeMismatch(*o, l.clone()))), } @@ -637,7 +629,7 @@ fn type_last_layer( mkerr(BinOpTypeMismatch(*o, r.clone())) ); - Ok(RetType(l.get_type()?.into_owned())) + Ok(RetTypeOnly(l.get_type()?.into_owned())) } BinOp(o, l, r) => { let t = builtin_to_type(match o { @@ -664,7 +656,7 @@ fn type_last_layer( mkerr(BinOpTypeMismatch(*o, r.clone())) ); - Ok(RetType(t)) + Ok(RetTypeOnly(t)) } Merge(record, union, type_annot) => { let handlers = match record.get_type()?.to_value() { @@ -679,48 +671,47 @@ 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(ctx)?; - let handler_type = handler.to_type(ctx)?; - let (x, tx, tb) = match &handler_type.to_value() { - Value::Pi(x, tx, tb) => { - (x.clone(), tx.to_type(ctx)?, tb.to_type(ctx)?) - } - _ => { - 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.to_typed(), + ))) + } + }; - 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.to_typed(), + tx.clone().to_normalized(), + variant_type.to_typed(), + )) + }); - // 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(ctx)?, - 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) => { @@ -742,10 +733,10 @@ fn type_last_layer( (Some(ref t1), Some(t2)) => { let t2 = t2.to_type(); ensure_equal!(t1, &t2, mkerr(MergeAnnotMismatch)); - Ok(RetType(t2)) + Ok(RetTypeOnly(t2)) } - (Some(t), None) => Ok(RetType(t)), - (None, Some(t)) => Ok(RetType(t.to_type())), + (Some(t), None) => Ok(RetTypeOnly(t)), + (None, Some(t)) => Ok(RetTypeOnly(t.to_type())), (None, None) => return Err(mkerr(MergeEmptyNeedsAnnotation)), } } @@ -764,7 +755,7 @@ fn type_last_layer( }; } - Ok(RetType( + Ok(RetTypeOnly( Typed::from_thunk_and_type( Value::RecordType(new_kts).into_thunk(), trecord.get_type()?.into_owned(), -- cgit v1.2.3