Restore more types in value_to_tyexpr

5 files changed, 93 insertions, 37 deletions

diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index 7086616..f470019 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -10,7 +10,7 @@ use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value};
 use crate::semantics::phase::{
     Normalized, NormalizedExpr, ToExprOptions, Typed,
 };
-use crate::semantics::{TyExpr, TyExprKind};
+use crate::semantics::{TyExpr, TyExprKind, Type};
 use crate::syntax::{
     BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label,
     NaiveDouble, Natural, Span,
@@ -75,8 +75,10 @@ pub(crate) enum ValueKind<Value> {
     RecordType(HashMap<Label, Value>),
     RecordLit(HashMap<Label, Value>),
     UnionType(HashMap<Label, Option<Value>>),
-    UnionConstructor(Label, HashMap<Label, Option<Value>>),
-    UnionLit(Label, Value, HashMap<Label, Option<Value>>),
+    // Also keep the type of the uniontype around
+    UnionConstructor(Label, HashMap<Label, Option<Value>>, Type),
+    // Also keep the type of the uniontype and the constructor around
+    UnionLit(Label, Value, HashMap<Label, Option<Value>>, Type, Type),
     // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and
     // contiguous text values must be merged.
     TextLit(Vec<InterpolatedTextContents<Value>>),
@@ -296,28 +298,40 @@ impl Value {
         }
 
         // TODO: properly recover intermediate types; `None` is a time-bomb here.
-        let rc =
-            |expr| TyExpr::new(TyExprKind::Expr(expr), None, Span::Artificial);
-
         let self_kind = self_kind.map_ref(|v| v.to_tyexpr());
         let expr = match self_kind {
             ValueKind::Var(_) => unreachable!(),
             ValueKind::Lam(x, t, e) => ExprKind::Lam(x.to_label(), t, e),
             ValueKind::Pi(x, t, e) => ExprKind::Pi(x.to_label(), t, e),
-            ValueKind::AppliedBuiltin(b, args) => args
-                .into_iter()
-                .fold(ExprKind::Builtin(b), |acc, v| ExprKind::App(rc(acc), v)),
+            ValueKind::AppliedBuiltin(b, args) => {
+                args.into_iter().fold(ExprKind::Builtin(b), |acc, v| {
+                    ExprKind::App(
+                        TyExpr::new(
+                            TyExprKind::Expr(acc),
+                            None, // TODO
+                            Span::Artificial,
+                        ),
+                        v,
+                    )
+                })
+            }
             ValueKind::Const(c) => ExprKind::Const(c),
             ValueKind::BoolLit(b) => ExprKind::BoolLit(b),
             ValueKind::NaturalLit(n) => ExprKind::NaturalLit(n),
             ValueKind::IntegerLit(n) => ExprKind::IntegerLit(n),
             ValueKind::DoubleLit(n) => ExprKind::DoubleLit(n),
-            ValueKind::EmptyOptionalLit(n) => {
-                ExprKind::App(rc(ExprKind::Builtin(Builtin::OptionalNone)), n)
-            }
+            ValueKind::EmptyOptionalLit(n) => ExprKind::App(
+                builtin_to_value(Builtin::OptionalNone).to_tyexpr(),
+                n,
+            ),
             ValueKind::NEOptionalLit(n) => ExprKind::SomeLit(n),
-            ValueKind::EmptyListLit(n) => ExprKind::EmptyListLit(rc(
-                ExprKind::App(rc(ExprKind::Builtin(Builtin::List)), n),
+            ValueKind::EmptyListLit(n) => ExprKind::EmptyListLit(TyExpr::new(
+                TyExprKind::Expr(ExprKind::App(
+                    builtin_to_value(Builtin::List).to_tyexpr(),
+                    n,
+                )),
+                Some(const_to_value(Const::Type)),
+                Span::Artificial,
             )),
             ValueKind::NEListLit(elts) => ExprKind::NEListLit(elts),
             ValueKind::RecordLit(kvs) => {
@@ -329,15 +343,31 @@ impl Value {
             ValueKind::UnionType(kts) => {
                 ExprKind::UnionType(kts.into_iter().collect())
             }
-            ValueKind::UnionConstructor(l, kts) => ExprKind::Field(
-                rc(ExprKind::UnionType(kts.into_iter().collect())),
+            ValueKind::UnionConstructor(l, kts, t) => ExprKind::Field(
+                TyExpr::new(
+                    TyExprKind::Expr(ExprKind::UnionType(
+                        kts.into_iter().collect(),
+                    )),
+                    Some(t),
+                    Span::Artificial,
+                ),
                 l,
             ),
-            ValueKind::UnionLit(l, v, kts) => ExprKind::App(
-                rc(ExprKind::Field(
-                    rc(ExprKind::UnionType(kts.into_iter().collect())),
-                    l,
-                )),
+            ValueKind::UnionLit(l, v, kts, uniont, ctort) => ExprKind::App(
+                TyExpr::new(
+                    TyExprKind::Expr(ExprKind::Field(
+                        TyExpr::new(
+                            TyExprKind::Expr(ExprKind::UnionType(
+                                kts.into_iter().collect(),
+                            )),
+                            Some(uniont),
+                            Span::Artificial,
+                        ),
+                        l,
+                    )),
+                    Some(ctort),
+                    Span::Artificial,
+                ),
                 v,
             ),
             ValueKind::TextLit(elts) => {
@@ -483,12 +513,13 @@ impl ValueKind<Value> {
                     x.normalize_mut();
                 }
             }
-            ValueKind::UnionType(kts) | ValueKind::UnionConstructor(_, kts) => {
+            ValueKind::UnionType(kts)
+            | ValueKind::UnionConstructor(_, kts, _) => {
                 for x in kts.values_mut().flat_map(|opt| opt) {
                     x.normalize_mut();
                 }
             }
-            ValueKind::UnionLit(_, v, kts) => {
+            ValueKind::UnionLit(_, v, kts, _, _) => {
                 v.normalize_mut();
                 for x in kts.values_mut().flat_map(|opt| opt) {
                     x.normalize_mut();
diff --git a/dhall/src/semantics/core/visitor.rs b/dhall/src/semantics/core/visitor.rs
index e61a649..a449f6c 100644
--- a/dhall/src/semantics/core/visitor.rs
+++ b/dhall/src/semantics/core/visitor.rs
@@ -94,12 +94,16 @@ where
         RecordType(kts) => RecordType(v.visit_map(kts)?),
         RecordLit(kvs) => RecordLit(v.visit_map(kvs)?),
         UnionType(kts) => UnionType(v.visit_optmap(kts)?),
-        UnionConstructor(l, kts) => {
-            UnionConstructor(l.clone(), v.visit_optmap(kts)?)
-        }
-        UnionLit(l, t, kts) => {
-            UnionLit(l.clone(), v.visit_val(t)?, v.visit_optmap(kts)?)
+        UnionConstructor(l, kts, t) => {
+            UnionConstructor(l.clone(), v.visit_optmap(kts)?, t.clone())
         }
+        UnionLit(l, x, kts, uniont, ctort) => UnionLit(
+            l.clone(),
+            v.visit_val(x)?,
+            v.visit_optmap(kts)?,
+            uniont.clone(),
+            ctort.clone(),
+        ),
         TextLit(ts) => TextLit(
             ts.iter()
                 .map(|t| t.traverse_ref(|e| v.visit_val(e)))
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index 541a196..f0a6a8c 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -374,9 +374,13 @@ pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind<Value> {
             let args = args.iter().cloned().chain(once(a.clone())).collect();
             apply_builtin(*b, args, ty)
         }
-        ValueKind::UnionConstructor(l, kts) => {
-            ValueKind::UnionLit(l.clone(), a, kts.clone())
-        }
+        ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit(
+            l.clone(),
+            a,
+            kts.clone(),
+            uniont.clone(),
+            f.get_type().unwrap(),
+        ),
         _ => {
             drop(f_borrow);
             ValueKind::PartialExpr(ExprKind::App(f, a))
@@ -692,9 +696,11 @@ pub(crate) fn normalize_one_layer(
                         Ret::Expr(expr)
                     }
                 },
-                UnionType(kts) => {
-                    Ret::ValueKind(UnionConstructor(l.clone(), kts.clone()))
-                }
+                UnionType(kts) => Ret::ValueKind(UnionConstructor(
+                    l.clone(),
+                    kts.clone(),
+                    v.get_type().unwrap(),
+                )),
                 _ => {
                     drop(v_borrow);
                     Ret::Expr(expr)
@@ -710,7 +716,8 @@ pub(crate) fn normalize_one_layer(
             let handlers_borrow = handlers.as_whnf();
             let variant_borrow = variant.as_whnf();
             match (&*handlers_borrow, &*variant_borrow) {
-                (RecordLit(kvs), UnionConstructor(l, _)) => match kvs.get(l) {
+                (RecordLit(kvs), UnionConstructor(l, _, _)) => match kvs.get(l)
+                {
                     Some(h) => Ret::Value(h.clone()),
                     None => {
                         drop(handlers_borrow);
@@ -718,7 +725,7 @@ pub(crate) fn normalize_one_layer(
                         Ret::Expr(expr)
                     }
                 },
-                (RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) {
+                (RecordLit(kvs), UnionLit(l, v, _, _, _)) => match kvs.get(l) {
                     Some(h) => Ret::Value(h.app(v.clone())),
                     None => {
                         drop(handlers_borrow);
diff --git a/dhall/src/semantics/tck/mod.rs b/dhall/src/semantics/tck/mod.rs
index 407605d..ba95847 100644
--- a/dhall/src/semantics/tck/mod.rs
+++ b/dhall/src/semantics/tck/mod.rs
@@ -1,2 +1,4 @@
+pub mod context;
 pub mod tyexpr;
+pub mod typecheck;
 pub(crate) use tyexpr::*;
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index f0fcdd1..36cae04 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,4 +1,6 @@
 #![allow(dead_code)]
+use crate::error::{TypeError, TypeMessage};
+use crate::semantics::core::context::TyCtx;
 use crate::semantics::core::var::AlphaVar;
 use crate::semantics::phase::typecheck::rc;
 use crate::semantics::phase::Normalized;
@@ -33,11 +35,21 @@ impl TyExpr {
     pub fn kind(&self) -> &TyExprKind {
         &*self.kind
     }
+    pub fn get_type(&self) -> Result<Type, TypeError> {
+        match &self.ty {
+            Some(t) => Ok(t.clone()),
+            None => Err(TypeError::new(&TyCtx::new(), TypeMessage::Sort)),
+        }
+    }
 
     /// Converts a value back to the corresponding AST expression.
-    pub fn to_expr<'a>(&'a self, opts: ToExprOptions) -> NormalizedExpr {
+    pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
         tyexpr_to_expr(self, opts, &mut Vec::new())
     }
+    // TODO: temporary hack
+    pub fn to_value(&self) -> Value {
+        todo!()
+    }
 }
 
 fn tyexpr_to_expr<'a>(