Update documentation

README.md

@@ -1,12 +1,19 @@
-**(WORK IN PROGRESS)**
-
 # Crepe
 
 Crepe is a library that allows you to write declarative logic programs in
 Rust, with a [Datalog](https://en.wikipedia.org/wiki/Datalog)-like syntax.
 It provides a procedural macro that generates efficient, safe code and
 interoperates seamlessly with Rust programs.
 
+## Features
+
+- Semi-naive evaluation
+- Stratified negation
+- Automatic generation of indices for relations
+- Easily call Rust functions from within Datalog rules
+- Typesafe way to initialize `@input` relations
+- Very fast, compiled directly with the rest of your Rust code
+
 ## Example
 
 The program below computes the transitive closure of a directed graph. Note
@@ -109,17 +116,20 @@ Walk: 89203
 NoWalk: 8207
 ```
 
-## Features
+## Notes
 
-- Semi-naive evaluation
-- Stratified negation
-- Automatic generation of indices for relations
-- Arbitrary Rust expression syntax allowed in rules
-- Typesafe way to initialize `@input` relations
-- Very fast, compiled directly with the rest of your Rust code
+From initial testing, the generated code is very fast. Variants of transitive
+closure for large graphs (~1000 nodes) run at comparable speed to compiled
+[Souffle](https://souffle-lang.github.io/), and at a fraction of the
+compilation time.
+
+This macro generates a `Crepe` struct in the current module, as well as structs
+for all of the declared relations. This means that to integrate Crepe inside a
+larger program, you should put it in its own module with related code. See the
+documentation for more information.
 
 ## Acknowledgements
 
-This work was heavily inspired by [Souffle](https://souffle-lang.github.io/)
+This project was heavily inspired by [Souffle](https://souffle-lang.github.io/)
 and [Formulog](https://github.com/HarvardPL/formulog), which both use similar
 models of Datalog compilation for static analysis.

src/lib.rs

@@ -127,9 +127,51 @@ use strata::Strata;
 /// Note that all Boolean conditions within the clauses of rules are evaluated
 /// in-place, and they must be surrounded by parentheses.
 ///
+/// # Evaluation Mode
+/// All generated code uses semi-naive evaluation (see Chapter 3 of _Datalog
+/// and Recursive Query Processing_), and it is split into multiple strata to
+/// enable stratified negation. For example, we can extend the code above to
+/// also compute the complement of transitive closure in a graph:
+/// ```
+/// mod datalog {
+///     use crepe::crepe;
+///
+///     crepe! {
+///         @input
+///         struct Edge(i32, i32);
+///
+///         @output
+///         struct Tc(i32, i32);
+///
+///         struct Node(i32);
+///
+///         @output
+///         struct NotTc(i32, i32);
+///
+///         Tc(x, y) <- Edge(x, y);
+///         Tc(x, z) <- Edge(x, y), Tc(y, z);
+///
+///         Node(x) <- Edge(x, _);
+///         Node(x) <- Edge(_, x);
+///         NotTc(x, y) <- Node(x), Node(y), !Tc(x, y);
+///     }
+///
+///     pub fn run(edges: &[(i32, i32)]) -> (Vec<(i32, i32)>, Vec<(i32, i32)>) {
+///         let mut runtime = Crepe::new();
+///         runtime.extend(edges.iter().map(|&(a, b)| Edge(a, b)));
+///         let (tc, not_tc) = runtime.run();
+///         (
+///             tc.into_iter().map(|Tc(a, b)| (a, b)).collect(),
+///             not_tc.into_iter().map(|NotTc(a, b)| (a, b)).collect(),
+///         )
+///     }
+/// }
+/// # fn main() {}
+/// ```
+///
 /// # Hygiene
 /// In addition to the relation structs, this macro generates implementations
-/// of private `Crepe` and `CrepeOutput` structs. Therefore, it is
+/// of a private struct named `Crepe` for the runtime. Therefore, it is
 /// recommended to place each Datalog program within its own module, to prevent
 /// name collisions.
 #[proc_macro]