From 77af0bbc171618f48531cc6b1d77e18089928885 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 13 Aug 2019 20:54:15 +0200
Subject: Stop tracking the absence of Embed values at the type level

---
 dhall/src/core/thunk.rs | 12 ++++++------
 dhall/src/core/value.rs | 10 +++++-----
 2 files changed, 11 insertions(+), 11 deletions(-)

(limited to 'dhall/src/core')

diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs
index c18014e..4d193f9 100644
--- a/dhall/src/core/thunk.rs
+++ b/dhall/src/core/thunk.rs
@@ -2,7 +2,7 @@ use std::borrow::Cow;
 use std::cell::{Ref, RefCell};
 use std::rc::Rc;
 
-use dhall_syntax::{Const, ExprF, X};
+use dhall_syntax::{Const, ExprF};
 
 use crate::core::context::{NormalizationContext, TypecheckContext};
 use crate::core::value::Value;
@@ -12,7 +12,7 @@ use crate::phase::normalize::{
     apply_any, normalize_one_layer, normalize_whnf, InputSubExpr, OutputSubExpr,
 };
 use crate::phase::typecheck::type_of_const;
-use crate::phase::{NormalizedSubExpr, Type, Typed};
+use crate::phase::{Normalized, NormalizedSubExpr, Type, Typed};
 
 #[derive(Debug, Clone, Copy)]
 enum Marker {
@@ -30,7 +30,7 @@ enum ThunkInternal {
     /// Partially normalized value whose subexpressions have been thunked (this is returned from
     /// typechecking). Note that this is different from `Value::PartialExpr` because there is no
     /// requirement of WHNF here.
-    PartialExpr(ExprF<Thunk, X>),
+    PartialExpr(ExprF<Thunk, Normalized>),
     /// Partially normalized value.
     /// Invariant: if the marker is `NF`, the value must be fully normalized
     Value(Marker, Value),
@@ -123,7 +123,7 @@ impl Thunk {
         ThunkInternal::Value(WHNF, v).into_thunk()
     }
 
-    pub fn from_partial_expr(e: ExprF<Thunk, X>) -> Thunk {
+    pub fn from_partial_expr(e: ExprF<Thunk, Normalized>) -> Thunk {
         ThunkInternal::PartialExpr(e).into_thunk()
     }
 
@@ -309,7 +309,7 @@ impl Shift for ThunkInternal {
                 e.traverse_ref_with_special_handling_of_binders(
                     |v| Ok(v.shift(delta, var)?),
                     |x, v| Ok(v.shift(delta, &var.under_binder(x))?),
-                    |x| Ok(X::clone(x)),
+                    |x| Ok(Normalized::clone(x)),
                 )?,
             ),
             ThunkInternal::Value(m, v) => {
@@ -356,7 +356,7 @@ impl Subst<Typed> for ThunkInternal {
                             &val.under_binder(x),
                         )
                     },
-                    X::clone,
+                    Normalized::clone,
                 ),
             ),
             ThunkInternal::Value(_, v) => {
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 8486d6e..88d7a20 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -2,7 +2,7 @@ use std::collections::HashMap;
 
 use dhall_syntax::{
     rc, Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label,
-    NaiveDouble, Natural, X,
+    NaiveDouble, Natural,
 };
 
 use crate::core::thunk::{Thunk, TypedThunk};
@@ -10,7 +10,7 @@ use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
 use crate::phase::normalize::{
     apply_builtin, normalize_one_layer, squash_textlit, OutputSubExpr,
 };
-use crate::phase::Typed;
+use crate::phase::{Normalized, Typed};
 
 /// A semantic value. The invariants ensure this value represents a Weak-Head
 /// Normal Form (WHNF). This means that this first constructor is the first constructor of the
@@ -59,7 +59,7 @@ pub enum Value {
     TextLit(Vec<InterpolatedTextContents<Thunk>>),
     Equivalence(TypedThunk, TypedThunk),
     // Invariant: this must not contain a value captured by one of the variants above.
-    PartialExpr(ExprF<Thunk, X>),
+    PartialExpr(ExprF<Thunk, Normalized>),
 }
 
 impl Value {
@@ -475,7 +475,7 @@ impl Shift for Value {
                 e.traverse_ref_with_special_handling_of_binders(
                     |v| Ok(v.shift(delta, var)?),
                     |x, v| Ok(v.shift(delta, &var.under_binder(x))?),
-                    |x| Ok(X::clone(x)),
+                    |x| Ok(Normalized::clone(x)),
                 )?,
             ),
         })
@@ -500,7 +500,7 @@ impl Subst<Typed> for Value {
                             &val.under_binder(x),
                         )
                     },
-                    X::clone,
+                    Normalized::clone,
                 ))
             }
             // Retry normalizing since substituting may allow progress
-- 
cgit v1.2.3