From 07a276c1d6ee892b93abbd7a73c78c96d56f4fe7 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 19 Aug 2019 22:26:17 +0200
Subject: Reduce untyped construction of Values

---
 dhall/src/core/context.rs | 34 +++++++++---------------
 dhall/src/core/value.rs   | 68 +++++++++++++++++++----------------------------
 dhall/src/core/valuef.rs  | 14 +++++++---
 3 files changed, 51 insertions(+), 65 deletions(-)

(limited to 'dhall/src/core')

diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs
index 851e4c4..deabe44 100644
--- a/dhall/src/core/context.rs
+++ b/dhall/src/core/context.rs
@@ -3,7 +3,7 @@ use std::rc::Rc;
 
 use dhall_syntax::{Label, V};
 
-use crate::core::value::{TypedValue, Value};
+use crate::core::value::TypedValue;
 use crate::core::valuef::ValueF;
 use crate::core::var::{AlphaVar, Shift, Subst};
 use crate::error::TypeError;
@@ -11,7 +11,7 @@ use crate::error::TypeError;
 #[derive(Debug, Clone)]
 enum CtxItem {
     Kept(AlphaVar, TypedValue),
-    Replaced(Value, TypedValue),
+    Replaced(TypedValue),
 }
 
 #[derive(Debug, Clone)]
@@ -32,10 +32,7 @@ impl TypecheckContext {
         e: TypedValue,
     ) -> Result<Self, TypeError> {
         let mut vec = self.0.as_ref().clone();
-        vec.push((
-            x.clone(),
-            CtxItem::Replaced(e.to_value(), e.get_type()?.into_owned()),
-        ));
+        vec.push((x.clone(), CtxItem::Replaced(e)));
         Ok(TypecheckContext(Rc::new(vec)))
     }
     pub fn lookup(&self, var: &V<Label>) -> Option<TypedValue> {
@@ -45,13 +42,15 @@ impl TypecheckContext {
             match var.over_binder(l) {
                 None => {
                     let i = i.under_multiple_binders(&shift_map);
-                    let (th, t) = match i {
+                    return Some(match i {
                         CtxItem::Kept(newvar, t) => {
-                            (ValueF::Var(newvar).into_value(), t)
+                            TypedValue::from_valuef_and_type(
+                                ValueF::Var(newvar),
+                                t,
+                            )
                         }
-                        CtxItem::Replaced(th, t) => (th, t),
-                    };
-                    return Some(TypedValue::from_value_and_type(th, t));
+                        CtxItem::Replaced(v) => v,
+                    });
                 }
                 Some(newvar) => var = newvar,
             };
@@ -114,9 +113,7 @@ impl Shift for CtxItem {
             CtxItem::Kept(v, t) => {
                 CtxItem::Kept(v.shift(delta, var)?, t.shift(delta, var)?)
             }
-            CtxItem::Replaced(e, t) => {
-                CtxItem::Replaced(e.shift(delta, var)?, t.shift(delta, var)?)
-            }
+            CtxItem::Replaced(e) => CtxItem::Replaced(e.shift(delta, var)?),
         })
     }
 }
