From 47c8fc62f61b1548f8d27d18e33550c11533adfe Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Tue, 7 Nov 2023 01:53:05 -0600
Subject: [PATCH] it FUCKING typechecks

---
 bidir/src/bidir.rs | 16 ++++++----------
 bidir/src/lib.rs   |  4 ++--
 bidir/src/main.rs  | 20 ++++++++++++++++----
 bidir/src/tests.rs |  2 ++
 4 files changed, 26 insertions(+), 16 deletions(-)

diff --git a/bidir/src/bidir.rs b/bidir/src/bidir.rs
index 4c18b9d..426f73f 100644
--- a/bidir/src/bidir.rs
+++ b/bidir/src/bidir.rs
@@ -2,10 +2,10 @@ use anyhow::{bail, Result};
 
 use crate::data::{Context, ContextEntry, FreeVar, Monotype, Term, Type};
 use crate::gensym::gensym_existential;
+use crate::DEPTH;
 
 // Figure 8. Applying a context, as a substitution, to a type
 
-#[instrument]
 pub fn app_ctx(ctx: &Context, ty: &Type) -> Result<Type> {
   match ty {
     Type::Unit => Ok(Type::Unit),
@@ -145,7 +145,6 @@ pub fn instantiate_right(ctx: &Context, ty_a: &Type, a: &str) -> Result<Context>
 
 // Figure 11. Algorithmic typing
 
-#[instrument]
 pub fn typecheck(ctx: &Context, term: &Term, ty: &Type) -> Result<Context> {
   match (term, ty) {
     // 1I rule
@@ -171,7 +170,6 @@ pub fn typecheck(ctx: &Context, term: &Term, ty: &Type) -> Result<Context> {
   }
 }
 
-#[instrument]
 pub fn synthesize(ctx: &Context, term: &Term) -> Result<(Type, Context)> {
   match term {
     // Var rule
@@ -227,7 +225,6 @@ pub fn synthesize(ctx: &Context, term: &Term) -> Result<(Type, Context)> {
         warn!("substituting {tau:?} looking for {name}");
         tau = tau.subst(&name, &Type::Var(ex_gen.clone()));
       }
-      info!("ex_gen = {ex_gen}, tau = {tau:?}");
 
       Ok((Type::Polytype(ex_gen, Box::new(tau)), before_marker))
     }
@@ -250,7 +247,6 @@ pub fn synthesize(ctx: &Context, term: &Term) -> Result<(Type, Context)> {
     //   ]);
 
     //   let wtf_ctx = typecheck(&aug_ctx, &e, &ex_b)?;
-    //   println!("the wtf ctx is {wtf_ctx:?}");
     //   Ok((Type::Arrow(Box::new(ex_a), Box::new(ex_b)), ctx.clone()))
     // }
 
@@ -264,14 +260,12 @@ pub fn synthesize(ctx: &Context, term: &Term) -> Result<(Type, Context)> {
   }
 }
 
-#[instrument]
 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) => {
-      info!("→App rule");
-      typecheck(ctx, e, ty_a)?;
-      Ok((*ty_c.clone(), ctx.clone()))
+      let out_ctx = typecheck(ctx, e, ty_a)?;
+      Ok((*ty_c.clone(), out_ctx))
     }
 
     // ∀App rule
@@ -281,7 +275,9 @@ pub fn app_synthesize(ctx: &Context, fun_ty: &Type, term: &Term) -> Result<(Type
       let aug_ctx = ctx.add(vec![ex.clone()]);
 
       let aug_ty = ty_a.subst(&a, &Type::Existential(ex_s));
-      app_synthesize(&aug_ctx, &aug_ty, e)
+      let (ty, ctx_delta) = app_synthesize(&aug_ctx, &aug_ty, e)?;
+
+      Ok((ty, ctx_delta))
     }
 
     // âApp rule
diff --git a/bidir/src/lib.rs b/bidir/src/lib.rs
index 8951385..4168c21 100644
--- a/bidir/src/lib.rs
+++ b/bidir/src/lib.rs
@@ -1,7 +1,7 @@
 #[macro_use]
-extern crate trace;
-#[macro_use]
 extern crate tracing;
+#[macro_use]
+extern crate trace;
 
 use lalrpop_util::lalrpop_mod;
 
diff --git a/bidir/src/main.rs b/bidir/src/main.rs
index 9bdd70a..3685a73 100644
--- a/bidir/src/main.rs
+++ b/bidir/src/main.rs
@@ -1,5 +1,9 @@
 use anyhow::Result;
-use bidir::{bidir::synthesize, data::Context, parser::TermParser};
+use bidir::{
+  bidir::{app_ctx, synthesize},
+  data::Context,
+  parser::TermParser,
+};
 use rustyline::{Config, DefaultEditor};
 
 fn main() -> Result<()> {
@@ -13,7 +17,6 @@ fn main() -> Result<()> {
       Ok(line) => line,
       Err(_) => break,
     };
-    println!("line: {}", line);
 
     let parsed_term = match term_parser.parse(&line) {
       Ok(term) => term,
@@ -25,8 +28,17 @@ fn main() -> Result<()> {
     println!("parsed: {:?}", parsed_term);
 
     let ctx = Context::default();
-    let synthesized_type = synthesize(&ctx, &parsed_term);
-    println!("synthesized: {:?}", synthesized_type);
+    let (ty, out_ctx) = match synthesize(&ctx, &parsed_term) {
+      Ok(v) => v,
+      Err(err) => {
+        eprintln!("typecheck error: {err}");
+        continue;
+      }
+    };
+
+    let ty = app_ctx(&out_ctx, &ty);
+
+    println!("synthesized: {:?}", ty);
   }
 
   Ok(())
diff --git a/bidir/src/tests.rs b/bidir/src/tests.rs
index 9003c76..209697e 100644
--- a/bidir/src/tests.rs
+++ b/bidir/src/tests.rs
@@ -28,6 +28,8 @@ fn test_id_of_unit() -> Result<()> {
   let ctx = Context::default();
 
   let (ty, out_ctx) = synthesize(&ctx, &id_of_unit)?;
+  let wtf = app_ctx(&out_ctx, &ty);
+  println!("WTF: {wtf:?}");
   bail!("Synthesized: {:?} (context = {:?})", ty, out_ctx);
   Ok(())
 }