From ecff0ecd47bb38937fb43e60b8d78ea92e2af01c Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 21 Apr 2019 22:52:00 +0200
Subject: Prepare for interop between two contexts

---
 dhall/src/lib.rs       |  1 +
 dhall/src/normalize.rs | 54 ++++++++++++++++++++++++++++++--------------
 dhall/src/typecheck.rs | 61 +++++++++++++++++++++++++++++++++++++++++++-------
 3 files changed, 91 insertions(+), 25 deletions(-)

(limited to 'dhall')

diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
index c85b962..3860890 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -4,6 +4,7 @@
 #![feature(label_break_value)]
 #![feature(non_exhaustive)]
 #![feature(bind_by_move_pattern_guards)]
+#![feature(try_trait)]
 #![cfg_attr(test, feature(custom_inner_attributes))]
 #![allow(
     clippy::type_complexity,
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 7aa8686..c17ed78 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -229,7 +229,21 @@ fn apply_builtin(b: Builtin, args: Vec<WHNF>) -> WHNF {
 #[derive(Debug, Clone)]
 enum EnvItem {
     Expr(WHNF),
-    Skip(usize),
+    Skip(V<Label>),
+}
+
+impl EnvItem {
+    fn shift0(&self, delta: isize, x: &Label) -> Self {
+        use EnvItem::*;
+        match self {
+            Expr(e) => {
+                let mut e = e.clone();
+                e.shift0(delta, x);
+                Expr(e)
+            }
+            Skip(var) => Skip(var.shift0(delta, x)),
+        }
+    }
 }
 
 #[derive(Debug, Clone)]
@@ -247,30 +261,36 @@ impl NormalizationContext {
     fn skip(&self, x: &Label) -> Self {
         NormalizationContext(Rc::new(
             self.0
-                .map(|l, e| {
-                    use EnvItem::*;
-                    match e {
-                        Expr(e) => {
-                            let mut e = e.clone();
-                            e.shift0(1, x);
-                            Expr(e)
-                        }
-                        Skip(n) if l == x => Skip(*n + 1),
-                        Skip(n) => Skip(*n),
-                    }
-                })
-                .insert(x.clone(), EnvItem::Skip(0)),
+                .map(|_, e| e.shift0(1, x))
+                .insert(x.clone(), EnvItem::Skip(V(x.clone(), 0))),
         ))
     }
     fn lookup(&self, var: &V<Label>) -> WHNF {
         let V(x, n) = var;
         match self.0.lookup(x, *n) {
             Some(EnvItem::Expr(e)) => e.clone(),
-            Some(EnvItem::Skip(m)) => {
-                WHNF::Expr(rc(ExprF::Var(V(x.clone(), *m))))
+            Some(EnvItem::Skip(newvar)) => {
+                WHNF::Expr(rc(ExprF::Var(newvar.clone())))
+            }
+            None => WHNF::Expr(rc(ExprF::Var(var.clone()))),
+        }
+    }
+    fn from_typecheck_ctx(tc_ctx: &crate::typecheck::TypecheckContext) -> Self {
+        use crate::typecheck::EnvItem::*;
+        let mut ctx = Context::new();
+        for (k, vs) in tc_ctx.0.iter_keys() {
+            for v in vs.iter().rev() {
+                let new_item = match v {
+                    Type(var, _) => EnvItem::Skip(var.clone()),
+                    Value(e) => EnvItem::Expr(normalize_whnf(
+                        NormalizationContext::new(),
+                        e.as_expr().embed_absurd(),
+                    )),
+                };
+                ctx = ctx.insert(k.clone(), new_item);
             }
-            None => WHNF::Expr(rc(ExprF::Var(V(x.clone(), *n)))),
         }
+        NormalizationContext(Rc::new(ctx))
     }
 }
 
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index a183944..e3ec849 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -3,6 +3,7 @@ use std::borrow::Borrow;
 use std::borrow::Cow;
 use std::fmt;
 use std::marker::PhantomData;
+use std::rc::Rc;
 
 use crate::expr::*;
 use crate::traits::DynamicType;
@@ -138,18 +139,56 @@ impl<'a> TypeInternal<'a> {
 }
 
 #[derive(Debug, Clone)]
-pub(crate) struct TypecheckContext(Context<Label, Type<'static>>);
+pub(crate) enum EnvItem {
+    Type(V<Label>, Type<'static>),
+    Value(Normalized<'static>),
+}
+
+impl EnvItem {
+    fn shift0(&self, delta: isize, x: &Label) -> Self {
+        use EnvItem::*;
+        match self {
+            Type(v, e) => Type(v.shift0(delta, x), e.shift0(delta, x)),
+            Value(e) => Value(e.shift0(delta, x)),
+        }
+    }
+}
+
+#[derive(Debug, Clone)]
+pub(crate) struct TypecheckContext(pub(crate) Context<Label, EnvItem>);
 
 impl TypecheckContext {
     pub(crate) fn new() -> Self {
         TypecheckContext(Context::new())
     }
-    pub(crate) fn insert_and_shift(&self, x: &Label, t: Type<'static>) -> Self {
-        TypecheckContext(self.0.insert(x.clone(), t).map(|_, e| e.shift0(1, x)))
+    pub(crate) fn insert_type(&self, x: &Label, t: Type<'static>) -> Self {
+        TypecheckContext(
+            self.0
+                .insert(x.clone(), EnvItem::Type(V(x.clone(), 0), t))
+                .map(|_, e| e.shift0(1, x)),
+        )
+    }
+    pub(crate) fn insert_value(
+        &self,
+        x: &Label,
+        t: Normalized<'static>,
+    ) -> Self {
+        TypecheckContext(
+            self.0
+                .insert(x.clone(), EnvItem::Value(t))
+                .map(|_, e| e.shift0(1, x)),
+        )
     }
-    pub(crate) fn lookup(&self, var: &V<Label>) -> Option<&Type<'static>> {
+    pub(crate) fn lookup(
+        &self,
+        var: &V<Label>,
+    ) -> Option<Cow<'_, Type<'static>>> {
         let V(x, n) = var;
-        self.0.lookup(x, *n)
+        match self.0.lookup(x, *n) {
+            Some(EnvItem::Type(_, t)) => Some(Cow::Borrowed(&t)),
+            Some(EnvItem::Value(t)) => Some(t.get_type()?),
+            None => None,
+        }
     }
 }
 
@@ -416,7 +455,7 @@ fn type_with(
     let ret = match e.as_ref() {
         Lam(x, t, b) => {
             let t = mktype(ctx, t.clone())?;
-            let ctx2 = ctx.insert_and_shift(x, t.clone());
+            let ctx2 = ctx.insert_type(x, t.clone());
             let b = type_with(&ctx2, b.clone())?;
             Ok(RetExpr(Pi(
                 x.clone(),
@@ -431,7 +470,7 @@ fn type_with(
                 mkerr(InvalidInputType(ta.into_normalized()?)),
             );
 
-            let ctx2 = ctx.insert_and_shift(x, ta.clone());
+            let ctx2 = ctx.insert_type(x, ta.clone());
             let tb = type_with(&ctx2, tb.clone())?;
             let kB = ensure_is_const!(
                 &tb.get_type()?,
@@ -507,7 +546,7 @@ fn type_last_layer(
         Let(_, _, _, _) => unreachable!(),
         Embed(_) => unreachable!(),
         Var(var) => match ctx.lookup(&var) {
-            Some(e) => Ok(RetType(e.clone())),
+            Some(e) => Ok(RetType(e.into_owned())),
             None => Err(mkerr(UnboundVariable)),
         },
         App(f, a) => {
@@ -808,6 +847,12 @@ impl TypeError {
     }
 }
 
+impl From<TypeError> for std::option::NoneError {
+    fn from(_: TypeError) -> std::option::NoneError {
+        std::option::NoneError
+    }
+}
+
 impl ::std::error::Error for TypeMessage<'static> {
     fn description(&self) -> &str {
         match *self {
-- 
cgit v1.2.3