Keep Spans through normalization and typechecking

3 files changed, 39 insertions, 36 deletions

diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index db426ce..5bde68f 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -204,16 +204,15 @@ impl Normalized {
     pub(crate) fn from_thunk_and_type(th: Thunk, t: Type) -> Self {
         Normalized(TypedInternal::from_thunk_and_type(th, t))
     }
-    // Deprecated
-    pub(crate) fn as_expr(&self) -> SubExpr<X, X> {
-        self.0.to_expr()
-    }
     pub(crate) fn to_expr(&self) -> SubExpr<X, X> {
         self.0.to_expr()
     }
     pub(crate) fn to_value(&self) -> Value {
         self.0.to_value()
     }
+    pub(crate) fn to_thunk(&self) -> Thunk {
+        self.0.to_thunk()
+    }
     #[allow(dead_code)]
     pub(crate) fn unnote(self) -> Normalized {
         Normalized(self.0)
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 4d87225..8ae746d 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -6,12 +6,12 @@ use dhall_proc_macros as dhall;
 use dhall_syntax::context::Context;
 use dhall_syntax::{
     rc, BinOp, Builtin, Const, ExprF, Integer, InterpolatedText,
-    InterpolatedTextContents, Label, Natural, SubExpr, V, X,
+    InterpolatedTextContents, Label, Natural, Span, SubExpr, V, X,
 };
 
 use crate::expr::{Normalized, Type, Typed, TypedInternal};
 
-type InputSubExpr = SubExpr<X, Normalized>;
+type InputSubExpr = SubExpr<Span, Normalized>;
 type OutputSubExpr = SubExpr<X, X>;
 
 impl Typed {
@@ -110,10 +110,7 @@ impl NormalizationContext {
             for v in vs.iter() {
                 let new_item = match v {
                     Type(var, _) => EnvItem::Skip(var.clone()),
-                    Value(e) => EnvItem::Thunk(Thunk::new(
-                        NormalizationContext::new(),
-                        e.as_expr().embed_absurd(),
-                    )),
+                    Value(e) => EnvItem::Thunk(e.to_thunk()),
                 };
                 ctx = ctx.insert(k.clone(), new_item);
             }
@@ -736,7 +733,10 @@ mod thunk {
         }
 
         pub(crate) fn from_normalized_expr(e: OutputSubExpr) -> Thunk {
-            Thunk::new(NormalizationContext::new(), e.embed_absurd())
+            Thunk::new(
+                NormalizationContext::new(),
+                e.embed_absurd().note_absurd(),
+            )
         }
 
         // Normalizes contents to normal form; faster than `normalize_nf` if
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 732f7bc..8b7f011 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -16,19 +16,19 @@ use self::TypeMessage::*;
 
 impl Resolved {
     pub fn typecheck(self) -> Result<Typed, TypeError> {
-        type_of(self.0.unnote())
+        type_of(self.0)
     }
     pub fn typecheck_with(self, ty: &Type) -> Result<Typed, TypeError> {
-        let expr: SubExpr<_, _> = self.0.unnote();
-        let ty: SubExpr<_, _> = ty.to_expr().embed_absurd();
-        type_of(rc(ExprF::Annot(expr, ty)))
+        let expr: SubExpr<_, _> = self.0;
+        let ty: SubExpr<_, _> = ty.to_expr().embed_absurd().note_absurd();
+        type_of(expr.rewrap(ExprF::Annot(expr.clone(), ty)))
     }
     /// Pretends this expression has been typechecked. Use with care.
     #[allow(dead_code)]
     pub fn skip_typecheck(self) -> Typed {
         Typed::from_thunk_untyped(Thunk::new(
             NormalizationContext::new(),
-            self.0.unnote(),
+            self.0,
         ))
     }
 }
@@ -97,7 +97,7 @@ impl TypeThunk {
             TypeThunk::Type(t) => Ok(t.clone()),
             TypeThunk::Thunk(th) => {
                 // TODO: rule out statically
-                mktype(ctx, th.normalize_to_expr().embed_absurd())
+                mktype(ctx, th.normalize_to_expr().embed_absurd().note_absurd())
             }
         }
     }
@@ -621,13 +621,16 @@ impl TypeIntermediate {
 /// and turn it into a type, typechecking it along the way.
 fn mktype(
     ctx: &TypecheckContext,
-    e: SubExpr<X, Normalized>,
+    e: SubExpr<Span, Normalized>,
 ) -> Result<Type, TypeError> {
     Ok(type_with(ctx, e)?.to_type())
 }
 
 fn builtin_to_type(b: Builtin) -> Result<Type, TypeError> {
-    mktype(&TypecheckContext::new(), rc(ExprF::Builtin(b)))
+    mktype(
+        &TypecheckContext::new(),
+        SubExpr::from_expr_no_note(ExprF::Builtin(b)),
+    )
 }
 
 /// Intermediary return type
@@ -636,18 +639,17 @@ enum Ret {
     RetTyped(Typed),
     /// Use the contained Type as the type of the input expression
     RetType(Type),
-    /// Returns an expression that must be typechecked and
-    /// turned into a Type first.
-    RetExpr(Expr<X, Normalized>),
 }
 
 /// Type-check an expression and return the expression alongside its type if type-checking
 /// succeeded, or an error if type-checking failed
 fn type_with(
     ctx: &TypecheckContext,
-    e: SubExpr<X, Normalized>,
+    e: SubExpr<Span, Normalized>,
 ) -> Result<Typed, TypeError> {
-    use dhall_syntax::ExprF::*;
+    use dhall_syntax::ExprF::{
+        Annot, App, Embed, Lam, Let, OldOptionalLit, Pi, SomeLit,
+    };
 
     use Ret::*;
     let ret = match e.as_ref() {
@@ -673,7 +675,7 @@ fn type_with(
         }
         Let(x, t, v, e) => {
             let v = if let Some(t) = t {
-                rc(Annot(v.clone(), t.clone()))
+                t.rewrap(Annot(v.clone(), t.clone()))
             } else {
                 v.clone()
             };
@@ -684,14 +686,18 @@ fn type_with(
             Ok(RetType(e.get_type()?.into_owned()))
         }
         OldOptionalLit(None, t) => {
-            let t = t.clone();
-            let e = dhall::subexpr!(None t);
+            let none = SubExpr::from_expr_no_note(ExprF::Builtin(
+                Builtin::OptionalNone,
+            ));
+            let e = e.rewrap(App(none, t.clone()));
             return type_with(ctx, e);
         }
         OldOptionalLit(Some(x), t) => {
-            let t = t.clone();
-            let x = x.clone();
-            let e = dhall::subexpr!(Some x : Optional t);
+            let optional =
+                SubExpr::from_expr_no_note(ExprF::Builtin(Builtin::Optional));
+            let x = x.rewrap(SomeLit(x.clone()));
+            let t = t.rewrap(App(optional, t.clone()));
+            let e = e.rewrap(Annot(x, t));
             return type_with(ctx, e);
         }
         Embed(p) => Ok(RetTyped(p.clone().into())),
@@ -703,10 +709,6 @@ fn type_with(
         ),
     }?;
     Ok(match ret {
-        RetExpr(ret) => Typed::from_thunk_and_type(
-            Thunk::new(ctx.to_normalization_ctx(), e),
-            mktype(ctx, rc(ret))?,
-        ),
         RetType(typ) => Typed::from_thunk_and_type(
             Thunk::new(ctx.to_normalization_ctx(), e),
             typ,
@@ -935,7 +937,9 @@ fn type_last_layer(
             }
         }
         Const(c) => Ok(RetTyped(const_to_typed(c))),
-        Builtin(b) => Ok(RetExpr(type_of_builtin(b))),
+        Builtin(b) => {
+            Ok(RetType(mktype(ctx, rc(type_of_builtin(b)).note_absurd())?))
+        }
         BoolLit(_) => Ok(RetType(builtin_to_type(Bool)?)),
         NaturalLit(_) => Ok(RetType(builtin_to_type(Natural)?)),
         IntegerLit(_) => Ok(RetType(builtin_to_type(Integer)?)),
@@ -994,7 +998,7 @@ fn type_last_layer(
 /// `typeOf` is the same as `type_with` with an empty context, meaning that the
 /// expression must be closed (i.e. no free variables), otherwise type-checking
 /// will fail.
-fn type_of(e: SubExpr<X, Normalized>) -> Result<Typed, TypeError> {
+fn type_of(e: SubExpr<Span, Normalized>) -> Result<Typed, TypeError> {
     let ctx = TypecheckContext::new();
     let e = type_with(&ctx, e)?;
     // Ensure `e` has a type (i.e. `e` is not `Sort`)