From 2863e10113551db2a635b0a701bf271e5c28f951 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Sat, 4 Nov 2023 13:50:45 -0500 Subject: [PATCH] gensym --- bidir/src/bidir.rs | 49 ++++++++++++------------ bidir/src/data.rs | 94 +++++++++++++++++++++++++++++++++++++--------- bidir/src/tests.rs | 6 ++- 3 files changed, 104 insertions(+), 45 deletions(-) diff --git a/bidir/src/bidir.rs b/bidir/src/bidir.rs index 3d9bd82..85cd9f0 100644 --- a/bidir/src/bidir.rs +++ b/bidir/src/bidir.rs @@ -2,7 +2,7 @@ use anyhow::{bail, Result}; use crate::DEPTH; -use crate::data::FreeVar; +use crate::data::{FreeVar, Monotype}; use crate::{ data::{Context, ContextEntry, Term, Type}, gensym::gensym_prefix, @@ -10,12 +10,11 @@ use crate::{ // Figure 8. Applying a context, as a substitution, to a type -#[trace] pub fn app_ctx(ctx: &Context, ty: &Type) -> Result { match ty { Type::Existential(a) => match ctx.lookup_existential(a) { - Some(Some(m)) => Ok(m.into_poly()), - Some(None) => Ok(Type::Existential(a.clone())), + Some((_, Some(m))) => Ok(m.into_poly()), + Some((_, None)) => Ok(Type::Existential(a.clone())), None => bail!("existential variable {a} doesn't exist in context"), }, @@ -38,22 +37,12 @@ pub fn subtype(ctx: &Context, a: &Type, b: &Type) -> Result { (Type::Unit, Type::Unit) => Ok(ctx.clone()), // <:Var rule - (Type::Var(x), Type::Var(y)) if x == y => { - // Ensure that the name exists in the context - if ctx.lookup_type(x).is_none() { - bail!("name {x} not in context"); - } - - Ok(ctx.clone()) - } + (Type::Var(x), Type::Var(y)) if x == y && ctx.lookup_type(x).is_some() => Ok(ctx.clone()), // <:Exvar rule - (Type::Existential(x), Type::Existential(y)) if x == y => { - // Ensure that the name exists in the context - if ctx.lookup_existential(x).is_none() { - bail!("name {x} not in context"); - } - + (Type::Existential(x), Type::Existential(y)) + if x == y && ctx.lookup_existential(x).is_some() => + { Ok(ctx.clone()) } @@ -90,9 +79,21 @@ pub fn instantiate_left(ctx: &Context, a: &str, ty_a: &Type) -> Result match ty_a { // InstLReach rule Type::Existential(b) if ctx.has_existential(a) && ctx.has_existential(b) => { - // TODO: WTF? - todo!() + let mut new_ctx = ctx.clone(); + { + let b_entry = new_ctx + .0 + .iter_mut() + .find(|entry| matches!(entry, ContextEntry::ExistentialVar(x) if x == b)) + .expect("should exist"); + + *b_entry = + ContextEntry::ExistentialSolved(b.to_owned(), Monotype::Existential(a.to_owned())); + } + + Ok(new_ctx) } + Type::Existential(b) => todo!(), Type::Unit => todo!(), @@ -134,13 +135,11 @@ pub fn typecheck(ctx: &Context, term: &Term, ty: &Type) -> Result { pub fn synthesize(ctx: &Context, term: &Term) -> Result<(Type, Context)> { match term { // Var rule - Term::Var(name) => { - let ty = match ctx.lookup_type(name) { - Some(v) => v, - None => bail!("could not find name {name}"), - }; + Term::Var(name) if ctx.has_type(name) => { + let (_, ty) = ctx.lookup_type(name).unwrap(); Ok((ty, ctx.clone())) } + Term::Var(name) => bail!("could not find name {name}"), // 1I⇒ rule Term::Unit => Ok((Type::Unit, ctx.clone())), diff --git a/bidir/src/data.rs b/bidir/src/data.rs index bcf2df1..5f5cdfd 100644 --- a/bidir/src/data.rs +++ b/bidir/src/data.rs @@ -1,8 +1,11 @@ -use std::hash::Hash; +use std::{ + fmt::{self, write}, + hash::Hash, +}; use im::{HashSet, Vector}; -#[derive(Debug, Clone)] +#[derive(Clone)] pub enum Term { Unit, Var(String), @@ -11,7 +14,19 @@ pub enum Term { Annot(Box, Type), } -#[derive(Debug, Clone)] +impl fmt::Debug for Term { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + Self::Unit => write!(f, "unit"), + Self::Var(arg0) => write!(f, "`{}", arg0), + Self::Lam(arg0, arg1) => write!(f, "λ{}.{:?}", arg0, arg1), + Self::App(arg0, arg1) => write!(f, "({:?} · {:?})", arg0, arg1), + Self::Annot(arg0, arg1) => write!(f, "({:?} : {:?})", arg0, arg1), + } + } +} + +#[derive(Clone)] pub enum Type { Unit, Var(String), @@ -20,6 +35,18 @@ pub enum Type { Arrow(Box, Box), } +impl fmt::Debug for Type { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + Self::Unit => write!(f, "𝟙"), + Self::Var(arg0) => write!(f, "`α-{}", arg0), + Self::Existential(arg0) => write!(f, "`α\u{0302}-{}", arg0), + Self::Polytype(arg0, arg1) => write!(f, "(∀{}.{:?})", arg0, arg1), + Self::Arrow(arg0, arg1) => write!(f, "({:?} → {:?})", arg0, arg1), + } + } +} + impl Type { pub fn into_mono(&self) -> Option { match self { @@ -90,7 +117,7 @@ impl Monotype { } } -#[derive(Debug, Clone)] +#[derive(Clone)] pub enum ContextEntry { TypeVar(String), TermAnnot(String, Type), @@ -99,6 +126,18 @@ pub enum ContextEntry { Marker(String), } +impl fmt::Debug for ContextEntry { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + Self::TypeVar(arg0) => write!(f, "`{}", arg0), + Self::TermAnnot(arg0, arg1) => write!(f, "{} : {:?}", arg0, arg1), + Self::ExistentialVar(arg0) => write!(f, "`{}", arg0), + Self::ExistentialSolved(arg0, arg1) => write!(f, "{:?} = {:?}", arg0, arg1), + Self::Marker(arg0) => write!(f, "▶{}", arg0), + } + } +} + #[derive(Debug, Clone)] pub enum CompleteContextEntry { TypeVar(String), @@ -107,8 +146,19 @@ pub enum CompleteContextEntry { Marker(String), } -#[derive(Debug, Clone, Default)] -pub struct Context(Vector); +#[derive(Clone, Default)] +pub struct Context(pub(crate) Vector); + +impl fmt::Debug for Context { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + f.write_str("Γ")?; + for rule in self.0.iter() { + f.write_str(", ")?; + rule.fmt(f)?; + } + Ok(()) + } +} impl Context { pub fn add(&self, entries: Vec) -> Context { @@ -119,12 +169,16 @@ impl Context { new_ctx } - /// Looks up a polytype by name - pub fn lookup_type(&self, name: impl AsRef) -> Option { - self.0.iter().find_map(|entry| match entry { - ContextEntry::TermAnnot(n, t) if n == name.as_ref() => Some(t.clone()), - _ => None, - }) + /// Looks up a polytype by name, also returning an index + pub fn lookup_type(&self, name: impl AsRef) -> Option<(usize, Type)> { + self + .0 + .iter() + .enumerate() + .find_map(|(i, entry)| match entry { + ContextEntry::TermAnnot(n, t) if n == name.as_ref() => Some((i, t.clone())), + _ => None, + }) } #[inline] @@ -136,12 +190,16 @@ 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) -> Option> { - self.0.iter().find_map(|entry| match entry { - ContextEntry::ExistentialVar(n) if n == name.as_ref() => Some(None), - ContextEntry::ExistentialSolved(n, t) if n == name.as_ref() => Some(Some(t.clone())), - _ => None, - }) + pub fn lookup_existential(&self, name: impl AsRef) -> Option<(usize, Option)> { + self + .0 + .iter() + .enumerate() + .find_map(|(i, entry)| match entry { + ContextEntry::ExistentialVar(n) if n == name.as_ref() => Some((i, None)), + ContextEntry::ExistentialSolved(n, t) if n == name.as_ref() => Some((i, Some(t.clone()))), + _ => None, + }) } #[inline] diff --git a/bidir/src/tests.rs b/bidir/src/tests.rs index 1efff03..ab1b67b 100644 --- a/bidir/src/tests.rs +++ b/bidir/src/tests.rs @@ -1,7 +1,7 @@ use anyhow::{bail, Result}; use crate::{ - bidir::synthesize, + bidir::{app_ctx, synthesize}, data::{Context, Term}, }; @@ -15,7 +15,9 @@ macro_rules! id_term { fn test_id() -> Result<()> { let id = id_term!(); let ctx = Context::default(); - bail!("Result: {:?}", synthesize(&ctx, &id)); + let (ty, out_ctx) = synthesize(&ctx, &id)?; + let ty2 = app_ctx(&out_ctx, &ty)?; + println!("Result: {:?}", ty2); Ok(()) }