add monotic counters, fix element binding case in app->for

1 files changed, 15 insertions, 8 deletions

diff --git a/src/checker_state.rs b/src/checker_state.rs
index a0fe6b1..3d933f2 100644
--- a/src/checker_state.rs
+++ b/src/checker_state.rs
@@ -1,9 +1,12 @@
 use crate::ast::*;
-use tracing::instrument;
 
 use derive_more::Display;
+use tracing::instrument;
+
 use std::collections::HashMap;
 use std::fmt;
+use std::sync::Arc;
+use std::sync::atomic::{AtomicUsize, Ordering};
 
 #[derive(Display)]
 pub enum CheckerError {
@@ -115,9 +118,8 @@ pub struct CheckerState {
     record_fields: HashMap<String, Field<Set>>,
     variant_fields: HashMap<String, Field<Set>>,
     signature_fields: HashMap<String, Field<Signature>>,
-    // TODO: do we need to make these strictly monotonic somewhere somehow?
-    binder_element: usize,
-    unique_name: usize,
+    binder_element: Arc<AtomicUsize>,
+    unique_name: Arc<AtomicUsize>,
 }
 
 impl fmt::Display for CheckerState {
@@ -427,11 +429,16 @@ impl CheckerState {
 
 // -----------------------------------------------------------------------------
 // Bindings
+
+fn _reserved_name(n: usize) -> String {
+    format!("#{}", n)
+}
+
 impl CheckerState {
     fn _make_canonical_element(&mut self, name: String, set: Set) -> Result<String, CheckerError> {
-        let canonical = format!("_#{}", self.binder_element);
+        let n = self.binder_element.fetch_add(1, Ordering::Relaxed);
+        let canonical = _reserved_name(n);
         self.add_element(name, Element::Var(canonical.clone()).into(), set)?;
-        self.binder_element += 1;
         Ok(canonical)
     }
 
@@ -456,7 +463,7 @@ impl CheckerState {
 
     #[instrument(skip(self))]
     pub fn make_unique_name(&mut self) -> String {
-        self.unique_name += 1;
-        format!("_#{}", self.unique_name)
+        let n = self.unique_name.fetch_add(1, Ordering::Relaxed);
+        _reserved_name(n)
     }
 }