mlsub 0.1.0

Template.
Documentation 
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

use itertools::Itertools;
use proptest::collection::vec;
use proptest::test_runner::Config;
use proptest::{prop_assert_eq, proptest};

use crate::auto::Automaton;
use crate::biunify::reference::{self, arb_constraint};
use crate::polar::Ty;
use crate::tests::Constructed;
use crate::Polarity;

#[test]
fn constructed() {
    let mut auto = Automaton::new();

    let mut builder = auto.builder();
    let lhs_id = builder.build_polar(
        Polarity::Pos,
        &Ty::Constructed(Constructed::Record(Default::default())),
    );
    let rhs_id = builder.build_polar(
        Polarity::Neg,
        &Ty::Add(
            Box::new(Ty::Zero),
            Box::new(Ty::Constructed(Constructed::Bool)),
        ),
    );
    drop(builder);

    assert!(auto.biunify(lhs_id, rhs_id).is_err());
}

proptest! {
    #![proptest_config(Config {
        cases: 1024,
        timeout: 10000,
        ..Config::default()
    })]

    #[test]
    fn biunify(con in arb_constraint()) {
        let mut auto = Automaton::new();

        let mut builder = auto.builder();
        let lhs_id = builder.build_polar(Polarity::Pos, &con.0);
        let rhs_id = builder.build_polar(Polarity::Neg, &con.1);
        drop(builder);

        prop_assert_eq!(
            auto.biunify(lhs_id, rhs_id).is_ok(),
            reference::biunify(con).is_ok()
        );
    }

    #[test]
    fn biunify_reduced(con in arb_constraint()) {
        let mut auto = Automaton::new();

        let mut builder = auto.builder();
        let lhs_id = builder.build_polar(Polarity::Pos, &con.0);
        let rhs_id = builder.build_polar(Polarity::Neg, &con.1);
        drop(builder);

        let mut reduced = Automaton::new();
        let dfa_ids: Vec<_> = reduced.reduce(&auto, [(lhs_id, Polarity::Pos), (rhs_id, Polarity::Neg)].iter().cloned()).collect();

        prop_assert_eq!(
            reduced.biunify(dfa_ids[0], dfa_ids[1]).is_ok(),
            reference::biunify(con).is_ok()
        );
    }
}

proptest! {
    #![proptest_config(Config {
        cases: 256,
        timeout: 10000,
        ..Config::default()
    })]

    #[test]
    fn biunify_all(cons in vec(arb_constraint(), 0..16)) {
        let mut auto = Automaton::new();

        let mut builder = auto.builder();
        let ids: Vec<_> = cons.iter().map(|con| {
            let lhs_id = builder.build_polar(Polarity::Pos, &con.0);
            let rhs_id = builder.build_polar(Polarity::Neg, &con.1);
            (lhs_id, rhs_id)
        }).collect();
        drop(builder);

        prop_assert_eq!(
            auto.biunify_all(ids).is_ok(),
            reference::biunify_all(cons).is_ok()
        );
    }

    #[test]
    fn biunify_all_reduced(cons in vec(arb_constraint(), 0..16)) {
        let mut auto = Automaton::new();

        let mut builder = auto.builder();
        let ids: Vec<_> = cons.iter().flat_map(|con| {
            let lhs_id = builder.build_polar(Polarity::Pos, &con.0);
            let rhs_id = builder.build_polar(Polarity::Neg, &con.1);
            vec![(lhs_id, Polarity::Pos), (rhs_id, Polarity::Neg)]
        }).collect();
        drop(builder);

        let mut reduced = Automaton::new();
        let dfa_ids = reduced.reduce(&auto, ids);

        prop_assert_eq!(
            reduced.biunify_all(dfa_ids.tuples()).is_ok(),
            reference::biunify_all(cons).is_ok()
        );
    }
}