From e3054cbbeb84bbaec626689c53584e54ca515d3e Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 7 May 2019 21:53:00 +0200
Subject: Don't discard normalization work done by typechecking

---
 dhall/src/core/context.rs    |  33 +++-------
 dhall/src/core/thunk.rs      |  52 ++++++++++++++--
 dhall/src/phase/typecheck.rs | 145 +++++++++++++++++++++++++++----------------
 3 files changed, 147 insertions(+), 83 deletions(-)

(limited to 'dhall/src')

diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs
index aeec7fb..56dec03 100644
--- a/dhall/src/core/context.rs
+++ b/dhall/src/core/context.rs
@@ -1,4 +1,3 @@
-use std::borrow::Cow;
 use std::rc::Rc;
 
 use dhall_syntax::context::Context as SimpleContext;
@@ -25,28 +24,10 @@ pub(crate) struct NormalizationContext(Context<()>);
 #[derive(Debug, Clone)]
 pub(crate) struct TypecheckContext(Context<Type>);
 
-impl<T> CtxItem<T> {
-    fn forget(&self) -> CtxItem<()> {
-        match self {
-            CtxItem::Kept(var, _) => CtxItem::Kept(var.clone(), ()),
-            CtxItem::Replaced(e, _) => CtxItem::Replaced(e.clone(), ()),
-        }
-    }
-}
-
 impl<T> Context<T> {
     pub(crate) fn new() -> Self {
         Context(Rc::new(SimpleContext::new()))
     }
-    pub(crate) fn forget(&self) -> Context<()> {
-        let mut ctx = SimpleContext::new();
-        for (k, vs) in self.0.iter_keys() {
-            for v in vs.iter() {
-                ctx = ctx.insert(k.clone(), v.forget());
-            }
-        }
-        Context(Rc::new(ctx))
-    }
     pub(crate) fn insert_kept(&self, x: &Label, t: T) -> Self
     where
         T: Shift + Clone,
@@ -103,16 +84,18 @@ impl TypecheckContext {
             e.get_type()?.into_owned(),
         )))
     }
-    pub(crate) fn lookup(&self, var: &V<Label>) -> Option<Cow<'_, Type>> {
+    pub(crate) fn lookup(&self, var: &V<Label>) -> Option<Typed> {
         match self.0.lookup(var) {
-            Some(CtxItem::Kept(_, t)) => Some(Cow::Borrowed(&t)),
-            Some(CtxItem::Replaced(_, t)) => Some(Cow::Borrowed(&t)),
+            Some(CtxItem::Kept(newvar, t)) => Some(Typed::from_thunk_and_type(
+                Thunk::from_value(Value::Var(newvar.clone())),
+                t.clone(),
+            )),
+            Some(CtxItem::Replaced(th, t)) => {
+                Some(Typed::from_thunk_and_type(th.clone(), t.clone()))
+            }
             None => None,
         }
     }
-    pub(crate) fn to_normalization_ctx(&self) -> NormalizationContext {
-        NormalizationContext(self.0.forget())
-    }
 }
 
 impl<T: Shift> Shift for CtxItem<T> {
diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs
index b3817dc..530762b 100644
--- a/dhall/src/core/thunk.rs
+++ b/dhall/src/core/thunk.rs
@@ -1,13 +1,15 @@
 use std::cell::{Ref, RefCell};
 use std::rc::Rc;
 
+use dhall_syntax::{ExprF, Label, X};
+
 use crate::core::context::NormalizationContext;
 use crate::core::context::TypecheckContext;
 use crate::core::value::Value;
 use crate::core::var::{AlphaVar, Shift, Subst};
 use crate::error::TypeError;
 use crate::phase::normalize::{
-    apply_any, normalize_whnf, InputSubExpr, OutputSubExpr,
+    apply_any, normalize_one_layer, normalize_whnf, InputSubExpr, OutputSubExpr,
 };
 use crate::phase::typecheck::mktype;
 use crate::phase::{Type, Typed};
@@ -25,6 +27,10 @@ use Marker::{NF, WHNF};
 enum ThunkInternal {
     /// Non-normalized value alongside a normalization context
     Unnormalized(NormalizationContext, InputSubExpr),
+    /// Partially normalized value whose subexpressions have been thunked (this is returned from
+    /// typechecking). Note that this is different from `Value::PartialExpr` because there is no
+    /// requirement of WHNF here.
+    PartialExpr(ExprF<Thunk, Label, X>),
     /// Partially normalized value.
     /// Invariant: if the marker is `NF`, the value must be fully normalized
     Value(Marker, Value),
@@ -57,6 +63,10 @@ impl ThunkInternal {
                     normalize_whnf(ctx.clone(), e.clone()),
                 )
             }
+            ThunkInternal::PartialExpr(e) => {
+                *self =
+                    ThunkInternal::Value(WHNF, normalize_one_layer(e.clone()))
+            }
             // Already at least in WHNF
             ThunkInternal::Value(_, _) => {}
         }
