Skip to content

Commit 53d76f2

Browse files
committed
documentation, borrow_check
1 parent 23c4c87 commit 53d76f2

File tree

4 files changed

+168
-7
lines changed

4 files changed

+168
-7
lines changed

src/bin/borrow_check.rs

Lines changed: 119 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,119 @@
1+
extern crate datalog;
2+
use datalog::Iteration;
3+
4+
type Region = u32;
5+
type Borrow = u32;
6+
type Point = u32;
7+
8+
fn main() {
9+
10+
let subset = {
11+
12+
// Create a new iteration context, ...
13+
let mut iteration1 = Iteration::new();
14+
15+
// .. some variables, ..
16+
let subset = iteration1.variable::<(Region, Region, Point)>("subset");
17+
18+
// different indices for `subset`.
19+
let subset_r1p = iteration1.variable::<((Region, Point), Region)>("subset_r1p");
20+
let subset_r2p = iteration1.variable::<((Region, Point), Region)>("subset_r2p");
21+
let subset_p = iteration1.variable::<(Point, (Region, Region))>("subset_p");
22+
23+
let subset_1 = iteration1.variable::<((Region, Point), Region)>("subset_1");
24+
let subset_2 = iteration1.variable::<((Region, Point), Region)>("subset_2");
25+
26+
let region_live_at = iteration1.variable::<((Region, Point), ())>("region_live_at");
27+
let cfg_edge_p = iteration1.variable::<(Point, Point)>("cfg_edge_p");
28+
29+
// load initial facts.
30+
subset.insert(Vec::new().into());
31+
region_live_at.insert(Vec::new().into());
32+
cfg_edge_p.insert(Vec::new().into());
33+
34+
// .. and then start iterating rules!
35+
while iteration1.changed() {
36+
37+
// remap fields to re-index by keys.
38+
subset_r1p.from_map(&subset, |&(r1,r2,p)| ((r1,p),r2));
39+
subset_r2p.from_map(&subset, |&(r1,r2,p)| ((r2,p),r1));
40+
subset_p.from_map(&subset, |&(r1,r2,p)| (p,(r1,r2)));
41+
42+
// R0: subset(R1, R2, P) :- outlives(R1, R2, P).
43+
// Already loaded; outlives is static.
44+
45+
// R1: subset(R1, R3, P) :-
46+
// subset(R1, R2, P),
47+
// subset(R2, R3, P).
48+
subset.from_join(&subset_r2p, &subset_r1p, |&(_r2,p),&r1,&r3| (r1,r3,p));
49+
50+
// R2: subset(R1, R2, Q) :-
51+
// subset(R1, R2, P),
52+
// cfg_edge(P, Q),
53+
// region_live_at(R1, Q),
54+
// region_live_at(R2, Q).
55+
56+
subset_1.from_join(&subset_p, &cfg_edge_p, |&_p, &(r1,r2), &q| ((r1,q),r2));
57+
subset_2.from_join(&subset_1, &region_live_at, |&(r1,q),&r2,&()| ((r2,q),r1));
58+
subset.from_join(&subset_2, &region_live_at, |&(r2,q),&r1,&()| (r1,r2,q));
59+
60+
}
61+
62+
subset_r1p.complete()
63+
};
64+
65+
let requires = {
66+
67+
// Create a new iteration context, ...
68+
let mut iteration2 = Iteration::new();
69+
70+
// .. some variables, ..
71+
let requires = iteration2.variable::<(Region, Borrow, Point)>("requires");
72+
requires.insert(Vec::new().into());
73+
74+
let requires_rp = iteration2.variable::<((Region, Point), Borrow)>("requires_rp");
75+
let requires_bp = iteration2.variable::<((Borrow, Point), Region)>("requires_bp");
76+
77+
let requires_1 = iteration2.variable::<(Point, (Borrow, Region))>("requires_1");
78+
let requires_2 = iteration2.variable::<((Region, Point), Borrow)>("requires_2");
79+
80+
let subset_r1p = iteration2.variable::<((Region, Point), Region)>("subset_r1p");
81+
subset_r1p.insert(subset);
82+
83+
let killed = Vec::new().into();
84+
let region_live_at = iteration2.variable::<((Region, Point), ())>("region_live_at");
85+
let cfg_edge_p = iteration2.variable::<(Point, Point)>("cfg_edge_p");
86+
87+
// .. and then start iterating rules!
88+
while iteration2.changed() {
89+
90+
requires_rp.from_map(&requires, |&(r,b,p)| ((r,p),b));
91+
requires_bp.from_map(&requires, |&(r,b,p)| ((b,p),r));
92+
93+
// requires(R, B, P) :- borrow_region(R, B, P).
94+
// Already loaded; borrow_region is static.
95+
96+
// requires(R2, B, P) :-
97+
// requires(R1, B, P),
98+
// subset(R1, R2, P).
99+
requires.from_join(&requires_rp, &subset_r1p, |&(_r1, p), &b, &r2| (r2, b, p));
100+
101+
// requires(R, B, Q) :-
102+
// requires(R, B, P),
103+
// !killed(B, P),
104+
// cfg_edge(P, Q),
105+
// (region_live_at(R, Q); universal_region(R)).
106+
107+
requires_1.from_antijoin(&requires_bp, &killed, |&(b,p),&r| (p,(b,r)));
108+
requires_2.from_join(&requires_1, &cfg_edge_p, |&_p, &(b,r), &q| ((r,q),b));
109+
requires.from_join(&requires_2, &region_live_at, |&(r,q),&b,&()| (r,b,q));
110+
}
111+
112+
requires.complete()
113+
};
114+
115+
// borrow_live_at(B, P) :- requires(R, B, P), region_live_at(R, P)
116+
117+
// borrow_live_at(B, P) :- requires(R, B, P), universal_region(R).
118+
119+
}

