From 5ceacacf9cbbe1e567a73599e0ba7759e908f50d Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Thu, 30 Nov 2023 11:22:31 -0600
Subject: [PATCH] ok kinda works?

---
 bidir/src/bidir_debruijn.rs | 57 +++++++++++++++++++++++++++++++++----
 bidir/src/data_debruijn.rs  |  9 ++++--
 2 files changed, 58 insertions(+), 8 deletions(-)

diff --git a/bidir/src/bidir_debruijn.rs b/bidir/src/bidir_debruijn.rs
index 615feec..7b6b90b 100644
--- a/bidir/src/bidir_debruijn.rs
+++ b/bidir/src/bidir_debruijn.rs
@@ -19,8 +19,14 @@ pub fn app_ctx(ctx: &Context, ty: &Type) -> Result<Type> {
       None => bail!("existential variable {a:?} doesn't exist in context"),
     },
 
+    // TODO: Is this right?
+    // Type::Polytype(t) => {
+    //   let t = app_ctx(ctx, t)?;
+    //   Ok(Type::Polytype(Box::new(t)))
+    // }
     Type::Polytype(t) => {
-      let t = app_ctx(ctx, t)?;
+      let (aug_ctx, _) = ctx.add(ContextEntry::ExistentialVar)?;
+      let t = app_ctx(&aug_ctx, t)?;
       Ok(Type::Polytype(Box::new(t)))
     }
 
@@ -56,8 +62,12 @@ pub fn subtype(ctx: &Context, left: &Type, right: &Type) -> Result<Context> {
       instantiate_left(ctx, a, ty_a)
     }
 
+    // <:InstantiateR
+    (ty_a, Type::Existential(a)) if ctx.get_existential(a).is_some() => {
+      instantiate_right (ctx, ty_a, a)
+    }
+
     (Type::Unit, Type::Var(_)) => todo!("wtf? {left:?} {right:?}"),
-    (Type::Unit, Type::Existential(_)) => todo!(),
     (Type::Unit, Type::Polytype(_)) => todo!(),
     (Type::Unit, Type::Arrow(_, _)) => todo!(),
     (Type::Var(_), Type::Unit) => todo!(),
@@ -125,6 +135,39 @@ pub fn instantiate_left(
   }
 }
 
+pub fn instantiate_right(
+  ctx: &Context,
+  ty_a: &Type,
+  a: &ContextIndex,
+) -> Result<Context> {
+  match ty_a {
+    // InstRSolve rule
+    ty if ty.is_mono() => {
+      let mut new_ctx = ctx.clone();
+      {
+        let a_entry = new_ctx
+          .vector
+          .get_mut(a.debruijn_level)
+          .expect("should exist");
+
+        ensure!(
+          matches!(a_entry, ContextEntry::ExistentialVar),
+          "not an existential variable"
+        );
+
+        *a_entry = ContextEntry::ExistentialSolved(ty.try_into_mono().unwrap());
+      }
+      Ok(new_ctx)
+    }
+
+    Type::Unit => todo!("a={a:?}, ty_a={ty_a:?}, ctx={ctx:?}"),
+    Type::Var(_) => todo!(),
+    Type::Existential(_) => todo!(),
+    Type::Polytype(_) => todo!(),
+    Type::Arrow(_, _) => todo!(),
+  }
+}
+
 // Figure 11. Algorithmic typing
 
 #[trace]
@@ -216,11 +259,15 @@ pub fn synthesize(ctx: &Context, term: &Term) -> Result<(Type, Context)> {
         }
       }
       let after_marker =
-        after_marker.transform_with_visitor(&V2(0, after_marker.size()))?;
+        after_marker.transform_with_visitor(&V2(1, after_marker.size()))?;
 
-      let tau = Type::Arrow(Box::new(ex_a_2), Box::new(ex_b));
-      let tau = app_ctx(&after_marker, &tau)?;
+      // τ=[∆'](â→β)
+      let tau = Type::Arrow(Box::new(ex_a_2), Box::new(ex_b_2));
       let tau = tau.transform_with_visitor(&V2(1, after_marker.size()))?;
+      let tau = app_ctx(&after_marker, &tau)?;
+
+      // let mut before_marker = before_marker;
+      // before_marker.vector.push_back(ContextEntry::ExistentialVar);
 
       Ok((Type::Polytype(Box::new(tau)), before_marker))
     }
diff --git a/bidir/src/data_debruijn.rs b/bidir/src/data_debruijn.rs
index 3441e2a..a3cba28 100644
--- a/bidir/src/data_debruijn.rs
+++ b/bidir/src/data_debruijn.rs
@@ -74,7 +74,7 @@ impl fmt::Debug for Type {
     match self {
       Self::Unit => write!(f, "𝟙"),
       Self::Var(arg0) => write!(f, "{:?}", arg0),
-      Self::Existential(arg0) => write!(f, "{:?}", arg0),
+      Self::Existential(arg0) => write!(f, "ex{:?}", arg0),
       Self::Polytype(arg1) => write!(f, "(∀.{:?})", arg1),
       Self::Arrow(arg0, arg1) => write!(f, "({:?} -> {:?})", arg0, arg1),
     }
@@ -316,7 +316,9 @@ impl Context {
 
   /// Splits the context
   pub fn split_at(&self, index: &ContextIndex) -> (Context, Context) {
-    let (before, after) = self.vector.clone().split_at(index.debruijn_level);
+    let (before, mut after) =
+      self.vector.clone().split_at(index.debruijn_level);
+    after.pop_front();
 
     (Context { vector: before }, Context { vector: after })
   }
@@ -432,11 +434,12 @@ pub fn convert_term(term: &data::Term) -> Term {
       data::Term::Unit => Term::Unit,
 
       data::Term::Var(name) => {
+        println!("Looking up name {name}");
         let (idx, _) = ctx.lookup_type(name).unwrap();
 
         let index = ContextIndex {
           debruijn_index: 0,
-          debruijn_level: ctx.0.len(),
+          debruijn_level: idx,
         };
         Term::Var(index)
       }