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 ++++++---
 dhall/src/phase/normalize.rs | 72 ++++++++++++++++++++++++++++----------------
 dhall/src/phase/typecheck.rs | 33 ++++++++++----------
 5 files changed, 113 insertions(+), 108 deletions(-)

(limited to 'dhall/src')

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 {
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index dabfe87..27858d8 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -20,7 +20,7 @@ macro_rules! make_closure {
             Label::from(stringify!($var)).into(),
             $n
         );
-        ValueF::Var(var).into_value()
+        ValueF::Var(var).into_value_untyped()
     }};
     // Warning: assumes that $ty, as a dhall value, has type `Type`
     (λ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => {
@@ -30,30 +30,40 @@ macro_rules! make_closure {
                 make_closure!($($ty)*),
             ),
             make_closure!($($rest)*),
-        ).into_value()
+        ).into_value_untyped()
+    };
+    (Natural) => {
+        ValueF::from_builtin(Builtin::Natural)
+            .into_value_simple_type()
     };
-    (Natural) => { ValueF::from_builtin(Builtin::Natural).into_value() };
     (List $($rest:tt)*) => {
         ValueF::from_builtin(Builtin::List)
             .app_value(make_closure!($($rest)*))
-            .into_value()
+            .into_value_simple_type()
     };
-    (Some $($rest:tt)*) => {
-        ValueF::NEOptionalLit(make_closure!($($rest)*)).into_value()
+    (Some($($rest:tt)*)) => {
+        ValueF::NEOptionalLit(make_closure!($($rest)*))
+            .into_value_untyped()
     };
     (1 + $($rest:tt)*) => {
         ValueF::PartialExpr(ExprF::BinOp(
             dhall_syntax::BinOp::NaturalPlus,
             make_closure!($($rest)*),
-            Value::from_valuef(ValueF::NaturalLit(1)),
-        )).into_value()
+            Value::from_valuef_and_type(
+                ValueF::NaturalLit(1),
+                TypedValue::from_value(make_closure!(Natural))
+            ),
+        )).into_value_with_type(
+            TypedValue::from_value(make_closure!(Natural))
+        )
     };
     ([ $($head:tt)* ] # $($tail:tt)*) => {
         ValueF::PartialExpr(ExprF::BinOp(
             dhall_syntax::BinOp::ListAppend,
-            ValueF::NEListLit(vec![make_closure!($($head)*)]).into_value(),
+            ValueF::NEListLit(vec![make_closure!($($head)*)])
+                .into_value_untyped(),
             make_closure!($($tail)*),
-        )).into_value()
+        )).into_value_untyped()
     };
 }
 
@@ -189,10 +199,17 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
                 let mut kts = HashMap::new();
                 kts.insert(
                     "index".into(),
-                    TypedValue::from_valuef(ValueF::from_builtin(Natural)),
+                    TypedValue::from_valuef_untyped(ValueF::from_builtin(
+                        Natural,
+                    )),
                 );
                 kts.insert("value".into(), t.clone());
-                Ok((r, EmptyListLit(TypedValue::from_valuef(RecordType(kts)))))
+                Ok((
+                    r,
+                    EmptyListLit(TypedValue::from_valuef_untyped(RecordType(
+                        kts,
+                    ))),
+                ))
             }
             NEListLit(xs) => {
                 let xs = xs
@@ -201,9 +218,12 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
                     .map(|(i, e)| {
                         let i = NaturalLit(i);
                         let mut kvs = HashMap::new();
-                        kvs.insert("index".into(), Value::from_valuef(i));
+                        kvs.insert(
+                            "index".into(),
+                            Value::from_valuef_untyped(i),
+                        );
                         kvs.insert("value".into(), e.clone());
-                        Value::from_valuef(RecordLit(kvs))
+                        Value::from_valuef_untyped(RecordLit(kvs))
                     })
                     .collect();
                 Ok((r, NEListLit(xs)))
@@ -246,7 +266,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
                         .clone()
                         .app_value(x.clone())
                         .app_value(v)
-                        .into_value();
+                        .into_value_untyped();
                 }
                 Ok((r, v.to_whnf()))
             }
@@ -267,7 +287,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
                 f.app_valuef(
                     ValueF::from_builtin(Optional).app_value(t.clone()),
                 )
