From 673a580e11d31356bec25d73213b283685fd6ea3 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 30 Jan 2020 19:49:03 +0000
Subject: Clarify normalization to ensure we only nze once

---
 dhall/src/semantics/builtins.rs | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'dhall/src/semantics/builtins.rs')

diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs
index 1357adf..85ef294 100644
--- a/dhall/src/semantics/builtins.rs
+++ b/dhall/src/semantics/builtins.rs
@@ -12,7 +12,7 @@ use std::collections::HashMap;
 use std::convert::TryInto;
 
 /// A partially applied builtin.
-/// Invariant: TODO
+/// Invariant: the evaluation of the given args must not be able to progress further
 #[derive(Debug, Clone)]
 pub(crate) struct BuiltinClosure<Value> {
     pub env: NzEnv,
@@ -41,9 +41,8 @@ impl BuiltinClosure<Value> {
         let types = self.types.iter().cloned().chain(once(f_ty)).collect();
         apply_builtin(self.b, args, ret_ty, types, self.env.clone())
     }
-    pub fn ensure_whnf(self, ret_ty: &Value) -> ValueKind {
-        apply_builtin(self.b, self.args, ret_ty, self.types, self.env)
-    }
+    /// This doesn't break the invariant because we already checked that the appropriate arguments
+    /// did not normalize to something that allows evaluation to proceed.
     pub fn normalize_mut(&mut self) {
         for x in self.args.iter_mut() {
             x.normalize_mut();
-- 
cgit v1.2.3