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/core/value.rs | 36 ++++++++++++++++++------------------ dhall/src/semantics/nze/nzexpr.rs | 13 ++++++------- dhall/src/semantics/tck/typecheck.rs | 34 ++++++++++++++++------------------ 3 files changed, 40 insertions(+), 43 deletions(-) (limited to 'dhall') 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, -- cgit v1.2.3