From 38a82c53ef45e802cf5816a8afcbf36a69c91174 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 20 Aug 2019 14:12:27 +0200
Subject: Clarify conversion of Const/Builtin to Value

---
 dhall/src/core/value.rs      |  7 ++-----
 dhall/src/phase/typecheck.rs | 43 +++++++++++++++++++++++++++----------------
 2 files changed, 29 insertions(+), 21 deletions(-)

(limited to 'dhall/src')

diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 0af7c8c..5367c86 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -9,7 +9,7 @@ use crate::core::valuef::ValueF;
 use crate::core::var::{AlphaVar, Shift, Subst};
 use crate::error::{TypeError, TypeMessage};
 use crate::phase::normalize::{apply_any, normalize_whnf, OutputSubExpr};
-use crate::phase::typecheck::type_of_const;
+use crate::phase::typecheck::const_to_value;
 use crate::phase::{NormalizedSubExpr, Typed};
 
 #[derive(Debug, Clone, Copy)]
@@ -110,10 +110,7 @@ impl Value {
         Value::from_valuef_and_type(v, Value::from_const(Const::Type))
     }
     pub(crate) fn from_const(c: Const) -> Self {
-        match type_of_const(c) {
-            Ok(t) => Value::from_valuef_and_type(ValueF::Const(c), t),
-            Err(_) => Value::from_valuef_untyped(ValueF::Const(c)),
-        }
+        const_to_value(c)
     }
     pub fn const_type() -> Self {
         Value::from_const(Const::Type)
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index c47eb78..1ea87d1 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -129,16 +129,24 @@ fn function_check(a: Const, b: Const) -> Const {
     }
 }
 
-pub(crate) fn type_of_const(c: Const) -> Result<Value, TypeError> {
+fn type_of_const(c: Const) -> Result<Value, TypeError> {
     match c {
-        Const::Type => Ok(Value::from_const(Const::Kind)),
-        Const::Kind => Ok(Value::from_const(Const::Sort)),
+        Const::Type => Ok(const_to_value(Const::Kind)),
+        Const::Kind => Ok(const_to_value(Const::Sort)),
         Const::Sort => {
             Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort))
         }
     }
 }
 
+pub(crate) fn const_to_value(c: Const) -> Value {
+    let v = ValueF::Const(c);
+    match type_of_const(c) {
+        Ok(t) => Value::from_valuef_and_type(v, t),
+        Err(_) => Value::from_valuef_untyped(v),
+    }
+}
+
 // Ad-hoc macro to help construct the types of builtins
 macro_rules! make_type {
     (Type) => { ExprF::Const(Const::Type) };
@@ -280,9 +288,12 @@ fn type_of_builtin<E>(b: Builtin) -> Expr<E> {
     }
 }
 
-// TODO: this can't fail in practise
-pub(crate) fn builtin_to_type(b: Builtin) -> Result<Value, TypeError> {
-    type_with(&TypecheckContext::new(), SubExpr::from_builtin(b))
+pub(crate) fn builtin_to_value(b: Builtin) -> Value {
+    let ctx = TypecheckContext::new();
+    Value::from_valuef_and_type(
+        ValueF::PartialExpr(ExprF::Builtin(b)),
+        type_with(&ctx, rc(type_of_builtin(b))).unwrap(),
+    )
 }
 
 /// Type-check an expression and return the expression alongside its type if type-checking
@@ -401,7 +412,7 @@ fn type_last_layer(
             RetTypeOnly(t.clone())
         }
         BoolIf(x, y, z) => {
-            if x.get_type()?.as_ref() != &builtin_to_type(Bool)? {
+            if x.get_type()?.as_ref() != &builtin_to_value(Bool) {
                 return mkerr(InvalidPredicate(x.clone()));
             }
 
@@ -523,14 +534,14 @@ fn type_last_layer(
                 // )),
             }
         }
-        Const(c) => RetWhole(Value::from_const(*c)),
-        Builtin(b) => RetTypeOnly(type_with(ctx, rc(type_of_builtin(*b)))?),
-        BoolLit(_) => RetTypeOnly(builtin_to_type(Bool)?),
-        NaturalLit(_) => RetTypeOnly(builtin_to_type(Natural)?),
-        IntegerLit(_) => RetTypeOnly(builtin_to_type(Integer)?),
-        DoubleLit(_) => RetTypeOnly(builtin_to_type(Double)?),
+        Const(c) => RetWhole(const_to_value(*c)),
+        Builtin(b) => RetWhole(builtin_to_value(*b)),
+        BoolLit(_) => RetTypeOnly(builtin_to_value(Bool)),
+        NaturalLit(_) => RetTypeOnly(builtin_to_value(Natural)),
+        IntegerLit(_) => RetTypeOnly(builtin_to_value(Integer)),
+        DoubleLit(_) => RetTypeOnly(builtin_to_value(Double)),
         TextLit(interpolated) => {
-            let text_type = builtin_to_type(Text)?;
+            let text_type = builtin_to_value(Text);
             for contents in interpolated.iter() {
                 use InterpolatedTextContents::Expr;
                 if let Expr(x) = contents {
@@ -665,7 +676,7 @@ fn type_last_layer(
             RetTypeOnly(Value::from_const(Type))
         }
         BinOp(o, l, r) => {
-            let t = builtin_to_type(match o {
+            let t = builtin_to_value(match o {
                 BoolAnd => Bool,
                 BoolOr => Bool,
                 BoolEQ => Bool,
@@ -679,7 +690,7 @@ fn type_last_layer(
                 RecursiveRecordTypeMerge => unreachable!(),
                 ImportAlt => unreachable!("There should remain no import alternatives in a resolved expression"),
                 Equivalence => unreachable!(),
-            })?;
+            });
 
             if l.get_type()?.as_ref() != &t {
                 return mkerr(BinOpTypeMismatch(*o, l.clone()));
-- 
cgit v1.2.3