From 9e148946933b312130c5bc0db820378a9b40750c Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Mon, 13 Nov 2023 03:08:32 -0600 Subject: [PATCH] fmt --- bidir/src/bidir.rs | 49 ++++++++++++++++++++++++++++--------- bidir/src/bidir_debruijn.rs | 39 +++++++++++++++++++++++++++++ bidir/src/convert_data.rs | 10 ++++++-- bidir/src/data.rs | 47 ++++++++++++++++++++++++++--------- bidir/src/data_debruijn.rs | 27 +++++++++++++++----- bidir/src/gensym.rs | 8 +++--- bidir/src/tests.rs | 21 +++++++++------- rustfmt.toml | 1 + 8 files changed, 158 insertions(+), 44 deletions(-) diff --git a/bidir/src/bidir.rs b/bidir/src/bidir.rs index 3493ddd..1726594 100644 --- a/bidir/src/bidir.rs +++ b/bidir/src/bidir.rs @@ -18,7 +18,9 @@ pub fn app_ctx(ctx: &Context, ty: &Type) -> Result { 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 { // Figure 10. Instantiation #[cfg_attr(feature = "trace_execution", trace)] -pub fn instantiate_left(ctx: &Context, a: &str, ty_a: &Type) -> Result { +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) => { + 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 = - ContextEntry::ExistentialSolved(b.to_owned(), Monotype::Existential(a.to_owned())); + *b_entry = ContextEntry::ExistentialSolved( + 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 } #[cfg_attr(feature = "trace_execution", trace)] -pub fn instantiate_right(ctx: &Context, ty_a: &Type, a: &str) -> Result { +pub fn instantiate_right( + ctx: &Context, + ty_a: &Type, + a: &str, +) -> Result { 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 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)?; diff --git a/bidir/src/bidir_debruijn.rs b/bidir/src/bidir_debruijn.rs index e69de29..c0b3334 100644 --- a/bidir/src/bidir_debruijn.rs +++ b/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 { + 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!(), + } +} diff --git a/bidir/src/convert_data.rs b/bidir/src/convert_data.rs index d704684..9c31d8a 100644 --- a/bidir/src/convert_data.rs +++ b/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, diff --git a/bidir/src/data.rs b/bidir/src/data.rs index 2cab8e8..3d45e98 100644 --- a/bidir/src/data.rs +++ b/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) => [FreeVar::Existential(x.to_owned())].into_iter().collect(), + Type::Existential(x) if ctx.lookup_existential(x).is_some() => { + 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) -> Option<(usize, Option)> { + 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()))), + 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, }) } @@ -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, diff --git a/bidir/src/data_debruijn.rs b/bidir/src/data_debruijn.rs index ba7f526..26a17a6 100644 --- a/bidir/src/data_debruijn.rs +++ b/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) -> Option<(usize, Option)> { + 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()))), + 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, }) } @@ -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()); diff --git a/bidir/src/gensym.rs b/bidir/src/gensym.rs index 85359d4..3c7f9af 100644 --- a/bidir/src/gensym.rs +++ b/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", - "T", "U", "V", "W", "X", "Y", "Z", + "A", "B", "C", "D", "E", "F", "G", "H", "I", "J", "K", "L", "M", "N", "O", + "P", "Q", "R", "S", "T", "U", "V", "W", "X", "Y", "Z", ]; pub fn gensym_existential() -> String { diff --git a/bidir/src/tests.rs b/bidir/src/tests.rs index 209697e..3925a8c 100644 --- a/bidir/src/tests.rs +++ b/bidir/src/tests.rs @@ -1,19 +1,23 @@ use anyhow::{bail, Result}; use crate::{ - bidir::{app_ctx, synthesize}, - data::{Context, Term}, + bidir_debruijn::{app_ctx, synthesize}, + convert_data::convert_term, + data_debruijn::Context, + data_debruijn::Term, + parser::TermParser, }; -macro_rules! id_term { - () => { - Term::Lam("x".to_owned(), Box::new(Term::Var("x".to_owned()))) - }; +fn term_of(str: &'static str) -> Result { + let term_parser = TermParser::new(); + 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::App(Box::new(id), Box::new(Term::Unit)); + let id_of_unit = term_of(r"(\x.x) ()")?; let ctx = Context::default(); let (ty, out_ctx) = synthesize(&ctx, &id_of_unit)?; diff --git a/rustfmt.toml b/rustfmt.toml index b196eaa..205c72c 100644 --- a/rustfmt.toml +++ b/rustfmt.toml @@ -1 +1,2 @@ tab_spaces = 2 +max_width = 80