diff options
Diffstat (limited to 'dhall/src/semantics/tck')
| -rw-r--r-- | dhall/src/semantics/tck/mod.rs | 2 | ||||
| -rw-r--r-- | dhall/src/semantics/tck/tyexpr.rs | 3 | ||||
| -rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 22 |
3 files changed, 12 insertions, 15 deletions
diff --git a/dhall/src/semantics/tck/mod.rs b/dhall/src/semantics/tck/mod.rs index 28974af..1df2a48 100644 --- a/dhall/src/semantics/tck/mod.rs +++ b/dhall/src/semantics/tck/mod.rs @@ -1,6 +1,6 @@ -pub mod context; pub mod env; pub mod tyexpr; pub mod typecheck; pub(crate) use env::*; pub(crate) use tyexpr::*; +pub(crate) use typecheck::*; diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs index 114bb14..bf7c130 100644 --- a/dhall/src/semantics/tck/tyexpr.rs +++ b/dhall/src/semantics/tck/tyexpr.rs @@ -1,9 +1,8 @@ use crate::error::{TypeError, TypeMessage}; use crate::semantics::phase::normalize::normalize_tyexpr_whnf; -use crate::semantics::phase::typecheck::rc; use crate::semantics::phase::Normalized; use crate::semantics::phase::{NormalizedExpr, ToExprOptions}; -use crate::semantics::{NameEnv, NzEnv, TyEnv, Value}; +use crate::semantics::{rc, NameEnv, NzEnv, TyEnv, Value}; use crate::syntax::{ExprKind, Span, V}; pub(crate) type Type = Value; diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 789105f..22ba72d 100644 --- a/dhall/src/semantics/tck/typecheck.rs +++ b/dhall/src/semantics/tck/typecheck.rs @@ -4,12 +4,10 @@ use std::collections::HashMap; use crate::error::{TypeError, TypeMessage}; 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, NzVar, TyEnv, TyExpr, TyExprKind, Type, Value, ValueKind, + type_of_builtin, Binder, Closure, NzVar, TyEnv, TyExpr, TyExprKind, Type, + Value, ValueKind, }; use crate::syntax; use crate::syntax::{ @@ -72,19 +70,19 @@ fn type_one_layer( | ExprKind::Const(Const::Sort) | ExprKind::Embed(..) => unreachable!(), // Handled in type_with - ExprKind::Const(Const::Type) => const_to_value(Const::Kind), - ExprKind::Const(Const::Kind) => const_to_value(Const::Sort), + ExprKind::Const(Const::Type) => Value::from_const(Const::Kind), + ExprKind::Const(Const::Kind) => Value::from_const(Const::Sort), ExprKind::Builtin(b) => { let t_expr = type_of_builtin(*b); let t_tyexpr = type_with(env, &t_expr)?; t_tyexpr.normalize_whnf(env.as_nzenv()) } - ExprKind::BoolLit(_) => builtin_to_value(Builtin::Bool), - ExprKind::NaturalLit(_) => builtin_to_value(Builtin::Natural), - ExprKind::IntegerLit(_) => builtin_to_value(Builtin::Integer), - ExprKind::DoubleLit(_) => builtin_to_value(Builtin::Double), + ExprKind::BoolLit(_) => Value::from_builtin(Builtin::Bool), + ExprKind::NaturalLit(_) => Value::from_builtin(Builtin::Natural), + ExprKind::IntegerLit(_) => Value::from_builtin(Builtin::Integer), + ExprKind::DoubleLit(_) => Value::from_builtin(Builtin::Double), ExprKind::TextLit(interpolated) => { - let text_type = builtin_to_value(Builtin::Text); + let text_type = Value::from_builtin(Builtin::Text); for contents in interpolated.iter() { use InterpolatedTextContents::Expr; if let Expr(x) = contents { @@ -388,7 +386,7 @@ fn type_one_layer( Value::from_const(Const::Type) } ExprKind::BinOp(o, l, r) => { - let t = builtin_to_value(match o { + let t = Value::from_builtin(match o { BinOp::BoolAnd | BinOp::BoolOr | BinOp::BoolEQ |