From c7d1b02f8dab38f8e7dc5048ec3e5aa0c03ed36c Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Tue, 7 Nov 2023 02:50:06 -0600 Subject: [PATCH] add some more rules --- Cargo.lock | 72 ++++++++++++++++++++++++++++++++++++++++ bidir/Cargo.toml | 14 ++++++-- bidir/src/bidir.rs | 58 +++++++++++++++++++++++++++++--- bidir/src/data.rs | 31 ++++++++++++++++- bidir/src/main.rs | 10 +++++- bidir/src/parser.lalrpop | 17 +++++++--- 6 files changed, 189 insertions(+), 13 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 995bfc9..b7449de 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2,6 +2,21 @@ # It is not intended for manual editing. version = 3 +[[package]] +name = "addr2line" +version = "0.21.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8a30b2e23b9e17a9f90641c7ab1549cd9b44f296d3ccbf309d2863cfe398a0cb" +dependencies = [ + "gimli", +] + +[[package]] +name = "adler" +version = "1.0.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f26201604c87b1e01bd3d98f8d5d9a8fcbb815e8cedb41ffccbeb4bf593a35fe" + [[package]] name = "aho-corasick" version = "1.1.2" @@ -16,6 +31,9 @@ name = "anyhow" version = "1.0.75" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a4668cab20f66d8d020e1fbc0ebe47217433c1b6c8f2040faf858554e394ace6" +dependencies = [ + "backtrace", +] [[package]] name = "ascii-canvas" @@ -32,6 +50,21 @@ version = "1.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d468802bab17cbc0cc575e9b053f41e72aa36bfa6b7f55e3529ffa43161b97fa" +[[package]] +name = "backtrace" +version = "0.3.69" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2089b7e3f35b9dd2d0ed921ead4f6d318c27680d4a5bd167b3ee120edb105837" +dependencies = [ + "addr2line", + "cc", + "cfg-if", + "libc", + "miniz_oxide", + "object", + "rustc-demangle", +] + [[package]] name = "bidir" version = "0.1.0" @@ -86,6 +119,15 @@ dependencies = [ "typenum", ] +[[package]] +name = "cc" +version = "1.0.83" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f1174fb0b6ec23863f8b971027804a42614e347eafb0a95bf0b12cdae21fc4d0" +dependencies = [ + "libc", +] + [[package]] name = "cfg-if" version = "1.0.0" @@ -246,6 +288,12 @@ dependencies = [ "wasi", ] +[[package]] +name = "gimli" +version = "0.28.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6fb8d784f27acf97159b40fc4db5ecd8aa23b9ad5ef69cdd136d3bc80665f0c0" + [[package]] name = "hashbrown" version = "0.14.2" @@ -415,6 +463,15 @@ version = "2.6.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "f665ee40bc4a3c5590afb1e9677db74a508659dfd71e126420da8274909a0167" +[[package]] +name = "miniz_oxide" +version = "0.7.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e7810e0be55b428ada41041c41f32c9f1a42817901b4ccf45fa3d4b6561e74c7" +dependencies = [ + "adler", +] + [[package]] name = "new_debug_unreachable" version = "1.0.4" @@ -451,6 +508,15 @@ dependencies = [ "winapi", ] +[[package]] +name = "object" +version = "0.32.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9cf5f9dd3933bd50a9e1f149ec995f39ae2c496d31fd772c1fd45ebc27e902b0" +dependencies = [ + "memchr", +] + [[package]] name = "once_cell" version = "1.18.0" @@ -642,6 +708,12 @@ version = "0.8.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "c08c74e62047bb2de4ff487b251e4a92e24f48745648451635cec7d591162d9f" +[[package]] +name = "rustc-demangle" +version = "0.1.23" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d626bb9dae77e28219937af045c257c28bfd3f69333c512553507f5f9798cb76" + [[package]] name = "rustix" version = "0.38.21" diff --git a/bidir/Cargo.toml b/bidir/Cargo.toml index af8d2eb..be76e5c 100644 --- a/bidir/Cargo.toml +++ b/bidir/Cargo.toml @@ -6,7 +6,7 @@ edition = "2021" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [dependencies] -anyhow = "1.0.75" +anyhow = { version = "1.0.75", features = ["backtrace"] } dashmap = "5.5.3" env_logger = "0.10.0" im = "15.1.0" @@ -15,10 +15,20 @@ lazy_static = "1.4.0" rustyline = "12.0.0" trace = "0.1.7" tracing = "0.1.40" -tracing-subscriber = { version = "0.3.17", features = ["env-filter", "json", "regex", "serde", "time", "tracing"] } +tracing-subscriber = { version = "0.3.17", features = [ + "env-filter", + "json", + "regex", + "serde", + "time", + "tracing", +] } [build-dependencies] lalrpop = "0.20.0" [dev-dependencies] test-log = { version = "0.2.13", features = ["trace"] } + +[features] +trace_execution = [] diff --git a/bidir/src/bidir.rs b/bidir/src/bidir.rs index 426f73f..3493ddd 100644 --- a/bidir/src/bidir.rs +++ b/bidir/src/bidir.rs @@ -6,6 +6,7 @@ use crate::DEPTH; // Figure 8. Applying a context, as a substitution, to a type +#[cfg_attr(feature = "trace_execution", trace)] pub fn app_ctx(ctx: &Context, ty: &Type) -> Result { match ty { Type::Unit => Ok(Type::Unit), @@ -29,7 +30,7 @@ pub fn app_ctx(ctx: &Context, ty: &Type) -> Result { // Figure 9. Algorithmic subtyping /// Under input context Γ , type A is a subtype of B, with output context ∆ -#[instrument] +#[cfg_attr(feature = "trace_execution", trace)] pub fn subtype(ctx: &Context, left: &Type, right: &Type) -> Result { match (left, right) { // <:Unit rule @@ -88,6 +89,7 @@ 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 { match ty_a { // InstLReach rule @@ -116,8 +118,43 @@ 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 { 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 ctx_theta = instantiate_left(&ctx_gamma_aug, &ex_a1_s, &ty_a1)?; + + let ty_a2_aug = app_ctx(&ctx_theta, &ty_a2)?; + let ctx_delta = instantiate_right(&ctx_theta, &ty_a2_aug, &ex_a2_s)?; + + Ok(ctx_delta) + } + + // InstRAllL + Type::Polytype(beta, ty_b) if ctx.has_existential(a) => { + let ex_b = gensym_existential(); + let aug_ctx = ctx.add(vec![ + ContextEntry::Marker(ex_b.to_owned()), + ContextEntry::ExistentialVar(ex_b.to_owned()), + ]); + + let aug_b = ty_b.subst(beta, &Type::Existential(ex_b.to_owned())); + 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)) + .unwrap(); + + Ok(before) + } + + // InstRSolve ty_a if ty_a.is_mono() && ctx.has_existential(a) => { let (before, after) = ctx .split_by(|entry| match entry { @@ -138,13 +175,14 @@ pub fn instantiate_right(ctx: &Context, ty_a: &Type, a: &str) -> Result Type::Unit => todo!(), Type::Var(_) => todo!(), Type::Existential(_) => todo!(), - Type::Polytype(_, _) => todo!(), - Type::Arrow(_, _) => todo!(), + + _ => todo!(), } } // Figure 11. Algorithmic typing +#[cfg_attr(feature = "trace_execution", trace)] pub fn typecheck(ctx: &Context, term: &Term, ty: &Type) -> Result { match (term, ty) { // 1I rule @@ -170,6 +208,7 @@ pub fn typecheck(ctx: &Context, term: &Term, ty: &Type) -> Result { } } +#[cfg_attr(feature = "trace_execution", trace)] pub fn synthesize(ctx: &Context, term: &Term) -> Result<(Type, Context)> { match term { // Var rule @@ -196,7 +235,7 @@ pub fn synthesize(ctx: &Context, term: &Term) -> Result<(Type, Context)> { let ex_a_s = gensym_existential(); let ex_b_s = gensym_existential(); - let ex_gen = format!("{}→", ex_a_s); + 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()); @@ -260,6 +299,7 @@ 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)> { match (fun_ty, term) { // →App rule @@ -281,7 +321,15 @@ pub fn app_synthesize(ctx: &Context, fun_ty: &Type, term: &Term) -> Result<(Type } // âApp rule - (Type::Existential(_), _) => todo!(), + (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 = Type::Existential(ex_a1_s.clone()); + let ctx_delta = typecheck(&ctx_gamma_aug, e, &ex_a1)?; + + let ex_a2 = Type::Existential(ex_a2_s.clone()); + Ok((ex_a2, ctx_delta)) + } _ => bail!("trying to appSynthesize with a non-function type"), } diff --git a/bidir/src/data.rs b/bidir/src/data.rs index 7314fba..34ad544 100644 --- a/bidir/src/data.rs +++ b/bidir/src/data.rs @@ -1,7 +1,10 @@ use std::{fmt, hash::Hash, mem::replace}; +use anyhow::{bail, Result}; use im::{HashSet, Vector}; +use crate::gensym::gensym_existential; + #[derive(Clone)] pub enum Term { Unit, @@ -155,7 +158,7 @@ impl fmt::Debug for ContextEntry { 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::ExistentialSolved(arg0, arg1) => write!(f, "{} ≔ {:?}", arg0, arg1), Self::Marker(arg0) => write!(f, "▶{}", arg0), } } @@ -265,4 +268,30 @@ impl Context { res.0.extend(right.0.clone().into_iter()); res } + + 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, + None => bail!("wtf?"), + }; + + let ex_a1_s = gensym_existential(); + let ex_a2_s = gensym_existential(); + ctx.0[idx] = ContextEntry::ExistentialSolved( + var.to_owned(), + Monotype::Arrow( + Box::new(Monotype::Existential(ex_a1_s.to_owned())), + Box::new(Monotype::Existential(ex_a2_s.to_owned())), + ), + ); + ctx + .0 + .insert(idx, ContextEntry::ExistentialVar(ex_a1_s.to_owned())); + ctx + .0 + .insert(idx, ContextEntry::ExistentialVar(ex_a2_s.to_owned())); + + Ok((ex_a1_s, ex_a2_s, ctx)) + } } diff --git a/bidir/src/main.rs b/bidir/src/main.rs index 3685a73..afdc348 100644 --- a/bidir/src/main.rs +++ b/bidir/src/main.rs @@ -32,11 +32,19 @@ fn main() -> Result<()> { Ok(v) => v, Err(err) => { eprintln!("typecheck error: {err}"); + eprintln!("{}", err.backtrace()); continue; } }; - let ty = app_ctx(&out_ctx, &ty); + let ty = match app_ctx(&out_ctx, &ty) { + Ok(v) => v, + Err(err) => { + eprintln!("substitution error: {err}"); + eprintln!("{}", err.backtrace()); + continue; + } + }; println!("synthesized: {:?}", ty); } diff --git a/bidir/src/parser.lalrpop b/bidir/src/parser.lalrpop index 20f9dd5..4849bae 100644 --- a/bidir/src/parser.lalrpop +++ b/bidir/src/parser.lalrpop @@ -3,12 +3,14 @@ grammar; use crate::data::*; pub Term: Term = { - #[precedence(level = "0")] + #[precedence(level = "1")] "()" => Term::Unit, - "(" ")" => term, + "(" ")" => term, + Ident => Term::Var(<>), + + #[precedence(level = "2")] "λ" "." => Term::Lam(name, Box::new(term)), "\\" "." => Term::Lam(name, Box::new(term)), - Ident => Term::Var(<>), #[precedence(level = "4")] ":" => Term::Annot(Box::new(term), ty), @@ -18,10 +20,14 @@ pub Term: Term = { => Term::App(Box::new(func), Box::new(arg)), } +// https://github.com/lalrpop/lalrpop/issues/596 +TermReset: Term = ; + pub Type: Type = { #[precedence(level = "0")] "()" => Type::Unit, - "(" ")" => ty, + "(" ")" => ty, + Ident => Type::Var(<>), ExistIdent => Type::Existential(<>), "forall" "." => Type::Polytype(name, Box::new(ty)), @@ -31,6 +37,9 @@ pub Type: Type = { "->" => Type::Arrow(Box::new(a), Box::new(b)), }; +// https://github.com/lalrpop/lalrpop/issues/596 +TypeReset: Type = ; + ExistIdent: String = { r"\^[A-Za-z_]+" => <>.to_string(), }