From 22bec94618454f57773716870f5624579ab712ce Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Wed, 29 Jan 2020 21:31:53 +0000
Subject: s/QuoteEnv/VarEnv/

---
 dhall/src/semantics/tck/typecheck.rs | 34 ++++++++++++++++------------------
 1 file changed, 16 insertions(+), 18 deletions(-)

(limited to 'dhall/src/semantics/tck')

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,
-- 
cgit v1.2.3