src/join.rs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1+
//! Join functionality.
2+
13
use super::{Variable, Relation};
24

35
pub fn join_into<Key: Ord, Val1: Ord, Val2: Ord, Result: Ord, F: Fn(&Key, &Val1, &Val2)->Result>(
@@ -28,6 +30,7 @@ pub fn join_into<Key: Ord, Val1: Ord, Val2: Ord, Result: Ord, F: Fn(&Key, &Val1,
2830
output.insert(results.into());
2931
}
3032

33+
/// Moves all recent tuples from `input1` that are not present in `input2` into `output`.
3134
pub fn antijoin_into<Key: Ord, Val: Ord, Result: Ord, F: Fn(&Key, &Val)->Result>(
3235
input1: &Variable<(Key, Val)>,
3336
input2: &Relation<Key>,

src/lib.rs

Lines changed: 43 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,15 @@
1-
//! A lightweight Datalog executor in Rust
1+
//! A lightweight Datalog engine in Rust
22
//!
3-
//! The intended design is that there are static relations, perhaps described
4-
//! by sorted `Vec<(Key, Val)>` lists, at which point you can make an iterative
5-
//! context in which you can name variables, define computations, and bind the
6-
//! results to named variables.
3+
//! The intended design is that one has static `Relation` types that are sets
4+
//! of tuples, and `Variable` types that represent monotonically increasing
5+
//! sets of tuples.
76
//!
7+
//! The types are mostly wrappers around `Vec<Tuple>` indicating sorted-ness,
8+
//! and the intent is that this code can be dropped in the middle of an otherwise
9+
//! normal Rust program, run to completion, and then the results extracted as
10+
//! vectors again.
11+
12+
#![forbid(missing_docs)]
813

914
use std::rc::Rc;
1015
use std::cell::RefCell;
@@ -18,6 +23,10 @@ mod join;
1823
/// Datalog computation we want to be sure that certain relations are not able
1924
/// to vary (for example, in antijoins).
2025
pub struct Relation<Tuple: Ord> {
26+
/// Wrapped elements in the relation.
27+
///
28+
/// It is crucial that if this type is constructed manually, this field be
29+
/// sorted, and it is probably important that all elements be distinct.
2130
pub elements: Vec<Tuple>
2231
}
2332

@@ -87,14 +96,30 @@ pub trait VariableTrait {
8796
}
8897

8998
/// An monotonically increasing set of `Tuple`s.
99+
///
100+
/// The design here is that there are three types of tuples: i. those that have been
101+
/// processed by all operators that can access the variable, ii. those that should now
102+
/// be processed by all operators that can access the variable, and iii. those that
103+
/// have only just been added and should eventually be promoted to type ii. (but which
104+
/// are currently hidden).
105+
///
106+
/// Each time `self.changed()` is called, the `recent` relation is folded into `tuples`,
107+
/// and the `to_add` relations are merged, deduplicated against `tuples`, and then made
108+
/// `recent`. This way, across calls to `changed()` all added relations are at some point
109+
/// in `recent` once and eventually all are in `tuples`.
90110
pub struct Variable<Tuple: Ord> {
111+
/// A useful name for the variable.
91112
pub name: String,
113+
/// A list of relations whose union are the accepted tuples.
92114
pub tuples: Rc<RefCell<Vec<Relation<Tuple>>>>,
115+
/// A list of recent tuples, still to be processed.
93116
pub recent: Rc<RefCell<Relation<Tuple>>>,
117+
/// A list of future tuples, to be introduced.
94118
pub to_add: Rc<RefCell<Vec<Relation<Tuple>>>>,
95119
}
96120

97121
impl<Tuple: Ord> Variable<Tuple> {
122+
/// Adds tuples that result from joining `input1` and `input2`.
98123
pub fn from_join<K: Ord,V1: Ord, V2: Ord, F: Fn(&K,&V1,&V2)->Tuple>(
99124
&self,
100125
input1: &Variable<(K,V1)>,
@@ -103,6 +128,7 @@ impl<Tuple: Ord> Variable<Tuple> {
103128
{
104129
join::join_into(input1, input2, self, logic)
105130
}
131+
/// Adds tuples that result from antijoining `input1` and `input2`.
106132
pub fn from_antijoin<K: Ord,V: Ord, F: Fn(&K,&V)->Tuple>(
107133
&self,
108134
input1: &Variable<(K,V)>,
@@ -111,7 +137,7 @@ impl<Tuple: Ord> Variable<Tuple> {
111137
{
112138
join::antijoin_into(input1, input2, self, logic)
113139
}
114-
140+
/// Adds tuples that result from mapping `input`.
115141
pub fn from_map<T2: Ord, F: Fn(&T2)->Tuple>(&self, input: &Variable<T2>, logic: F) {
116142
map::map_into(input, self, logic)
117143
}
@@ -137,9 +163,20 @@ impl<Tuple: Ord> Variable<Tuple> {
137163
to_add: Rc::new(RefCell::new(Vec::new().into())),
138164
}
139165
}
166+
/// Inserts a relation into the variable.
167+
///
168+
/// This is most commonly used to load initial values into a variable.
169+
/// it is not obvious that it should be commonly used otherwise, but
170+
/// it should not be harmful.
140171
pub fn insert(&self, relation: Relation<Tuple>) {
141172
self.to_add.borrow_mut().push(relation);
142173
}
174+
/// Consumes the variable and returns a relation.
175+
///
176+
/// This method removes the ability for the variable to develop, and
177+
/// flattens all internal tuples down to one relation. The method
178+
/// asserts that iteration has completed, in that `self.recent` and
179+
/// `self.to_add` should both be empty.
143180
pub fn complete(self) -> Relation<Tuple> {
144181

145182
assert!(self.recent.borrow().is_empty());

src/map.rs

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1+
//! Map functionality.
2+
13
use super::Variable;
24

35
pub fn map_into<T1: Ord, T2: Ord, F: Fn(&T1)->T2>(
@@ -12,4 +14,4 @@ pub fn map_into<T1: Ord, T2: Ord, F: Fn(&T1)->T2>(
1214
}
1315

1416
output.insert(results.into());
15-
}
17+
}

0 commit comments

Comments
 (0)