diff options
author | Nadrieril | 2019-04-27 22:46:29 +0200 |
---|---|---|
committer | Nadrieril | 2019-04-27 22:47:55 +0200 |
commit | 949da31876c899dc7de295328fb7acc8063cdc7c (patch) | |
tree | 4d38d7ca7bd4b4f11e5c5d70196270da225bf13b /dhall/src/normalize.rs | |
parent | 290d013e38849e52c35c1bb26c80452590f68e9a (diff) |
Move Pi to WHNF
Diffstat (limited to 'dhall/src/normalize.rs')
-rw-r--r-- | dhall/src/normalize.rs | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index 9ca890e..2dc4cab 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -345,6 +345,7 @@ pub(crate) enum WHNF { ListConsClosure(TypeThunk, Option<Thunk>), /// `λ(x : Natural) -> x + 1` NaturalSuccClosure, + Pi(Label, TypeThunk, TypeThunk), BoolLit(bool), NaturalLit(Natural), @@ -400,6 +401,11 @@ impl WHNF { WHNF::NaturalSuccClosure => { dhall::subexpr!(λ(x : Natural) -> x + 1) } + WHNF::Pi(x, t, e) => rc(ExprF::Pi( + x, + t.normalize().normalize_to_expr(), + e.normalize().normalize_to_expr(), + )), WHNF::BoolLit(b) => rc(ExprF::BoolLit(b)), WHNF::NaturalLit(n) => rc(ExprF::NaturalLit(n)), WHNF::IntegerLit(n) => rc(ExprF::IntegerLit(n)), @@ -558,6 +564,10 @@ impl WHNF { x.shift(delta, var); } } + WHNF::Pi(x, t, e) => { + t.shift(delta, var); + e.shift(delta, &var.shift0(1, x)); + } WHNF::NEListLit(elts) => { for x in elts.iter_mut() { x.shift(delta, var); |