From b72f0968ac19058b9cc513ab0ed1785133232a3d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 24 Jan 2020 21:33:21 +0000 Subject: Implement basic typecheck with new approach --- dhall/src/semantics/tck/typecheck.rs | 147 +++++++++++++++++++++++++++++++++++ 1 file changed, 147 insertions(+) create mode 100644 dhall/src/semantics/tck/typecheck.rs (limited to 'dhall/src/semantics/tck') diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs new file mode 100644 index 0000000..aab5f83 --- /dev/null +++ b/dhall/src/semantics/tck/typecheck.rs @@ -0,0 +1,147 @@ +#![allow(dead_code)] +#![allow(unused_variables)] +#![allow(unreachable_code)] +#![allow(unused_imports)] +use std::borrow::Cow; +use std::cmp::max; +use std::collections::HashMap; + +use crate::error::{TypeError, TypeMessage}; +use crate::semantics::core::context::TyCtx; +use crate::semantics::nze::{NameEnv, QuoteEnv}; +use crate::semantics::phase::normalize::{merge_maps, NzEnv}; +use crate::semantics::phase::Normalized; +use crate::semantics::{ + AlphaVar, Binder, Closure, TyExpr, TyExprKind, Type, Value, ValueKind, +}; +use crate::syntax; +use crate::syntax::{ + Builtin, Const, Expr, ExprKind, InterpolatedTextContents, Label, Span, + UnspannedExpr, V, +}; + +#[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 as_quoteenv(&self) -> QuoteEnv { + self.names.as_quoteenv() + } + pub fn as_nzenv(&self) -> &NzEnv { + &self.items + } + pub fn as_nameenv(&self) -> &NameEnv { + &self.names + } + + pub fn insert_type(&self, x: &Label, t: Value) -> 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_var(&self, var: &V