s/as_whnf/kind/

4 files changed, 53 insertions, 55 deletions

diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs
index a23591e..a536261 100644
--- a/dhall/src/semantics/builtins.rs
+++ b/dhall/src/semantics/builtins.rs
@@ -290,31 +290,31 @@ fn apply_builtin(
 
     let ret = match (b, args.as_slice()) {
         (OptionalNone, [t]) => Ret::ValueKind(EmptyOptionalLit(t.clone())),
-        (NaturalIsZero, [n]) => match &*n.as_whnf() {
+        (NaturalIsZero, [n]) => match &*n.kind() {
             NaturalLit(n) => Ret::ValueKind(BoolLit(*n == 0)),
             _ => Ret::DoneAsIs,
         },
-        (NaturalEven, [n]) => match &*n.as_whnf() {
+        (NaturalEven, [n]) => match &*n.kind() {
             NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 == 0)),
             _ => Ret::DoneAsIs,
         },
-        (NaturalOdd, [n]) => match &*n.as_whnf() {
+        (NaturalOdd, [n]) => match &*n.kind() {
             NaturalLit(n) => Ret::ValueKind(BoolLit(*n % 2 != 0)),
             _ => Ret::DoneAsIs,
         },
-        (NaturalToInteger, [n]) => match &*n.as_whnf() {
+        (NaturalToInteger, [n]) => match &*n.kind() {
             NaturalLit(n) => Ret::ValueKind(IntegerLit(*n as isize)),
             _ => Ret::DoneAsIs,
         },
         (NaturalShow, [n]) => {
-            match &*n.as_whnf() {
+            match &*n.kind() {
                 NaturalLit(n) => Ret::ValueKind(TextLit(vec![
                     InterpolatedTextContents::Text(n.to_string()),
                 ])),
                 _ => Ret::DoneAsIs,
             }
         }
-        (NaturalSubtract, [a, b]) => match (&*a.as_whnf(), &*b.as_whnf()) {
+        (NaturalSubtract, [a, b]) => match (&*a.kind(), &*b.kind()) {
             (NaturalLit(a), NaturalLit(b)) => {
                 Ret::ValueKind(NaturalLit(if b > a { b - a } else { 0 }))
             }
@@ -323,7 +323,7 @@ fn apply_builtin(
             _ if a == b => Ret::ValueKind(NaturalLit(0)),
             _ => Ret::DoneAsIs,
         },
-        (IntegerShow, [n]) => match &*n.as_whnf() {
+        (IntegerShow, [n]) => match &*n.kind() {
             IntegerLit(n) => {
                 let s = if *n < 0 {
                     n.to_string()
@@ -334,31 +334,31 @@ fn apply_builtin(
             }
             _ => Ret::DoneAsIs,
         },
-        (IntegerToDouble, [n]) => match &*n.as_whnf() {
+        (IntegerToDouble, [n]) => match &*n.kind() {
             IntegerLit(n) => {
                 Ret::ValueKind(DoubleLit(NaiveDouble::from(*n as f64)))
             }
             _ => Ret::DoneAsIs,
         },
-        (IntegerNegate, [n]) => match &*n.as_whnf() {
+        (IntegerNegate, [n]) => match &*n.kind() {
             IntegerLit(n) => Ret::ValueKind(IntegerLit(-n)),
             _ => Ret::DoneAsIs,
         },
-        (IntegerClamp, [n]) => match &*n.as_whnf() {
+        (IntegerClamp, [n]) => match &*n.kind() {
             IntegerLit(n) => {
                 Ret::ValueKind(NaturalLit((*n).try_into().unwrap_or(0)))
             }
             _ => Ret::DoneAsIs,
         },
         (DoubleShow, [n]) => {
-            match &*n.as_whnf() {
+            match &*n.kind() {
                 DoubleLit(n) => Ret::ValueKind(TextLit(vec![
                     InterpolatedTextContents::Text(n.to_string()),
                 ])),
                 _ => Ret::DoneAsIs,
             }
         }
-        (TextShow, [v]) => match &*v.as_whnf() {
+        (TextShow, [v]) => match &*v.kind() {
             TextLit(elts) => {
                 match elts.as_slice() {
                     // Empty string literal.
@@ -390,26 +390,26 @@ fn apply_builtin(
             }
             _ => Ret::DoneAsIs,
         },
-        (ListLength, [_, l]) => match &*l.as_whnf() {
+        (ListLength, [_, l]) => match &*l.kind() {
             EmptyListLit(_) => Ret::ValueKind(NaturalLit(0)),
             NEListLit(xs) => Ret::ValueKind(NaturalLit(xs.len())),
             _ => Ret::DoneAsIs,
         },
-        (ListHead, [_, l]) => match &*l.as_whnf() {
+        (ListHead, [_, l]) => match &*l.kind() {
             EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())),
             NEListLit(xs) => {
                 Ret::ValueKind(NEOptionalLit(xs.iter().next().unwrap().clone()))
             }
             _ => Ret::DoneAsIs,
         },
-        (ListLast, [_, l]) => match &*l.as_whnf() {
+        (ListLast, [_, l]) => match &*l.kind() {
             EmptyListLit(n) => Ret::ValueKind(EmptyOptionalLit(n.clone())),
             NEListLit(xs) => Ret::ValueKind(NEOptionalLit(
                 xs.iter().rev().next().unwrap().clone(),
             )),
             _ => Ret::DoneAsIs,
         },
-        (ListReverse, [_, l]) => match &*l.as_whnf() {
+        (ListReverse, [_, l]) => match &*l.kind() {
             EmptyListLit(n) => Ret::ValueKind(EmptyListLit(n.clone())),
             NEListLit(xs) => {
                 Ret::ValueKind(NEListLit(xs.iter().rev().cloned().collect()))
@@ -417,7 +417,7 @@ fn apply_builtin(
             _ => Ret::DoneAsIs,
         },
         (ListIndexed, [_, l]) => {
-            let l_whnf = l.as_whnf();
+            let l_whnf = l.kind();
             match &*l_whnf {
                 EmptyListLit(_) | NEListLit(_) => {
                     // Extract the type of the list elements
@@ -484,7 +484,7 @@ fn apply_builtin(
                     .app(EmptyListLit(t.clone()).into_value_with_type(list_t)),
             )
         }
-        (ListFold, [_, l, _, cons, nil]) => match &*l.as_whnf() {
+        (ListFold, [_, l, _, cons, nil]) => match &*l.kind() {
             EmptyListLit(_) => Ret::Value(nil.clone()),
             NEListLit(xs) => {
                 let mut v = nil.clone();
@@ -513,7 +513,7 @@ fn apply_builtin(
                     ),
             )
         }
-        (OptionalFold, [_, v, _, just, nothing]) => match &*v.as_whnf() {
+        (OptionalFold, [_, v, _, just, nothing]) => match &*v.kind() {
             EmptyOptionalLit(_) => Ret::Value(nothing.clone()),
             NEOptionalLit(x) => Ret::Value(just.app(x.clone())),
             _ => Ret::DoneAsIs,
@@ -530,7 +530,7 @@ fn apply_builtin(
                 ),
         ),
 
-        (NaturalFold, [n, t, succ, zero]) => match &*n.as_whnf() {
+        (NaturalFold, [n, t, succ, zero]) => match &*n.kind() {
             NaturalLit(0) => Ret::Value(zero.clone()),
             NaturalLit(n) => {
                 let fold = Value::from_builtin(NaturalFold)
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index e69d220..02c8013 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -157,7 +157,7 @@ impl Value {
     }
 
     pub(crate) fn as_const(&self) -> Option<Const> {
-        match &*self.as_whnf() {
+        match &*self.kind() {
             ValueKind::Const(c) => Some(*c),
             _ => None,
         }
@@ -180,7 +180,7 @@ impl Value {
     /// This is what you want if you want to pattern-match on the value.
     /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut
     /// panics.
-    pub(crate) fn as_whnf(&self) -> Ref<ValueKind<Value>> {
+    pub(crate) fn kind(&self) -> Ref<ValueKind<Value>> {
         self.normalize_whnf();
         self.as_kind()
     }
@@ -194,7 +194,7 @@ impl Value {
         self.to_tyexpr_noenv().to_expr(opts)
     }
     pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind<Value> {
-        self.as_whnf().clone()
+        self.kind().clone()
     }
     /// Before discarding type information, check that it matches the expected return type.
     pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueKind<Value> {
@@ -233,7 +233,7 @@ impl Value {
     }
 
     pub(crate) fn app(&self, v: Value) -> Value {
-        let body_t = match &*self.get_type_not_sort().as_whnf() {
+        let body_t = match &*self.get_type_not_sort().kind() {
             ValueKind::PiClosure { annot, closure, .. } => {
                 v.check_type(annot);
                 closure.apply(v.clone())
@@ -617,7 +617,7 @@ impl Closure {
 // TODO: use Rc comparison to shortcut on identical pointers
 impl std::cmp::PartialEq for Value {
     fn eq(&self, other: &Self) -> bool {
-        *self.as_whnf() == *other.as_whnf()
+        *self.kind() == *other.kind()
     }
 }
 impl std::cmp::Eq for Value {}
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index d7720c7..f36ec4a 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -10,7 +10,7 @@ use crate::syntax::{
 };
 
 pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind<Value> {
-    let f_borrow = f.as_whnf();
+    let f_borrow = f.kind();
     match &*f_borrow {
         ValueKind::LamClosure { closure, .. } => {
             closure.apply(a).to_whnf_check_type(ty)
@@ -47,7 +47,7 @@ pub(crate) fn squash_textlit(
             match contents {
                 Text(s) => crnt_str.push_str(&s),
                 Expr(e) => {
-                    let e_borrow = e.as_whnf();
+                    let e_borrow = e.kind();
                     match &*e_borrow {
                         ValueKind::TextLit(elts2) => {
                             inner(elts2.iter().cloned(), crnt_str, ret)
@@ -123,8 +123,8 @@ fn apply_binop<'a>(
         BoolLit, EmptyListLit, NEListLit, NaturalLit, RecordLit, RecordType,
         TextLit,
     };
-    let x_borrow = x.as_whnf();
-    let y_borrow = y.as_whnf();
+    let x_borrow = x.kind();
+    let y_borrow = y.kind();
     Some(match (o, &*x_borrow, &*y_borrow) {
         (BoolAnd, BoolLit(true), _) => Ret::ValueRef(y),
         (BoolAnd, _, BoolLit(true)) => Ret::ValueRef(x),
@@ -206,7 +206,7 @@ fn apply_binop<'a>(
             Ret::ValueRef(y)
         }
         (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
-            let ty_borrow = ty.as_whnf();
+            let ty_borrow = ty.kind();
             let kts = match &*ty_borrow {
                 RecordType(kts) => kts,
                 _ => unreachable!("Internal type error"),
@@ -286,7 +286,7 @@ pub(crate) fn normalize_one_layer(
         ExprKind::DoubleLit(n) => Ret::ValueKind(DoubleLit(n)),
         ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)),
         ExprKind::EmptyListLit(t) => {
-            let arg = match &*t.as_whnf() {
+            let arg = match &*t.kind() {
                 ValueKind::AppliedBuiltin(BuiltinClosure {
                     b: Builtin::List,
                     args,
@@ -319,13 +319,13 @@ pub(crate) fn normalize_one_layer(
             }
         }
         ExprKind::BoolIf(ref b, ref e1, ref e2) => {
-            let b_borrow = b.as_whnf();
+            let b_borrow = b.kind();
             match &*b_borrow {
                 BoolLit(true) => Ret::ValueRef(e1),
                 BoolLit(false) => Ret::ValueRef(e2),
                 _ => {
-                    let e1_borrow = e1.as_whnf();
-                    let e2_borrow = e2.as_whnf();
+                    let e1_borrow = e1.kind();
+                    let e2_borrow = e2.kind();
                     match (&*e1_borrow, &*e2_borrow) {
                         // Simplify `if b then True else False`
                         (BoolLit(true), BoolLit(false)) => Ret::ValueRef(b),
@@ -349,7 +349,7 @@ pub(crate) fn normalize_one_layer(
             Ret::ValueKind(RecordLit(HashMap::new()))
         }
         ExprKind::Projection(ref v, ref ls) => {
-            let v_borrow = v.as_whnf();
+            let v_borrow = v.kind();
             match &*v_borrow {
                 RecordLit(kvs) => Ret::ValueKind(RecordLit(
                     ls.iter()
@@ -365,7 +365,7 @@ pub(crate) fn normalize_one_layer(
             }
         }
         ExprKind::Field(ref v, ref l) => {
-            let v_borrow = v.as_whnf();
+            let v_borrow = v.kind();
             match &*v_borrow {
                 RecordLit(kvs) => match kvs.get(l) {
                     Some(r) => Ret::Value(r.clone()),
@@ -391,8 +391,8 @@ pub(crate) fn normalize_one_layer(
         ExprKind::Completion(_, _) => unimplemented!("record completion"),
 
         ExprKind::Merge(ref handlers, ref variant, _) => {
-            let handlers_borrow = handlers.as_whnf();
-            let variant_borrow = variant.as_whnf();
+            let handlers_borrow = handlers.kind();
+            let variant_borrow = variant.kind();
             match (&*handlers_borrow, &*variant_borrow) {
                 (RecordLit(kvs), UnionConstructor(l, _, _)) => match kvs.get(l)
                 {
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index e1a9c11..0c5e779 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -94,7 +94,7 @@ fn type_one_layer(
         }
         ExprKind::EmptyListLit(t) => {
             let t = t.normalize_nf(env.as_nzenv());
-            match &*t.as_whnf() {
+            match &*t.kind() {
                 ValueKind::AppliedBuiltin(BuiltinClosure {
                     b: Builtin::List,
                     args,
@@ -189,7 +189,7 @@ fn type_one_layer(
             Value::from_const(k)
         }
         ExprKind::Field(scrut, x) => {
-            match &*scrut.get_type()?.as_whnf() {
+            match &*scrut.get_type()?.kind() {
                 ValueKind::RecordType(kts) => match kts.get(&x) {
                     Some(tth) => tth.clone(),
                     None => return mkerr("MissingRecordField"),
@@ -197,7 +197,7 @@ fn type_one_layer(
                 // TODO: branch here only when scrut.get_type() is a Const
                 _ => {
                     let scrut_nf = scrut.normalize_nf(env.as_nzenv());
-                    let scrut_nf_borrow = scrut_nf.as_whnf();
+                    let scrut_nf_borrow = scrut_nf.kind();
                     match &*scrut_nf_borrow {
                         ValueKind::UnionType(kts) => match kts.get(x) {
                             // Constructor has type T -> < x: T, ... >
@@ -244,7 +244,7 @@ fn type_one_layer(
         }
         ExprKind::Assert(t) => {
             let t = t.normalize_whnf(env.as_nzenv());
-            match &*t.as_whnf() {
+            match &*t.kind() {
                 ValueKind::Equivalence(x, y) if x == y => {}
                 ValueKind::Equivalence(..) => return mkerr("AssertMismatch"),
                 _ => return mkerr("AssertMustTakeEquivalence"),
@@ -253,7 +253,7 @@ fn type_one_layer(
         }
         ExprKind::App(f, arg) => {
             let tf = f.get_type()?;
-            let tf_borrow = tf.as_whnf();
+            let tf_borrow = tf.kind();
             match &*tf_borrow {
                 ValueKind::PiClosure { annot, closure, .. } => {
                     if arg.get_type()? != *annot {
@@ -275,9 +275,7 @@ fn type_one_layer(
             }
         }
         ExprKind::BoolIf(x, y, z) => {
-            if *x.get_type()?.as_whnf()
-                != ValueKind::from_builtin(Builtin::Bool)
-            {
+            if *x.get_type()?.kind() != ValueKind::from_builtin(Builtin::Bool) {
                 return mkerr("InvalidPredicate");
             }
             if y.get_type()?.get_type()?.as_const() != Some(Const::Type) {
@@ -297,14 +295,14 @@ fn type_one_layer(
             let y_type = y.get_type()?;
 
             // Extract the LHS record type
-            let x_type_borrow = x_type.as_whnf();
+            let x_type_borrow = x_type.kind();
             let kts_x = match &*x_type_borrow {
                 ValueKind::RecordType(kts) => kts,
                 _ => return mkerr("MustCombineRecord"),
             };
 
             // Extract the RHS record type
-            let y_type_borrow = y_type.as_whnf();
+            let y_type_borrow = y_type.kind();
             let kts_y = match &*y_type_borrow {
                 ValueKind::RecordType(kts) => kts,
                 _ => return mkerr("MustCombineRecord"),
@@ -336,8 +334,8 @@ fn type_one_layer(
         ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => {
             let x_val = x.normalize_whnf(env.as_nzenv());
             let y_val = y.normalize_whnf(env.as_nzenv());
-            let x_val_borrow = x_val.as_whnf();
-            let y_val_borrow = y_val.as_whnf();
+            let x_val_borrow = x_val.kind();
+            let y_val_borrow = y_val.kind();
             let kts_x = match &*x_val_borrow {
                 ValueKind::RecordType(kts) => kts,
                 _ => return mkerr("RecordTypeMergeRequiresRecordType"),
@@ -366,7 +364,7 @@ fn type_one_layer(
         }
         ExprKind::BinOp(BinOp::ListAppend, l, r) => {
             let l_ty = l.get_type()?;
-            match &*l_ty.as_whnf() {
+            match &*l_ty.kind() {
                 ValueKind::AppliedBuiltin(BuiltinClosure {
                     b: Builtin::List,
                     ..
@@ -418,14 +416,14 @@ fn type_one_layer(
         }
         ExprKind::Merge(record, union, type_annot) => {
             let record_type = record.get_type()?;
-            let record_borrow = record_type.as_whnf();
+            let record_borrow = record_type.kind();
             let handlers = match &*record_borrow {
                 ValueKind::RecordType(kts) => kts,
                 _ => return mkerr("Merge1ArgMustBeRecord"),
             };
 
             let union_type = union.get_type()?;
-            let union_borrow = union_type.as_whnf();
+            let union_borrow = union_type.kind();
             let variants = match &*union_borrow {
                 ValueKind::UnionType(kts) => Cow::Borrowed(kts),
                 ValueKind::AppliedBuiltin(BuiltinClosure {
@@ -447,7 +445,7 @@ fn type_one_layer(
                 let handler_return_type = match variants.get(x) {
                     // Union alternative with type
                     Some(Some(variant_type)) => {
-                        let handler_type_borrow = handler_type.as_whnf();
+                        let handler_type_borrow = handler_type.kind();
                         match &*handler_type_borrow {
                             ValueKind::PiClosure { closure, annot, .. } => {
                                 if variant_type != annot {
@@ -498,7 +496,7 @@ fn type_one_layer(
         ExprKind::ToMap(_, _) => unimplemented!("toMap"),
         ExprKind::Projection(record, labels) => {
             let record_type = record.get_type()?;
-            let record_type_borrow = record_type.as_whnf();
+            let record_type_borrow = record_type.kind();
             let kts = match &*record_type_borrow {
                 ValueKind::RecordType(kts) => kts,
                 _ => return mkerr("ProjectionMustBeRecord"),