From d20044501bcc2e645a1ccc5ee7a8d3d2cd1467bf Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Tue, 7 Nov 2023 01:33:59 -0600 Subject: [PATCH] id of unit --- Cargo.lock | 287 ++++++++++++++++++++++++++++++++++++++++++++- bidir/Cargo.toml | 6 + bidir/src/bidir.rs | 98 +++++++++++----- bidir/src/data.rs | 33 +++++- bidir/src/lib.rs | 2 + bidir/src/tests.rs | 5 +- 6 files changed, 394 insertions(+), 37 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index f4fa903..995bfc9 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -38,12 +38,16 @@ version = "0.1.0" dependencies = [ "anyhow", "dashmap", + "env_logger", "im", "lalrpop", "lalrpop-util", "lazy_static", "rustyline", + "test-log", "trace", + "tracing", + "tracing-subscriber", ] [[package]] @@ -118,6 +122,15 @@ dependencies = [ "parking_lot_core", ] +[[package]] +name = "deranged" +version = "0.3.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0f32d04922c60427da6f9fef14d042d9edddef64cb9d4ce0d64d0685fbeb1fd3" +dependencies = [ + "powerfmt", +] + [[package]] name = "diff" version = "0.1.13" @@ -166,6 +179,19 @@ version = "0.1.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "c34f04666d835ff5d62e058c3995147c06f42fe86ff053337632bca83e42702d" +[[package]] +name = "env_logger" +version = "0.10.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "85cdab6a89accf66733ad5a1693a4dcced6aeff64602b634530dd73c1f3ee9f0" +dependencies = [ + "humantime", + "is-terminal", + "log", + "regex", + "termcolor", +] + [[package]] name = "equivalent" version = "1.0.1" @@ -241,6 +267,12 @@ dependencies = [ "windows-sys", ] +[[package]] +name = "humantime" +version = "2.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9a3a5bfb195931eeb336b2a7b4d761daec841b97f947d34394601737a7bba5e4" + [[package]] name = "im" version = "15.1.0" @@ -285,6 +317,12 @@ dependencies = [ "either", ] +[[package]] +name = "itoa" +version = "1.0.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "af150ab688ff2122fcef229be89cb50dd66af9e01a4ff320cc137eecc9bacc38" + [[package]] name = "lalrpop" version = "0.20.0" @@ -362,6 +400,15 @@ version = "0.4.20" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b5e6163cb8c49088c2c36f57875e58ccd8c87c7427f7fbd50ea6710b2f3f2e8f" +[[package]] +name = "matchers" +version = "0.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8263075bb86c5a1b1427b5ae862e8889656f126e9f77c484496e8b47cf5c5558" +dependencies = [ + "regex-automata 0.1.10", +] + [[package]] name = "memchr" version = "2.6.4" @@ -394,12 +441,28 @@ dependencies = [ "libc", ] +[[package]] +name = "nu-ansi-term" +version = "0.46.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "77a8165726e8236064dbb45459242600304b42a5ea24ee2948e18e023bf7ba84" +dependencies = [ + "overload", + "winapi", +] + [[package]] name = "once_cell" version = "1.18.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "dd8b5dd2ae5ed71462c540258bedcb51965123ad7e7ccf4b9a8cafaa4a63576d" +[[package]] +name = "overload" +version = "0.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b15813163c1d831bf4a13c3610c05c0d03b39feb07f7e09fa234dac9b15aaf39" + [[package]] name = "parking_lot" version = "0.12.1" @@ -448,6 +511,18 @@ version = "0.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "5be167a7af36ee22fe3115051bc51f6e6c7054c9348e28deb4f49bd6f705a315" +[[package]] +name = "pin-project-lite" +version = "0.2.13" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8afb450f006bf6385ca15ef45d71d2288452bc3683ce2e2cacc0d18e4be60b58" + +[[package]] +name = "powerfmt" +version = "0.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "439ee305def115ba05938db6eb1644ff94165c5ab5e9420d1c1bcedbba909391" + [[package]] name = "precomputed-hash" version = "0.1.1" @@ -525,10 +600,19 @@ checksum = "380b951a9c5e80ddfd6136919eef32310721aa4aacd4889a8d39124b026ab343" dependencies = [ "aho-corasick", "memchr", - "regex-automata", + "regex-automata 0.4.3", "regex-syntax 0.8.2", ] +[[package]] +name = "regex-automata" +version = "0.1.10" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6c230d73fb8d8c1b9c0b3135c5142a8acee3a0558fb8db5cf1cb65f8d7862132" +dependencies = [ + "regex-syntax 0.6.29", +] + [[package]] name = "regex-automata" version = "0.4.3" @@ -540,6 +624,12 @@ dependencies = [ "regex-syntax 0.8.2", ] +[[package]] +name = "regex-syntax" +version = "0.6.29" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f162c6dd7b008981e4d40210aca20b4bd0f9b60ca9271061b07f78537722f2e1" + [[package]] name = "regex-syntax" version = "0.7.5" @@ -594,12 +684,58 @@ dependencies = [ "winapi", ] +[[package]] +name = "ryu" +version = "1.0.15" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1ad4cc8da4ef723ed60bced201181d83791ad433213d8c24efffda1eec85d741" + [[package]] name = "scopeguard" version = "1.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" +[[package]] +name = "serde" +version = "1.0.192" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bca2a08484b285dcb282d0f67b26cadc0df8b19f8c12502c13d966bf9482f001" +dependencies = [ + "serde_derive", +] + +[[package]] +name = "serde_derive" +version = "1.0.192" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d6c7207fbec9faa48073f3e3074cbe553af6ea512d7c21ba46e434e70ea9fbc1" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.38", +] + +[[package]] +name = "serde_json" +version = "1.0.108" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3d1c7e3eac408d115102c4c24ad393e0821bb3a5df4d506a80f85f7a742a526b" +dependencies = [ + "itoa", + "ryu", + "serde", +] + +[[package]] +name = "sharded-slab" +version = "0.1.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f40ca3c46823713e0d4209592e8d6e826aa57e928f09752619fc696c499637f6" +dependencies = [ + "lazy_static", +] + [[package]] name = "siphasher" version = "0.3.11" @@ -674,6 +810,26 @@ dependencies = [ "winapi", ] +[[package]] +name = "termcolor" +version = "1.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6093bad37da69aab9d123a8091e4be0aa4a03e4d601ec641c327398315f62b64" +dependencies = [ + "winapi-util", +] + +[[package]] +name = "test-log" +version = "0.2.13" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f66edd6b6cd810743c0c71e1d085e92b01ce6a72782032e3f794c8284fe4bcdd" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.38", +] + [[package]] name = "thiserror" version = "1.0.50" @@ -694,6 +850,45 @@ dependencies = [ "syn 2.0.38", ] +[[package]] +name = "thread_local" +version = "1.1.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3fdd6f064ccff2d6567adcb3873ca630700f00b5ad3f060c25b5dcfd9a4ce152" +dependencies = [ + "cfg-if", + "once_cell", +] + +[[package]] +name = "time" +version = "0.3.30" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c4a34ab300f2dee6e562c10a046fc05e358b29f9bf92277f30c3c8d82275f6f5" +dependencies = [ + "deranged", + "itoa", + "powerfmt", + "serde", + "time-core", + "time-macros", +] + +[[package]] +name = "time-core" +version = "0.1.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ef927ca75afb808a4d64dd374f00a2adf8d0fcff8e7b184af886c3c87ec4a3f3" + +[[package]] +name = "time-macros" +version = "0.2.15" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4ad70d68dba9e1f8aceda7aa6711965dfec1cac869f311a51bd08b3a2ccbce20" +dependencies = [ + "time-core", +] + [[package]] name = "tiny-keccak" version = "2.0.2" @@ -714,6 +909,81 @@ dependencies = [ "syn 1.0.109", ] +[[package]] +name = "tracing" +version = "0.1.40" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c3523ab5a71916ccf420eebdf5521fcef02141234bbc0b8a49f2fdc4544364ef" +dependencies = [ + "pin-project-lite", + "tracing-attributes", + "tracing-core", +] + +[[package]] +name = "tracing-attributes" +version = "0.1.27" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.38", +] + +[[package]] +name = "tracing-core" +version = "0.1.32" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c06d3da6113f116aaee68e4d601191614c9053067f9ab7f6edbcb161237daa54" +dependencies = [ + "once_cell", + "valuable", +] + +[[package]] +name = "tracing-log" +version = "0.1.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f751112709b4e791d8ce53e32c4ed2d353565a795ce84da2285393f41557bdf2" +dependencies = [ + "log", + "once_cell", + "tracing-core", +] + +[[package]] +name = "tracing-serde" +version = "0.1.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bc6b213177105856957181934e4920de57730fc69bf42c37ee5bb664d406d9e1" +dependencies = [ + "serde", + "tracing-core", +] + +[[package]] +name = "tracing-subscriber" +version = "0.3.17" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "30a651bc37f915e81f087d86e62a18eec5f79550c7faff886f7090b4ea757c77" +dependencies = [ + "matchers", + "nu-ansi-term", + "once_cell", + "regex", + "serde", + "serde_json", + "sharded-slab", + "smallvec", + "thread_local", + "time", + "tracing", + "tracing-core", + "tracing-log", + "tracing-serde", +] + [[package]] name = "typenum" version = "1.17.0" @@ -750,6 +1020,12 @@ version = "0.2.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "711b9620af191e0cdc7468a8d14e709c3dcdb115b36f838e601583af800a370a" +[[package]] +name = "valuable" +version = "0.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "830b7e5d4d90034032940e4ace0d9a9a057e7a45cd94e6c007832e39edb82f6d" + [[package]] name = "version_check" version = "0.9.4" @@ -778,6 +1054,15 @@ version = "0.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6" +[[package]] +name = "winapi-util" +version = "0.1.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f29e6f9198ba0d26b4c9f07dbe6f9ed633e1f3d5b8b414090084349e46a52596" +dependencies = [ + "winapi", +] + [[package]] name = "winapi-x86_64-pc-windows-gnu" version = "0.4.0" diff --git a/bidir/Cargo.toml b/bidir/Cargo.toml index d9a059d..af8d2eb 100644 --- a/bidir/Cargo.toml +++ b/bidir/Cargo.toml @@ -8,11 +8,17 @@ edition = "2021" [dependencies] anyhow = "1.0.75" dashmap = "5.5.3" +env_logger = "0.10.0" im = "15.1.0" lalrpop-util = { version = "0.20.0", features = ["lexer", "regex", "unicode"] } 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"] } [build-dependencies] lalrpop = "0.20.0" + +[dev-dependencies] +test-log = { version = "0.2.13", features = ["trace"] } diff --git a/bidir/src/bidir.rs b/bidir/src/bidir.rs index ae8ffab..4c18b9d 100644 --- a/bidir/src/bidir.rs +++ b/bidir/src/bidir.rs @@ -1,14 +1,16 @@ use anyhow::{bail, Result}; -use crate::DEPTH; - use crate::data::{Context, ContextEntry, FreeVar, Monotype, Term, Type}; use crate::gensym::gensym_existential; // Figure 8. Applying a context, as a substitution, to a type +#[instrument] 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())), @@ -21,14 +23,13 @@ pub fn app_ctx(ctx: &Context, ty: &Type) -> Result { Box::new(app_ctx(ctx, a)?), Box::new(app_ctx(ctx, b)?), )), - _ => todo!("shiiet ctx = {ctx:?}, ty = {ty:?}"), } } // Figure 9. Algorithmic subtyping /// Under input context Γ , type A is a subtype of B, with output context ∆ -#[trace] +#[instrument] pub fn subtype(ctx: &Context, left: &Type, right: &Type) -> Result { match (left, right) { // <:Unit rule @@ -44,8 +45,9 @@ pub fn subtype(ctx: &Context, left: &Type, right: &Type) -> Result { Ok(ctx.clone()) } + // <:InstantiateL (Type::Existential(a), ty_a) - if !right + if !ty_a .free_vars() .contains(&FreeVar::Existential(a.to_string())) && ctx.lookup_existential(a).is_some() => @@ -53,6 +55,18 @@ pub fn subtype(ctx: &Context, left: &Type, right: &Type) -> Result { let ctx_delta = instantiate_left(ctx, a, ty_a)?; Ok(ctx_delta) } + + // <:InstantiateR + (ty_a, Type::Existential(a)) + if !ty_a + .free_vars() + .contains(&FreeVar::Existential(a.to_string())) + && ctx.lookup_existential(a).is_some() => + { + let ctx_delta = instantiate_right(ctx, ty_a, a)?; + Ok(ctx_delta) + } + (Type::Existential(_), Type::Unit) => todo!(), (Type::Existential(_), Type::Var(_)) => todo!(), (Type::Existential(_), Type::Polytype(_, _)) => todo!(), @@ -74,7 +88,6 @@ pub fn subtype(ctx: &Context, left: &Type, right: &Type) -> Result { // Figure 10. Instantiation -#[trace] pub fn instantiate_left(ctx: &Context, a: &str, ty_a: &Type) -> Result { match ty_a { // InstLReach rule @@ -103,9 +116,36 @@ pub fn instantiate_left(ctx: &Context, a: &str, ty_a: &Type) -> Result } } +pub fn instantiate_right(ctx: &Context, ty_a: &Type, a: &str) -> Result { + match ty_a { + ty_a if ty_a.is_mono() && ctx.has_existential(a) => { + let (before, after) = ctx + .split_by(|entry| match entry { + ContextEntry::ExistentialVar(n) if n == a => true, + _ => false, + }) + .unwrap(); + + let ty_a_mono = ty_a.into_mono().unwrap(); + + Ok(Context::unsplit( + &before, + ContextEntry::ExistentialSolved(a.to_owned(), ty_a_mono), + &after, + )) + } + + Type::Unit => todo!(), + Type::Var(_) => todo!(), + Type::Existential(_) => todo!(), + Type::Polytype(_, _) => todo!(), + Type::Arrow(_, _) => todo!(), + } +} + // Figure 11. Algorithmic typing -#[trace] +#[instrument] pub fn typecheck(ctx: &Context, term: &Term, ty: &Type) -> Result { match (term, ty) { // 1I rule @@ -131,7 +171,7 @@ pub fn typecheck(ctx: &Context, term: &Term, ty: &Type) -> Result { } } -#[trace] +#[instrument] pub fn synthesize(ctx: &Context, term: &Term) -> Result<(Type, Context)> { match term { // Var rule @@ -158,7 +198,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()); @@ -171,29 +211,23 @@ pub fn synthesize(ctx: &Context, term: &Term) -> Result<(Type, Context)> { ]); let wtf_ctx = typecheck(&aug_ctx, &e, &ex_b)?; - println!("WTF CTX {wtf_ctx:?}"); + info!("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 (before_marker, after_marker) = wtf_ctx + .split_by(|entry| match entry { + ContextEntry::Marker(m) if *m == ex_a_s => true, + _ => false, + }) + .unwrap(); + info!("Unsolved: {:?}", after_marker.unsolved_existentials()); 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())); + 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)) } @@ -230,17 +264,25 @@ pub fn synthesize(ctx: &Context, term: &Term) -> Result<(Type, Context)> { } } -#[trace] +#[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())) } // ∀App rule - (Type::Polytype(_, _), _) => todo!(), + (Type::Polytype(a, ty_a), e) => { + let ex_s = gensym_existential(); + let ex = ContextEntry::ExistentialVar(ex_s.clone()); + 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) + } // âApp rule (Type::Existential(_), _) => todo!(), diff --git a/bidir/src/data.rs b/bidir/src/data.rs index 7020f30..7314fba 100644 --- a/bidir/src/data.rs +++ b/bidir/src/data.rs @@ -15,7 +15,7 @@ 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::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), @@ -94,12 +94,12 @@ impl Type { free_vars_with_context(&Context::default(), self) } - pub fn subst(&self, var: impl AsRef, replacement: &Type) -> Type { - let var = var.as_ref(); + pub fn subst(&self, var: &str, replacement: &Type) -> Type { match self { Type::Unit => Type::Unit, Type::Var(n) if n == var => replacement.clone(), 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::Arrow(a, b) => Type::Arrow( @@ -122,7 +122,7 @@ impl fmt::Debug for Monotype { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { Self::Unit => write!(f, "𝟙"), - Self::Var(arg0) => write!(f, "`{}", arg0), + Self::Var(arg0) => write!(f, "{}", arg0), Self::Existential(arg0) => write!(f, "{}", arg0), Self::Arrow(arg0, arg1) => write!(f, "({arg0:?} -> {arg1:?})"), } @@ -152,9 +152,9 @@ pub enum ContextEntry { impl fmt::Debug for ContextEntry { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { - Self::TypeVar(arg0) => write!(f, "`{}", arg0), + Self::TypeVar(arg0) => write!(f, "{}", arg0), Self::TermAnnot(arg0, arg1) => write!(f, "{} : {:?}", arg0, arg1), - Self::ExistentialVar(arg0) => write!(f, "`{}", arg0), + Self::ExistentialVar(arg0) => write!(f, "{}", arg0), Self::ExistentialSolved(arg0, arg1) => write!(f, "{} = {:?}", arg0, arg1), Self::Marker(arg0) => write!(f, "▶{}", arg0), } @@ -230,6 +230,7 @@ impl Context { self.lookup_existential(name).is_some() } + /// Returns a list of names of unsolved existentials pub fn unsolved_existentials(&self) -> HashSet { let mut unsolved = HashSet::new(); @@ -244,4 +245,24 @@ impl Context { unsolved } + + /// Returns (before, after) + pub fn split_by

