45 lines
1.2 KiB
Plaintext
45 lines
1.2 KiB
Plaintext
|
// TodoList: A simple relational model for tracking tasks
|
||
|
|
//
|
||
|
|
// This demonstrates geolog as a persistent relational database.
|
||
|
|
// Elements represent tasks, and relations track their status.
|
||
|
|
|
||
|
|
theory TodoList {
|
||
|
|
// The sort of todo items
|
||
|
|
Item : Sort;
|
||
|
|
|
||
|
|
// Unary relations for item status (simple arrow syntax)
|
||
|
|
completed : Item -> Prop;
|
||
|
|
high_priority : Item -> Prop;
|
||
|
|
blocked : Item -> Prop;
|
||
|
|
|
||
|
|
// Binary relation for dependencies
|
||
|
|
depends : [item: Item, on: Item] -> Prop;
|
||
|
|
|
||
|
|
// Axiom: if an item depends on another, either it is blocked
|
||
|
|
// or the dependency is completed
|
||
|
|
ax/dep_blocked : forall x : Item, y : Item.
|
||
|
|
[item: x, on: y] depends |- x blocked \/ y completed;
|
||
|
|
}
|
||
|
|
|
||
|
|
// Example: An empty todo list ready for interactive use
|
||
|
|
instance MyTodos : TodoList = {
|
||
|
|
// Start empty - add items interactively with :add
|
||
|
|
}
|
||
|
|
|
||
|
|
// Example: A pre-populated todo list
|
||
|
|
instance SampleTodos : TodoList = {
|
||
|
|
// Items
|
||
|
|
buy_groceries : Item;
|
||
|
|
cook_dinner : Item;
|
||
|
|
do_laundry : Item;
|
||
|
|
clean_house : Item;
|
||
|
|
|
||
|
|
// Status: unary relations use simple syntax
|
||
|
|
buy_groceries completed;
|
||
|
|
cook_dinner high_priority;
|
||
|
|
|
||
|
|
// Dependencies: cook_dinner depends on buy_groceries
|
||
|
|
// Mixed syntax: first positional arg maps to 'item' field
|
||
|
|
[cook_dinner, on: buy_groceries] depends;
|
||
|
|
}
|