Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

chore: Fix code in README.md + (auto)align version in repl + minor improvements (typos, etc.) #36

Merged
merged 2 commits into from
Jan 20, 2025
Merged

chore: Fix code in README.md + (auto)align version in repl + minor improvements (typos, etc.) #36

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
61985f7
docs/chore: minor improvements
duesee Jan 8, 2025
7ec6471
docs: test and fix README.md
duesee Jan 8, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
52 changes: 29 additions & 23 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,9 +26,9 @@ Features that are implemented:
In the REPL you can quickly get started by loading one of the provided test files with some
pre-defined facts and rules, e.g. for [Peano arithmetic](testfiles/arithmetic.lru):

```
```text
#===================#
# LogRu REPL v0.1.0 #
# LogRu REPL v0.4.1 #
#===================#

?- :load testfiles/arithmetic.lru
Expand All @@ -37,7 +37,7 @@ Loaded!

We can then ask it to solve 2 + 3 (and find the correct answer 5):

```
```text
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This PR makes it so that README.md is used in lib.rs as Rust doc (see below) to check the code. Rust assumes code blocks to be "rust" by default, so we need to say "text" here.

?- add(s(s(z)), s(s(s(z))), X).
Found solution:
X = s(s(s(s(s(z)))))
Expand All @@ -46,7 +46,7 @@ No more solutions.

It is also possible to enumerate all pairs of terms that add up to five:

```
```text
?- add(X, Y, s(s(s(s(s(z)))))).
Found solution:
X = s(s(s(s(s(z)))))
Expand All @@ -72,14 +72,14 @@ No more solutions.
While there is no standard library, using the cut operation, it is possible to build many of the
common combinators, such as `once`:

```
```text
?- :define once(X) :- X, !.
Defined!
```

Given a predicate producing multiple choices...

```
```text
?- :define foo(hello). foo(world).
Defined!
?- foo(X).
Expand All @@ -92,7 +92,7 @@ No more solutions.

..., we can now restrict it to produce only the first choice:

```
```text
?- once(foo(X)).
Found solution:
X = hello
Expand All @@ -114,10 +114,18 @@ hold all known facts and rules. A few simple rules for [Peano
arithmetic](https://en.wikipedia.org/wiki/Peano_axioms#Addition) can be defined like this:

```rust
use logru::{
ast::{self, exists, Query, Rule},
query_dfs,
resolve::RuleResolver,
search::Solution,
SymbolStorage,
};

let mut syms = logru::SymbolStore::new();
let mut r = logru::RuleSet::new();

// Obtain IDs for t he symbols we want to use in our terms.
// Obtain IDs for the symbols we want to use in our terms.
// The order of these calls doesn't matter.
let s = syms.get_or_insert_named("s");
let z = syms.get_or_insert_named("z");
Expand All @@ -131,8 +139,7 @@ r.insert(Rule::fact(is_natural, vec![z.into()]));
// Define the rule `is_natural(s(P)) :- is_natural(P)`, i.e. that
// the successor of P is a natural number if P is also a natural number.
r.insert(ast::forall(|[p]| {
Rule::fact(is_natural, vec![ast::app(s, vec![p.into()])])
.when(is_natural, vec![p.into()])
Rule::fact(is_natural, vec![ast::app(s, vec![p.into()])]).when(is_natural, vec![p.into()])
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is due to rustfmt.

}));