@@ -64,7 +74,8 @@ impl ThunkInternal {
 
     fn normalize_nf(&mut self) {
         match self {
-            ThunkInternal::Unnormalized(_, _) => {
+            ThunkInternal::Unnormalized(_, _)
+            | ThunkInternal::PartialExpr(_) => {
                 self.normalize_whnf();
                 self.normalize_nf();
             }
@@ -80,7 +91,8 @@ impl ThunkInternal {
     // Always use normalize_whnf before
     fn as_whnf(&self) -> &Value {
         match self {
-            ThunkInternal::Unnormalized(_, _) => unreachable!(),
+            ThunkInternal::Unnormalized(_, _)
+            | ThunkInternal::PartialExpr(_) => unreachable!(),
             ThunkInternal::Value(_, v) => v,
         }
     }
@@ -88,8 +100,9 @@ impl ThunkInternal {
     // Always use normalize_nf before
     fn as_nf(&self) -> &Value {
         match self {
-            ThunkInternal::Unnormalized(_, _) => unreachable!(),
-            ThunkInternal::Value(WHNF, _) => unreachable!(),
+            ThunkInternal::Unnormalized(_, _)
+            | ThunkInternal::PartialExpr(_)
+            | ThunkInternal::Value(WHNF, _) => unreachable!(),
             ThunkInternal::Value(NF, v) => v,
         }
     }
@@ -108,6 +121,10 @@ impl Thunk {
         Thunk::new(NormalizationContext::new(), e.absurd())
     }
 
+    pub(crate) fn from_partial_expr(e: ExprF<Thunk, Label, X>) -> Thunk {
+        ThunkInternal::PartialExpr(e).into_thunk()
+    }
+
     // Normalizes contents to normal form; faster than `normalize_nf` if
     // no one else shares this thunk
     pub(crate) fn normalize_mut(&mut self) {
@@ -122,7 +139,8 @@ impl Thunk {
     fn do_normalize_whnf(&self) {
         let borrow = self.0.borrow();
         match &*borrow {
-            ThunkInternal::Unnormalized(_, _) => {
+            ThunkInternal::Unnormalized(_, _)
+            | ThunkInternal::PartialExpr(_) => {
                 drop(borrow);
                 self.0.borrow_mut().normalize_whnf();
             }
@@ -135,6 +153,7 @@ impl Thunk {
         let borrow = self.0.borrow();
         match &*borrow {
             ThunkInternal::Unnormalized(_, _)
+            | ThunkInternal::PartialExpr(_)
             | ThunkInternal::Value(WHNF, _) => {
                 drop(borrow);
                 self.0.borrow_mut().normalize_nf();
@@ -249,6 +268,14 @@ impl Shift for ThunkInternal {
             ThunkInternal::Unnormalized(ctx, e) => {
                 ThunkInternal::Unnormalized(ctx.shift(delta, var), e.clone())
             }
+            ThunkInternal::PartialExpr(e) => ThunkInternal::PartialExpr(
+                e.map_ref_with_special_handling_of_binders(
+                    |v| v.shift(delta, var),
+                    |x, v| v.shift(delta, &var.shift(1, &x.into())),
+                    X::clone,
+                    Label::clone,
+                ),
+            ),
             ThunkInternal::Value(m, v) => {
                 ThunkInternal::Value(*m, v.shift(delta, var))
             }
@@ -278,6 +305,19 @@ impl Subst<Typed> for ThunkInternal {
                 ctx.subst_shift(var, val),
                 e.clone(),
             ),
+            ThunkInternal::PartialExpr(e) => ThunkInternal::PartialExpr(
+                e.map_ref_with_special_handling_of_binders(
+                    |v| v.subst_shift(var, val),
+                    |x, v| {
+                        v.subst_shift(
+                            &var.shift(1, &x.into()),
+                            &val.shift(1, &x.into()),
+                        )
+                    },
+                    X::clone,
+                    Label::clone,
+                ),
+            ),
             ThunkInternal::Value(_, v) => {
                 // The resulting value may not stay in normal form after substitution
                 ThunkInternal::Value(WHNF, v.subst_shift(var, val))
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index b163af6..ecc2d85 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -341,23 +341,34 @@ enum Ret {
 }
 
 /// Type-check an expression and return the expression alongside its type if type-checking
-/// succeeded, or an error if type-checking failed
+/// succeeded, or an error if type-checking failed.
+/// Some normalization is done while typechecking, so the returned expression might be partially
+/// normalized as well.
 fn type_with(
     ctx: &TypecheckContext,
     e: SubExpr<Span, Normalized>,
 ) -> Result<Typed, TypeError> {
     use dhall_syntax::ExprF::{
-        Annot, App, Embed, Lam, Let, OldOptionalLit, Pi, SomeLit,
+        Annot, App, Embed, Lam, Let, OldOptionalLit, Pi, SomeLit, Var,
     };
 
     use Ret::*;
-    let ret = match e.as_ref() {
+    Ok(match e.as_ref() {
         Lam(x, t, b) => {
             let tx = mktype(ctx, t.clone())?;
             let ctx2 = ctx.insert_type(x, tx.clone());
             let b = type_with(&ctx2, b.clone())?;
+            let v = Value::Lam(
+                x.clone().into(),
+                TypeThunk::from_type(tx.clone()),
+                b.to_thunk(),
+            );
             let tb = b.get_type()?.into_owned();
-            Ok(RetTypeIntermediate(TypeIntermediate::Pi(x.clone(), tx, tb)))
+            let ti = TypeIntermediate::Pi(x.clone(), tx, tb);
+            Typed::from_thunk_and_type(
+                Thunk::from_value(v),
+                ti.typecheck(ctx)?.to_type(),
+            )
         }
         Pi(x, ta, tb) => {
             let ta = mktype(ctx, ta.clone())?;
@@ -390,24 +401,44 @@ fn type_with(
             let e = e.rewrap(Annot(x, t));
             return type_with(ctx, e);
         }
-        Embed(p) => Ok(RetTyped(p.clone().into())),
-        _ => type_last_layer(
-            ctx,
+        Embed(p) => p.clone().into(),
+        Var(var) => match ctx.lookup(&var) {
+            Some(typed) => typed,
+            None => {
+                return Err(TypeError::new(
+                    ctx,
+                    TypeMessage::UnboundVariable(var.clone()),
+                ))
+            }
+        },
+        _ => {
             // Typecheck recursively all subexpressions
-            e.as_ref()
-                .traverse_ref_simple(|e| Ok(type_with(ctx, e.clone())?))?,
-        ),
-    }?;
-    Ok(match ret {
-        RetType(typ) => Typed::from_thunk_and_type(
-            Thunk::new(ctx.to_normalization_ctx(), e),
-            typ,
-        ),
-        RetTypeIntermediate(ti) => Typed::from_thunk_and_type(
-            Thunk::new(ctx.to_normalization_ctx(), e),
-            ti.typecheck(ctx)?.to_type(),
-        ),
-        RetTyped(tt) => tt,
+            let expr =
+                e.as_ref().traverse_ref_with_special_handling_of_binders(
+                    |e| type_with(ctx, e.clone()),
+                    |_, _| unreachable!(),
+                    |_| unreachable!(),
+                    |l| Ok(Label::clone(l)),
+                )?;
+            let ret = type_last_layer(ctx, &expr)?;
+            let ret = match ret {
+                RetTypeIntermediate(ti) => {
+                    RetType(ti.typecheck(ctx)?.to_type())
+                }
+                ret => ret,
+            };
+            match ret {
+                RetTypeIntermediate(_) => unreachable!(),
+                RetType(typ) => {
+                    let expr = expr.map_ref_simple(|typed| typed.to_thunk());
+                    Typed::from_thunk_and_type(
+                        Thunk::from_partial_expr(expr),
+                        typ,
+                    )
+                }
+                RetTyped(tt) => tt,
+            }
+        }
     })
 }
 
@@ -415,7 +446,7 @@ fn type_with(
 /// layer.
 fn type_last_layer(
     ctx: &TypecheckContext,
-    e: ExprF<Typed, Label, Normalized>,
+    e: &ExprF<Typed, Label, X>,
 ) -> Result<Ret, TypeError> {
     use crate::error::TypeMessage::*;
     use dhall_syntax::BinOp::*;
@@ -429,10 +460,7 @@ fn type_last_layer(
         Pi(_, _, _) => unreachable!(),
         Let(_, _, _, _) => unreachable!(),
         Embed(_) => unreachable!(),
-        Var(var) => match ctx.lookup(&var) {
-            Some(e) => Ok(RetType(e.into_owned())),
-            None => Err(mkerr(UnboundVariable(var.clone()))),
-        },
+        Var(_) => unreachable!(),
         App(f, a) => {
             let tf = f.get_type()?;
             let tf_internal = tf.internal_whnf();
@@ -448,7 +476,11 @@ fn type_last_layer(
                 _ => return Err(mkerr(NotAFunction(f.clone()))),
             };
             ensure_equal!(a.get_type()?, tx, {
-                mkerr(TypeMismatch(f.clone(), tx.clone().to_normalized(), a))
+                mkerr(TypeMismatch(
+                    f.clone(),
+                    tx.clone().to_normalized(),
+                    a.clone(),
+                ))
             });
 
             Ok(RetType(tb.subst_shift(&x.into(), &a)))
@@ -458,7 +490,7 @@ fn type_last_layer(
             ensure_equal!(
                 &t,
                 x.get_type()?,
-                mkerr(AnnotMismatch(x, t.to_normalized()))
+                mkerr(AnnotMismatch(x.clone(), t.to_normalized()))
             );
             Ok(RetType(x.get_type()?.into_owned()))
         }
@@ -466,23 +498,23 @@ fn type_last_layer(
             ensure_equal!(
                 x.get_type()?,
                 &builtin_to_type(Bool)?,
-                mkerr(InvalidPredicate(x)),
+                mkerr(InvalidPredicate(x.clone())),
             );
 
             ensure_simple_type!(
                 y.get_type()?,
-                mkerr(IfBranchMustBeTerm(true, y)),
+                mkerr(IfBranchMustBeTerm(true, y.clone())),
             );
 
             ensure_simple_type!(
                 z.get_type()?,
-                mkerr(IfBranchMustBeTerm(false, z)),
+                mkerr(IfBranchMustBeTerm(false, z.clone())),
             );
 
             ensure_equal!(
                 y.get_type()?,
                 z.get_type()?,
-                mkerr(IfBranchMismatch(y, z))
+                mkerr(IfBranchMismatch(y.clone(), z.clone()))
             );
 
             Ok(RetType(y.get_type()?.into_owned()))
@@ -492,7 +524,7 @@ fn type_last_layer(
             Ok(RetTypeIntermediate(TypeIntermediate::ListType(t)))
         }
         NEListLit(xs) => {
-            let mut iter = xs.into_iter().enumerate();
+            let mut iter = xs.iter().enumerate();
             let (_, x) = iter.next().unwrap();
             for (i, y) in iter {
                 ensure_equal!(
@@ -501,7 +533,7 @@ fn type_last_layer(
                     mkerr(InvalidListElement(
                         i,
                         x.get_type()?.to_normalized(),
-                        y
+                        y.clone()
                     ))
                 );
             }
@@ -514,17 +546,17 @@ fn type_last_layer(
         }
         RecordType(kts) => {
             let kts: BTreeMap<_, _> = kts
-                .into_iter()
-                .map(|(x, t)| Ok((x, t.to_type())))
+                .iter()
+                .map(|(x, t)| Ok((x.clone(), t.to_type())))
                 .collect::<Result<_, _>>()?;
             Ok(RetTyped(TypeIntermediate::RecordType(kts).typecheck(ctx)?))
         }
         UnionType(kts) => {
             let kts: BTreeMap<_, _> = kts
-                .into_iter()
+                .iter()
                 .map(|(x, t)| {
                     Ok((
-                        x,
+                        x.clone(),
                         match t {
                             None => None,
                             Some(t) => Some(t.to_type()),
@@ -536,24 +568,24 @@ fn type_last_layer(
         }
         RecordLit(kvs) => {
             let kts = kvs
-                .into_iter()
-                .map(|(x, v)| Ok((x, v.get_type()?.into_owned())))
+                .iter()
+                .map(|(x, v)| Ok((x.clone(), v.get_type()?.into_owned())))
                 .collect::<Result<_, _>>()?;
             Ok(RetTypeIntermediate(TypeIntermediate::RecordType(kts)))
         }
         UnionLit(x, v, kvs) => {
             let mut kts: std::collections::BTreeMap<_, _> = kvs
-                .into_iter()
+                .iter()
                 .map(|(x, v)| {
                     let t = match v {
                         Some(x) => Some(x.to_type()),
                         None => None,
                     };
-                    Ok((x, t))
+                    Ok((x.clone(), t))
                 })
                 .collect::<Result<_, _>>()?;
             let t = v.get_type()?.into_owned();
-            kts.insert(x, Some(t));
+            kts.insert(x.clone(), Some(t));
             Ok(RetTypeIntermediate(TypeIntermediate::UnionType(kts)))
         }
         Field(r, x) => {
@@ -562,7 +594,8 @@ fn type_last_layer(
                     Some(tth) => {
                         Ok(RetType(tth.to_type(ctx)?))
                     },
-                    None => Err(mkerr(MissingRecordField(x, r.clone()))),
+                    None => Err(mkerr(MissingRecordField(x.clone(),
+                                        r.clone()))),
                 },
                 // TODO: branch here only when r.get_type() is a Const
                 _ => {
@@ -584,14 +617,14 @@ fn type_last_layer(
                             },
                             None => {
                                 Err(mkerr(MissingUnionField(
-                                    x,
+                                    x.clone(),
                                     r.to_normalized(),
                                 )))
                             },
                         },
                         _ => {
                             Err(mkerr(NotARecord(
-                                x,
+                                x.clone(),
                                 r.to_normalized()
                             )))
                         },
@@ -603,9 +636,9 @@ fn type_last_layer(
                 // ))),
             }
         }
-        Const(c) => Ok(RetTyped(Typed::from_const(c))),
+        Const(c) => Ok(RetTyped(Typed::from_const(*c))),
         Builtin(b) => {
-            Ok(RetType(mktype(ctx, rc(type_of_builtin(b)).absurd())?))
+            Ok(RetType(mktype(ctx, rc(type_of_builtin(*b)).absurd())?))
         }
         BoolLit(_) => Ok(RetType(builtin_to_type(Bool)?)),
         NaturalLit(_) => Ok(RetType(builtin_to_type(Natural)?)),
@@ -628,13 +661,13 @@ fn type_last_layer(
         BinOp(o @ ListAppend, l, r) => {
             match l.get_type()?.internal_whnf() {
                 Some(Value::AppliedBuiltin(List, _)) => {}
-                _ => return Err(mkerr(BinOpTypeMismatch(o, l.clone()))),
+                _ => return Err(mkerr(BinOpTypeMismatch(*o, l.clone()))),
             }
 
             ensure_equal!(
                 l.get_type()?,
                 r.get_type()?,
-                mkerr(BinOpTypeMismatch(o, r))
+                mkerr(BinOpTypeMismatch(*o, r.clone()))
             );
 
             Ok(RetType(l.get_type()?.into_owned()))
@@ -652,9 +685,17 @@ fn type_last_layer(
                 _ => return Err(mkerr(Unimplemented)),
             })?;
 
-            ensure_equal!(l.get_type()?, &t, mkerr(BinOpTypeMismatch(o, l)));
+            ensure_equal!(
+                l.get_type()?,
+                &t,
+                mkerr(BinOpTypeMismatch(*o, l.clone()))
+            );
 
-            ensure_equal!(r.get_type()?, &t, mkerr(BinOpTypeMismatch(o, r)));
+            ensure_equal!(
+                r.get_type()?,
+                &t,
+                mkerr(BinOpTypeMismatch(*o, r.clone()))
+            );
 
             Ok(RetType(t))
         }
-- 
cgit v1.2.3