1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134

//!

use crate::infer::InferenceTable;
use chalk_ir::interner::Interner;
use chalk_ir::visit::{TypeSuperVisitable, TypeVisitable, TypeVisitor};
use chalk_ir::*;
use std::cmp::max;
use std::ops::ControlFlow;

/// "Truncation" (called "abstraction" in the papers referenced below)
/// refers to the act of modifying a goal or answer that has become
/// too large in order to guarantee termination.
///
/// Currently we don't perform truncation (but it might me readded later).
///
/// Citations:
///
/// - Terminating Evaluation of Logic Programs with Finite Three-Valued Models
///   - Riguzzi and Swift; ACM Transactions on Computational Logic 2013
/// - Radial Restraint
///   - Grosof and Swift; 2013
pub fn needs_truncation<I: Interner>(
    interner: I,
    infer: &mut InferenceTable<I>,
    max_size: usize,
    value: impl TypeVisitable<I>,
) -> bool {
    let mut visitor = TySizeVisitor::new(interner, infer);
    value.visit_with(&mut visitor, DebruijnIndex::INNERMOST);

    visitor.max_size > max_size
}

struct TySizeVisitor<'infer, I: Interner> {
    interner: I,
    infer: &'infer mut InferenceTable<I>,
    size: usize,
    depth: usize,
    max_size: usize,
}

impl<'infer, I: Interner> TySizeVisitor<'infer, I> {
    fn new(interner: I, infer: &'infer mut InferenceTable<I>) -> Self {
        Self {
            interner,
            infer,
            size: 0,
            depth: 0,
            max_size: 0,
        }
    }
}

impl<'infer, I: Interner> TypeVisitor<I> for TySizeVisitor<'infer, I> {
    type BreakTy = ();

    fn as_dyn(&mut self) -> &mut dyn TypeVisitor<I, BreakTy = Self::BreakTy> {
        self
    }

    fn visit_ty(&mut self, ty: &Ty<I>, outer_binder: DebruijnIndex) -> ControlFlow<()> {
        if let Some(normalized_ty) = self.infer.normalize_ty_shallow(self.interner, ty) {
            normalized_ty.visit_with(self, outer_binder);
            return ControlFlow::Continue(());
        }

        self.size += 1;
        self.max_size = max(self.size, self.max_size);

        self.depth += 1;
        ty.super_visit_with(self, outer_binder);
        self.depth -= 1;

        // When we get back to the first invocation, clear the counters.
        // We process each outermost type independently.
        if self.depth == 0 {
            self.size = 0;
        }
        ControlFlow::Continue(())
    }

    fn interner(&self) -> I {
        self.interner
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    use chalk_integration::{arg, ty};

    #[test]
    fn one_type() {
        use chalk_integration::interner::ChalkIr;
        let interner = ChalkIr;
        let mut table = InferenceTable::<chalk_integration::interner::ChalkIr>::new();
        let _u1 = table.new_universe();

        // Vec<Vec<Vec<Vec<T>>>>
        let ty0 = ty!(apply (item 0)
                      (apply (item 0)
                       (apply (item 0)
                        (apply (item 0)
                         (placeholder 1)))));

        let mut visitor = TySizeVisitor::new(interner, &mut table);
        ty0.visit_with(&mut visitor, DebruijnIndex::INNERMOST);
        assert!(visitor.max_size == 5);
    }

    #[test]
    fn multiple_types() {
        use chalk_integration::interner::ChalkIr;
        let interner = ChalkIr;
        let mut table = InferenceTable::<chalk_integration::interner::ChalkIr>::new();
        let _u1 = table.new_universe();

        // Vec<Vec<Vec<Vec<T>>>>
        let ty0 = ty!(apply (item 0)
                      (apply (item 0)
                       (apply (item 0)
                        (apply (item 0)
                         (placeholder 1)))));

        let ty1 = ty!(apply (item 0)
                      (apply (item 0)
                       (apply (item 0)
                        (placeholder 1))));

        let mut visitor = TySizeVisitor::new(interner, &mut table);
        vec![&ty0, &ty1].visit_with(&mut visitor, DebruijnIndex::INNERMOST);
        assert!(visitor.max_size == 5);
    }
}