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) => {
282 if !out.contains(n) {
283 out.push(n.clone());
284 }
285 }
286 Level::Succ(inner) => collect_level_params_in_level(inner, out),
287 Level::Max(a, b) | Level::IMax(a, b) => {
288 collect_level_params_in_level(a, out);
289 collect_level_params_in_level(b, out);
290 }
291 _ => {}
292 }
293}
294pub fn check_level_params_consistent(e: &Expr, declared: &[Name]) -> Result<(), Name> {
296 let found = collect_level_params_in_expr(e);
297 for p in found {
298 if !declared.contains(&p) {
299 return Err(p);
300 }
301 }
302 Ok(())
303}
304#[cfg(test)]
305mod extended_tests {
306 use super::*;
307 fn mk_axiom(name: &str) -> ConstantInfo {
308 ConstantInfo::Axiom(AxiomVal {
309 common: ConstantVal {
310 name: Name::str(name),
311 level_params: vec![],
312 ty: Expr::Sort(Level::zero()),
313 },
314 is_unsafe: false,
315 })
316 }
317 fn mk_poly_axiom(name: &str, params: Vec<&str>) -> ConstantInfo {
318 ConstantInfo::Axiom(AxiomVal {
319 common: ConstantVal {
320 name: Name::str(name),
321 level_params: params.into_iter().map(Name::str).collect(),
322 ty: Expr::Sort(Level::zero()),
323 },
324 is_unsafe: false,
325 })
326 }
327 #[test]
328 fn test_constant_kind_axiom() {
329 let info = mk_axiom("Foo");
330 assert_eq!(info.kind(), ConstantKind::Axiom);
331 }
332 #[test]
333 fn test_kind_as_str() {
334 assert_eq!(ConstantKind::Axiom.as_str(), "axiom");
335 assert_eq!(ConstantKind::Definition.as_str(), "definition");
336 assert_eq!(ConstantKind::Theorem.as_str(), "theorem");
337 assert_eq!(ConstantKind::Inductive.as_str(), "inductive");
338 assert_eq!(ConstantKind::Constructor.as_str(), "constructor");
339 assert_eq!(ConstantKind::Recursor.as_str(), "recursor");
340 assert_eq!(ConstantKind::Quotient.as_str(), "quotient");
341 }
342 #[test]
343 fn test_kind_has_body() {
344 assert!(ConstantKind::Definition.has_body());
345 assert!(ConstantKind::Theorem.has_body());
346 assert!(ConstantKind::Opaque.has_body());
347 assert!(!ConstantKind::Axiom.has_body());
348 assert!(!ConstantKind::Inductive.has_body());
349 }
350 #[test]
351 fn test_kind_is_inductive_family() {
352 assert!(ConstantKind::Inductive.is_inductive_family());
353 assert!(ConstantKind::Constructor.is_inductive_family());
354 assert!(ConstantKind::Recursor.is_inductive_family());
355 assert!(!ConstantKind::Axiom.is_inductive_family());
356 assert!(!ConstantKind::Definition.is_inductive_family());
357 }
358 #[test]
359 fn test_num_level_params() {
360 let mono = mk_axiom("Foo");
361 assert_eq!(mono.num_level_params(), 0);
362 assert!(!mono.is_polymorphic());
363 let poly = mk_poly_axiom("Bar", vec!["u", "v"]);
364 assert_eq!(poly.num_level_params(), 2);
365 assert!(poly.is_polymorphic());
366 }
367 #[test]
368 fn test_summarize() {
369 let info = mk_poly_axiom("MyAxiom", vec!["u"]);
370 let s = info.summarize();
371 assert_eq!(s.name, Name::str("MyAxiom"));
372 assert_eq!(s.kind, ConstantKind::Axiom);
373 assert_eq!(s.num_level_params, 1);
374 assert!(s.is_polymorphic);
375 }
376 #[test]
377 fn test_display_string_monomorphic() {
378 let info = mk_axiom("Foo");
379 let s = info.display_string();
380 assert!(s.contains("axiom"));
381 assert!(s.contains("Foo"));
382 }
383 #[test]
384 fn test_display_string_polymorphic() {
385 let info = mk_poly_axiom("Bar", vec!["u", "v"]);
386 let s = info.display_string();
387 assert!(s.contains("axiom"));
388 assert!(s.contains("Bar"));
389 assert!(s.contains("u"));
390 }
391 #[test]
392 fn test_definition_safety() {
393 assert!(DefinitionSafety::Safe.is_safe());
394 assert!(!DefinitionSafety::Unsafe.is_safe());
395 assert!(DefinitionSafety::Partial.is_partial());
396 assert!(!DefinitionSafety::Safe.is_partial());
397 assert_eq!(DefinitionSafety::Safe.as_str(), "safe");
398 assert_eq!(DefinitionSafety::Unsafe.as_str(), "unsafe");
399 assert_eq!(DefinitionSafety::Partial.as_str(), "partial");
400 }
401 #[test]
402 fn test_collect_level_params_in_sort() {
403 let e = Expr::Sort(Level::Param(Name::str("u")));
404 let params = collect_level_params_in_expr(&e);
405 assert_eq!(params, vec![Name::str("u")]);
406 }
407 #[test]
408 fn test_collect_level_params_in_const() {
409 let e = Expr::Const(
410 Name::str("List"),
411 vec![Level::Param(Name::str("u")), Level::zero()],
412 );
413 let params = collect_level_params_in_expr(&e);
414 assert!(params.contains(&Name::str("u")));
415 assert_eq!(params.len(), 1);
416 }
417 #[test]
418 fn test_check_level_params_consistent_ok() {
419 let e = Expr::Sort(Level::Param(Name::str("u")));
420 assert!(check_level_params_consistent(&e, &[Name::str("u")]).is_ok());
421 }
422 #[test]
423 fn test_check_level_params_consistent_fail() {
424 let e = Expr::Sort(Level::Param(Name::str("v")));
425 let result = check_level_params_consistent(&e, &[Name::str("u")]);
426 assert!(result.is_err());
427 assert_eq!(result.unwrap_err(), Name::str("v"));
428 }
429 #[test]
430 fn test_parent_inductive() {
431 let info = mk_axiom("Foo");
432 assert!(info.parent_inductive().is_none());
433 }
434}
435#[cfg(test)]
436mod tests_declaration_extra {
437 use super::*;
438 #[test]
439 fn test_decl_kind() {
440 assert!(DeclKind::Theorem.has_body());
441 assert!(!DeclKind::Axiom.has_body());
442 assert!(DeclKind::Inductive.is_type_decl());
443 assert!(!DeclKind::Theorem.is_type_decl());
444 assert_eq!(DeclKind::Theorem.label(), "theorem");
445 }
446 #[test]
447 fn test_decl_visibility() {
448 assert!(DeclVisibility::Public.is_externally_visible());
449 assert!(!DeclVisibility::Private.is_externally_visible());
450 }
451 #[test]
452 fn test_decl_attr() {
453 let a = DeclAttr::Simp;
454 assert_eq!(a.name(), "simp");
455 let u = DeclAttr::Unknown("myattr".into());
456 assert_eq!(u.name(), "myattr");
457 }
458 #[test]
459 fn test_decl_signature() {
460 let sig = DeclSignature::new("Nat.succ", "Nat → Nat").with_uparam("u");
461 assert_eq!(sig.name, "Nat.succ");
462 assert!(sig.is_universe_poly());
463 assert_eq!(sig.uparams, vec!["u".to_string()]);
464 }
465 #[test]
466 fn test_decl_index() {
467 let mut idx = DeclIndex::new();
468 idx.insert("Nat.succ", 0);
469 idx.insert("Nat.zero", 1);
470 assert_eq!(idx.get("Nat.succ"), Some(0));
471 assert_eq!(idx.get("missing"), None);
472 assert_eq!(idx.len(), 2);
473 }
474 #[test]
475 fn test_decl_dependencies() {
476 let mut deps = DeclDependencies::new(3);
477 deps.add(1, 0);
478 deps.add(2, 0);
479 deps.add(2, 1);
480 assert!(deps.directly_depends(1, 0));
481 assert!(!deps.directly_depends(0, 1));
482 assert_eq!(deps.total_edges(), 3);
483 }
484}
485#[cfg(test)]
486mod tests_decl_filter {
487 use super::*;
488 #[test]
489 fn test_decl_filter() {
490 let filter = DeclFilter::accept_all()
491 .with_kinds(vec![DeclKind::Theorem, DeclKind::Axiom])
492 .in_namespace("Nat");
493 let sig = DeclSignature::new("Nat.zero_add", "∀ n, 0 + n = n");
494 assert!(filter.accepts(&sig, DeclKind::Theorem, &[]));
495 let other = DeclSignature::new("List.length", "List α → Nat");
496 assert!(!filter.accepts(&other, DeclKind::Definition, &[]));
497 }
498 #[test]
499 fn test_decl_filter_attr() {
500 let filter = DeclFilter::accept_all().with_attr(DeclAttr::Simp);
501 let sig = DeclSignature::new("Foo.bar", "Prop");
502 assert!(!filter.accepts(&sig, DeclKind::Theorem, &[DeclAttr::Inline]));
503 assert!(filter.accepts(&sig, DeclKind::Theorem, &[DeclAttr::Simp]));
504 }
505}
506#[cfg(test)]
507mod tests_common_infra {
508 use super::*;
509 #[test]
510 fn test_event_counter() {
511 let mut ec = EventCounter::new();
512 ec.inc("hit");
513 ec.inc("hit");
514 ec.inc("miss");
515 assert_eq!(ec.get("hit"), 2);
516 assert_eq!(ec.get("miss"), 1);
517 assert_eq!(ec.total(), 3);
518 ec.reset();
519 assert_eq!(ec.total(), 0);
520 }
521 #[test]
522 fn test_diag_meta() {
523 let mut m = DiagMeta::new();
524 m.add("os", "linux");
525 m.add("arch", "x86_64");
526 assert_eq!(m.get("os"), Some("linux"));
527 assert_eq!(m.len(), 2);
528 let s = m.to_string();
529 assert!(s.contains("os=linux"));
530 }
531 #[test]
532 fn test_scope_stack() {
533 let mut ss = ScopeStack::new();
534 ss.push("Nat");
535 ss.push("succ");
536 assert_eq!(ss.current(), Some("succ"));
537 assert_eq!(ss.depth(), 2);
538 assert_eq!(ss.path(), "Nat.succ");
539 ss.pop();
540 assert_eq!(ss.current(), Some("Nat"));
541 }
542 #[test]
543 fn test_annotation_table() {
544 let mut tbl = AnnotationTable::new();
545 tbl.annotate("doc", "first line");
546 tbl.annotate("doc", "second line");
547 assert_eq!(tbl.get_all("doc").len(), 2);
548 assert!(tbl.has("doc"));
549 assert!(!tbl.has("other"));
550 }
551 #[test]
552 fn test_work_stack() {
553 let mut ws = WorkStack::new();
554 ws.push(1u32);
555 ws.push(2u32);
556 assert_eq!(ws.pop(), Some(2));
557 assert_eq!(ws.len(), 1);
558 }
559 #[test]
560 fn test_work_queue() {
561 let mut wq = WorkQueue::new();
562 wq.enqueue(1u32);
563 wq.enqueue(2u32);
564 assert_eq!(wq.dequeue(), Some(1));
565 assert_eq!(wq.len(), 1);
566 }
567 #[test]
568 fn test_sparse_bit_set() {
569 let mut bs = SparseBitSet::new(128);
570 bs.set(5);
571 bs.set(63);
572 bs.set(64);
573 assert!(bs.get(5));
574 assert!(bs.get(63));
575 assert!(bs.get(64));
576 assert!(!bs.get(0));
577 assert_eq!(bs.count_ones(), 3);
578 bs.clear(5);
579 assert!(!bs.get(5));
580 }
581 #[test]
582 fn test_loop_clock() {
583 let mut clk = LoopClock::start();
584 for _ in 0..10 {
585 clk.tick();
586 }
587 assert_eq!(clk.iters(), 10);
588 assert!(clk.elapsed_us() >= 0.0);
589 }
590}
591#[cfg(test)]
592mod tests_extra_data_structures {
593 use super::*;
594 #[test]
595 fn test_simple_lru_cache() {
596 let mut cache: SimpleLruCache<&str, u32> = SimpleLruCache::new(3);
597 cache.put("a", 1);
598 cache.put("b", 2);
599 cache.put("c", 3);
600 assert_eq!(cache.get(&"a"), Some(&1));
601 cache.put("d", 4);
602 assert!(cache.len() <= 3);
603 }
604 #[test]
605 fn test_string_interner() {
606 let mut si = StringInterner::new();
607 let id1 = si.intern("hello");
608 let id2 = si.intern("hello");
609 assert_eq!(id1, id2);
610 let id3 = si.intern("world");
611 assert_ne!(id1, id3);
612 assert_eq!(si.get(id1), Some("hello"));
613 assert_eq!(si.len(), 2);
614 }
615 #[test]
616 fn test_frequency_table() {
617 let mut ft = FrequencyTable::new();
618 ft.record("a");
619 ft.record("b");
620 ft.record("a");
621 ft.record("a");
622 assert_eq!(ft.freq(&"a"), 3);
623 assert_eq!(ft.freq(&"b"), 1);
624 assert_eq!(ft.most_frequent(), Some((&"a", 3)));
625 assert_eq!(ft.total(), 4);
626 assert_eq!(ft.distinct(), 2);
627 }
628 #[test]
629 fn test_bimap() {
630 let mut bm: BiMap<u32, &str> = BiMap::new();
631 bm.insert(1, "one");
632 bm.insert(2, "two");
633 assert_eq!(bm.get_b(&1), Some(&"one"));
634 assert_eq!(bm.get_a(&"two"), Some(&2));
635 assert_eq!(bm.len(), 2);
636 }
637}
638#[cfg(test)]
639mod tests_interval_set {
640 use super::*;
641 #[test]
642 fn test_interval_set() {
643 let mut s = IntervalSet::new();
644 s.add(1, 5);
645 s.add(3, 8);
646 assert_eq!(s.num_intervals(), 1);
647 assert_eq!(s.cardinality(), 8);
648 assert!(s.contains(4));
649 assert!(!s.contains(9));
650 s.add(10, 15);
651 assert_eq!(s.num_intervals(), 2);
652 }
653}
654#[allow(dead_code)]
656pub fn now_us() -> Timestamp {
657 let us = std::time::SystemTime::UNIX_EPOCH
658 .elapsed()
659 .map(|d| d.as_micros() as u64)
660 .unwrap_or(0);
661 Timestamp::from_us(us)
662}
663#[cfg(test)]
664mod tests_typed_utilities {
665 use super::*;
666 #[test]
667 fn test_timestamp() {
668 let t1 = Timestamp::from_us(1000);
669 let t2 = Timestamp::from_us(1500);
670 assert_eq!(t2.elapsed_since(t1), 500);
671 assert!(t1 < t2);
672 }
673 #[test]
674 fn test_typed_id() {
675 struct Foo;
676 let id: TypedId<Foo> = TypedId::new(42);
677 assert_eq!(id.raw(), 42);
678 assert_eq!(format!("{id}"), "#42");
679 }
680 #[test]
681 fn test_id_dispenser() {
682 struct Bar;
683 let mut disp: IdDispenser<Bar> = IdDispenser::new();
684 let a = disp.next();
685 let b = disp.next();
686 assert_eq!(a.raw(), 0);
687 assert_eq!(b.raw(), 1);
688 assert_eq!(disp.count(), 2);
689 }
690 #[test]
691 fn test_slot() {
692 let mut slot: Slot<u32> = Slot::empty();
693 assert!(!slot.is_filled());
694 slot.fill(99);
695 assert!(slot.is_filled());
696 assert_eq!(slot.get(), Some(&99));
697 let v = slot.take();
698 assert_eq!(v, Some(99));
699 assert!(!slot.is_filled());
700 }
701 #[test]
702 #[should_panic]
703 fn test_slot_double_fill() {
704 let mut slot: Slot<u32> = Slot::empty();
705 slot.fill(1);
706 slot.fill(2);
707 }
708 #[test]
709 fn test_memo_slot() {
710 let mut ms: MemoSlot<u32> = MemoSlot::new();
711 assert!(!ms.is_cached());
712 let val = ms.get_or_compute(|| 42);
713 assert_eq!(*val, 42);
714 assert!(ms.is_cached());
715 ms.invalidate();
716 assert!(!ms.is_cached());
717 }
718}
719#[cfg(test)]
720mod tests_ring_buffer {
721 use super::*;
722 #[test]
723 fn test_ring_buffer() {
724 let mut rb = RingBuffer::new(3);
725 rb.push(1u32);
726 rb.push(2u32);
727 rb.push(3u32);
728 assert!(rb.is_full());
729 rb.push(4u32);
730 assert_eq!(rb.pop(), Some(2));
731 assert_eq!(rb.len(), 2);
732 }
733 #[test]
734 fn test_before_after() {
735 let ba = BeforeAfter::new(10u32, 10u32);
736 assert!(ba.unchanged());
737 let ba2 = BeforeAfter::new(10u32, 20u32);
738 assert!(!ba2.unchanged());
739 }
740 #[test]
741 fn test_seq_num() {
742 let s = SeqNum::ZERO;
743 assert_eq!(s.value(), 0);
744 let s2 = s.next();
745 assert_eq!(s2.value(), 1);
746 assert!(s < s2);
747 }
748 #[test]
749 fn test_generation() {
750 let g0 = Generation::INITIAL;
751 let g1 = g0.advance();
752 assert_eq!(g0.number(), 0);
753 assert_eq!(g1.number(), 1);
754 assert_ne!(g0, g1);
755 }
756}