pub fn greatest_common_prefix(goals: &Vec<MatchGoal>) -> ExplicitPosition {

        // gcp is empty if there are no match goals

        if goals.is_empty() {

        }

        // Initialise the prefix with the first match goal, can only shrink afterwards

        let first_match_pos = &goals.first().unwrap().announcement.position;

        let mut gcp_length = first_match_pos.len();

        let prefix = &first_match_pos.clone();

        for g in goals {

            let compare_length = min(gcp_length, g.announcement.position.len());

            // gcp_length shrinks if they are not the same up to compare_length

            gcp_length = MatchGoal::common_prefix_length(

                &prefix.indices[0..compare_length],

                &g.announcement.position.indices[0..compare_length],

            );

            for mo in &g.obligations {

                // Compare up to gcp_length or the length of the match obligation position

                let compare_length = min(gcp_length, mo.position.len());

                // gcp_length shrinks if they are not the same up to compare_length

                gcp_length = MatchGoal::common_prefix_length(

                    &prefix.indices[0..compare_length],

                    &mo.position.indices[0..compare_length],

                );

            }

        let greatest_common_prefix = SmallVec::from_slice(&prefix.indices[0..gcp_length]);

        ExplicitPosition {

            indices: greatest_common_prefix,

        }

    }

    pub fn remove_prefix(mut goals: Vec<MatchGoal>, len: usize) -> Vec<MatchGoal> {

        for goal in &mut goals {

            goal.announcement.position = ExplicitPosition {

                indices: SmallVec::from_slice(&goal.announcement.position.indices[len..]),

            };

            for mo_index in 0..goal.obligations.len() {

                let shortened = ExplicitPosition {

                    indices: SmallVec::from_slice(&goal.obligations.get(mo_index).unwrap().position.indices[len..]),

                };

                goal.obligations.get_mut(mo_index).unwrap().position = shortened;

            }

        goals

    }

    pub fn partition(goals: Vec<MatchGoal>) -> Vec<(Vec<MatchGoal>, Vec<ExplicitPosition>)> {

        let mut partitions = vec![];

        trace!("=== partition(match_goals = [ ===");

        for mg in &goals {

            trace!("\t {}", mg);

        trace!("]");

        partitions = if goals.iter().any(|g| g.announcement.position.is_empty()) {

            let mut all_positions = Vec::new();

            for g in &goals {

                if !all_positions.contains(&g.announcement.position) {

                    all_positions.push(g.announcement.position.clone())

                }

            partitions.push((goals, all_positions));

            partitions

            let mut position_to_goals = HashMap::new();

            for (i, g) in goals.iter().enumerate() {

                if !position_to_goals.contains_key(&g.announcement.position) {

                    position_to_goals.insert(g.announcement.position.clone(), vec![i]);

                } else {

                    let vec = position_to_goals.get_mut(&g.announcement.position).unwrap();

                    vec.push(i);

                }

            let mut all_positions: Vec<ExplicitPosition> = position_to_goals.keys().cloned().collect();

            all_positions.sort_unstable();

            // Compute the partitions, finished when all positions are processed

            let mut p_index = 0; // position index

            while p_index < all_positions.len() {

                let p = &all_positions[p_index];

                let mut pos_in_partition = vec![p.clone()];

                let mut goals_in_partition = vec![];

                // put the goals with position p in the partition

                let g = position_to_goals.get(p).unwrap();

                for i in g {

                    goals_in_partition.push(goals[*i].clone());

                }

                p_index += 1;

                while p_index < all_positions.len() && MatchGoal::pos_comparable(p, &all_positions[p_index]) {

                    pos_in_partition.push(all_positions[p_index].clone());

                    // Put the goals with position all_positions[p_index] in the partition

                    let g = position_to_goals.get(&all_positions[p_index]).unwrap();

                    for i in g {

                        goals_in_partition.push(goals[*i].clone());

                    }

                    p_index += 1;

                partitions.push((goals_in_partition, pos_in_partition));

            partitions

        for (goals, pos) in &partitions {

            trace!("pos {{");

            for mg in pos {

                trace!("\t {}", mg);

            trace!("}} -> {{");

            for mg in goals {

                trace!("\t {}", mg);

            trace!("}}");

        partitions

    }

    fn common_prefix_length(pos1: &[usize], pos2: &[usize]) -> usize {

        debug_assert_eq!(pos1.len(), pos2.len(), "Given arrays should be of the same length.");

        let mut common_length = 0;

        for i in 0..pos1.len() {

            if pos1.get(i).unwrap() == pos2.get(i).unwrap() {

                common_length += 1;

            } else {

                break;

        common_length

    }

    pub fn pos_comparable(p1: &ExplicitPosition, p2: &ExplicitPosition) -> bool {

        let mut index = 0;

            if p1.len() == index || p2.len() == index {

                return true;

            }

            if p1.indices[index] != p2.indices[index] {

                return false;

            }

            index += 1;

    }