false/
false.rs

1#[macro_use]
2extern crate terms;
3#[macro_use]
4extern crate tree_automata as ta;
5extern crate automatic_relations as automatic;
6
7use std::cell::Cell;
8use std::cmp::Ord;
9use std::fmt;
10use std::collections::HashSet;
11use terms::{
12	Term,
13	Pattern,
14	Var,
15	variable::{
16		Spawnable,
17		Family,
18		Parented
19	}
20};
21use ta::{
22    Symbol,
23    State,
24    Sorted,
25    NoLabel,
26    Rank,
27    Ranked,
28    bottom_up::{
29        Automaton,
30        Configuration,
31        // LanguageState,
32        width_search::TermFragment
33    }
34};
35
36use automatic::{
37    Relation,
38    Convolution,
39    Convoluted,
40    MaybeBottom,
41    convolution::aligned
42};
43
44struct PList<'a, T: fmt::Display>(&'a [T]);
45
46impl<'a, T: fmt::Display> fmt::Display for PList<'a, T> {
47    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
48        match self.0.split_first() {
49            Some((head, tail)) => {
50                head.fmt(f)?;
51                for e in tail.iter() {
52                    write!(f, ",")?;
53                    e.fmt(f)?;
54                }
55                Ok(())
56            },
57            None => Ok(())
58        }
59    }
60}
61
62fn assert_multi_search<F: Ranked + Symbol + Ord, Q: State, X: Family + Ord>(automata: &[&Automaton<Rank<Convoluted<F>>, Q, NoLabel>], mut patterns: Vec<Vec<Pattern<F, X>>>, mut expected_output: Vec<Vec<Term<Rank<Convoluted<F>>>>>) {
63    // prepare the patterns.
64    let convoluted_patterns = patterns.drain(..).map(|patterns| {
65        Convoluted(patterns.into_iter().map(|p| MaybeBottom::Some(p)).collect())
66    }).collect();
67
68    let it = aligned::multi_search(automata, convoluted_patterns, None);
69
70    let mut output: Vec<Vec<Term<Rank<Convoluted<F>>>>> = Vec::with_capacity(expected_output.len());
71    for terms in it {
72		let terms = terms.unwrap();
73
74        #[cfg(debug_assertions)]
75        {
76            if output.len() >= expected_output.len() {
77                for terms in output.iter() {
78                    println!("FOUND {}", PList(terms));
79                }
80                println!("FOUND {}", PList(&terms));
81            }
82        }
83        assert!(output.len() < expected_output.len());
84        output.push(terms)
85    }
86
87    let mut expected_output_set = HashSet::new();
88    for e in expected_output.drain(..) {
89        expected_output_set.insert(e);
90    }
91
92    #[cfg(debug_assertions)]
93    {
94        if output.len() != expected_output_set.len() {
95            println!("EXPECTED OUTPUT:");
96            for terms in expected_output_set.iter() {
97                println!("{}", PList(terms));
98            }
99            println!("\nOUTPUT:");
100            for terms in output.iter() {
101                println!("{}", PList(terms));
102            }
103        }
104    }
105
106    assert!(output.len() == expected_output_set.len());
107
108    for terms in output.iter() {
109        #[cfg(debug_assertions)]
110        {
111            if !expected_output_set.contains(terms) {
112                println!("UNEXPECTED TERM: {}", PList(terms));
113            }
114        }
115
116        assert!(expected_output_set.contains(terms));
117    }
118}
119
120fn main() {
121    let a = Rank("a", 0);
122    let b = Rank("b", 0);
123
124    let nil = Rank("nil", 0);
125    let cons = Rank("cons", 2);
126
127    let a_conv = Rank(Convoluted(vec![MaybeBottom::Some(a)]), 0);
128    let b_conv = Rank(Convoluted(vec![MaybeBottom::Some(b)]), 0);
129    let nil_conv = Rank(Convoluted(vec![MaybeBottom::Some(nil)]), 0);
130    let cons_conv = Rank(Convoluted(vec![MaybeBottom::Some(cons)]), 2);
131
132    let mut prop_all_false = automaton! {
133        b_conv -> "0:Bool",
134        cons_conv("0:List", "0:Bool") -> "0:List",
135        nil_conv -> "0:List",
136
137        finals "0:List"
138    };
139
140    let mut prop_sorted = automaton! {
141        cons_conv("_:List", "_:Bool") -> "_:List",
142        cons_conv("1:List", "_:Bool") -> "_:List",
143        cons_conv("2:List", "0:Bool") -> "_:List",
144        cons_conv("_:List", "1:Bool") -> "_:List",
145        cons_conv("_:List", "0:Bool") -> "_:List",
146        cons_conv("0:List", "_:Bool") -> "_:List",
147        cons_conv("2:List", "1:Bool") -> "_:List",
148        cons_conv("2:List", "_:Bool") -> "_:List",
149        cons_conv("1:List", "0:Bool") -> "2:List",
150        a_conv -> "1:Bool",
151        nil_conv -> "0:List",
152        cons_conv("0:List", "0:Bool") -> "1:List",
153        cons_conv("0:List", "1:Bool") -> "1:List",
154        cons_conv("1:List", "1:Bool") -> "1:List",
155        b_conv -> "0:Bool",
156
157        finals "_:List" "2:List"
158    };
159
160    let namespace = Cell::new(0);
161    let x: Parented<Var<_>> = Parented::spawn(&&namespace);
162
163    assert_multi_search(
164        &[&prop_all_false, &prop_sorted],
165        vec![ vec![ pattern![ ?x ] ], vec! [ pattern![ cons(?x, b) ] ] ],
166        vec![
167            vec![
168                aligned::Convolution::convolute(vec![ Some(term![ cons(nil, b) ]) ]),
169                aligned::Convolution::convolute(vec![ Some(term![ cons(cons(nil, b), b) ]) ])
170            ]
171        ]
172    )
173}
false/false.rs

false/
false.rs
