1use crate::reduce::ReducibilityHint;
6use crate::{Expr, Level, Name};
7
8use super::types::{
9 AnnotationTable, AxiomVal, BeforeAfter, BiMap, ConstantInfo, ConstantKind, ConstantVal,
10 ConstructorVal, DeclAttr, DeclDependencies, DeclFilter, DeclIndex, DeclKind, DeclSignature,
11 DeclVisibility, DefinitionSafety, DefinitionVal, DiagMeta, EventCounter, FrequencyTable,
12 Generation, IdDispenser, InductiveVal, IntervalSet, LoopClock, MemoSlot, QuotKind, QuotVal,
13 RecursorVal, RingBuffer, ScopeStack, SeqNum, SimpleLruCache, Slot, SparseBitSet,
14 StringInterner, Timestamp, TypedId, WorkQueue, WorkStack,
15};
16
17pub fn instantiate_level_params(expr: &Expr, param_names: &[Name], levels: &[Level]) -> Expr {
22 if param_names.is_empty() || levels.is_empty() {
23 return expr.clone();
24 }
25 instantiate_level_params_core(expr, param_names, levels)
26}
27fn instantiate_level_params_core(expr: &Expr, param_names: &[Name], levels: &[Level]) -> Expr {
28 match expr {
29 Expr::Sort(l) => {
30 let new_l = instantiate_level_param(l, param_names, levels);
31 Expr::Sort(new_l)
32 }
33 Expr::Const(name, ls) => {
34 let new_ls: Vec<Level> = ls
35 .iter()
36 .map(|l| instantiate_level_param(l, param_names, levels))
37 .collect();
38 Expr::Const(name.clone(), new_ls)
39 }
40 Expr::App(f, a) => {
41 let f_new = instantiate_level_params_core(f, param_names, levels);
42 let a_new = instantiate_level_params_core(a, param_names, levels);
43 Expr::App(Box::new(f_new), Box::new(a_new))
44 }
45 Expr::Lam(bi, name, ty, body) => {
46 let ty_new = instantiate_level_params_core(ty, param_names, levels);
47 let body_new = instantiate_level_params_core(body, param_names, levels);
48 Expr::Lam(*bi, name.clone(), Box::new(ty_new), Box::new(body_new))
49 }
50 Expr::Pi(bi, name, ty, body) => {
51 let ty_new = instantiate_level_params_core(ty, param_names, levels);
52 let body_new = instantiate_level_params_core(body, param_names, levels);
53 Expr::Pi(*bi, name.clone(), Box::new(ty_new), Box::new(body_new))
54 }
55 Expr::Let(name, ty, val, body) => {
56 let ty_new = instantiate_level_params_core(ty, param_names, levels);
57 let val_new = instantiate_level_params_core(val, param_names, levels);
58 let body_new = instantiate_level_params_core(body, param_names, levels);
59 Expr::Let(
60 name.clone(),
61 Box::new(ty_new),
62 Box::new(val_new),
63 Box::new(body_new),
64 )
65 }
66 Expr::Proj(name, idx, e) => {
67 let e_new = instantiate_level_params_core(e, param_names, levels);
68 Expr::Proj(name.clone(), *idx, Box::new(e_new))
69 }
70 Expr::BVar(_) | Expr::FVar(_) | Expr::Lit(_) => expr.clone(),
71 }
72}
73fn instantiate_level_param(level: &Level, param_names: &[Name], levels: &[Level]) -> Level {
75 match level {
76 Level::Param(name) => {
77 for (i, pn) in param_names.iter().enumerate() {
78 if pn == name {
79 if let Some(l) = levels.get(i) {
80 return l.clone();
81 }
82 }
83 }
84 level.clone()
85 }
86 Level::Succ(l) => Level::succ(instantiate_level_param(l, param_names, levels)),
87 Level::Max(l1, l2) => Level::max(
88 instantiate_level_param(l1, param_names, levels),
89 instantiate_level_param(l2, param_names, levels),
90 ),
91 Level::IMax(l1, l2) => Level::imax(
92 instantiate_level_param(l1, param_names, levels),
93 instantiate_level_param(l2, param_names, levels),
94 ),
95 Level::Zero | Level::MVar(_) => level.clone(),
96 }
97}
98#[cfg(test)]
99mod tests {
100 use super::*;
101 use crate::BinderInfo;
102 #[test]
103 fn test_constant_info_accessors() {
104 let info = ConstantInfo::Axiom(AxiomVal {
105 common: ConstantVal {
106 name: Name::str("propext"),
107 level_params: vec![],
108 ty: Expr::Sort(Level::zero()),
109 },
110 is_unsafe: false,
111 });
112 assert_eq!(info.name(), &Name::str("propext"));
113 assert!(info.is_axiom());
114 assert!(!info.is_unsafe());
115 assert!(!info.has_value(false));
116 }
117 #[test]
118 fn test_definition_val() {
119 let info = ConstantInfo::Definition(DefinitionVal {
120 common: ConstantVal {
121 name: Name::str("id"),
122 level_params: vec![Name::str("u")],
123 ty: Expr::Sort(Level::param(Name::str("u"))),
124 },
125 value: Expr::Lam(
126 BinderInfo::Default,
127 Name::str("x"),
128 Box::new(Expr::BVar(0)),
129 Box::new(Expr::BVar(0)),
130 ),
131 hints: ReducibilityHint::Abbrev,
132 safety: DefinitionSafety::Safe,
133 all: vec![Name::str("id")],
134 });
135 assert!(info.is_definition());
136 assert!(info.has_value(false));
137 assert_eq!(info.reducibility_hint(), ReducibilityHint::Abbrev);
138 }
139 #[test]
140 fn test_recursor_major_idx() {
141 let rec = RecursorVal {
142 common: ConstantVal {
143 name: Name::str("Nat.rec"),
144 level_params: vec![Name::str("u")],
145 ty: Expr::Sort(Level::zero()),
146 },
147 all: vec![Name::str("Nat")],
148 num_params: 0,
149 num_indices: 0,
150 num_motives: 1,
151 num_minors: 2,
152 rules: vec![],
153 k: false,
154 is_unsafe: false,
155 };
156 assert_eq!(rec.get_major_idx(), 3);
157 }
158 #[test]
159 fn test_constructor_val() {
160 let info = ConstantInfo::Constructor(ConstructorVal {
161 common: ConstantVal {
162 name: Name::str("Nat.succ"),
163 level_params: vec![],
164 ty: Expr::Sort(Level::zero()),
165 },
166 induct: Name::str("Nat"),
167 cidx: 1,
168 num_params: 0,
169 num_fields: 1,
170 is_unsafe: false,
171 });
172 assert!(info.is_constructor());
173 let ctor = info.to_constructor_val().expect("ctor should be present");
174 assert_eq!(ctor.induct, Name::str("Nat"));
175 assert_eq!(ctor.cidx, 1);
176 assert_eq!(ctor.num_fields, 1);
177 }
178 #[test]
179 fn test_inductive_val() {
180 let info = ConstantInfo::Inductive(InductiveVal {
181 common: ConstantVal {
182 name: Name::str("Nat"),
183 level_params: vec![],
184 ty: Expr::Sort(Level::succ(Level::zero())),
185 },
186 num_params: 0,
187 num_indices: 0,
188 all: vec![Name::str("Nat")],
189 ctors: vec![Name::str("Nat.zero"), Name::str("Nat.succ")],
190 num_nested: 0,
191 is_rec: true,
192 is_unsafe: false,
193 is_reflexive: false,
194 is_prop: false,
195 });
196 assert!(info.is_inductive());
197 assert!(!info.is_structure_like());
198 let ind = info.to_inductive_val().expect("ind should be present");
199 assert_eq!(ind.ctors.len(), 2);
200 }
201 #[test]
202 fn test_structure_like() {
203 let info = ConstantInfo::Inductive(InductiveVal {
204 common: ConstantVal {
205 name: Name::str("Prod"),
206 level_params: vec![Name::str("u"), Name::str("v")],
207 ty: Expr::Sort(Level::zero()),
208 },
209 num_params: 2,
210 num_indices: 0,
211 all: vec![Name::str("Prod")],
212 ctors: vec![Name::str("Prod.mk")],
213 num_nested: 0,
214 is_rec: false,
215 is_unsafe: false,
216 is_reflexive: false,
217 is_prop: false,
218 });
219 assert!(info.is_structure_like());
220 }
221 #[test]
222 fn test_instantiate_level_params() {
223 let expr = Expr::Sort(Level::param(Name::str("u")));
224 let result =
225 instantiate_level_params(&expr, &[Name::str("u")], &[Level::succ(Level::zero())]);
226 assert_eq!(result, Expr::Sort(Level::succ(Level::zero())));
227 }
228 #[test]
229 fn test_instantiate_level_params_const() {
230 let expr = Expr::Const(Name::str("List"), vec![Level::param(Name::str("u"))]);
231 let result = instantiate_level_params(&expr, &[Name::str("u")], &[Level::zero()]);
232 assert_eq!(result, Expr::Const(Name::str("List"), vec![Level::zero()]));
233 }
234 #[test]
235 fn test_quot_val() {
236 let info = ConstantInfo::Quotient(QuotVal {
237 common: ConstantVal {
238 name: Name::str("Quot"),
239 level_params: vec![Name::str("u")],
240 ty: Expr::Sort(Level::zero()),
241 },
242 kind: QuotKind::Type,
243 });
244 assert!(info.is_quotient());
245 let qv = info.to_quotient_val().expect("qv should be present");
246 assert_eq!(qv.kind, QuotKind::Type);
247 }
248}
249pub fn collect_level_params_in_expr(e: &Expr) -> Vec<Name> {
251 let mut result = Vec::new();
252 collect_level_params_in_expr_impl(e, &mut result);
253 result
254}
255fn collect_level_params_in_expr_impl(e: &Expr, out: &mut Vec<Name>) {
256 match e {
257 Expr::Sort(level) => collect_level_params_in_level(level, out),
258 Expr::Const(_, levels) => {
259 for l in levels {
260 collect_level_params_in_level(l, out);
261 }
262 }
263 Expr::App(f, a) => {
264 collect_level_params_in_expr_impl(f, out);
265 collect_level_params_in_expr_impl(a, out);
266 }
267 Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
268 collect_level_params_in_expr_impl(ty, out);
269 collect_level_params_in_expr_impl(body, out);
270 }
271 Expr::Let(_, ty, val, body) => {
272 collect_level_params_in_expr_impl(ty, out);
273 collect_level_params_in_expr_impl(val, out);
274 collect_level_params_in_expr_impl(body, out);
275 }
276 _ => {}
277 }
278}
279fn collect_level_params_in_level(l: &Level, out: &mut Vec<Name>) {
280 match l {
281 Level::Param(n) if !out.contains(n) => {
282 out.push(n.clone());
283 }
284 Level::Param(_) => {}
285 Level::Succ(inner) => collect_level_params_in_level(inner, out),
286 Level::Max(a, b) | Level::IMax(a, b) => {
287 collect_level_params_in_level(a, out);
288 collect_level_params_in_level(b, out);
289 }
290 _ => {}
291 }
292}
293pub fn check_level_params_consistent(e: &Expr, declared: &[Name]) -> Result<(), Name> {
295 let found = collect_level_params_in_expr(e);
296 for p in found {
297 if !declared.contains(&p) {
298 return Err(p);
299 }
300 }
301 Ok(())
302}
303#[cfg(test)]
304mod extended_tests {
305 use super::*;
306 fn mk_axiom(name: &str) -> ConstantInfo {
307 ConstantInfo::Axiom(AxiomVal {
308 common: ConstantVal {
309 name: Name::str(name),
310 level_params: vec![],
311 ty: Expr::Sort(Level::zero()),
312 },
313 is_unsafe: false,
314 })
315 }
316 fn mk_poly_axiom(name: &str, params: Vec<&str>) -> ConstantInfo {
317 ConstantInfo::Axiom(AxiomVal {
318 common: ConstantVal {
319 name: Name::str(name),
320 level_params: params.into_iter().map(Name::str).collect(),
321 ty: Expr::Sort(Level::zero()),
322 },
323 is_unsafe: false,
324 })
325 }
326 #[test]
327 fn test_constant_kind_axiom() {
328 let info = mk_axiom("Foo");
329 assert_eq!(info.kind(), ConstantKind::Axiom);
330 }
331 #[test]
332 fn test_kind_as_str() {
333 assert_eq!(ConstantKind::Axiom.as_str(), "axiom");
334 assert_eq!(ConstantKind::Definition.as_str(), "definition");
335 assert_eq!(ConstantKind::Theorem.as_str(), "theorem");
336 assert_eq!(ConstantKind::Inductive.as_str(), "inductive");
337 assert_eq!(ConstantKind::Constructor.as_str(), "constructor");
338 assert_eq!(ConstantKind::Recursor.as_str(), "recursor");
339 assert_eq!(ConstantKind::Quotient.as_str(), "quotient");
340 }
341 #[test]
342 fn test_kind_has_body() {
343 assert!(ConstantKind::Definition.has_body());
344 assert!(ConstantKind::Theorem.has_body());
345 assert!(ConstantKind::Opaque.has_body());
346 assert!(!ConstantKind::Axiom.has_body());
347 assert!(!ConstantKind::Inductive.has_body());
348 }
349 #[test]
350 fn test_kind_is_inductive_family() {
351 assert!(ConstantKind::Inductive.is_inductive_family());
352 assert!(ConstantKind::Constructor.is_inductive_family());
353 assert!(ConstantKind::Recursor.is_inductive_family());
354 assert!(!ConstantKind::Axiom.is_inductive_family());
355 assert!(!ConstantKind::Definition.is_inductive_family());
356 }
357 #[test]
358 fn test_num_level_params() {
359 let mono = mk_axiom("Foo");
360 assert_eq!(mono.num_level_params(), 0);
361 assert!(!mono.is_polymorphic());
362 let poly = mk_poly_axiom("Bar", vec!["u", "v"]);
363 assert_eq!(poly.num_level_params(), 2);
364 assert!(poly.is_polymorphic());
365 }
366 #[test]
367 fn test_summarize() {
368 let info = mk_poly_axiom("MyAxiom", vec!["u"]);
369 let s = info.summarize();
370 assert_eq!(s.name, Name::str("MyAxiom"));
371 assert_eq!(s.kind, ConstantKind::Axiom);
372 assert_eq!(s.num_level_params, 1);
373 assert!(s.is_polymorphic);
374 }
375 #[test]
376 fn test_display_string_monomorphic() {
377 let info = mk_axiom("Foo");
378 let s = info.display_string();
379 assert!(s.contains("axiom"));
380 assert!(s.contains("Foo"));
381 }
382 #[test]
383 fn test_display_string_polymorphic() {
384 let info = mk_poly_axiom("Bar", vec!["u", "v"]);
385 let s = info.display_string();
386 assert!(s.contains("axiom"));
387 assert!(s.contains("Bar"));
388 assert!(s.contains("u"));
389 }
390 #[test]
391 fn test_definition_safety() {
392 assert!(DefinitionSafety::Safe.is_safe());
393 assert!(!DefinitionSafety::Unsafe.is_safe());
394 assert!(DefinitionSafety::Partial.is_partial());
395 assert!(!DefinitionSafety::Safe.is_partial());
396 assert_eq!(DefinitionSafety::Safe.as_str(), "safe");
397 assert_eq!(DefinitionSafety::Unsafe.as_str(), "unsafe");
398 assert_eq!(DefinitionSafety::Partial.as_str(), "partial");
399 }
400 #[test]
401 fn test_collect_level_params_in_sort() {
402 let e = Expr::Sort(Level::Param(Name::str("u")));
403 let params = collect_level_params_in_expr(&e);
404 assert_eq!(params, vec![Name::str("u")]);
405 }
406 #[test]
407 fn test_collect_level_params_in_const() {
408 let e = Expr::Const(
409 Name::str("List"),
410 vec![Level::Param(Name::str("u")), Level::zero()],
411 );
412 let params = collect_level_params_in_expr(&e);
413 assert!(params.contains(&Name::str("u")));
414 assert_eq!(params.len(), 1);
415 }
416 #[test]
417 fn test_check_level_params_consistent_ok() {
418 let e = Expr::Sort(Level::Param(Name::str("u")));
419 assert!(check_level_params_consistent(&e, &[Name::str("u")]).is_ok());
420 }
421 #[test]
422 fn test_check_level_params_consistent_fail() {
423 let e = Expr::Sort(Level::Param(Name::str("v")));
424 let result = check_level_params_consistent(&e, &[Name::str("u")]);
425 assert!(result.is_err());
426 assert_eq!(result.unwrap_err(), Name::str("v"));
427 }
428 #[test]
429 fn test_parent_inductive() {
430 let info = mk_axiom("Foo");
431 assert!(info.parent_inductive().is_none());
432 }
433}
434#[cfg(test)]
435mod tests_declaration_extra {
436 use super::*;
437 #[test]
438 fn test_decl_kind() {
439 assert!(DeclKind::Theorem.has_body());
440 assert!(!DeclKind::Axiom.has_body());
441 assert!(DeclKind::Inductive.is_type_decl());
442 assert!(!DeclKind::Theorem.is_type_decl());
443 assert_eq!(DeclKind::Theorem.label(), "theorem");
444 }
445 #[test]
446 fn test_decl_visibility() {
447 assert!(DeclVisibility::Public.is_externally_visible());
448 assert!(!DeclVisibility::Private.is_externally_visible());
449 }
450 #[test]
451 fn test_decl_attr() {
452 let a = DeclAttr::Simp;
453 assert_eq!(a.name(), "simp");
454 let u = DeclAttr::Unknown("myattr".into());
455 assert_eq!(u.name(), "myattr");
456 }
457 #[test]
458 fn test_decl_signature() {
459 let sig = DeclSignature::new("Nat.succ", "Nat → Nat").with_uparam("u");
460 assert_eq!(sig.name, "Nat.succ");
461 assert!(sig.is_universe_poly());
462 assert_eq!(sig.uparams, vec!["u".to_string()]);
463 }
464 #[test]
465 fn test_decl_index() {
466 let mut idx = DeclIndex::new();
467 idx.insert("Nat.succ", 0);
468 idx.insert("Nat.zero", 1);
469 assert_eq!(idx.get("Nat.succ"), Some(0));
470 assert_eq!(idx.get("missing"), None);
471 assert_eq!(idx.len(), 2);
472 }
473 #[test]
474 fn test_decl_dependencies() {
475 let mut deps = DeclDependencies::new(3);
476 deps.add(1, 0);
477 deps.add(2, 0);
478 deps.add(2, 1);
479 assert!(deps.directly_depends(1, 0));
480 assert!(!deps.directly_depends(0, 1));
481 assert_eq!(deps.total_edges(), 3);
482 }
483}
484#[cfg(test)]
485mod tests_decl_filter {
486 use super::*;
487 #[test]
488 fn test_decl_filter() {
489 let filter = DeclFilter::accept_all()
490 .with_kinds(vec![DeclKind::Theorem, DeclKind::Axiom])
491 .in_namespace("Nat");
492 let sig = DeclSignature::new("Nat.zero_add", "∀ n, 0 + n = n");
493 assert!(filter.accepts(&sig, DeclKind::Theorem, &[]));
494 let other = DeclSignature::new("List.length", "List α → Nat");
495 assert!(!filter.accepts(&other, DeclKind::Definition, &[]));
496 }
497 #[test]
498 fn test_decl_filter_attr() {
499 let filter = DeclFilter::accept_all().with_attr(DeclAttr::Simp);
500 let sig = DeclSignature::new("Foo.bar", "Prop");
501 assert!(!filter.accepts(&sig, DeclKind::Theorem, &[DeclAttr::Inline]));
502 assert!(filter.accepts(&sig, DeclKind::Theorem, &[DeclAttr::Simp]));
503 }
504}
505#[cfg(test)]
506mod tests_common_infra {
507 use super::*;
508 #[test]
509 fn test_event_counter() {
510 let mut ec = EventCounter::new();
511 ec.inc("hit");
512 ec.inc("hit");
513 ec.inc("miss");
514 assert_eq!(ec.get("hit"), 2);
515 assert_eq!(ec.get("miss"), 1);
516 assert_eq!(ec.total(), 3);
517 ec.reset();
518 assert_eq!(ec.total(), 0);
519 }
520 #[test]
521 fn test_diag_meta() {
522 let mut m = DiagMeta::new();
523 m.add("os", "linux");
524 m.add("arch", "x86_64");
525 assert_eq!(m.get("os"), Some("linux"));
526 assert_eq!(m.len(), 2);
527 let s = m.to_string();
528 assert!(s.contains("os=linux"));
529 }
530 #[test]
531 fn test_scope_stack() {
532 let mut ss = ScopeStack::new();
533 ss.push("Nat");
534 ss.push("succ");
535 assert_eq!(ss.current(), Some("succ"));
536 assert_eq!(ss.depth(), 2);
537 assert_eq!(ss.path(), "Nat.succ");
538 ss.pop();
539 assert_eq!(ss.current(), Some("Nat"));
540 }
541 #[test]
542 fn test_annotation_table() {
543 let mut tbl = AnnotationTable::new();
544 tbl.annotate("doc", "first line");
545 tbl.annotate("doc", "second line");
546 assert_eq!(tbl.get_all("doc").len(), 2);
547 assert!(tbl.has("doc"));
548 assert!(!tbl.has("other"));
549 }
550 #[test]
551 fn test_work_stack() {
552 let mut ws = WorkStack::new();
553 ws.push(1u32);
554 ws.push(2u32);
555 assert_eq!(ws.pop(), Some(2));
556 assert_eq!(ws.len(), 1);
557 }
558 #[test]
559 fn test_work_queue() {
560 let mut wq = WorkQueue::new();
561 wq.enqueue(1u32);
562 wq.enqueue(2u32);
563 assert_eq!(wq.dequeue(), Some(1));
564 assert_eq!(wq.len(), 1);
565 }
566 #[test]
567 fn test_sparse_bit_set() {
568 let mut bs = SparseBitSet::new(128);
569 bs.set(5);
570 bs.set(63);
571 bs.set(64);
572 assert!(bs.get(5));
573 assert!(bs.get(63));
574 assert!(bs.get(64));
575 assert!(!bs.get(0));
576 assert_eq!(bs.count_ones(), 3);
577 bs.clear(5);
578 assert!(!bs.get(5));
579 }
580 #[test]
581 fn test_loop_clock() {
582 let mut clk = LoopClock::start();
583 for _ in 0..10 {
584 clk.tick();
585 }
586 assert_eq!(clk.iters(), 10);
587 assert!(clk.elapsed_us() >= 0.0);
588 }
589}
590#[cfg(test)]
591mod tests_extra_data_structures {
592 use super::*;
593 #[test]
594 fn test_simple_lru_cache() {
595 let mut cache: SimpleLruCache<&str, u32> = SimpleLruCache::new(3);
596 cache.put("a", 1);
597 cache.put("b", 2);
598 cache.put("c", 3);
599 assert_eq!(cache.get(&"a"), Some(&1));
600 cache.put("d", 4);
601 assert!(cache.len() <= 3);
602 }
603 #[test]
604 fn test_string_interner() {
605 let mut si = StringInterner::new();
606 let id1 = si.intern("hello");
607 let id2 = si.intern("hello");
608 assert_eq!(id1, id2);
609 let id3 = si.intern("world");
610 assert_ne!(id1, id3);
611 assert_eq!(si.get(id1), Some("hello"));
612 assert_eq!(si.len(), 2);
613 }
614 #[test]
615 fn test_frequency_table() {
616 let mut ft = FrequencyTable::new();
617 ft.record("a");
618 ft.record("b");
619 ft.record("a");
620 ft.record("a");
621 assert_eq!(ft.freq(&"a"), 3);
622 assert_eq!(ft.freq(&"b"), 1);
623 assert_eq!(ft.most_frequent(), Some((&"a", 3)));
624 assert_eq!(ft.total(), 4);
625 assert_eq!(ft.distinct(), 2);
626 }
627 #[test]
628 fn test_bimap() {
629 let mut bm: BiMap<u32, &str> = BiMap::new();
630 bm.insert(1, "one");
631 bm.insert(2, "two");
632 assert_eq!(bm.get_b(&1), Some(&"one"));
633 assert_eq!(bm.get_a(&"two"), Some(&2));
634 assert_eq!(bm.len(), 2);
635 }
636}
637#[cfg(test)]
638mod tests_interval_set {
639 use super::*;
640 #[test]
641 fn test_interval_set() {
642 let mut s = IntervalSet::new();
643 s.add(1, 5);
644 s.add(3, 8);
645 assert_eq!(s.num_intervals(), 1);
646 assert_eq!(s.cardinality(), 8);
647 assert!(s.contains(4));
648 assert!(!s.contains(9));
649 s.add(10, 15);
650 assert_eq!(s.num_intervals(), 2);
651 }
652}
653#[allow(dead_code)]
655pub fn now_us() -> Timestamp {
656 let us = std::time::SystemTime::UNIX_EPOCH
657 .elapsed()
658 .map(|d| d.as_micros() as u64)
659 .unwrap_or(0);
660 Timestamp::from_us(us)
661}
662#[cfg(test)]
663mod tests_typed_utilities {
664 use super::*;
665 #[test]
666 fn test_timestamp() {
667 let t1 = Timestamp::from_us(1000);
668 let t2 = Timestamp::from_us(1500);
669 assert_eq!(t2.elapsed_since(t1), 500);
670 assert!(t1 < t2);
671 }
672 #[test]
673 fn test_typed_id() {
674 struct Foo;
675 let id: TypedId<Foo> = TypedId::new(42);
676 assert_eq!(id.raw(), 42);
677 assert_eq!(format!("{id}"), "#42");
678 }
679 #[test]
680 fn test_id_dispenser() {
681 struct Bar;
682 let mut disp: IdDispenser<Bar> = IdDispenser::new();
683 let a = disp.next();
684 let b = disp.next();
685 assert_eq!(a.raw(), 0);
686 assert_eq!(b.raw(), 1);
687 assert_eq!(disp.count(), 2);
688 }
689 #[test]
690 fn test_slot() {
691 let mut slot: Slot<u32> = Slot::empty();
692 assert!(!slot.is_filled());
693 slot.fill(99);
694 assert!(slot.is_filled());
695 assert_eq!(slot.get(), Some(&99));
696 let v = slot.take();
697 assert_eq!(v, Some(99));
698 assert!(!slot.is_filled());
699 }
700 #[test]
701 #[should_panic]
702 fn test_slot_double_fill() {
703 let mut slot: Slot<u32> = Slot::empty();
704 slot.fill(1);
705 slot.fill(2);
706 }
707 #[test]
708 fn test_memo_slot() {
709 let mut ms: MemoSlot<u32> = MemoSlot::new();
710 assert!(!ms.is_cached());
711 let val = ms.get_or_compute(|| 42);
712 assert_eq!(*val, 42);
713 assert!(ms.is_cached());
714 ms.invalidate();
715 assert!(!ms.is_cached());
716 }
717}
718#[cfg(test)]
719mod tests_ring_buffer {
720 use super::*;
721 #[test]
722 fn test_ring_buffer() {
723 let mut rb = RingBuffer::new(3);
724 rb.push(1u32);
725 rb.push(2u32);
726 rb.push(3u32);
727 assert!(rb.is_full());
728 rb.push(4u32);
729 assert_eq!(rb.pop(), Some(2));
730 assert_eq!(rb.len(), 2);
731 }
732 #[test]
733 fn test_before_after() {
734 let ba = BeforeAfter::new(10u32, 10u32);
735 assert!(ba.unchanged());
736 let ba2 = BeforeAfter::new(10u32, 20u32);
737 assert!(!ba2.unchanged());
738 }
739 #[test]
740 fn test_seq_num() {
741 let s = SeqNum::ZERO;
742 assert_eq!(s.value(), 0);
743 let s2 = s.next();
744 assert_eq!(s2.value(), 1);
745 assert!(s < s2);
746 }
747 #[test]
748 fn test_generation() {
749 let g0 = Generation::INITIAL;
750 let g1 = g0.advance();
751 assert_eq!(g0.number(), 0);
752 assert_eq!(g1.number(), 1);
753 assert_ne!(g0, g1);
754 }
755}