diff --git a/Cargo.toml b/Cargo.toml index c787dd8..25c9555 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "rify" -version = "0.6.0" +version = "0.7.0" authors = [ "Andrew Dirksen ", "Sam Hellawell " diff --git a/README.md b/README.md index e786ab0..5b6a029 100644 --- a/README.md +++ b/README.md @@ -8,7 +8,7 @@ Rify is a [forward chaining](https://en.wikipedia.org/wiki/Forward_chaining) [in It accepts conjunctive rules with limited expressiveness so reasoning is bounded by `O(n^k)` in both memory and in computation where n is the number of nodes in the input RDF dataset. -Reasoning generates a proof which can be used to quickly verify the result pragmatically. +Given premises and target statement[s], rify can generate a proof which can be used to quickly verify the result programatically. Logical rules are defined as if-then clauses. Something like this: @@ -48,11 +48,11 @@ Rify doesn't care whether its input and output is valid rdf. For example, it wil # Use -Two functions are central to this library: `prove` and `validate`. +Three functions are central to this library: `prove`, `validate`, and `infer`. -```rust -// Example use of `prove` +## prove +```rust use rify::{ prove, Entity::{Unbound, Bound}, @@ -96,13 +96,13 @@ assert_eq!( ); ``` -```rust -// Example use of `validate` +# validate +```rust use rify::{ prove, validate, Valid, Rule, RuleApplication, - Entity::{Bound, Unbound} + Entity::{Bound, Unbound} }; // same as above @@ -131,6 +131,43 @@ let Valid { assumed, implied } = validate::<&str, &str>( // quads in `implied` are also true. ``` +## infer + +```rust +use rify::{infer, Entity::{Unbound, Bound}, Rule}; + +// (?a, is, awesome) ∧ (?a, score, ?s) -> (?a score, awesome) +let awesome_score_axiom = Rule::create( + vec![ + // if someone is awesome + [Unbound("a"), Bound("is"), Bound("awesome"), Bound("default_graph")], + // and they have some score + [Unbound("a"), Bound("score"), Unbound("s"), Bound("default_graph")], + ], + vec![ + // then they must have an awesome score + [Unbound("a"), Bound("score"), Bound("awesome"), Bound("default_graph")] + ], +).expect("invalid rule"); + +let mut facts = vec![ + ["you", "score", "unspecified", "default_graph"], + ["you", "is", "awesome", "default_graph"] +]; + +let new_facts = infer::<&str, &str>(&facts, &[awesome_score_axiom]); +facts.extend(new_facts); + +assert_eq!( + &facts, + &[ + ["you", "score", "unspecified", "default_graph"], + ["you", "is", "awesome", "default_graph"], + ["you", "score", "awesome", "default_graph"], + ], +); +``` + # Recipes In addition to normal cargo commands like `cargo test` and `cargo check` the `./justfile` diff --git a/bindings/js_wasm/binding_tests/test.js b/bindings/js_wasm/binding_tests/test.js index 0ef5e9b..2d232ba 100644 --- a/bindings/js_wasm/binding_tests/test.js +++ b/bindings/js_wasm/binding_tests/test.js @@ -1,4 +1,4 @@ -import { prove, validate } from 'rify'; +import { prove, validate, infer } from 'rify'; import { expect } from 'chai'; // poor man's replacement for jest because making jest work with webpack+wasm is problematic @@ -232,6 +232,30 @@ tests([ // After verifying all the assumptions in the proof are true, we know that the // quads in valid.implied are true with respect to the provided rules. }], + + ['Example from doctest for infer actually runs.', () => { + // (?a, is, awesome) ∧ (?a, score, ?s) -> (?a score, awesome) + let awesome_score_axiom = { + if_all: [ + [{ Unbound: "a" }, { Bound: "is" }, { Bound: "awesome" }, { Bound: "default_graph" }], + [{ Unbound: "a" }, { Bound: "score" }, { Unbound: "s" }, { Bound: "default_graph" }], + ], + then: [ + [{ Unbound: "a" }, { Bound: "score" }, { Bound: "awesome" }, { Bound: "default_graph" }] + ], + }; + let facts = [ + ["you", "score", "unspecified", "default_graph"], + ["you", "is", "awesome", "default_graph"], + ]; + let new_facts = infer(facts, [awesome_score_axiom]); + facts = facts.concat(new_facts); + expect(facts).to.deep.equal([ + ["you", "score", "unspecified", "default_graph"], + ["you", "is", "awesome", "default_graph"], + ["you", "score", "awesome", "default_graph"], + ]); + }], ]); /// catch whichever error is emitted by when cb is called and return it diff --git a/bindings/js_wasm/package.json b/bindings/js_wasm/package.json index 503c736..64d3e2a 100644 --- a/bindings/js_wasm/package.json +++ b/bindings/js_wasm/package.json @@ -5,7 +5,7 @@ "Sam Hellawell " ], "description": "RDF reasoner that operates on RIF-like conjunctive rules. Outputs a machine\nreadable proof of some claim which can be cheaply verified.\n", - "version": "0.6.0", + "version": "0.7.0", "license": "MIT OR Apache-2.0", "repository": { "type": "git", diff --git a/bindings/js_wasm/src/js_wasm_test.rs b/bindings/js_wasm/src/js_wasm_test.rs index 155129a..521e1a5 100644 --- a/bindings/js_wasm/src/js_wasm_test.rs +++ b/bindings/js_wasm/src/js_wasm_test.rs @@ -11,6 +11,7 @@ type ProofInput = Vec>; /// with the actual interface fn _types_correct(r: RulesInput, c: ClaimsInput, p: ProofInput) -> ProofInput { super::validate_(r.clone(), p).unwrap(); + super::infer_(c.clone(), r.clone()).unwrap(); super::prove_(c.clone(), c, r).unwrap() } diff --git a/bindings/js_wasm/src/lib.rs b/bindings/js_wasm/src/lib.rs index 491244a..42a2bb0 100644 --- a/bindings/js_wasm/src/lib.rs +++ b/bindings/js_wasm/src/lib.rs @@ -134,6 +134,44 @@ pub fn validate_( Ok(valid) } +/// Make all possible true inferences given input premises and rules. This is open-ended reasoning. +/// +/// ```js +/// // (?a, is, awesome) ∧ (?a, score, ?s) -> (?a score, awesome) +/// let awesome_score_axiom = { +/// if_all: [ +/// [{ Unbound: "a" }, { Bound: "is" }, { Bound: "awesome" }, { Bound: "default_graph" }], +/// [{ Unbound: "a" }, { Bound: "score" }, { Unbound: "s" }, { Bound: "default_graph" }], +/// ], +/// then: [ +/// [{ Unbound: "a" }, { Bound: "score" }, { Bound: "awesome" }, { Bound: "default_graph" }] +/// ], +/// }; +/// let facts = [ +/// ["you", "score", "unspecified", "default_graph"], +/// ["you", "is", "awesome", "default_graph"], +/// ]; +/// let new_facts = infer(facts, [awesome_score_axiom]); +/// facts = facts.concat(new_facts); +/// expect(facts).to.deep.equal([ +/// ["you", "score", "unspecified", "default_graph"], +/// ["you", "is", "awesome", "default_graph"], +/// ["you", "score", "awesome", "default_graph"], +/// ]); +/// ``` +#[wasm_bindgen] +pub fn infer(premises: Box<[JsValue]>, rules: Box<[JsValue]>) -> Result { + Ok(ser(&infer_(deser_list(&premises)?, deser_list(&rules)?)?)) +} + +pub fn infer_( + premises: Vec<[String; 4]>, + rules: Vec, +) -> Result, Error> { + let rules = RuleUnchecked::check_all(rules)?; + Ok(rify::infer::(&premises, &rules)) +} + #[derive(PartialEq, Eq, PartialOrd, Ord, Debug, Clone, serde::Serialize, serde::Deserialize)] pub enum Entity { Unbound(String), diff --git a/src/common.rs b/src/common.rs index c632b63..6ea7e23 100644 --- a/src/common.rs +++ b/src/common.rs @@ -1,3 +1,11 @@ +use crate::reasoner::Quad; +use crate::rule::Rule; +use crate::translator::Translator; +use crate::Entity; +use crate::RuleApplication; +use alloc::collections::BTreeMap; +use core::fmt::Debug; + /// Increment argument then return previous value. /// /// ```nocompile @@ -19,6 +27,101 @@ where ret } +#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)] +/// A proof element that has yet to be translated to a presentable form. +/// +/// [crate::prove::prove] function does not immediately convert LowRuleApplication's to +/// [RuleApplication]'s. Rather, it converts only the LowRuleApplication's it is going to return +/// to the caller. +pub struct LowRuleApplication { + pub rule_index: usize, + pub instantiations: BTreeMap, +} + +impl LowRuleApplication { + /// Translate to a higher representation [RuleApplication]. The higher representation is + /// portable to other machines as long as those machines assume the same rule list. + /// This lower representation is not portable. + /// + /// Panics + /// + /// This function will panic if: + /// - an unbound item from originial_rule is not instatiated by self + /// - or there is no translation for a global instatiation of one of the unbound entities in + /// original_rule. + pub fn raise( + &self, + original_rule: &Rule, + trans: &Translator, + ) -> RuleApplication { + let mut instantiations = Vec::new(); + + // unbound_human -> unbound_local + let uhul: BTreeMap<&Unbound, usize> = original_rule + .cononical_unbound() + .enumerate() + .map(|(i, a)| (a, i)) + .collect(); + + for unbound_human in original_rule.cononical_unbound() { + let unbound_local: usize = uhul[unbound_human]; + let bound_global: usize = self.instantiations[&unbound_local]; + let bound_human: &Bound = trans.back(bound_global).unwrap(); + instantiations.push(bound_human.clone()); + } + + RuleApplication { + rule_index: self.rule_index, + instantiations, + } + } +} + +/// Attempt to forward translate a quad. +/// This is a helper function. It translates all four element of a quad, calling +/// [Translator::forward] for each element. If any element has no translation +/// this function will return `None`. +pub fn forward(translator: &Translator, key: &[T; 4]) -> Option { + let [s, p, o, g] = key; + Some( + [ + translator.forward(s)?, + translator.forward(p)?, + translator.forward(o)?, + translator.forward(g)?, + ] + .into(), + ) +} + +/// Reverse of [forward]. +/// [forward] translates each element from `T` to `usize`. This function translates each element +/// from `usize` to `T`. If any element has no translation this function will return `None`. +pub fn back(translator: &Translator, key: Quad) -> Option<[&T; 4]> { + let Quad { s, p, o, g } = key; + Some([ + translator.back(s.0)?, + translator.back(p.0)?, + translator.back(o.0)?, + translator.back(g.0)?, + ]) +} + +/// list with repetition all bound vertices of rules and all verticies of premises +pub fn vertices<'a, 'b, 'c, Bound, Unbound>( + premises: &'a [[Bound; 4]], + rules: &'b [Rule], +) -> impl Iterator +where + 'a: 'c, + 'b: 'c, +{ + rules + .iter() + .flat_map(|rule| rule.iter_entities().filter_map(Entity::as_bound)) + .chain(premises.iter().flatten()) +} + #[cfg(test)] mod test_util { use core::fmt::Debug; diff --git a/src/infer.rs b/src/infer.rs new file mode 100644 index 0000000..a6ab38c --- /dev/null +++ b/src/infer.rs @@ -0,0 +1,260 @@ +use crate::common::back; +use crate::common::{forward, vertices}; +use crate::reasoner::{Quad, Reasoner}; +use crate::rule::{LowRule, Rule}; +use crate::translator::Translator; +use alloc::collections::BTreeSet; + +/// Make all possible inferences. +pub fn infer( + premises: &[[Bound; 4]], + rules: &[Rule], +) -> Vec<[Bound; 4]> { + let tran: Translator = vertices(premises, rules).cloned().collect(); + let lpremises: Vec = premises + .iter() + .map(|quad| forward(&tran, quad).unwrap()) + .collect(); + let lrules: Vec = rules + .iter() + .map(|rule| rule.lower(&tran).map_err(|_| ()).unwrap()) + .collect(); + low_infer(&lpremises, &lrules) + .into_iter() + .map(|quad| clones(back(&tran, quad).unwrap())) + .collect() +} + +/// A version of infer that operates on lowered input an returns output in lowered form. +fn low_infer(premises: &[Quad], rules: &[LowRule]) -> Vec { + let mut rs = Reasoner::default(); + for prem in premises { + rs.insert(prem.clone()); + } + let initial_len = rs.claims_ref().len(); // number of premises after dedup + debug_assert!(initial_len <= premises.len()); + + loop { + let mut to_add = BTreeSet::::new(); + for rr in rules.iter() { + rs.apply(&mut rr.if_all.clone(), &mut rr.inst.clone(), &mut |inst| { + let ins = inst.as_ref(); + for implied in &rr.then { + let new_quad = [ + ins[&implied.s.0], + ins[&implied.p.0], + ins[&implied.o.0], + ins[&implied.g.0], + ] + .into(); + if !rs.contains(&new_quad) { + to_add.insert(new_quad); + } + } + }); + } + if to_add.is_empty() { + break; + } + for new in to_add.into_iter() { + rs.insert(new); + } + } + + // remove all premises, we only want to return new inferences + let mut claims = rs.claims(); + drop(claims.drain(0..initial_len)); + + debug_assert!( + { + let mut rc = claims.clone(); + rc.sort_unstable(); + rc.dedup(); + rc.len() == claims.len() + }, + "duplicate inferences should never be reported, this is a bug in rify" + ); + debug_assert!( + { + let rc = claims.iter().collect::>(); + premises.iter().all(|p| !rc.contains(p)) + }, + "premises should never be reported as new inferences, this is a bug in rify" + ); + + claims +} + +fn clones(arr: [&T; 4]) -> [T; 4] { + let [a, b, c, d] = arr; + [a.clone(), b.clone(), c.clone(), d.clone()] +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::common::decl_rules; + use crate::rule::Entity::{Bound as B, Unbound as U}; + + const DG: &str = "default_graph"; + + #[test] + fn ancestry() { + let parent = "parent"; + let ancestor = "ancestor"; + let default_graph = "default_graph"; + let nodes: Vec = (0..10).map(|n| format!("node_{}", n)).collect(); + let facts: Vec<[&str; 4]> = nodes + .iter() + .zip(nodes.iter().cycle().skip(1)) + .map(|(a, b)| [a, parent, b, default_graph]) + .collect(); + let rules = decl_rules(&[ + [ + &[[U("a"), B(parent), U("b"), B(default_graph)]], + &[[U("a"), B(ancestor), U("b"), B(default_graph)]], + ], + [ + &[ + [U("a"), B(ancestor), U("b"), B(default_graph)], + [U("b"), B(ancestor), U("c"), B(default_graph)], + ], + &[[U("a"), B(ancestor), U("c"), B(default_graph)]], + ], + ]); + let mut inferences = infer(&facts, &rules); + // every node is ancestor to every other node + let mut expected: Vec<[&str; 4]> = nodes + .iter() + .flat_map(|n0| nodes.iter().map(move |n1| (n0, n1))) + .map(|(n0, n1)| [n0, ancestor, n1, default_graph]) + .collect(); + + { + // checking multiset equality + expected.sort(); + inferences.sort(); + assert_eq!(inferences, expected); + } + } + + #[test] + fn unconditional_rule() { + let facts: Vec<[&str; 4]> = vec![]; + let rules = decl_rules::<&str, &str>(&[[ + &[], + &[[B("nachos"), B("are"), B("food"), B("default_graph")]], + ]]); + let inferences = infer::<&str, &str>(&facts, &rules); + assert_eq!(&inferences, &[["nachos", "are", "food", "default_graph"]]); + } + + #[test] + fn reasoning_is_already_complete() { + let facts: Vec<[&str; 4]> = vec![ + ["nachos", "are", "tasty", "default_graph"], + ["nachos", "are", "food", "default_graph"], + ]; + let rules = decl_rules::<&str, &str>(&[[ + &[[B("nachos"), B("are"), B("tasty"), B("default_graph")]], + &[[B("nachos"), B("are"), B("food"), B("default_graph")]], + ]]); + let expected: [[&str; 4]; 0] = []; + assert_eq!(&infer(&facts, &rules), &expected) + } + + #[test] + fn empty_ruleset() { + let facts: Vec<[&str; 4]> = vec![ + ["nachos", "are", "tasty", "default_graph"], + ["nachos", "are", "food", "default_graph"], + ]; + let rules = decl_rules::<&str, &str>(&[]); + let inferences = infer::<&str, &str>(&facts, &rules); + let expected: [[&str; 4]; 0] = []; + assert_eq!(&inferences, &expected); + } + + #[test] + fn empty_claimgraph() { + let facts: Vec<[&str; 4]> = vec![]; + let rules = decl_rules::<&str, &str>(&[[ + &[[B("nachos"), B("are"), B("tasty"), B("default_graph")]], + &[[B("nachos"), B("are"), B("food"), B("default_graph")]], + ]]); + let inferences = infer::<&str, &str>(&facts, &rules); + let expected: [[&str; 4]; 0] = []; + assert_eq!(&inferences, &expected); + } + + #[test] + fn sum_of_consecutive_ints_is_odd() { + let mut facts = vec![ + ["B", "is a consecutive int to", "A", DG], + ["A+B", "result of op", "op_add_A_B", DG], + ["op_add_A_B", "op_type", "add", DG], + ["op_add_A_B", "left_hand", "A", DG], + ["op_add_A_B", "right_hand", "B", DG], + ]; + + let rules = [ + Rule::create( + // consecutive ints = x, x+1 + vec![[U("y"), B("is a consecutive int to"), U("x"), B(DG)]], + vec![[U("y"), B("equals (t -> t+1) of"), U("x"), B(DG)]], // y=x+1 + ) + .expect("invalid rule"), + Rule::create( + // int+int == int + vec![ + [U("y"), B("is type"), B("int"), B(DG)], + [U("x"), B("is type"), B("int"), B(DG)], + [U("x+y"), B("result of op"), U("op1"), B(DG)], + [U("op1"), B("op_type"), B("add"), B(DG)], + [U("op1"), B("left_hand"), U("x"), B(DG)], + [U("op1"), B("right_hand"), U("y"), B(DG)], + ], + vec![[U("x+y"), B("is type"), B("int"), B(DG)]], + ) + .expect("invalid rule"), + Rule::create( + // x+(x+1) = 2x+1 + vec![ + [U("y"), B("equals (t -> t+1) of"), U("x"), B(DG)], + [U("x+y"), B("result of op"), U("op1"), B(DG)], + [U("op1"), B("op_type"), B("add"), B(DG)], + [U("op1"), B("left_hand"), U("x"), B(DG)], + [U("op1"), B("right_hand"), U("y"), B(DG)], + ], + vec![[U("x+y"), B("equals (t -> 2*t+1) of"), U("x"), B(DG)]], + ) + .expect("invalid rule"), + Rule::create( + // if r == 2t+1, t int, then r is odd + vec![ + [U("v"), B("equals (t -> 2*t+1) of"), U("w"), B(DG)], + [U("v"), B("is type"), B("int"), B(DG)], + [U("w"), B("is type"), B("int"), B(DG)], + ], + vec![[U("v"), B("is"), B("odd"), B(DG)]], + ) + .expect("invalid rule"), + Rule::create( + // consecutive ints are ints + vec![[U("p"), B("is a consecutive int to"), U("q"), B(DG)]], + vec![ + [U("p"), B("is type"), B("int"), B(DG)], + [U("q"), B("is type"), B("int"), B(DG)], + ], + ) + .expect("invalid rule"), + ]; + + let new_facts = infer::<&str, &str>(&facts, &rules); + facts.extend(new_facts); + + // did we prove that A+B is odd ? + let to_prove = ["A+B", "is", "odd", DG]; + assert!(facts.contains(&to_prove)); + } +} diff --git a/src/lib.rs b/src/lib.rs index 1ad3c5a..663834c 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -2,6 +2,7 @@ extern crate alloc; extern crate core; mod common; +mod infer; mod mapstack; mod prove; mod reasoner; @@ -10,6 +11,7 @@ mod translator; mod validate; mod vecset; +pub use infer::infer; pub use prove::{prove, CantProve, RuleApplication}; pub use rule::{Entity, InvalidRule, Rule}; pub use validate::{validate, Invalid, Valid}; @@ -17,11 +19,11 @@ pub use validate::{validate, Invalid, Valid}; #[cfg(doctest)] mod test_readme { macro_rules! external_doc_test { - ($x:expr) => { - #[doc = $x] - extern {} - }; - } + ($x:expr) => { + #[doc = $x] + extern "C" {} + }; + } external_doc_test!(include_str!("../README.md")); } diff --git a/src/prove.rs b/src/prove.rs index 2f85bda..e377882 100644 --- a/src/prove.rs +++ b/src/prove.rs @@ -1,3 +1,6 @@ +use crate::common::forward; +use crate::common::vertices; +use crate::common::LowRuleApplication; use crate::reasoner::{Quad, Reasoner}; use crate::rule::{Entity, LowRule, Rule}; use crate::translator::Translator; @@ -57,27 +60,14 @@ pub fn prove<'a, Unbound: Ord + Clone, Bound: Ord + Clone>( to_prove: &'a [[Bound; 4]], rules: &'a [Rule], ) -> Result>, CantProve> { - let tran: Translator = rules + let tran: Translator = vertices(premises, rules).cloned().collect(); + let lpremises: Vec = premises .iter() - .flat_map(|rule| rule.iter_entities().filter_map(Entity::as_bound)) - .chain(premises.iter().flatten()) - .cloned() + .map(|spog| forward(&tran, spog).unwrap()) .collect(); - let as_raw = |[s, p, o, g]: &[Bound; 4]| -> Option { - Some( - [ - tran.forward(&s)?, - tran.forward(&p)?, - tran.forward(&o)?, - tran.forward(&g)?, - ] - .into(), - ) - }; - let lpremises: Vec = premises.iter().map(|spo| as_raw(spo).unwrap()).collect(); let lto_prove: Vec = to_prove .iter() - .map(as_raw) + .map(|spog| forward(&tran, spog)) .collect::>() .ok_or(CantProve::NovelName)?; let lrules: Vec = rules @@ -219,49 +209,39 @@ impl Display for CantProve { #[cfg(feature = "std")] impl std::error::Error for CantProve {} -#[derive(Clone, Debug, PartialEq, Eq)] -struct LowRuleApplication { - rule_index: usize, - instantiations: BTreeMap, -} - -impl LowRuleApplication { - /// Panics - /// - /// This function will panic if: - /// - an unbound item from originial_rule is not instatiated by self - /// - or there is no translation for a global instatiation of one of the unbound entities in - /// original_rule. - fn raise( - &self, - original_rule: &Rule, - trans: &Translator, - ) -> RuleApplication { - let mut instantiations = Vec::new(); - - // unbound_human -> unbound_local - let uhul: BTreeMap<&Unbound, usize> = original_rule - .cononical_unbound() - .enumerate() - .map(|(i, a)| (a, i)) - .collect(); - - for unbound_human in original_rule.cononical_unbound() { - let unbound_local: usize = uhul[unbound_human]; - let bound_global: usize = self.instantiations[&unbound_local]; - let bound_human: &Bound = trans.back(bound_global).unwrap(); - instantiations.push(bound_human.clone()); - } - - RuleApplication { - rule_index: self.rule_index, - instantiations, - } - } -} - #[derive(Debug, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(serde::Deserialize, serde::Serialize))] +/// An element of a deductive proof. Proofs can be transmitted and later validatated as long as the +/// validator assumes the same rule list as the prover. +/// +/// Unbound variables are bound to the values in `instanitations`. They are bound in order of +/// initial appearance. +/// +/// Given the rule: +/// +/// ```customlang +/// ifall +/// [?z ex:foo ?x DG] +/// then +/// [?x ex:bar ?z DG] +/// ``` +/// +/// and the RuleApplication: +/// +/// ```customlang +/// RuleApplication { +/// rule_index: 0, +/// instantiations: vec!["foer", "bary"], +/// } +/// ``` +/// +/// The rule application represents the deductive proof: +/// +/// ```customlang +/// [foer ex:foo bary DG] +/// therefore +/// [bary ex:bar foer DG] +/// ``` pub struct RuleApplication { /// The index of the rule in the implicitly associated rule list. pub rule_index: usize, diff --git a/src/reasoner.rs b/src/reasoner.rs index b2f82f0..572feaf 100644 --- a/src/reasoner.rs +++ b/src/reasoner.rs @@ -197,6 +197,18 @@ impl Reasoner { let (strictest, less_strict) = rule.split_first_mut().expect("rule to be non-empty"); Some((strictest, less_strict)) } + + /// Get the deduplicated history of all claims that were inserted into this reasoner. + /// The returned list will be in insertion order. + pub fn claims(self) -> Vec { + self.claims + } + + /// Get the deduplicated history of all claims that were inserted into this reasoner. + /// The returned list will be in insertion order. + pub fn claims_ref(&self) -> &[Quad] { + &self.claims + } } trait Indexed { @@ -484,6 +496,22 @@ mod tests { assert_eq!(claims, expected_claims); } + #[test] + fn claims() { + let mut rs = Reasoner::default(); + for quad in &[[1, 1, 1, 1], [1, 2, 2, 2], [1, 1, 1, 1], [1, 3, 3, 3]] { + rs.insert(quad.clone().into()); + } + assert_eq!( + &rs.claims(), + &[ + [1, 1, 1, 1].into(), + [1, 2, 2, 2].into(), + [1, 3, 3, 3].into() + ], + ); + } + /// panics if an unbound name is implied /// panics if rule contains bound names that are not present in Translator fn low_rule(rule: [&[[Entity<&str, &str>; 4]]; 2], trans: &Translator<&str>) -> LowRule { diff --git a/src/rule.rs b/src/rule.rs index 8621a36..f512e11 100644 --- a/src/rule.rs +++ b/src/rule.rs @@ -1,6 +1,4 @@ -//! The reasoner's rule representation is optimized machine use, not human use. Comprehending and -//! composing rules directly is difficult for humans. This module provides a human friendly rule -//! description datatype that can be lowered to the reasoner's rule representation. +//! Defines a human frendly-ish logical rule representation [Rule]. use crate::common::inc; use crate::reasoner::{Instantiations, Quad}; @@ -11,9 +9,17 @@ use core::fmt::Debug; use core::fmt::Display; #[derive(Clone, Debug, PartialEq, Eq)] -// invariants held: -// unbound names may not exists in `then` unless they exist also in `if_all` -// +/// The reasoner's rule representation. +/// It is is optimized machine use, not human use. Comprehending and writing these rules directly +/// is difficult for humans. +/// [Rule] is the human friendly representation. +/// A [Rule] can be converted to a [LowRule] via the [Rule::lower]. +/// We hide the lowered rule representation from the user of this library. +/// Interfaces like [crate::prove::prove], [crate::validate::validate], and [crate::infer::infer] +/// accept [Rule] as input and lower to this representation before passing it to the reasoner. +/// +/// Invariants held: +/// unbound names may not exists in `then` unless they exist also in `if_all` // TODO: find a way to make fields non-public to protect invariant pub(crate) struct LowRule { pub if_all: Vec, // contains locally scoped names @@ -46,14 +52,23 @@ impl Entity { #[derive(PartialEq, Eq, PartialOrd, Ord, Debug, Clone)] #[cfg_attr(feature = "serde", derive(serde::Deserialize, serde::Serialize))] -// invariants held: -// unbound names may not exists in `then` unless they exist also in `if_all` +/// A human friendly-ish logical rule representation. Each rule represents an +/// if-then statement (implication relationship). Statements in the rule +/// may contain constants and/or variables. Constants are represented as [Entity::Bound]. +/// Variables are represented as [Entity::Unbound]. +/// +/// So that rules remain turing-incomplete, an invariant is upheld: +/// Unbound entities may not exists in the `then` clause unless they exist also in the `if_all` +/// clause. pub struct Rule { if_all: Vec<[Entity; 4]>, then: Vec<[Entity; 4]>, } impl<'a, Unbound: Ord + Clone, Bound: Ord> Rule { + /// This constructor ensures that any unbound element in `then` also exists somewhere + /// in `if_all`. If this is not the case the rule is invalid and the function will return + /// `Err`. Otherwise it will return `Ok`. pub fn create( if_all: Vec<[Entity; 4]>, then: Vec<[Entity; 4]>, @@ -70,6 +85,10 @@ impl<'a, Unbound: Ord + Clone, Bound: Ord> Rule { Ok(Self { if_all, then }) } + /// Converts [Rule] to [LowRule]. As part of the conversion + /// this function uses `translator` to convert bound entities to + /// the usize representation. If the rule contains any bound entity for which the translator + /// contains no translation this function will return `Err`. Otherwise it will return `Ok`. pub(crate) fn lower(&self, tran: &Translator) -> Result> { // There are three types of name at play here. // - human names are represented as Entities