summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/tck
diff options
context:
space:
mode:
authorNadrieril2020-01-30 11:09:39 +0000
committerNadrieril2020-01-30 11:14:49 +0000
commit655f67fb29ca847f86c3e19338757e7b031d4f50 (patch)
treec7e7f73a1830cf254d04be485ac861880949d707 /dhall/src/semantics/tck
parenta928c3c4f51d87fd942e8a81727962c00abf6808 (diff)
Move builtins-related code to its own module
Diffstat (limited to 'dhall/src/semantics/tck')
-rw-r--r--dhall/src/semantics/tck/mod.rs2
-rw-r--r--dhall/src/semantics/tck/tyexpr.rs3
-rw-r--r--dhall/src/semantics/tck/typecheck.rs22
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