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/normalize.rs | 54 ++++++++++++++++++++++++++++++++++----------------
 1 file changed, 37 insertions(+), 17 deletions(-)

(limited to 'dhall/src/normalize.rs')

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))
     }
 }
 
-- 
cgit v1.2.3