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