131 lines
3.7 KiB
Plaintext
131 lines
3.7 KiB
Plaintext
// Example: RelAlgIR query plan instances
|
|
//
|
|
// This demonstrates creating query plans as RelAlgIR instances.
|
|
// These show the string diagram representation of relational algebra.
|
|
//
|
|
// First we need to load both GeologMeta (for Srt, Func, etc.) and RelAlgIR.
|
|
// This file just defines instances; load theories first in the REPL:
|
|
// :load theories/GeologMeta.geolog
|
|
// :load theories/RelAlgIR.geolog
|
|
// :load examples/geolog/relalg_simple.geolog
|
|
//
|
|
// Note: RelAlgIR extends GeologMeta, so a RelAlgIR instance contains
|
|
// elements from both GeologMeta sorts (Srt, Func, Elem) and RelAlgIR
|
|
// sorts (Wire, Schema, ScanOp, etc.)
|
|
|
|
// ============================================================
|
|
// Example 1: Simple Scan
|
|
// ============================================================
|
|
// Query: "scan all elements of sort V"
|
|
// Plan: () --[ScanOp]--> Wire
|
|
|
|
instance ScanV : RelAlgIR = chase {
|
|
// -- Schema (target theory) --
|
|
target_theory : GeologMeta/Theory;
|
|
target_theory GeologMeta/Theory/parent = target_theory;
|
|
|
|
v_srt : GeologMeta/Srt;
|
|
v_srt GeologMeta/Srt/theory = target_theory;
|
|
|
|
// -- Query Plan --
|
|
v_base_schema : BaseSchema;
|
|
v_base_schema BaseSchema/srt = v_srt;
|
|
|
|
v_schema : Schema;
|
|
v_base_schema BaseSchema/schema = v_schema;
|
|
|
|
scan_out : Wire;
|
|
scan_out Wire/schema = v_schema;
|
|
|
|
scan : ScanOp;
|
|
scan ScanOp/srt = v_srt;
|
|
scan ScanOp/out = scan_out;
|
|
|
|
scan_op : Op;
|
|
scan ScanOp/op = scan_op;
|
|
}
|
|
|
|
// ============================================================
|
|
// Example 2: Filter(Scan)
|
|
// ============================================================
|
|
// Query: "scan E, filter where src(e) = some vertex"
|
|
// Plan: () --[Scan]--> w1 --[Filter]--> w2
|
|
//
|
|
// This demonstrates composition via wire sharing.
|
|
|
|
// Uses chase to derive relations.
|
|
instance FilterScan : RelAlgIR = chase {
|
|
// -- Schema (representing Graph theory) --
|
|
target_theory : GeologMeta/Theory;
|
|
target_theory GeologMeta/Theory/parent = target_theory;
|
|
|
|
// Sorts: V (vertices), E (edges)
|
|
v_srt : GeologMeta/Srt;
|
|
v_srt GeologMeta/Srt/theory = target_theory;
|
|
|
|
e_srt : GeologMeta/Srt;
|
|
e_srt GeologMeta/Srt/theory = target_theory;
|
|
|
|
// Functions: src : E -> V
|
|
// First create the DSort wrappers
|
|
v_base_ds : GeologMeta/BaseDS;
|
|
v_base_ds GeologMeta/BaseDS/srt = v_srt;
|
|
|
|
e_base_ds : GeologMeta/BaseDS;
|
|
e_base_ds GeologMeta/BaseDS/srt = e_srt;
|
|
|
|
v_dsort : GeologMeta/DSort;
|
|
v_base_ds GeologMeta/BaseDS/dsort = v_dsort;
|
|
|
|
e_dsort : GeologMeta/DSort;
|
|
e_base_ds GeologMeta/BaseDS/dsort = e_dsort;
|
|
|
|
src_func : GeologMeta/Func;
|
|
src_func GeologMeta/Func/theory = target_theory;
|
|
src_func GeologMeta/Func/dom = e_dsort;
|
|
src_func GeologMeta/Func/cod = v_dsort;
|
|
|
|
// NOTE: For a complete example, we'd also need an Instance element
|
|
// and Elem elements. For simplicity, we use a simpler predicate structure.
|
|
|
|
// Using TruePred for now (matches all, demonstrating structure)
|
|
|
|
// -- Query Plan --
|
|
// Schema for E
|
|
e_base_schema : BaseSchema;
|
|
e_base_schema BaseSchema/srt = e_srt;
|
|
|
|
e_schema : Schema;
|
|
e_base_schema BaseSchema/schema = e_schema;
|
|
|
|
// Wire 1: output of Scan (E elements)
|
|
w1 : Wire;
|
|
w1 Wire/schema = e_schema;
|
|
|
|
// Wire 2: output of Filter (filtered E elements)
|
|
w2 : Wire;
|
|
w2 Wire/schema = e_schema;
|
|
|
|
// Scan operation
|
|
scan : ScanOp;
|
|
scan ScanOp/srt = e_srt;
|
|
scan ScanOp/out = w1;
|
|
|
|
scan_op : Op;
|
|
scan ScanOp/op = scan_op;
|
|
|
|
// Predicate: TruePred (matches all - demonstrates filter structure)
|
|
true_pred : TruePred;
|
|
pred_elem : Pred;
|
|
true_pred TruePred/pred = pred_elem;
|
|
|
|
// Filter operation: w1 --[Filter(pred)]--> w2
|
|
filter : FilterOp;
|
|
filter FilterOp/in = w1;
|
|
filter FilterOp/out = w2;
|
|
filter FilterOp/pred = pred_elem;
|
|
|
|
filter_op : Op;
|
|
filter FilterOp/op = filter_op;
|
|
}
|