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 earlier: Vec<T>,
215 current: T,
217}
218#[allow(dead_code)]
219impl<T: Clone> VersionedRecord<T> {
220 pub fn new(initial: T) -> Self {
222 Self {
223 earlier: Vec::new(),
224 current: initial,
225 }
226 }
227 pub fn update(&mut self, val: T) {
229 let previous = std::mem::replace(&mut self.current, val);
230 self.earlier.push(previous);
231 }
232 pub fn current(&self) -> &T {
234 &self.current
235 }
236 pub fn at_version(&self, n: usize) -> Option<&T> {
238 match self.earlier.get(n) {
239 Some(value) => Some(value),
240 None if n == self.earlier.len() => Some(&self.current),
241 None => None,
242 }
243 }
244 pub fn version(&self) -> usize {
246 self.earlier.len()
247 }
248 pub fn has_history(&self) -> bool {
250 !self.earlier.is_empty()
251 }
252}
253#[allow(dead_code)]
255pub struct TransitiveClosure {
256 adj: Vec<Vec<usize>>,
257 n: usize,
258}
259#[allow(dead_code)]
260impl TransitiveClosure {
261 pub fn new(n: usize) -> Self {
263 Self {
264 adj: vec![Vec::new(); n],
265 n,
266 }
267 }
268 pub fn add_edge(&mut self, from: usize, to: usize) {
270 if from < self.n {
271 self.adj[from].push(to);
272 }
273 }
274 pub fn reachable_from(&self, start: usize) -> Vec<usize> {
276 let mut visited = vec![false; self.n];
277 let mut queue = std::collections::VecDeque::new();
278 queue.push_back(start);
279 while let Some(node) = queue.pop_front() {
280 if node >= self.n || visited[node] {
281 continue;
282 }
283 visited[node] = true;
284 for &next in &self.adj[node] {
285 queue.push_back(next);
286 }
287 }
288 (0..self.n).filter(|&i| visited[i]).collect()
289 }
290 pub fn can_reach(&self, from: usize, to: usize) -> bool {
292 self.reachable_from(from).contains(&to)
293 }
294}
295#[allow(dead_code)]
297#[allow(missing_docs)]
298pub enum DecisionNode {
299 Leaf(String),
301 Branch {
303 key: String,
304 val: String,
305 yes_branch: Box<DecisionNode>,
306 no_branch: Box<DecisionNode>,
307 },
308}
309#[allow(dead_code)]
310impl DecisionNode {
311 pub fn evaluate(&self, ctx: &std::collections::HashMap<String, String>) -> &str {
313 match self {
314 DecisionNode::Leaf(action) => action.as_str(),
315 DecisionNode::Branch {
316 key,
317 val,
318 yes_branch,
319 no_branch,
320 } => {
321 let actual = ctx.get(key).map(|s| s.as_str()).unwrap_or("");
322 if actual == val.as_str() {
323 yes_branch.evaluate(ctx)
324 } else {
325 no_branch.evaluate(ctx)
326 }
327 }
328 }
329 }
330 pub fn depth(&self) -> usize {
332 match self {
333 DecisionNode::Leaf(_) => 0,
334 DecisionNode::Branch {
335 yes_branch,
336 no_branch,
337 ..
338 } => 1 + yes_branch.depth().max(no_branch.depth()),
339 }
340 }
341}
342#[allow(dead_code)]
344pub struct SparseVec<T: Default + Clone + PartialEq> {
345 entries: std::collections::HashMap<usize, T>,
346 default_: T,
347 logical_len: usize,
348}
349#[allow(dead_code)]
350impl<T: Default + Clone + PartialEq> SparseVec<T> {
351 pub fn new(len: usize) -> Self {
353 Self {
354 entries: std::collections::HashMap::new(),
355 default_: T::default(),
356 logical_len: len,
357 }
358 }
359 pub fn set(&mut self, idx: usize, val: T) {
361 if val == self.default_ {
362 self.entries.remove(&idx);
363 } else {
364 self.entries.insert(idx, val);
365 }
366 }
367 pub fn get(&self, idx: usize) -> &T {
369 self.entries.get(&idx).unwrap_or(&self.default_)
370 }
371 pub fn len(&self) -> usize {
373 self.logical_len
374 }
375 pub fn is_empty(&self) -> bool {
377 self.len() == 0
378 }
379 pub fn nnz(&self) -> usize {
381 self.entries.len()
382 }
383}
384#[allow(dead_code)]
386pub struct ConfigNode {
387 key: String,
388 value: Option<String>,
389 children: Vec<ConfigNode>,
390}
391#[allow(dead_code)]
392impl ConfigNode {
393 pub fn leaf(key: impl Into<String>, value: impl Into<String>) -> Self {
395 Self {
396 key: key.into(),
397 value: Some(value.into()),
398 children: Vec::new(),
399 }
400 }
401 pub fn section(key: impl Into<String>) -> Self {
403 Self {
404 key: key.into(),
405 value: None,
406 children: Vec::new(),
407 }
408 }
409 pub fn add_child(&mut self, child: ConfigNode) {
411 self.children.push(child);
412 }
413 pub fn key(&self) -> &str {
415 &self.key
416 }
417 pub fn value(&self) -> Option<&str> {
419 self.value.as_deref()
420 }
421 pub fn num_children(&self) -> usize {
423 self.children.len()
424 }
425 pub fn lookup(&self, path: &str) -> Option<&str> {
427 let mut parts = path.splitn(2, '.');
428 let head = parts.next()?;
429 let tail = parts.next();
430 if head != self.key {
431 return None;
432 }
433 match tail {
434 None => self.value.as_deref(),
435 Some(rest) => self.children.iter().find_map(|c| c.lookup_relative(rest)),
436 }
437 }
438 fn lookup_relative(&self, path: &str) -> Option<&str> {
439 let mut parts = path.splitn(2, '.');
440 let head = parts.next()?;
441 let tail = parts.next();
442 if head != self.key {
443 return None;
444 }
445 match tail {
446 None => self.value.as_deref(),
447 Some(rest) => self.children.iter().find_map(|c| c.lookup_relative(rest)),
448 }
449 }
450}
451#[allow(dead_code)]
453pub struct SmallMap<K: Ord + Clone, V: Clone> {
454 entries: Vec<(K, V)>,
455}
456#[allow(dead_code)]
457impl<K: Ord + Clone, V: Clone> SmallMap<K, V> {
458 pub fn new() -> Self {
460 Self {
461 entries: Vec::new(),
462 }
463 }
464 pub fn insert(&mut self, key: K, val: V) {
466 match self.entries.binary_search_by_key(&&key, |(k, _)| k) {
467 Ok(i) => self.entries[i].1 = val,
468 Err(i) => self.entries.insert(i, (key, val)),
469 }
470 }
471 pub fn get(&self, key: &K) -> Option<&V> {
473 self.entries
474 .binary_search_by_key(&key, |(k, _)| k)
475 .ok()
476 .map(|i| &self.entries[i].1)
477 }
478 pub fn len(&self) -> usize {
480 self.entries.len()
481 }
482 pub fn is_empty(&self) -> bool {
484 self.entries.is_empty()
485 }
486 pub fn keys(&self) -> Vec<&K> {
488 self.entries.iter().map(|(k, _)| k).collect()
489 }
490 pub fn values(&self) -> Vec<&V> {
492 self.entries.iter().map(|(_, v)| v).collect()
493 }
494}
495#[allow(dead_code)]
497pub struct PathBuf {
498 components: Vec<String>,
499}
500#[allow(dead_code)]
501impl PathBuf {
502 pub fn new() -> Self {
504 Self {
505 components: Vec::new(),
506 }
507 }
508 pub fn push(&mut self, comp: impl Into<String>) {
510 self.components.push(comp.into());
511 }
512 pub fn pop(&mut self) {
514 self.components.pop();
515 }
516 pub fn as_str(&self) -> String {
518 self.components.join("/")
519 }
520 pub fn depth(&self) -> usize {
522 self.components.len()
523 }
524 pub fn clear(&mut self) {
526 self.components.clear();
527 }
528}
529#[derive(Debug, Clone)]
531pub struct ParamInfo {
532 pub name: Name,
534 pub pos: usize,
536 pub inductive_type: Option<Name>,
538}
539#[allow(dead_code)]
541pub struct NonEmptyVec<T> {
542 head: T,
543 tail: Vec<T>,
544}
545#[allow(dead_code)]
546impl<T> NonEmptyVec<T> {
547 pub fn singleton(val: T) -> Self {
549 Self {
550 head: val,
551 tail: Vec::new(),
552 }
553 }
554 pub fn push(&mut self, val: T) {
556 self.tail.push(val);
557 }
558 pub fn first(&self) -> &T {
560 &self.head
561 }
562 pub fn last(&self) -> &T {
564 self.tail.last().unwrap_or(&self.head)
565 }
566 pub fn len(&self) -> usize {
568 1 + self.tail.len()
569 }
570 pub fn is_empty(&self) -> bool {
572 self.len() == 0
573 }
574 pub fn to_vec(&self) -> Vec<&T> {
576 let mut v = vec![&self.head];
577 v.extend(self.tail.iter());
578 v
579 }
580}
581#[allow(dead_code)]
583pub struct WriteOnce<T> {
584 value: std::cell::Cell<Option<T>>,
585}
586#[allow(dead_code)]
587impl<T: Copy> WriteOnce<T> {
588 pub fn new() -> Self {
590 Self {
591 value: std::cell::Cell::new(None),
592 }
593 }
594 pub fn write(&self, val: T) -> bool {
596 if self.value.get().is_some() {
597 return false;
598 }
599 self.value.set(Some(val));
600 true
601 }
602 pub fn read(&self) -> Option<T> {
604 self.value.get()
605 }
606 pub fn is_written(&self) -> bool {
608 self.value.get().is_some()
609 }
610}
611#[allow(dead_code)]
613#[derive(Debug, Clone, PartialEq, Eq)]
614pub enum WfRelationKind {
615 Structural {
617 inductive_type: Name,
619 param_index: usize,
621 },
622 Measure {
624 measure_fn: Name,
626 },
627 Lexicographic {
629 components: Vec<WfRelationKind>,
631 },
632 NatSub,
634 Custom {
636 relation: Name,
638 },
639}
640impl WfRelationKind {
641 #[allow(dead_code)]
643 pub fn is_structural(&self) -> bool {
644 matches!(self, WfRelationKind::Structural { .. })
645 }
646 #[allow(dead_code)]
648 pub fn lex_depth(&self) -> usize {
649 match self {
650 WfRelationKind::Lexicographic { components } => components.len(),
651 _ => 1,
652 }
653 }
654 #[allow(dead_code)]
656 pub fn description(&self) -> String {
657 match self {
658 WfRelationKind::Structural {
659 inductive_type,
660 param_index,
661 } => {
662 format!("structural on {} (param {})", inductive_type, param_index)
663 }
664 WfRelationKind::Measure { measure_fn } => {
665 format!("measure by {}", measure_fn)
666 }
667 WfRelationKind::Lexicographic { components } => {
668 format!("lexicographic ({} components)", components.len())
669 }
670 WfRelationKind::NatSub => "nat subtraction".to_string(),
671 WfRelationKind::Custom { relation } => {
672 format!("custom relation {}", relation)
673 }
674 }
675 }
676}
677#[derive(Debug, Clone)]
679pub struct TerminationResult {
680 pub decreasing_param: Option<usize>,
682 pub recursive_calls: Vec<RecCallInfo>,
684 pub is_terminating: bool,
686}
687#[allow(dead_code)]
689#[derive(Debug, Clone, Default)]
690pub struct StringTrie {
691 pub(super) children: std::collections::HashMap<char, StringTrie>,
692 is_end: bool,
693 pub(super) value: Option<String>,
694}
695impl StringTrie {
696 #[allow(dead_code)]
698 pub fn new() -> Self {
699 Self::default()
700 }
701 #[allow(dead_code)]
703 pub fn insert(&mut self, s: &str) {
704 let mut node = self;
705 for c in s.chars() {
706 node = node.children.entry(c).or_default();
707 }
708 node.is_end = true;
709 node.value = Some(s.to_string());
710 }
711 #[allow(dead_code)]
713 pub fn contains(&self, s: &str) -> bool {
714 let mut node = self;
715 for c in s.chars() {
716 match node.children.get(&c) {
717 Some(next) => node = next,
718 None => return false,
719 }
720 }
721 node.is_end
722 }
723 #[allow(dead_code)]
725 pub fn starts_with(&self, prefix: &str) -> Vec<String> {
726 let mut node = self;
727 for c in prefix.chars() {
728 match node.children.get(&c) {
729 Some(next) => node = next,
730 None => return vec![],
731 }
732 }
733 let mut results = Vec::new();
734 collect_strings(node, &mut results);
735 results
736 }
737 #[allow(dead_code)]
739 pub fn len(&self) -> usize {
740 let mut count = if self.is_end { 1 } else { 0 };
741 for child in self.children.values() {
742 count += child.len();
743 }
744 count
745 }
746 #[allow(dead_code)]
748 pub fn is_empty(&self) -> bool {
749 self.len() == 0
750 }
751}
752#[allow(dead_code)]
754pub struct LabelSet {
755 labels: Vec<String>,
756}
757#[allow(dead_code)]
758impl LabelSet {
759 pub fn new() -> Self {
761 Self { labels: Vec::new() }
762 }
763 pub fn add(&mut self, label: impl Into<String>) {
765 let s = label.into();
766 if !self.labels.contains(&s) {
767 self.labels.push(s);
768 }
769 }
770 pub fn has(&self, label: &str) -> bool {
772 self.labels.iter().any(|l| l == label)
773 }
774 pub fn count(&self) -> usize {
776 self.labels.len()
777 }
778 pub fn all(&self) -> &[String] {
780 &self.labels
781 }
782}
783#[allow(dead_code)]
785pub struct Stopwatch {
786 start: crate::wall_clock::Instant,
787 splits: Vec<f64>,
788}
789#[allow(dead_code)]
790impl Stopwatch {
791 pub fn start() -> Self {
793 Self {
794 start: crate::wall_clock::Instant::now(),
795 splits: Vec::new(),
796 }
797 }
798 pub fn split(&mut self) {
800 self.splits.push(self.elapsed_ms());
801 }
802 pub fn elapsed_ms(&self) -> f64 {
804 self.start.elapsed().as_secs_f64() * 1000.0
805 }
806 pub fn splits(&self) -> &[f64] {
808 &self.splits
809 }
810 pub fn num_splits(&self) -> usize {
812 self.splits.len()
813 }
814}
815#[derive(Debug, Clone)]
817pub struct RecCallInfo {
818 pub callee: Name,
820 pub arg_pos: usize,
822 pub arg: Expr,
824 pub is_decreasing: bool,
826}
827pub struct TerminationChecker {
829 checking: HashSet<Name>,
831 param_info: HashMap<Name, Vec<ParamInfo>>,
833 call_info: HashMap<Name, Vec<RecCallInfo>>,
835 smaller: HashMap<Expr, HashSet<Expr>>,
838}
839impl TerminationChecker {
840 pub fn new() -> Self {
842 Self {
843 checking: HashSet::new(),
844 param_info: HashMap::new(),
845 call_info: HashMap::new(),
846 smaller: HashMap::new(),
847 }
848 }
849 pub fn register_params(&mut self, name: Name, params: Vec<ParamInfo>) {
851 self.param_info.insert(name, params);
852 }
853 pub fn add_smaller(&mut self, big: Expr, small: Expr) {
858 self.smaller.entry(big).or_default().insert(small);
859 }
860 pub fn is_smaller(&self, big: &Expr, small: &Expr) -> bool {
862 if let Some(smalls) = self.smaller.get(big) {
863 if smalls.contains(small) {
864 return true;
865 }
866 for mid in smalls {
867 if self.is_smaller(mid, small) {
868 return true;
869 }
870 }
871 }
872 false
873 }
874 pub fn check_terminates(&mut self, name: &Name, body: &Expr) -> Result<(), String> {
879 if self.checking.contains(name) {
880 return Err(format!("Cyclic dependency detected for {}", name));
881 }
882 self.checking.insert(name.clone());
883 let mut calls = Vec::new();
884 self.collect_recursive_calls(name, body, &mut calls, 0)?;
885 self.call_info.insert(name.clone(), calls.clone());
886 if calls.is_empty() {
887 self.checking.remove(name);
888 return Ok(());
889 }
890 let result = self.find_decreasing_param(name, &calls);
891 self.checking.remove(name);
892 if result.is_terminating {
893 Ok(())
894 } else {
895 Err(format!(
896 "Cannot verify termination of '{}': no structurally decreasing argument found",
897 name
898 ))
899 }
900 }
901 pub fn check_mutual_terminates(
903 &mut self,
904 names: &[Name],
905 bodies: &[Expr],
906 ) -> Result<(), String> {
907 if names.len() != bodies.len() {
908 return Err("Mismatched names and bodies in mutual recursion".to_string());
909 }
910 for name in names {
911 self.checking.insert(name.clone());
912 }
913 for (name, body) in names.iter().zip(bodies.iter()) {
914 let mut calls = Vec::new();
915 self.collect_recursive_calls_mutual(names, body, &mut calls, 0)?;
916 self.call_info.insert(name.clone(), calls);
917 }
918 for name in names {
919 if let Some(calls) = self.call_info.get(name) {
920 if !calls.is_empty() {
921 let result = self.find_decreasing_param(name, calls);
922 if !result.is_terminating {
923 for n in names {
924 self.checking.remove(n);
925 }
926 return Err(format!(
927 "Cannot verify termination of '{}' in mutual recursion block",
928 name
929 ));
930 }
931 }
932 }
933 }
934 for name in names {
935 self.checking.remove(name);
936 }
937 Ok(())
938 }
939 fn collect_recursive_calls(
941 &self,
942 fname: &Name,
943 expr: &Expr,
944 calls: &mut Vec<RecCallInfo>,
945 depth: usize,
946 ) -> Result<(), String> {
947 if depth > 200 {
948 return Err("Definition too deeply nested".to_string());
949 }
950 match expr {
951 Expr::App(f, a) => {
952 if let Some(call) = self.check_recursive_call(fname, expr) {
953 calls.push(call);
954 }
955 self.collect_recursive_calls(fname, f, calls, depth + 1)?;
956 self.collect_recursive_calls(fname, a, calls, depth + 1)
957 }
958 Expr::Lam(_, _, ty, body) => {
959 self.collect_recursive_calls(fname, ty, calls, depth + 1)?;
960 self.collect_recursive_calls(fname, body, calls, depth + 1)
961 }
962 Expr::Pi(_, _, ty, body) => {
963 self.collect_recursive_calls(fname, ty, calls, depth + 1)?;
964 self.collect_recursive_calls(fname, body, calls, depth + 1)
965 }
966 Expr::Let(_, ty, val, body) => {
967 self.collect_recursive_calls(fname, ty, calls, depth + 1)?;
968 self.collect_recursive_calls(fname, val, calls, depth + 1)?;
969 self.collect_recursive_calls(fname, body, calls, depth + 1)
970 }
971 _ => Ok(()),
972 }
973 }
974 fn collect_recursive_calls_mutual(
976 &self,
977 fnames: &[Name],
978 expr: &Expr,
979 calls: &mut Vec<RecCallInfo>,
980 depth: usize,
981 ) -> Result<(), String> {
982 if depth > 200 {
983 return Err("Definition too deeply nested".to_string());
984 }
985 match expr {
986 Expr::App(f, a) => {
987 for fname in fnames {
988 if let Some(call) = self.check_recursive_call(fname, expr) {
989 calls.push(call);
990 }
991 }
992 self.collect_recursive_calls_mutual(fnames, f, calls, depth + 1)?;
993 self.collect_recursive_calls_mutual(fnames, a, calls, depth + 1)
994 }
995 Expr::Lam(_, _, ty, body) => {
996 self.collect_recursive_calls_mutual(fnames, ty, calls, depth + 1)?;
997 self.collect_recursive_calls_mutual(fnames, body, calls, depth + 1)
998 }
999 Expr::Pi(_, _, ty, body) => {
1000 self.collect_recursive_calls_mutual(fnames, ty, calls, depth + 1)?;
1001 self.collect_recursive_calls_mutual(fnames, body, calls, depth + 1)
1002 }
1003 Expr::Let(_, ty, val, body) => {
1004 self.collect_recursive_calls_mutual(fnames, ty, calls, depth + 1)?;
1005 self.collect_recursive_calls_mutual(fnames, val, calls, depth + 1)?;
1006 self.collect_recursive_calls_mutual(fnames, body, calls, depth + 1)
1007 }
1008 _ => Ok(()),
1009 }
1010 }
1011 fn check_recursive_call(&self, fname: &Name, app: &Expr) -> Option<RecCallInfo> {
1013 let (head, args) = collect_app_args(app);
1014 if let Expr::Const(name, _) = head {
1015 if name == fname {
1016 for (i, arg) in args.iter().enumerate() {
1017 let is_dec = self.is_structurally_smaller(arg);
1018 if is_dec {
1019 return Some(RecCallInfo {
1020 callee: name.clone(),
1021 arg_pos: i,
1022 arg: (*arg).clone(),
1023 is_decreasing: true,
1024 });
1025 }
1026 }
1027 if let Some(first_arg) = args.first() {
1028 return Some(RecCallInfo {
1029 callee: name.clone(),
1030 arg_pos: 0,
1031 arg: (*first_arg).clone(),
1032 is_decreasing: false,
1033 });
1034 }
1035 }
1036 }
1037 None
1038 }
1039 fn is_structurally_smaller(&self, expr: &Expr) -> bool {
1041 for smalls in self.smaller.values() {
1042 if smalls.contains(expr) {
1043 return true;
1044 }
1045 }
1046 false
1047 }
1048 fn find_decreasing_param(&self, _name: &Name, calls: &[RecCallInfo]) -> TerminationResult {
1050 if calls.is_empty() {
1051 return TerminationResult {
1052 decreasing_param: None,
1053 recursive_calls: calls.to_vec(),
1054 is_terminating: true,
1055 };
1056 }
1057 let max_pos = calls.iter().map(|c| c.arg_pos).max().unwrap_or(0);
1058 for pos in 0..=max_pos {
1059 let all_decreasing = calls.iter().all(|c| {
1060 if c.arg_pos == pos {
1061 c.is_decreasing
1062 } else {
1063 true
1064 }
1065 });
1066 if all_decreasing && calls.iter().any(|c| c.arg_pos == pos && c.is_decreasing) {
1067 return TerminationResult {
1068 decreasing_param: Some(pos),
1069 recursive_calls: calls.to_vec(),
1070 is_terminating: true,
1071 };
1072 }
1073 }
1074 let all_dec = calls.iter().all(|c| c.is_decreasing);
1075 TerminationResult {
1076 decreasing_param: None,
1077 recursive_calls: calls.to_vec(),
1078 is_terminating: all_dec,
1079 }
1080 }
1081 pub fn get_calls(&self, name: &Name) -> Option<&Vec<RecCallInfo>> {
1083 self.call_info.get(name)
1084 }
1085}
1086#[allow(dead_code)]
1088#[allow(missing_docs)]
1089pub struct RewriteRule {
1090 pub name: String,
1092 pub lhs: String,
1094 pub rhs: String,
1096 pub conditional: bool,
1098}
1099#[allow(dead_code)]
1100impl RewriteRule {
1101 pub fn unconditional(
1103 name: impl Into<String>,
1104 lhs: impl Into<String>,
1105 rhs: impl Into<String>,
1106 ) -> Self {
1107 Self {
1108 name: name.into(),
1109 lhs: lhs.into(),
1110 rhs: rhs.into(),
1111 conditional: false,
1112 }
1113 }
1114 pub fn conditional(
1116 name: impl Into<String>,
1117 lhs: impl Into<String>,
1118 rhs: impl Into<String>,
1119 ) -> Self {
1120 Self {
1121 name: name.into(),
1122 lhs: lhs.into(),
1123 rhs: rhs.into(),
1124 conditional: true,
1125 }
1126 }
1127 pub fn display(&self) -> String {
1129 format!("{}: {} → {}", self.name, self.lhs, self.rhs)
1130 }
1131}
1132#[allow(dead_code)]
1134pub struct RawFnPtr {
1135 ptr: usize,
1137 arity: usize,
1138 name: String,
1139}
1140#[allow(dead_code)]
1141impl RawFnPtr {
1142 pub fn new(ptr: usize, arity: usize, name: impl Into<String>) -> Self {
1144 Self {
1145 ptr,
1146 arity,
1147 name: name.into(),
1148 }
1149 }
1150 pub fn arity(&self) -> usize {
1152 self.arity
1153 }
1154 pub fn name(&self) -> &str {
1156 &self.name
1157 }
1158 pub fn raw(&self) -> usize {
1160 self.ptr
1161 }
1162}
1163#[allow(dead_code)]
1165pub struct TransformStat {
1166 before: StatSummary,
1167 after: StatSummary,
1168}
1169#[allow(dead_code)]
1170impl TransformStat {
1171 pub fn new() -> Self {
1173 Self {
1174 before: StatSummary::new(),
1175 after: StatSummary::new(),
1176 }
1177 }
1178 pub fn record_before(&mut self, v: f64) {
1180 self.before.record(v);
1181 }
1182 pub fn record_after(&mut self, v: f64) {
1184 self.after.record(v);
1185 }
1186 pub fn mean_ratio(&self) -> Option<f64> {
1188 let b = self.before.mean()?;
1189 let a = self.after.mean()?;
1190 if b.abs() < f64::EPSILON {
1191 return None;
1192 }
1193 Some(a / b)
1194 }
1195}
1196#[allow(dead_code)]
1198pub struct FlatSubstitution {
1199 pairs: Vec<(String, String)>,
1200}
1201#[allow(dead_code)]
1202impl FlatSubstitution {
1203 pub fn new() -> Self {
1205 Self { pairs: Vec::new() }
1206 }
1207 pub fn add(&mut self, from: impl Into<String>, to: impl Into<String>) {
1209 self.pairs.push((from.into(), to.into()));
1210 }
1211 pub fn apply(&self, s: &str) -> String {
1213 let mut result = s.to_string();
1214 for (from, to) in &self.pairs {
1215 result = result.replace(from.as_str(), to.as_str());
1216 }
1217 result
1218 }
1219 pub fn len(&self) -> usize {
1221 self.pairs.len()
1222 }
1223 pub fn is_empty(&self) -> bool {
1225 self.pairs.is_empty()
1226 }
1227}
1228#[allow(dead_code)]
1230pub struct StringPool {
1231 free: Vec<String>,
1232}
1233#[allow(dead_code)]
1234impl StringPool {
1235 pub fn new() -> Self {
1237 Self { free: Vec::new() }
1238 }
1239 pub fn take(&mut self) -> String {
1241 self.free.pop().unwrap_or_default()
1242 }
1243 pub fn give(&mut self, mut s: String) {
1245 s.clear();
1246 self.free.push(s);
1247 }
1248 pub fn free_count(&self) -> usize {
1250 self.free.len()
1251 }
1252}
1253#[allow(dead_code)]
1255pub struct PrefixCounter {
1256 children: std::collections::HashMap<char, PrefixCounter>,
1257 count: usize,
1258}
1259#[allow(dead_code)]
1260impl PrefixCounter {
1261 pub fn new() -> Self {
1263 Self {
1264 children: std::collections::HashMap::new(),
1265 count: 0,
1266 }
1267 }
1268 pub fn record(&mut self, s: &str) {
1270 self.count += 1;
1271 let mut node = self;
1272 for c in s.chars() {
1273 node = node.children.entry(c).or_default();
1274 node.count += 1;
1275 }
1276 }
1277 pub fn count_with_prefix(&self, prefix: &str) -> usize {
1279 let mut node = self;
1280 for c in prefix.chars() {
1281 match node.children.get(&c) {
1282 Some(n) => node = n,
1283 None => return 0,
1284 }
1285 }
1286 node.count
1287 }
1288}
1289#[allow(dead_code)]
1291pub struct StatSummary {
1292 count: u64,
1293 sum: f64,
1294 min: f64,
1295 max: f64,
1296}
1297#[allow(dead_code)]
1298impl StatSummary {
1299 pub fn new() -> Self {
1301 Self {
1302 count: 0,
1303 sum: 0.0,
1304 min: f64::INFINITY,
1305 max: f64::NEG_INFINITY,
1306 }
1307 }
1308 pub fn record(&mut self, val: f64) {
1310 self.count += 1;
1311 self.sum += val;
1312 if val < self.min {
1313 self.min = val;
1314 }
1315 if val > self.max {
1316 self.max = val;
1317 }
1318 }
1319 pub fn mean(&self) -> Option<f64> {
1321 if self.count == 0 {
1322 None
1323 } else {
1324 Some(self.sum / self.count as f64)
1325 }
1326 }
1327 pub fn min(&self) -> Option<f64> {
1329 if self.count == 0 {
1330 None
1331 } else {
1332 Some(self.min)
1333 }
1334 }
1335 pub fn max(&self) -> Option<f64> {
1337 if self.count == 0 {
1338 None
1339 } else {
1340 Some(self.max)
1341 }
1342 }
1343 pub fn count(&self) -> u64 {
1345 self.count
1346 }
1347}
1348#[allow(dead_code)]
1350pub struct WindowIterator<'a, T> {
1351 pub(super) data: &'a [T],
1352 pub(super) pos: usize,
1353 pub(super) window: usize,
1354}
1355#[allow(dead_code)]
1356impl<'a, T> WindowIterator<'a, T> {
1357 pub fn new(data: &'a [T], window: usize) -> Self {
1359 Self {
1360 data,
1361 pos: 0,
1362 window,
1363 }
1364 }
1365}
1366#[allow(dead_code)]
1368pub struct TokenBucket {
1369 capacity: u64,
1370 tokens: u64,
1371 refill_per_ms: u64,
1372 last_refill: crate::wall_clock::Instant,
1373}
1374#[allow(dead_code)]
1375impl TokenBucket {
1376 pub fn new(capacity: u64, refill_per_ms: u64) -> Self {
1378 Self {
1379 capacity,
1380 tokens: capacity,
1381 refill_per_ms,
1382 last_refill: crate::wall_clock::Instant::now(),
1383 }
1384 }
1385 pub fn try_consume(&mut self, n: u64) -> bool {
1387 self.refill();
1388 if self.tokens >= n {
1389 self.tokens -= n;
1390 true
1391 } else {
1392 false
1393 }
1394 }
1395 fn refill(&mut self) {
1396 let now = crate::wall_clock::Instant::now();
1397 let elapsed_ms = now.duration_since(self.last_refill).as_millis() as u64;
1398 if elapsed_ms > 0 {
1399 let new_tokens = elapsed_ms * self.refill_per_ms;
1400 self.tokens = (self.tokens + new_tokens).min(self.capacity);
1401 self.last_refill = now;
1402 }
1403 }
1404 pub fn available(&self) -> u64 {
1406 self.tokens
1407 }
1408 pub fn capacity(&self) -> u64 {
1410 self.capacity
1411 }
1412}
1413#[allow(dead_code)]
1415#[derive(Debug, Clone)]
1416pub struct DetailedTerminationResult {
1417 pub terminates: bool,
1419 pub wf_relation: Option<WfRelationKind>,
1421 pub function_name: Name,
1423 pub explanation: String,
1425 pub recursive_calls: Vec<RecCallInfo>,
1427}
1428impl DetailedTerminationResult {
1429 #[allow(dead_code)]
1431 pub fn non_recursive(name: Name) -> Self {
1432 Self {
1433 terminates: true,
1434 wf_relation: None,
1435 function_name: name,
1436 explanation: "No recursive calls; trivially terminating.".to_string(),
1437 recursive_calls: vec![],
1438 }
1439 }
1440 #[allow(dead_code)]
1442 pub fn success(name: Name, wf: WfRelationKind, calls: Vec<RecCallInfo>) -> Self {
1443 let explanation = format!("Termination verified via {}.", wf.description());
1444 Self {
1445 terminates: true,
1446 wf_relation: Some(wf),
1447 function_name: name,
1448 explanation,
1449 recursive_calls: calls,
1450 }
1451 }
1452 #[allow(dead_code)]
1454 pub fn failure(name: Name, calls: Vec<RecCallInfo>, reason: impl Into<String>) -> Self {
1455 Self {
1456 terminates: false,
1457 wf_relation: None,
1458 function_name: name,
1459 explanation: reason.into(),
1460 recursive_calls: calls,
1461 }
1462 }
1463}
1464#[allow(dead_code)]
1466pub struct Fixture {
1467 data: std::collections::HashMap<String, String>,
1468}
1469#[allow(dead_code)]
1470impl Fixture {
1471 pub fn new() -> Self {
1473 Self {
1474 data: std::collections::HashMap::new(),
1475 }
1476 }
1477 pub fn set(&mut self, key: impl Into<String>, val: impl Into<String>) {
1479 self.data.insert(key.into(), val.into());
1480 }
1481 pub fn get(&self, key: &str) -> Option<&str> {
1483 self.data.get(key).map(|s| s.as_str())
1484 }
1485 pub fn len(&self) -> usize {
1487 self.data.len()
1488 }
1489 pub fn is_empty(&self) -> bool {
1491 self.len() == 0
1492 }
1493}
1494#[allow(dead_code)]
1496pub struct StackCalc {
1497 stack: Vec<i64>,
1498}
1499#[allow(dead_code)]
1500impl StackCalc {
1501 pub fn new() -> Self {
1503 Self { stack: Vec::new() }
1504 }
1505 pub fn push(&mut self, n: i64) {
1507 self.stack.push(n);
1508 }
1509 fn apply_binary(&mut self, op: impl FnOnce(i64, i64) -> i64) -> Option<i64> {
1513 let (rest_len, a, b) = match self.stack[..] {
1514 [ref rest @ .., a, b] => (rest.len(), a, b),
1515 _ => return None,
1516 };
1517 let value = op(a, b);
1518 self.stack.truncate(rest_len);
1519 self.stack.push(value);
1520 Some(value)
1521 }
1522 pub fn add(&mut self) -> Option<i64> {
1526 self.apply_binary(|a, b| a + b)
1527 }
1528 pub fn sub(&mut self) -> Option<i64> {
1532 self.apply_binary(|a, b| a - b)
1533 }
1534 pub fn mul(&mut self) -> Option<i64> {
1538 self.apply_binary(|a, b| a * b)
1539 }
1540 pub fn peek(&self) -> Option<i64> {
1542 self.stack.last().copied()
1543 }
1544 pub fn depth(&self) -> usize {
1546 self.stack.len()
1547 }
1548}
1549#[allow(dead_code)]
1551pub enum Either2<A, B> {
1552 First(A),
1554 Second(B),
1556}
1557#[allow(dead_code)]
1558impl<A, B> Either2<A, B> {
1559 pub fn is_first(&self) -> bool {
1561 matches!(self, Either2::First(_))
1562 }
1563 pub fn is_second(&self) -> bool {
1565 matches!(self, Either2::Second(_))
1566 }
1567 pub fn first(self) -> Option<A> {
1569 match self {
1570 Either2::First(a) => Some(a),
1571 _ => None,
1572 }
1573 }
1574 pub fn second(self) -> Option<B> {
1576 match self {
1577 Either2::Second(b) => Some(b),
1578 _ => None,
1579 }
1580 }
1581 pub fn map_first<C, F: FnOnce(A) -> C>(self, f: F) -> Either2<C, B> {
1583 match self {
1584 Either2::First(a) => Either2::First(f(a)),
1585 Either2::Second(b) => Either2::Second(b),
1586 }
1587 }
1588}
1589#[allow(dead_code)]
1591#[derive(Debug, Clone, Default)]
1592pub struct NameIndex {
1593 names: Vec<String>,
1594 index: std::collections::HashMap<String, usize>,
1595}
1596impl NameIndex {
1597 #[allow(dead_code)]
1599 pub fn new() -> Self {
1600 Self::default()
1601 }
1602 #[allow(dead_code)]
1605 pub fn insert(&mut self, name: impl Into<String>) -> usize {
1606 let name = name.into();
1607 if let Some(&id) = self.index.get(&name) {
1608 return id;
1609 }
1610 let id = self.names.len();
1611 self.index.insert(name.clone(), id);
1612 self.names.push(name);
1613 id
1614 }
1615 #[allow(dead_code)]
1617 pub fn get_id(&self, name: &str) -> Option<usize> {
1618 self.index.get(name).copied()
1619 }
1620 #[allow(dead_code)]
1622 pub fn get_name(&self, id: usize) -> Option<&str> {
1623 self.names.get(id).map(|s| s.as_str())
1624 }
1625 #[allow(dead_code)]
1627 pub fn len(&self) -> usize {
1628 self.names.len()
1629 }
1630 #[allow(dead_code)]
1632 pub fn is_empty(&self) -> bool {
1633 self.names.is_empty()
1634 }
1635 #[allow(dead_code)]
1637 pub fn all_names(&self) -> &[String] {
1638 &self.names
1639 }
1640}
1641#[allow(dead_code)]
1643pub struct RewriteRuleSet {
1644 rules: Vec<RewriteRule>,
1645}
1646#[allow(dead_code)]
1647impl RewriteRuleSet {
1648 pub fn new() -> Self {
1650 Self { rules: Vec::new() }
1651 }
1652 pub fn add(&mut self, rule: RewriteRule) {
1654 self.rules.push(rule);
1655 }
1656 pub fn len(&self) -> usize {
1658 self.rules.len()
1659 }
1660 pub fn is_empty(&self) -> bool {
1662 self.rules.is_empty()
1663 }
1664 pub fn conditional_rules(&self) -> Vec<&RewriteRule> {
1666 self.rules.iter().filter(|r| r.conditional).collect()
1667 }
1668 pub fn unconditional_rules(&self) -> Vec<&RewriteRule> {
1670 self.rules.iter().filter(|r| !r.conditional).collect()
1671 }
1672 pub fn get(&self, name: &str) -> Option<&RewriteRule> {
1674 self.rules.iter().find(|r| r.name == name)
1675 }
1676}
1677#[allow(dead_code)]
1679#[derive(Debug, Clone, Default)]
1680pub struct TerminationCache {
1681 results: HashMap<Name, bool>,
1682}
1683impl TerminationCache {
1684 #[allow(dead_code)]
1686 pub fn new() -> Self {
1687 Self::default()
1688 }
1689 #[allow(dead_code)]
1691 pub fn mark_terminating(&mut self, name: Name) {
1692 self.results.insert(name, true);
1693 }
1694 #[allow(dead_code)]
1696 pub fn mark_nonterminating(&mut self, name: Name) {
1697 self.results.insert(name, false);
1698 }
1699 #[allow(dead_code)]
1701 pub fn is_known_terminating(&self, name: &Name) -> Option<bool> {
1702 self.results.get(name).copied()
1703 }
1704 #[allow(dead_code)]
1706 pub fn len(&self) -> usize {
1707 self.results.len()
1708 }
1709 #[allow(dead_code)]
1711 pub fn is_empty(&self) -> bool {
1712 self.results.is_empty()
1713 }
1714 #[allow(dead_code)]
1716 pub fn clear(&mut self) {
1717 self.results.clear();
1718 }
1719}
1720#[allow(dead_code)]
1722pub struct FocusStack<T> {
1723 items: Vec<T>,
1724}
1725#[allow(dead_code)]
1726impl<T> FocusStack<T> {
1727 pub fn new() -> Self {
1729 Self { items: Vec::new() }
1730 }
1731 pub fn focus(&mut self, item: T) {
1733 self.items.push(item);
1734 }
1735 pub fn blur(&mut self) -> Option<T> {
1737 self.items.pop()
1738 }
1739 pub fn current(&self) -> Option<&T> {
1741 self.items.last()
1742 }
1743 pub fn depth(&self) -> usize {
1745 self.items.len()
1746 }
1747 pub fn is_empty(&self) -> bool {
1749 self.items.is_empty()
1750 }
1751}