@@ -130,14 +127,9 @@ impl Shift for TypecheckContext {
 impl Subst<TypedValue> for CtxItem {
     fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self {
         match self {
-            CtxItem::Replaced(e, t) => CtxItem::Replaced(
-                e.subst_shift(var, val),
-                t.subst_shift(var, val),
-            ),
+            CtxItem::Replaced(e) => CtxItem::Replaced(e.subst_shift(var, val)),
             CtxItem::Kept(v, t) => match v.shift(-1, var) {
-                None => {
-                    CtxItem::Replaced(val.to_value(), t.subst_shift(var, val))
-                }
+                None => CtxItem::Replaced(val.clone()),
                 Some(newvar) => CtxItem::Kept(newvar, t.subst_shift(var, val)),
             },
         }
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index f4cb6b6..c4e3831 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -2,7 +2,7 @@ use std::borrow::Cow;
 use std::cell::{Ref, RefCell, RefMut};
 use std::rc::Rc;
 
-use dhall_syntax::{Const, ExprF};
+use dhall_syntax::Const;
 
 use crate::core::context::TypecheckContext;
 use crate::core::valuef::ValueF;
@@ -10,7 +10,7 @@ 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::{Normalized, NormalizedSubExpr, Typed};
+use crate::phase::{NormalizedSubExpr, Typed};
 
 #[derive(Debug, Clone, Copy)]
 enum Form {
@@ -28,7 +28,7 @@ enum Form {
 }
 use Form::{Unevaled, NF, WHNF};
 
-#[derive(Debug, Clone)]
+#[derive(Debug)]
 /// Partially normalized value.
 /// Invariant: if `form` is `WHNF`, `value` must be in Weak Head Normal Form
 /// Invariant: if `form` is `NF`, `value` must be fully normalized
@@ -108,7 +108,7 @@ impl ValueInternal {
 }
 
 impl Value {
-    pub(crate) fn from_valuef(v: ValueF) -> Value {
+    pub(crate) fn from_valuef_untyped(v: ValueF) -> Value {
         ValueInternal {
             form: Unevaled,
             value: v,
@@ -124,18 +124,8 @@ impl Value {
         }
         .into_value()
     }
-    pub(crate) fn from_partial_expr(e: ExprF<Value, Normalized>) -> Value {
-        Value::from_valuef(ValueF::PartialExpr(e))
-    }
-    // TODO: avoid using this function
-    pub(crate) fn with_type(self, t: TypedValue) -> Value {
-        let vint = self.as_internal();
-        ValueInternal {
-            form: vint.form,
-            value: vint.value.clone(),
-            ty: Some(t),
-        }
-        .into_value()
+    pub(crate) fn from_valuef_simple_type(v: ValueF) -> Value {
+        Value::from_valuef_and_type(v, TypedValue::from_const(Const::Type))
     }
 
     /// Mutates the contents. If no one else shares this thunk,
@@ -214,7 +204,7 @@ impl Value {
     }
 
     pub(crate) fn app_valuef(&self, val: ValueF) -> ValueF {
-        self.app_value(val.into_value())
+        self.app_value(val.into_value_untyped())
     }
 
     pub(crate) fn app_value(&self, th: Value) -> ValueF {
@@ -227,41 +217,39 @@ impl Value {
 }
 
 impl TypedValue {
-    pub(crate) fn from_valuef(v: ValueF) -> TypedValue {
-        TypedValue::from_value_untyped(Value::from_valuef(v))
-    }
-
-    pub(crate) fn normalize_nf(&self) -> ValueF {
-        self.0.normalize_nf().clone()
-    }
-
-    pub(crate) fn normalize_to_expr_maybe_alpha(
-        &self,
-        alpha: bool,
-    ) -> OutputSubExpr {
-        self.normalize_nf().normalize_to_expr_maybe_alpha(alpha)
+    pub fn from_value(th: Value) -> Self {
+        TypedValue(th)
     }
-
-    pub(crate) fn from_value_and_type(th: Value, t: TypedValue) -> Self {
-        TypedValue(th.with_type(t))
+    pub(crate) fn from_valuef_untyped(v: ValueF) -> TypedValue {
+        TypedValue::from_value(Value::from_valuef_untyped(v))
     }
-    pub fn from_value_simple_type(th: Value) -> Self {
-        TypedValue::from_value_and_type(th, TypedValue::const_type())
+    pub(crate) fn from_valuef_and_type(v: ValueF, t: TypedValue) -> Self {
+        TypedValue(Value::from_valuef_and_type(v, t))
     }
-    pub(crate) fn from_value_untyped(th: Value) -> Self {
-        TypedValue(th)
+    // TODO: do something with the info that the type is Type. Maybe check
+    // is a type is present ?
+    pub(crate) fn from_value_simple_type(th: Value) -> Self {
+        TypedValue::from_value(th)
     }
     pub(crate) fn from_const(c: Const) -> Self {
         match type_of_const(c) {
             Ok(t) => TypedValue::from_valuef_and_type(ValueF::Const(c), t),
-            Err(_) => TypedValue::from_valuef(ValueF::Const(c)),
+            Err(_) => TypedValue::from_valuef_untyped(ValueF::Const(c)),
         }
     }
     pub fn const_type() -> Self {
         TypedValue::from_const(Const::Type)
     }
-    pub(crate) fn from_valuef_and_type(v: ValueF, t: TypedValue) -> Self {
-        TypedValue(Value::from_valuef_and_type(v, t))
+
+    pub(crate) fn normalize_nf(&self) -> ValueF {
+        self.0.normalize_nf().clone()
+    }
+
+    pub(crate) fn normalize_to_expr_maybe_alpha(
+        &self,
+        alpha: bool,
+    ) -> OutputSubExpr {
+        self.normalize_nf().normalize_to_expr_maybe_alpha(alpha)
     }
 
     /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut
diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs
index b948eb1..de55d2f 100644
--- a/dhall/src/core/valuef.rs
+++ b/dhall/src/core/valuef.rs
@@ -48,8 +48,14 @@ pub enum ValueF {
 }
 
 impl ValueF {
-    pub(crate) fn into_value(self) -> Value {
-        Value::from_valuef(self)
+    pub(crate) fn into_value_untyped(self) -> Value {
+        Value::from_valuef_untyped(self)
+    }
+    pub(crate) fn into_value_with_type(self, t: TypedValue) -> Value {
+        Value::from_valuef_and_type(self, t)
+    }
+    pub(crate) fn into_value_simple_type(self) -> Value {
+        Value::from_valuef_simple_type(self)
     }
 
     /// Convert the value to a fully normalized syntactic expression
@@ -258,12 +264,12 @@ impl ValueF {
 
     /// Apply to a value
     pub(crate) fn app_valuef(self, val: ValueF) -> ValueF {
-        self.app_value(val.into_value())
+        self.app_value(val.into_value_untyped())
     }
 
     /// Apply to a thunk
     pub fn app_value(self, th: Value) -> ValueF {
-        Value::from_valuef(self).app_value(th)
+        Value::from_valuef_untyped(self).app_value(th)
     }
 
     pub fn from_builtin(b: Builtin) -> ValueF {
-- 
cgit v1.2.3