2 files changed, 85 insertions, 0 deletions
diff --git a/dhall/src/semantics/tck/mod.rs b/dhall/src/semantics/tck/mod.rs
new file mode 100644
index 0000000..407605d
--- /dev/null
+++ b/dhall/src/semantics/tck/mod.rs
@@ -0,0 +1,2 @@
+pub mod tyexpr;
+pub(crate) use tyexpr::*;
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
new file mode 100644
index 0000000..a8b8e58
--- /dev/null
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -0,0 +1,83 @@
+#![allow(dead_code)]
+use crate::semantics::core::var::AlphaVar;
+use crate::semantics::phase::typecheck::rc;
+use crate::semantics::phase::Normalized;
+use crate::semantics::phase::{NormalizedExpr, ToExprOptions};
+use crate::semantics::Value;
+use crate::syntax::{ExprKind, Label, Span, V};
+
+pub(crate) type Type = Value;
+
+// An expression with inferred types at every node and resolved variables.
+pub(crate) struct TyExpr {
+    kind: Box<TyExprKind>,
+    ty: Option<Type>,
+    span: Span,
+}
+
+pub(crate) enum TyExprKind {
+    Var(AlphaVar),
+    // Forbidden ExprKind variants: Var
+    Expr(ExprKind<TyExpr, Normalized>),
+}
+
+impl TyExpr {
+    pub fn new(kind: TyExprKind, ty: Option<Type>, span: Span) -> Self {
+        TyExpr {
+            kind: Box::new(kind),
+            ty,
+            span,
+        }
+    }
+
+    pub fn kind(&self) -> &TyExprKind {
+        &*self.kind
+    }
+
+    /// Converts a value back to the corresponding AST expression.
+    pub fn to_expr<'a>(&'a self, opts: ToExprOptions) -> NormalizedExpr {
+        tyexpr_to_expr(self, opts, &Vec::new())
+    }
+}
+
+// TODO: mutate context once map_ref gets simplified
+fn tyexpr_to_expr<'a>(
+    tyexpr: &'a TyExpr,
+    opts: ToExprOptions,
+    ctx: &Vec<&'a Label>,
+) -> NormalizedExpr {
+    rc(match tyexpr.kind() {
+        TyExprKind::Var(v) if opts.alpha => {
+            ExprKind::Var(V("_".into(), v.idx()))
+        }
+        TyExprKind::Var(v) => {
+            let name = ctx[ctx.len() - 1 - v.idx()];
+            let mut idx = 0;
+            for l in ctx.iter().rev().take(v.idx()) {
+                if *l == name {
+                    idx += 1;
+                }
+            }
+            ExprKind::Var(V(name.clone(), idx))
+        }
+        TyExprKind::Expr(e) => {
+            let e = e.map_ref_with_special_handling_of_binders(
+                |tye| tyexpr_to_expr(tye, opts, ctx),
+                |l, tye| {
+                    let ctx = ctx.iter().copied().chain(Some(l)).collect();
+                    tyexpr_to_expr(tye, opts, &ctx)
+                },
+            );
+
+            match e {
+                ExprKind::Lam(_, t, e) if opts.alpha => {
+                    ExprKind::Lam("_".into(), t, e)
+                }
+                ExprKind::Pi(_, t, e) if opts.alpha => {
+                    ExprKind::Pi("_".into(), t, e)
+                }
+                e => e,
+            }
+        }
+    })
+}