From 949da31876c899dc7de295328fb7acc8063cdc7c Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 27 Apr 2019 22:46:29 +0200
Subject: Move Pi to WHNF

---
 dhall/src/normalize.rs | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'dhall/src/normalize.rs')

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);
-- 
cgit v1.2.3