-                .app_value(make_closure!(λ(x: #t) -> Some var(x, 0)))
+                .app_value(make_closure!(λ(x: #t) -> Some(var(x, 0))))
                 .app_valuef(EmptyOptionalLit(
                     TypedValue::from_value_simple_type(t.clone()),
                 )),
@@ -327,7 +347,7 @@ pub(crate) fn apply_any(f: Value, a: Value) -> ValueF {
     let f_borrow = f.as_whnf();
     match &*f_borrow {
         ValueF::Lam(x, _, e) => {
-            let val = TypedValue::from_value_untyped(a);
+            let val = TypedValue::from_value(a);
             e.subst_shift(&x.into(), &val).to_whnf()
         }
         ValueF::AppliedBuiltin(b, args) => {
@@ -602,11 +622,11 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
         }
         (RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
             let kvs = merge_maps(kvs1, kvs2, |v1, v2| {
-                Value::from_partial_expr(ExprF::BinOp(
+                Value::from_valuef_untyped(ValueF::PartialExpr(ExprF::BinOp(
                     RecursiveRecordMerge,
                     v1.clone(),
                     v2.clone(),
-                ))
+                )))
             });
             Ret::ValueF(RecordLit(kvs))
         }
@@ -619,7 +639,7 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
         }
         (RecursiveRecordTypeMerge, RecordType(kvs1), RecordType(kvs2)) => {
             let kvs = merge_maps(kvs1, kvs2, |v1, v2| {
-                TypedValue::from_value_untyped(Value::from_partial_expr(
+                TypedValue::from_valuef_untyped(ValueF::PartialExpr(
                     ExprF::BinOp(
                         RecursiveRecordTypeMerge,
                         v1.to_value(),
@@ -655,15 +675,15 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
         ExprF::Annot(x, _) => Ret::Value(x),
         ExprF::Assert(_) => Ret::Expr(expr),
         ExprF::Lam(x, t, e) => {
-            Ret::ValueF(Lam(x.into(), TypedValue::from_value_untyped(t), e))
+            Ret::ValueF(Lam(x.into(), TypedValue::from_value(t), e))
         }
         ExprF::Pi(x, t, e) => Ret::ValueF(Pi(
             x.into(),
-            TypedValue::from_value_untyped(t),
-            TypedValue::from_value_untyped(e),
+            TypedValue::from_value(t),
+            TypedValue::from_value(e),
         )),
         ExprF::Let(x, _, v, b) => {
-            let v = TypedValue::from_value_untyped(v);
+            let v = TypedValue::from_value(v);
             Ret::Value(b.subst_shift(&x.into(), &v))
         }
         ExprF::App(v, a) => Ret::ValueF(v.app_value(a)),
@@ -697,12 +717,12 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
         }
         ExprF::RecordType(kts) => Ret::ValueF(RecordType(
             kts.into_iter()
-                .map(|(k, t)| (k, TypedValue::from_value_untyped(t)))
+                .map(|(k, t)| (k, TypedValue::from_value(t)))
                 .collect(),
         )),
         ExprF::UnionType(kts) => Ret::ValueF(UnionType(
             kts.into_iter()
-                .map(|(k, t)| (k, t.map(|t| TypedValue::from_value_untyped(t))))
+                .map(|(k, t)| (k, t.map(|t| TypedValue::from_value(t))))
                 .collect(),
         )),
         ExprF::TextLit(elts) => {
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 07c4ad8..e24f5a3 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -5,7 +5,7 @@ use dhall_syntax::{
 };
 
 use crate::core::context::TypecheckContext;
-use crate::core::value::{TypedValue, Value};
+use crate::core::value::TypedValue;
 use crate::core::valuef::ValueF;
 use crate::core::var::{Shift, Subst};
 use crate::error::{TypeError, TypeMessage};
@@ -37,8 +37,8 @@ fn tck_pi_type(
 
     let k = function_check(ka, kb);
 
-    Ok(TypedValue::from_value_and_type(
-        ValueF::Pi(x.into(), tx, te).into_value(),
+    Ok(TypedValue::from_valuef_and_type(
+        ValueF::Pi(x.into(), tx, te),
         TypedValue::from_const(k),
     ))
 }
@@ -70,8 +70,8 @@ fn tck_record_type(
     // An empty record type has type Type
     let k = k.unwrap_or(Const::Type);
 
-    Ok(TypedValue::from_value_and_type(
-        ValueF::RecordType(new_kts).into_value(),
+    Ok(TypedValue::from_valuef_and_type(
+        ValueF::RecordType(new_kts),
         TypedValue::from_const(k),
     ))
 }
@@ -115,8 +115,8 @@ where
     // an union type with only unary variants also has type Type
     let k = k.unwrap_or(Const::Type);
 
-    Ok(TypedValue::from_value_and_type(
-        ValueF::UnionType(new_kts).into_value(),
+    Ok(TypedValue::from_valuef_and_type(
+        ValueF::UnionType(new_kts),
         TypedValue::from_const(k),
     ))
 }
@@ -281,6 +281,7 @@ 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<TypedValue, TypeError> {
     type_with(&TypecheckContext::new(), SubExpr::from_builtin(b))
 }
@@ -351,8 +352,8 @@ fn type_with(
             match ret {
                 RetTypeOnly(typ) => {
                     let expr = expr.map_ref(|typed| typed.to_value());
-                    TypedValue::from_value_and_type(
-                        Value::from_partial_expr(expr),
+                    TypedValue::from_valuef_and_type(
+                        ValueF::PartialExpr(expr),
                         typ,
                     )
                 }
@@ -465,10 +466,9 @@ fn type_last_layer(
                 ));
             }
 
-            Ok(RetTypeOnly(TypedValue::from_value_and_type(
+            Ok(RetTypeOnly(TypedValue::from_valuef_and_type(
                 ValueF::from_builtin(dhall_syntax::Builtin::List)
-                    .app_value(t.to_value())
-                    .into_value(),
+                    .app_value(t.to_value()),
                 TypedValue::from_const(Type),
             )))
         }
@@ -478,10 +478,9 @@ fn type_last_layer(
                 return Err(TypeError::new(ctx, InvalidOptionalType(t)));
             }
 
-            Ok(RetTypeOnly(TypedValue::from_value_and_type(
+            Ok(RetTypeOnly(TypedValue::from_valuef_and_type(
                 ValueF::from_builtin(dhall_syntax::Builtin::Optional)
-                    .app_value(t.to_value())
-                    .into_value(),
+                    .app_value(t.to_value()),
                 TypedValue::from_const(Type),
             )))
         }
@@ -942,8 +941,8 @@ fn type_last_layer(
                 };
             }
 
-            Ok(RetTypeOnly(TypedValue::from_value_and_type(
-                ValueF::RecordType(new_kts).into_value(),
+            Ok(RetTypeOnly(TypedValue::from_valuef_and_type(
+                ValueF::RecordType(new_kts),
                 record_type.get_type()?.into_owned(),
             )))
         }
-- 
cgit v1.2.3