1
use std::cmp::min;
2
use std::fmt;
3

            
4
use crate::utilities::DataPosition;
5
use ahash::HashMap;
6
use ahash::HashMapExt;
7
use log::trace;
8

            
9
use super::MatchAnnouncement;
10
use super::MatchObligation;
11

            
12
/// A match goal contains a number of obligations (positions that must still be
13
/// matched) and the corresponding rule that can be announced as being a match.
14
#[derive(Clone, Eq, Hash, Ord, PartialEq, PartialOrd)]
15
pub struct MatchGoal {
16
    pub obligations: Vec<MatchObligation>,
17
    pub announcement: MatchAnnouncement,
18
}
19

            
20
impl MatchGoal {
21
1560
    pub fn new(announcement: MatchAnnouncement, obligations: Vec<MatchObligation>) -> Self {
22
1560
        Self {
23
1560
            obligations,
24
1560
            announcement,
25
1560
        }
26
1560
    }
27

            
28
    /// Derive the greatest common prefix of the announcement and obligation positions
29
    /// of a list of match goals.
30
46652
    pub fn greatest_common_prefix(goals: &Vec<MatchGoal>) -> DataPosition {
31
        // gcp is empty if there are no match goals
32
46652
        if goals.is_empty() {
33
            return DataPosition::empty();
34
46652
        }
35

            
36
        // Initialise the prefix with the first match goal, can only shrink afterwards
37
46652
        let first_match_pos = &goals.first().unwrap().announcement.position;
38
46652
        let mut gcp_length = first_match_pos.len();
39
46652
        let prefix = &first_match_pos.clone();
40

            
41
2589776
        for g in goals {
42
            // Compare up to gcp_length or the length of the announcement position
43
2589776
            let compare_length = min(gcp_length, g.announcement.position.len());
44
            // gcp_length shrinks if they are not the same up to compare_length
45
2589776
            gcp_length = MatchGoal::common_prefix_length(
46
2589776
                &prefix.indices()[0..compare_length],
47
2589776
                &g.announcement.position.indices()[0..compare_length],
48
2589776
            );
49

            
50
2615248
            for mo in &g.obligations {
51
2615248
                // Compare up to gcp_length or the length of the match obligation position
52
2615248
                let compare_length = min(gcp_length, mo.position.len());
53
2615248
                // gcp_length shrinks if they are not the same up to compare_length
54
2615248
                gcp_length = MatchGoal::common_prefix_length(
55
2615248
                    &prefix.indices()[0..compare_length],
56
2615248
                    &mo.position.indices()[0..compare_length],
57
2615248
                );
58
2615248
            }
59
        }
60

            
61
        // The gcp is constructed by taking the first gcp_length indices of the first match goal prefix
62
46652
        DataPosition::new(&prefix.indices()[0..gcp_length])
63
46652
    }
64

            
65
    /// Removes the first len position indices of the match goal and obligation positions
66
46652
    pub fn remove_prefix(mut goals: Vec<MatchGoal>, len: usize) -> Vec<MatchGoal> {
67
2589776
        for goal in &mut goals {
68
            // update match announcement
69
2589776
            goal.announcement.position = DataPosition::new(&goal.announcement.position.indices()[len..]);
70
2615248
            for mo_index in 0..goal.obligations.len() {
71
2615248
                let shortened = DataPosition::new(&goal.obligations.get(mo_index).unwrap().position.indices()[len..]);
72
2615248
                goal.obligations.get_mut(mo_index).unwrap().position = shortened;
73
2615248
            }
74
        }
75
46652
        goals
76
46652
    }
77

            
78
    /// Returns a Vec where each element is a partition containing the goals and
79
    /// the positions. This partitioning can be done in multiple ways, but
80
    /// currently match goals are equivalent when their match announcements have
81
    /// a comparable position.
82
34429
    pub fn partition(goals: Vec<MatchGoal>) -> Vec<(Vec<MatchGoal>, Vec<DataPosition>)> {
83
34429
        let mut partitions = vec![];
84

            
85
34429
        trace!("=== partition(match_goals = [ ===");
86
2589776
        for mg in &goals {
87
2589776
            trace!("\t {mg:?}");
88
        }
89
34429
        trace!("]");
90

            
91
        // If one of the goals has a root position all goals are related.
92
2550011
        partitions = if goals.iter().any(|g| g.announcement.position.is_empty()) {
93
1530
            let mut all_positions = Vec::new();
94
59584
            for g in &goals {
95
59584
                if !all_positions.contains(&g.announcement.position) {
96
3653
                    all_positions.push(g.announcement.position.clone())
97
55931
                }
98
            }
99
1530
            partitions.push((goals, all_positions));
100
1530
            partitions
101
        } else {
102
            // Create a mapping from positions to goals, goals are represented with an index
103
            // on function parameter goals
104
32899
            let mut position_to_goals = HashMap::new();
105
2530192
            for (i, g) in goals.iter().enumerate() {
106
2530192
                if !position_to_goals.contains_key(&g.announcement.position) {
107
68879
                    position_to_goals.insert(g.announcement.position.clone(), vec![i]);
108
2461313
                } else {
109
2461313
                    let vec = position_to_goals.get_mut(&g.announcement.position).unwrap();
110
2461313
                    vec.push(i);
111
2461313
                }
112
            }
113

            
114
            // Sort the positions. They are now in depth first order.
115
32899
            let mut all_positions: Vec<DataPosition> = position_to_goals.keys().cloned().collect();
116
32899
            all_positions.sort_unstable();
117

            
118
            // Compute the partitions, finished when all positions are processed
119
32899
            let mut p_index = 0; // position index
120
78021
            while p_index < all_positions.len() {
121
                // Start the partition with a position
122
45122
                let p = &all_positions[p_index];
123
45122
                let mut pos_in_partition = vec![p.clone()];
124
45122
                let mut goals_in_partition = vec![];
125

            
126
                // put the goals with position p in the partition
127
45122
                let g = position_to_goals.get(p).unwrap();
128
1537409
                for i in g {
129
1537409
                    goals_in_partition.push(goals[*i].clone());
130
1537409
                }
131

            
132
                // Go over the positions until we find a position that is not comparable to p
133
                // Because all_positions is sorted we know that once we find a position that is not comparable
134
                // all subsequent positions will also not be comparable.
135
                // Moreover, all positions in the partition are related to p. p is the highest in the partition.
136
45122
                p_index += 1;
137
68879
                while p_index < all_positions.len() && MatchGoal::pos_comparable(p, &all_positions[p_index]) {
138
23757
                    pos_in_partition.push(all_positions[p_index].clone());
139
                    // Put the goals with position all_positions[p_index] in the partition
140
23757
                    let g = position_to_goals.get(&all_positions[p_index]).unwrap();
141
992783
                    for i in g {
142
992783
                        goals_in_partition.push(goals[*i].clone());
143
992783
                    }
144
23757
                    p_index += 1;
145
                }
146

            
147
45122
                partitions.push((goals_in_partition, pos_in_partition));
148
            }
149

            
150
32899
            partitions
151
        };
152

            
153
46652
        for (goals, pos) in &partitions {
154
46652
            trace!("pos {{");
155
72532
            for mg in pos {
156
72532
                trace!("\t {mg}");
157
            }
158
46652
            trace!("}} -> {{");
159
2589776
            for mg in goals {
160
2589776
                trace!("\t {mg:?}");
161
            }
162
46652
            trace!("}}");
163
        }
164

            
165
34429
        partitions
166
34429
    }
167

            
168
    // Assumes two slices are of the same length and computes to what length they are equal
169
5205024
    fn common_prefix_length(pos1: &[usize], pos2: &[usize]) -> usize {
170
5205024
        debug_assert_eq!(pos1.len(), pos2.len(), "Given arrays should be of the same length.");
171

            
172
5205024
        let mut common_length = 0;
173
7087664
        for i in 0..pos1.len() {
174
7087664
            if pos1.get(i).unwrap() == pos2.get(i).unwrap() {
175
7087533
                common_length += 1;
176
7087533
            } else {
177
131
                break;
178
            }
179
        }
180
5205024
        common_length
181
5205024
    }
182

            
183
    /// Checks for two positions whether one is a subposition of the other.
184
    /// For example 2.2.3 and 2 are comparable. 2.2.3 and 1 are not.
185
122510
    pub fn pos_comparable(p1: &DataPosition, p2: &DataPosition) -> bool {
186
122510
        let mut index = 0;
187
        loop {
188
183044
            if p1.len() == index || p2.len() == index {
189
41549
                return true;
190
141495
            }
191

            
192
141495
            if p1.indices()[index] != p2.indices()[index] {
193
80961
                return false;
194
60534
            }
195
60534
            index += 1;
196
        }
197
122510
    }
198
}
199

            
200
impl fmt::Debug for MatchGoal {
201
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
202
        let mut first = true;
203
        for obligation in &self.obligations {
204
            if !first {
205
                write!(f, ", ")?;
206
            }
207
            write!(f, "{obligation:?}")?;
208
            first = false;
209
        }
210

            
211
        write!(f, " ↪ {:?}", self.announcement)
212
    }
213
}