1use std::cmp::Ordering;
2use std::cmp::Reverse;
3use std::collections::BinaryHeap;
4use std::collections::HashMap;
5use std::slice::Iter;
6use std::str::FromStr;
7
8#[derive(Debug)]
9#[cfg_attr(test, derive(PartialEq))]
10pub enum Term {
11 Constant(String),
12 Variable(String),
13 Compound(String, Terms),
14}
15
16#[derive(Clone)]
17pub struct TermsIter<'a> {
18 iter: Iter<'a, Term>,
19}
20
21impl<'a> Iterator for TermsIter<'a> {
22 type Item = &'a Term;
23 fn next(&mut self) -> Option<Self::Item> {
24 self.iter.next()
25 }
26}
27
28impl ExactSizeIterator for TermsIter<'_> {
29 fn len(&self) -> usize {
30 self.iter.len()
31 }
32}
33
34#[derive(Debug)]
35#[cfg_attr(test, derive(PartialEq))]
36pub struct Terms {
37 vec: Vec<Term>,
38}
39
40impl<T: Into<Vec<Term>>> From<T> for Terms {
41 fn from(vec: T) -> Self {
42 Terms { vec: vec.into() }
43 }
44}
45
46impl<'a> IntoIterator for &'a Terms {
47 type Item = &'a Term;
48 type IntoIter = TermsIter<'a>;
49 fn into_iter(self) -> Self::IntoIter {
50 TermsIter {
51 iter: self.vec.iter(),
52 }
53 }
54}
55
56impl Terms {
57 fn new() -> Self {
58 return Terms { vec: Vec::new() };
59 }
60 fn head_and_tail(head: Term, mut tail: Self) -> Self {
61 tail.vec.insert(0, head);
62 return tail;
63 }
64 fn len(&self) -> usize {
65 self.vec.len()
66 }
67}
68
69#[derive(Debug)]
70#[cfg_attr(test, derive(PartialEq))]
71pub enum Rule {
72 Rule(u64, Term, Terms),
73}
74
75#[derive(Clone)]
76pub struct RulesIter<'a> {
77 iter: Iter<'a, Rule>,
78}
79
80impl<'a> Iterator for RulesIter<'a> {
81 type Item = &'a Rule;
82 fn next(&mut self) -> Option<Self::Item> {
83 self.iter.next()
84 }
85}
86
87#[derive(Debug)]
88#[cfg_attr(test, derive(PartialEq))]
89pub struct Rules {
90 vec: Vec<Rule>,
91}
92
93impl<T: Into<Vec<Rule>>> From<T> for Rules {
94 fn from(vec: T) -> Self {
95 Rules { vec: vec.into() }
96 }
97}
98
99impl<'a> IntoIterator for &'a Rules {
100 type Item = &'a Rule;
101 type IntoIter = RulesIter<'a>;
102 fn into_iter(self) -> Self::IntoIter {
103 RulesIter {
104 iter: self.vec.iter(),
105 }
106 }
107}
108
109impl Rules {
110 fn new() -> Self {
111 return Rules { vec: Vec::new() };
112 }
113 fn head_and_tail(head: Rule, mut tail: Self) -> Self {
114 tail.vec.insert(0, head);
115 return tail;
116 }
117}
118
119fn stringify_goal(goal: (u64, &Term), table: &HashMap<(u64, &str), (u64, &Term)>) -> String {
120 match goal {
121 (ns, Term::Compound(label, args)) => {
122 let goals_string: Vec<String> = args
123 .into_iter()
124 .map(|x| stringify_goal((ns, x), table))
125 .collect();
126 label.clone() + "(" + &goals_string.join(", ") + ")"
127 }
128 (_, Term::Constant(label)) => label.clone() + "*",
129 (ns, Term::Variable(label)) => match table.get(&(ns, label)) {
130 Some(&goal) => stringify_goal(goal, table),
131 None => label.clone() + "#" + &ns.to_string(),
132 },
133 }
134}
135
136pub fn stringify_table(table: &HashMap<(u64, &str), (u64, &Term)>) -> Vec<String> {
137 let mut res = Vec::new();
138 for (&(ns, label), &goal) in table {
139 if ns == 0 {
140 res.push(label.to_string() + " = " + &stringify_goal(goal, table) + "\n");
141 }
142 }
143 res
144}
145
146fn take_term_args<'a>(iter: &mut impl Iterator<Item = &'a str>) -> Option<Terms> {
147 let term = take_term(iter)?;
148 match iter.next()? {
149 "," => Some(Terms::head_and_tail(term, take_term_args(iter)?)),
150 ")" => Some(Terms::head_and_tail(term, Terms::new())),
151 _ => None,
152 }
153}
154
155fn take_term<'a>(iter: &mut impl Iterator<Item = &'a str>) -> Option<Term> {
156 let label = iter.next()?;
157 match iter.next()? {
158 "*" => Some(Term::Constant(String::from(label))),
159 "?" => Some(Term::Variable(String::from(label))),
160 "(" => Some(Term::Compound(String::from(label), take_term_args(iter)?)),
161 _ => None,
162 }
163}
164
165fn take_terms<'a>(iter: &mut impl Iterator<Item = &'a str>) -> Option<Terms> {
166 let term = take_term(iter)?;
167 match iter.next()? {
168 "," => Some(Terms::head_and_tail(term, take_terms(iter)?)),
169 "." => Some(Terms::head_and_tail(term, Terms::new())),
170 _ => None,
171 }
172}
173
174fn take_rule<'a>(iter: &mut impl Iterator<Item = &'a str>) -> Option<Rule> {
175 let cost = iter.next()?.parse().ok()?;
176 let _ = (iter.next()? == "]").then_some(())?;
177 let head = take_term(iter)?;
178 match iter.next()? {
179 ":-" => Some(Rule::Rule(cost, head, take_terms(iter)?)),
180 "." => Some(Rule::Rule(cost, head, Terms::new())),
181 _ => None,
182 }
183}
184
185fn take_rules<'a>(iter: &mut impl Iterator<Item = &'a str>) -> Option<Rules> {
186 match iter.next() {
187 Some("[") => Some(Rules::head_and_tail(take_rule(iter)?, take_rules(iter)?)),
188 None => Some(Rules::new()),
189 _ => None,
190 }
191}
192
193impl FromStr for Term {
194 type Err = ();
195 fn from_str(s: &str) -> Result<Self, Self::Err> {
196 let mut tokenizer = kohaku::Tokenizer::new(["(", ")", ",", "*", "?"]);
197 let mut iter = tokenizer.tokenize(s).map_while(|x| x.ok());
198 let term = take_term(&mut iter).ok_or(())?;
199 iter.next().is_none().then_some(term).ok_or(())
200 }
201}
202
203impl FromStr for Terms {
204 type Err = ();
205 fn from_str(s: &str) -> Result<Self, Self::Err> {
206 let mut tokenizer = kohaku::Tokenizer::new(["(", ")", ",", "*", "?", "."]);
207 let mut iter = tokenizer.tokenize(s).map_while(|x| x.ok());
208 let query = take_terms(&mut iter).ok_or(())?;
209 iter.next().is_none().then_some(query).ok_or(())
210 }
211}
212
213impl FromStr for Rules {
214 type Err = ();
215 fn from_str(s: &str) -> Result<Self, Self::Err> {
216 let mut tokenizer = kohaku::Tokenizer::new(["(", ")", ",", "*", "?", ".", ":-", "[", "]"]);
217 let mut iter = tokenizer.tokenize(s).map_while(|x| x.ok());
218 let rules = take_rules(&mut iter).ok_or(())?;
219 iter.next().is_none().then_some(rules).ok_or(())
220 }
221}
222
223fn occurs_check(
224 (nsv, s): (u64, &str),
225 (nst, t): (u64, &Term),
226 r: &HashMap<(u64, &str), (u64, &Term)>,
227) -> bool {
228 match t {
229 Term::Compound(_, args) => args
230 .into_iter()
231 .all(|c| occurs_check((nsv, s), (nst, c), r)),
232 Term::Variable(s1) if nsv == nst && s == s1 => false,
233 Term::Variable(s1) => r
234 .get(&(nst, s1))
235 .is_none_or(|&(ns1, t1)| occurs_check((nsv, s), (ns1, t1), r)),
236 _ => true,
237 }
238}
239
240fn unify<'a>(
241 goal1: (u64, &'a Term),
242 goal2: (u64, &'a Term),
243 mut r: HashMap<(u64, &'a str), (u64, &'a Term)>,
244) -> Option<HashMap<(u64, &'a str), (u64, &'a Term)>> {
245 match (goal1, goal2) {
246 ((ns1, Term::Compound(s1, args1)), (ns2, Term::Compound(s2, args2)))
247 if s1 == s2 && args1.len() == args2.len() =>
248 {
249 let mut iter = args1.into_iter().zip(args2.into_iter());
250 iter.try_fold(r, |r, (c1, c2)| unify((ns1, c1), (ns2, c2), r))
251 }
252 ((_, Term::Constant(s1)), (_, Term::Constant(s2))) if s1 == s2 => Some(r),
253 ((ns1, Term::Variable(s1)), (ns2, Term::Variable(s2))) if ns1 == ns2 && s1 == s2 => Some(r),
254 ((ns, Term::Variable(s)), goal) | (goal, (ns, Term::Variable(s)))
255 if r.contains_key(&(ns, s)) =>
256 {
257 let &goal_variable = r.get(&(ns, s)).unwrap();
258 unify(goal_variable, goal, r)
259 }
260 ((ns, Term::Variable(s)), goal) | (goal, (ns, Term::Variable(s)))
261 if occurs_check((ns, s), goal, &r) =>
262 {
263 r.insert((ns, s), goal);
264 Some(r)
265 }
266 _ => None,
267 }
268}
269
270#[derive(Clone)]
271struct State<'a> {
272 cost: u64,
273 namespace: u64,
274 table: HashMap<(u64, &'a str), (u64, &'a Term)>,
275 shared: Vec<(u64, &'a Term)>,
276 shared_remaining: Vec<(u64, &'a Term)>,
277 goals: Vec<(u64, &'a Term, TermsIter<'a>)>,
278 rules_iter: RulesIter<'a>,
279}
280
281impl Eq for State<'_> {}
282
283impl PartialEq for State<'_> {
284 fn eq(&self, other: &Self) -> bool {
285 self.cost == other.cost
286 }
287}
288
289impl PartialOrd for State<'_> {
290 fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
291 Some(self.cmp(other))
292 }
293}
294
295impl Ord for State<'_> {
296 fn cmp(&self, other: &Self) -> Ordering {
297 self.cost.cmp(&other.cost)
298 }
299}
300
301struct Infer<'a> {
302 rules_iter: RulesIter<'a>,
303 pq: BinaryHeap<Reverse<State<'a>>>,
304}
305
306impl<'a> Infer<'a> {
307 fn push_state(&mut self, state: State<'a>) {
308 self.pq.push(Reverse(state))
309 }
310
311 fn pop_state(&mut self) -> Option<State<'a>> {
312 self.pq.pop().map(|x| x.0)
313 }
314
315 fn push_goals(
316 &mut self,
317 goals: &mut Vec<(u64, &'a Term, TermsIter<'a>)>,
318 goals_iter: (u64, &'a Term, TermsIter<'a>),
319 ) {
320 goals.push(goals_iter)
321 }
322
323 fn pop_goal(&mut self, goals: &mut Vec<(u64, &'a Term, TermsIter<'a>)>) -> (u64, &'a Term) {
324 let (namespace, _, iter) = goals.last_mut().unwrap();
325 (*namespace, iter.next().unwrap())
326 }
327
328 fn is_empty_goal(&mut self, goals: &mut Vec<(u64, &'a Term, TermsIter<'a>)>) -> bool {
329 goals.is_empty()
330 }
331
332 fn update_goals(
333 &mut self,
334 goals: &mut Vec<(u64, &'a Term, TermsIter<'a>)>,
335 shared: &mut Vec<(u64, &'a Term)>,
336 ) {
337 while let Some((namespace, head, goals_iter)) = goals.last_mut()
338 && goals_iter.len() == 0
339 {
340 shared.push((*namespace, head));
341 goals.pop();
342 }
343 }
344}
345
346impl<'a> Iterator for Infer<'a> {
347 type Item = (u64, HashMap<(u64, &'a str), (u64, &'a Term)>);
348
349 fn next(&mut self) -> Option<Self::Item> {
350 loop {
351 let mut state = self.pop_state()?;
352 if self.is_empty_goal(&mut state.goals) {
353 return Some((state.cost, state.table));
354 }
355 if let Some((namespace, term)) = state.shared_remaining.pop() {
356 self.push_state(state.clone());
357 let (namespace_goal, goal) = self.pop_goal(&mut state.goals);
358 let Some(table) = unify((namespace, term), (namespace_goal, goal), state.table)
359 else {
360 continue;
361 };
362 state.table = table;
363 self.update_goals(&mut state.goals, &mut state.shared);
364 state.rules_iter = self.rules_iter.clone();
365 state.shared_remaining = state.shared.clone();
366 self.push_state(state);
367 continue;
368 }
369 let Some(Rule::Rule(cost_rule, head, body)) = state.rules_iter.next() else {
370 continue;
371 };
372 self.push_state(state.clone());
373 let (namespace_goal, goal) = self.pop_goal(&mut state.goals);
374 state.cost = state.cost + cost_rule;
375 state.namespace += 1;
376 let Some(table) = unify((state.namespace, head), (namespace_goal, goal), state.table)
377 else {
378 continue;
379 };
380 state.table = table;
381 self.push_goals(&mut state.goals, (state.namespace, head, body.into_iter()));
382 self.update_goals(&mut state.goals, &mut state.shared);
383 state.rules_iter = self.rules_iter.clone();
384 state.shared_remaining = state.shared.clone();
385 self.push_state(state);
386 }
387 }
388}
389
390fn infer_iter<'a>(goals: &'a Terms, rules: &'a Rules) -> Infer<'a> {
391 let goals_iter = goals.into_iter();
392 let rules_iter = rules.into_iter();
393 Infer {
394 rules_iter: rules_iter.clone(),
395 pq: BinaryHeap::from([Reverse(State {
396 cost: 0,
397 namespace: 0,
398 table: HashMap::new(),
399 shared: Vec::new(),
400 shared_remaining: Vec::new(),
401 goals: vec![(0, goals_iter.clone().next().unwrap(), goals_iter.clone())],
402 rules_iter: rules_iter.clone(),
403 })]),
404 }
405}
406
407pub fn infer<'a>(
408 goals: &'a Terms,
409 rules: &'a Rules,
410) -> Option<(u64, HashMap<(u64, &'a str), (u64, &'a Term)>)> {
411 infer_iter(goals, rules).next()
412}
413
414#[cfg(test)]
415mod tests {
416 use super::*;
417
418 #[test]
419 fn test_stringify_goal_1() {
420 assert_eq!(
421 stringify_goal((0, &"a*".parse().unwrap()), &HashMap::new()),
422 "a*"
423 );
424 }
425
426 #[test]
427 fn test_stringify_goal_2() {
428 assert_eq!(
429 stringify_goal((0, &"x?".parse().unwrap()), &HashMap::new()),
430 "x#0"
431 );
432 }
433
434 #[test]
435 fn test_stringify_goal_3() {
436 assert_eq!(
437 stringify_goal(
438 (2, &"x?".parse().unwrap()),
439 &HashMap::from([((2, "x"), (1, &"y?".parse().unwrap()))])
440 ),
441 "y#1"
442 );
443 }
444
445 #[test]
446 fn test_stringify_goal_4() {
447 assert_eq!(
448 stringify_goal((0, &"ab(c_d(e_f*),g_h?)".parse().unwrap()), &HashMap::new()),
449 "ab(c_d(e_f*), g_h#0)"
450 );
451 }
452
453 #[test]
454 fn test_stringify_goal_5() {
455 assert_eq!(
456 stringify_goal(
457 (2, &"f(a*, b*, x?)".parse().unwrap()),
458 &HashMap::from([((2, "x"), (1, &"ab(c_d(e_f*),g_h?)".parse().unwrap()))])
459 ),
460 "f(a*, b*, ab(c_d(e_f*), g_h#1))"
461 );
462 }
463
464 #[test]
465 fn test_stringify_table_1() {
466 let strings = stringify_table(&HashMap::from([
467 ((0, "x"), (1, &"x?".parse().unwrap())),
468 ((1, "x"), (2, &"x?".parse().unwrap())),
469 ((0, "y"), (1, &"x?".parse().unwrap())),
470 ]));
471 assert_eq!(strings.len(), 2);
472 assert!(strings.contains(&"x = x#2\n".into()));
473 assert!(strings.contains(&"y = x#2\n".into()));
474 }
475
476 #[test]
477 fn test_parse_term_1() {
478 assert_eq!(
479 "ab(c_d(e_f*),g_h?)".parse(),
480 Ok(Term::Compound(
481 String::from("ab"),
482 [
483 Term::Compound(
484 String::from("c_d"),
485 [Term::Constant(String::from("e_f"))].into(),
486 ),
487 Term::Variable(String::from("g_h")),
488 ]
489 .into(),
490 ))
491 );
492 }
493
494 #[test]
495 fn test_parse_term_2() {
496 assert_eq!("ab(c_d(*e_f),?g_h)))(".parse::<Term>(), Err(()));
497 }
498
499 #[test]
500 fn test_parse_term_3() {
501 assert_eq!("a*(".parse::<Term>(), Err(()));
502 }
503
504 #[test]
505 fn test_parse_term_4() {
506 assert_eq!("a,a*)".parse::<Term>(), Err(()));
507 }
508
509 #[test]
510 fn test_parse_term_5() {
511 assert_eq!("a(b*(c*)".parse::<Term>(), Err(()));
512 }
513
514 #[test]
515 fn test_parse_term_6() {
516 assert_eq!("a)".parse::<Term>(), Err(()));
517 }
518
519 #[test]
520 fn test_parse_term_7() {
521 assert_eq!("a(b**".parse::<Term>(), Err(()));
522 }
523
524 #[test]
525 fn test_parse_term_8() {
526 assert_eq!("a(*)".parse::<Term>(), Err(()));
527 }
528
529 #[test]
530 fn test_parse_term_9() {
531 assert_eq!("(a*)".parse::<Term>(), Err(()));
532 }
533
534 #[test]
535 fn test_parse_term_10() {
536 assert_eq!("a*a".parse::<Term>(), Err(()));
537 }
538
539 #[test]
540 fn test_parse_term_11() {
541 assert_eq!("a(a*a)".parse::<Term>(), Err(()));
542 }
543
544 #[test]
545 fn test_parse_term_12() {
546 assert_eq!(
547 "f(a*, b*, x?)".parse(),
548 Ok(Term::Compound(
549 String::from("f"),
550 [
551 Term::Constant(String::from("a")),
552 Term::Constant(String::from("b")),
553 Term::Variable(String::from("x")),
554 ]
555 .into(),
556 ))
557 );
558 }
559
560 #[test]
561 fn test_parse_term_13() {
562 assert_eq!("f(a, b, X)".parse::<Term>(), Err(()));
563 }
564
565 #[test]
566 fn test_parse_term_14() {
567 assert_eq!("f(*a, *b, ?x)".parse::<Term>(), Err(()));
568 }
569
570 #[test]
571 fn test_parse_term_15() {
572 assert_eq!("ab(c_d(e_f),g_h)))(".parse::<Term>(), Err(()));
573 }
574
575 #[test]
576 fn test_parse_term_16() {
577 assert_eq!("ab(c_d(e_f*),g_h?)))(".parse::<Term>(), Err(()));
578 }
579
580 #[test]
581 fn test_parse_query_1() {
582 let query = "f(a*, b*, x?).".parse::<Terms>();
583 assert_eq!(
584 query,
585 Ok([Term::Compound(
586 String::from("f"),
587 [
588 Term::Constant(String::from("a")),
589 Term::Constant(String::from("b")),
590 Term::Variable(String::from("x")),
591 ]
592 .into()
593 )]
594 .into())
595 );
596 }
597
598 #[test]
599 fn test_parse_query_2() {
600 let query = "f(a*, b*, x?), g(c*, y?), h(d*).".parse::<Terms>();
601 assert_eq!(
602 query,
603 Ok([
604 Term::Compound(
605 String::from("f"),
606 [
607 Term::Constant(String::from("a")),
608 Term::Constant(String::from("b")),
609 Term::Variable(String::from("x")),
610 ]
611 .into()
612 ),
613 Term::Compound(
614 String::from("g"),
615 [
616 Term::Constant(String::from("c")),
617 Term::Variable(String::from("y")),
618 ]
619 .into()
620 ),
621 Term::Compound(
622 String::from("h"),
623 [Term::Constant(String::from("d"))].into()
624 )
625 ]
626 .into())
627 );
628 }
629
630 #[test]
631 fn test_parse_rules_1() {
632 let rules = "[2]a* :- b*, c?. \n[4]d*.\n".parse::<Rules>();
633 assert_eq!(
634 rules,
635 Ok([
636 Rule::Rule(
637 2,
638 Term::Constant(String::from("a")),
639 [
640 Term::Constant(String::from("b")),
641 Term::Variable(String::from("c"))
642 ]
643 .into()
644 ),
645 Rule::Rule(4, Term::Constant(String::from("d")), Terms::new())
646 ]
647 .into())
648 );
649 }
650
651 #[test]
652 fn test_take_rules_2() {
653 let rules = "[2]a:-b,C.\n".parse::<Rules>();
654 assert_eq!(rules, Err(()));
655 }
656
657 #[test]
658 fn test_take_rules_3() {
659 let rules = "[2]a:-b,C. \n[4]d.\n".parse::<Rules>();
660 assert_eq!(rules, Err(()));
661 }
662
663 #[test]
664 fn test_take_rules_4() {
665 let rules = "[2]*a :- *b, ?c. \n[4]*d.\n".parse::<Rules>();
666 assert_eq!(rules, Err(()));
667 }
668
669 #[test]
670 fn test_unify_1() {
671 assert_eq!(
672 unify(
673 (0, &"f(a* ,b* ,x? )".parse().unwrap()),
674 (1, &"f(y? ,b* ,c* )".parse().unwrap()),
675 HashMap::new()
676 )
677 .unwrap(),
678 HashMap::from([
679 ((0, "x"), (1, &"c*".parse().unwrap())),
680 ((1, "y"), (0, &"a*".parse().unwrap()))
681 ])
682 )
683 }
684
685 #[test]
686 fn test_unify_2() {
687 assert_eq!(
688 unify(
689 (1, &"f(x? ,y? )".parse().unwrap()),
690 (1, &"f(a* ,b* )".parse().unwrap()),
691 HashMap::new()
692 )
693 .unwrap(),
694 HashMap::from([
695 ((1, "x"), (1, &"a*".parse().unwrap())),
696 ((1, "y"), (1, &"b*".parse().unwrap()))
697 ])
698 )
699 }
700
701 #[test]
702 fn test_unify_3() {
703 assert_eq!(
704 unify(
705 (0, &"x?".parse().unwrap()),
706 (0, &"y?".parse().unwrap()),
707 HashMap::new()
708 )
709 .unwrap(),
710 HashMap::from([((0, "x"), (0, &"y?".parse().unwrap()))])
711 )
712 }
713
714 #[test]
715 fn test_unify_4() {
716 assert_eq!(
717 unify(
718 (0, &"f(a*,b*)".parse().unwrap()),
719 (1, &"f(x?,x?)".parse().unwrap()),
720 HashMap::new()
721 ),
722 None
723 )
724 }
725
726 #[test]
727 fn test_unify_5() {
728 assert_eq!(
729 unify(
730 (0, &"x?".parse().unwrap()),
731 (0, &"f(x?)".parse().unwrap()),
732 HashMap::new()
733 ),
734 None
735 )
736 }
737
738 #[test]
739 fn test_unify_6() {
740 assert_eq!(
741 unify(
742 (1, &"f(f(x?),g(y?))".parse().unwrap()),
743 (1, &"f(y?,x?)".parse().unwrap()),
744 HashMap::new()
745 ),
746 None
747 )
748 }
749
750 #[test]
751 fn test_unify_7() {
752 assert_eq!(
753 unify(
754 (1, &"g(x?,y?,x?)".parse().unwrap()),
755 (1, &"g(f(x?),f(y?),y?)".parse().unwrap()),
756 HashMap::new()
757 ),
758 None
759 )
760 }
761
762 #[test]
763 fn test_unify_8() {
764 assert_eq!(
765 unify(
766 (0, &"x?".parse().unwrap()),
767 (0, &"x?".parse().unwrap()),
768 HashMap::new()
769 )
770 .unwrap(),
771 HashMap::new()
772 )
773 }
774
775 #[test]
776 fn test_unify_9() {
777 assert_eq!(
778 unify(
779 (0, &"x?".parse().unwrap()),
780 (1, &"f(x?)".parse().unwrap()),
781 HashMap::new()
782 )
783 .unwrap(),
784 HashMap::from([((0, "x"), (1, &"f(x?)".parse().unwrap()))])
785 )
786 }
787
788 #[test]
789 fn test_unify_10() {
790 assert_eq!(
791 unify(
792 (0, &"x?".parse().unwrap()),
793 (1, &"x?".parse().unwrap()),
794 HashMap::new()
795 )
796 .unwrap(),
797 HashMap::from([((0, "x"), (1, &"x?".parse().unwrap()))])
798 )
799 }
800
801 #[test]
802 fn test_unify_11() {
803 assert_eq!(
804 unify(
805 (0, &"f(f(x?),g(y?))".parse().unwrap()),
806 (1, &"f(y?,x?)".parse().unwrap()),
807 HashMap::new()
808 )
809 .unwrap(),
810 HashMap::from([
811 ((1, "x"), (0, &"g(y?)".parse().unwrap())),
812 ((1, "y"), (0, &"f(x?)".parse().unwrap()))
813 ])
814 )
815 }
816
817 #[test]
818 fn test_unify_12() {
819 assert_eq!(
820 unify(
821 (0, &"f(f(x?), x?)".parse().unwrap()),
822 (1, &"f(x?,x?)".parse().unwrap()),
823 HashMap::new()
824 ),
825 None
826 )
827 }
828
829 const RULES1: &str = r#"
830 [0] parent(pam*, bob*).
831 [0] parent(tom*, bob*).
832 [0] parent(tom*, liz*).
833 [0] parent(bob*, ann*).
834 [0] parent(bob*, pat*).
835 [0] parent(pat*, jim*).
836 "#;
837
838 #[test]
839 fn test_infer_1_1() {
840 let rules = &RULES1.parse().unwrap();
841 let query = &"parent(bob*, pat*).".parse().unwrap();
842 assert_eq!(
843 infer_iter(query, rules).collect::<Vec<(u64, HashMap<(u64, &str), (u64, &Term)>)>>(),
844 [(0, HashMap::new())]
845 );
846 }
847
848 #[test]
849 fn test_infer_1_2() {
850 let rules = &RULES1.parse().unwrap();
851 let query = &"parent(liz*, pat*).".parse().unwrap();
852 assert_eq!(
853 infer_iter(query, rules).collect::<Vec<(u64, HashMap<(u64, &str), (u64, &Term)>)>>(),
854 []
855 );
856 }
857
858 #[test]
859 fn test_infer_1_3() {
860 let rules = &RULES1.parse().unwrap();
861 let query = &"parent(tom*, ben*).".parse().unwrap();
862 assert_eq!(
863 infer_iter(query, rules).collect::<Vec<(u64, HashMap<(u64, &str), (u64, &Term)>)>>(),
864 []
865 );
866 }
867
868 #[test]
869 fn test_infer_1_4() {
870 let rules = &RULES1.parse().unwrap();
871 let query = &"parent(x?, liz*).".parse().unwrap();
872 assert_eq!(
873 infer_iter(query, rules).collect::<Vec<(u64, HashMap<(u64, &str), (u64, &Term)>)>>(),
874 [(
875 0,
876 HashMap::from([((0, "x"), (1, &"tom*".parse().unwrap()))])
877 )]
878 );
879 }
880
881 #[test]
882 fn test_infer_1_5() {
883 let rules = &RULES1.parse().unwrap();
884 let query = &"parent(bob*, y?).".parse().unwrap();
885 let res =
886 infer_iter(query, rules).collect::<Vec<(u64, HashMap<(u64, &str), (u64, &Term)>)>>();
887 assert!(res.len() == 2);
888 assert!(res.contains(&(
889 0,
890 HashMap::from([((0, "y"), (1, &"ann*".parse().unwrap()))])
891 )));
892 assert!(res.contains(&(
893 0,
894 HashMap::from([((0, "y"), (1, &"pat*".parse().unwrap()))])
895 )));
896 }
897
898 #[test]
899 fn test_infer_1_6() {
900 let rules = &RULES1.parse().unwrap();
901 let query = &"parent(p?, q?).".parse().unwrap();
902 let res =
903 infer_iter(query, rules).collect::<Vec<(u64, HashMap<(u64, &str), (u64, &Term)>)>>();
904 assert!(res.len() == 6);
905 assert!(res.contains(&(
906 0,
907 HashMap::from([
908 ((0, "p"), (1, &"pam*".parse().unwrap())),
909 ((0, "q"), (1, &"bob*".parse().unwrap()))
910 ])
911 )));
912 assert!(res.contains(&(
913 0,
914 HashMap::from([
915 ((0, "p"), (1, &"tom*".parse().unwrap())),
916 ((0, "q"), (1, &"bob*".parse().unwrap()))
917 ])
918 )));
919 assert!(res.contains(&(
920 0,
921 HashMap::from([
922 ((0, "p"), (1, &"tom*".parse().unwrap())),
923 ((0, "q"), (1, &"liz*".parse().unwrap()))
924 ])
925 )));
926 assert!(res.contains(&(
927 0,
928 HashMap::from([
929 ((0, "p"), (1, &"bob*".parse().unwrap())),
930 ((0, "q"), (1, &"ann*".parse().unwrap()))
931 ])
932 )));
933 assert!(res.contains(&(
934 0,
935 HashMap::from([
936 ((0, "p"), (1, &"bob*".parse().unwrap())),
937 ((0, "q"), (1, &"pat*".parse().unwrap()))
938 ])
939 )));
940 assert!(res.contains(&(
941 0,
942 HashMap::from([
943 ((0, "p"), (1, &"pat*".parse().unwrap())),
944 ((0, "q"), (1, &"jim*".parse().unwrap()))
945 ])
946 )));
947 }
948
949 #[test]
950 fn test_infer_1_7() {
951 let rules = &RULES1.parse().unwrap();
952 let query = &"parent(y?, jim*), parent(x?, y?).".parse().unwrap();
953 assert_eq!(
954 infer_iter(query, rules).collect::<Vec<(u64, HashMap<(u64, &str), (u64, &Term)>)>>(),
955 [(
956 0,
957 HashMap::from([
958 ((0, "y"), (1, &"pat*".parse().unwrap())),
959 ((0, "x"), (2, &"bob*".parse().unwrap()))
960 ])
961 )]
962 )
963 }
964
965 #[test]
966 fn test_infer_1_8() {
967 let rules = &RULES1.parse().unwrap();
968 let query = &"parent(tom*, x?), parent(x?, y?).".parse().unwrap();
969 let res =
970 infer_iter(query, rules).collect::<Vec<(u64, HashMap<(u64, &str), (u64, &Term)>)>>();
971 assert!(res.len() == 2);
972 assert!(res.contains(&(
973 0,
974 HashMap::from([
975 ((0, "x"), (1, &"bob*".parse().unwrap())),
976 ((0, "y"), (2, &"ann*".parse().unwrap()))
977 ])
978 )));
979 assert!(res.contains(&(
980 0,
981 HashMap::from([
982 ((0, "x"), (1, &"bob*".parse().unwrap())),
983 ((0, "y"), (2, &"pat*".parse().unwrap()))
984 ])
985 )));
986 }
987
988 #[test]
989 fn test_infer_1_9() {
990 let rules = &RULES1.parse().unwrap();
991 let query = &"parent(x?, ann*), parent(x?, pat*).".parse().unwrap();
992 assert_eq!(
993 infer_iter(query, rules).collect::<Vec<(u64, HashMap<(u64, &str), (u64, &Term)>)>>(),
994 [(
995 0,
996 HashMap::from([((0, "x"), (1, &"bob*".parse().unwrap()))])
997 )]
998 )
999 }
1000
1001 #[test]
1002 fn test_infer_1_10() {
1003 let rules = &RULES1.parse().unwrap();
1004 let query = &"parent(pam*, x?), parent(x?, y?), parent(y?, jim*)."
1005 .parse()
1006 .unwrap();
1007 assert_eq!(
1008 infer_iter(query, rules).collect::<Vec<(u64, HashMap<(u64, &str), (u64, &Term)>)>>(),
1009 [(
1010 0,
1011 HashMap::from([
1012 ((0, "x"), (1, &"bob*".parse().unwrap())),
1013 ((0, "y"), (2, &"pat*".parse().unwrap()))
1014 ])
1015 )]
1016 )
1017 }
1018
1019 const RULES2: &str = r#"
1020 [0] big(bear*).
1021 [0] big(elephant*).
1022 [0] small(cat*).
1023 [0] brown(bear*).
1024 [0] black(cat*).
1025 [0] gray(elephant*).
1026 [0] dark(z?) :- black(z?).
1027 [0] dark(z?) :- brown(z?).
1028 "#;
1029
1030 #[test]
1031 fn test_infer_2() {
1032 let rules = &RULES2.parse().unwrap();
1033 let query = &"dark(x?), big(x?).".parse().unwrap();
1034 assert_eq!(
1035 infer_iter(query, rules).collect::<Vec<(u64, HashMap<(u64, &str), (u64, &Term)>)>>(),
1036 [(
1037 0,
1038 HashMap::from([
1039 ((1, "z"), (0, &"x?".parse().unwrap())),
1040 ((0, "x"), (2, &"bear*".parse().unwrap()))
1041 ])
1042 )]
1043 )
1044 }
1045
1046 const RULES3: &str = r#"
1047 [0] parent(pam*, bob*).
1048 [0] parent(tom*, bob*).
1049 [0] parent(tom*, liz*).
1050 [0] parent(bob*, ann*).
1051 [0] parent(bob*, pat*).
1052 [0] parent(pat*, jim*).
1053 [0] female(pam*).
1054 [0] male(tom*).
1055 [0] male(bob*).
1056 [0] female(liz*).
1057 [0] female(ann*).
1058 [0] female(pat*).
1059 [0] male(jim*).
1060 [0] offspring(y?, x?) :- parent(x?, y?).
1061 [0] mother(x?, y?) :- parent(x?, y?), female(x?).
1062 [0] grandparent(x?, z?) :- parent(x?, y?), parent(y?, z?).
1063 [0] sister(x?, y?) :- parent(z?, x?), parent(z?, y?), female(x?), different(x?, y?).
1064 [0] predecessor(x?, z?) :- parent(x?, z?).
1065 [0] predecessor(x?, z?) :- parent(x?, y?), predecessor(y?, z?).
1066 "#;
1067
1068 #[test]
1069 fn test_infer_3_1() {
1070 let rules = &RULES3.parse().unwrap();
1071 let query = &"predecessor(tom*, pat*).".parse().unwrap();
1072 assert_eq!(
1073 infer_iter(query, rules).collect::<Vec<(u64, HashMap<(u64, &str), (u64, &Term)>)>>(),
1074 [(
1075 0,
1076 HashMap::from([
1077 ((1, "x"), (0, &"tom*".parse().unwrap())),
1078 ((1, "z"), (0, &"pat*".parse().unwrap())),
1079 ((1, "y"), (2, &"bob*".parse().unwrap())),
1080 ((3, "x"), (2, &"bob*".parse().unwrap())),
1081 ((3, "z"), (0, &"pat*".parse().unwrap()))
1082 ])
1083 )]
1084 )
1085 }
1086
1087 #[test]
1088 fn test_infer_3_2() {
1089 let rules = &RULES3.parse().unwrap();
1090 let query = &"parent(pam*, bob*).".parse().unwrap();
1091 assert_eq!(
1092 infer_iter(query, rules).collect::<Vec<(u64, HashMap<(u64, &str), (u64, &Term)>)>>(),
1093 [(0, HashMap::from([]))]
1094 )
1095 }
1096
1097 #[test]
1098 fn test_infer_3_3() {
1099 let rules = &RULES3.parse().unwrap();
1100 let query = &"mother(pam*, bob*).".parse().unwrap();
1101 assert_eq!(
1102 infer_iter(query, rules).collect::<Vec<(u64, HashMap<(u64, &str), (u64, &Term)>)>>(),
1103 [(
1104 0,
1105 HashMap::from([
1106 ((1, "x"), (0, &"pam*".parse().unwrap())),
1107 ((1, "y"), (0, &"bob*".parse().unwrap()))
1108 ])
1109 )]
1110 )
1111 }
1112
1113 #[test]
1114 fn test_infer_3_4() {
1115 let rules = &RULES3.parse().unwrap();
1116 let query = &"grandparent(pam*, ann*).".parse().unwrap();
1117 assert_eq!(
1118 infer_iter(query, rules).collect::<Vec<(u64, HashMap<(u64, &str), (u64, &Term)>)>>(),
1119 [(
1120 0,
1121 HashMap::from([
1122 ((1, "x"), (0, &"pam*".parse().unwrap())),
1123 ((1, "z"), (0, &"ann*".parse().unwrap())),
1124 ((1, "y"), (2, &"bob*".parse().unwrap()))
1125 ])
1126 )]
1127 )
1128 }
1129
1130 #[test]
1131 fn test_infer_3_5() {
1132 let rules = &RULES3.parse().unwrap();
1133 let query = &"grandparent(bob*, jim*).".parse().unwrap();
1134 assert_eq!(
1135 infer_iter(query, rules).collect::<Vec<(u64, HashMap<(u64, &str), (u64, &Term)>)>>(),
1136 [(
1137 0,
1138 HashMap::from([
1139 ((1, "x"), (0, &"bob*".parse().unwrap())),
1140 ((1, "z"), (0, &"jim*".parse().unwrap())),
1141 ((1, "y"), (2, &"pat*".parse().unwrap()))
1142 ])
1143 )]
1144 )
1145 }
1146
1147 const RULES4: &str = r#"
1148 [6] parent(pam*, bob*).
1149 [5] parent(tom*, bob*).
1150 [4] parent(tom*, liz*).
1151 [3] parent(bob*, ann*).
1152 [2] parent(bob*, pat*).
1153 [1] parent(pat*, jim*).
1154 "#;
1155
1156 #[test]
1157 fn test_infer_4_1() {
1158 let rules = &RULES4.parse().unwrap();
1159 let query = &"parent(bob*, pat*).".parse().unwrap();
1160 assert_eq!(
1161 infer_iter(query, rules).collect::<Vec<(u64, HashMap<(u64, &str), (u64, &Term)>)>>(),
1162 [(2, HashMap::new())]
1163 );
1164 }
1165
1166 #[test]
1167 fn test_infer_4_2() {
1168 let rules = &RULES4.parse().unwrap();
1169 let query = &"parent(liz*, pat*).".parse().unwrap();
1170 assert_eq!(
1171 infer_iter(query, rules).collect::<Vec<(u64, HashMap<(u64, &str), (u64, &Term)>)>>(),
1172 []
1173 );
1174 }
1175
1176 #[test]
1177 fn test_infer_4_3() {
1178 let rules = &RULES4.parse().unwrap();
1179 let query = &"parent(tom*, ben*).".parse().unwrap();
1180 assert_eq!(
1181 infer_iter(query, rules).collect::<Vec<(u64, HashMap<(u64, &str), (u64, &Term)>)>>(),
1182 []
1183 );
1184 }
1185
1186 #[test]
1187 fn test_infer_4_4() {
1188 let rules = &RULES4.parse().unwrap();
1189 let query = &"parent(x?, liz*).".parse().unwrap();
1190 assert_eq!(
1191 infer_iter(query, rules).collect::<Vec<(u64, HashMap<(u64, &str), (u64, &Term)>)>>(),
1192 [(
1193 4,
1194 HashMap::from([((0, "x"), (1, &"tom*".parse().unwrap()))])
1195 )]
1196 );
1197 }
1198
1199 #[test]
1200 fn test_infer_4_5() {
1201 let rules = &RULES4.parse().unwrap();
1202 let query = &"parent(bob*, y?).".parse().unwrap();
1203 assert_eq!(
1204 infer_iter(query, rules).collect::<Vec<(u64, HashMap<(u64, &str), (u64, &Term)>)>>(),
1205 [
1206 (
1207 2,
1208 HashMap::from([((0, "y"), (1, &"pat*".parse().unwrap()))])
1209 ),
1210 (
1211 3,
1212 HashMap::from([((0, "y"), (1, &"ann*".parse().unwrap()))])
1213 )
1214 ]
1215 );
1216 }
1217
1218 #[test]
1219 fn test_infer_4_6() {
1220 let rules = &RULES4.parse().unwrap();
1221 let query = &"parent(p?, q?).".parse().unwrap();
1222 assert_eq!(
1223 infer_iter(query, rules).collect::<Vec<(u64, HashMap<(u64, &str), (u64, &Term)>)>>(),
1224 [
1225 (
1226 1,
1227 HashMap::from([
1228 ((0, "p"), (1, &"pat*".parse().unwrap())),
1229 ((0, "q"), (1, &"jim*".parse().unwrap()))
1230 ])
1231 ),
1232 (
1233 2,
1234 HashMap::from([
1235 ((0, "p"), (1, &"bob*".parse().unwrap())),
1236 ((0, "q"), (1, &"pat*".parse().unwrap()))
1237 ])
1238 ),
1239 (
1240 3,
1241 HashMap::from([
1242 ((0, "p"), (1, &"bob*".parse().unwrap())),
1243 ((0, "q"), (1, &"ann*".parse().unwrap()))
1244 ])
1245 ),
1246 (
1247 4,
1248 HashMap::from([
1249 ((0, "p"), (1, &"tom*".parse().unwrap())),
1250 ((0, "q"), (1, &"liz*".parse().unwrap()))
1251 ])
1252 ),
1253 (
1254 5,
1255 HashMap::from([
1256 ((0, "p"), (1, &"tom*".parse().unwrap())),
1257 ((0, "q"), (1, &"bob*".parse().unwrap()))
1258 ])
1259 ),
1260 (
1261 6,
1262 HashMap::from([
1263 ((0, "p"), (1, &"pam*".parse().unwrap())),
1264 ((0, "q"), (1, &"bob*".parse().unwrap()))
1265 ])
1266 )
1267 ]
1268 );
1269 }
1270
1271 #[test]
1272 fn test_infer_4_7() {
1273 let rules = &RULES4.parse().unwrap();
1274 let query = &"parent(y?, jim*), parent(x?, y?).".parse().unwrap();
1275 assert_eq!(
1276 infer_iter(query, rules).collect::<Vec<(u64, HashMap<(u64, &str), (u64, &Term)>)>>(),
1277 [(
1278 1 + 2,
1279 HashMap::from([
1280 ((0, "y"), (1, &"pat*".parse().unwrap())),
1281 ((0, "x"), (2, &"bob*".parse().unwrap()))
1282 ])
1283 )]
1284 )
1285 }
1286
1287 #[test]
1288 fn test_infer_4_8() {
1289 let rules = &RULES4.parse().unwrap();
1290 let query = &"parent(tom*, x?), parent(x?, y?).".parse().unwrap();
1291 assert_eq!(
1292 infer_iter(query, rules).collect::<Vec<(u64, HashMap<(u64, &str), (u64, &Term)>)>>(),
1293 [
1294 (
1295 5 + 2,
1296 HashMap::from([
1297 ((0, "x"), (1, &"bob*".parse().unwrap())),
1298 ((0, "y"), (2, &"pat*".parse().unwrap()))
1299 ])
1300 ),
1301 (
1302 5 + 3,
1303 HashMap::from([
1304 ((0, "x"), (1, &"bob*".parse().unwrap())),
1305 ((0, "y"), (2, &"ann*".parse().unwrap()))
1306 ])
1307 )
1308 ]
1309 )
1310 }
1311
1312 #[test]
1313 fn test_infer_4_9() {
1314 let rules = &RULES4.parse().unwrap();
1315 let query = &"parent(x?, ann*), parent(x?, pat*).".parse().unwrap();
1316 assert_eq!(
1317 infer_iter(query, rules).collect::<Vec<(u64, HashMap<(u64, &str), (u64, &Term)>)>>(),
1318 [(
1319 3 + 2,
1320 HashMap::from([((0, "x"), (1, &"bob*".parse().unwrap()))])
1321 )]
1322 )
1323 }
1324
1325 #[test]
1326 fn test_infer_4_10() {
1327 let rules = &RULES4.parse().unwrap();
1328 let query = &"parent(pam*, x?), parent(x?, y?), parent(y?, jim*)."
1329 .parse()
1330 .unwrap();
1331 assert_eq!(
1332 infer_iter(query, rules).collect::<Vec<(u64, HashMap<(u64, &str), (u64, &Term)>)>>(),
1333 [(
1334 6 + 2 + 1,
1335 HashMap::from([
1336 ((0, "x"), (1, &"bob*".parse().unwrap())),
1337 ((0, "y"), (2, &"pat*".parse().unwrap()))
1338 ])
1339 )]
1340 )
1341 }
1342
1343 const RULES5: &str = r#"
1344 [2] p* :- q*.
1345 [1] q*.
1346 [1] p* :- r*.
1347 [3] r*.
1348 "#;
1349
1350 #[test]
1351 fn test_infer_5_1() {
1352 let rules = &RULES5.parse().unwrap();
1353 let query = &"p*.".parse().unwrap();
1354 assert_eq!(
1355 infer_iter(query, rules).collect::<Vec<(u64, HashMap<(u64, &str), (u64, &Term)>)>>(),
1356 [(3, HashMap::from([])), (4, HashMap::from([]))]
1357 )
1358 }
1359
1360 const RULES6: &str = r#"
1361 [1] f(p*) :- g(q*).
1362 [2] g(q*).
1363 [4] f(q*).
1364 "#;
1365
1366 #[test]
1367 fn test_infer_6_1() {
1368 let rules = &RULES6.parse().unwrap();
1369 let query = &"f(x?), g(q*).".parse().unwrap();
1370 assert_eq!(
1371 infer_iter(query, rules).collect::<Vec<(u64, HashMap<(u64, &str), (u64, &Term)>)>>(),
1372 [
1373 (3, HashMap::from([((0, "x"), (1, &"p*".parse().unwrap())),])),
1374 (5, HashMap::from([((0, "x"), (1, &"p*".parse().unwrap())),])),
1375 (6, HashMap::from([((0, "x"), (1, &"q*".parse().unwrap())),]))
1376 ]
1377 )
1378 }
1379}