summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/tck/typecheck.rs
diff options
context:
space:
mode:
authorNadrieril2020-01-29 21:56:52 +0000
committerNadrieril2020-01-29 21:56:52 +0000
commit489174a426e6057a68b6edd2e9b4387d09912a25 (patch)
treedc73718183a78548ef018e5dc0ac040d09f15c19 /dhall/src/semantics/tck/typecheck.rs
parent280b3174476ef8fe5a98f3614f4fe253fa243d8c (diff)
Move envs to their own files
Diffstat (limited to 'dhall/src/semantics/tck/typecheck.rs')
-rw-r--r--dhall/src/semantics/tck/typecheck.rs58
1 files changed, 3 insertions, 55 deletions
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 7a225f7..789105f 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -3,71 +3,19 @@ use std::cmp::max;
use std::collections::HashMap;
use crate::error::{TypeError, TypeMessage};
-use crate::semantics::nze::{NameEnv, NzVar, VarEnv};
-use crate::semantics::phase::normalize::{merge_maps, NzEnv};
+use crate::semantics::phase::normalize::merge_maps;
use crate::semantics::phase::typecheck::{
builtin_to_value, const_to_value, type_of_builtin,
};
use crate::semantics::phase::Normalized;
use crate::semantics::{
- Binder, Closure, TyExpr, TyExprKind, Type, Value, ValueKind,
+ Binder, Closure, NzVar, TyEnv, TyExpr, TyExprKind, Type, Value, ValueKind,
};
use crate::syntax;
use crate::syntax::{
- BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label,
- Span, V,
+ BinOp, Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Span,
};
-#[derive(Debug, Clone)]
-pub(crate) struct TyEnv {
- names: NameEnv,
- items: NzEnv,
-}
-
-impl TyEnv {
- pub fn new() -> Self {
- TyEnv {
- names: NameEnv::new(),
- items: NzEnv::new(),
- }
- }
- pub fn from_nzenv_alpha(items: &NzEnv) -> Self {
- TyEnv {
- names: NameEnv::from_binders(
- std::iter::repeat("_".into()).take(items.size()),
- ),
- items: items.clone(),
- }
- }
- pub fn as_varenv(&self) -> VarEnv {
- self.names.as_varenv()
- }
- pub fn as_nzenv(&self) -> &NzEnv {
- &self.items
- }
- pub fn as_nameenv(&self) -> &NameEnv {
- &self.names
- }
-
- pub fn insert_type(&self, x: &Label, t: Type) -> Self {
- TyEnv {
- names: self.names.insert(x),
- items: self.items.insert_type(t),
- }
- }
- pub fn insert_value(&self, x: &Label, e: Value) -> Self {
- TyEnv {
- names: self.names.insert(x),
- items: self.items.insert_value(e),
- }
- }
- pub fn lookup(&self, var: &V<Label>) -> Option<(TyExprKind, Type)> {
- let var = self.names.unlabel_var(var)?;
- let ty = self.items.lookup_val(&var).get_type().unwrap();
- Some((TyExprKind::Var(var), ty))
- }
-}
-
fn type_of_recordtype<'a>(
tys: impl Iterator<Item = Cow<'a, TyExpr>>,
) -> Result<Type, TypeError> {