1use crate::level::{self, LevelMVarId};
6use crate::{Level, LevelView, 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 earlier: Vec<T>,
123 current: T,
125}
126#[allow(dead_code)]
127impl<T: Clone> VersionedRecord<T> {
128 pub fn new(initial: T) -> Self {
130 Self {
131 earlier: Vec::new(),
132 current: initial,
133 }
134 }
135 pub fn update(&mut self, val: T) {
137 let previous = std::mem::replace(&mut self.current, val);
138 self.earlier.push(previous);
139 }
140 pub fn current(&self) -> &T {
142 &self.current
143 }
144 pub fn at_version(&self, n: usize) -> Option<&T> {
146 match self.earlier.get(n) {
147 Some(value) => Some(value),
148 None if n == self.earlier.len() => Some(&self.current),
149 None => None,
150 }
151 }
152 pub fn version(&self) -> usize {
154 self.earlier.len()
155 }
156 pub fn has_history(&self) -> bool {
158 !self.earlier.is_empty()
159 }
160}
161#[allow(dead_code)]
163pub struct WindowIterator<'a, T> {
164 pub(super) data: &'a [T],
165 pub(super) pos: usize,
166 pub(super) window: usize,
167}
168#[allow(dead_code)]
169impl<'a, T> WindowIterator<'a, T> {
170 pub fn new(data: &'a [T], window: usize) -> Self {
172 Self {
173 data,
174 pos: 0,
175 window,
176 }
177 }
178}
179#[allow(dead_code)]
181pub struct SmallMap<K: Ord + Clone, V: Clone> {
182 entries: Vec<(K, V)>,
183}
184#[allow(dead_code)]
185impl<K: Ord + Clone, V: Clone> SmallMap<K, V> {
186 pub fn new() -> Self {
188 Self {
189 entries: Vec::new(),
190 }
191 }
192 pub fn insert(&mut self, key: K, val: V) {
194 match self.entries.binary_search_by_key(&&key, |(k, _)| k) {
195 Ok(i) => self.entries[i].1 = val,
196 Err(i) => self.entries.insert(i, (key, val)),
197 }
198 }
199 pub fn get(&self, key: &K) -> Option<&V> {
201 self.entries
202 .binary_search_by_key(&key, |(k, _)| k)
203 .ok()
204 .map(|i| &self.entries[i].1)
205 }
206 pub fn len(&self) -> usize {
208 self.entries.len()
209 }
210 pub fn is_empty(&self) -> bool {
212 self.entries.is_empty()
213 }
214 pub fn keys(&self) -> Vec<&K> {
216 self.entries.iter().map(|(k, _)| k).collect()
217 }
218 pub fn values(&self) -> Vec<&V> {
220 self.entries.iter().map(|(_, v)| v).collect()
221 }
222}
223#[allow(dead_code)]
225pub struct RewriteRuleSet {
226 rules: Vec<RewriteRule>,
227}
228#[allow(dead_code)]
229impl RewriteRuleSet {
230 pub fn new() -> Self {
232 Self { rules: Vec::new() }
233 }
234 pub fn add(&mut self, rule: RewriteRule) {
236 self.rules.push(rule);
237 }
238 pub fn len(&self) -> usize {
240 self.rules.len()
241 }
242 pub fn is_empty(&self) -> bool {
244 self.rules.is_empty()
245 }
246 pub fn conditional_rules(&self) -> Vec<&RewriteRule> {
248 self.rules.iter().filter(|r| r.conditional).collect()
249 }
250 pub fn unconditional_rules(&self) -> Vec<&RewriteRule> {
252 self.rules.iter().filter(|r| !r.conditional).collect()
253 }
254 pub fn get(&self, name: &str) -> Option<&RewriteRule> {
256 self.rules.iter().find(|r| r.name == name)
257 }
258}
259#[derive(Debug, Clone, Default)]
263pub struct LevelComparisonTable {
264 levels: Vec<Level>,
265 geq_cache: std::collections::HashMap<(usize, usize), bool>,
267}
268impl LevelComparisonTable {
269 pub fn new(levels: Vec<Level>) -> Self {
271 let mut table = Self {
272 levels,
273 geq_cache: Default::default(),
274 };
275 table.precompute();
276 table
277 }
278 fn precompute(&mut self) {
279 let checker = UnivChecker::new();
280 let n = self.levels.len();
281 for i in 0..n {
282 for j in 0..n {
283 let result = checker.is_geq(&self.levels[i].clone(), &self.levels[j].clone());
284 self.geq_cache.insert((i, j), result);
285 }
286 }
287 }
288 pub fn geq(&self, i: usize, j: usize) -> Option<bool> {
290 self.geq_cache.get(&(i, j)).copied()
291 }
292 pub fn max_idx(&self) -> Option<usize> {
294 (0..self.levels.len()).max_by(|&i, &j| {
295 let checker = UnivChecker::new();
296 if checker.is_geq(&self.levels[i], &self.levels[j]) {
297 std::cmp::Ordering::Greater
298 } else {
299 std::cmp::Ordering::Less
300 }
301 })
302 }
303 pub fn len(&self) -> usize {
305 self.levels.len()
306 }
307 pub fn is_empty(&self) -> bool {
309 self.levels.is_empty()
310 }
311}
312#[allow(dead_code)]
314pub enum Either2<A, B> {
315 First(A),
317 Second(B),
319}
320#[allow(dead_code)]
321impl<A, B> Either2<A, B> {
322 pub fn is_first(&self) -> bool {
324 matches!(self, Either2::First(_))
325 }
326 pub fn is_second(&self) -> bool {
328 matches!(self, Either2::Second(_))
329 }
330 pub fn first(self) -> Option<A> {
332 match self {
333 Either2::First(a) => Some(a),
334 _ => None,
335 }
336 }
337 pub fn second(self) -> Option<B> {
339 match self {
340 Either2::Second(b) => Some(b),
341 _ => None,
342 }
343 }
344 pub fn map_first<C, F: FnOnce(A) -> C>(self, f: F) -> Either2<C, B> {
346 match self {
347 Either2::First(a) => Either2::First(f(a)),
348 Either2::Second(b) => Either2::Second(b),
349 }
350 }
351}
352#[allow(dead_code)]
354pub struct WriteOnce<T> {
355 value: std::cell::Cell<Option<T>>,
356}
357#[allow(dead_code)]
358impl<T: Copy> WriteOnce<T> {
359 pub fn new() -> Self {
361 Self {
362 value: std::cell::Cell::new(None),
363 }
364 }
365 pub fn write(&self, val: T) -> bool {
367 if self.value.get().is_some() {
368 return false;
369 }
370 self.value.set(Some(val));
371 true
372 }
373 pub fn read(&self) -> Option<T> {
375 self.value.get()
376 }
377 pub fn is_written(&self) -> bool {
379 self.value.get().is_some()
380 }
381}
382#[allow(dead_code)]
384pub struct TransformStat {
385 before: StatSummary,
386 after: StatSummary,
387}
388#[allow(dead_code)]
389impl TransformStat {
390 pub fn new() -> Self {
392 Self {
393 before: StatSummary::new(),
394 after: StatSummary::new(),
395 }
396 }
397 pub fn record_before(&mut self, v: f64) {
399 self.before.record(v);
400 }
401 pub fn record_after(&mut self, v: f64) {
403 self.after.record(v);
404 }
405 pub fn mean_ratio(&self) -> Option<f64> {
407 let b = self.before.mean()?;
408 let a = self.after.mean()?;
409 if b.abs() < f64::EPSILON {
410 return None;
411 }
412 Some(a / b)
413 }
414}
415#[allow(dead_code)]
417pub struct TokenBucket {
418 capacity: u64,
419 tokens: u64,
420 refill_per_ms: u64,
421 last_refill: crate::wall_clock::Instant,
422}
423#[allow(dead_code)]
424impl TokenBucket {
425 pub fn new(capacity: u64, refill_per_ms: u64) -> Self {
427 Self {
428 capacity,
429 tokens: capacity,
430 refill_per_ms,
431 last_refill: crate::wall_clock::Instant::now(),
432 }
433 }
434 pub fn try_consume(&mut self, n: u64) -> bool {
436 self.refill();
437 if self.tokens >= n {
438 self.tokens -= n;
439 true
440 } else {
441 false
442 }
443 }
444 fn refill(&mut self) {
445 let now = crate::wall_clock::Instant::now();
446 let elapsed_ms = now.duration_since(self.last_refill).as_millis() as u64;
447 if elapsed_ms > 0 {
448 let new_tokens = elapsed_ms * self.refill_per_ms;
449 self.tokens = (self.tokens + new_tokens).min(self.capacity);
450 self.last_refill = now;
451 }
452 }
453 pub fn available(&self) -> u64 {
455 self.tokens
456 }
457 pub fn capacity(&self) -> u64 {
459 self.capacity
460 }
461}
462#[derive(Debug, Clone, PartialEq, Eq)]
464pub struct LevelNormalForm {
465 pub components: Vec<(Option<Name>, u32)>,
467}
468impl LevelNormalForm {
469 pub fn from_level(l: &Level) -> Self {
471 let mut comps = Vec::new();
472 collect_nf_comps(l, 0, &mut comps);
473 comps.dedup();
474 LevelNormalForm { components: comps }
475 }
476 pub fn to_level(&self) -> Level {
478 if self.components.is_empty() {
479 return Level::zero();
480 }
481 let levels: Vec<Level> = self
482 .components
483 .iter()
484 .map(|(base, succs)| {
485 let base_l = match base {
486 Some(name) => Level::param(name.clone()),
487 None => Level::zero(),
488 };
489 add_succs(base_l, *succs)
490 })
491 .collect();
492 levels
493 .into_iter()
494 .reduce(Level::max)
495 .unwrap_or(Level::zero())
496 }
497}
498#[derive(Debug, Clone)]
502pub struct UnivPolySignature {
503 pub params: Vec<Name>,
505 pub constraints: UnivConstraintSet,
507}
508impl UnivPolySignature {
509 pub fn new(params: Vec<Name>) -> Self {
511 Self {
512 params,
513 constraints: UnivConstraintSet::new(),
514 }
515 }
516 pub fn add_constraint(&mut self, c: UnivConstraint) {
518 self.constraints.add(c);
519 }
520 pub fn arity(&self) -> usize {
522 self.params.len()
523 }
524 pub fn instantiate(&self, args: &[Level]) -> Option<UniverseInstantiation> {
528 if args.len() != self.params.len() {
529 return None;
530 }
531 let mut inst = UniverseInstantiation::new();
532 for (p, l) in self.params.iter().zip(args.iter()) {
533 inst.add(p.clone(), l.clone());
534 }
535 Some(inst)
536 }
537 pub fn check_instantiation(&self, inst: &UniverseInstantiation) -> Result<(), String> {
539 let mut checker = UnivChecker::new();
540 for p in &self.params {
541 checker.add_univ_var(p.clone());
542 }
543 for c in &self.constraints.constraints {
544 let c_inst = match c {
545 UnivConstraint::Lt(u, v) => UnivConstraint::Lt(inst.apply(u), inst.apply(v)),
546 UnivConstraint::Le(u, v) => UnivConstraint::Le(inst.apply(u), inst.apply(v)),
547 UnivConstraint::Eq(u, v) => UnivConstraint::Eq(inst.apply(u), inst.apply(v)),
548 };
549 checker.add_constraint(c_inst);
550 }
551 checker.check()
552 }
553}
554#[allow(dead_code)]
556pub struct SparseVec<T: Default + Clone + PartialEq> {
557 entries: std::collections::HashMap<usize, T>,
558 default_: T,
559 logical_len: usize,
560}
561#[allow(dead_code)]
562impl<T: Default + Clone + PartialEq> SparseVec<T> {
563 pub fn new(len: usize) -> Self {
565 Self {
566 entries: std::collections::HashMap::new(),
567 default_: T::default(),
568 logical_len: len,
569 }
570 }
571 pub fn set(&mut self, idx: usize, val: T) {
573 if val == self.default_ {
574 self.entries.remove(&idx);
575 } else {
576 self.entries.insert(idx, val);
577 }
578 }
579 pub fn get(&self, idx: usize) -> &T {
581 self.entries.get(&idx).unwrap_or(&self.default_)
582 }
583 pub fn len(&self) -> usize {
585 self.logical_len
586 }
587 pub fn is_empty(&self) -> bool {
589 self.len() == 0
590 }
591 pub fn nnz(&self) -> usize {
593 self.entries.len()
594 }
595}
596#[allow(dead_code)]
598pub struct SimpleDag {
599 edges: Vec<Vec<usize>>,
601}
602#[allow(dead_code)]
603impl SimpleDag {
604 pub fn new(n: usize) -> Self {
606 Self {
607 edges: vec![Vec::new(); n],
608 }
609 }
610 pub fn add_edge(&mut self, from: usize, to: usize) {
612 if from < self.edges.len() {
613 self.edges[from].push(to);
614 }
615 }
616 pub fn successors(&self, node: usize) -> &[usize] {
618 self.edges.get(node).map(|v| v.as_slice()).unwrap_or(&[])
619 }
620 pub fn can_reach(&self, from: usize, to: usize) -> bool {
622 let mut visited = vec![false; self.edges.len()];
623 self.dfs(from, to, &mut visited)
624 }
625 fn dfs(&self, cur: usize, target: usize, visited: &mut Vec<bool>) -> bool {
626 if cur == target {
627 return true;
628 }
629 if cur >= visited.len() || visited[cur] {
630 return false;
631 }
632 visited[cur] = true;
633 for &next in self.successors(cur) {
634 if self.dfs(next, target, visited) {
635 return true;
636 }
637 }
638 false
639 }
640 pub fn topological_sort(&self) -> Option<Vec<usize>> {
642 let n = self.edges.len();
643 let mut in_degree = vec![0usize; n];
644 for succs in &self.edges {
645 for &s in succs {
646 if s < n {
647 in_degree[s] += 1;
648 }
649 }
650 }
651 let mut queue: std::collections::VecDeque<usize> =
652 (0..n).filter(|&i| in_degree[i] == 0).collect();
653 let mut order = Vec::new();
654 while let Some(node) = queue.pop_front() {
655 order.push(node);
656 for &s in self.successors(node) {
657 if s < n {
658 in_degree[s] -= 1;
659 if in_degree[s] == 0 {
660 queue.push_back(s);
661 }
662 }
663 }
664 }
665 if order.len() == n {
666 Some(order)
667 } else {
668 None
669 }
670 }
671 pub fn num_nodes(&self) -> usize {
673 self.edges.len()
674 }
675}
676#[derive(Debug, Clone, Default)]
678pub struct UniverseInstantiation {
679 pub subst: std::collections::HashMap<Name, Level>,
681}
682impl UniverseInstantiation {
683 pub fn new() -> Self {
685 Self::default()
686 }
687 pub fn add(&mut self, param: Name, level: Level) {
689 self.subst.insert(param, level);
690 }
691 pub fn apply(&self, l: &Level) -> Level {
693 let mut result = l.clone();
694 for (p, replacement) in &self.subst {
695 result = substitute_level_param(&result, p, replacement);
696 }
697 result
698 }
699 pub fn len(&self) -> usize {
701 self.subst.len()
702 }
703 pub fn is_empty(&self) -> bool {
705 self.subst.is_empty()
706 }
707 pub fn compose(&self, other: &Self) -> Self {
709 let mut result = Self::new();
710 for (p, l) in &other.subst {
711 result.add(p.clone(), self.apply(l));
712 }
713 for (p, l) in &self.subst {
714 result.subst.entry(p.clone()).or_insert_with(|| l.clone());
715 }
716 result
717 }
718}
719#[allow(dead_code)]
721pub struct StatSummary {
722 count: u64,
723 sum: f64,
724 min: f64,
725 max: f64,
726}
727#[allow(dead_code)]
728impl StatSummary {
729 pub fn new() -> Self {
731 Self {
732 count: 0,
733 sum: 0.0,
734 min: f64::INFINITY,
735 max: f64::NEG_INFINITY,
736 }
737 }
738 pub fn record(&mut self, val: f64) {
740 self.count += 1;
741 self.sum += val;
742 if val < self.min {
743 self.min = val;
744 }
745 if val > self.max {
746 self.max = val;
747 }
748 }
749 pub fn mean(&self) -> Option<f64> {
751 if self.count == 0 {
752 None
753 } else {
754 Some(self.sum / self.count as f64)
755 }
756 }
757 pub fn min(&self) -> Option<f64> {
759 if self.count == 0 {
760 None
761 } else {
762 Some(self.min)
763 }
764 }
765 pub fn max(&self) -> Option<f64> {
767 if self.count == 0 {
768 None
769 } else {
770 Some(self.max)
771 }
772 }
773 pub fn count(&self) -> u64 {
775 self.count
776 }
777}
778#[allow(dead_code)]
780pub struct SlidingSum {
781 window: Vec<f64>,
782 capacity: usize,
783 pos: usize,
784 sum: f64,
785 count: usize,
786}
787#[allow(dead_code)]
788impl SlidingSum {
789 pub fn new(capacity: usize) -> Self {
791 Self {
792 window: vec![0.0; capacity],
793 capacity,
794 pos: 0,
795 sum: 0.0,
796 count: 0,
797 }
798 }
799 pub fn push(&mut self, val: f64) {
801 let oldest = self.window[self.pos];
802 self.sum -= oldest;
803 self.sum += val;
804 self.window[self.pos] = val;
805 self.pos = (self.pos + 1) % self.capacity;
806 if self.count < self.capacity {
807 self.count += 1;
808 }
809 }
810 pub fn sum(&self) -> f64 {
812 self.sum
813 }
814 pub fn mean(&self) -> Option<f64> {
816 if self.count == 0 {
817 None
818 } else {
819 Some(self.sum / self.count as f64)
820 }
821 }
822 pub fn count(&self) -> usize {
824 self.count
825 }
826}
827#[allow(dead_code)]
829pub struct TransitiveClosure {
830 adj: Vec<Vec<usize>>,
831 n: usize,
832}
833#[allow(dead_code)]
834impl TransitiveClosure {
835 pub fn new(n: usize) -> Self {
837 Self {
838 adj: vec![Vec::new(); n],
839 n,
840 }
841 }
842 pub fn add_edge(&mut self, from: usize, to: usize) {
844 if from < self.n {
845 self.adj[from].push(to);
846 }
847 }
848 pub fn reachable_from(&self, start: usize) -> Vec<usize> {
850 let mut visited = vec![false; self.n];
851 let mut queue = std::collections::VecDeque::new();
852 queue.push_back(start);
853 while let Some(node) = queue.pop_front() {
854 if node >= self.n || visited[node] {
855 continue;
856 }
857 visited[node] = true;
858 for &next in &self.adj[node] {
859 queue.push_back(next);
860 }
861 }
862 (0..self.n).filter(|&i| visited[i]).collect()
863 }
864 pub fn can_reach(&self, from: usize, to: usize) -> bool {
866 self.reachable_from(from).contains(&to)
867 }
868}
869#[allow(dead_code)]
871pub struct RawFnPtr {
872 ptr: usize,
874 arity: usize,
875 name: String,
876}
877#[allow(dead_code)]
878impl RawFnPtr {
879 pub fn new(ptr: usize, arity: usize, name: impl Into<String>) -> Self {
881 Self {
882 ptr,
883 arity,
884 name: name.into(),
885 }
886 }
887 pub fn arity(&self) -> usize {
889 self.arity
890 }
891 pub fn name(&self) -> &str {
893 &self.name
894 }
895 pub fn raw(&self) -> usize {
897 self.ptr
898 }
899}
900#[allow(dead_code)]
902pub struct NonEmptyVec<T> {
903 head: T,
904 tail: Vec<T>,
905}
906#[allow(dead_code)]
907impl<T> NonEmptyVec<T> {
908 pub fn singleton(val: T) -> Self {
910 Self {
911 head: val,
912 tail: Vec::new(),
913 }
914 }
915 pub fn push(&mut self, val: T) {
917 self.tail.push(val);
918 }
919 pub fn first(&self) -> &T {
921 &self.head
922 }
923 pub fn last(&self) -> &T {
925 self.tail.last().unwrap_or(&self.head)
926 }
927 pub fn len(&self) -> usize {
929 1 + self.tail.len()
930 }
931 pub fn is_empty(&self) -> bool {
933 self.len() == 0
934 }
935 pub fn to_vec(&self) -> Vec<&T> {
937 let mut v = vec![&self.head];
938 v.extend(self.tail.iter());
939 v
940 }
941}
942#[allow(dead_code)]
944pub struct PathBuf {
945 components: Vec<String>,
946}
947#[allow(dead_code)]
948impl PathBuf {
949 pub fn new() -> Self {
951 Self {
952 components: Vec::new(),
953 }
954 }
955 pub fn push(&mut self, comp: impl Into<String>) {
957 self.components.push(comp.into());
958 }
959 pub fn pop(&mut self) {
961 self.components.pop();
962 }
963 pub fn as_str(&self) -> String {
965 self.components.join("/")
966 }
967 pub fn depth(&self) -> usize {
969 self.components.len()
970 }
971 pub fn clear(&mut self) {
973 self.components.clear();
974 }
975}
976#[derive(Debug, Clone, Default)]
978pub struct UnivConstraintSet {
979 constraints: Vec<UnivConstraint>,
980}
981impl UnivConstraintSet {
982 pub fn new() -> Self {
984 Self::default()
985 }
986 pub fn add(&mut self, c: UnivConstraint) {
988 if !self.constraints.contains(&c) {
989 self.constraints.push(c);
990 }
991 }
992 pub fn merge(&mut self, other: &Self) {
994 for c in &other.constraints {
995 self.add(c.clone());
996 }
997 }
998 pub fn len(&self) -> usize {
1000 self.constraints.len()
1001 }
1002 pub fn is_empty(&self) -> bool {
1004 self.constraints.is_empty()
1005 }
1006 pub fn check_all(&self, checker: &UnivChecker) -> Result<(), String> {
1008 for c in &self.constraints {
1009 match c {
1010 UnivConstraint::Lt(u, v) => {
1011 if !checker.is_gt(v, u) {
1012 return Err(format!(
1013 "constraint {} < {} violated",
1014 format_level(u),
1015 format_level(v)
1016 ));
1017 }
1018 }
1019 UnivConstraint::Le(u, v) => {
1020 if !checker.is_geq(v, u) {
1021 return Err(format!(
1022 "constraint {} <= {} violated",
1023 format_level(u),
1024 format_level(v)
1025 ));
1026 }
1027 }
1028 UnivConstraint::Eq(u, v) => {
1029 if !checker.is_level_def_eq(u, v) {
1030 return Err(format!(
1031 "constraint {} = {} violated",
1032 format_level(u),
1033 format_level(v)
1034 ));
1035 }
1036 }
1037 }
1038 }
1039 Ok(())
1040 }
1041 pub fn dedup(&mut self) {
1043 let mut seen = std::collections::HashSet::new();
1044 self.constraints.retain(|c| seen.insert(c.clone()));
1045 }
1046}
1047pub struct UnivChecker {
1049 constraints: Vec<UnivConstraint>,
1051 univ_vars: HashSet<Name>,
1053 mvar_assignments: HashMap<LevelMVarId, Level>,
1055 next_mvar_id: u64,
1057}
1058impl UnivChecker {
1059 pub fn new() -> Self {
1061 Self {
1062 constraints: Vec::new(),
1063 univ_vars: HashSet::new(),
1064 mvar_assignments: HashMap::new(),
1065 next_mvar_id: 0,
1066 }
1067 }
1068 pub fn add_univ_var(&mut self, name: Name) {
1070 self.univ_vars.insert(name);
1071 }
1072 pub fn add_constraint(&mut self, constraint: UnivConstraint) {
1074 self.constraints.push(constraint);
1075 }
1076 pub fn fresh_level_mvar(&mut self) -> Level {
1078 let id = LevelMVarId(self.next_mvar_id);
1079 self.next_mvar_id += 1;
1080 Level::mvar(id)
1081 }
1082 pub fn assign_mvar(&mut self, id: LevelMVarId, level: Level) {
1084 self.mvar_assignments.insert(id, level);
1085 }
1086 pub fn get_mvar_assignment(&self, id: &LevelMVarId) -> Option<&Level> {
1088 self.mvar_assignments.get(id)
1089 }
1090 pub fn instantiate_mvars(&self, l: &Level) -> Level {
1092 level::instantiate_level_mvars(l, &|id| self.mvar_assignments.get(&id).cloned())
1093 }
1094 pub fn is_level_def_eq(&self, l1: &Level, l2: &Level) -> bool {
1098 let l1_inst = self.instantiate_mvars(l1);
1099 let l2_inst = self.instantiate_mvars(l2);
1100 level::is_equivalent(&l1_inst, &l2_inst)
1101 }
1102 pub fn is_geq(&self, l1: &Level, l2: &Level) -> bool {
1104 let l1_inst = self.instantiate_mvars(l1);
1105 let l2_inst = self.instantiate_mvars(l2);
1106 level::is_geq(&l1_inst, &l2_inst)
1107 }
1108 pub fn is_gt(&self, l1: &Level, l2: &Level) -> bool {
1112 let l1_inst = self.instantiate_mvars(l1);
1113 let l2_inst = self.instantiate_mvars(l2);
1114 level::is_geq(&l1_inst, &Level::succ(l2_inst))
1115 }
1116 pub fn check(&self) -> Result<(), String> {
1118 for constraint in &self.constraints {
1119 match constraint {
1120 UnivConstraint::Lt(u, v) => {
1121 let u_inst = self.instantiate_mvars(u);
1122 let v_inst = self.instantiate_mvars(v);
1123 if !self.check_lt(&u_inst, &v_inst) {
1124 return Err(format!(
1125 "Universe constraint violated: {} < {}",
1126 u_inst, v_inst
1127 ));
1128 }
1129 }
1130 UnivConstraint::Le(u, v) => {
1131 let u_inst = self.instantiate_mvars(u);
1132 let v_inst = self.instantiate_mvars(v);
1133 if !level::is_geq(&v_inst, &u_inst) {
1134 return Err(format!(
1135 "Universe constraint violated: {} <= {}",
1136 u_inst, v_inst
1137 ));
1138 }
1139 }
1140 UnivConstraint::Eq(u, v) => {
1141 let u_inst = self.instantiate_mvars(u);
1142 let v_inst = self.instantiate_mvars(v);
1143 if !level::is_equivalent(&u_inst, &v_inst) {
1144 return Err(format!(
1145 "Universe constraint violated: {} = {}",
1146 u_inst, v_inst
1147 ));
1148 }
1149 }
1150 }
1151 }
1152 Ok(())
1153 }
1154 fn check_lt(&self, u: &Level, v: &Level) -> bool {
1156 level::is_geq(v, &Level::succ(u.clone()))
1157 }
1158 pub fn solve_simple(&mut self) -> bool {
1163 let mut changed = true;
1164 let mut any_solved = false;
1165 while changed {
1166 changed = false;
1167 let constraints = self.constraints.clone();
1168 for constraint in &constraints {
1169 if let UnivConstraint::Eq(l, r) = constraint {
1170 let l_inst = self.instantiate_mvars(l);
1171 let r_inst = self.instantiate_mvars(r);
1172 if let LevelView::MVar(id) = l_inst.view() {
1173 if !r_inst.has_mvar() {
1174 self.mvar_assignments.insert(id, r_inst);
1175 changed = true;
1176 any_solved = true;
1177 continue;
1178 }
1179 }
1180 if let LevelView::MVar(id) = r_inst.view() {
1181 if !l_inst.has_mvar() {
1182 self.mvar_assignments.insert(id, l_inst);
1183 changed = true;
1184 any_solved = true;
1185 }
1186 }
1187 }
1188 }
1189 }
1190 any_solved
1191 }
1192 pub fn all_constraints(&self) -> &[UnivConstraint] {
1194 &self.constraints
1195 }
1196 pub fn all_univ_vars(&self) -> &HashSet<Name> {
1198 &self.univ_vars
1199 }
1200 pub fn clear(&mut self) {
1202 self.constraints.clear();
1203 self.mvar_assignments.clear();
1204 }
1205 pub fn has_unassigned_mvars(&self, l: &Level) -> bool {
1207 let inst = self.instantiate_mvars(l);
1208 inst.has_mvar()
1209 }
1210}
1211#[allow(dead_code)]
1213pub struct FocusStack<T> {
1214 items: Vec<T>,
1215}
1216#[allow(dead_code)]
1217impl<T> FocusStack<T> {
1218 pub fn new() -> Self {
1220 Self { items: Vec::new() }
1221 }
1222 pub fn focus(&mut self, item: T) {
1224 self.items.push(item);
1225 }
1226 pub fn blur(&mut self) -> Option<T> {
1228 self.items.pop()
1229 }
1230 pub fn current(&self) -> Option<&T> {
1232 self.items.last()
1233 }
1234 pub fn depth(&self) -> usize {
1236 self.items.len()
1237 }
1238 pub fn is_empty(&self) -> bool {
1240 self.items.is_empty()
1241 }
1242}
1243#[allow(dead_code)]
1245pub struct StringPool {
1246 free: Vec<String>,
1247}
1248#[allow(dead_code)]
1249impl StringPool {
1250 pub fn new() -> Self {
1252 Self { free: Vec::new() }
1253 }
1254 pub fn take(&mut self) -> String {
1256 self.free.pop().unwrap_or_default()
1257 }
1258 pub fn give(&mut self, mut s: String) {
1260 s.clear();
1261 self.free.push(s);
1262 }
1263 pub fn free_count(&self) -> usize {
1265 self.free.len()
1266 }
1267}
1268#[allow(dead_code)]
1270pub struct Stopwatch {
1271 start: crate::wall_clock::Instant,
1272 splits: Vec<f64>,
1273}
1274#[allow(dead_code)]
1275impl Stopwatch {
1276 pub fn start() -> Self {
1278 Self {
1279 start: crate::wall_clock::Instant::now(),
1280 splits: Vec::new(),
1281 }
1282 }
1283 pub fn split(&mut self) {
1285 self.splits.push(self.elapsed_ms());
1286 }
1287 pub fn elapsed_ms(&self) -> f64 {
1289 self.start.elapsed().as_secs_f64() * 1000.0
1290 }
1291 pub fn splits(&self) -> &[f64] {
1293 &self.splits
1294 }
1295 pub fn num_splits(&self) -> usize {
1297 self.splits.len()
1298 }
1299}
1300#[allow(dead_code)]
1302pub struct StackCalc {
1303 stack: Vec<i64>,
1304}
1305#[allow(dead_code)]
1306impl StackCalc {
1307 pub fn new() -> Self {
1309 Self { stack: Vec::new() }
1310 }
1311 pub fn push(&mut self, n: i64) {
1313 self.stack.push(n);
1314 }
1315 fn apply_binary(&mut self, op: impl FnOnce(i64, i64) -> i64) -> Option<i64> {
1319 let (rest_len, a, b) = match self.stack[..] {
1320 [ref rest @ .., a, b] => (rest.len(), a, b),
1321 _ => return None,
1322 };
1323 let value = op(a, b);
1324 self.stack.truncate(rest_len);
1325 self.stack.push(value);
1326 Some(value)
1327 }
1328 pub fn add(&mut self) -> Option<i64> {
1332 self.apply_binary(|a, b| a + b)
1333 }
1334 pub fn sub(&mut self) -> Option<i64> {
1338 self.apply_binary(|a, b| a - b)
1339 }
1340 pub fn mul(&mut self) -> Option<i64> {
1344 self.apply_binary(|a, b| a * b)
1345 }
1346 pub fn peek(&self) -> Option<i64> {
1348 self.stack.last().copied()
1349 }
1350 pub fn depth(&self) -> usize {
1352 self.stack.len()
1353 }
1354}
1355#[allow(dead_code)]
1357pub struct FlatSubstitution {
1358 pairs: Vec<(String, String)>,
1359}
1360#[allow(dead_code)]
1361impl FlatSubstitution {
1362 pub fn new() -> Self {
1364 Self { pairs: Vec::new() }
1365 }
1366 pub fn add(&mut self, from: impl Into<String>, to: impl Into<String>) {
1368 self.pairs.push((from.into(), to.into()));
1369 }
1370 pub fn apply(&self, s: &str) -> String {
1372 let mut result = s.to_string();
1373 for (from, to) in &self.pairs {
1374 result = result.replace(from.as_str(), to.as_str());
1375 }
1376 result
1377 }
1378 pub fn len(&self) -> usize {
1380 self.pairs.len()
1381 }
1382 pub fn is_empty(&self) -> bool {
1384 self.pairs.is_empty()
1385 }
1386}
1387#[allow(dead_code)]
1389pub struct ConfigNode {
1390 key: String,
1391 value: Option<String>,
1392 children: Vec<ConfigNode>,
1393}
1394#[allow(dead_code)]
1395impl ConfigNode {
1396 pub fn leaf(key: impl Into<String>, value: impl Into<String>) -> Self {
1398 Self {
1399 key: key.into(),
1400 value: Some(value.into()),
1401 children: Vec::new(),
1402 }
1403 }
1404 pub fn section(key: impl Into<String>) -> Self {
1406 Self {
1407 key: key.into(),
1408 value: None,
1409 children: Vec::new(),
1410 }
1411 }
1412 pub fn add_child(&mut self, child: ConfigNode) {
1414 self.children.push(child);
1415 }
1416 pub fn key(&self) -> &str {
1418 &self.key
1419 }
1420 pub fn value(&self) -> Option<&str> {
1422 self.value.as_deref()
1423 }
1424 pub fn num_children(&self) -> usize {
1426 self.children.len()
1427 }
1428 pub fn lookup(&self, path: &str) -> Option<&str> {
1430 let mut parts = path.splitn(2, '.');
1431 let head = parts.next()?;
1432 let tail = parts.next();
1433 if head != self.key {
1434 return None;
1435 }
1436 match tail {
1437 None => self.value.as_deref(),
1438 Some(rest) => self.children.iter().find_map(|c| c.lookup_relative(rest)),
1439 }
1440 }
1441 fn lookup_relative(&self, path: &str) -> Option<&str> {
1442 let mut parts = path.splitn(2, '.');
1443 let head = parts.next()?;
1444 let tail = parts.next();
1445 if head != self.key {
1446 return None;
1447 }
1448 match tail {
1449 None => self.value.as_deref(),
1450 Some(rest) => self.children.iter().find_map(|c| c.lookup_relative(rest)),
1451 }
1452 }
1453}
1454#[allow(dead_code)]
1456#[allow(missing_docs)]
1457pub enum DecisionNode {
1458 Leaf(String),
1460 Branch {
1462 key: String,
1463 val: String,
1464 yes_branch: Box<DecisionNode>,
1465 no_branch: Box<DecisionNode>,
1466 },
1467}
1468#[allow(dead_code)]
1469impl DecisionNode {
1470 pub fn evaluate(&self, ctx: &std::collections::HashMap<String, String>) -> &str {
1472 match self {
1473 DecisionNode::Leaf(action) => action.as_str(),
1474 DecisionNode::Branch {
1475 key,
1476 val,
1477 yes_branch,
1478 no_branch,
1479 } => {
1480 let actual = ctx.get(key).map(|s| s.as_str()).unwrap_or("");
1481 if actual == val.as_str() {
1482 yes_branch.evaluate(ctx)
1483 } else {
1484 no_branch.evaluate(ctx)
1485 }
1486 }
1487 }
1488 }
1489 pub fn depth(&self) -> usize {
1491 match self {
1492 DecisionNode::Leaf(_) => 0,
1493 DecisionNode::Branch {
1494 yes_branch,
1495 no_branch,
1496 ..
1497 } => 1 + yes_branch.depth().max(no_branch.depth()),
1498 }
1499 }
1500}
1501#[allow(dead_code)]
1503pub struct LabelSet {
1504 labels: Vec<String>,
1505}
1506#[allow(dead_code)]
1507impl LabelSet {
1508 pub fn new() -> Self {
1510 Self { labels: Vec::new() }
1511 }
1512 pub fn add(&mut self, label: impl Into<String>) {
1514 let s = label.into();
1515 if !self.labels.contains(&s) {
1516 self.labels.push(s);
1517 }
1518 }
1519 pub fn has(&self, label: &str) -> bool {
1521 self.labels.iter().any(|l| l == label)
1522 }
1523 pub fn count(&self) -> usize {
1525 self.labels.len()
1526 }
1527 pub fn all(&self) -> &[String] {
1529 &self.labels
1530 }
1531}