fmt

bidir/src/bidir.rs

@@ -18,7 +18,9 @@ pub fn app_ctx(ctx: &Context, ty: &Type) -> Result<Type> {
       None => bail!("existential variable {a} doesn't exist in context"),
     },
 
-    Type::Polytype(a, t) => Ok(Type::Polytype(a.clone(), Box::new(app_ctx(ctx, t)?))),
+    Type::Polytype(a, t) => {
+      Ok(Type::Polytype(a.clone(), Box::new(app_ctx(ctx, t)?)))
+    }
 
     Type::Arrow(a, b) => Ok(Type::Arrow(
       Box::new(app_ctx(ctx, a)?),
@@ -90,20 +92,30 @@ pub fn subtype(ctx: &Context, left: &Type, right: &Type) -> Result<Context> {
 // Figure 10. Instantiation
 
 #[cfg_attr(feature = "trace_execution", trace)]
-pub fn instantiate_left(ctx: &Context, a: &str, ty_a: &Type) -> Result<Context> {
+pub fn instantiate_left(
+  ctx: &Context,
+  a: &str,
+  ty_a: &Type,
+) -> Result<Context> {
   match ty_a {
     // InstLReach rule
-    Type::Existential(b) if ctx.has_existential(a) && ctx.has_existential(b) => {
+    Type::Existential(b)
+      if ctx.has_existential(a) && ctx.has_existential(b) =>
+    {
       let mut new_ctx = ctx.clone();
       {
         let b_entry = new_ctx
           .0
           .iter_mut()
-          .find(|entry| matches!(entry, ContextEntry::ExistentialVar(x) if x == b))
+          .find(
+            |entry| matches!(entry, ContextEntry::ExistentialVar(x) if x == b),
+          )
           .expect("should exist");
 
-        *b_entry =
+        *b_entry = ContextEntry::ExistentialSolved(
-          ContextEntry::ExistentialSolved(b.to_owned(), Monotype::Existential(a.to_owned()));
+          b.to_owned(),
+          Monotype::Existential(a.to_owned()),
+        );
       }
 
       Ok(new_ctx)
@@ -119,14 +131,19 @@ pub fn instantiate_left(ctx: &Context, a: &str, ty_a: &Type) -> Result<Context>
 }
 
 #[cfg_attr(feature = "trace_execution", trace)]
-pub fn instantiate_right(ctx: &Context, ty_a: &Type, a: &str) -> Result<Context> {
+pub fn instantiate_right(
+  ctx: &Context,
+  ty_a: &Type,
+  a: &str,
+) -> Result<Context> {
   match ty_a {
     // InstRArr
     Type::Arrow(ty_a1, ty_a2) if ctx.has_existential(a) => {
       // TODO: In case it's already solved?
       println!("original ctx: {ctx:?}");
 
-      let (ex_a1_s, ex_a2_s, ctx_gamma_aug) = ctx.split_existential_function(a)?;
+      let (ex_a1_s, ex_a2_s, ctx_gamma_aug) =
+        ctx.split_existential_function(a)?;
 
       let ctx_theta = instantiate_left(&ctx_gamma_aug, &ex_a1_s, &ty_a1)?;
 
@@ -148,7 +165,9 @@ pub fn instantiate_right(ctx: &Context, ty_a: &Type, a: &str) -> Result<Context>
       let out_ctx = instantiate_right(&aug_ctx, &aug_b, a)?;
 
       let (before, after) = out_ctx
-        .split_by(|entry| matches!(entry, ContextEntry::Marker(m) if *m == ex_b))
+        .split_by(
+          |entry| matches!(entry, ContextEntry::Marker(m) if *m == ex_b),
+        )
         .unwrap();
 
       Ok(before)
@@ -259,7 +278,8 @@ pub fn synthesize(ctx: &Context, term: &Term) -> Result<(Type, Context)> {
         .unwrap();
       info!("Unsolved: {:?}", after_marker.unsolved_existentials());
 
-      let mut tau = app_ctx(&after_marker, &Type::Arrow(Box::new(ex_a), Box::new(ex_b)))?;
+      let mut tau =
+        app_ctx(&after_marker, &Type::Arrow(Box::new(ex_a), Box::new(ex_b)))?;
       for name in after_marker.unsolved_existentials() {
         warn!("substituting {tau:?} looking for {name}");
         tau = tau.subst(&name, &Type::Var(ex_gen.clone()));
@@ -300,7 +320,11 @@ pub fn synthesize(ctx: &Context, term: &Term) -> Result<(Type, Context)> {
 }
 
 #[cfg_attr(feature = "trace_execution", trace)]
-pub fn app_synthesize(ctx: &Context, fun_ty: &Type, term: &Term) -> Result<(Type, Context)> {
+pub fn app_synthesize(
+  ctx: &Context,
+  fun_ty: &Type,
+  term: &Term,
+) -> Result<(Type, Context)> {
   match (fun_ty, term) {
     // →App rule
     (Type::Arrow(ty_a, ty_c), e) => {
@@ -322,7 +346,8 @@ pub fn app_synthesize(ctx: &Context, fun_ty: &Type, term: &Term) -> Result<(Type
 
     // âApp rule
     (Type::Existential(a), e) if ctx.has_existential(a) => {
-      let (ex_a1_s, ex_a2_s, ctx_gamma_aug) = ctx.split_existential_function(a)?;
+      let (ex_a1_s, ex_a2_s, ctx_gamma_aug) =
+        ctx.split_existential_function(a)?;
 
       let ex_a1 = Type::Existential(ex_a1_s.clone());
       let ctx_delta = typecheck(&ctx_gamma_aug, e, &ex_a1)?;

bidir/src/bidir_debruijn.rs

@@ -0,0 +1,39 @@
+use anyhow::{bail, Result};
+
+use crate::data_debruijn::{Context, Term, Type};
+
+// Figure 8. Applying a context, as a substitution, to a type
+
+pub fn app_ctx(ctx: &Context, ty: &Type) -> Result<Type> {
+  match ty {
+    Type::Unit => Ok(Type::Unit),
+    Type::Var(s) => Ok(Type::Var(s.clone())),
+
+    Type::Existential(a) => match ctx.lookup_existential(a) {
+      Some((_, Some(m))) => Ok(m.into_poly()),
+      Some((_, None)) => Ok(Type::Existential(a.clone())),
+      None => bail!("existential variable {a} doesn't exist in context"),
+    },
+
+    Type::Polytype(a, t) => {
+      Ok(Type::Polytype(a.clone(), Box::new(app_ctx(ctx, t)?)))
+    }
+
+    Type::Arrow(a, b) => Ok(Type::Arrow(
+      Box::new(app_ctx(ctx, a)?),
+      Box::new(app_ctx(ctx, b)?),
+    )),
+  }
+}
+
+pub fn synthesize(ctx: &Context, term: &Term) -> Result<(Type, Context)> {
+  match term {
+    // 1I⇒ rule
+    Term::Unit => Ok((Type::Unit, ctx.clone())),
+
+    Term::Var(_) => todo!(),
+    Term::Lam(_) => todo!(),
+    Term::App(_, _) => todo!(),
+    Term::Annot(_, _) => todo!(),
+  }
+}

bidir/src/convert_data.rs

@@ -2,7 +2,10 @@ use crate::DEPTH;
 use crate::{data, data_debruijn, gensym::gensym_type};
 
 pub fn convert_term(term: &data::Term) -> data_debruijn::Term {
-  fn convert_term_with_context(ctx: &data::Context, term: &data::Term) -> data_debruijn::Term {
+  fn convert_term_with_context(
+    ctx: &data::Context,
+    term: &data::Term,
+  ) -> data_debruijn::Term {
     match term {
       data::Term::Unit => data_debruijn::Term::Unit,
 
@@ -36,7 +39,10 @@ pub fn convert_term(term: &data::Term) -> data_debruijn::Term {
     }
   }
 
-  fn convert_ty_with_context(ctx: &data::Context, ty: &data::Type) -> data_debruijn::Type {
+  fn convert_ty_with_context(
+    ctx: &data::Context,
+    ty: &data::Type,
+  ) -> data_debruijn::Type {
     match ty {
       data::Type::Unit => data_debruijn::Type::Unit,
 

bidir/src/data.rs

@@ -80,10 +80,15 @@ impl Type {
         Type::Unit => HashSet::default(),
         Type::Var(x) if ctx.lookup_type(x).is_some() => HashSet::default(),
         Type::Var(x) => [FreeVar::Var(x.to_owned())].into_iter().collect(),
-        Type::Existential(x) if ctx.lookup_existential(x).is_some() => HashSet::default(),
+        Type::Existential(x) if ctx.lookup_existential(x).is_some() => {
-        Type::Existential(x) => [FreeVar::Existential(x.to_owned())].into_iter().collect(),
+          HashSet::default()
+        }
+        Type::Existential(x) => {
+          [FreeVar::Existential(x.to_owned())].into_iter().collect()
+        }
         Type::Polytype(x, ty_a) => {
-          let new_ctx = ctx.add(vec![ContextEntry::ExistentialVar(x.to_owned())]);
+          let new_ctx =
+            ctx.add(vec![ContextEntry::ExistentialVar(x.to_owned())]);
           free_vars_with_context(&new_ctx, &ty_a)
         }
         Type::Arrow(ty_a, ty_b) => {
@@ -104,7 +109,9 @@ impl Type {
       Type::Var(n) => Type::Var(n.clone()),
       Type::Existential(s) if s == var => replacement.clone(),
       Type::Existential(s) => Type::Existential(s.clone()),
-      Type::Polytype(a, t) => Type::Polytype(a.clone(), Box::new(t.subst(var, replacement))),
+      Type::Polytype(a, t) => {
+        Type::Polytype(a.clone(), Box::new(t.subst(var, replacement)))
+      }
       Type::Arrow(a, b) => Type::Arrow(
         Box::new(a.subst(var, replacement)),
         Box::new(b.subst(var, replacement)),
@@ -138,7 +145,9 @@ impl Monotype {
       Monotype::Unit => Type::Unit,
       Monotype::Var(x) => Type::Var(x.clone()),
       Monotype::Existential(x) => Type::Existential(x.clone()),
-      Monotype::Arrow(a, b) => Type::Arrow(Box::new(a.into_poly()), Box::new(b.into_poly())),
+      Monotype::Arrow(a, b) => {
+        Type::Arrow(Box::new(a.into_poly()), Box::new(b.into_poly()))
+      }
     }
   }
 }
@@ -202,7 +211,9 @@ impl Context {
       .iter()
       .enumerate()
       .find_map(|(i, entry)| match entry {
-        ContextEntry::TermAnnot(n, t) if n == name.as_ref() => Some((i, t.clone())),
+        ContextEntry::TermAnnot(n, t) if n == name.as_ref() => {
+          Some((i, t.clone()))
+        }
         _ => None,
       })
   }
@@ -216,14 +227,21 @@ impl Context {
   /// - Returns Some(Some(t)) if solved
   /// - Returns Some(None) if exists but unsolved
   /// - Returns None if not found
-  pub fn lookup_existential(&self, name: impl AsRef<str>) -> Option<(usize, Option<Monotype>)> {
+  pub fn lookup_existential(
+    &self,
+    name: impl AsRef<str>,
+  ) -> Option<(usize, Option<Monotype>)> {
     self
       .0
       .iter()
       .enumerate()
       .find_map(|(i, entry)| match entry {
-        ContextEntry::ExistentialVar(n) if n == name.as_ref() => Some((i, None)),
+        ContextEntry::ExistentialVar(n) if n == name.as_ref() => {
-        ContextEntry::ExistentialSolved(n, t) if n == name.as_ref() => Some((i, Some(t.clone()))),
+          Some((i, None))
+        }
+        ContextEntry::ExistentialSolved(n, t) if n == name.as_ref() => {
+          Some((i, Some(t.clone())))
+        }
         _ => None,
       })
   }
@@ -262,14 +280,21 @@ impl Context {
     Some((Context(before), Context(after)))
   }
 
-  pub fn unsplit(left: &Context, center: ContextEntry, right: &Context) -> Context {
+  pub fn unsplit(
+    left: &Context,
+    center: ContextEntry,
+    right: &Context,
+  ) -> Context {
     let mut res = left.clone();
     res.0.push_back(center);
     res.0.extend(right.0.clone().into_iter());
     res
   }
 
-  pub fn split_existential_function(&self, var: &str) -> Result<(String, String, Context)> {
+  pub fn split_existential_function(
+    &self,
+    var: &str,
+  ) -> Result<(String, String, Context)> {
     let mut ctx = self.clone();
     let idx = match ctx.lookup_existential(var) {
       Some((idx, _)) => idx,

bidir/src/data_debruijn.rs

@@ -153,7 +153,9 @@ impl Monotype {
       Monotype::Unit => Type::Unit,
       Monotype::Var(x) => Type::Var(x.clone()),
       Monotype::Existential(x) => Type::Existential(x.clone()),
-      Monotype::Arrow(a, b) => Type::Arrow(Box::new(a.into_poly()), Box::new(b.into_poly())),
+      Monotype::Arrow(a, b) => {
+        Type::Arrow(Box::new(a.into_poly()), Box::new(b.into_poly()))
+      }
     }
   }
 }
@@ -217,7 +219,9 @@ impl Context {
       .iter()
       .enumerate()
       .find_map(|(i, entry)| match entry {
-        ContextEntry::TermAnnot(n, t) if n == name.as_ref() => Some((i, t.clone())),
+        ContextEntry::TermAnnot(n, t) if n == name.as_ref() => {
+          Some((i, t.clone()))
+        }
         _ => None,
       })
   }
@@ -231,14 +235,21 @@ impl Context {
   /// - Returns Some(Some(t)) if solved
   /// - Returns Some(None) if exists but unsolved
   /// - Returns None if not found
-  pub fn lookup_existential(&self, name: impl AsRef<str>) -> Option<(usize, Option<Monotype>)> {
+  pub fn lookup_existential(
+    &self,
+    name: impl AsRef<str>,
+  ) -> Option<(usize, Option<Monotype>)> {
     self
       .0
       .iter()
       .enumerate()
       .find_map(|(i, entry)| match entry {
-        ContextEntry::ExistentialVar(n) if n == name.as_ref() => Some((i, None)),
+        ContextEntry::ExistentialVar(n) if n == name.as_ref() => {
-        ContextEntry::ExistentialSolved(n, t) if n == name.as_ref() => Some((i, Some(t.clone()))),
+          Some((i, None))
+        }
+        ContextEntry::ExistentialSolved(n, t) if n == name.as_ref() => {
+          Some((i, Some(t.clone())))
+        }
         _ => None,
       })
   }
@@ -277,7 +288,11 @@ impl Context {
     Some((Context(before), Context(after)))
   }
 
-  pub fn unsplit(left: &Context, center: ContextEntry, right: &Context) -> Context {
+  pub fn unsplit(
+    left: &Context,
+    center: ContextEntry,
+    right: &Context,
+  ) -> Context {
     let mut res = left.clone();
     res.0.push_back(center);
     res.0.extend(right.0.clone().into_iter());

bidir/src/gensym.rs

@@ -6,13 +6,13 @@ thread_local! {
 }
 
 const EXISTENTIALS: [&'static str; 24] = [
-  "α", "β", "γ", "δ", "ε", "ζ", "η", "θ", "ι", "κ", "λ", "μ", "ν", "ξ", "ο", "π", "ρ", "σ", "τ",
+  "α", "β", "γ", "δ", "ε", "ζ", "η", "θ", "ι", "κ", "λ", "μ", "ν", "ξ", "ο",
-  "υ", "φ", "χ", "ψ", "ω",
+  "π", "ρ", "σ", "τ", "υ", "φ", "χ", "ψ", "ω",
 ];
 
 const TYPEVARS: [&'static str; 26] = [
-  "A", "B", "C", "D", "E", "F", "G", "H", "I", "J", "K", "L", "M", "N", "O", "P", "Q", "R", "S",
+  "A", "B", "C", "D", "E", "F", "G", "H", "I", "J", "K", "L", "M", "N", "O",
-  "T", "U", "V", "W", "X", "Y", "Z",
+  "P", "Q", "R", "S", "T", "U", "V", "W", "X", "Y", "Z",
 ];
 
 pub fn gensym_existential() -> String {

bidir/src/tests.rs

@@ -1,19 +1,23 @@
 use anyhow::{bail, Result};
 
 use crate::{
-  bidir::{app_ctx, synthesize},
+  bidir_debruijn::{app_ctx, synthesize},
-  data::{Context, Term},
+  convert_data::convert_term,
+  data_debruijn::Context,
+  data_debruijn::Term,
+  parser::TermParser,
 };
 
-macro_rules! id_term {
+fn term_of(str: &'static str) -> Result<Term> {
-  () => {
+  let term_parser = TermParser::new();
-    Term::Lam("x".to_owned(), Box::new(Term::Var("x".to_owned())))
+  let term = term_parser.parse(str)?;
-  };
+  let converted = convert_term(&term);
+  Ok(converted)
 }
 
 #[test]
 fn test_id() -> Result<()> {
-  let id = id_term!();
+  let id = term_of(r"\x.x")?;
   let ctx = Context::default();
   let (ty, out_ctx) = synthesize(&ctx, &id)?;
   bail!("Synthesized: {:?} (context = {:?})", ty, out_ctx);
@@ -23,8 +27,7 @@ fn test_id() -> Result<()> {
 
 #[test]
 fn test_id_of_unit() -> Result<()> {
-  let id = id_term!();
+  let id_of_unit = term_of(r"(\x.x) ()")?;
-  let id_of_unit = Term::App(Box::new(id), Box::new(Term::Unit));
   let ctx = Context::default();
 
   let (ty, out_ctx) = synthesize(&ctx, &id_of_unit)?;

rustfmt.toml

@@ -1 +1,2 @@
 tab_spaces = 2
+max_width = 80