1use crate::{Expr, Level, Name};
6
7use super::types::{
8 AnnotatedError, ConfigNode, DecisionNode, Diagnostic, DiagnosticCollection, Either2,
9 ErrorAccumulator, ErrorCategory, ErrorContext, ErrorNote, ErrorReport, Fixture,
10 FlatSubstitution, FocusStack, KernelError, KernelPhase, LabelSet, MinHeap, NonEmptyVec,
11 PathBuf, PhasedError, PrefixCounter, RewriteRule, RewriteRuleSet, Severity, SimpleDag,
12 SlidingSum, SmallMap, SparseVec, StackCalc, StatSummary, Stopwatch, StringPool, TokenBucket,
13 TransformStat, TransitiveClosure, VersionedRecord, WindowIterator, WriteOnce,
14};
15
16pub type KernelResult<T> = Result<T, KernelError>;
18pub fn format_error_panel(err: &KernelError, width: usize) -> String {
20 let separator = "-".repeat(width);
21 let mut lines = vec![
22 separator.clone(),
23 format!(" Error [{:?}]", err.category()),
24 format!(" {}", err.short_description()),
25 ];
26 match err {
27 KernelError::TypeMismatch {
28 expected,
29 got,
30 context,
31 } => {
32 lines.push(format!(" Context : {}", context));
33 lines.push(format!(" Expected : {}", expected));
34 lines.push(format!(" Got : {}", got));
35 }
36 KernelError::UniverseInconsistency { lhs, rhs } => {
37 lines.push(format!(" LHS : {}", lhs));
38 lines.push(format!(" RHS : {}", rhs));
39 }
40 _ => {}
41 }
42 lines.push(separator);
43 lines.join("\n")
44}
45pub fn summarise_error(err: &KernelError, max_len: usize) -> String {
47 let full = err.to_string();
48 if full.len() <= max_len {
49 full
50 } else {
51 format!("{}...", &full[..max_len.saturating_sub(3)])
52 }
53}
54pub fn collect_unknown_constants(errors: &[KernelError]) -> Vec<&Name> {
56 let mut out = vec![];
57 for err in errors {
58 if let KernelError::UnknownConstant(name) = err {
59 if !out.contains(&name) {
60 out.push(name);
61 }
62 }
63 }
64 out
65}
66pub fn has_universe_errors(errors: &[KernelError]) -> bool {
68 errors
69 .iter()
70 .any(|e| matches!(e, KernelError::UniverseInconsistency { .. }))
71}
72#[allow(clippy::result_large_err)]
74pub trait KernelResultExt<T> {
75 fn context(self, ctx: impl Into<String>) -> Result<T, KernelError>;
77}
78impl<T> KernelResultExt<T> for Result<T, KernelError> {
79 fn context(self, ctx: impl Into<String>) -> Result<T, KernelError> {
80 self.map_err(|e| e.with_context(ctx))
81 }
82}
83#[allow(clippy::result_large_err)]
85pub fn try_kernel<T, E: std::error::Error>(f: impl FnOnce() -> Result<T, E>) -> KernelResult<T> {
86 f().map_err(|e| KernelError::Other(e.to_string()))
87}
88#[cfg(test)]
89mod tests {
90 use super::*;
91 fn mk_sort() -> Expr {
92 Expr::Sort(Level::zero())
93 }
94 #[test]
95 fn test_type_mismatch_display() {
96 let err = KernelError::TypeMismatch {
97 expected: mk_sort(),
98 got: mk_sort(),
99 context: "test".to_string(),
100 };
101 let s = err.to_string();
102 assert!(s.contains("type mismatch"));
103 assert!(s.contains("test"));
104 }
105 #[test]
106 fn test_unbound_variable_display() {
107 let err = KernelError::UnboundVariable(7);
108 assert_eq!(err.to_string(), "unbound variable: #7");
109 }
110 #[test]
111 fn test_unknown_constant_display() {
112 let name = Name::str("Nat");
113 let err = KernelError::UnknownConstant(name);
114 assert!(err.to_string().contains("Nat"));
115 }
116 #[test]
117 fn test_category_assignment() {
118 assert_eq!(
119 KernelError::UnboundVariable(0).category(),
120 ErrorCategory::Binding
121 );
122 assert_eq!(
123 KernelError::UnknownConstant(Name::str("X")).category(),
124 ErrorCategory::Resolution
125 );
126 assert_eq!(
127 KernelError::Other("x".to_string()).category(),
128 ErrorCategory::Other
129 );
130 }
131 #[test]
132 fn test_recoverability() {
133 assert!(KernelError::UnknownConstant(Name::str("X")).is_recoverable());
134 assert!(KernelError::Other("x".to_string()).is_recoverable());
135 assert!(KernelError::UnboundVariable(0).is_fatal());
136 }
137 #[test]
138 fn test_error_accumulator_basic() {
139 let mut acc = ErrorAccumulator::new();
140 assert!(acc.is_empty());
141 acc.push(KernelError::UnboundVariable(1));
142 acc.push(KernelError::Other("oops".to_string()));
143 assert_eq!(acc.len(), 2);
144 }
145 #[test]
146 fn test_error_accumulator_into_result() {
147 let mut acc = ErrorAccumulator::new();
148 acc.push(KernelError::UnboundVariable(0));
149 assert!(acc.into_result().is_err());
150 assert!(ErrorAccumulator::new().into_result().is_ok());
151 }
152 #[test]
153 fn test_error_accumulator_drain() {
154 let mut acc = ErrorAccumulator::new();
155 acc.push(KernelError::UnboundVariable(0));
156 acc.push(KernelError::UnboundVariable(1));
157 let drained = acc.drain();
158 assert_eq!(drained.len(), 2);
159 assert!(acc.is_empty());
160 }
161 #[test]
162 fn test_error_report_display() {
163 let err = KernelError::Other("bad".to_string());
164 let report = ErrorReport::new(err)
165 .with_location(Name::str("myTheorem"))
166 .add_note("try again");
167 let s = report.to_string();
168 assert!(s.contains("myTheorem"));
169 assert!(s.contains("bad"));
170 assert!(s.contains("try again"));
171 }
172 #[test]
173 fn test_diagnostic_collection_has_errors() {
174 let mut coll = DiagnosticCollection::new();
175 assert!(!coll.has_errors());
176 coll.add(Diagnostic::warning("some warning"));
177 assert!(!coll.has_errors());
178 coll.add(Diagnostic::error("some error"));
179 assert!(coll.has_errors());
180 }
181 #[test]
182 fn test_severity_ordering() {
183 assert!(Severity::Info < Severity::Warning);
184 assert!(Severity::Warning < Severity::Error);
185 }
186 #[test]
187 fn test_diagnostic_display() {
188 let d = Diagnostic::error("bad type").at(Name::str("foo"));
189 let s = d.to_string();
190 assert!(s.contains("error"));
191 assert!(s.contains("foo"));
192 assert!(s.contains("bad type"));
193 }
194 #[test]
195 fn test_error_context_format() {
196 let ctx = ErrorContext::new()
197 .push("checking Nat.add")
198 .push("checking body");
199 let s = ctx.format();
200 assert!(s.contains("checking Nat.add"));
201 }
202 #[test]
203 fn test_error_context_into_error() {
204 let ctx = ErrorContext::new().push("step 1");
205 let err = ctx.into_error("something went wrong");
206 assert!(matches!(err, KernelError::Other(_)));
207 }
208 #[test]
209 fn test_format_error_panel() {
210 let err = KernelError::UnboundVariable(3);
211 let panel = format_error_panel(&err, 40);
212 assert!(panel.contains("unbound variable"));
213 }
214 #[test]
215 fn test_summarise_error_long() {
216 let err = KernelError::Other("a".repeat(200));
217 let s = summarise_error(&err, 50);
218 assert!(s.len() <= 50);
219 assert!(s.ends_with("..."));
220 }
221 #[test]
222 fn test_summarise_error_short() {
223 let err = KernelError::Other("short".to_string());
224 let s = summarise_error(&err, 100);
225 assert_eq!(s, "short");
226 }
227 #[test]
228 fn test_collect_unknown_constants() {
229 let errs = vec![
230 KernelError::UnknownConstant(Name::str("Foo")),
231 KernelError::UnboundVariable(1),
232 KernelError::UnknownConstant(Name::str("Bar")),
233 KernelError::UnknownConstant(Name::str("Foo")),
234 ];
235 let names = collect_unknown_constants(&errs);
236 assert_eq!(names.len(), 2);
237 }
238 #[test]
239 fn test_has_universe_errors() {
240 let no_univ = vec![KernelError::UnboundVariable(0)];
241 assert!(!has_universe_errors(&no_univ));
242 let with_univ = vec![KernelError::UniverseInconsistency {
243 lhs: Level::zero(),
244 rhs: Level::succ(Level::zero()),
245 }];
246 assert!(has_universe_errors(&with_univ));
247 }
248 #[test]
249 fn test_kernel_result_ext_context() {
250 let r: Result<(), KernelError> = Err(KernelError::UnboundVariable(5));
251 let r2 = r.context("while checking foo");
252 let s = r2.unwrap_err().to_string();
253 assert!(s.contains("while checking foo"));
254 }
255 #[test]
256 fn test_from_string_conversion() {
257 let err: KernelError = "hello".into();
258 assert!(matches!(err, KernelError::Other(_)));
259 let err2: KernelError = String::from("world").into();
260 assert!(matches!(err2, KernelError::Other(_)));
261 }
262 #[test]
263 fn test_count_by_category() {
264 let mut acc = ErrorAccumulator::new();
265 acc.push(KernelError::UnboundVariable(0));
266 acc.push(KernelError::UnboundVariable(1));
267 acc.push(KernelError::UnknownConstant(Name::str("X")));
268 let counts = acc.count_by_category();
269 assert_eq!(counts[&ErrorCategory::Binding], 2);
270 assert_eq!(counts[&ErrorCategory::Resolution], 1);
271 }
272 #[test]
273 fn test_fatal_recoverable_split() {
274 let mut acc = ErrorAccumulator::new();
275 acc.push(KernelError::UnboundVariable(0));
276 acc.push(KernelError::Other("x".to_string()));
277 assert_eq!(acc.fatal_errors().len(), 1);
278 assert_eq!(acc.recoverable_errors().len(), 1);
279 }
280 #[test]
281 fn test_short_description() {
282 let err = KernelError::NotASort(mk_sort());
283 assert!(err.short_description().contains("sort"));
284 let err2 = KernelError::NotAFunction(mk_sort());
285 assert!(err2.short_description().contains("function"));
286 }
287 #[test]
288 fn test_with_context_type_mismatch() {
289 let err = KernelError::TypeMismatch {
290 expected: mk_sort(),
291 got: mk_sort(),
292 context: "inner".to_string(),
293 };
294 let err2 = err.with_context("outer");
295 if let KernelError::TypeMismatch { context, .. } = err2 {
296 assert!(context.contains("outer"));
297 assert!(context.contains("inner"));
298 } else {
299 panic!("expected TypeMismatch");
300 }
301 }
302 #[test]
303 fn test_try_kernel_ok() {
304 let r: KernelResult<i32> = try_kernel(|| Ok::<i32, std::num::ParseIntError>(42));
305 assert_eq!(r.expect("r should be valid"), 42);
306 }
307 #[test]
308 fn test_try_kernel_err() {
309 let r: KernelResult<i32> = try_kernel(|| "abc".parse::<i32>());
310 assert!(r.is_err());
311 }
312 #[test]
313 fn test_diagnostic_collection_by_severity() {
314 let mut coll = DiagnosticCollection::new();
315 coll.add(Diagnostic::error("e1"));
316 coll.add(Diagnostic::warning("w1"));
317 coll.add(Diagnostic::info("i1"));
318 coll.add(Diagnostic::error("e2"));
319 assert_eq!(coll.errors().len(), 2);
320 assert_eq!(coll.warnings().len(), 1);
321 assert_eq!(coll.by_severity(Severity::Info).len(), 1);
322 }
323}
324#[cfg(test)]
325mod extra_error_tests {
326 use super::*;
327 #[test]
328 fn test_error_note_display_no_location() {
329 let note = ErrorNote::new("try something else");
330 let s = note.to_string();
331 assert!(s.contains("try something else"));
332 assert!(s.contains("note:"));
333 }
334 #[test]
335 fn test_error_note_display_with_location() {
336 let note = ErrorNote::new("see definition").at(Name::str("Foo.bar"));
337 let s = note.to_string();
338 assert!(s.contains("Foo.bar"));
339 }
340 #[test]
341 fn test_annotated_error_no_notes() {
342 let ae = AnnotatedError::new(KernelError::UnboundVariable(3));
343 assert_eq!(ae.num_notes(), 0);
344 }
345 #[test]
346 fn test_annotated_error_with_note() {
347 let ae = AnnotatedError::new(KernelError::UnboundVariable(3))
348 .with_note(ErrorNote::new("check binder count"));
349 assert_eq!(ae.num_notes(), 1);
350 }
351 #[test]
352 fn test_annotated_error_display() {
353 let ae =
354 AnnotatedError::new(KernelError::Other("bad".into())).with_note(ErrorNote::new("hint"));
355 let s = ae.to_string();
356 assert!(s.contains("bad"));
357 assert!(s.contains("hint"));
358 }
359 #[test]
360 fn test_annotated_error_is_fatal() {
361 let ae = AnnotatedError::new(KernelError::UnboundVariable(0));
362 assert!(ae.is_fatal());
363 let ae2 = AnnotatedError::new(KernelError::Other("x".into()));
364 assert!(!ae2.is_fatal());
365 }
366 #[test]
367 fn test_kernel_phase_display() {
368 assert_eq!(format!("{}", KernelPhase::Parse), "parse");
369 assert_eq!(format!("{}", KernelPhase::TypeCheck), "type-check");
370 }
371 #[test]
372 fn test_phased_error_display() {
373 let pe = PhasedError::new(KernelPhase::Elab, KernelError::UnboundVariable(2));
374 let s = pe.to_string();
375 assert!(s.contains("elab"));
376 assert!(s.contains("unbound"));
377 }
378 #[test]
379 fn test_phased_error_new() {
380 let pe = PhasedError::new(KernelPhase::Reduction, KernelError::Other("x".into()));
381 assert_eq!(pe.phase, KernelPhase::Reduction);
382 }
383 #[test]
384 fn test_error_note_at() {
385 let note = ErrorNote::new("see here").at(Name::str("Nat.add"));
386 assert!(note.location.is_some());
387 }
388}
389#[cfg(test)]
390mod tests_padding_infra {
391 use super::*;
392 #[test]
393 fn test_stat_summary() {
394 let mut ss = StatSummary::new();
395 ss.record(10.0);
396 ss.record(20.0);
397 ss.record(30.0);
398 assert_eq!(ss.count(), 3);
399 assert!((ss.mean().expect("mean should succeed") - 20.0).abs() < 1e-9);
400 assert_eq!(ss.min().expect("min should succeed") as i64, 10);
401 assert_eq!(ss.max().expect("max should succeed") as i64, 30);
402 }
403 #[test]
404 fn test_transform_stat() {
405 let mut ts = TransformStat::new();
406 ts.record_before(100.0);
407 ts.record_after(80.0);
408 let ratio = ts.mean_ratio().expect("ratio should be present");
409 assert!((ratio - 0.8).abs() < 1e-9);
410 }
411 #[test]
412 fn test_small_map() {
413 let mut m: SmallMap<u32, &str> = SmallMap::new();
414 m.insert(3, "three");
415 m.insert(1, "one");
416 m.insert(2, "two");
417 assert_eq!(m.get(&2), Some(&"two"));
418 assert_eq!(m.len(), 3);
419 let keys = m.keys();
420 assert_eq!(*keys[0], 1);
421 assert_eq!(*keys[2], 3);
422 }
423 #[test]
424 fn test_label_set() {
425 let mut ls = LabelSet::new();
426 ls.add("foo");
427 ls.add("bar");
428 ls.add("foo");
429 assert_eq!(ls.count(), 2);
430 assert!(ls.has("bar"));
431 assert!(!ls.has("baz"));
432 }
433 #[test]
434 fn test_config_node() {
435 let mut root = ConfigNode::section("root");
436 let child = ConfigNode::leaf("key", "value");
437 root.add_child(child);
438 assert_eq!(root.num_children(), 1);
439 }
440 #[test]
441 fn test_versioned_record() {
442 let mut vr = VersionedRecord::new(0u32);
443 vr.update(1);
444 vr.update(2);
445 assert_eq!(*vr.current(), 2);
446 assert_eq!(vr.version(), 2);
447 assert!(vr.has_history());
448 assert_eq!(*vr.at_version(0).expect("value should be present"), 0);
449 }
450 #[test]
451 fn test_simple_dag() {
452 let mut dag = SimpleDag::new(4);
453 dag.add_edge(0, 1);
454 dag.add_edge(1, 2);
455 dag.add_edge(2, 3);
456 assert!(dag.can_reach(0, 3));
457 assert!(!dag.can_reach(3, 0));
458 let order = dag.topological_sort().expect("order should be present");
459 assert_eq!(order, vec![0, 1, 2, 3]);
460 }
461 #[test]
462 fn test_focus_stack() {
463 let mut fs: FocusStack<&str> = FocusStack::new();
464 fs.focus("a");
465 fs.focus("b");
466 assert_eq!(fs.current(), Some(&"b"));
467 assert_eq!(fs.depth(), 2);
468 fs.blur();
469 assert_eq!(fs.current(), Some(&"a"));
470 }
471}
472#[cfg(test)]
473mod tests_extra_iterators {
474 use super::*;
475 #[test]
476 fn test_window_iterator() {
477 let data = vec![1u32, 2, 3, 4, 5];
478 let windows: Vec<_> = WindowIterator::new(&data, 3).collect();
479 assert_eq!(windows.len(), 3);
480 assert_eq!(windows[0], &[1, 2, 3]);
481 assert_eq!(windows[2], &[3, 4, 5]);
482 }
483 #[test]
484 fn test_non_empty_vec() {
485 let mut nev = NonEmptyVec::singleton(10u32);
486 nev.push(20);
487 nev.push(30);
488 assert_eq!(nev.len(), 3);
489 assert_eq!(*nev.first(), 10);
490 assert_eq!(*nev.last(), 30);
491 }
492}
493#[cfg(test)]
494mod tests_padding2 {
495 use super::*;
496 #[test]
497 fn test_sliding_sum() {
498 let mut ss = SlidingSum::new(3);
499 ss.push(1.0);
500 ss.push(2.0);
501 ss.push(3.0);
502 assert!((ss.sum() - 6.0).abs() < 1e-9);
503 ss.push(4.0);
504 assert!((ss.sum() - 9.0).abs() < 1e-9);
505 assert_eq!(ss.count(), 3);
506 }
507 #[test]
508 fn test_path_buf() {
509 let mut pb = PathBuf::new();
510 pb.push("src");
511 pb.push("main");
512 assert_eq!(pb.as_str(), "src/main");
513 assert_eq!(pb.depth(), 2);
514 pb.pop();
515 assert_eq!(pb.as_str(), "src");
516 }
517 #[test]
518 fn test_string_pool() {
519 let mut pool = StringPool::new();
520 let s = pool.take();
521 assert!(s.is_empty());
522 pool.give("hello".to_string());
523 let s2 = pool.take();
524 assert!(s2.is_empty());
525 assert_eq!(pool.free_count(), 0);
526 }
527 #[test]
528 fn test_transitive_closure() {
529 let mut tc = TransitiveClosure::new(4);
530 tc.add_edge(0, 1);
531 tc.add_edge(1, 2);
532 tc.add_edge(2, 3);
533 assert!(tc.can_reach(0, 3));
534 assert!(!tc.can_reach(3, 0));
535 let r = tc.reachable_from(0);
536 assert_eq!(r.len(), 4);
537 }
538 #[test]
539 fn test_token_bucket() {
540 let mut tb = TokenBucket::new(100, 10);
541 assert_eq!(tb.available(), 100);
542 assert!(tb.try_consume(50));
543 assert_eq!(tb.available(), 50);
544 assert!(!tb.try_consume(60));
545 assert_eq!(tb.capacity(), 100);
546 }
547 #[test]
548 fn test_rewrite_rule_set() {
549 let mut rrs = RewriteRuleSet::new();
550 rrs.add(RewriteRule::unconditional(
551 "beta",
552 "App(Lam(x, b), v)",
553 "b[x:=v]",
554 ));
555 rrs.add(RewriteRule::conditional("comm", "a + b", "b + a"));
556 assert_eq!(rrs.len(), 2);
557 assert_eq!(rrs.unconditional_rules().len(), 1);
558 assert_eq!(rrs.conditional_rules().len(), 1);
559 assert!(rrs.get("beta").is_some());
560 let disp = rrs
561 .get("beta")
562 .expect("element at \'beta\' should exist")
563 .display();
564 assert!(disp.contains("→"));
565 }
566}
567#[cfg(test)]
568mod tests_padding3 {
569 use super::*;
570 #[test]
571 fn test_decision_node() {
572 let tree = DecisionNode::Branch {
573 key: "x".into(),
574 val: "1".into(),
575 yes_branch: Box::new(DecisionNode::Leaf("yes".into())),
576 no_branch: Box::new(DecisionNode::Leaf("no".into())),
577 };
578 let mut ctx = std::collections::HashMap::new();
579 ctx.insert("x".into(), "1".into());
580 assert_eq!(tree.evaluate(&ctx), "yes");
581 ctx.insert("x".into(), "2".into());
582 assert_eq!(tree.evaluate(&ctx), "no");
583 assert_eq!(tree.depth(), 1);
584 }
585 #[test]
586 fn test_flat_substitution() {
587 let mut sub = FlatSubstitution::new();
588 sub.add("foo", "bar");
589 sub.add("baz", "qux");
590 assert_eq!(sub.apply("foo and baz"), "bar and qux");
591 assert_eq!(sub.len(), 2);
592 }
593 #[test]
594 fn test_stopwatch() {
595 let mut sw = Stopwatch::start();
596 sw.split();
597 sw.split();
598 assert_eq!(sw.num_splits(), 2);
599 assert!(sw.elapsed_ms() >= 0.0);
600 for &s in sw.splits() {
601 assert!(s >= 0.0);
602 }
603 }
604 #[test]
605 fn test_either2() {
606 let e: Either2<i32, &str> = Either2::First(42);
607 assert!(e.is_first());
608 let mapped = e.map_first(|x| x * 2);
609 assert_eq!(mapped.first(), Some(84));
610 let e2: Either2<i32, &str> = Either2::Second("hello");
611 assert!(e2.is_second());
612 assert_eq!(e2.second(), Some("hello"));
613 }
614 #[test]
615 fn test_write_once() {
616 let wo: WriteOnce<u32> = WriteOnce::new();
617 assert!(!wo.is_written());
618 assert!(wo.write(42));
619 assert!(!wo.write(99));
620 assert_eq!(wo.read(), Some(42));
621 }
622 #[test]
623 fn test_sparse_vec() {
624 let mut sv: SparseVec<i32> = SparseVec::new(100);
625 sv.set(5, 10);
626 sv.set(50, 20);
627 assert_eq!(*sv.get(5), 10);
628 assert_eq!(*sv.get(50), 20);
629 assert_eq!(*sv.get(0), 0);
630 assert_eq!(sv.nnz(), 2);
631 sv.set(5, 0);
632 assert_eq!(sv.nnz(), 1);
633 }
634 #[test]
635 fn test_stack_calc() {
636 let mut calc = StackCalc::new();
637 calc.push(3);
638 calc.push(4);
639 calc.add();
640 assert_eq!(calc.peek(), Some(7));
641 calc.push(2);
642 calc.mul();
643 assert_eq!(calc.peek(), Some(14));
644 }
645}
646#[cfg(test)]
647mod tests_final_padding {
648 use super::*;
649 #[test]
650 fn test_min_heap() {
651 let mut h = MinHeap::new();
652 h.push(5u32);
653 h.push(1u32);
654 h.push(3u32);
655 assert_eq!(h.peek(), Some(&1));
656 assert_eq!(h.pop(), Some(1));
657 assert_eq!(h.pop(), Some(3));
658 assert_eq!(h.pop(), Some(5));
659 assert!(h.is_empty());
660 }
661 #[test]
662 fn test_prefix_counter() {
663 let mut pc = PrefixCounter::new();
664 pc.record("hello");
665 pc.record("help");
666 pc.record("world");
667 assert_eq!(pc.count_with_prefix("hel"), 2);
668 assert_eq!(pc.count_with_prefix("wor"), 1);
669 assert_eq!(pc.count_with_prefix("xyz"), 0);
670 }
671 #[test]
672 fn test_fixture() {
673 let mut f = Fixture::new();
674 f.set("key1", "val1");
675 f.set("key2", "val2");
676 assert_eq!(f.get("key1"), Some("val1"));
677 assert_eq!(f.get("key3"), None);
678 assert_eq!(f.len(), 2);
679 }
680}