diff options
author | Nadrieril | 2019-04-27 17:09:24 +0200 |
---|---|---|
committer | Nadrieril | 2019-04-27 17:15:39 +0200 |
commit | 5b5d4b683b483b153f7e30c0b91270ed237f18c8 (patch) | |
tree | 6aa512b150cf423fcc60b24ecd5c833903355ed7 /dhall/src/normalize.rs | |
parent | f8c5d756edd1de37e3ea09dba9bfa0e46078529b (diff) |
Replace TypeInternal::RecordType with WHNF::RecordType
Diffstat (limited to '')
-rw-r--r-- | dhall/src/normalize.rs | 21 |
1 files changed, 17 insertions, 4 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index 9c62923..9ca890e 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, Typed}; +use crate::expr::{Normalized, PartiallyNormalized, Type, Typed}; type InputSubExpr = SubExpr<X, Normalized<'static>>; type OutputSubExpr = SubExpr<X, X>; @@ -365,7 +365,7 @@ pub(crate) enum WHNF { impl WHNF { /// Convert the value back to a (normalized) syntactic expression - fn normalize_to_expr(self) -> OutputSubExpr { + pub(crate) fn normalize_to_expr(self) -> OutputSubExpr { match self { WHNF::Lam(x, t, (ctx, e)) => { let ctx2 = ctx.skip(&x); @@ -615,7 +615,7 @@ impl Thunk { Thunk::Normalized(Box::new(v)) } - fn normalize(self) -> WHNF { + pub(crate) fn normalize(self) -> WHNF { match self { Thunk::Normalized(v) => *v, Thunk::Unnormalized(ctx, e) => normalize_whnf(ctx, e), @@ -634,7 +634,7 @@ impl Thunk { #[derive(Debug, Clone)] pub(crate) enum TypeThunk { Thunk(Thunk), - // Type(Type<'static>), + Type(Type<'static>), } impl TypeThunk { @@ -646,6 +646,10 @@ impl TypeThunk { TypeThunk::Thunk(th) } + pub(crate) fn from_type(t: Type<'static>) -> Self { + TypeThunk::Type(t) + } + fn from_whnf(v: WHNF) -> Self { TypeThunk::from_thunk(Thunk::from_whnf(v)) } @@ -653,12 +657,21 @@ impl TypeThunk { fn normalize(self) -> WHNF { match self { TypeThunk::Thunk(th) => th.normalize(), + // TODO: let's hope for the best with the unwraps + TypeThunk::Type(t) => normalize_whnf( + NormalizationContext::new(), + t.into_normalized().unwrap().0.embed_absurd(), + ), } } fn shift(&mut self, delta: isize, var: &V<Label>) { match self { TypeThunk::Thunk(th) => th.shift(delta, var), + TypeThunk::Type(t) => { + let shifted = t.shift(delta, var); + std::mem::replace(t, shifted); + } } } } |