logru/resolve/
rules.rs

1use crate::search::{ResolveContext, Resolved, Resolver, SolutionState};
2use crate::term_arena::AppTerm;
3use crate::universe::CompiledRule;
4use crate::{term_arena, RuleSet};
5
6/// A goal resolver that uses a user-defined [`RuleSet`] for resolving goals.
7#[derive(Debug, Clone)]
8pub struct RuleResolver<'a> {
9    rules: &'a RuleSet,
10}
11
12impl<'a> RuleResolver<'a> {
13    pub const fn new(rules: &'a RuleSet) -> Self {
14        Self { rules }
15    }
16
17    /// Unify a goal term with a rule and return the new sub goals if the unification was
18    /// successful.
19    fn unify_rule(
20        &self,
21        goal_term: term_arena::TermId,
22        rule: &'a CompiledRule,
23        solution: &mut SolutionState,
24    ) -> Option<impl Iterator<Item = term_arena::TermId> + 'a> {
25        // add uninstantiated variables for the rule
26        let var_start = solution.allocate_vars(rule.var_slots());
27        let var_offset = var_start.ord();
28
29        // instantiate head for now
30        let (head, head_blueprint) = rule.head();
31        let conv_rule_head = solution
32            .terms_mut()
33            .instantiate_blueprint(head_blueprint, var_offset);
34        let instantiated_rule_head = conv_rule_head(head);
35
36        // TODO: simplify things even more so that we can use the argument ranges directly for
37        // unification, since we already know at this point that the head symbols match.
38        if solution.unify(goal_term, instantiated_rule_head) {
39            // instantiate tail terms
40            let (tail, tail_blueprint) = rule.tail();
41            let conv_rule_tail = solution
42                .terms_mut()
43                .instantiate_blueprint(tail_blueprint, var_offset);
44            // and return the updated term IDs (in reverse order) so that the originally leftmost
45            // goal ends up on the top of the goal stack, and hence is processed next.
46            Some(tail.iter().rev().map(move |tail| conv_rule_tail(*tail)))
47        } else {
48            None
49        }
50    }
51
52    fn apply_first_rule(
53        &self,
54        mut rules: &'a [CompiledRule],
55        goal_id: term_arena::TermId,
56        context: &mut ResolveContext,
57    ) -> Option<&'a [CompiledRule]> {
58        while let Some((first, rest)) = rules.split_first() {
59            rules = rest;
60            let result = self.unify_rule(goal_id, first, context.solution_mut());
61            if let Some(goals) = result {
62                context.extend_goals(goals);
63                return Some(rest);
64            } else {
65                context.reset();
66            }
67        }
68        None
69    }
70}
71
72impl<'a> Resolver for RuleResolver<'a> {
73    type Choice = &'a [CompiledRule];
74
75    fn resolve(
76        &mut self,
77        goal_id: term_arena::TermId,
78        AppTerm(sym, _): term_arena::AppTerm,
79        context: &mut ResolveContext,
80    ) -> Option<Resolved<Self::Choice>> {
81        let rules = self.rules.rules_by_head(sym);
82        let rest = self.apply_first_rule(rules, goal_id, context)?;
83        if rest.is_empty() {
84            Some(Resolved::Success)
85        } else {
86            Some(Resolved::SuccessRetry(rest))
87        }
88    }
89
90    fn resume(
91        &mut self,
92        choice: &mut Self::Choice,
93        goal_id: term_arena::TermId,
94        context: &mut ResolveContext,
95    ) -> bool {
96        if let Some(rest) = self.apply_first_rule(choice, goal_id, context) {
97            *choice = rest;
98            true
99        } else {
100            false
101        }
102    }
103}
logru/resolve/rules.rs

logru/resolve/
rules.rs
