1use crate::{BinderInfo, Expr, FVarId, Name};
6use std::collections::HashMap;
7
8use super::types::{
9 ConfigNode, Context, ContextChain, ContextDiff, ContextEntry, ContextStats, DecisionNode,
10 Either2, FlatSubstitution, FocusStack, FreshNameSeq, HypContext, LabelSet, NameGenerator,
11 NonEmptyVec, PathBuf, RewriteRule, RewriteRuleSet, ScopedContext, SimpleDag, SlidingSum,
12 SmallMap, SparseVec, StackCalc, StatSummary, Stopwatch, StringPool, TokenBucket, TransformStat,
13 TransitiveClosure, VersionedRecord, WindowIterator, WriteOnce,
14};
15
16pub(super) fn abstract_fvar(expr: Expr, fvar: FVarId) -> Expr {
18 abstract_fvar_at(expr, fvar, 0)
19}
20pub(super) fn abstract_fvar_at(expr: Expr, fvar: FVarId, depth: u32) -> Expr {
22 match expr {
23 Expr::FVar(id) if id == fvar => Expr::BVar(depth),
24 Expr::App(f, a) => Expr::App(
25 Box::new(abstract_fvar_at(*f, fvar, depth)),
26 Box::new(abstract_fvar_at(*a, fvar, depth)),
27 ),
28 Expr::Lam(bi, n, ty, body) => Expr::Lam(
29 bi,
30 n,
31 Box::new(abstract_fvar_at(*ty, fvar, depth)),
32 Box::new(abstract_fvar_at(*body, fvar, depth + 1)),
33 ),
34 Expr::Pi(bi, n, ty, body) => Expr::Pi(
35 bi,
36 n,
37 Box::new(abstract_fvar_at(*ty, fvar, depth)),
38 Box::new(abstract_fvar_at(*body, fvar, depth + 1)),
39 ),
40 Expr::Let(n, ty, val, body) => Expr::Let(
41 n,
42 Box::new(abstract_fvar_at(*ty, fvar, depth)),
43 Box::new(abstract_fvar_at(*val, fvar, depth)),
44 Box::new(abstract_fvar_at(*body, fvar, depth + 1)),
45 ),
46 _ => expr,
47 }
48}
49pub(super) fn abstract_fvars_in_type(ty: Expr, fvars: &[FVarId], current_fvar: FVarId) -> Expr {
59 let current_idx = match fvars.iter().position(|&f| f == current_fvar) {
60 Some(idx) => idx,
61 None => return ty,
62 };
63 if current_idx == 0 {
64 return ty;
65 }
66 let mut result = ty;
67 for (i, &fvar) in fvars[..current_idx].iter().enumerate() {
68 let depth = (current_idx - 1 - i) as u32;
69 result = abstract_fvar_at(result, fvar, depth);
70 }
71 result
72}
73#[cfg(test)]
74mod tests {
75 use super::*;
76 use crate::{Level, Literal};
77 #[test]
78 fn test_context_create() {
79 let ctx = Context::new();
80 assert_eq!(ctx.num_locals(), 0);
81 assert!(ctx.is_empty());
82 }
83 #[test]
84 fn test_push_local() {
85 let mut ctx = Context::new();
86 let ty = Expr::Sort(Level::zero());
87 let fvar = ctx.push_local(Name::str("x"), ty, None);
88 assert_eq!(ctx.num_locals(), 1);
89 assert!(!ctx.is_empty());
90 let local = ctx.get_local(fvar).expect("local should be present");
91 assert_eq!(local.name, Name::str("x"));
92 }
93 #[test]
94 fn test_pop_local() {
95 let mut ctx = Context::new();
96 let ty = Expr::Sort(Level::zero());
97 ctx.push_local(Name::str("x"), ty.clone(), None);
98 ctx.push_local(Name::str("y"), ty, None);
99 assert_eq!(ctx.num_locals(), 2);
100 let popped = ctx.pop_local().expect("popped should be present");
101 assert_eq!(popped.name, Name::str("y"));
102 assert_eq!(ctx.num_locals(), 1);
103 }
104 #[test]
105 fn test_find_local() {
106 let mut ctx = Context::new();
107 let ty = Expr::Sort(Level::zero());
108 ctx.push_local(Name::str("x"), ty.clone(), None);
109 ctx.push_local(Name::str("y"), ty, None);
110 let local = ctx
111 .find_local(&Name::str("x"))
112 .expect("local should be present");
113 assert_eq!(local.name, Name::str("x"));
114 }
115 #[test]
116 fn test_find_local_not_found() {
117 let ctx = Context::new();
118 assert!(ctx.find_local(&Name::str("z")).is_none());
119 }
120 #[test]
121 fn test_local_with_value() {
122 let mut ctx = Context::new();
123 let ty = Expr::Sort(Level::zero());
124 let val = Expr::Lit(Literal::Nat(42));
125 let fvar = ctx.push_local(Name::str("x"), ty, Some(val.clone()));
126 let local = ctx.get_local(fvar).expect("local should be present");
127 assert!(local.val.is_some());
128 assert_eq!(local.val.as_ref().expect("as_ref should succeed"), &val);
129 }
130 #[test]
131 fn test_clear() {
132 let mut ctx = Context::new();
133 let ty = Expr::Sort(Level::zero());
134 ctx.push_local(Name::str("x"), ty, None);
135 ctx.clear();
136 assert_eq!(ctx.num_locals(), 0);
137 assert!(ctx.is_empty());
138 }
139 #[test]
140 fn test_mk_local_decl() {
141 let mut ctx = Context::new();
142 let ty = Expr::Sort(Level::zero());
143 let fvar_expr = ctx.mk_local_decl(Name::str("x"), BinderInfo::Default, ty);
144 assert!(matches!(fvar_expr, Expr::FVar(_)));
145 assert_eq!(ctx.num_locals(), 1);
146 }
147 #[test]
148 fn test_mk_let_decl() {
149 let mut ctx = Context::new();
150 let ty = Expr::Sort(Level::zero());
151 let val = Expr::Lit(Literal::Nat(42));
152 let fvar_expr = ctx.mk_let_decl(Name::str("x"), ty, val);
153 if let Expr::FVar(id) = fvar_expr {
154 assert!(ctx.is_let(id));
155 } else {
156 panic!("Expected FVar");
157 }
158 }
159 #[test]
160 fn test_save_restore() {
161 let mut ctx = Context::new();
162 let ty = Expr::Sort(Level::zero());
163 ctx.push_local(Name::str("x"), ty.clone(), None);
164 let snap = ctx.save();
165 ctx.push_local(Name::str("y"), ty.clone(), None);
166 ctx.push_local(Name::str("z"), ty, None);
167 assert_eq!(ctx.num_locals(), 3);
168 ctx.restore(&snap);
169 assert_eq!(ctx.num_locals(), 1);
170 }
171 #[test]
172 fn test_get_fvars() {
173 let mut ctx = Context::new();
174 let ty = Expr::Sort(Level::zero());
175 ctx.push_local(Name::str("x"), ty.clone(), None);
176 ctx.push_local(Name::str("y"), ty, None);
177 let fvars = ctx.get_fvars();
178 assert_eq!(fvars.len(), 2);
179 }
180 #[test]
181 fn test_name_generator() {
182 let mut gen = NameGenerator::new("x");
183 let n1 = gen.next();
184 let n2 = gen.next();
185 assert_ne!(n1, n2);
186 assert_eq!(n1, Name::str("x_0"));
187 assert_eq!(n2, Name::str("x_1"));
188 }
189 #[test]
190 fn test_with_local() {
191 let mut ctx = Context::new();
192 let ty = Expr::Sort(Level::zero());
193 let fvar_inside = ctx.with_local(Name::str("temp"), ty, |ctx, fvar| {
194 assert_eq!(ctx.num_locals(), 1);
195 assert!(ctx.get_local(fvar).is_some());
196 fvar
197 });
198 assert_eq!(ctx.num_locals(), 0);
199 assert!(ctx.get_local(fvar_inside).is_none());
200 }
201 #[test]
202 fn test_binder_info_preserved() {
203 let mut ctx = Context::new();
204 let ty = Expr::Sort(Level::zero());
205 let fvar = ctx.push_local_with_binder(Name::str("x"), BinderInfo::Implicit, ty, None);
206 let local = ctx.get_local(fvar).expect("local should be present");
207 assert_eq!(local.binder_info, BinderInfo::Implicit);
208 }
209 #[test]
210 fn test_abstract_fvar() {
211 let fvar_id = FVarId(42);
212 let expr = Expr::App(
213 Box::new(Expr::Const(Name::str("f"), vec![])),
214 Box::new(Expr::FVar(fvar_id)),
215 );
216 let abstracted = abstract_fvar(expr, fvar_id);
217 let expected = Expr::App(
218 Box::new(Expr::Const(Name::str("f"), vec![])),
219 Box::new(Expr::BVar(0)),
220 );
221 assert_eq!(abstracted, expected);
222 }
223}
224#[allow(dead_code)]
226pub mod name_gen {
227 use super::Name;
228 pub fn fresh(base: &str, counter: u64) -> Name {
230 Name::str(format!("{}_{}", base, counter))
231 }
232 pub fn greek(idx: usize) -> Name {
234 const GREEK: &[&str] = &[
235 "alpha", "beta", "gamma", "delta", "epsilon", "zeta", "eta", "theta", "iota", "kappa",
236 "lambda", "mu", "nu", "xi", "pi", "rho", "sigma", "tau", "upsilon", "phi", "chi",
237 "psi", "omega",
238 ];
239 if idx < GREEK.len() {
240 Name::str(GREEK[idx])
241 } else {
242 Name::str(format!("alpha{}", idx))
243 }
244 }
245 pub fn mvar(idx: u64) -> Name {
247 Name::str(format!("?m{}", idx))
248 }
249 pub fn hyp(idx: usize) -> Name {
251 Name::str(format!("h{}", idx))
252 }
253}
254#[cfg(test)]
255mod extended_ctx_tests {
256 use super::*;
257 use crate::{Level, Literal};
258 #[test]
259 fn test_context_entry_local() {
260 let e = ContextEntry::local(Name::str("x"), Expr::Sort(Level::zero()));
261 assert!(!e.is_let());
262 assert!(!e.is_implicit());
263 }
264 #[test]
265 fn test_context_entry_implicit() {
266 let e = ContextEntry::implicit(Name::str("alpha"), Expr::Sort(Level::zero()));
267 assert!(e.is_implicit());
268 assert!(!e.is_let());
269 }
270 #[test]
271 fn test_context_entry_let() {
272 let e = ContextEntry::let_binding(
273 Name::str("x"),
274 Expr::Sort(Level::zero()),
275 Expr::Lit(Literal::Nat(1)),
276 );
277 assert!(e.is_let());
278 }
279 #[test]
280 fn test_context_chain_empty() {
281 let chain = ContextChain::new();
282 assert!(chain.is_empty());
283 assert_eq!(chain.len(), 0);
284 }
285 #[test]
286 fn test_context_chain_push_pop() {
287 let mut chain = ContextChain::new();
288 chain.push(ContextEntry::local(
289 Name::str("x"),
290 Expr::Sort(Level::zero()),
291 ));
292 chain.push(ContextEntry::implicit(
293 Name::str("y"),
294 Expr::Sort(Level::zero()),
295 ));
296 assert_eq!(chain.len(), 2);
297 assert_eq!(chain.num_implicit(), 1);
298 assert_eq!(chain.num_lets(), 0);
299 let popped = chain.pop().expect("collection should not be empty");
300 assert_eq!(popped.name, Name::str("y"));
301 }
302 #[test]
303 fn test_context_chain_find() {
304 let mut chain = ContextChain::new();
305 chain.push(ContextEntry::local(
306 Name::str("a"),
307 Expr::Sort(Level::zero()),
308 ));
309 chain.push(ContextEntry::local(
310 Name::str("b"),
311 Expr::Sort(Level::zero()),
312 ));
313 assert!(chain.find(&Name::str("a")).is_some());
314 assert!(chain.find(&Name::str("c")).is_none());
315 }
316 #[test]
317 fn test_context_chain_from_context() {
318 let mut ctx = Context::new();
319 ctx.push_local(Name::str("x"), Expr::Sort(Level::zero()), None);
320 ctx.push_local(
321 Name::str("y"),
322 Expr::Sort(Level::zero()),
323 Some(Expr::Lit(Literal::Nat(0))),
324 );
325 let chain = ContextChain::from_context(&ctx);
326 assert_eq!(chain.len(), 2);
327 assert_eq!(chain.num_lets(), 1);
328 }
329 #[test]
330 fn test_context_stats() {
331 let mut ctx = Context::new();
332 ctx.push_local(Name::str("x"), Expr::Sort(Level::zero()), None);
333 ctx.push_local_with_binder(
334 Name::str("y"),
335 BinderInfo::Implicit,
336 Expr::Sort(Level::zero()),
337 None,
338 );
339 let stats = ContextStats::from_context(&ctx);
340 assert_eq!(stats.num_locals, 2);
341 assert_eq!(stats.num_implicit, 1);
342 assert_eq!(stats.num_lets, 0);
343 }
344 #[test]
345 fn test_context_diff_compute() {
346 let mut old_ctx = Context::new();
347 old_ctx.push_local(Name::str("x"), Expr::Sort(Level::zero()), None);
348 let mut new_ctx = Context::new();
349 new_ctx.push_local(Name::str("x"), Expr::Sort(Level::zero()), None);
350 new_ctx.push_local(Name::str("y"), Expr::Sort(Level::zero()), None);
351 let diff = ContextDiff::compute(&old_ctx, &new_ctx);
352 assert!(diff.added.contains(&Name::str("y")));
353 assert!(diff.removed.is_empty());
354 assert!(!diff.is_empty());
355 }
356 #[test]
357 fn test_context_diff_empty() {
358 let ctx = Context::new();
359 let diff = ContextDiff::compute(&ctx, &ctx);
360 assert!(diff.is_empty());
361 }
362 #[test]
363 fn test_name_gen_fresh() {
364 let n = name_gen::fresh("x", 5);
365 assert_eq!(n, Name::str("x_5"));
366 }
367 #[test]
368 fn test_name_gen_greek() {
369 let alpha = name_gen::greek(0);
370 let beta = name_gen::greek(1);
371 assert_ne!(alpha, beta);
372 let overflow = name_gen::greek(100);
373 assert_eq!(overflow, Name::str("alpha100"));
374 }
375 #[test]
376 fn test_name_gen_mvar() {
377 let m = name_gen::mvar(3);
378 assert_eq!(m, Name::str("?m3"));
379 }
380 #[test]
381 fn test_name_gen_hyp() {
382 let h = name_gen::hyp(0);
383 assert_eq!(h, Name::str("h0"));
384 }
385 #[test]
386 fn test_context_with_local_cleanup() {
387 let mut ctx = Context::new();
388 let ty = Expr::Sort(Level::zero());
389 let saw_local = ctx.with_local(Name::str("temp"), ty, |ctx, _fvar| {
390 assert_eq!(ctx.num_locals(), 1);
391 true
392 });
393 assert!(saw_local);
394 assert_eq!(ctx.num_locals(), 0);
395 }
396 #[test]
397 fn test_context_mk_lambda() {
398 let mut ctx = Context::new();
399 let ty = Expr::Sort(Level::zero());
400 let fvar = ctx.push_local(Name::str("x"), ty, None);
401 let body = Expr::FVar(fvar);
402 let lam = ctx.mk_lambda(&[fvar], body);
403 assert!(matches!(lam, Expr::Lam(_, _, _, _)));
404 }
405 #[test]
406 fn test_context_mk_pi() {
407 let mut ctx = Context::new();
408 let ty = Expr::Sort(Level::zero());
409 let fvar = ctx.push_local(Name::str("x"), ty, None);
410 let body = Expr::FVar(fvar);
411 let pi = ctx.mk_pi(&[fvar], body);
412 assert!(matches!(pi, Expr::Pi(_, _, _, _)));
413 }
414}
415#[allow(dead_code)]
419pub fn rename_fvar(expr: Expr, old: FVarId, new: FVarId) -> Expr {
420 match expr {
421 Expr::FVar(id) if id == old => Expr::FVar(new),
422 Expr::App(f, a) => Expr::App(
423 Box::new(rename_fvar(*f, old, new)),
424 Box::new(rename_fvar(*a, old, new)),
425 ),
426 Expr::Lam(bi, n, ty, body) => Expr::Lam(
427 bi,
428 n,
429 Box::new(rename_fvar(*ty, old, new)),
430 Box::new(rename_fvar(*body, old, new)),
431 ),
432 Expr::Pi(bi, n, ty, body) => Expr::Pi(
433 bi,
434 n,
435 Box::new(rename_fvar(*ty, old, new)),
436 Box::new(rename_fvar(*body, old, new)),
437 ),
438 Expr::Let(n, ty, val, body) => Expr::Let(
439 n,
440 Box::new(rename_fvar(*ty, old, new)),
441 Box::new(rename_fvar(*val, old, new)),
442 Box::new(rename_fvar(*body, old, new)),
443 ),
444 other => other,
445 }
446}
447#[allow(dead_code)]
449pub fn collect_fvars(expr: &Expr) -> Vec<FVarId> {
450 let mut result = Vec::new();
451 collect_fvars_helper(expr, &mut result);
452 result
453}
454pub(super) fn collect_fvars_helper(expr: &Expr, acc: &mut Vec<FVarId>) {
455 match expr {
456 Expr::FVar(id) => {
457 if !acc.contains(id) {
458 acc.push(*id);
459 }
460 }
461 Expr::App(f, a) => {
462 collect_fvars_helper(f, acc);
463 collect_fvars_helper(a, acc);
464 }
465 Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
466 collect_fvars_helper(ty, acc);
467 collect_fvars_helper(body, acc);
468 }
469 Expr::Let(_, ty, val, body) => {
470 collect_fvars_helper(ty, acc);
471 collect_fvars_helper(val, acc);
472 collect_fvars_helper(body, acc);
473 }
474 _ => {}
475 }
476}
477#[allow(dead_code)]
479pub fn count_fvar(expr: &Expr, fvar: FVarId) -> usize {
480 match expr {
481 Expr::FVar(id) => {
482 if *id == fvar {
483 1
484 } else {
485 0
486 }
487 }
488 Expr::App(f, a) => count_fvar(f, fvar) + count_fvar(a, fvar),
489 Expr::Lam(_, _, ty, body) | Expr::Pi(_, _, ty, body) => {
490 count_fvar(ty, fvar) + count_fvar(body, fvar)
491 }
492 Expr::Let(_, ty, val, body) => {
493 count_fvar(ty, fvar) + count_fvar(val, fvar) + count_fvar(body, fvar)
494 }
495 _ => 0,
496 }
497}
498#[allow(dead_code)]
500pub fn fvar_occurs(expr: &Expr, fvar: FVarId) -> bool {
501 count_fvar(expr, fvar) > 0
502}
503#[cfg(test)]
504mod scoped_ctx_tests {
505 use super::*;
506 use crate::Level;
507 #[test]
508 fn test_rename_fvar() {
509 let old = FVarId(0);
510 let new = FVarId(1);
511 let expr = Expr::App(
512 Box::new(Expr::Const(Name::str("f"), vec![])),
513 Box::new(Expr::FVar(old)),
514 );
515 let renamed = rename_fvar(expr, old, new);
516 if let Expr::App(_, a) = renamed {
517 assert_eq!(*a, Expr::FVar(new));
518 } else {
519 panic!("expected App");
520 }
521 }
522 #[test]
523 fn test_collect_fvars() {
524 let e1 = Expr::FVar(FVarId(0));
525 let e2 = Expr::FVar(FVarId(1));
526 let expr = Expr::App(Box::new(e1), Box::new(e2));
527 let fvars = collect_fvars(&expr);
528 assert_eq!(fvars.len(), 2);
529 }
530 #[test]
531 fn test_collect_fvars_dedup() {
532 let fv = FVarId(5);
533 let expr = Expr::App(Box::new(Expr::FVar(fv)), Box::new(Expr::FVar(fv)));
534 let fvars = collect_fvars(&expr);
535 assert_eq!(fvars.len(), 1);
536 }
537 #[test]
538 fn test_count_fvar() {
539 let fv = FVarId(3);
540 let expr = Expr::App(Box::new(Expr::FVar(fv)), Box::new(Expr::FVar(fv)));
541 assert_eq!(count_fvar(&expr, fv), 2);
542 assert_eq!(count_fvar(&expr, FVarId(99)), 0);
543 }
544 #[test]
545 fn test_fvar_occurs() {
546 let fv = FVarId(7);
547 let expr = Expr::FVar(fv);
548 assert!(fvar_occurs(&expr, fv));
549 assert!(!fvar_occurs(&expr, FVarId(8)));
550 }
551 #[test]
552 fn test_scoped_context_push_pop() {
553 let mut ctx = ScopedContext::new();
554 ctx.push_scope();
555 ctx.add_local(Name::str("x"), Expr::Sort(Level::zero()));
556 assert_eq!(ctx.num_locals(), 1);
557 ctx.pop_scope();
558 assert_eq!(ctx.num_locals(), 0);
559 }
560 #[test]
561 fn test_scoped_context_depth() {
562 let mut ctx = ScopedContext::new();
563 assert_eq!(ctx.scope_depth(), 0);
564 ctx.push_scope();
565 assert_eq!(ctx.scope_depth(), 1);
566 ctx.push_scope();
567 assert_eq!(ctx.scope_depth(), 2);
568 ctx.pop_scope();
569 assert_eq!(ctx.scope_depth(), 1);
570 }
571 #[test]
572 fn test_hyp_context_add_find() {
573 let mut ctx = HypContext::new();
574 let ty = Expr::Sort(Level::zero());
575 let fvar = ctx.add_hyp(Name::str("h"), ty);
576 let found = ctx.find_hyp(&Name::str("h"));
577 assert_eq!(found, Some(fvar));
578 assert_eq!(ctx.num_hyps(), 1);
579 }
580 #[test]
581 fn test_hyp_context_not_found() {
582 let ctx = HypContext::new();
583 assert!(ctx.find_hyp(&Name::str("missing")).is_none());
584 }
585 #[test]
586 fn test_hyp_context_hyp_type() {
587 let mut ctx = HypContext::new();
588 let ty = Expr::Sort(Level::zero());
589 let fvar = ctx.add_hyp(Name::str("h"), ty.clone());
590 assert_eq!(ctx.hyp_type(fvar), Some(&ty));
591 }
592 #[test]
593 fn test_hyp_context_remove_last() {
594 let mut ctx = HypContext::new();
595 let ty = Expr::Sort(Level::zero());
596 ctx.add_hyp(Name::str("h1"), ty.clone());
597 ctx.add_hyp(Name::str("h2"), ty);
598 ctx.remove_last_hyp();
599 assert_eq!(ctx.num_hyps(), 1);
600 assert!(ctx.find_hyp(&Name::str("h2")).is_none());
601 }
602 #[test]
603 fn test_fresh_name_seq() {
604 let mut seq = FreshNameSeq::new("x");
605 let n1 = seq.next();
606 let n2 = seq.next();
607 assert_ne!(n1, n2);
608 assert_eq!(seq.count(), 2);
609 }
610 #[test]
611 fn test_fresh_name_seq_reserve() {
612 let mut seq = FreshNameSeq::new("h");
613 seq.reserve("h");
614 let n = seq.next();
615 assert_ne!(n, Name::str("h"));
616 }
617}
618#[cfg(test)]
619mod tests_padding_infra {
620 use super::*;
621 #[test]
622 fn test_stat_summary() {
623 let mut ss = StatSummary::new();
624 ss.record(10.0);
625 ss.record(20.0);
626 ss.record(30.0);
627 assert_eq!(ss.count(), 3);
628 assert!((ss.mean().expect("mean should succeed") - 20.0).abs() < 1e-9);
629 assert_eq!(ss.min().expect("min should succeed") as i64, 10);
630 assert_eq!(ss.max().expect("max should succeed") as i64, 30);
631 }
632 #[test]
633 fn test_transform_stat() {
634 let mut ts = TransformStat::new();
635 ts.record_before(100.0);
636 ts.record_after(80.0);
637 let ratio = ts.mean_ratio().expect("ratio should be present");
638 assert!((ratio - 0.8).abs() < 1e-9);
639 }
640 #[test]
641 fn test_small_map() {
642 let mut m: SmallMap<u32, &str> = SmallMap::new();
643 m.insert(3, "three");
644 m.insert(1, "one");
645 m.insert(2, "two");
646 assert_eq!(m.get(&2), Some(&"two"));
647 assert_eq!(m.len(), 3);
648 let keys = m.keys();
649 assert_eq!(*keys[0], 1);
650 assert_eq!(*keys[2], 3);
651 }
652 #[test]
653 fn test_label_set() {
654 let mut ls = LabelSet::new();
655 ls.add("foo");
656 ls.add("bar");
657 ls.add("foo");
658 assert_eq!(ls.count(), 2);
659 assert!(ls.has("bar"));
660 assert!(!ls.has("baz"));
661 }
662 #[test]
663 fn test_config_node() {
664 let mut root = ConfigNode::section("root");
665 let child = ConfigNode::leaf("key", "value");
666 root.add_child(child);
667 assert_eq!(root.num_children(), 1);
668 }
669 #[test]
670 fn test_versioned_record() {
671 let mut vr = VersionedRecord::new(0u32);
672 vr.update(1);
673 vr.update(2);
674 assert_eq!(*vr.current(), 2);
675 assert_eq!(vr.version(), 2);
676 assert!(vr.has_history());
677 assert_eq!(*vr.at_version(0).expect("value should be present"), 0);
678 }
679 #[test]
680 fn test_simple_dag() {
681 let mut dag = SimpleDag::new(4);
682 dag.add_edge(0, 1);
683 dag.add_edge(1, 2);
684 dag.add_edge(2, 3);
685 assert!(dag.can_reach(0, 3));
686 assert!(!dag.can_reach(3, 0));
687 let order = dag.topological_sort().expect("order should be present");
688 assert_eq!(order, vec![0, 1, 2, 3]);
689 }
690 #[test]
691 fn test_focus_stack() {
692 let mut fs: FocusStack<&str> = FocusStack::new();
693 fs.focus("a");
694 fs.focus("b");
695 assert_eq!(fs.current(), Some(&"b"));
696 assert_eq!(fs.depth(), 2);
697 fs.blur();
698 assert_eq!(fs.current(), Some(&"a"));
699 }
700}
701#[cfg(test)]
702mod tests_extra_iterators {
703 use super::*;
704 #[test]
705 fn test_window_iterator() {
706 let data = vec![1u32, 2, 3, 4, 5];
707 let windows: Vec<_> = WindowIterator::new(&data, 3).collect();
708 assert_eq!(windows.len(), 3);
709 assert_eq!(windows[0], &[1, 2, 3]);
710 assert_eq!(windows[2], &[3, 4, 5]);
711 }
712 #[test]
713 fn test_non_empty_vec() {
714 let mut nev = NonEmptyVec::singleton(10u32);
715 nev.push(20);
716 nev.push(30);
717 assert_eq!(nev.len(), 3);
718 assert_eq!(*nev.first(), 10);
719 assert_eq!(*nev.last(), 30);
720 }
721}
722#[cfg(test)]
723mod tests_padding2 {
724 use super::*;
725 #[test]
726 fn test_sliding_sum() {
727 let mut ss = SlidingSum::new(3);
728 ss.push(1.0);
729 ss.push(2.0);
730 ss.push(3.0);
731 assert!((ss.sum() - 6.0).abs() < 1e-9);
732 ss.push(4.0);
733 assert!((ss.sum() - 9.0).abs() < 1e-9);
734 assert_eq!(ss.count(), 3);
735 }
736 #[test]
737 fn test_path_buf() {
738 let mut pb = PathBuf::new();
739 pb.push("src");
740 pb.push("main");
741 assert_eq!(pb.as_str(), "src/main");
742 assert_eq!(pb.depth(), 2);
743 pb.pop();
744 assert_eq!(pb.as_str(), "src");
745 }
746 #[test]
747 fn test_string_pool() {
748 let mut pool = StringPool::new();
749 let s = pool.take();
750 assert!(s.is_empty());
751 pool.give("hello".to_string());
752 let s2 = pool.take();
753 assert!(s2.is_empty());
754 assert_eq!(pool.free_count(), 0);
755 }
756 #[test]
757 fn test_transitive_closure() {
758 let mut tc = TransitiveClosure::new(4);
759 tc.add_edge(0, 1);
760 tc.add_edge(1, 2);
761 tc.add_edge(2, 3);
762 assert!(tc.can_reach(0, 3));
763 assert!(!tc.can_reach(3, 0));
764 let r = tc.reachable_from(0);
765 assert_eq!(r.len(), 4);
766 }
767 #[test]
768 fn test_token_bucket() {
769 let mut tb = TokenBucket::new(100, 10);
770 assert_eq!(tb.available(), 100);
771 assert!(tb.try_consume(50));
772 assert_eq!(tb.available(), 50);
773 assert!(!tb.try_consume(60));
774 assert_eq!(tb.capacity(), 100);
775 }
776 #[test]
777 fn test_rewrite_rule_set() {
778 let mut rrs = RewriteRuleSet::new();
779 rrs.add(RewriteRule::unconditional(
780 "beta",
781 "App(Lam(x, b), v)",
782 "b[x:=v]",
783 ));
784 rrs.add(RewriteRule::conditional("comm", "a + b", "b + a"));
785 assert_eq!(rrs.len(), 2);
786 assert_eq!(rrs.unconditional_rules().len(), 1);
787 assert_eq!(rrs.conditional_rules().len(), 1);
788 assert!(rrs.get("beta").is_some());
789 let disp = rrs
790 .get("beta")
791 .expect("element at \'beta\' should exist")
792 .display();
793 assert!(disp.contains("→"));
794 }
795}
796#[cfg(test)]
797mod tests_padding3 {
798 use super::*;
799 #[test]
800 fn test_decision_node() {
801 let tree = DecisionNode::Branch {
802 key: "x".into(),
803 val: "1".into(),
804 yes_branch: Box::new(DecisionNode::Leaf("yes".into())),
805 no_branch: Box::new(DecisionNode::Leaf("no".into())),
806 };
807 let mut ctx = std::collections::HashMap::new();
808 ctx.insert("x".into(), "1".into());
809 assert_eq!(tree.evaluate(&ctx), "yes");
810 ctx.insert("x".into(), "2".into());
811 assert_eq!(tree.evaluate(&ctx), "no");
812 assert_eq!(tree.depth(), 1);
813 }
814 #[test]
815 fn test_flat_substitution() {
816 let mut sub = FlatSubstitution::new();
817 sub.add("foo", "bar");
818 sub.add("baz", "qux");
819 assert_eq!(sub.apply("foo and baz"), "bar and qux");
820 assert_eq!(sub.len(), 2);
821 }
822 #[test]
823 fn test_stopwatch() {
824 let mut sw = Stopwatch::start();
825 sw.split();
826 sw.split();
827 assert_eq!(sw.num_splits(), 2);
828 assert!(sw.elapsed_ms() >= 0.0);
829 for &s in sw.splits() {
830 assert!(s >= 0.0);
831 }
832 }
833 #[test]
834 fn test_either2() {
835 let e: Either2<i32, &str> = Either2::First(42);
836 assert!(e.is_first());
837 let mapped = e.map_first(|x| x * 2);
838 assert_eq!(mapped.first(), Some(84));
839 let e2: Either2<i32, &str> = Either2::Second("hello");
840 assert!(e2.is_second());
841 assert_eq!(e2.second(), Some("hello"));
842 }
843 #[test]
844 fn test_write_once() {
845 let wo: WriteOnce<u32> = WriteOnce::new();
846 assert!(!wo.is_written());
847 assert!(wo.write(42));
848 assert!(!wo.write(99));
849 assert_eq!(wo.read(), Some(42));
850 }
851 #[test]
852 fn test_sparse_vec() {
853 let mut sv: SparseVec<i32> = SparseVec::new(100);
854 sv.set(5, 10);
855 sv.set(50, 20);
856 assert_eq!(*sv.get(5), 10);
857 assert_eq!(*sv.get(50), 20);
858 assert_eq!(*sv.get(0), 0);
859 assert_eq!(sv.nnz(), 2);
860 sv.set(5, 0);
861 assert_eq!(sv.nnz(), 1);
862 }
863 #[test]
864 fn test_stack_calc() {
865 let mut calc = StackCalc::new();
866 calc.push(3);
867 calc.push(4);
868 calc.add();
869 assert_eq!(calc.peek(), Some(7));
870 calc.push(2);
871 calc.mul();
872 assert_eq!(calc.peek(), Some(14));
873 }
874}