diff --git a/bidir/src/bidir.rs b/bidir/src/bidir.rs index e309f37..ae8ffab 100644 --- a/bidir/src/bidir.rs +++ b/bidir/src/bidir.rs @@ -15,12 +15,13 @@ pub fn app_ctx(ctx: &Context, ty: &Type) -> Result { None => bail!("existential variable {a} doesn't exist in context"), }, - Type::Polytype(_, _) => todo!(), + 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)?), )), - _ => todo!("shiiet"), + _ => todo!("shiiet ctx = {ctx:?}, ty = {ty:?}"), } } @@ -152,28 +153,73 @@ pub fn synthesize(ctx: &Context, term: &Term) -> Result<(Type, Context)> { Ok((ty_a.clone(), ctx_delta)) } - // →I⇒ rule - // > Rule →I⇒ corresponds to Decl→I⇒, one of the guessing rules, so we - // > create new existential variables ^α (for the function domain) and ^β (for - // > the codomain) and check the function body against ^β. As in ∀App, we do - // > not place a marker before ^α, because ^α and ^β appear in the output type - // > (λx. e ⇒ ^α → ^β). + // →I⇒' rule Term::Lam(x, e) => { let ex_a_s = gensym_existential(); let ex_b_s = gensym_existential(); + + let ex_gen = format!("{}->", ex_a_s); + let ex_a = Type::Existential(ex_a_s.clone()); let ex_b = Type::Existential(ex_b_s.clone()); + let aug_ctx = ctx.add(vec![ + ContextEntry::Marker(ex_a_s.clone()), ContextEntry::ExistentialVar(ex_a_s.clone()), ContextEntry::ExistentialVar(ex_b_s.clone()), ContextEntry::TermAnnot(x.clone(), ex_a.clone()), ]); 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())) + println!("WTF CTX {wtf_ctx:?}"); + + // Split back out at the marker + let (before_marker, after_marker) = { + let marker_idx = wtf_ctx + .0 + .iter() + .position(|entry| match entry { + ContextEntry::Marker(m) if *m == ex_a_s => true, + _ => false, + }) + .unwrap(); + + // println!("Marker index: {marker_idx}"); + wtf_ctx.0.clone().split_at(marker_idx) + }; + let before_marker = Context(before_marker); + let after_marker = Context(after_marker); + + let mut tau = app_ctx(&after_marker, &Type::Arrow(Box::new(ex_a), Box::new(ex_b)))?; + for name in after_marker.unsolved_existentials() { + tau = tau.subst(name, &Type::Var(ex_gen.clone())); + } + + Ok((Type::Polytype(ex_gen, Box::new(tau)), before_marker)) } + // // →I⇒ rule + // // > Rule →I⇒ corresponds to Decl→I⇒, one of the guessing rules, so we + // // > create new existential variables ^α (for the function domain) and ^β (for + // // > the codomain) and check the function body against ^β. As in ∀App, we do + // // > not place a marker before ^α, because ^α and ^β appear in the output type + // // > (λx. e ⇒ ^α → ^β). + // Term::Lam(x, e) => { + // let ex_a_s = gensym_existential(); + // let ex_b_s = gensym_existential(); + // let ex_a = Type::Existential(ex_a_s.clone()); + // let ex_b = Type::Existential(ex_b_s.clone()); + // let aug_ctx = ctx.add(vec![ + // ContextEntry::ExistentialVar(ex_a_s.clone()), + // ContextEntry::ExistentialVar(ex_b_s.clone()), + // ContextEntry::TermAnnot(x.clone(), ex_a.clone()), + // ]); + + // 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())) + // } + // →E rule Term::App(e1, e2) => { let (ty_a, ctx_theta) = synthesize(ctx, e1)?; diff --git a/bidir/src/data.rs b/bidir/src/data.rs index f63df0b..7020f30 100644 --- a/bidir/src/data.rs +++ b/bidir/src/data.rs @@ -1,4 +1,4 @@ -use std::{fmt, hash::Hash}; +use std::{fmt, hash::Hash, mem::replace}; use im::{HashSet, Vector}; @@ -38,7 +38,7 @@ impl fmt::Debug for Type { Self::Unit => write!(f, "𝟙"), Self::Var(arg0) => write!(f, "{}", arg0), Self::Existential(arg0) => write!(f, "{}", arg0), - Self::Polytype(arg0, arg1) => write!(f, "(∀{}.{:?})", arg0, arg1), + Self::Polytype(arg0, arg1) => write!(f, "(∀ {} . {:?})", arg0, arg1), Self::Arrow(arg0, arg1) => write!(f, "({:?} -> {:?})", arg0, arg1), } } @@ -93,6 +93,21 @@ impl Type { free_vars_with_context(&Context::default(), self) } + + pub fn subst(&self, var: impl AsRef, replacement: &Type) -> Type { + let var = var.as_ref(); + match self { + Type::Unit => Type::Unit, + Type::Var(n) if n == var => replacement.clone(), + Type::Var(n) => Type::Var(n.clone()), + Type::Existential(s) => Type::Existential(s.clone()), + 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)), + ), + } + } } #[derive(Clone)] @@ -214,4 +229,19 @@ impl Context { pub fn has_existential(&self, name: impl AsRef) -> bool { self.lookup_existential(name).is_some() } + + pub fn unsolved_existentials(&self) -> HashSet { + let mut unsolved = HashSet::new(); + + for entry in self.0.iter() { + match entry { + ContextEntry::ExistentialVar(n) => { + unsolved.insert(n.clone()); + } + _ => {} + } + } + + unsolved + } } diff --git a/bidir/src/tests.rs b/bidir/src/tests.rs index ab1b67b..5e540b7 100644 --- a/bidir/src/tests.rs +++ b/bidir/src/tests.rs @@ -16,8 +16,8 @@ fn test_id() -> Result<()> { let id = id_term!(); let ctx = Context::default(); let (ty, out_ctx) = synthesize(&ctx, &id)?; - let ty2 = app_ctx(&out_ctx, &ty)?; - println!("Result: {:?}", ty2); + println!("Synthesis result: {ty:?} | {out_ctx:?}"); + Ok(()) } @@ -26,6 +26,7 @@ fn test_id_of_unit() -> Result<()> { let id = id_term!(); let id_of_unit = Term::App(Box::new(id), Box::new(Term::Unit)); let ctx = Context::default(); + bail!("Result: {:?}", synthesize(&ctx, &id_of_unit)); Ok(()) }