diff options
| -rw-r--r-- | src/checker.rs | 1 | ||||
| -rw-r--r-- | src/checker_signature.rs | 9 | ||||
| -rw-r--r-- | src/checker_state.rs | 23 | ||||
| -rw-r--r-- | src/main.rs | 3 |
4 files changed, 19 insertions, 17 deletions
diff --git a/src/checker.rs b/src/checker.rs index adb5012..fdba181 100644 --- a/src/checker.rs +++ b/src/checker.rs @@ -16,7 +16,6 @@ impl CheckerState { let Programme(decls) = prog; for decl in decls { - debug!(%self, %decl); match decl { Decl::Set { name, set } => { self.assert_unbound_set(name)?; diff --git a/src/checker_signature.rs b/src/checker_signature.rs index 17154dd..bad38eb 100644 --- a/src/checker_signature.rs +++ b/src/checker_signature.rs @@ -1,5 +1,3 @@ -// Time-stamp: <2026-04-30 17h19 BST (9561bc0c)> - use crate::ast::*; use crate::checker_state::*; use std::collections::HashMap; @@ -443,12 +441,7 @@ impl CheckerState { let mut ctx = self.clone(); let first_set = ctx.check_set(¶ms[0].set)?; let element_checked = self.check_element(element, &first_set)?; - ctx.make_element_definition( - params[0].name.clone(), - element_checked, - first_set, - )?; - + ctx.add_element(params[0].name.clone(), element_checked.into(), first_set)?; if params.len() == 1 { ctx.check_instance(body, signature) } else { 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) } } diff --git a/src/main.rs b/src/main.rs index a395db8..eb16b32 100644 --- a/src/main.rs +++ b/src/main.rs @@ -35,6 +35,9 @@ let set NatEdges = record { target: set-of(natGraph .Node), connected: set-of(natGraph .Edge source target) } + +let element s_val : FinTwo = zero. {} +let element edge : set-of(natGraph .Edge s_val ( one. {} )) = true "#; let programme = parser::debug_parse(src); |