s/QuoteEnv/VarEnv/

3 files changed, 40 insertions, 43 deletions

diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index 30c4116..df1382b 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -4,7 +4,7 @@ use std::rc::Rc;
 
 use crate::error::{TypeError, TypeMessage};
 use crate::semantics::core::var::{AlphaVar, Binder};
-use crate::semantics::nze::{NzVar, QuoteEnv};
+use crate::semantics::nze::{NzVar, VarEnv};
 use crate::semantics::phase::normalize::{apply_any, normalize_whnf, NzEnv};
 use crate::semantics::phase::typecheck::{
     builtin_to_value, builtin_to_value_env, const_to_value,
@@ -277,21 +277,21 @@ impl Value {
         }
     }
 
-    pub fn to_tyexpr(&self, qenv: QuoteEnv) -> TyExpr {
+    pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr {
         let tye = match &*self.as_kind() {
             // ValueKind::Var(v, _w) => TyExprKind::Var(*v),
             // TODO: Only works when we don't normalize under lambdas
-            ValueKind::Var(_v, w) => TyExprKind::Var(qenv.lookup(w)),
+            ValueKind::Var(_v, w) => TyExprKind::Var(venv.lookup(w)),
             ValueKind::LamClosure {
                 binder,
                 annot,
                 closure,
             } => TyExprKind::Expr(ExprKind::Lam(
                 binder.to_label(),
-                annot.to_tyexpr(qenv),
+                annot.to_tyexpr(venv),
                 closure
-                    .apply_var(NzVar::new(qenv.size()))
-                    .to_tyexpr(qenv.insert()),
+                    .apply_var(NzVar::new(venv.size()))
+                    .to_tyexpr(venv.insert()),
             )),
             ValueKind::PiClosure {
                 binder,
@@ -299,10 +299,10 @@ impl Value {
                 closure,
             } => TyExprKind::Expr(ExprKind::Pi(
                 binder.to_label(),
-                annot.to_tyexpr(qenv),
+                annot.to_tyexpr(venv),
                 closure
-                    .apply_var(NzVar::new(qenv.size()))
-                    .to_tyexpr(qenv.insert()),
+                    .apply_var(NzVar::new(venv.size()))
+                    .to_tyexpr(venv.insert()),
             )),
             ValueKind::AppliedBuiltin(b, args, types, _) => {
                 TyExprKind::Expr(args.into_iter().zip(types.into_iter()).fold(
@@ -314,7 +314,7 @@ impl Value {
                                 Some(ty.clone()),
                                 Span::Artificial,
                             ),
-                            v.to_tyexpr(qenv),
+                            v.to_tyexpr(venv),
                         )
                     },
                 ))
@@ -327,7 +327,7 @@ impl Value {
                                 .map(|(k, v)| {
                                     (
                                         k.clone(),
-                                        v.as_ref().map(|v| v.to_tyexpr(qenv)),
+                                        v.as_ref().map(|v| v.to_tyexpr(venv)),
                                     )
                                 })
                                 .collect(),
@@ -349,7 +349,7 @@ impl Value {
                                             (
                                                 k.clone(),
                                                 v.as_ref()
-                                                    .map(|v| v.to_tyexpr(qenv)),
+                                                    .map(|v| v.to_tyexpr(venv)),
                                             )
                                         })
                                         .collect(),
@@ -362,14 +362,14 @@ impl Value {
                         Some(ctort.clone()),
                         Span::Artificial,
                     ),
-                    v.to_tyexpr(qenv),
+                    v.to_tyexpr(venv),
                 ))
             }
             self_kind => {
                 let self_kind = self_kind
                     .map_ref_with_special_handling_of_binders(
-                        |v| v.to_tyexpr(qenv),
-                        |_, _, v| v.to_tyexpr(qenv.insert()),
+                        |v| v.to_tyexpr(venv),
+                        |_, _, v| v.to_tyexpr(venv.insert()),
                     );
                 let expr = match self_kind {
                     ValueKind::Var(..)
@@ -384,14 +384,14 @@ impl Value {
                     ValueKind::IntegerLit(n) => ExprKind::IntegerLit(n),
                     ValueKind::DoubleLit(n) => ExprKind::DoubleLit(n),
                     ValueKind::EmptyOptionalLit(n) => ExprKind::App(
-                        builtin_to_value(Builtin::OptionalNone).to_tyexpr(qenv),
+                        builtin_to_value(Builtin::OptionalNone).to_tyexpr(venv),
                         n,
                     ),
                     ValueKind::NEOptionalLit(n) => ExprKind::SomeLit(n),
                     ValueKind::EmptyListLit(n) => {
                         ExprKind::EmptyListLit(TyExpr::new(
                             TyExprKind::Expr(ExprKind::App(
-                                builtin_to_value(Builtin::List).to_tyexpr(qenv),
+                                builtin_to_value(Builtin::List).to_tyexpr(venv),
                                 n,
                             )),
                             Some(const_to_value(Const::Type)),
@@ -425,7 +425,7 @@ impl Value {
         TyExpr::new(tye, self_ty, self_span)
     }
     pub fn to_tyexpr_noenv(&self) -> TyExpr {
-        self.to_tyexpr(QuoteEnv::new())
+        self.to_tyexpr(VarEnv::new())
     }
 }
 
diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs
index 7263cac..87d0269 100644
--- a/dhall/src/semantics/nze/nzexpr.rs
+++ b/dhall/src/semantics/nze/nzexpr.rs
@@ -9,7 +9,7 @@ pub(crate) struct NameEnv {
 }
 
 #[derive(Debug, Clone, Copy)]
-pub(crate) struct QuoteEnv {
+pub(crate) struct VarEnv {
     size: usize,
 }
 
@@ -30,8 +30,8 @@ impl NameEnv {
             names: names.collect(),
         }
     }
-    pub fn as_quoteenv(&self) -> QuoteEnv {
-        QuoteEnv {
+    pub fn as_varenv(&self) -> VarEnv {
+        VarEnv {
             size: self.names.len(),
         }
     }
@@ -72,16 +72,15 @@ impl NameEnv {
     }
 }
 
-// TODO: rename to VarEnv
-impl QuoteEnv {
+impl VarEnv {
     pub fn new() -> Self {
-        QuoteEnv { size: 0 }
+        VarEnv { size: 0 }
     }
     pub fn size(&self) -> usize {
         self.size
     }
     pub fn insert(&self) -> Self {
-        QuoteEnv {
+        VarEnv {
             size: self.size + 1,
         }
     }
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 99eb31f..7a225f7 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -3,7 +3,7 @@ use std::cmp::max;
 use std::collections::HashMap;
 
 use crate::error::{TypeError, TypeMessage};
-use crate::semantics::nze::{NameEnv, NzVar, QuoteEnv};
+use crate::semantics::nze::{NameEnv, NzVar, VarEnv};
 use crate::semantics::phase::normalize::{merge_maps, NzEnv};
 use crate::semantics::phase::typecheck::{
     builtin_to_value, const_to_value, type_of_builtin,
@@ -39,8 +39,8 @@ impl TyEnv {
             items: items.clone(),
         }
     }
-    pub fn as_quoteenv(&self) -> QuoteEnv {
-        self.names.as_quoteenv()
+    pub fn as_varenv(&self) -> VarEnv {
+        self.names.as_varenv()
     }
     pub fn as_nzenv(&self) -> &NzEnv {
         &self.items
@@ -194,7 +194,7 @@ fn type_one_layer(
 
             let ty = type_of_recordtype(
                 kts.iter()
-                    .map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_quoteenv()))),
+                    .map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_varenv()))),
             )?;
             Value::from_kind_and_type(ValueKind::RecordType(kts), ty)
         }
@@ -282,13 +282,13 @@ fn type_one_layer(
                 return mkerr(format!(
                     "annot mismatch: ({} : {}) : {}",
                     x.to_expr_tyenv(env),
-                    x_ty.to_tyexpr(env.as_quoteenv()).to_expr_tyenv(env),
-                    t.to_tyexpr(env.as_quoteenv()).to_expr_tyenv(env)
+                    x_ty.to_tyexpr(env.as_varenv()).to_expr_tyenv(env),
+                    t.to_tyexpr(env.as_varenv()).to_expr_tyenv(env)
                 ));
                 // return mkerr(format!(
                 //     "annot mismatch: {} != {}",
-                //     x_ty.to_tyexpr(env.as_quoteenv()).to_expr_tyenv(env),
-                //     t.to_tyexpr(env.as_quoteenv()).to_expr_tyenv(env)
+                //     x_ty.to_tyexpr(env.as_varenv()).to_expr_tyenv(env),
+                //     t.to_tyexpr(env.as_varenv()).to_expr_tyenv(env)
                 // ));
                 // return mkerr(format!("annot mismatch: {:#?} : {:#?}", x, t,));
             }
@@ -314,11 +314,9 @@ fn type_one_layer(
                             "function annot mismatch: ({} : {}) : {}",
                             arg.to_expr_tyenv(env),
                             arg.get_type()?
-                                .to_tyexpr(env.as_quoteenv())
-                                .to_expr_tyenv(env),
-                            annot
-                                .to_tyexpr(env.as_quoteenv())
+                                .to_tyexpr(env.as_varenv())
                                 .to_expr_tyenv(env),
+                            annot.to_tyexpr(env.as_varenv()).to_expr_tyenv(env),
                         ));
                     }
 
@@ -373,15 +371,15 @@ fn type_one_layer(
             // Construct the final record type
             let ty = type_of_recordtype(
                 kts.iter()
-                    .map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_quoteenv()))),
+                    .map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_varenv()))),
             )?;
             Value::from_kind_and_type(ValueKind::RecordType(kts), ty)
         }
         ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => {
             let ekind = ExprKind::BinOp(
                 BinOp::RecursiveRecordTypeMerge,
-                x.get_type()?.to_tyexpr(env.as_quoteenv()),
-                y.get_type()?.to_tyexpr(env.as_quoteenv()),
+                x.get_type()?.to_tyexpr(env.as_varenv()),
+                y.get_type()?.to_tyexpr(env.as_varenv()),
             );
             let ty = type_one_layer(env, &ekind)?;
             TyExpr::new(TyExprKind::Expr(ekind), Some(ty), Span::Artificial)
@@ -406,8 +404,8 @@ fn type_one_layer(
                         env,
                         &ExprKind::BinOp(
                             BinOp::RecursiveRecordTypeMerge,
-                            tx.to_tyexpr(env.as_quoteenv()),
-                            ty.to_tyexpr(env.as_quoteenv()),
+                            tx.to_tyexpr(env.as_varenv()),
+                            ty.to_tyexpr(env.as_varenv()),
                         ),
                     )?;
                 }
@@ -613,7 +611,7 @@ pub(crate) fn type_with(
                 TyExprKind::Expr(ExprKind::Pi(
                     binder.clone(),
                     annot.clone(),
-                    body_ty.to_tyexpr(body_env.as_quoteenv()),
+                    body_ty.to_tyexpr(body_env.as_varenv()),
                 )),
                 Some(type_of_function(annot.get_type()?, body_ty.get_type()?)?),
                 Span::Artificial,