claimr 0.4.0

Claimr — a constraint logic programming language, Prolog III inspired, parsed with a rustemo-generated LR parser.
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

// SPDX-License-Identifier: Apache-2.0

//! CLM-0027 (docs/design/2026-11-10-tabling-for-recursive-rules.md): the
//! tables of the program's tabled predicates. A table is keyed by a call's
//! *variant* — the call as a template with its unbound variables numbered
//! in order of first occurrence — and holds the ground answers of that call
//! as closed templates, a set in insertion order, each with the derivation
//! that first produced it when explanations were on. A table's content is
//! a function of the program alone (it is computed over the world store),
//! so the registry lives on the `Program` and survives queries.

use std::collections::{HashMap, HashSet};

use super::answer::ProofNode;
use super::compile::TTerm;

/// Where a table stands in the linear-tabling evaluation.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub(crate) enum TableState {
    /// No evaluation can add to it: consumed as a list of facts.
    Complete,
    /// Being computed by the evaluation frame at this depth of the
    /// machine's evaluation stack; a call to it is a recursive variant call,
    /// which consumes the answers so far.
    Evaluating(usize),
    /// Its evaluation returned while it depended on a frame still being
    /// evaluated (the leader); re-evaluated when called again in the
    /// leader's next pass, completed with the leader.
    Incomplete,
}

#[derive(Debug, Clone)]
pub(crate) struct Table {
    pub answers: Vec<TTerm>,
    /// Per answer: the derivation that first produced it, when recorded.
    pub proofs: Vec<Option<Vec<ProofNode>>>,
    seen: HashSet<TTerm>,
    pub state: TableState,
}

#[derive(Debug, Clone, Default)]
pub(crate) struct Tables {
    map: HashMap<TTerm, Table>,
    /// Answers recorded in all tables, ever: a leader compares it across a
    /// pass to know whether to iterate.
    pub total: usize,
}

impl Tables {
    pub fn state(&self, key: &TTerm) -> Option<TableState> {
        self.map.get(key).map(|t| t.state)
    }

    /// Start (or restart) the evaluation of `key` at `depth`, keeping the
    /// answers found so far.
    pub fn begin(&mut self, key: &TTerm, depth: usize) {
        let t = self.map.entry(key.clone()).or_insert_with(|| Table {
            answers: Vec::new(),
            proofs: Vec::new(),
            seen: HashSet::new(),
            state: TableState::Evaluating(depth),
        });
        t.state = TableState::Evaluating(depth);
    }

    pub fn set_state(&mut self, key: &TTerm, state: TableState) {
        if let Some(t) = self.map.get_mut(key) {
            t.state = state;
        }
    }

    /// Record an answer; false if it was already there.
    pub fn add(&mut self, key: &TTerm, answer: TTerm, proof: Option<Vec<ProofNode>>) -> bool {
        let Some(t) = self.map.get_mut(key) else {
            return false;
        };
        if !t.seen.insert(answer.clone()) {
            return false;
        }
        t.answers.push(answer);
        t.proofs.push(proof);
        self.total += 1;
        true
    }

    #[cfg(test)]
    pub fn is_empty(&self) -> bool {
        self.map.is_empty()
    }

    pub fn len(&self, key: &TTerm) -> usize {
        self.map.get(key).map_or(0, |t| t.answers.len())
    }

    pub fn answer(&self, key: &TTerm, i: usize) -> Option<(&TTerm, &Option<Vec<ProofNode>>)> {
        let t = self.map.get(key)?;
        Some((t.answers.get(i)?, t.proofs.get(i)?))
    }

    /// A query stopped inside an evaluation: forget every table that is not
    /// complete, so the next query starts clean.
    pub fn abandon(&mut self) {
        self.map.retain(|_, t| t.state == TableState::Complete);
    }
}