diff options
author | Nadrieril | 2019-04-30 15:35:13 +0200 |
---|---|---|
committer | Nadrieril | 2019-04-30 15:35:13 +0200 |
commit | 77198a2833297289770867acdaf31db0e2011ea9 (patch) | |
tree | c5bbfad8e1cfc82f2e22868938a41d630ac4962a /dhall/src | |
parent | e2626a0bfd4b145e7d54c2150457f57e798ba2f7 (diff) |
Merge Typed and PartiallyNormalized
Diffstat (limited to 'dhall/src')
-rw-r--r-- | dhall/src/expr.rs | 7 | ||||
-rw-r--r-- | dhall/src/normalize.rs | 74 | ||||
-rw-r--r-- | dhall/src/typecheck.rs | 137 |
3 files changed, 94 insertions, 124 deletions
diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs index c794324..1ddc4ba 100644 --- a/dhall/src/expr.rs +++ b/dhall/src/expr.rs @@ -44,13 +44,6 @@ pub(crate) struct Typed<'a>( ); #[derive(Debug, Clone)] -pub(crate) struct PartiallyNormalized<'a>( - pub(crate) crate::normalize::Value, - pub(crate) Option<Type<'static>>, - pub(crate) PhantomData<&'a ()>, -); - -#[derive(Debug, Clone)] pub(crate) struct Normalized<'a>( pub(crate) SubExpr<X, X>, pub(crate) Option<Type<'static>>, diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index 5151790..f15eea4 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -9,7 +9,7 @@ use dhall_core::{ }; use dhall_generator as dhall; -use crate::expr::{Normalized, PartiallyNormalized, Type, Typed}; +use crate::expr::{Normalized, Type, Typed}; type InputSubExpr = SubExpr<X, Normalized<'static>>; type OutputSubExpr = SubExpr<X, X>; @@ -25,37 +25,35 @@ impl<'a> Typed<'a> { /// leave ill-typed sub-expressions unevaluated. /// pub fn normalize(self) -> Normalized<'a> { - self.partially_normalize().normalize() + Normalized(self.0.as_whnf().normalize_to_expr(), self.1, self.2) } - pub(crate) fn partially_normalize(self) -> PartiallyNormalized<'a> { - PartiallyNormalized(self.0.as_whnf(), self.1, self.2) - } -} -impl<'a> PartiallyNormalized<'a> { - pub(crate) fn normalize(self) -> Normalized<'a> { - Normalized(self.0.normalize_to_expr(), self.1, self.2) - } pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self { - PartiallyNormalized( + Typed( self.0.shift(delta, var), self.1.as_ref().map(|x| x.shift(delta, var)), self.2, ) } + pub(crate) fn subst_shift( &self, var: &V<Label>, - val: &PartiallyNormalized<'static>, + val: &Typed<'static>, ) -> Self { - PartiallyNormalized( + Typed( self.0.subst_shift(var, val), self.1.as_ref().map(|x| x.subst_shift(var, val)), self.2, ) } - pub(crate) fn into_whnf(self) -> Value { - self.0 + + pub(crate) fn normalize_whnf(&self) -> Value { + self.0.as_whnf() + } + + pub(crate) fn as_thunk(&self) -> Thunk { + self.0.clone() } } @@ -268,13 +266,11 @@ impl EnvItem { pub(crate) fn subst_shift( &self, var: &V<Label>, - val: &PartiallyNormalized<'static>, + val: &Typed<'static>, ) -> Self { match self { EnvItem::Thunk(e) => EnvItem::Thunk(e.subst_shift(var, val)), - EnvItem::Skip(v) if v == var => { - EnvItem::Thunk(Thunk::from_whnf(val.clone().into_whnf())) - } + EnvItem::Skip(v) if v == var => EnvItem::Thunk(val.as_thunk()), EnvItem::Skip(v) => EnvItem::Skip(v.shift(-1, var)), } } @@ -331,11 +327,7 @@ impl NormalizationContext { NormalizationContext(Rc::new(self.0.map(|_, e| e.shift(delta, var)))) } - fn subst_shift( - &self, - var: &V<Label>, - val: &PartiallyNormalized<'static>, - ) -> Self { + fn subst_shift(&self, var: &V<Label>, val: &Typed<'static>) -> Self { NormalizationContext(Rc::new( self.0.map(|_, e| e.subst_shift(var, val)), )) @@ -377,6 +369,10 @@ pub(crate) enum Value { } impl Value { + pub(crate) fn into_thunk(self) -> Thunk { + Thunk::from_whnf(self) + } + /// Convert the value back to a (normalized) syntactic expression pub(crate) fn normalize_to_expr(self) -> OutputSubExpr { match self { @@ -585,8 +581,11 @@ impl Value { pub(crate) fn app(self, val: Value) -> Value { match (self, val) { (Value::Lam(x, _, e), val) => { - let val = - PartiallyNormalized(val, None, std::marker::PhantomData); + let val = Typed( + Thunk::from_whnf(val), + None, + std::marker::PhantomData, + ); e.subst_shift(&V(x, 0), &val).as_whnf() } (Value::AppliedBuiltin(b, mut args), val) => { @@ -717,7 +716,7 @@ impl Value { pub(crate) fn subst_shift( &self, var: &V<Label>, - val: &PartiallyNormalized<'static>, + val: &Typed<'static>, ) -> Self { match self { Value::Lam(x, t, e) => Value::Lam( @@ -742,7 +741,7 @@ impl Value { t.subst_shift(var, val), e.subst_shift(&var.shift0(1, x), val), ), - Value::Var(v) if v == var => val.clone().into_whnf(), + Value::Var(v) if v == var => val.normalize_whnf(), Value::Var(v) => Value::Var(v.shift(-1, var)), Value::Const(c) => Value::Const(*c), Value::BoolLit(b) => Value::BoolLit(*b), @@ -814,7 +813,7 @@ impl Value { mod thunk { use super::{normalize_whnf, InputSubExpr, NormalizationContext, Value}; - use crate::expr::PartiallyNormalized; + use crate::expr::Typed; use dhall_core::{Label, V}; use std::cell::RefCell; use std::rc::Rc; @@ -900,11 +899,7 @@ mod thunk { } } - fn subst_shift( - &self, - var: &V<Label>, - val: &PartiallyNormalized<'static>, - ) -> Self { + fn subst_shift(&self, var: &V<Label>, val: &Typed<'static>) -> Self { match self { ThunkInternal::Unnormalized(ctx, e) => { ThunkInternal::Unnormalized( @@ -953,7 +948,7 @@ mod thunk { pub(crate) fn subst_shift( &self, var: &V<Label>, - val: &PartiallyNormalized<'static>, + val: &Typed<'static>, ) -> Self { self.0.borrow().subst_shift(var, val).into_thunk() } @@ -1003,7 +998,7 @@ impl TypeThunk { pub(crate) fn subst_shift( &self, var: &V<Label>, - val: &PartiallyNormalized<'static>, + val: &Typed<'static>, ) -> Self { match self { TypeThunk::Thunk(th) => TypeThunk::Thunk(th.subst_shift(var, val)), @@ -1015,12 +1010,7 @@ impl TypeThunk { match self { TypeThunk::Thunk(th) => th.as_nf(), // TODO: let's hope for the best with the unwrap - TypeThunk::Type(t) => t - .clone() - .partially_normalize() - .unwrap() - .into_whnf() - .normalize(), + TypeThunk::Type(t) => t.normalize_whnf().unwrap().normalize(), } } } diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 85de42a..f22925a 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -68,8 +68,8 @@ impl<'a> Normalized<'a> { // TODO: wasteful type_with(ctx, self.0.embed_absurd())?.normalize_to_type() } - _ => Type(TypeInternal::PNzed(Box::new(PartiallyNormalized( - Value::Expr(self.0), + _ => Type(TypeInternal::Typed(Box::new(Typed( + Value::Expr(self.0).into_thunk(), self.1, self.2, )))), @@ -86,11 +86,12 @@ impl Normalized<'static> { rc(ExprF::Embed(self)) } } -impl<'a> PartiallyNormalized<'a> { +impl<'a> Typed<'a> { fn normalize_to_type(self) -> Type<'a> { - match &self.0 { + // TODO: avoid cloning Value + match &self.normalize_whnf() { Value::Const(c) => Type(TypeInternal::Const(*c)), - _ => Type(TypeInternal::PNzed(Box::new(self))), + _ => Type(TypeInternal::Typed(Box::new(self))), } } } @@ -103,18 +104,16 @@ impl<'a> Type<'a> { pub(crate) fn into_normalized(self) -> Result<Normalized<'a>, TypeError> { self.0.into_normalized() } - fn normalize_whnf(self) -> Result<Value, TypeError> { + pub(crate) fn normalize_whnf(&self) -> Result<Value, TypeError> { self.0.normalize_whnf() } - pub(crate) fn partially_normalize( - self, - ) -> Result<PartiallyNormalized<'a>, TypeError> { - self.0.partially_normalize() + pub(crate) fn as_typed(&self) -> Result<Typed<'a>, TypeError> { + self.0.as_typed() } fn internal(&self) -> &TypeInternal<'a> { &self.0 } - fn internal_whnf(&self) -> Option<&Value> { + fn internal_whnf(&self) -> Option<Value> { self.0.whnf() } pub(crate) fn shift0(&self, delta: isize, label: &Label) -> Self { @@ -126,7 +125,7 @@ impl<'a> Type<'a> { pub(crate) fn subst_shift( &self, var: &V<Label>, - val: &PartiallyNormalized<'static>, + val: &Typed<'static>, ) -> Self { Type(self.0.subst_shift(var, val)) } @@ -172,20 +171,20 @@ pub(crate) enum TypeInternal<'a> { /// The type of `Sort` SuperType, /// This must not contain Const value. - PNzed(Box<PartiallyNormalized<'a>>), + Typed(Box<Typed<'a>>), } impl<'a> TypeInternal<'a> { - pub(crate) fn into_normalized(self) -> Result<Normalized<'a>, TypeError> { - Ok(self.partially_normalize()?.normalize()) + pub(crate) fn into_normalized(&self) -> Result<Normalized<'a>, TypeError> { + Ok(self.as_typed()?.normalize()) } - fn normalize_whnf(self) -> Result<Value, TypeError> { - Ok(self.partially_normalize()?.into_whnf()) + fn normalize_whnf(&self) -> Result<Value, TypeError> { + Ok(self.as_typed()?.normalize_whnf()) } - fn partially_normalize(self) -> Result<PartiallyNormalized<'a>, TypeError> { + fn as_typed(&self) -> Result<Typed<'a>, TypeError> { Ok(match self { - TypeInternal::PNzed(e) => *e, - TypeInternal::Const(c) => const_to_pnormalized(c), + TypeInternal::Typed(e) => e.as_ref().clone(), + TypeInternal::Const(c) => const_to_typed(*c), TypeInternal::SuperType => { return Err(TypeError::new( &TypecheckContext::new(), @@ -194,9 +193,10 @@ impl<'a> TypeInternal<'a> { } }) } - fn whnf(&self) -> Option<&Value> { + fn whnf(&self) -> Option<Value> { + // TODO: return reference match self { - TypeInternal::PNzed(e) => Some(&e.0), + TypeInternal::Typed(e) => Some(e.normalize_whnf()), _ => None, } } @@ -206,19 +206,15 @@ impl<'a> TypeInternal<'a> { fn shift(&self, delta: isize, var: &V<Label>) -> Self { use TypeInternal::*; match self { - PNzed(e) => PNzed(Box::new(e.shift(delta, var))), + Typed(e) => Typed(Box::new(e.shift(delta, var))), Const(c) => Const(*c), SuperType => SuperType, } } - fn subst_shift( - &self, - var: &V<Label>, - val: &PartiallyNormalized<'static>, - ) -> Self { + fn subst_shift(&self, var: &V<Label>, val: &Typed<'static>) -> Self { use TypeInternal::*; match self { - PNzed(e) => PNzed(Box::new(e.subst_shift(var, val))), + Typed(e) => Typed(Box::new(e.subst_shift(var, val))), Const(c) => Const(*c), SuperType => SuperType, } @@ -252,9 +248,7 @@ impl TypedOrType { } fn normalize_to_type(self) -> Type<'static> { match self { - TypedOrType::Typed(e) => { - e.partially_normalize().normalize_to_type() - } + TypedOrType::Typed(e) => e.normalize_to_type(), TypedOrType::Type(t) => t, } } @@ -270,12 +264,10 @@ impl TypedOrType { TypedOrType::Type(t) => Ok(t.get_type()?.into_owned()), } } - fn partially_normalize( - self, - ) -> Result<PartiallyNormalized<'static>, TypeError> { + fn as_typed(&self) -> Result<Typed<'static>, TypeError> { match self { - TypedOrType::Typed(e) => Ok(e.partially_normalize()), - TypedOrType::Type(t) => Ok(t.partially_normalize()?), + TypedOrType::Typed(e) => Ok(e.clone()), + TypedOrType::Type(t) => Ok(t.as_typed()?), } } } @@ -442,8 +434,12 @@ where } } -fn const_to_pnormalized<'a>(c: Const) -> PartiallyNormalized<'a> { - PartiallyNormalized(Value::Const(c), Some(type_of_const(c)), PhantomData) +fn const_to_typed<'a>(c: Const) -> Typed<'a> { + Typed( + Value::Const(c).into_thunk(), + Some(type_of_const(c)), + PhantomData, + ) } fn const_to_type<'a>(c: Const) -> Type<'a> { @@ -555,7 +551,7 @@ pub(crate) enum TypeIntermediate { impl TypeIntermediate { fn typecheck(self) -> Result<TypedOrType, TypeError> { let mkerr = |ctx, msg| TypeError::new(ctx, msg); - match &self { + let typed = match &self { TypeIntermediate::Pi(ctx, x, ta, tb) => { let ctx2 = ctx.insert_type(x, ta.clone()); @@ -600,18 +596,16 @@ impl TypeIntermediate { } }; - let pnormalized = PartiallyNormalized( + Typed( Value::Pi( x.clone(), TypeThunk::from_type(ta.clone()), TypeThunk::from_type(tb.clone()), - ), + ) + .into_thunk(), Some(const_to_type(k)), PhantomData, - ); - Ok(TypedOrType::Type(Type(TypeInternal::PNzed(Box::new( - pnormalized, - ))))) + ) } TypeIntermediate::RecordType(ctx, kts) => { // Check that all types are the same const @@ -634,20 +628,18 @@ impl TypeIntermediate { // An empty record type has type Type let k = k.unwrap_or(dhall_core::Const::Type); - let pnormalized = PartiallyNormalized( + Typed( Value::RecordType( kts.iter() .map(|(k, t)| { (k.clone(), TypeThunk::from_type(t.clone())) }) .collect(), - ), + ) + .into_thunk(), Some(const_to_type(k)), PhantomData, - ); - Ok(TypedOrType::Type(Type(TypeInternal::PNzed(Box::new( - pnormalized, - ))))) + ) } TypeIntermediate::UnionType(ctx, kts) => { // Check that all types are the same const @@ -675,7 +667,7 @@ impl TypeIntermediate { // an union type with only unary variants also has type Type let k = k.unwrap_or(dhall_core::Const::Type); - let pnormalized = PartiallyNormalized( + Typed( Value::UnionType( kts.iter() .map(|(k, t)| { @@ -687,28 +679,24 @@ impl TypeIntermediate { ) }) .collect(), - ), + ) + .into_thunk(), Some(const_to_type(k)), PhantomData, - ); - Ok(TypedOrType::Type(Type(TypeInternal::PNzed(Box::new( - pnormalized, - ))))) + ) } TypeIntermediate::ListType(ctx, t) => { ensure_simple_type!( t, mkerr(ctx, InvalidListType(t.clone().into_normalized()?)), ); - let pnormalized = PartiallyNormalized( + Typed( Value::from_builtin(Builtin::List) - .app(t.clone().normalize_whnf()?), + .app(t.clone().normalize_whnf()?) + .into_thunk(), Some(const_to_type(Const::Type)), PhantomData, - ); - Ok(TypedOrType::Type(Type(TypeInternal::PNzed(Box::new( - pnormalized, - ))))) + ) } TypeIntermediate::OptionalType(ctx, t) => { ensure_simple_type!( @@ -718,17 +706,18 @@ impl TypeIntermediate { InvalidOptionalType(t.clone().into_normalized()?) ), ); - let pnormalized = PartiallyNormalized( + Typed( Value::from_builtin(Builtin::Optional) - .app(t.clone().normalize_whnf()?), + .app(t.clone().normalize_whnf()?) + .into_thunk(), Some(const_to_type(Const::Type)), PhantomData, - ); - Ok(TypedOrType::Type(Type(TypeInternal::PNzed(Box::new( - pnormalized, - ))))) + ) } - } + }; + Ok(TypedOrType::Type(Type(TypeInternal::Typed(Box::new( + typed, + ))))) } } @@ -867,13 +856,11 @@ fn type_last_layer( } _ => return Err(mkerr(NotAFunction(f))), }; - ensure_equal!(a.get_type()?, tx, { + ensure_equal!(a.get_type()?, &tx, { mkerr(TypeMismatch(f.clone(), tx.clone().into_normalized()?, a)) }); - Ok(RetType( - tb.subst_shift(&V(x.clone(), 0), &a.partially_normalize()?), - )) + Ok(RetType(tb.subst_shift(&V(x.clone(), 0), &a.as_typed()?))) } Annot(x, t) => { let t = t.normalize_to_type(); |