(&self, p: P) -> Option<(Context, Context)> + where + P: Fn(&ContextEntry) -> bool, + { + let (before, after) = { + let idx = self.0.iter().position(p)?; + self.0.clone().split_at(idx) + }; + + Some((Context(before), Context(after))) + } + + 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 + } } diff --git a/bidir/src/lib.rs b/bidir/src/lib.rs index 4d24404..8951385 100644 --- a/bidir/src/lib.rs +++ b/bidir/src/lib.rs @@ -1,5 +1,7 @@ #[macro_use] extern crate trace; +#[macro_use] +extern crate tracing; use lalrpop_util::lalrpop_mod; diff --git a/bidir/src/tests.rs b/bidir/src/tests.rs index 5e540b7..9003c76 100644 --- a/bidir/src/tests.rs +++ b/bidir/src/tests.rs @@ -16,7 +16,7 @@ fn test_id() -> Result<()> { let id = id_term!(); let ctx = Context::default(); let (ty, out_ctx) = synthesize(&ctx, &id)?; - println!("Synthesis result: {ty:?} | {out_ctx:?}"); + bail!("Synthesized: {:?} (context = {:?})", ty, out_ctx); Ok(()) } @@ -27,6 +27,7 @@ fn test_id_of_unit() -> Result<()> { let id_of_unit = Term::App(Box::new(id), Box::new(Term::Unit)); let ctx = Context::default(); - bail!("Result: {:?}", synthesize(&ctx, &id_of_unit)); + let (ty, out_ctx) = synthesize(&ctx, &id_of_unit)?; + bail!("Synthesized: {:?} (context = {:?})", ty, out_ctx); Ok(()) }