From c7d9a8659214a228963ea40d76e361bbc08129bb Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 18 Aug 2019 15:24:13 +0200
Subject: Rework ValueInternal and clarify invariants around ValueF

---
 dhall/src/phase/normalize.rs | 29 +++++++++++++++++++++--------
 1 file changed, 21 insertions(+), 8 deletions(-)

(limited to 'dhall/src/phase')

diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 93f2528..6c65e43 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -389,14 +389,6 @@ pub(crate) fn squash_textlit(
     ret
 }
 
-// Small helper enum to avoid repetition
-enum Ret<'a> {
-    ValueF(ValueF),
-    Value(Value),
-    ValueRef(&'a Value),
-    Expr(ExprF<Value, Normalized>),
-}
-
 /// Performs an intersection of two HashMaps.
 ///
 /// # Arguments
@@ -510,6 +502,14 @@ where
     kvs
 }
 
+// Small helper enum to avoid repetition
+enum Ret<'a> {
+    ValueF(ValueF),
+    Value(Value),
+    ValueRef(&'a Value),
+    Expr(ExprF<Value, Normalized>),
+}
+
 fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
     use BinOp::{
         BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus,
@@ -819,3 +819,16 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
         Ret::Expr(expr) => ValueF::PartialExpr(expr),
     }
 }
+
+/// Normalize a ValueF into WHNF
+pub(crate) fn normalize_whnf(v: ValueF) -> ValueF {
+    match v {
+        ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args),
+        ValueF::PartialExpr(e) => normalize_one_layer(e),
+        ValueF::TextLit(elts) => {
+            ValueF::TextLit(squash_textlit(elts.into_iter()))
+        }
+        // All other cases are already in WHNF
+        v => v,
+    }
+}
-- 
cgit v1.2.3