better gensym

Cargo.lock

@@ -19,6 +19,7 @@ name = "bidir"
 version = "0.1.0"
 dependencies = [
  "anyhow",
+ "dashmap",
  "im",
  "lazy_static",
  "parking_lot",
@@ -46,6 +47,25 @@ version = "1.0.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
 
+[[package]]
+name = "dashmap"
+version = "5.5.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "978747c1d849a7d2ee5e8adc0159961c48fb7e5db2f06af6723b80123bb53856"
+dependencies = [
+ "cfg-if",
+ "hashbrown",
+ "lock_api",
+ "once_cell",
+ "parking_lot_core",
+]
+
+[[package]]
+name = "hashbrown"
+version = "0.14.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f93e7192158dbcda357bdec5fb5788eebf8bbac027f3f33e719d29135ae84156"
+
 [[package]]
 name = "im"
 version = "15.1.0"
@@ -82,6 +102,12 @@ dependencies = [
  "scopeguard",
 ]
 
+[[package]]
+name = "once_cell"
+version = "1.18.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "dd8b5dd2ae5ed71462c540258bedcb51965123ad7e7ccf4b9a8cafaa4a63576d"
+
 [[package]]
 name = "parking_lot"
 version = "0.12.1"

bidir/Cargo.toml

@@ -7,6 +7,7 @@ edition = "2021"
 
 [dependencies]
 anyhow = "1.0.75"
+dashmap = "5.5.3"
 im = "15.1.0"
 lazy_static = "1.4.0"
 parking_lot = "0.12.1"

bidir/src/bidir.rs

@@ -3,10 +3,8 @@ use anyhow::{bail, Result};
 use crate::DEPTH;
 
 use crate::data::FreeVar;
-use crate::{
-  data::{Context, ContextEntry, Term, Type},
-  gensym::gensym_prefix,
-};
+use crate::data::{Context, ContextEntry, Term, Type};
+use crate::gensym::gensym_existential;
 
 // Figure 8. Applying a context, as a substitution, to a type
 
@@ -161,8 +159,8 @@ pub fn synthesize(ctx: &Context, term: &Term) -> Result<(Type, Context)> {
     // > not place a marker before ^α, because ^α and ^β appear in the output type
     // > (λx. e ⇒ ^α → ^β).
     Term::Lam(x, e) => {
-      let ex_a_s = gensym_prefix("ex");
-      let ex_b_s = gensym_prefix("ex");
+      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![

bidir/src/gensym.rs

@@ -1,18 +1,35 @@
+use dashmap::DashMap;
 use lazy_static::lazy_static;
-use parking_lot::Mutex;
 
-lazy_static! {
-  static ref CTR: Mutex<usize> = Mutex::new(0);
+thread_local! {
+  static CTRMAP: DashMap<&'static str, usize> = DashMap::new();
 }
 
-pub fn gensym() -> String {
-  gensym_prefix("var")
+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",
+];
+
+pub fn gensym_existential() -> String {
+  let result = idx("existential");
+  format!("{}\u{0302}", EXISTENTIALS[result])
 }
 
-pub fn gensym_prefix(prefix: impl AsRef<str>) -> String {
-  let mut g = CTR.lock();
-  let ctr = *g;
-  *g += 1;
-  drop(g);
-  format!("{}{}", prefix.as_ref(), ctr)
+pub fn gensym_type() -> String {
+  let result = idx("existential");
+  format!("{}\u{0302}", TYPEVARS[result])
+}
+
+fn idx(ty: &'static str) -> usize {
+  CTRMAP.with(|ctrmap| {
+    let mut g = ctrmap.entry(ty).or_insert(0);
+    let ctr = *g;
+    *g += 1;
+    ctr
+  })
 }