1 
use std::collections::HashSet;
2 

            

        

            

                3
            

            

                
            

            

                
use merc_syntax::DefId;

            

        

            

                4
            

            

                
            

            

                
use merc_syntax::IdDecl;

            

        

            

                5
            

            

                
            

            

                
use merc_syntax::SortExpression;

            

        

            

                6
            

            

                
            

            

                
use merc_syntax::UntypedDataSpecification;

            

        

            

                7
            

            

                
            

            

                

            

        

            

                8
            

            

                
            

            

                
use crate::argument_sorts;

            

        

            

                9
            

            

                
            

            

                
use crate::target_sort;

            

        

            

                10
            

            

                
            

            

                

            

        

            

                11
            

            

                
            

            

                
/// Returns true iff the sort is syntactically non-empty, i.e., there is at

            

        

            

                12
            

            

                
            

            

                
/// least one constructor for the target sort that has a non-empty sort.

            

        

            

                13
            

            

                1
            

            

                
pub fn is_nonempty_sort(sort: &str, spec: &UntypedDataSpecification) -> bool {

            

        

            

                14
            

            

                1
            

            

                
    debug_assert!(

            

        

            

                15
            

            

                1
            

            

                
        spec.sort_declarations.iter().any(|id| id.id.is_some()),

            

        

            

                16
            

            

                
            

            

                
        "The sorts must be resolved"

            

        

            

                17
            

            

                
            

            

                
    );

            

        

            

                18
            

            

                
            

            

                

            

        

            

                19
            

            

                1
            

            

                
    let sort_id = spec

            

        

            

                20
            

            

                1
            

            

                
        .sort_declarations

            

        

            

                21
            

            

                1
            

            

                
        .iter()

            

        

            

                22
            

            

                1
            

            

                
        .find(|id| id.identifier == sort)

            

        

            

                23
            

            

                1
            

            

                
        .expect("The sort should be declared")

            

        

            

                24
            

            

                
            

            

                
        .id

            

        

            

                25
            

            

                1
            

            

                
        .unwrap();

            

        

            

                26
            

            

                
            

            

                

            

        

            

                27
            

            

                1
            

            

                
    let mut seen = HashSet::new();

            

        

            

                28
            

            

                1
            

            

                
    is_nonempty_sort_rec(sort_id, &spec.constructor_declarations, &mut seen)

            

        

            

                29
            

            

                1
            

            

                
}

            

        

            

                30
            

            

                
            

            

                

            

        

            

                31
            

            

                
            

            

                
/// The recursive definition of non-emptiness.

            

        

            

                32
            

            

                2
            

            

                
fn is_nonempty_sort_rec(sort: DefId, constructors: &Vec<IdDecl>, seen: &mut HashSet<DefId>) -> bool {

            

        

            

                33
            

            

                2
            

            

                
    if seen.contains(&sort) {

            

        

            

                34
            

            

                1
            

            

                
        return false; // We have already seen this sort, so we have a cycle.

            

        

            

                35
            

            

                1
            

            

                
    }

            

        

            

                36
            

            

                
            

            

                

            

        

            

                37
            

            

                1
            

            

                
    for constructor in constructors.iter().filter(|id| {

            

        

            

                38
            

            

                1
            

            

                
        if let SortExpression::Resolved(_, id) = target_sort(&id.sort) {

            

        

            

                39
            

            

                1
            

            

                
            *id == sort

            

        

            

                40
            

            

                
            

            

                
        } else {

            

        

            

                41
            

            

                
            

            

                
            unreachable!(

            

        

            

                42
            

            

                
            

            

                
                "The target sort of a constructor should always be a reference sort, but is not for {:?}",

            

        

            

                43
            

            

                
            

            

                
                id.sort

            

        

            

                44
            

            

                
            

            

                
            )

            

        

            

                45
            

            

                
            

            

                
        }

            

        

            

                46
            

            

                1
            

            

                
    }) {

            

        

            

                47
            

            

                1
            

            

                
        if argument_sorts(&constructor.sort).is_empty() {

            

        

            

                48
            

            

                
            

            

                
            return true; // We have found a constructor with no arguments, so the sort is non-empty.

            

        

            

                49
            

            

                1
            

            

                
        }

            

        

            

                50
            

            

                
            

            

                

            

        

            

                51
            

            

                1
            

            

                
        seen.insert(sort); // Mark the current sort as seen to avoid cycles.

            

        

            

                52
            

            

                
            

            

                

            

        

            

                53
            

            

                1
            

            

                
        if argument_sorts(&constructor.sort).iter().all(|arg| match arg {

            

        

            

                54
            

            

                1
            

            

                
            SortExpression::Resolved(_, id) => is_nonempty_sort_rec(*id, constructors, seen),

            

        

            

                55
            

            

                
            

            

                
            _ => true,

            

        

            

                56
            

            

                1
            

            

                
        }) {

            

        

            

                57
            

            

                
            

            

                
            return true; // All argument sorts are non-empty, so the sort is non-empty.

            

        

            

                58
            

            

                1
            

            

                
        }

            

        

            

                59
            

            

                
            

            

                

            

        

            

                60
            

            

                1
            

            

                
        seen.remove(&sort); // Unmark the current sort as seen to allow other paths to explore it.        

            

        

            

                61
            

            

                
            

            

                
    }

            

        

            

                62
            

            

                
            

            

                

            

        

            

                63
            

            

                1
            

            

                
    false

            

        

            

                64
            

            

                2
            

            

                
}

            

        

            

                65
            

            

                
            

            

                

            

        

            

                66
            

            

                
            

            

                
#[cfg(test)]

            

        

            

                67
            

            

                
            

            

                
mod tests {

            

        

            

                68
            

            

                
            

            

                
    use merc_syntax::UntypedDataSpecification;

            

        

            

                69
            

            

                
            

            

                

            

        

            

                70
            

            

                
            

            

                
    use crate::DataSpecification;

            

        

            

                71
            

            

                
            

            

                
    use crate::WellTypedError;

            

        

            

                72
            

            

                
            

            

                

            

        

            

                73
            

            

                
            

            

                
    #[test]

            

        

            

                74
            

            

                1
            

            

                
    fn test_empty_data_spec() {

            

        

            

                75
            

            

                1
            

            

                
        let spec = UntypedDataSpecification::parse(

            

        

            

                76
            

            

                1
            

            

                
            "

            

        

            

                77
            

            

                1
            

            

                
            sort D;

            

        

            

                78
            

            

                1
            

            

                
            cons f: D -> D;

            

        

            

                79
            

            

                1
            

            

                
        ",

            

        

            

                80
            

            

                
            

            

                
        )

            

        

            

                81
            

            

                1
            

            

                
        .unwrap();

            

        

            

                82
            

            

                
            

            

                

            

        

            

                83
            

            

                1
            

            

                
        match DataSpecification::from_untyped(spec) {

            

        

            

                84
            

            

                1
            

            

                
            Err(WellTypedError::EmptySort { sort }) if sort == "D" => {}

            

        

            

                85
            

            

                
            

            

                
            Err(other) => panic!("Unexpected {:?}", other),

            

        

            

                86
            

            

                
            

            

                
            _ => panic!("Unexpected from_untyped to fail"),

            

        

            

                87
            

            

                
            

            

                
        }

            

        

            

                88
            

            

                1
            

            

                
    }

            

        

            

                89
            

            

                
            

            

                
}