From a987d01a8d1248f35ba19babb66aebabfad47a6d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 27 Apr 2019 15:28:16 +0200 Subject: Define new intermediate expression type --- dhall/src/expr.rs | 7 +++++++ dhall/src/normalize.rs | 55 +++++++++++++++++++++++++++++++++----------------- 2 files changed, 43 insertions(+), 19 deletions(-) diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs index a548d32..6048928 100644 --- a/dhall/src/expr.rs +++ b/dhall/src/expr.rs @@ -45,6 +45,13 @@ pub(crate) struct Typed<'a>( ); derive_other_traits!(Typed); +#[derive(Debug, Clone)] +pub(crate) struct PartiallyNormalized<'a>( + pub(crate) crate::normalize::WHNF, + pub(crate) Option>, + pub(crate) PhantomData<&'a ()>, +); + #[derive(Debug, Clone)] pub(crate) struct Normalized<'a>( pub(crate) SubExpr, diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index 7d19ec0..14b062f 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -9,15 +9,27 @@ use dhall_core::{ }; use dhall_generator as dhall; -use crate::expr::{Normalized, Typed}; +use crate::expr::{Normalized, PartiallyNormalized, Typed}; type InputSubExpr = SubExpr>; type OutputSubExpr = SubExpr; impl<'a> Typed<'a> { + /// Reduce an expression to its normal form, performing beta reduction + /// + /// `normalize` does not type-check the expression. You may want to type-check + /// expressions before normalizing them since normalization can convert an + /// ill-typed expression into a well-typed expression. + /// + /// However, `normalize` will not fail if the expression is ill-typed and will + /// leave ill-typed sub-expressions unevaluated. + /// pub fn normalize(self) -> Normalized<'a> { - Normalized( - normalize( + self.normalize_whnf().normalize() + } + pub(crate) fn normalize_whnf(self) -> PartiallyNormalized<'a> { + PartiallyNormalized( + normalize_whnf( NormalizationContext::from_typecheck_ctx(&self.2), self.0, ), @@ -36,6 +48,24 @@ impl<'a> Typed<'a> { } } +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