Introduce intermediate representation that stores typed expr

8 files changed, 177 insertions, 129 deletions

diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index 8b3ada1..a1125cd 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -7,10 +7,12 @@ use crate::semantics::core::context::TyCtx;
 use crate::semantics::core::var::{AlphaVar, Binder};
 use crate::semantics::phase::normalize::{apply_any, normalize_whnf};
 use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value};
-use crate::semantics::phase::{Normalized, NormalizedExpr, Typed};
-use crate::semantics::to_expr;
+use crate::semantics::phase::{
+    Normalized, NormalizedExpr, ToExprOptions, Typed,
+};
+use crate::semantics::{TyExpr, TyExprKind};
 use crate::syntax::{
-    Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label,
+    BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label,
     NaiveDouble, Natural, Span,
 };
 
@@ -159,11 +161,12 @@ impl Value {
     }
 
     /// Converts a value back to the corresponding AST expression.
-    pub(crate) fn to_expr(
-        &self,
-        opts: to_expr::ToExprOptions,
-    ) -> NormalizedExpr {
-        to_expr::value_to_expr(self, opts, &vec![])
+    pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
+        if opts.normalize {
+            self.normalize_nf();
+        }
+
+        self.to_tyexpr().to_expr(opts)
     }
     pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind<Value> {
         self.as_whnf().clone()
@@ -283,6 +286,10 @@ impl Value {
     //         }
     //     }
     // }
+
+    pub fn to_tyexpr(&self) -> TyExpr {
+        value_to_tyexpr(self)
+    }
 }
 
 impl ValueInternal {
@@ -510,6 +517,70 @@ impl<V> ValueKind<V> {
     }
 }
 
+fn value_to_tyexpr(val: &Value) -> TyExpr {
+    let val_kind = val.as_kind();
+    let val_ty = val.as_internal().ty.clone();
+    let val_span = val.as_internal().span.clone();
+    if let ValueKind::Var(v) = &*val_kind {
+        return TyExpr::new(TyExprKind::Var(*v), val_ty, val_span);
+    }
+
+    // TODO: properly recover intermediate types; `None` is a time-bomb here.
+    let rc = |expr| TyExpr::new(TyExprKind::Expr(expr), None, Span::Artificial);
+
+    let val_kind = val_kind.map_ref(|v| v.to_tyexpr());
+    let expr = match val_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::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::NEOptionalLit(n) => ExprKind::SomeLit(n),
+        ValueKind::EmptyListLit(n) => ExprKind::EmptyListLit(rc(
+            ExprKind::App(rc(ExprKind::Builtin(Builtin::List)), n),
+        )),
+        ValueKind::NEListLit(elts) => ExprKind::NEListLit(elts),
+        ValueKind::RecordLit(kvs) => {
+            ExprKind::RecordLit(kvs.into_iter().collect())
+        }
+        ValueKind::RecordType(kts) => {
+            ExprKind::RecordType(kts.into_iter().collect())
+        }
+        ValueKind::UnionType(kts) => {
+            ExprKind::UnionType(kts.into_iter().collect())
+        }
+        ValueKind::UnionConstructor(l, kts) => ExprKind::Field(
+            rc(ExprKind::UnionType(kts.into_iter().collect())),
+            l,
+        ),
+        ValueKind::UnionLit(l, v, kts) => ExprKind::App(
+            rc(ExprKind::Field(
+                rc(ExprKind::UnionType(kts.into_iter().collect())),
+                l,
+            )),
+            v,
+        ),
+        ValueKind::TextLit(elts) => {
+            ExprKind::TextLit(elts.into_iter().collect())
+        }
+        ValueKind::Equivalence(x, y) => {
+            ExprKind::BinOp(BinOp::Equivalence, x, y)
+        }
+        ValueKind::PartialExpr(e) => e,
+    };
+
+    TyExpr::new(TyExprKind::Expr(expr), val_ty, val_span)
+}
+
 // TODO: use Rc comparison to shortcut on identical pointers
 impl std::cmp::PartialEq for Value {
     fn eq(&self, other: &Self) -> bool {
diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs
index b336c66..0aa86d5 100644
--- a/dhall/src/semantics/core/var.rs
+++ b/dhall/src/semantics/core/var.rs
@@ -1,7 +1,7 @@
 use crate::syntax::{Label, V};
 
 /// Stores an alpha-normalized variable.
-#[derive(Clone, Eq)]
+#[derive(Clone, Copy, PartialEq, Eq)]
 pub struct AlphaVar {
     alpha: V<()>,
 }
@@ -36,28 +36,12 @@ impl Binder {
     pub(crate) fn new(name: Label) -> Self {
         Binder { name }
     }
-    pub(crate) fn to_label_maybe_alpha(&self, alpha: bool) -> Label {
-        if alpha {
-            "_".into()
-        } else {
-            self.to_label()
-        }
-    }
     pub(crate) fn to_label(&self) -> Label {
         self.clone().into()
     }
-    pub(crate) fn name(&self) -> &Label {
-        &self.name
-    }
 }
 
 /// Equality up to alpha-equivalence
-impl std::cmp::PartialEq for AlphaVar {
-    fn eq(&self, other: &Self) -> bool {
-        self.alpha == other.alpha
-    }
-}
-/// Equality up to alpha-equivalence
 impl std::cmp::PartialEq for Binder {
     fn eq(&self, _other: &Self) -> bool {
         true
diff --git a/dhall/src/semantics/mod.rs b/dhall/src/semantics/mod.rs
index 3ef1aba..63f74ee 100644
--- a/dhall/src/semantics/mod.rs
+++ b/dhall/src/semantics/mod.rs
@@ -1,4 +1,5 @@
 pub mod core;
 pub mod phase;
-pub mod to_expr;
+pub mod tck;
 pub(crate) use self::core::*;
+pub(crate) use self::tck::*;
diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs
index 6afed88..4dc91e7 100644
--- a/dhall/src/semantics/phase/mod.rs
+++ b/dhall/src/semantics/phase/mod.rs
@@ -4,7 +4,6 @@ use std::path::Path;
 use crate::error::{EncodeError, Error, ImportError, TypeError};
 use crate::semantics::core::value::Value;
 use crate::semantics::core::value::ValueKind;
-use crate::semantics::to_expr::ToExprOptions;
 use crate::syntax::binary;
 use crate::syntax::{Builtin, Const, Expr};
 use resolve::ImportRoot;
@@ -38,6 +37,15 @@ pub struct Typed(Value);
 #[derive(Debug, Clone)]
 pub struct Normalized(Typed);
 
+/// Controls conversion from `Value` to `Expr`
+#[derive(Copy, Clone)]
+pub(crate) struct ToExprOptions {
+    /// Whether to convert all variables to `_`
+    pub(crate) alpha: bool,
+    /// Whether to normalize before converting
+    pub(crate) normalize: bool,
+}
+
 impl Parsed {
     pub fn parse_file(f: &Path) -> Result<Parsed, Error> {
         parse::parse_file(f)
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,
+            }
+        }
+    })
+}
diff --git a/dhall/src/semantics/to_expr.rs b/dhall/src/semantics/to_expr.rs
deleted file mode 100644
index 612f794..0000000
--- a/dhall/src/semantics/to_expr.rs
+++ /dev/null
@@ -1,101 +0,0 @@
-use crate::semantics::core::var::Binder;
-use crate::semantics::phase::typecheck::rc;
-use crate::semantics::phase::NormalizedExpr;
-use crate::semantics::{Value, ValueKind};
-use crate::syntax;
-use crate::syntax::{Builtin, ExprKind, V};
-
-/// Controls conversion from `Value` to `Expr`
-#[derive(Copy, Clone)]
-pub(crate) struct ToExprOptions {
-    /// Whether to convert all variables to `_`
-    pub(crate) alpha: bool,
-    /// Whether to normalize before converting
-    pub(crate) normalize: bool,
-}
-
-/// Converts a value back to the corresponding AST expression.
-pub(crate) fn value_to_expr<'a>(
-    val: &'a Value,
-    opts: ToExprOptions,
-    ctx: &Vec<&'a Binder>,
-) -> NormalizedExpr {
-    if opts.normalize {
-        val.normalize_whnf();
-    }
-
-    let kind = val.as_kind();
-    let kind = kind.map_ref_with_special_handling_of_binders(
-        |v| value_to_expr(v, opts, ctx),
-        |b, _, v| {
-            let mut ctx = ctx.clone();
-            ctx.push(b);
-            value_to_expr(v, opts, &ctx)
-        },
-    );
-    match kind {
-        ValueKind::Var(v) if opts.alpha => {
-            rc(ExprKind::Var(V("_".into(), v.idx())))
-        }
-        ValueKind::Var(v) => {
-            let name = ctx[ctx.len() - 1 - v.idx()].to_label();
-            let mut idx = 0;
-            for b in ctx.iter().rev().take(v.idx()) {
-                if b.name() == &name {
-                    idx += 1;
-                }
-            }
-            rc(ExprKind::Var(V(name, idx)))
-        }
-        ValueKind::Lam(x, t, e) => {
-            rc(ExprKind::Lam(x.to_label_maybe_alpha(opts.alpha), t, e))
-        }
-        ValueKind::AppliedBuiltin(b, args) => args
-            .into_iter()
-            .fold(rc(ExprKind::Builtin(b)), |acc, v| rc(ExprKind::App(acc, v))),
-        ValueKind::Pi(x, t, e) => {
-            rc(ExprKind::Pi(x.to_label_maybe_alpha(opts.alpha), t, e))
-        }
-        ValueKind::Const(c) => rc(ExprKind::Const(c)),
-        ValueKind::BoolLit(b) => rc(ExprKind::BoolLit(b)),
-        ValueKind::NaturalLit(n) => rc(ExprKind::NaturalLit(n)),
-        ValueKind::IntegerLit(n) => rc(ExprKind::IntegerLit(n)),
-        ValueKind::DoubleLit(n) => rc(ExprKind::DoubleLit(n)),
-        ValueKind::EmptyOptionalLit(n) => rc(ExprKind::App(
-            rc(ExprKind::Builtin(Builtin::OptionalNone)),
-            n,
-        )),
-        ValueKind::NEOptionalLit(n) => rc(ExprKind::SomeLit(n)),
-        ValueKind::EmptyListLit(n) => rc(ExprKind::EmptyListLit(rc(
-            ExprKind::App(rc(ExprKind::Builtin(Builtin::List)), n),
-        ))),
-        ValueKind::NEListLit(elts) => rc(ExprKind::NEListLit(elts)),
-        ValueKind::RecordLit(kvs) => {
-            rc(ExprKind::RecordLit(kvs.into_iter().collect()))
-        }
-        ValueKind::RecordType(kts) => {
-            rc(ExprKind::RecordType(kts.into_iter().collect()))
-        }
-        ValueKind::UnionType(kts) => {
-            rc(ExprKind::UnionType(kts.into_iter().collect()))
-        }
-        ValueKind::UnionConstructor(l, kts) => rc(ExprKind::Field(
-            rc(ExprKind::UnionType(kts.into_iter().collect())),
-            l,
-        )),
-        ValueKind::UnionLit(l, v, kts) => rc(ExprKind::App(
-            rc(ExprKind::Field(
-                rc(ExprKind::UnionType(kts.into_iter().collect())),
-                l,
-            )),
-            v,
-        )),
-        ValueKind::TextLit(elts) => {
-            rc(ExprKind::TextLit(elts.into_iter().collect()))
-        }
-        ValueKind::Equivalence(x, y) => {
-            rc(ExprKind::BinOp(syntax::BinOp::Equivalence, x, y))
-        }
-        ValueKind::PartialExpr(e) => rc(e),
-    }
-}
diff --git a/dhall/src/syntax/ast/expr.rs b/dhall/src/syntax/ast/expr.rs
index 170cbe7..f22a279 100644
--- a/dhall/src/syntax/ast/expr.rs
+++ b/dhall/src/syntax/ast/expr.rs
@@ -23,7 +23,7 @@ pub enum Const {
 /// The `Label` field is the variable's name (i.e. \"`x`\").
 /// The `Int` field is a DeBruijn index.
 /// See dhall-lang/standard/semantics.md for details
-#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
 pub struct V<Label>(pub Label, pub usize);
 
 // Definition order must match precedence order for