Naming tweaks

4 files changed, 33 insertions, 41 deletions

diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index f897f16..5055ac2 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -8,7 +8,7 @@ use crate::core::context::TypecheckContext;
 use crate::core::valuef::ValueF;
 use crate::core::var::{AlphaVar, Shift, Subst};
 use crate::error::{TypeError, TypeMessage};
-use crate::phase::normalize::{apply_any, normalize_whnf, OutputSubExpr};
+use crate::phase::normalize::{apply_any, normalize_whnf};
 use crate::phase::typecheck::{builtin_to_value, const_to_value};
 use crate::phase::{NormalizedSubExpr, Typed};
 
@@ -208,11 +208,11 @@ impl Value {
     pub(crate) fn normalize_to_expr_maybe_alpha(
         &self,
         alpha: bool,
-    ) -> OutputSubExpr {
+    ) -> NormalizedSubExpr {
         self.as_nf().normalize_to_expr_maybe_alpha(alpha)
     }
 
-    pub(crate) fn app_value(&self, th: Value) -> ValueF {
+    pub(crate) fn app(&self, th: Value) -> ValueF {
         apply_any(self.clone(), th)
     }
 
diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs
index da03cbd..e9049c7 100644
--- a/dhall/src/core/valuef.rs
+++ b/dhall/src/core/valuef.rs
@@ -7,8 +7,7 @@ use dhall_syntax::{
 
 use crate::core::value::Value;
 use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
-use crate::phase::normalize::OutputSubExpr;
-use crate::phase::Normalized;
+use crate::phase::{Normalized, NormalizedSubExpr};
 
 /// A semantic value. Subexpressions are Values, which are partially evaluated expressions that are
 /// normalized on-demand.
@@ -59,7 +58,7 @@ impl ValueF {
     }
 
     /// Convert the value to a fully normalized syntactic expression
-    pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr {
+    pub(crate) fn normalize_to_expr(&self) -> NormalizedSubExpr {
         self.normalize_to_expr_maybe_alpha(false)
     }
     /// Convert the value to a fully normalized syntactic expression. Also alpha-normalize
@@ -67,7 +66,7 @@ impl ValueF {
     pub(crate) fn normalize_to_expr_maybe_alpha(
         &self,
         alpha: bool,
-    ) -> OutputSubExpr {
+    ) -> NormalizedSubExpr {
         match self {
             ValueF::Lam(x, t, e) => rc(ExprF::Lam(
                 x.to_label_maybe_alpha(alpha),
@@ -258,8 +257,8 @@ impl ValueF {
     }
 
     /// Apply to a value
-    pub fn app_value(self, th: Value) -> ValueF {
-        Value::from_valuef_untyped(self).app_value(th)
+    pub fn app(self, th: Value) -> ValueF {
+        Value::from_valuef_untyped(self).app(th)
     }
 
     pub fn from_builtin(b: Builtin) -> ValueF {
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index f943171..afc2e7f 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -8,9 +8,7 @@ use dhall_syntax::{
 use crate::core::value::Value;
 use crate::core::valuef::ValueF;
 use crate::core::var::{Shift, Subst};
-use crate::phase::{Normalized, NormalizedSubExpr};
-
-pub(crate) type OutputSubExpr = NormalizedSubExpr;
+use crate::phase::Normalized;
 
 // Ad-hoc macro to help construct closures
 macro_rules! make_closure {
@@ -35,7 +33,7 @@ macro_rules! make_closure {
     };
     (List $($rest:tt)*) => {
         Value::from_builtin(Builtin::List)
-            .app_value(make_closure!($($rest)*))
+            .app(make_closure!($($rest)*))
             .into_value_simple_type()
     };
     (Some($($rest:tt)*)) => {
@@ -229,12 +227,12 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
             }
             _ => {
                 let list_t = Value::from_builtin(List)
-                    .app_value(t.clone())
+                    .app(t.clone())
                     .into_value_simple_type();
                 Ok((
                     r,
-                    f.app_value(list_t.clone())
-                        .app_value({
+                    f.app(list_t.clone())
+                        .app({
                             // Move `t` under new `x` variable
                             let t1 = t.under_binder(Label::from("x"));
                             make_closure!(
@@ -243,7 +241,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
                                 [ var(x, 1) ] # var(xs, 0)
                             )
                         })
-                        .app_value(
+                        .app(
                             EmptyListLit(t.clone())
                                 .into_value_with_type(list_t),
                         ),
@@ -255,11 +253,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
             NEListLit(xs) => {
                 let mut v = nil.clone();
                 for x in xs.iter().rev() {
-                    v = cons
-                        .clone()
-                        .app_value(x.clone())
-                        .app_value(v)
-                        .into_value_untyped();
+                    v = cons.clone().app(x.clone()).app(v).into_value_untyped();
                 }
                 Ok((r, v.to_whnf()))
             }
@@ -277,13 +271,13 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
             }
             _ => {
                 let optional_t = Value::from_builtin(Optional)
-                    .app_value(t.clone())
+                    .app(t.clone())
                     .into_value_simple_type();
                 Ok((
                     r,
-                    f.app_value(optional_t.clone())
-                        .app_value(make_closure!(λ(x: #t) -> Some(var(x, 0))))
-                        .app_value(
+                    f.app(optional_t.clone())
+                        .app(make_closure!(λ(x: #t) -> Some(var(x, 0))))
+                        .app(
                             EmptyOptionalLit(t.clone())
                                 .into_value_with_type(optional_t),
                         ),
@@ -292,7 +286,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
         },
         (OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_whnf() {
             EmptyOptionalLit(_) => Ok((r, nothing.to_whnf())),
-            NEOptionalLit(x) => Ok((r, just.app_value(x.clone()))),
+            NEOptionalLit(x) => Ok((r, just.app(x.clone()))),
             _ => Err(()),
         },
         (NaturalBuild, [f, r..]) => match &*f.as_whnf() {
@@ -307,9 +301,9 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
             }
             _ => Ok((
                 r,
-                f.app_value(Value::from_builtin(Natural))
-                    .app_value(make_closure!(λ(x : Natural) -> 1 + var(x, 0)))
-                    .app_value(
+                f.app(Value::from_builtin(Natural))
+                    .app(make_closure!(λ(x : Natural) -> 1 + var(x, 0)))
+                    .app(
                         NaturalLit(0)
                             .into_value_with_type(Value::from_builtin(Natural)),
                     ),
@@ -319,15 +313,15 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
             NaturalLit(0) => Ok((r, zero.to_whnf())),
             NaturalLit(n) => {
                 let fold = Value::from_builtin(NaturalFold)
-                    .app_value(
+                    .app(
                         NaturalLit(n - 1)
                             .into_value_with_type(Value::from_builtin(Natural)),
                     )
-                    .app_value(t.clone())
-                    .app_value(succ.clone())
-                    .app_value(zero.clone())
+                    .app(t.clone())
+                    .app(succ.clone())
+                    .app(zero.clone())
                     .into_value_with_type(t.clone());
-                Ok((r, succ.app_value(fold)))
+                Ok((r, succ.app(fold)))
             }
             _ => Err(()),
         },
@@ -337,7 +331,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
         Ok((unconsumed_args, mut v)) => {
             let n_consumed_args = args.len() - unconsumed_args.len();
             for x in args.into_iter().skip(n_consumed_args) {
-                v = v.app_value(x);
+                v = v.app(x);
             }
             v
         }
@@ -621,7 +615,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
         ExprF::Lam(x, t, e) => Ret::ValueF(Lam(x.into(), t, e)),
         ExprF::Pi(x, t, e) => Ret::ValueF(Pi(x.into(), t, e)),
         ExprF::Let(x, _, v, b) => Ret::Value(b.subst_shift(&x.into(), &v)),
-        ExprF::App(v, a) => Ret::ValueF(v.app_value(a)),
+        ExprF::App(v, a) => Ret::ValueF(v.app(a)),
         ExprF::Builtin(b) => Ret::ValueF(ValueF::from_builtin(b)),
         ExprF::Const(c) => Ret::ValueF(ValueF::Const(c)),
         ExprF::BoolLit(b) => Ret::ValueF(BoolLit(b)),
@@ -743,7 +737,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
                     }
                 },
                 (RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) {
-                    Some(h) => Ret::ValueF(h.app_value(v.clone())),
+                    Some(h) => Ret::ValueF(h.app(v.clone())),
                     None => {
                         drop(handlers_borrow);
                         drop(variant_borrow);
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 1ea87d1..440d694 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -457,7 +457,7 @@ fn type_last_layer(
 
             RetTypeOnly(Value::from_valuef_and_type(
                 ValueF::from_builtin(dhall_syntax::Builtin::List)
-                    .app_value(t.into_owned()),
+                    .app(t.into_owned()),
                 Value::from_const(Type),
             ))
         }
@@ -468,8 +468,7 @@ fn type_last_layer(
             }
 
             RetTypeOnly(Value::from_valuef_and_type(
-                ValueF::from_builtin(dhall_syntax::Builtin::Optional)
-                    .app_value(t),
+                ValueF::from_builtin(dhall_syntax::Builtin::Optional).app(t),
                 Value::from_const(Type),
             ))
         }