// Now we define a predicate for addition that we'll call add.
Expand All @@ -142,8 +149,7 @@ r.insert(ast::forall(|[p]| {
// adding zero to P is P if P is a natural number.
// This is the base case of Peano addition.
r.insert(ast::forall(|[p]| {
Rule::fact(add, vec![p.into(), z.into(), p.into()])
.when(is_natural, vec![p.into()])
Rule::fact(add, vec![p.into(), z.into(), p.into()]).when(is_natural, vec![p.into()])
}));

// Finally, define the rule `add(P, s(Q), s(R)) :- add(P, Q, R)`,
Expand All @@ -159,16 +165,16 @@ r.insert(ast::forall(|[p, q, r]| {
)
.when(add, vec![p.into(), q.into(), r.into()])
}));
```

We can now ask the solver to prove statements within this universe, e.g. that "there exists an X
such that X + 2 = 3". This statement is indeed true for X = 1, and indeed, the solver will provide
this answer:
// We can now ask the solver to prove statements within this universe, e.g. that "there exists an X
Copy link
Contributor Author

@duesee duesee Jan 10, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The easiest way to make cargo test pass was to merge these blocks. We are trading flexibility of writing for correctness, though.

// such that X + 2 = 3". This statement is indeed true for X = 1, and indeed, the solver will provide
// this answer:

let mut r = RuleResolver::new(&r);

```rust
// Obtain an iterator that allows us to exhaustively search the solution space:
let solutions = query_dfs(
&r,
&mut r,
Copy link
Contributor Author

@duesee duesee Jan 10, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This and the following makes cargo test pass. Not sure if it's the best way to resolve.

&exists(|[x]| {
Query::single_app(
add,
Expand All @@ -180,10 +186,11 @@ let solutions = query_dfs(
)
}),
);

// Sanity check
assert_eq!(
solutions.collect::<Vec<_>>(),
vec![vec![Some(ast::app(s, vec![z.into()]))],]
vec![Solution(vec![Some(ast::app(s, vec![z.into()]))])],
);
```

Expand Down Expand Up @@ -218,7 +225,7 @@ in ~23ms.
Although even with the occurs check enabled, SWI Prolog is only a few milliseconds slower, so there
are likely other optimizations at play, too.

```
```text
?- :load testfiles/zebra-reverse.lru
Loaded!
?- :time puzzle($0).
Expand All @@ -228,7 +235,7 @@ No more solutions.
Took 0.0603s
```

```
```text
?- consult('testfiles/zebra-reverse.lru').
true.

Expand All @@ -237,7 +244,6 @@ true.
Houses = list(house(yellow, norway, water, diplomat, fox), house(blue, italy, tea, physician, horse), house(red, england, milk, photographer, snails), house(white, spain, juice, violinist, dog), house(green, japan, coffee, painter, zebra)) ;
% 22,610 inferences, 0.004 CPU in 0.004 seconds (100% CPU, 6459533 Lips)
false.

```


Expand Down Expand Up @@ -268,4 +274,4 @@ at your option.

Unless you explicitly state otherwise, any contribution intentionally submitted
for inclusion in the work by you, as defined in the Apache-2.0 license, shall be
dual licensed as above, without any additional terms or conditions.
dual licensed as above, without any additional terms or conditions.
12 changes: 7 additions & 5 deletions examples/repl.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,11 +18,13 @@ use rustyline::history::DefaultHistory;
use rustyline::validate::Validator;
use rustyline::{Editor, Helper};

const HEADER: &str = "
#===================#
# LogRu REPL v0.1.0 #
#===================#
";
const HEADER: &str = concat!(
"#===================#\n",
"# LogRu REPL v",
env!("CARGO_PKG_VERSION"),
" #\n",
"#===================#\n"
);

fn main() {
// install global collector configured based on RUST_LOG env var.
Expand Down
5 changes: 5 additions & 0 deletions src/lib.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -147,6 +147,11 @@
//!
//!

// Test examples from README.md.
Copy link
Contributor Author

@duesee duesee Jan 10, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This "trick" allows to ensure the code in the README.md is checked during cargo test w/o using additional dependencies.

#[doc = include_str!("../README.md")]
#[cfg(doctest)]
pub struct ReadmeDoctests;

pub mod ast;
pub mod resolve;
pub mod search;
Expand Down
2 changes: 1 addition & 1 deletion testfiles/arithmetic.lru
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,4 +6,4 @@ add(X, z, X) :- is_natural(X).
add(X, s(Y), s(Z)) :- add(X, Y, Z).

mul(X, z, z) :- is_natural(X).
mul(X, s(Y), Z) :- mul(X,Y,W), add(X,W,Z).
mul(X, s(Y), Z) :- mul(X, Y, W), add(X, W, Z).
Loading