1use crate::level::{self, LevelMVarId};
6use crate::{Level, Name};
7use std::collections::{HashMap, HashSet};
8
9use super::functions::{add_succs, collect_nf_comps, format_level, substitute_level_param};
10
11#[allow(dead_code)]
13#[allow(missing_docs)]
14pub struct RewriteRule {
15 pub name: String,
17 pub lhs: String,
19 pub rhs: String,
21 pub conditional: bool,
23}
24#[allow(dead_code)]
25impl RewriteRule {
26 pub fn unconditional(
28 name: impl Into<String>,
29 lhs: impl Into<String>,
30 rhs: impl Into<String>,
31 ) -> Self {
32 Self {
33 name: name.into(),
34 lhs: lhs.into(),
35 rhs: rhs.into(),
36 conditional: false,
37 }
38 }
39 pub fn conditional(
41 name: impl Into<String>,
42 lhs: impl Into<String>,
43 rhs: impl Into<String>,
44 ) -> Self {
45 Self {
46 name: name.into(),
47 lhs: lhs.into(),
48 rhs: rhs.into(),
49 conditional: true,
50 }
51 }
52 pub fn display(&self) -> String {
54 format!("{}: {} → {}", self.name, self.lhs, self.rhs)
55 }
56}
57#[derive(Debug, Clone, Default)]
59pub struct UnivSatChecker {
60 lower_bounds: std::collections::HashMap<Name, u32>,
61 upper_bounds: std::collections::HashMap<Name, u32>,
62 unsatisfiable: bool,
63}
64impl UnivSatChecker {
65 pub fn new() -> Self {
67 Self::default()
68 }
69 pub fn add_lower_bound(&mut self, param: Name, n: u32) {
71 let entry = self.lower_bounds.entry(param.clone()).or_insert(0);
72 *entry = (*entry).max(n);
73 if let Some(ub) = self.upper_bounds.get(¶m) {
74 if *entry > *ub {
75 self.unsatisfiable = true;
76 }
77 }
78 }
79 pub fn add_upper_bound(&mut self, param: Name, n: u32) {
81 let entry = self.upper_bounds.entry(param.clone()).or_insert(u32::MAX);
82 *entry = (*entry).min(n);
83 if let Some(lb) = self.lower_bounds.get(¶m) {
84 if *lb > *entry {
85 self.unsatisfiable = true;
86 }
87 }
88 }
89 pub fn is_satisfiable(&self) -> bool {
91 !self.unsatisfiable
92 }
93 pub fn get_assignment(&self) -> Option<std::collections::HashMap<Name, u32>> {
95 if self.unsatisfiable {
96 return None;
97 }
98 let mut m = std::collections::HashMap::new();
99 for (p, lb) in &self.lower_bounds {
100 m.insert(p.clone(), *lb);
101 }
102 for p in self.upper_bounds.keys() {
103 m.entry(p.clone()).or_insert(0);
104 }
105 Some(m)
106 }
107}
108#[derive(Debug, Clone, PartialEq, Eq, Hash)]
110pub enum UnivConstraint {
111 Lt(Level, Level),
113 Le(Level, Level),
115 Eq(Level, Level),
117}
118#[allow(dead_code)]
120pub struct VersionedRecord<T: Clone> {
121 history: Vec<T>,
122}
123#[allow(dead_code)]
124impl<T: Clone> VersionedRecord<T> {
125 pub fn new(initial: T) -> Self {
127 Self {
128 history: vec![initial],
129 }
130 }
131 pub fn update(&mut self, val: T) {
133 self.history.push(val);
134 }
135 pub fn current(&self) -> &T {
137 self.history
138 .last()
139 .expect("VersionedRecord history is always non-empty after construction")
140 }
141 pub fn at_version(&self, n: usize) -> Option<&T> {
143 self.history.get(n)
144 }
145 pub fn version(&self) -> usize {
147 self.history.len() - 1
148 }
149 pub fn has_history(&self) -> bool {
151 self.history.len() > 1
152 }
153}
154#[allow(dead_code)]
156pub struct WindowIterator<'a, T> {
157 pub(super) data: &'a [T],
158 pub(super) pos: usize,
159 pub(super) window: usize,
160}
161#[allow(dead_code)]
162impl<'a, T> WindowIterator<'a, T> {
163 pub fn new(data: &'a [T], window: usize) -> Self {
165 Self {
166 data,
167 pos: 0,
168 window,
169 }
170 }
171}
172#[allow(dead_code)]
174pub struct SmallMap<K: Ord + Clone, V: Clone> {
175 entries: Vec<(K, V)>,
176}
177#[allow(dead_code)]
178impl<K: Ord + Clone, V: Clone> SmallMap<K, V> {
179 pub fn new() -> Self {
181 Self {
182 entries: Vec::new(),
183 }
184 }
185 pub fn insert(&mut self, key: K, val: V) {
187 match self.entries.binary_search_by_key(&&key, |(k, _)| k) {
188 Ok(i) => self.entries[i].1 = val,
189 Err(i) => self.entries.insert(i, (key, val)),
190 }
191 }
192 pub fn get(&self, key: &K) -> Option<&V> {
194 self.entries
195 .binary_search_by_key(&key, |(k, _)| k)
196 .ok()
197 .map(|i| &self.entries[i].1)
198 }
199 pub fn len(&self) -> usize {
201 self.entries.len()
202 }
203 pub fn is_empty(&self) -> bool {
205 self.entries.is_empty()
206 }
207 pub fn keys(&self) -> Vec<&K> {
209 self.entries.iter().map(|(k, _)| k).collect()
210 }
211 pub fn values(&self) -> Vec<&V> {
213 self.entries.iter().map(|(_, v)| v).collect()
214 }
215}
216#[allow(dead_code)]
218pub struct RewriteRuleSet {
219 rules: Vec<RewriteRule>,
220}
221#[allow(dead_code)]
222impl RewriteRuleSet {
223 pub fn new() -> Self {
225 Self { rules: Vec::new() }
226 }
227 pub fn add(&mut self, rule: RewriteRule) {
229 self.rules.push(rule);
230 }
231 pub fn len(&self) -> usize {
233 self.rules.len()
234 }
235 pub fn is_empty(&self) -> bool {
237 self.rules.is_empty()
238 }
239 pub fn conditional_rules(&self) -> Vec<&RewriteRule> {
241 self.rules.iter().filter(|r| r.conditional).collect()
242 }
243 pub fn unconditional_rules(&self) -> Vec<&RewriteRule> {
245 self.rules.iter().filter(|r| !r.conditional).collect()
246 }
247 pub fn get(&self, name: &str) -> Option<&RewriteRule> {
249 self.rules.iter().find(|r| r.name == name)
250 }
251}
252#[derive(Debug, Clone, Default)]
256pub struct LevelComparisonTable {
257 levels: Vec<Level>,
258 geq_cache: std::collections::HashMap<(usize, usize), bool>,
260}
261impl LevelComparisonTable {
262 pub fn new(levels: Vec<Level>) -> Self {
264 let mut table = Self {
265 levels,
266 geq_cache: Default::default(),
267 };
268 table.precompute();
269 table
270 }
271 fn precompute(&mut self) {
272 let checker = UnivChecker::new();
273 let n = self.levels.len();
274 for i in 0..n {
275 for j in 0..n {
276 let result = checker.is_geq(&self.levels[i].clone(), &self.levels[j].clone());
277 self.geq_cache.insert((i, j), result);
278 }
279 }
280 }
281 pub fn geq(&self, i: usize, j: usize) -> Option<bool> {
283 self.geq_cache.get(&(i, j)).copied()
284 }
285 pub fn max_idx(&self) -> Option<usize> {
287 (0..self.levels.len()).max_by(|&i, &j| {
288 let checker = UnivChecker::new();
289 if checker.is_geq(&self.levels[i], &self.levels[j]) {
290 std::cmp::Ordering::Greater
291 } else {
292 std::cmp::Ordering::Less
293 }
294 })
295 }
296 pub fn len(&self) -> usize {
298 self.levels.len()
299 }
300 pub fn is_empty(&self) -> bool {
302 self.levels.is_empty()
303 }
304}
305#[allow(dead_code)]
307pub enum Either2<A, B> {
308 First(A),
310 Second(B),
312}
313#[allow(dead_code)]
314impl<A, B> Either2<A, B> {
315 pub fn is_first(&self) -> bool {
317 matches!(self, Either2::First(_))
318 }
319 pub fn is_second(&self) -> bool {
321 matches!(self, Either2::Second(_))
322 }
323 pub fn first(self) -> Option<A> {
325 match self {
326 Either2::First(a) => Some(a),
327 _ => None,
328 }
329 }
330 pub fn second(self) -> Option<B> {
332 match self {
333 Either2::Second(b) => Some(b),
334 _ => None,
335 }
336 }
337 pub fn map_first<C, F: FnOnce(A) -> C>(self, f: F) -> Either2<C, B> {
339 match self {
340 Either2::First(a) => Either2::First(f(a)),
341 Either2::Second(b) => Either2::Second(b),
342 }
343 }
344}
345#[allow(dead_code)]
347pub struct WriteOnce<T> {
348 value: std::cell::Cell<Option<T>>,
349}
350#[allow(dead_code)]
351impl<T: Copy> WriteOnce<T> {
352 pub fn new() -> Self {
354 Self {
355 value: std::cell::Cell::new(None),
356 }
357 }
358 pub fn write(&self, val: T) -> bool {
360 if self.value.get().is_some() {
361 return false;
362 }
363 self.value.set(Some(val));
364 true
365 }
366 pub fn read(&self) -> Option<T> {
368 self.value.get()
369 }
370 pub fn is_written(&self) -> bool {
372 self.value.get().is_some()
373 }
374}
375#[allow(dead_code)]
377pub struct TransformStat {
378 before: StatSummary,
379 after: StatSummary,
380}
381#[allow(dead_code)]
382impl TransformStat {
383 pub fn new() -> Self {
385 Self {
386 before: StatSummary::new(),
387 after: StatSummary::new(),
388 }
389 }
390 pub fn record_before(&mut self, v: f64) {
392 self.before.record(v);
393 }
394 pub fn record_after(&mut self, v: f64) {
396 self.after.record(v);
397 }
398 pub fn mean_ratio(&self) -> Option<f64> {
400 let b = self.before.mean()?;
401 let a = self.after.mean()?;
402 if b.abs() < f64::EPSILON {
403 return None;
404 }
405 Some(a / b)
406 }
407}
408#[allow(dead_code)]
410pub struct TokenBucket {
411 capacity: u64,
412 tokens: u64,
413 refill_per_ms: u64,
414 last_refill: std::time::Instant,
415}
416#[allow(dead_code)]
417impl TokenBucket {
418 pub fn new(capacity: u64, refill_per_ms: u64) -> Self {
420 Self {
421 capacity,
422 tokens: capacity,
423 refill_per_ms,
424 last_refill: std::time::Instant::now(),
425 }
426 }
427 pub fn try_consume(&mut self, n: u64) -> bool {
429 self.refill();
430 if self.tokens >= n {
431 self.tokens -= n;
432 true
433 } else {
434 false
435 }
436 }
437 fn refill(&mut self) {
438 let now = std::time::Instant::now();
439 let elapsed_ms = now.duration_since(self.last_refill).as_millis() as u64;
440 if elapsed_ms > 0 {
441 let new_tokens = elapsed_ms * self.refill_per_ms;
442 self.tokens = (self.tokens + new_tokens).min(self.capacity);
443 self.last_refill = now;
444 }
445 }
446 pub fn available(&self) -> u64 {
448 self.tokens
449 }
450 pub fn capacity(&self) -> u64 {
452 self.capacity
453 }
454}
455#[derive(Debug, Clone, PartialEq, Eq)]
457pub struct LevelNormalForm {
458 pub components: Vec<(Option<Name>, u32)>,
460}
461impl LevelNormalForm {
462 pub fn from_level(l: &Level) -> Self {
464 let mut comps = Vec::new();
465 collect_nf_comps(l, 0, &mut comps);
466 comps.dedup();
467 LevelNormalForm { components: comps }
468 }
469 pub fn to_level(&self) -> Level {
471 if self.components.is_empty() {
472 return Level::zero();
473 }
474 let levels: Vec<Level> = self
475 .components
476 .iter()
477 .map(|(base, succs)| {
478 let base_l = match base {
479 Some(name) => Level::param(name.clone()),
480 None => Level::zero(),
481 };
482 add_succs(base_l, *succs)
483 })
484 .collect();
485 levels
486 .into_iter()
487 .reduce(Level::max)
488 .unwrap_or(Level::zero())
489 }
490}
491#[derive(Debug, Clone)]
495pub struct UnivPolySignature {
496 pub params: Vec<Name>,
498 pub constraints: UnivConstraintSet,
500}
501impl UnivPolySignature {
502 pub fn new(params: Vec<Name>) -> Self {
504 Self {
505 params,
506 constraints: UnivConstraintSet::new(),
507 }
508 }
509 pub fn add_constraint(&mut self, c: UnivConstraint) {
511 self.constraints.add(c);
512 }
513 pub fn arity(&self) -> usize {
515 self.params.len()
516 }
517 pub fn instantiate(&self, args: &[Level]) -> Option<UniverseInstantiation> {
521 if args.len() != self.params.len() {
522 return None;
523 }
524 let mut inst = UniverseInstantiation::new();
525 for (p, l) in self.params.iter().zip(args.iter()) {
526 inst.add(p.clone(), l.clone());
527 }
528 Some(inst)
529 }
530 pub fn check_instantiation(&self, inst: &UniverseInstantiation) -> Result<(), String> {
532 let mut checker = UnivChecker::new();
533 for p in &self.params {
534 checker.add_univ_var(p.clone());
535 }
536 for c in &self.constraints.constraints {
537 let c_inst = match c {
538 UnivConstraint::Lt(u, v) => UnivConstraint::Lt(inst.apply(u), inst.apply(v)),
539 UnivConstraint::Le(u, v) => UnivConstraint::Le(inst.apply(u), inst.apply(v)),
540 UnivConstraint::Eq(u, v) => UnivConstraint::Eq(inst.apply(u), inst.apply(v)),
541 };
542 checker.add_constraint(c_inst);
543 }
544 checker.check()
545 }
546}
547#[allow(dead_code)]
549pub struct SparseVec<T: Default + Clone + PartialEq> {
550 entries: std::collections::HashMap<usize, T>,
551 default_: T,
552 logical_len: usize,
553}
554#[allow(dead_code)]
555impl<T: Default + Clone + PartialEq> SparseVec<T> {
556 pub fn new(len: usize) -> Self {
558 Self {
559 entries: std::collections::HashMap::new(),
560 default_: T::default(),
561 logical_len: len,
562 }
563 }
564 pub fn set(&mut self, idx: usize, val: T) {
566 if val == self.default_ {
567 self.entries.remove(&idx);
568 } else {
569 self.entries.insert(idx, val);
570 }
571 }
572 pub fn get(&self, idx: usize) -> &T {
574 self.entries.get(&idx).unwrap_or(&self.default_)
575 }
576 pub fn len(&self) -> usize {
578 self.logical_len
579 }
580 pub fn is_empty(&self) -> bool {
582 self.len() == 0
583 }
584 pub fn nnz(&self) -> usize {
586 self.entries.len()
587 }
588}
589#[allow(dead_code)]
591pub struct SimpleDag {
592 edges: Vec<Vec<usize>>,
594}
595#[allow(dead_code)]
596impl SimpleDag {
597 pub fn new(n: usize) -> Self {
599 Self {
600 edges: vec![Vec::new(); n],
601 }
602 }
603 pub fn add_edge(&mut self, from: usize, to: usize) {
605 if from < self.edges.len() {
606 self.edges[from].push(to);
607 }
608 }
609 pub fn successors(&self, node: usize) -> &[usize] {
611 self.edges.get(node).map(|v| v.as_slice()).unwrap_or(&[])
612 }
613 pub fn can_reach(&self, from: usize, to: usize) -> bool {
615 let mut visited = vec![false; self.edges.len()];
616 self.dfs(from, to, &mut visited)
617 }
618 fn dfs(&self, cur: usize, target: usize, visited: &mut Vec<bool>) -> bool {
619 if cur == target {
620 return true;
621 }
622 if cur >= visited.len() || visited[cur] {
623 return false;
624 }
625 visited[cur] = true;
626 for &next in self.successors(cur) {
627 if self.dfs(next, target, visited) {
628 return true;
629 }
630 }
631 false
632 }
633 pub fn topological_sort(&self) -> Option<Vec<usize>> {
635 let n = self.edges.len();
636 let mut in_degree = vec![0usize; n];
637 for succs in &self.edges {
638 for &s in succs {
639 if s < n {
640 in_degree[s] += 1;
641 }
642 }
643 }
644 let mut queue: std::collections::VecDeque<usize> =
645 (0..n).filter(|&i| in_degree[i] == 0).collect();
646 let mut order = Vec::new();
647 while let Some(node) = queue.pop_front() {
648 order.push(node);
649 for &s in self.successors(node) {
650 if s < n {
651 in_degree[s] -= 1;
652 if in_degree[s] == 0 {
653 queue.push_back(s);
654 }
655 }
656 }
657 }
658 if order.len() == n {
659 Some(order)
660 } else {
661 None
662 }
663 }
664 pub fn num_nodes(&self) -> usize {
666 self.edges.len()
667 }
668}
669#[derive(Debug, Clone, Default)]
671pub struct UniverseInstantiation {
672 pub subst: std::collections::HashMap<Name, Level>,
674}
675impl UniverseInstantiation {
676 pub fn new() -> Self {
678 Self::default()
679 }
680 pub fn add(&mut self, param: Name, level: Level) {
682 self.subst.insert(param, level);
683 }
684 pub fn apply(&self, l: &Level) -> Level {
686 let mut result = l.clone();
687 for (p, replacement) in &self.subst {
688 result = substitute_level_param(&result, p, replacement);
689 }
690 result
691 }
692 pub fn len(&self) -> usize {
694 self.subst.len()
695 }
696 pub fn is_empty(&self) -> bool {
698 self.subst.is_empty()
699 }
700 pub fn compose(&self, other: &Self) -> Self {
702 let mut result = Self::new();
703 for (p, l) in &other.subst {
704 result.add(p.clone(), self.apply(l));
705 }
706 for (p, l) in &self.subst {
707 result.subst.entry(p.clone()).or_insert_with(|| l.clone());
708 }
709 result
710 }
711}
712#[allow(dead_code)]
714pub struct StatSummary {
715 count: u64,
716 sum: f64,
717 min: f64,
718 max: f64,
719}
720#[allow(dead_code)]
721impl StatSummary {
722 pub fn new() -> Self {
724 Self {
725 count: 0,
726 sum: 0.0,
727 min: f64::INFINITY,
728 max: f64::NEG_INFINITY,
729 }
730 }
731 pub fn record(&mut self, val: f64) {
733 self.count += 1;
734 self.sum += val;
735 if val < self.min {
736 self.min = val;
737 }
738 if val > self.max {
739 self.max = val;
740 }
741 }
742 pub fn mean(&self) -> Option<f64> {
744 if self.count == 0 {
745 None
746 } else {
747 Some(self.sum / self.count as f64)
748 }
749 }
750 pub fn min(&self) -> Option<f64> {
752 if self.count == 0 {
753 None
754 } else {
755 Some(self.min)
756 }
757 }
758 pub fn max(&self) -> Option<f64> {
760 if self.count == 0 {
761 None
762 } else {
763 Some(self.max)
764 }
765 }
766 pub fn count(&self) -> u64 {
768 self.count
769 }
770}
771#[allow(dead_code)]
773pub struct SlidingSum {
774 window: Vec<f64>,
775 capacity: usize,
776 pos: usize,
777 sum: f64,
778 count: usize,
779}
780#[allow(dead_code)]
781impl SlidingSum {
782 pub fn new(capacity: usize) -> Self {
784 Self {
785 window: vec![0.0; capacity],
786 capacity,
787 pos: 0,
788 sum: 0.0,
789 count: 0,
790 }
791 }
792 pub fn push(&mut self, val: f64) {
794 let oldest = self.window[self.pos];
795 self.sum -= oldest;
796 self.sum += val;
797 self.window[self.pos] = val;
798 self.pos = (self.pos + 1) % self.capacity;
799 if self.count < self.capacity {
800 self.count += 1;
801 }
802 }
803 pub fn sum(&self) -> f64 {
805 self.sum
806 }
807 pub fn mean(&self) -> Option<f64> {
809 if self.count == 0 {
810 None
811 } else {
812 Some(self.sum / self.count as f64)
813 }
814 }
815 pub fn count(&self) -> usize {
817 self.count
818 }
819}
820#[allow(dead_code)]
822pub struct TransitiveClosure {
823 adj: Vec<Vec<usize>>,
824 n: usize,
825}
826#[allow(dead_code)]
827impl TransitiveClosure {
828 pub fn new(n: usize) -> Self {
830 Self {
831 adj: vec![Vec::new(); n],
832 n,
833 }
834 }
835 pub fn add_edge(&mut self, from: usize, to: usize) {
837 if from < self.n {
838 self.adj[from].push(to);
839 }
840 }
841 pub fn reachable_from(&self, start: usize) -> Vec<usize> {
843 let mut visited = vec![false; self.n];
844 let mut queue = std::collections::VecDeque::new();
845 queue.push_back(start);
846 while let Some(node) = queue.pop_front() {
847 if node >= self.n || visited[node] {
848 continue;
849 }
850 visited[node] = true;
851 for &next in &self.adj[node] {
852 queue.push_back(next);
853 }
854 }
855 (0..self.n).filter(|&i| visited[i]).collect()
856 }
857 pub fn can_reach(&self, from: usize, to: usize) -> bool {
859 self.reachable_from(from).contains(&to)
860 }
861}
862#[allow(dead_code)]
864pub struct RawFnPtr {
865 ptr: usize,
867 arity: usize,
868 name: String,
869}
870#[allow(dead_code)]
871impl RawFnPtr {
872 pub fn new(ptr: usize, arity: usize, name: impl Into<String>) -> Self {
874 Self {
875 ptr,
876 arity,
877 name: name.into(),
878 }
879 }
880 pub fn arity(&self) -> usize {
882 self.arity
883 }
884 pub fn name(&self) -> &str {
886 &self.name
887 }
888 pub fn raw(&self) -> usize {
890 self.ptr
891 }
892}
893#[allow(dead_code)]
895pub struct NonEmptyVec<T> {
896 head: T,
897 tail: Vec<T>,
898}
899#[allow(dead_code)]
900impl<T> NonEmptyVec<T> {
901 pub fn singleton(val: T) -> Self {
903 Self {
904 head: val,
905 tail: Vec::new(),
906 }
907 }
908 pub fn push(&mut self, val: T) {
910 self.tail.push(val);
911 }
912 pub fn first(&self) -> &T {
914 &self.head
915 }
916 pub fn last(&self) -> &T {
918 self.tail.last().unwrap_or(&self.head)
919 }
920 pub fn len(&self) -> usize {
922 1 + self.tail.len()
923 }
924 pub fn is_empty(&self) -> bool {
926 self.len() == 0
927 }
928 pub fn to_vec(&self) -> Vec<&T> {
930 let mut v = vec![&self.head];
931 v.extend(self.tail.iter());
932 v
933 }
934}
935#[allow(dead_code)]
937pub struct PathBuf {
938 components: Vec<String>,
939}
940#[allow(dead_code)]
941impl PathBuf {
942 pub fn new() -> Self {
944 Self {
945 components: Vec::new(),
946 }
947 }
948 pub fn push(&mut self, comp: impl Into<String>) {
950 self.components.push(comp.into());
951 }
952 pub fn pop(&mut self) {
954 self.components.pop();
955 }
956 pub fn as_str(&self) -> String {
958 self.components.join("/")
959 }
960 pub fn depth(&self) -> usize {
962 self.components.len()
963 }
964 pub fn clear(&mut self) {
966 self.components.clear();
967 }
968}
969#[derive(Debug, Clone, Default)]
971pub struct UnivConstraintSet {
972 constraints: Vec<UnivConstraint>,
973}
974impl UnivConstraintSet {
975 pub fn new() -> Self {
977 Self::default()
978 }
979 pub fn add(&mut self, c: UnivConstraint) {
981 if !self.constraints.contains(&c) {
982 self.constraints.push(c);
983 }
984 }
985 pub fn merge(&mut self, other: &Self) {
987 for c in &other.constraints {
988 self.add(c.clone());
989 }
990 }
991 pub fn len(&self) -> usize {
993 self.constraints.len()
994 }
995 pub fn is_empty(&self) -> bool {
997 self.constraints.is_empty()
998 }
999 pub fn check_all(&self, checker: &UnivChecker) -> Result<(), String> {
1001 for c in &self.constraints {
1002 match c {
1003 UnivConstraint::Lt(u, v) => {
1004 if !checker.is_gt(v, u) {
1005 return Err(format!(
1006 "constraint {} < {} violated",
1007 format_level(u),
1008 format_level(v)
1009 ));
1010 }
1011 }
1012 UnivConstraint::Le(u, v) => {
1013 if !checker.is_geq(v, u) {
1014 return Err(format!(
1015 "constraint {} <= {} violated",
1016 format_level(u),
1017 format_level(v)
1018 ));
1019 }
1020 }
1021 UnivConstraint::Eq(u, v) => {
1022 if !checker.is_level_def_eq(u, v) {
1023 return Err(format!(
1024 "constraint {} = {} violated",
1025 format_level(u),
1026 format_level(v)
1027 ));
1028 }
1029 }
1030 }
1031 }
1032 Ok(())
1033 }
1034 pub fn dedup(&mut self) {
1036 let mut seen = std::collections::HashSet::new();
1037 self.constraints.retain(|c| seen.insert(c.clone()));
1038 }
1039}
1040pub struct UnivChecker {
1042 constraints: Vec<UnivConstraint>,
1044 univ_vars: HashSet<Name>,
1046 mvar_assignments: HashMap<LevelMVarId, Level>,
1048 next_mvar_id: u64,
1050}
1051impl UnivChecker {
1052 pub fn new() -> Self {
1054 Self {
1055 constraints: Vec::new(),
1056 univ_vars: HashSet::new(),
1057 mvar_assignments: HashMap::new(),
1058 next_mvar_id: 0,
1059 }
1060 }
1061 pub fn add_univ_var(&mut self, name: Name) {
1063 self.univ_vars.insert(name);
1064 }
1065 pub fn add_constraint(&mut self, constraint: UnivConstraint) {
1067 self.constraints.push(constraint);
1068 }
1069 pub fn fresh_level_mvar(&mut self) -> Level {
1071 let id = LevelMVarId(self.next_mvar_id);
1072 self.next_mvar_id += 1;
1073 Level::MVar(id)
1074 }
1075 pub fn assign_mvar(&mut self, id: LevelMVarId, level: Level) {
1077 self.mvar_assignments.insert(id, level);
1078 }
1079 pub fn get_mvar_assignment(&self, id: &LevelMVarId) -> Option<&Level> {
1081 self.mvar_assignments.get(id)
1082 }
1083 pub fn instantiate_mvars(&self, l: &Level) -> Level {
1085 level::instantiate_level_mvars(l, &|id| self.mvar_assignments.get(&id).cloned())
1086 }
1087 pub fn is_level_def_eq(&self, l1: &Level, l2: &Level) -> bool {
1091 let l1_inst = self.instantiate_mvars(l1);
1092 let l2_inst = self.instantiate_mvars(l2);
1093 level::is_equivalent(&l1_inst, &l2_inst)
1094 }
1095 pub fn is_geq(&self, l1: &Level, l2: &Level) -> bool {
1097 let l1_inst = self.instantiate_mvars(l1);
1098 let l2_inst = self.instantiate_mvars(l2);
1099 level::is_geq(&l1_inst, &l2_inst)
1100 }
1101 pub fn is_gt(&self, l1: &Level, l2: &Level) -> bool {
1105 let l1_inst = self.instantiate_mvars(l1);
1106 let l2_inst = self.instantiate_mvars(l2);
1107 level::is_geq(&l1_inst, &Level::succ(l2_inst))
1108 }
1109 pub fn check(&self) -> Result<(), String> {
1111 for constraint in &self.constraints {
1112 match constraint {
1113 UnivConstraint::Lt(u, v) => {
1114 let u_inst = self.instantiate_mvars(u);
1115 let v_inst = self.instantiate_mvars(v);
1116 if !self.check_lt(&u_inst, &v_inst) {
1117 return Err(format!(
1118 "Universe constraint violated: {} < {}",
1119 u_inst, v_inst
1120 ));
1121 }
1122 }
1123 UnivConstraint::Le(u, v) => {
1124 let u_inst = self.instantiate_mvars(u);
1125 let v_inst = self.instantiate_mvars(v);
1126 if !level::is_geq(&v_inst, &u_inst) {
1127 return Err(format!(
1128 "Universe constraint violated: {} <= {}",
1129 u_inst, v_inst
1130 ));
1131 }
1132 }
1133 UnivConstraint::Eq(u, v) => {
1134 let u_inst = self.instantiate_mvars(u);
1135 let v_inst = self.instantiate_mvars(v);
1136 if !level::is_equivalent(&u_inst, &v_inst) {
1137 return Err(format!(
1138 "Universe constraint violated: {} = {}",
1139 u_inst, v_inst
1140 ));
1141 }
1142 }
1143 }
1144 }
1145 Ok(())
1146 }
1147 fn check_lt(&self, u: &Level, v: &Level) -> bool {
1149 level::is_geq(v, &Level::succ(u.clone()))
1150 }
1151 pub fn solve_simple(&mut self) -> bool {
1156 let mut changed = true;
1157 let mut any_solved = false;
1158 while changed {
1159 changed = false;
1160 let constraints = self.constraints.clone();
1161 for constraint in &constraints {
1162 if let UnivConstraint::Eq(l, r) = constraint {
1163 let l_inst = self.instantiate_mvars(l);
1164 let r_inst = self.instantiate_mvars(r);
1165 if let Level::MVar(id) = &l_inst {
1166 if !r_inst.has_mvar() {
1167 self.mvar_assignments.insert(*id, r_inst);
1168 changed = true;
1169 any_solved = true;
1170 continue;
1171 }
1172 }
1173 if let Level::MVar(id) = &r_inst {
1174 if !l_inst.has_mvar() {
1175 self.mvar_assignments.insert(*id, l_inst);
1176 changed = true;
1177 any_solved = true;
1178 }
1179 }
1180 }
1181 }
1182 }
1183 any_solved
1184 }
1185 pub fn all_constraints(&self) -> &[UnivConstraint] {
1187 &self.constraints
1188 }
1189 pub fn all_univ_vars(&self) -> &HashSet<Name> {
1191 &self.univ_vars
1192 }
1193 pub fn clear(&mut self) {
1195 self.constraints.clear();
1196 self.mvar_assignments.clear();
1197 }
1198 pub fn has_unassigned_mvars(&self, l: &Level) -> bool {
1200 let inst = self.instantiate_mvars(l);
1201 inst.has_mvar()
1202 }
1203}
1204#[allow(dead_code)]
1206pub struct FocusStack<T> {
1207 items: Vec<T>,
1208}
1209#[allow(dead_code)]
1210impl<T> FocusStack<T> {
1211 pub fn new() -> Self {
1213 Self { items: Vec::new() }
1214 }
1215 pub fn focus(&mut self, item: T) {
1217 self.items.push(item);
1218 }
1219 pub fn blur(&mut self) -> Option<T> {
1221 self.items.pop()
1222 }
1223 pub fn current(&self) -> Option<&T> {
1225 self.items.last()
1226 }
1227 pub fn depth(&self) -> usize {
1229 self.items.len()
1230 }
1231 pub fn is_empty(&self) -> bool {
1233 self.items.is_empty()
1234 }
1235}
1236#[allow(dead_code)]
1238pub struct StringPool {
1239 free: Vec<String>,
1240}
1241#[allow(dead_code)]
1242impl StringPool {
1243 pub fn new() -> Self {
1245 Self { free: Vec::new() }
1246 }
1247 pub fn take(&mut self) -> String {
1249 self.free.pop().unwrap_or_default()
1250 }
1251 pub fn give(&mut self, mut s: String) {
1253 s.clear();
1254 self.free.push(s);
1255 }
1256 pub fn free_count(&self) -> usize {
1258 self.free.len()
1259 }
1260}
1261#[allow(dead_code)]
1263pub struct Stopwatch {
1264 start: std::time::Instant,
1265 splits: Vec<f64>,
1266}
1267#[allow(dead_code)]
1268impl Stopwatch {
1269 pub fn start() -> Self {
1271 Self {
1272 start: std::time::Instant::now(),
1273 splits: Vec::new(),
1274 }
1275 }
1276 pub fn split(&mut self) {
1278 self.splits.push(self.elapsed_ms());
1279 }
1280 pub fn elapsed_ms(&self) -> f64 {
1282 self.start.elapsed().as_secs_f64() * 1000.0
1283 }
1284 pub fn splits(&self) -> &[f64] {
1286 &self.splits
1287 }
1288 pub fn num_splits(&self) -> usize {
1290 self.splits.len()
1291 }
1292}
1293#[allow(dead_code)]
1295pub struct StackCalc {
1296 stack: Vec<i64>,
1297}
1298#[allow(dead_code)]
1299impl StackCalc {
1300 pub fn new() -> Self {
1302 Self { stack: Vec::new() }
1303 }
1304 pub fn push(&mut self, n: i64) {
1306 self.stack.push(n);
1307 }
1308 pub fn add(&mut self) {
1310 let b = self
1311 .stack
1312 .pop()
1313 .expect("stack must have at least two values for add");
1314 let a = self
1315 .stack
1316 .pop()
1317 .expect("stack must have at least two values for add");
1318 self.stack.push(a + b);
1319 }
1320 pub fn sub(&mut self) {
1322 let b = self
1323 .stack
1324 .pop()
1325 .expect("stack must have at least two values for sub");
1326 let a = self
1327 .stack
1328 .pop()
1329 .expect("stack must have at least two values for sub");
1330 self.stack.push(a - b);
1331 }
1332 pub fn mul(&mut self) {
1334 let b = self
1335 .stack
1336 .pop()
1337 .expect("stack must have at least two values for mul");
1338 let a = self
1339 .stack
1340 .pop()
1341 .expect("stack must have at least two values for mul");
1342 self.stack.push(a * b);
1343 }
1344 pub fn peek(&self) -> Option<i64> {
1346 self.stack.last().copied()
1347 }
1348 pub fn depth(&self) -> usize {
1350 self.stack.len()
1351 }
1352}
1353#[allow(dead_code)]
1355pub struct FlatSubstitution {
1356 pairs: Vec<(String, String)>,
1357}
1358#[allow(dead_code)]
1359impl FlatSubstitution {
1360 pub fn new() -> Self {
1362 Self { pairs: Vec::new() }
1363 }
1364 pub fn add(&mut self, from: impl Into<String>, to: impl Into<String>) {
1366 self.pairs.push((from.into(), to.into()));
1367 }
1368 pub fn apply(&self, s: &str) -> String {
1370 let mut result = s.to_string();
1371 for (from, to) in &self.pairs {
1372 result = result.replace(from.as_str(), to.as_str());
1373 }
1374 result
1375 }
1376 pub fn len(&self) -> usize {
1378 self.pairs.len()
1379 }
1380 pub fn is_empty(&self) -> bool {
1382 self.pairs.is_empty()
1383 }
1384}
1385#[allow(dead_code)]
1387pub struct ConfigNode {
1388 key: String,
1389 value: Option<String>,
1390 children: Vec<ConfigNode>,
1391}
1392#[allow(dead_code)]
1393impl ConfigNode {
1394 pub fn leaf(key: impl Into<String>, value: impl Into<String>) -> Self {
1396 Self {
1397 key: key.into(),
1398 value: Some(value.into()),
1399 children: Vec::new(),
1400 }
1401 }
1402 pub fn section(key: impl Into<String>) -> Self {
1404 Self {
1405 key: key.into(),
1406 value: None,
1407 children: Vec::new(),
1408 }
1409 }
1410 pub fn add_child(&mut self, child: ConfigNode) {
1412 self.children.push(child);
1413 }
1414 pub fn key(&self) -> &str {
1416 &self.key
1417 }
1418 pub fn value(&self) -> Option<&str> {
1420 self.value.as_deref()
1421 }
1422 pub fn num_children(&self) -> usize {
1424 self.children.len()
1425 }
1426 pub fn lookup(&self, path: &str) -> Option<&str> {
1428 let mut parts = path.splitn(2, '.');
1429 let head = parts.next()?;
1430 let tail = parts.next();
1431 if head != self.key {
1432 return None;
1433 }
1434 match tail {
1435 None => self.value.as_deref(),
1436 Some(rest) => self.children.iter().find_map(|c| c.lookup_relative(rest)),
1437 }
1438 }
1439 fn lookup_relative(&self, path: &str) -> Option<&str> {
1440 let mut parts = path.splitn(2, '.');
1441 let head = parts.next()?;
1442 let tail = parts.next();
1443 if head != self.key {
1444 return None;
1445 }
1446 match tail {
1447 None => self.value.as_deref(),
1448 Some(rest) => self.children.iter().find_map(|c| c.lookup_relative(rest)),
1449 }
1450 }
1451}
1452#[allow(dead_code)]
1454#[allow(missing_docs)]
1455pub enum DecisionNode {
1456 Leaf(String),
1458 Branch {
1460 key: String,
1461 val: String,
1462 yes_branch: Box<DecisionNode>,
1463 no_branch: Box<DecisionNode>,
1464 },
1465}
1466#[allow(dead_code)]
1467impl DecisionNode {
1468 pub fn evaluate(&self, ctx: &std::collections::HashMap<String, String>) -> &str {
1470 match self {
1471 DecisionNode::Leaf(action) => action.as_str(),
1472 DecisionNode::Branch {
1473 key,
1474 val,
1475 yes_branch,
1476 no_branch,
1477 } => {
1478 let actual = ctx.get(key).map(|s| s.as_str()).unwrap_or("");
1479 if actual == val.as_str() {
1480 yes_branch.evaluate(ctx)
1481 } else {
1482 no_branch.evaluate(ctx)
1483 }
1484 }
1485 }
1486 }
1487 pub fn depth(&self) -> usize {
1489 match self {
1490 DecisionNode::Leaf(_) => 0,
1491 DecisionNode::Branch {
1492 yes_branch,
1493 no_branch,
1494 ..
1495 } => 1 + yes_branch.depth().max(no_branch.depth()),
1496 }
1497 }
1498}
1499#[allow(dead_code)]
1501pub struct LabelSet {
1502 labels: Vec<String>,
1503}
1504#[allow(dead_code)]
1505impl LabelSet {
1506 pub fn new() -> Self {
1508 Self { labels: Vec::new() }
1509 }
1510 pub fn add(&mut self, label: impl Into<String>) {
1512 let s = label.into();
1513 if !self.labels.contains(&s) {
1514 self.labels.push(s);
1515 }
1516 }
1517 pub fn has(&self, label: &str) -> bool {
1519 self.labels.iter().any(|l| l == label)
1520 }
1521 pub fn count(&self) -> usize {
1523 self.labels.len()
1524 }
1525 pub fn all(&self) -> &[String] {
1527 &self.labels
1528 }
1529}