1use super::functions::*;
6use crate::{Expr, Name};
7use std::collections::{HashMap, HashSet};
8
9#[allow(dead_code)]
11pub struct SimpleDag {
12 edges: Vec<Vec<usize>>,
14}
15#[allow(dead_code)]
16impl SimpleDag {
17 pub fn new(n: usize) -> Self {
19 Self {
20 edges: vec![Vec::new(); n],
21 }
22 }
23 pub fn add_edge(&mut self, from: usize, to: usize) {
25 if from < self.edges.len() {
26 self.edges[from].push(to);
27 }
28 }
29 pub fn successors(&self, node: usize) -> &[usize] {
31 self.edges.get(node).map(|v| v.as_slice()).unwrap_or(&[])
32 }
33 pub fn can_reach(&self, from: usize, to: usize) -> bool {
35 let mut visited = vec![false; self.edges.len()];
36 self.dfs(from, to, &mut visited)
37 }
38 fn dfs(&self, cur: usize, target: usize, visited: &mut Vec<bool>) -> bool {
39 if cur == target {
40 return true;
41 }
42 if cur >= visited.len() || visited[cur] {
43 return false;
44 }
45 visited[cur] = true;
46 for &next in self.successors(cur) {
47 if self.dfs(next, target, visited) {
48 return true;
49 }
50 }
51 false
52 }
53 pub fn topological_sort(&self) -> Option<Vec<usize>> {
55 let n = self.edges.len();
56 let mut in_degree = vec![0usize; n];
57 for succs in &self.edges {
58 for &s in succs {
59 if s < n {
60 in_degree[s] += 1;
61 }
62 }
63 }
64 let mut queue: std::collections::VecDeque<usize> =
65 (0..n).filter(|&i| in_degree[i] == 0).collect();
66 let mut order = Vec::new();
67 while let Some(node) = queue.pop_front() {
68 order.push(node);
69 for &s in self.successors(node) {
70 if s < n {
71 in_degree[s] -= 1;
72 if in_degree[s] == 0 {
73 queue.push_back(s);
74 }
75 }
76 }
77 }
78 if order.len() == n {
79 Some(order)
80 } else {
81 None
82 }
83 }
84 pub fn num_nodes(&self) -> usize {
86 self.edges.len()
87 }
88}
89#[allow(dead_code)]
91pub struct SlidingSum {
92 window: Vec<f64>,
93 capacity: usize,
94 pos: usize,
95 sum: f64,
96 count: usize,
97}
98#[allow(dead_code)]
99impl SlidingSum {
100 pub fn new(capacity: usize) -> Self {
102 Self {
103 window: vec![0.0; capacity],
104 capacity,
105 pos: 0,
106 sum: 0.0,
107 count: 0,
108 }
109 }
110 pub fn push(&mut self, val: f64) {
112 let oldest = self.window[self.pos];
113 self.sum -= oldest;
114 self.sum += val;
115 self.window[self.pos] = val;
116 self.pos = (self.pos + 1) % self.capacity;
117 if self.count < self.capacity {
118 self.count += 1;
119 }
120 }
121 pub fn sum(&self) -> f64 {
123 self.sum
124 }
125 pub fn mean(&self) -> Option<f64> {
127 if self.count == 0 {
128 None
129 } else {
130 Some(self.sum / self.count as f64)
131 }
132 }
133 pub fn count(&self) -> usize {
135 self.count
136 }
137}
138#[allow(dead_code)]
140pub struct MinHeap<T: Ord> {
141 data: Vec<T>,
142}
143#[allow(dead_code)]
144impl<T: Ord> MinHeap<T> {
145 pub fn new() -> Self {
147 Self { data: Vec::new() }
148 }
149 pub fn push(&mut self, val: T) {
151 self.data.push(val);
152 self.sift_up(self.data.len() - 1);
153 }
154 pub fn pop(&mut self) -> Option<T> {
156 if self.data.is_empty() {
157 return None;
158 }
159 let n = self.data.len();
160 self.data.swap(0, n - 1);
161 let min = self.data.pop();
162 if !self.data.is_empty() {
163 self.sift_down(0);
164 }
165 min
166 }
167 pub fn peek(&self) -> Option<&T> {
169 self.data.first()
170 }
171 pub fn len(&self) -> usize {
173 self.data.len()
174 }
175 pub fn is_empty(&self) -> bool {
177 self.data.is_empty()
178 }
179 fn sift_up(&mut self, mut i: usize) {
180 while i > 0 {
181 let parent = (i - 1) / 2;
182 if self.data[i] < self.data[parent] {
183 self.data.swap(i, parent);
184 i = parent;
185 } else {
186 break;
187 }
188 }
189 }
190 fn sift_down(&mut self, mut i: usize) {
191 let n = self.data.len();
192 loop {
193 let left = 2 * i + 1;
194 let right = 2 * i + 2;
195 let mut smallest = i;
196 if left < n && self.data[left] < self.data[smallest] {
197 smallest = left;
198 }
199 if right < n && self.data[right] < self.data[smallest] {
200 smallest = right;
201 }
202 if smallest == i {
203 break;
204 }
205 self.data.swap(i, smallest);
206 i = smallest;
207 }
208 }
209}
210#[allow(dead_code)]
212pub struct VersionedRecord<T: Clone> {
213 history: Vec<T>,
214}
215#[allow(dead_code)]
216impl<T: Clone> VersionedRecord<T> {
217 pub fn new(initial: T) -> Self {
219 Self {
220 history: vec![initial],
221 }
222 }
223 pub fn update(&mut self, val: T) {
225 self.history.push(val);
226 }
227 pub fn current(&self) -> &T {
229 self.history
230 .last()
231 .expect("VersionedRecord history is always non-empty after construction")
232 }
233 pub fn at_version(&self, n: usize) -> Option<&T> {
235 self.history.get(n)
236 }
237 pub fn version(&self) -> usize {
239 self.history.len() - 1
240 }
241 pub fn has_history(&self) -> bool {
243 self.history.len() > 1
244 }
245}
246#[allow(dead_code)]
248pub struct TransitiveClosure {
249 adj: Vec<Vec<usize>>,
250 n: usize,
251}
252#[allow(dead_code)]
253impl TransitiveClosure {
254 pub fn new(n: usize) -> Self {
256 Self {
257 adj: vec![Vec::new(); n],
258 n,
259 }
260 }
261 pub fn add_edge(&mut self, from: usize, to: usize) {
263 if from < self.n {
264 self.adj[from].push(to);
265 }
266 }
267 pub fn reachable_from(&self, start: usize) -> Vec<usize> {
269 let mut visited = vec![false; self.n];
270 let mut queue = std::collections::VecDeque::new();
271 queue.push_back(start);
272 while let Some(node) = queue.pop_front() {
273 if node >= self.n || visited[node] {
274 continue;
275 }
276 visited[node] = true;
277 for &next in &self.adj[node] {
278 queue.push_back(next);
279 }
280 }
281 (0..self.n).filter(|&i| visited[i]).collect()
282 }
283 pub fn can_reach(&self, from: usize, to: usize) -> bool {
285 self.reachable_from(from).contains(&to)
286 }
287}
288#[allow(dead_code)]
290#[allow(missing_docs)]
291pub enum DecisionNode {
292 Leaf(String),
294 Branch {
296 key: String,
297 val: String,
298 yes_branch: Box<DecisionNode>,
299 no_branch: Box<DecisionNode>,
300 },
301}
302#[allow(dead_code)]
303impl DecisionNode {
304 pub fn evaluate(&self, ctx: &std::collections::HashMap<String, String>) -> &str {
306 match self {
307 DecisionNode::Leaf(action) => action.as_str(),
308 DecisionNode::Branch {
309 key,
310 val,
311 yes_branch,
312 no_branch,
313 } => {
314 let actual = ctx.get(key).map(|s| s.as_str()).unwrap_or("");
315 if actual == val.as_str() {
316 yes_branch.evaluate(ctx)
317 } else {
318 no_branch.evaluate(ctx)
319 }
320 }
321 }
322 }
323 pub fn depth(&self) -> usize {
325 match self {
326 DecisionNode::Leaf(_) => 0,
327 DecisionNode::Branch {
328 yes_branch,
329 no_branch,
330 ..
331 } => 1 + yes_branch.depth().max(no_branch.depth()),
332 }
333 }
334}
335#[allow(dead_code)]
337pub struct SparseVec<T: Default + Clone + PartialEq> {
338 entries: std::collections::HashMap<usize, T>,
339 default_: T,
340 logical_len: usize,
341}
342#[allow(dead_code)]
343impl<T: Default + Clone + PartialEq> SparseVec<T> {
344 pub fn new(len: usize) -> Self {
346 Self {
347 entries: std::collections::HashMap::new(),
348 default_: T::default(),
349 logical_len: len,
350 }
351 }
352 pub fn set(&mut self, idx: usize, val: T) {
354 if val == self.default_ {
355 self.entries.remove(&idx);
356 } else {
357 self.entries.insert(idx, val);
358 }
359 }
360 pub fn get(&self, idx: usize) -> &T {
362 self.entries.get(&idx).unwrap_or(&self.default_)
363 }
364 pub fn len(&self) -> usize {
366 self.logical_len
367 }
368 pub fn is_empty(&self) -> bool {
370 self.len() == 0
371 }
372 pub fn nnz(&self) -> usize {
374 self.entries.len()
375 }
376}
377#[allow(dead_code)]
379pub struct ConfigNode {
380 key: String,
381 value: Option<String>,
382 children: Vec<ConfigNode>,
383}
384#[allow(dead_code)]
385impl ConfigNode {
386 pub fn leaf(key: impl Into<String>, value: impl Into<String>) -> Self {
388 Self {
389 key: key.into(),
390 value: Some(value.into()),
391 children: Vec::new(),
392 }
393 }
394 pub fn section(key: impl Into<String>) -> Self {
396 Self {
397 key: key.into(),
398 value: None,
399 children: Vec::new(),
400 }
401 }
402 pub fn add_child(&mut self, child: ConfigNode) {
404 self.children.push(child);
405 }
406 pub fn key(&self) -> &str {
408 &self.key
409 }
410 pub fn value(&self) -> Option<&str> {
412 self.value.as_deref()
413 }
414 pub fn num_children(&self) -> usize {
416 self.children.len()
417 }
418 pub fn lookup(&self, path: &str) -> Option<&str> {
420 let mut parts = path.splitn(2, '.');
421 let head = parts.next()?;
422 let tail = parts.next();
423 if head != self.key {
424 return None;
425 }
426 match tail {
427 None => self.value.as_deref(),
428 Some(rest) => self.children.iter().find_map(|c| c.lookup_relative(rest)),
429 }
430 }
431 fn lookup_relative(&self, path: &str) -> Option<&str> {
432 let mut parts = path.splitn(2, '.');
433 let head = parts.next()?;
434 let tail = parts.next();
435 if head != self.key {
436 return None;
437 }
438 match tail {
439 None => self.value.as_deref(),
440 Some(rest) => self.children.iter().find_map(|c| c.lookup_relative(rest)),
441 }
442 }
443}
444#[allow(dead_code)]
446pub struct SmallMap<K: Ord + Clone, V: Clone> {
447 entries: Vec<(K, V)>,
448}
449#[allow(dead_code)]
450impl<K: Ord + Clone, V: Clone> SmallMap<K, V> {
451 pub fn new() -> Self {
453 Self {
454 entries: Vec::new(),
455 }
456 }
457 pub fn insert(&mut self, key: K, val: V) {
459 match self.entries.binary_search_by_key(&&key, |(k, _)| k) {
460 Ok(i) => self.entries[i].1 = val,
461 Err(i) => self.entries.insert(i, (key, val)),
462 }
463 }
464 pub fn get(&self, key: &K) -> Option<&V> {
466 self.entries
467 .binary_search_by_key(&key, |(k, _)| k)
468 .ok()
469 .map(|i| &self.entries[i].1)
470 }
471 pub fn len(&self) -> usize {
473 self.entries.len()
474 }
475 pub fn is_empty(&self) -> bool {
477 self.entries.is_empty()
478 }
479 pub fn keys(&self) -> Vec<&K> {
481 self.entries.iter().map(|(k, _)| k).collect()
482 }
483 pub fn values(&self) -> Vec<&V> {
485 self.entries.iter().map(|(_, v)| v).collect()
486 }
487}
488#[allow(dead_code)]
490pub struct PathBuf {
491 components: Vec<String>,
492}
493#[allow(dead_code)]
494impl PathBuf {
495 pub fn new() -> Self {
497 Self {
498 components: Vec::new(),
499 }
500 }
501 pub fn push(&mut self, comp: impl Into<String>) {
503 self.components.push(comp.into());
504 }
505 pub fn pop(&mut self) {
507 self.components.pop();
508 }
509 pub fn as_str(&self) -> String {
511 self.components.join("/")
512 }
513 pub fn depth(&self) -> usize {
515 self.components.len()
516 }
517 pub fn clear(&mut self) {
519 self.components.clear();
520 }
521}
522#[derive(Debug, Clone)]
524pub struct ParamInfo {
525 pub name: Name,
527 pub pos: usize,
529 pub inductive_type: Option<Name>,
531}
532#[allow(dead_code)]
534pub struct NonEmptyVec<T> {
535 head: T,
536 tail: Vec<T>,
537}
538#[allow(dead_code)]
539impl<T> NonEmptyVec<T> {
540 pub fn singleton(val: T) -> Self {
542 Self {
543 head: val,
544 tail: Vec::new(),
545 }
546 }
547 pub fn push(&mut self, val: T) {
549 self.tail.push(val);
550 }
551 pub fn first(&self) -> &T {
553 &self.head
554 }
555 pub fn last(&self) -> &T {
557 self.tail.last().unwrap_or(&self.head)
558 }
559 pub fn len(&self) -> usize {
561 1 + self.tail.len()
562 }
563 pub fn is_empty(&self) -> bool {
565 self.len() == 0
566 }
567 pub fn to_vec(&self) -> Vec<&T> {
569 let mut v = vec![&self.head];
570 v.extend(self.tail.iter());
571 v
572 }
573}
574#[allow(dead_code)]
576pub struct WriteOnce<T> {
577 value: std::cell::Cell<Option<T>>,
578}
579#[allow(dead_code)]
580impl<T: Copy> WriteOnce<T> {
581 pub fn new() -> Self {
583 Self {
584 value: std::cell::Cell::new(None),
585 }
586 }
587 pub fn write(&self, val: T) -> bool {
589 if self.value.get().is_some() {
590 return false;
591 }
592 self.value.set(Some(val));
593 true
594 }
595 pub fn read(&self) -> Option<T> {
597 self.value.get()
598 }
599 pub fn is_written(&self) -> bool {
601 self.value.get().is_some()
602 }
603}
604#[allow(dead_code)]
606#[derive(Debug, Clone, PartialEq, Eq)]
607pub enum WfRelationKind {
608 Structural {
610 inductive_type: Name,
612 param_index: usize,
614 },
615 Measure {
617 measure_fn: Name,
619 },
620 Lexicographic {
622 components: Vec<WfRelationKind>,
624 },
625 NatSub,
627 Custom {
629 relation: Name,
631 },
632}
633impl WfRelationKind {
634 #[allow(dead_code)]
636 pub fn is_structural(&self) -> bool {
637 matches!(self, WfRelationKind::Structural { .. })
638 }
639 #[allow(dead_code)]
641 pub fn lex_depth(&self) -> usize {
642 match self {
643 WfRelationKind::Lexicographic { components } => components.len(),
644 _ => 1,
645 }
646 }
647 #[allow(dead_code)]
649 pub fn description(&self) -> String {
650 match self {
651 WfRelationKind::Structural {
652 inductive_type,
653 param_index,
654 } => {
655 format!("structural on {} (param {})", inductive_type, param_index)
656 }
657 WfRelationKind::Measure { measure_fn } => {
658 format!("measure by {}", measure_fn)
659 }
660 WfRelationKind::Lexicographic { components } => {
661 format!("lexicographic ({} components)", components.len())
662 }
663 WfRelationKind::NatSub => "nat subtraction".to_string(),
664 WfRelationKind::Custom { relation } => {
665 format!("custom relation {}", relation)
666 }
667 }
668 }
669}
670#[derive(Debug, Clone)]
672pub struct TerminationResult {
673 pub decreasing_param: Option<usize>,
675 pub recursive_calls: Vec<RecCallInfo>,
677 pub is_terminating: bool,
679}
680#[allow(dead_code)]
682#[derive(Debug, Clone, Default)]
683pub struct StringTrie {
684 pub(super) children: std::collections::HashMap<char, StringTrie>,
685 is_end: bool,
686 pub(super) value: Option<String>,
687}
688impl StringTrie {
689 #[allow(dead_code)]
691 pub fn new() -> Self {
692 Self::default()
693 }
694 #[allow(dead_code)]
696 pub fn insert(&mut self, s: &str) {
697 let mut node = self;
698 for c in s.chars() {
699 node = node.children.entry(c).or_default();
700 }
701 node.is_end = true;
702 node.value = Some(s.to_string());
703 }
704 #[allow(dead_code)]
706 pub fn contains(&self, s: &str) -> bool {
707 let mut node = self;
708 for c in s.chars() {
709 match node.children.get(&c) {
710 Some(next) => node = next,
711 None => return false,
712 }
713 }
714 node.is_end
715 }
716 #[allow(dead_code)]
718 pub fn starts_with(&self, prefix: &str) -> Vec<String> {
719 let mut node = self;
720 for c in prefix.chars() {
721 match node.children.get(&c) {
722 Some(next) => node = next,
723 None => return vec![],
724 }
725 }
726 let mut results = Vec::new();
727 collect_strings(node, &mut results);
728 results
729 }
730 #[allow(dead_code)]
732 pub fn len(&self) -> usize {
733 let mut count = if self.is_end { 1 } else { 0 };
734 for child in self.children.values() {
735 count += child.len();
736 }
737 count
738 }
739 #[allow(dead_code)]
741 pub fn is_empty(&self) -> bool {
742 self.len() == 0
743 }
744}
745#[allow(dead_code)]
747pub struct LabelSet {
748 labels: Vec<String>,
749}
750#[allow(dead_code)]
751impl LabelSet {
752 pub fn new() -> Self {
754 Self { labels: Vec::new() }
755 }
756 pub fn add(&mut self, label: impl Into<String>) {
758 let s = label.into();
759 if !self.labels.contains(&s) {
760 self.labels.push(s);
761 }
762 }
763 pub fn has(&self, label: &str) -> bool {
765 self.labels.iter().any(|l| l == label)
766 }
767 pub fn count(&self) -> usize {
769 self.labels.len()
770 }
771 pub fn all(&self) -> &[String] {
773 &self.labels
774 }
775}
776#[allow(dead_code)]
778pub struct Stopwatch {
779 start: std::time::Instant,
780 splits: Vec<f64>,
781}
782#[allow(dead_code)]
783impl Stopwatch {
784 pub fn start() -> Self {
786 Self {
787 start: std::time::Instant::now(),
788 splits: Vec::new(),
789 }
790 }
791 pub fn split(&mut self) {
793 self.splits.push(self.elapsed_ms());
794 }
795 pub fn elapsed_ms(&self) -> f64 {
797 self.start.elapsed().as_secs_f64() * 1000.0
798 }
799 pub fn splits(&self) -> &[f64] {
801 &self.splits
802 }
803 pub fn num_splits(&self) -> usize {
805 self.splits.len()
806 }
807}
808#[derive(Debug, Clone)]
810pub struct RecCallInfo {
811 pub callee: Name,
813 pub arg_pos: usize,
815 pub arg: Expr,
817 pub is_decreasing: bool,
819}
820pub struct TerminationChecker {
822 checking: HashSet<Name>,
824 param_info: HashMap<Name, Vec<ParamInfo>>,
826 call_info: HashMap<Name, Vec<RecCallInfo>>,
828 smaller: HashMap<Expr, HashSet<Expr>>,
831}
832impl TerminationChecker {
833 pub fn new() -> Self {
835 Self {
836 checking: HashSet::new(),
837 param_info: HashMap::new(),
838 call_info: HashMap::new(),
839 smaller: HashMap::new(),
840 }
841 }
842 pub fn register_params(&mut self, name: Name, params: Vec<ParamInfo>) {
844 self.param_info.insert(name, params);
845 }
846 pub fn add_smaller(&mut self, big: Expr, small: Expr) {
851 self.smaller.entry(big).or_default().insert(small);
852 }
853 pub fn is_smaller(&self, big: &Expr, small: &Expr) -> bool {
855 if let Some(smalls) = self.smaller.get(big) {
856 if smalls.contains(small) {
857 return true;
858 }
859 for mid in smalls {
860 if self.is_smaller(mid, small) {
861 return true;
862 }
863 }
864 }
865 false
866 }
867 pub fn check_terminates(&mut self, name: &Name, body: &Expr) -> Result<(), String> {
872 if self.checking.contains(name) {
873 return Err(format!("Cyclic dependency detected for {}", name));
874 }
875 self.checking.insert(name.clone());
876 let mut calls = Vec::new();
877 self.collect_recursive_calls(name, body, &mut calls, 0)?;
878 self.call_info.insert(name.clone(), calls.clone());
879 if calls.is_empty() {
880 self.checking.remove(name);
881 return Ok(());
882 }
883 let result = self.find_decreasing_param(name, &calls);
884 self.checking.remove(name);
885 if result.is_terminating {
886 Ok(())
887 } else {
888 Err(format!(
889 "Cannot verify termination of '{}': no structurally decreasing argument found",
890 name
891 ))
892 }
893 }
894 pub fn check_mutual_terminates(
896 &mut self,
897 names: &[Name],
898 bodies: &[Expr],
899 ) -> Result<(), String> {
900 if names.len() != bodies.len() {
901 return Err("Mismatched names and bodies in mutual recursion".to_string());
902 }
903 for name in names {
904 self.checking.insert(name.clone());
905 }
906 for (name, body) in names.iter().zip(bodies.iter()) {
907 let mut calls = Vec::new();
908 self.collect_recursive_calls_mutual(names, body, &mut calls, 0)?;
909 self.call_info.insert(name.clone(), calls);
910 }
911 for name in names {
912 if let Some(calls) = self.call_info.get(name) {
913 if !calls.is_empty() {
914 let result = self.find_decreasing_param(name, calls);
915 if !result.is_terminating {
916 for n in names {
917 self.checking.remove(n);
918 }
919 return Err(format!(
920 "Cannot verify termination of '{}' in mutual recursion block",
921 name
922 ));
923 }
924 }
925 }
926 }
927 for name in names {
928 self.checking.remove(name);
929 }
930 Ok(())
931 }
932 fn collect_recursive_calls(
934 &self,
935 fname: &Name,
936 expr: &Expr,
937 calls: &mut Vec<RecCallInfo>,
938 depth: usize,
939 ) -> Result<(), String> {
940 if depth > 200 {
941 return Err("Definition too deeply nested".to_string());
942 }
943 match expr {
944 Expr::App(f, a) => {
945 if let Some(call) = self.check_recursive_call(fname, expr) {
946 calls.push(call);
947 }
948 self.collect_recursive_calls(fname, f, calls, depth + 1)?;
949 self.collect_recursive_calls(fname, a, calls, depth + 1)
950 }
951 Expr::Lam(_, _, ty, body) => {
952 self.collect_recursive_calls(fname, ty, calls, depth + 1)?;
953 self.collect_recursive_calls(fname, body, calls, depth + 1)
954 }
955 Expr::Pi(_, _, ty, body) => {
956 self.collect_recursive_calls(fname, ty, calls, depth + 1)?;
957 self.collect_recursive_calls(fname, body, calls, depth + 1)
958 }
959 Expr::Let(_, ty, val, body) => {
960 self.collect_recursive_calls(fname, ty, calls, depth + 1)?;
961 self.collect_recursive_calls(fname, val, calls, depth + 1)?;
962 self.collect_recursive_calls(fname, body, calls, depth + 1)
963 }
964 _ => Ok(()),
965 }
966 }
967 fn collect_recursive_calls_mutual(
969 &self,
970 fnames: &[Name],
971 expr: &Expr,
972 calls: &mut Vec<RecCallInfo>,
973 depth: usize,
974 ) -> Result<(), String> {
975 if depth > 200 {
976 return Err("Definition too deeply nested".to_string());
977 }
978 match expr {
979 Expr::App(f, a) => {
980 for fname in fnames {
981 if let Some(call) = self.check_recursive_call(fname, expr) {
982 calls.push(call);
983 }
984 }
985 self.collect_recursive_calls_mutual(fnames, f, calls, depth + 1)?;
986 self.collect_recursive_calls_mutual(fnames, a, calls, depth + 1)
987 }
988 Expr::Lam(_, _, ty, body) => {
989 self.collect_recursive_calls_mutual(fnames, ty, calls, depth + 1)?;
990 self.collect_recursive_calls_mutual(fnames, body, calls, depth + 1)
991 }
992 Expr::Pi(_, _, ty, body) => {
993 self.collect_recursive_calls_mutual(fnames, ty, calls, depth + 1)?;
994 self.collect_recursive_calls_mutual(fnames, body, calls, depth + 1)
995 }
996 Expr::Let(_, ty, val, body) => {
997 self.collect_recursive_calls_mutual(fnames, ty, calls, depth + 1)?;
998 self.collect_recursive_calls_mutual(fnames, val, calls, depth + 1)?;
999 self.collect_recursive_calls_mutual(fnames, body, calls, depth + 1)
1000 }
1001 _ => Ok(()),
1002 }
1003 }
1004 fn check_recursive_call(&self, fname: &Name, app: &Expr) -> Option<RecCallInfo> {
1006 let (head, args) = collect_app_args(app);
1007 if let Expr::Const(name, _) = head {
1008 if name == fname {
1009 for (i, arg) in args.iter().enumerate() {
1010 let is_dec = self.is_structurally_smaller(arg);
1011 if is_dec {
1012 return Some(RecCallInfo {
1013 callee: name.clone(),
1014 arg_pos: i,
1015 arg: (*arg).clone(),
1016 is_decreasing: true,
1017 });
1018 }
1019 }
1020 if let Some(first_arg) = args.first() {
1021 return Some(RecCallInfo {
1022 callee: name.clone(),
1023 arg_pos: 0,
1024 arg: (*first_arg).clone(),
1025 is_decreasing: false,
1026 });
1027 }
1028 }
1029 }
1030 None
1031 }
1032 fn is_structurally_smaller(&self, expr: &Expr) -> bool {
1034 for smalls in self.smaller.values() {
1035 if smalls.contains(expr) {
1036 return true;
1037 }
1038 }
1039 false
1040 }
1041 fn find_decreasing_param(&self, _name: &Name, calls: &[RecCallInfo]) -> TerminationResult {
1043 if calls.is_empty() {
1044 return TerminationResult {
1045 decreasing_param: None,
1046 recursive_calls: calls.to_vec(),
1047 is_terminating: true,
1048 };
1049 }
1050 let max_pos = calls.iter().map(|c| c.arg_pos).max().unwrap_or(0);
1051 for pos in 0..=max_pos {
1052 let all_decreasing = calls.iter().all(|c| {
1053 if c.arg_pos == pos {
1054 c.is_decreasing
1055 } else {
1056 true
1057 }
1058 });
1059 if all_decreasing && calls.iter().any(|c| c.arg_pos == pos && c.is_decreasing) {
1060 return TerminationResult {
1061 decreasing_param: Some(pos),
1062 recursive_calls: calls.to_vec(),
1063 is_terminating: true,
1064 };
1065 }
1066 }
1067 let all_dec = calls.iter().all(|c| c.is_decreasing);
1068 TerminationResult {
1069 decreasing_param: None,
1070 recursive_calls: calls.to_vec(),
1071 is_terminating: all_dec,
1072 }
1073 }
1074 pub fn get_calls(&self, name: &Name) -> Option<&Vec<RecCallInfo>> {
1076 self.call_info.get(name)
1077 }
1078}
1079#[allow(dead_code)]
1081#[allow(missing_docs)]
1082pub struct RewriteRule {
1083 pub name: String,
1085 pub lhs: String,
1087 pub rhs: String,
1089 pub conditional: bool,
1091}
1092#[allow(dead_code)]
1093impl RewriteRule {
1094 pub fn unconditional(
1096 name: impl Into<String>,
1097 lhs: impl Into<String>,
1098 rhs: impl Into<String>,
1099 ) -> Self {
1100 Self {
1101 name: name.into(),
1102 lhs: lhs.into(),
1103 rhs: rhs.into(),
1104 conditional: false,
1105 }
1106 }
1107 pub fn conditional(
1109 name: impl Into<String>,
1110 lhs: impl Into<String>,
1111 rhs: impl Into<String>,
1112 ) -> Self {
1113 Self {
1114 name: name.into(),
1115 lhs: lhs.into(),
1116 rhs: rhs.into(),
1117 conditional: true,
1118 }
1119 }
1120 pub fn display(&self) -> String {
1122 format!("{}: {} → {}", self.name, self.lhs, self.rhs)
1123 }
1124}
1125#[allow(dead_code)]
1127pub struct RawFnPtr {
1128 ptr: usize,
1130 arity: usize,
1131 name: String,
1132}
1133#[allow(dead_code)]
1134impl RawFnPtr {
1135 pub fn new(ptr: usize, arity: usize, name: impl Into<String>) -> Self {
1137 Self {
1138 ptr,
1139 arity,
1140 name: name.into(),
1141 }
1142 }
1143 pub fn arity(&self) -> usize {
1145 self.arity
1146 }
1147 pub fn name(&self) -> &str {
1149 &self.name
1150 }
1151 pub fn raw(&self) -> usize {
1153 self.ptr
1154 }
1155}
1156#[allow(dead_code)]
1158pub struct TransformStat {
1159 before: StatSummary,
1160 after: StatSummary,
1161}
1162#[allow(dead_code)]
1163impl TransformStat {
1164 pub fn new() -> Self {
1166 Self {
1167 before: StatSummary::new(),
1168 after: StatSummary::new(),
1169 }
1170 }
1171 pub fn record_before(&mut self, v: f64) {
1173 self.before.record(v);
1174 }
1175 pub fn record_after(&mut self, v: f64) {
1177 self.after.record(v);
1178 }
1179 pub fn mean_ratio(&self) -> Option<f64> {
1181 let b = self.before.mean()?;
1182 let a = self.after.mean()?;
1183 if b.abs() < f64::EPSILON {
1184 return None;
1185 }
1186 Some(a / b)
1187 }
1188}
1189#[allow(dead_code)]
1191pub struct FlatSubstitution {
1192 pairs: Vec<(String, String)>,
1193}
1194#[allow(dead_code)]
1195impl FlatSubstitution {
1196 pub fn new() -> Self {
1198 Self { pairs: Vec::new() }
1199 }
1200 pub fn add(&mut self, from: impl Into<String>, to: impl Into<String>) {
1202 self.pairs.push((from.into(), to.into()));
1203 }
1204 pub fn apply(&self, s: &str) -> String {
1206 let mut result = s.to_string();
1207 for (from, to) in &self.pairs {
1208 result = result.replace(from.as_str(), to.as_str());
1209 }
1210 result
1211 }
1212 pub fn len(&self) -> usize {
1214 self.pairs.len()
1215 }
1216 pub fn is_empty(&self) -> bool {
1218 self.pairs.is_empty()
1219 }
1220}
1221#[allow(dead_code)]
1223pub struct StringPool {
1224 free: Vec<String>,
1225}
1226#[allow(dead_code)]
1227impl StringPool {
1228 pub fn new() -> Self {
1230 Self { free: Vec::new() }
1231 }
1232 pub fn take(&mut self) -> String {
1234 self.free.pop().unwrap_or_default()
1235 }
1236 pub fn give(&mut self, mut s: String) {
1238 s.clear();
1239 self.free.push(s);
1240 }
1241 pub fn free_count(&self) -> usize {
1243 self.free.len()
1244 }
1245}
1246#[allow(dead_code)]
1248pub struct PrefixCounter {
1249 children: std::collections::HashMap<char, PrefixCounter>,
1250 count: usize,
1251}
1252#[allow(dead_code)]
1253impl PrefixCounter {
1254 pub fn new() -> Self {
1256 Self {
1257 children: std::collections::HashMap::new(),
1258 count: 0,
1259 }
1260 }
1261 pub fn record(&mut self, s: &str) {
1263 self.count += 1;
1264 let mut node = self;
1265 for c in s.chars() {
1266 node = node.children.entry(c).or_default();
1267 node.count += 1;
1268 }
1269 }
1270 pub fn count_with_prefix(&self, prefix: &str) -> usize {
1272 let mut node = self;
1273 for c in prefix.chars() {
1274 match node.children.get(&c) {
1275 Some(n) => node = n,
1276 None => return 0,
1277 }
1278 }
1279 node.count
1280 }
1281}
1282#[allow(dead_code)]
1284pub struct StatSummary {
1285 count: u64,
1286 sum: f64,
1287 min: f64,
1288 max: f64,
1289}
1290#[allow(dead_code)]
1291impl StatSummary {
1292 pub fn new() -> Self {
1294 Self {
1295 count: 0,
1296 sum: 0.0,
1297 min: f64::INFINITY,
1298 max: f64::NEG_INFINITY,
1299 }
1300 }
1301 pub fn record(&mut self, val: f64) {
1303 self.count += 1;
1304 self.sum += val;
1305 if val < self.min {
1306 self.min = val;
1307 }
1308 if val > self.max {
1309 self.max = val;
1310 }
1311 }
1312 pub fn mean(&self) -> Option<f64> {
1314 if self.count == 0 {
1315 None
1316 } else {
1317 Some(self.sum / self.count as f64)
1318 }
1319 }
1320 pub fn min(&self) -> Option<f64> {
1322 if self.count == 0 {
1323 None
1324 } else {
1325 Some(self.min)
1326 }
1327 }
1328 pub fn max(&self) -> Option<f64> {
1330 if self.count == 0 {
1331 None
1332 } else {
1333 Some(self.max)
1334 }
1335 }
1336 pub fn count(&self) -> u64 {
1338 self.count
1339 }
1340}
1341#[allow(dead_code)]
1343pub struct WindowIterator<'a, T> {
1344 pub(super) data: &'a [T],
1345 pub(super) pos: usize,
1346 pub(super) window: usize,
1347}
1348#[allow(dead_code)]
1349impl<'a, T> WindowIterator<'a, T> {
1350 pub fn new(data: &'a [T], window: usize) -> Self {
1352 Self {
1353 data,
1354 pos: 0,
1355 window,
1356 }
1357 }
1358}
1359#[allow(dead_code)]
1361pub struct TokenBucket {
1362 capacity: u64,
1363 tokens: u64,
1364 refill_per_ms: u64,
1365 last_refill: std::time::Instant,
1366}
1367#[allow(dead_code)]
1368impl TokenBucket {
1369 pub fn new(capacity: u64, refill_per_ms: u64) -> Self {
1371 Self {
1372 capacity,
1373 tokens: capacity,
1374 refill_per_ms,
1375 last_refill: std::time::Instant::now(),
1376 }
1377 }
1378 pub fn try_consume(&mut self, n: u64) -> bool {
1380 self.refill();
1381 if self.tokens >= n {
1382 self.tokens -= n;
1383 true
1384 } else {
1385 false
1386 }
1387 }
1388 fn refill(&mut self) {
1389 let now = std::time::Instant::now();
1390 let elapsed_ms = now.duration_since(self.last_refill).as_millis() as u64;
1391 if elapsed_ms > 0 {
1392 let new_tokens = elapsed_ms * self.refill_per_ms;
1393 self.tokens = (self.tokens + new_tokens).min(self.capacity);
1394 self.last_refill = now;
1395 }
1396 }
1397 pub fn available(&self) -> u64 {
1399 self.tokens
1400 }
1401 pub fn capacity(&self) -> u64 {
1403 self.capacity
1404 }
1405}
1406#[allow(dead_code)]
1408#[derive(Debug, Clone)]
1409pub struct DetailedTerminationResult {
1410 pub terminates: bool,
1412 pub wf_relation: Option<WfRelationKind>,
1414 pub function_name: Name,
1416 pub explanation: String,
1418 pub recursive_calls: Vec<RecCallInfo>,
1420}
1421impl DetailedTerminationResult {
1422 #[allow(dead_code)]
1424 pub fn non_recursive(name: Name) -> Self {
1425 Self {
1426 terminates: true,
1427 wf_relation: None,
1428 function_name: name,
1429 explanation: "No recursive calls; trivially terminating.".to_string(),
1430 recursive_calls: vec![],
1431 }
1432 }
1433 #[allow(dead_code)]
1435 pub fn success(name: Name, wf: WfRelationKind, calls: Vec<RecCallInfo>) -> Self {
1436 let explanation = format!("Termination verified via {}.", wf.description());
1437 Self {
1438 terminates: true,
1439 wf_relation: Some(wf),
1440 function_name: name,
1441 explanation,
1442 recursive_calls: calls,
1443 }
1444 }
1445 #[allow(dead_code)]
1447 pub fn failure(name: Name, calls: Vec<RecCallInfo>, reason: impl Into<String>) -> Self {
1448 Self {
1449 terminates: false,
1450 wf_relation: None,
1451 function_name: name,
1452 explanation: reason.into(),
1453 recursive_calls: calls,
1454 }
1455 }
1456}
1457#[allow(dead_code)]
1459pub struct Fixture {
1460 data: std::collections::HashMap<String, String>,
1461}
1462#[allow(dead_code)]
1463impl Fixture {
1464 pub fn new() -> Self {
1466 Self {
1467 data: std::collections::HashMap::new(),
1468 }
1469 }
1470 pub fn set(&mut self, key: impl Into<String>, val: impl Into<String>) {
1472 self.data.insert(key.into(), val.into());
1473 }
1474 pub fn get(&self, key: &str) -> Option<&str> {
1476 self.data.get(key).map(|s| s.as_str())
1477 }
1478 pub fn len(&self) -> usize {
1480 self.data.len()
1481 }
1482 pub fn is_empty(&self) -> bool {
1484 self.len() == 0
1485 }
1486}
1487#[allow(dead_code)]
1489pub struct StackCalc {
1490 stack: Vec<i64>,
1491}
1492#[allow(dead_code)]
1493impl StackCalc {
1494 pub fn new() -> Self {
1496 Self { stack: Vec::new() }
1497 }
1498 pub fn push(&mut self, n: i64) {
1500 self.stack.push(n);
1501 }
1502 pub fn add(&mut self) {
1504 let b = self
1505 .stack
1506 .pop()
1507 .expect("stack must have at least two values for add");
1508 let a = self
1509 .stack
1510 .pop()
1511 .expect("stack must have at least two values for add");
1512 self.stack.push(a + b);
1513 }
1514 pub fn sub(&mut self) {
1516 let b = self
1517 .stack
1518 .pop()
1519 .expect("stack must have at least two values for sub");
1520 let a = self
1521 .stack
1522 .pop()
1523 .expect("stack must have at least two values for sub");
1524 self.stack.push(a - b);
1525 }
1526 pub fn mul(&mut self) {
1528 let b = self
1529 .stack
1530 .pop()
1531 .expect("stack must have at least two values for mul");
1532 let a = self
1533 .stack
1534 .pop()
1535 .expect("stack must have at least two values for mul");
1536 self.stack.push(a * b);
1537 }
1538 pub fn peek(&self) -> Option<i64> {
1540 self.stack.last().copied()
1541 }
1542 pub fn depth(&self) -> usize {
1544 self.stack.len()
1545 }
1546}
1547#[allow(dead_code)]
1549pub enum Either2<A, B> {
1550 First(A),
1552 Second(B),
1554}
1555#[allow(dead_code)]
1556impl<A, B> Either2<A, B> {
1557 pub fn is_first(&self) -> bool {
1559 matches!(self, Either2::First(_))
1560 }
1561 pub fn is_second(&self) -> bool {
1563 matches!(self, Either2::Second(_))
1564 }
1565 pub fn first(self) -> Option<A> {
1567 match self {
1568 Either2::First(a) => Some(a),
1569 _ => None,
1570 }
1571 }
1572 pub fn second(self) -> Option<B> {
1574 match self {
1575 Either2::Second(b) => Some(b),
1576 _ => None,
1577 }
1578 }
1579 pub fn map_first<C, F: FnOnce(A) -> C>(self, f: F) -> Either2<C, B> {
1581 match self {
1582 Either2::First(a) => Either2::First(f(a)),
1583 Either2::Second(b) => Either2::Second(b),
1584 }
1585 }
1586}
1587#[allow(dead_code)]
1589#[derive(Debug, Clone, Default)]
1590pub struct NameIndex {
1591 names: Vec<String>,
1592 index: std::collections::HashMap<String, usize>,
1593}
1594impl NameIndex {
1595 #[allow(dead_code)]
1597 pub fn new() -> Self {
1598 Self::default()
1599 }
1600 #[allow(dead_code)]
1603 pub fn insert(&mut self, name: impl Into<String>) -> usize {
1604 let name = name.into();
1605 if let Some(&id) = self.index.get(&name) {
1606 return id;
1607 }
1608 let id = self.names.len();
1609 self.index.insert(name.clone(), id);
1610 self.names.push(name);
1611 id
1612 }
1613 #[allow(dead_code)]
1615 pub fn get_id(&self, name: &str) -> Option<usize> {
1616 self.index.get(name).copied()
1617 }
1618 #[allow(dead_code)]
1620 pub fn get_name(&self, id: usize) -> Option<&str> {
1621 self.names.get(id).map(|s| s.as_str())
1622 }
1623 #[allow(dead_code)]
1625 pub fn len(&self) -> usize {
1626 self.names.len()
1627 }
1628 #[allow(dead_code)]
1630 pub fn is_empty(&self) -> bool {
1631 self.names.is_empty()
1632 }
1633 #[allow(dead_code)]
1635 pub fn all_names(&self) -> &[String] {
1636 &self.names
1637 }
1638}
1639#[allow(dead_code)]
1641pub struct RewriteRuleSet {
1642 rules: Vec<RewriteRule>,
1643}
1644#[allow(dead_code)]
1645impl RewriteRuleSet {
1646 pub fn new() -> Self {
1648 Self { rules: Vec::new() }
1649 }
1650 pub fn add(&mut self, rule: RewriteRule) {
1652 self.rules.push(rule);
1653 }
1654 pub fn len(&self) -> usize {
1656 self.rules.len()
1657 }
1658 pub fn is_empty(&self) -> bool {
1660 self.rules.is_empty()
1661 }
1662 pub fn conditional_rules(&self) -> Vec<&RewriteRule> {
1664 self.rules.iter().filter(|r| r.conditional).collect()
1665 }
1666 pub fn unconditional_rules(&self) -> Vec<&RewriteRule> {
1668 self.rules.iter().filter(|r| !r.conditional).collect()
1669 }
1670 pub fn get(&self, name: &str) -> Option<&RewriteRule> {
1672 self.rules.iter().find(|r| r.name == name)
1673 }
1674}
1675#[allow(dead_code)]
1677#[derive(Debug, Clone, Default)]
1678pub struct TerminationCache {
1679 results: HashMap<Name, bool>,
1680}
1681impl TerminationCache {
1682 #[allow(dead_code)]
1684 pub fn new() -> Self {
1685 Self::default()
1686 }
1687 #[allow(dead_code)]
1689 pub fn mark_terminating(&mut self, name: Name) {
1690 self.results.insert(name, true);
1691 }
1692 #[allow(dead_code)]
1694 pub fn mark_nonterminating(&mut self, name: Name) {
1695 self.results.insert(name, false);
1696 }
1697 #[allow(dead_code)]
1699 pub fn is_known_terminating(&self, name: &Name) -> Option<bool> {
1700 self.results.get(name).copied()
1701 }
1702 #[allow(dead_code)]
1704 pub fn len(&self) -> usize {
1705 self.results.len()
1706 }
1707 #[allow(dead_code)]
1709 pub fn is_empty(&self) -> bool {
1710 self.results.is_empty()
1711 }
1712 #[allow(dead_code)]
1714 pub fn clear(&mut self) {
1715 self.results.clear();
1716 }
1717}
1718#[allow(dead_code)]
1720pub struct FocusStack<T> {
1721 items: Vec<T>,
1722}
1723#[allow(dead_code)]
1724impl<T> FocusStack<T> {
1725 pub fn new() -> Self {
1727 Self { items: Vec::new() }
1728 }
1729 pub fn focus(&mut self, item: T) {
1731 self.items.push(item);
1732 }
1733 pub fn blur(&mut self) -> Option<T> {
1735 self.items.pop()
1736 }
1737 pub fn current(&self) -> Option<&T> {
1739 self.items.last()
1740 }
1741 pub fn depth(&self) -> usize {
1743 self.items.len()
1744 }
1745 pub fn is_empty(&self) -> bool {
1747 self.items.is_empty()
1748 }
1749}