From 655f67fb29ca847f86c3e19338757e7b031d4f50 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 30 Jan 2020 11:09:39 +0000
Subject: Move builtins-related code to its own module

---
 dhall/src/semantics/tck/mod.rs       |  2 +-
 dhall/src/semantics/tck/tyexpr.rs    |  3 +--
 dhall/src/semantics/tck/typecheck.rs | 22 ++++++++++------------
 3 files changed, 12 insertions(+), 15 deletions(-)

(limited to 'dhall/src/semantics/tck')

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
-- 
cgit v1.2.3