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
4710
    pub fn new(announcement: MatchAnnouncement, obligations: Vec<MatchObligation>) -> Self {
22
4710
        Self {
23
4710
            obligations,
24
4710
            announcement,
25
4710
        }
26
4710
    }
27

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

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

            
41
7769328
        for g in goals {
42
            // Compare up to gcp_length or the length of the announcement position
43
7769328
            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
7769328
            gcp_length = MatchGoal::common_prefix_length(
46
7769328
                &prefix.indices()[0..compare_length],
47
7769328
                &g.announcement.position.indices()[0..compare_length],
48
7769328
            );
49

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

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

            
65
    /// Removes the first len position indices of the match goal and obligation positions
66
139956
    pub fn remove_prefix(mut goals: Vec<MatchGoal>, len: usize) -> Vec<MatchGoal> {
67
7769328
        for goal in &mut goals {
68
            // update match announcement
69
7769328
            goal.announcement.position = DataPosition::new(&goal.announcement.position.indices()[len..]);
70
7845744
            for mo_index in 0..goal.obligations.len() {
71
7845744
                let shortened = DataPosition::new(&goal.obligations.get(mo_index).unwrap().position.indices()[len..]);
72
7845744
                goal.obligations.get_mut(mo_index).unwrap().position = shortened;
73
7845744
            }
74
        }
75
139956
        goals
76
139956
    }
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
103302
    pub fn partition(goals: Vec<MatchGoal>) -> Vec<(Vec<MatchGoal>, Vec<DataPosition>)> {
83
103302
        let mut partitions = vec![];
84

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

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

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

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

            
126
                // put the goals with position p in the partition
127
135366
                let g = position_to_goals.get(p).unwrap();
128
4612227
                for i in g {
129
4612227
                    goals_in_partition.push(goals[*i].clone());
130
4612227
                }
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
135366
                p_index += 1;
137
206637
                while p_index < all_positions.len() && MatchGoal::pos_comparable(p, &all_positions[p_index]) {
138
71271
                    pos_in_partition.push(all_positions[p_index].clone());
139
                    // Put the goals with position all_positions[p_index] in the partition
140
71271
                    let g = position_to_goals.get(&all_positions[p_index]).unwrap();
141
2978349
                    for i in g {
142
2978349
                        goals_in_partition.push(goals[*i].clone());
143
2978349
                    }
144
71271
                    p_index += 1;
145
                }
146

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

            
150
98712
            partitions
151
        };
152

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

            
165
103302
        partitions
166
103302
    }
167

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

            
172
15615072
        let mut common_length = 0;
173
21243924
        for i in 0..pos1.len() {
174
21243924
            if pos1.get(i).unwrap() == pos2.get(i).unwrap() {
175
21243531
                common_length += 1;
176
21243531
            } else {
177
393
                break;
178
            }
179
        }
180
15615072
        common_length
181
15615072
    }
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
367431
    pub fn pos_comparable(p1: &DataPosition, p2: &DataPosition) -> bool {
186
367431
        let mut index = 0;
187
        loop {
188
549033
            if p1.len() == index || p2.len() == index {
189
124647
                return true;
190
424386
            }
191

            
192
424386
            if p1.indices()[index] != p2.indices()[index] {
193
242784
                return false;
194
181602
            }
195
181602
            index += 1;
196
        }
197
367431
    }
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
}