## incremental deletion

when the insertion of a value depends on the non-presence of another (contained in a negated relation), then that means for insertions into a negated relation, existing facts must be removed if they can not be backed by any other rule. take for instance `C(x) :- A(x), !B(x).` which subtracts set B from set A. this is equivalent to `!C(x) :- !A(x). !C(x) :- B(x).`, which could be called deletion rules. simply put, `Y(x) :- X(x). Y(x) :- Z(x).`, without any further disjunctive rules, implies `!Y(x) :- !X(x),!Z(x).`, and in a "convex" set this can be ignored, but if `!X` and `!Z` conclusions exist, then `!Y` conclusions must also be realized. all this gives us clear logical paths to follow and thus seems reasonable to me, if only it is unclear how to implement this efficiently.
## incremental deletion when the insertion of a value depends on the non-presence of another (contained in a negated relation), then that means for insertions into a negated relation, existing facts must be removed if they can not be backed by any other rule. take for instance `C(x) :- A(x), !B(x).` which subtracts set B from set A. this is equivalent to `!C(x) :- !A(x). !C(x) :- B(x).`, which could be called deletion rules. simply put, `Y(x) :- X(x). Y(x) :- Z(x).`, without any further disjunctive rules, implies `!Y(x) :- !X(x),!Z(x).`, and in a "convex" set this can be ignored, but if `!X` and `!Z` conclusions exist, then `!Y` conclusions must also be realized. all this gives us clear logical paths to follow and thus seems reasonable to me, if only it is unclear how to implement this efficiently.
## incremental deletion

when the insertion of a value depends on the non-presence of another (contained in a negated relation), then that means for insertions into a negated relation, existing facts must be removed if they can not be backed by any other rule. take for instance `C(x) :- A(x), !B(x).` which subtracts set B from set A. this is equivalent to `!C(x) :- !A(x). !C(x) :- B(x).`, which could be called deletion rules. simply put, `Y(x) :- X(x). Y(x) :- Z(x).`, without any further disjunctive rules, implies `!Y(x) :- !X(x),!Z(x).`, and in a "convex" set this can be ignored, but if `!X` and `!Z` conclusions exist, then `!Y` conclusions must also be realized. all this gives us clear logical paths to follow and thus seems reasonable to me, if only it is unclear how to implement this efficiently.
## incremental deletion when the insertion of a value depends on the non-presence of another (contained in a negated relation), then that means for insertions into a negated relation, existing facts must be removed if they can not be backed by any other rule. take for instance `C(x) :- A(x), !B(x).` which subtracts set B from set A. this is equivalent to `!C(x) :- !A(x). !C(x) :- B(x).`, which could be called deletion rules. simply put, `Y(x) :- X(x). Y(x) :- Z(x).`, without any further disjunctive rules, implies `!Y(x) :- !X(x),!Z(x).`, and in a "convex" set this can be ignored, but if `!X` and `!Z` conclusions exist, then `!Y` conclusions must also be realized. all this gives us clear logical paths to follow and thus seems reasonable to me, if only it is unclear how to implement this efficiently.
## relations as first-class objects

logically, all relations could be collated into a single relation of polymorphic variadic type, where the relation itself becomes the first argument, i.e. `rel(x,...)` becomes `(rel,x,...)`.

this then makes it possible to e.g. match all relations that contain a specific value in a specific column, or to enumerate all relations that exist in the program, or to interrogate the program. it would also permit dynamic creation of new relations at runtime, although more properties are required to capture every aspect of a relation. to begin with, what is the arity of a relation? this, too, is an arbitrary constraint.

the "super relation" as i would call it also hosts every virtual relation, and thus likely has cosmic proportions, so can not be naively enumerated.
## relations as first-class objects logically, all relations could be collated into a single relation of polymorphic variadic type, where the relation itself becomes the first argument, i.e. `rel(x,...)` becomes `(rel,x,...)`. this then makes it possible to e.g. match all relations that contain a specific value in a specific column, or to enumerate all relations that exist in the program, or to interrogate the program. it would also permit dynamic creation of new relations at runtime, although more properties are required to capture every aspect of a relation. to begin with, what is the arity of a relation? this, too, is an arbitrary constraint. the "super relation" as i would call it also hosts every virtual relation, and thus likely has cosmic proportions, so can not be naively enumerated.
## incremental deletion

when the insertion of a value depends on the non-presence of another (contained in a negated relation), then that means for insertions into a negated relation, existing facts must be removed if they can not be backed by any other rule. take for instance `C(x) :- A(x), !B(x).` which subtracts set B from set A. this is equivalent to `!C(x) :- !A(x). !C(x) :- B(x).`, which could be called deletion rules. simply put, `Y(x) :- X(x). Y(x) :- Z(x).`, without any further disjunctive rules, implies `!Y(x) :- !X(x),!Z(x).`, and in a "convex" set this can be ignored, but if `!X` and `!Z` conclusions exist, then `!Y` conclusions must also be realized. all this gives us clear logical paths to follow and thus seems reasonable to me, if only it is unclear how to implement this efficiently.
## incremental deletion when the insertion of a value depends on the non-presence of another (contained in a negated relation), then that means for insertions into a negated relation, existing facts must be removed if they can not be backed by any other rule. take for instance `C(x) :- A(x), !B(x).` which subtracts set B from set A. this is equivalent to `!C(x) :- !A(x). !C(x) :- B(x).`, which could be called deletion rules. simply put, `Y(x) :- X(x). Y(x) :- Z(x).`, without any further disjunctive rules, implies `!Y(x) :- !X(x),!Z(x).`, and in a "convex" set this can be ignored, but if `!X` and `!Z` conclusions exist, then `!Y` conclusions must also be realized. all this gives us clear logical paths to follow and thus seems reasonable to me, if only it is unclear how to implement this efficiently.
# will produce following topological order and lifetimes:
    ---------------
    rel_order
    ===============
    0       i
    1       b
    1       a
    2       c
    2       d
    3       o
    ===============
    ---------------
    rel_lt
    ===============
    1       i
    2       b
    2       a
    3       o
    3       c
    3       d
    ===============

struct i (x : s32)
struct a (x : s32)
struct b (x : s32)
struct c (x : s32)
struct d (x : s32)
struct o (x : s32)

a x if (i x)

a x if (b x)
b x if (a x)

c x if (b x)
d x if (c x)
c x if (d x)

o x if (d x)
# will produce following topological order and lifetimes: --------------- rel_order =============== 0 i 1 b 1 a 2 c 2 d 3 o =============== --------------- rel_lt =============== 1 i 2 b 2 a 3 o 3 c 3 d =============== struct i (x : s32) struct a (x : s32) struct b (x : s32) struct c (x : s32) struct d (x : s32) struct o (x : s32) a x if (i x) a x if (b x) b x if (a x) c x if (b x) d x if (c x) c x if (d x) o x if (d x)
// topological order of relations
.decl rel_order(n:number, rel:symbol)
rel_order(i,rel) :- Rel(rel), scc(scc_id, rel),
    scc_order(i, scc_id).

// relation lifetime (after which order can we free this relation)
.decl rel_lt(n:number, rel:symbol)
rel_lt(i,rel) :- Rel(rel), scc(scc_id, rel),
    !scc_dep(_, scc_id),
    scc_order(i, scc_id).
rel_lt(mxi,rel) :- Rel(rel), scc(scc_id, rel),
    scc_dep(scc_user, scc_id),
    mxi = max i : {
        scc_order(i, scc_user)
    }.
// topological order of relations .decl rel_order(n:number, rel:symbol) rel_order(i,rel) :- Rel(rel), scc(scc_id, rel), scc_order(i, scc_id). // relation lifetime (after which order can we free this relation) .decl rel_lt(n:number, rel:symbol) rel_lt(i,rel) :- Rel(rel), scc(scc_id, rel), !scc_dep(_, scc_id), scc_order(i, scc_id). rel_lt(mxi,rel) :- Rel(rel), scc(scc_id, rel), scc_dep(scc_user, scc_id), mxi = max i : { scc_order(i, scc_user) }.

#include "dldsl_defines.hh"

.decl TypeKind(id:number, name:symbol)
#define T(NAME, STR, ...) TypeKind(autoinc(), STR):-true.
DLDSL_TYPES(T)
#undef T

.decl OpKind(id:number, name:symbol, mn:number, mx:number)
#define T(NAME, STR, MN, MX, ...) OpKind(autoinc(), STR, MN, MX):-true.
DLDSL_OP_KIND(T)
#undef T

.decl Type(name:symbol, kind:number, alias:symbol, builtin_name:symbol)

.decl Rel(name:symbol)
.decl RelAlias(name:symbol, alias:symbol)

.decl Field(rel:symbol, index:number, name:symbol, type:symbol)

.decl TermExpr(id:number, rel:symbol)
.decl OpExpr(id:number, type:symbol, op:number)
.decl ExprConst(id:number, index:number, type:symbol, value:symbol)
.decl ExprVar(id:number, index:number, name:symbol)
.decl ExprExpr(id:number, index:number, expr:number)

.decl Rule(id:number, conc_expr:number)
.decl RulePrem(id:number, expr_id:number)
.decl RuleVar(id:number, name:symbol, type:symbol)
#include "dldsl_defines.hh" .decl TypeKind(id:number, name:symbol) #define T(NAME, STR, ...) TypeKind(autoinc(), STR):-true. DLDSL_TYPES(T) #undef T .decl OpKind(id:number, name:symbol, mn:number, mx:number) #define T(NAME, STR, MN, MX, ...) OpKind(autoinc(), STR, MN, MX):-true. DLDSL_OP_KIND(T) #undef T .decl Type(name:symbol, kind:number, alias:symbol, builtin_name:symbol) .decl Rel(name:symbol) .decl RelAlias(name:symbol, alias:symbol) .decl Field(rel:symbol, index:number, name:symbol, type:symbol) .decl TermExpr(id:number, rel:symbol) .decl OpExpr(id:number, type:symbol, op:number) .decl ExprConst(id:number, index:number, type:symbol, value:symbol) .decl ExprVar(id:number, index:number, name:symbol) .decl ExprExpr(id:number, index:number, expr:number) .decl Rule(id:number, conc_expr:number) .decl RulePrem(id:number, expr_id:number) .decl RuleVar(id:number, name:symbol, type:symbol)

#include "dldsl_defines.hh"

.decl TypeKind(id:number, name:symbol)
#define T(NAME, STR, ...) TypeKind(autoinc(), STR):-true.
DLDSL_TYPES(T)
#undef T

.decl OpKind(id:number, name:symbol, mn:number, mx:number)
#define T(NAME, STR, MN, MX, ...) OpKind(autoinc(), STR, MN, MX):-true.
DLDSL_OP_KIND(T)
#undef T

.decl Type(name:symbol, kind:number, alias:symbol, builtin_name:symbol)

.decl Rel(name:symbol)
.decl RelAlias(name:symbol, alias:symbol)

.decl Field(rel:symbol, index:number, name:symbol, type:symbol)

.decl TermExpr(id:number, rel:symbol)
.decl OpExpr(id:number, type:symbol, op:number)
.decl ExprConst(id:number, index:number, type:symbol, value:symbol)
.decl ExprVar(id:number, index:number, name:symbol)
.decl ExprExpr(id:number, index:number, expr:number)

.decl Rule(id:number, conc_expr:number)
.decl RulePrem(id:number, expr_id:number)
.decl RuleVar(id:number, name:symbol, type:symbol)
#include "dldsl_defines.hh" .decl TypeKind(id:number, name:symbol) #define T(NAME, STR, ...) TypeKind(autoinc(), STR):-true. DLDSL_TYPES(T) #undef T .decl OpKind(id:number, name:symbol, mn:number, mx:number) #define T(NAME, STR, MN, MX, ...) OpKind(autoinc(), STR, MN, MX):-true. DLDSL_OP_KIND(T) #undef T .decl Type(name:symbol, kind:number, alias:symbol, builtin_name:symbol) .decl Rel(name:symbol) .decl RelAlias(name:symbol, alias:symbol) .decl Field(rel:symbol, index:number, name:symbol, type:symbol) .decl TermExpr(id:number, rel:symbol) .decl OpExpr(id:number, type:symbol, op:number) .decl ExprConst(id:number, index:number, type:symbol, value:symbol) .decl ExprVar(id:number, index:number, name:symbol) .decl ExprExpr(id:number, index:number, expr:number) .decl Rule(id:number, conc_expr:number) .decl RulePrem(id:number, expr_id:number) .decl RuleVar(id:number, name:symbol, type:symbol)

NIC> (split-by-level *k*)
((((0 0 -1) ((BAR) (BAR) (BAR) (BAR) (BAR) (BAR) (BAR)))
  ((0 1 -1) ((BAR) (BAR) (BAR) (BAR) (BAR) (BAR) (BAR)))
  ((0 2 -1) ((BAR) (BAR) (BAR) (BAR) (BAR) (BAR) (BAR)))
  ((0 3 -1) ((BAR) (BAR) (BAR) (BAR) (BAR) (BAR) (BAR)))
  ((0 4 -1) ((BAR) (BAR) (BAR) (BAR) (BAR) (BAR) (BAR)))
  ((0 5 -1) ((BAR) (BAR) (BAR) (BAR) (BAR) (BAR) (BAR))))
 (((0 0 0) ((BAR) (BAR) (BAR) (BAR) (BAR) (BAR) (BAR)))
  ((0 1 0) ((BAR) (FOO) (FOO) (FOO) (FOO) (FOO) (BAR)))
  ((0 2 0) ((BAR) (FOO) (FOO) (FOO) (FOO) (FOO) (BAR)))
  ((0 3 0) ((BAR) (FOO) (FOO) (FOO) (FOO) (FOO) (BAR)))
  ((0 4 0) ((BAR) (FOO) (FOO) (FOO) (FOO) (FOO) (BAR)))
  ((0 5 0) ((BAR) (BAR) (BAR) (BAR) (BAR) (BAR) (BAR))))
 (((0 0 1) ((BAR) (BAR) (BAR) (BAR) (BAR) (BAR) (BAR)))
  ((0 1 1) ((BAR) (BAR) (BAR) (BAR) (BAR) (BAR) (BAR)))
  ((0 2 1) ((BAR) (BAR) (BAR) (BAR) (BAR) (BAR) (BAR)))
  ((0 3 1) ((BAR) (BAR) (BAR) (BAR) (BAR) (BAR) (BAR)))
  ((0 4 1) ((BAR) (BAR) (BAR) (BAR) (BAR) (BAR) (BAR)))
  ((0 5 1) ((BAR) (BAR) (BAR) (BAR) (BAR) (BAR) (BAR)))))
NIC>
NIC> (split-by-level *k*) ((((0 0 -1) ((BAR) (BAR) (BAR) (BAR) (BAR) (BAR) (BAR))) ((0 1 -1) ((BAR) (BAR) (BAR) (BAR) (BAR) (BAR) (BAR))) ((0 2 -1) ((BAR) (BAR) (BAR) (BAR) (BAR) (BAR) (BAR))) ((0 3 -1) ((BAR) (BAR) (BAR) (BAR) (BAR) (BAR) (BAR))) ((0 4 -1) ((BAR) (BAR) (BAR) (BAR) (BAR) (BAR) (BAR))) ((0 5 -1) ((BAR) (BAR) (BAR) (BAR) (BAR) (BAR) (BAR)))) (((0 0 0) ((BAR) (BAR) (BAR) (BAR) (BAR) (BAR) (BAR))) ((0 1 0) ((BAR) (FOO) (FOO) (FOO) (FOO) (FOO) (BAR))) ((0 2 0) ((BAR) (FOO) (FOO) (FOO) (FOO) (FOO) (BAR))) ((0 3 0) ((BAR) (FOO) (FOO) (FOO) (FOO) (FOO) (BAR))) ((0 4 0) ((BAR) (FOO) (FOO) (FOO) (FOO) (FOO) (BAR))) ((0 5 0) ((BAR) (BAR) (BAR) (BAR) (BAR) (BAR) (BAR)))) (((0 0 1) ((BAR) (BAR) (BAR) (BAR) (BAR) (BAR) (BAR))) ((0 1 1) ((BAR) (BAR) (BAR) (BAR) (BAR) (BAR) (BAR))) ((0 2 1) ((BAR) (BAR) (BAR) (BAR) (BAR) (BAR) (BAR))) ((0 3 1) ((BAR) (BAR) (BAR) (BAR) (BAR) (BAR) (BAR))) ((0 4 1) ((BAR) (BAR) (BAR) (BAR) (BAR) (BAR) (BAR))) ((0 5 1) ((BAR) (BAR) (BAR) (BAR) (BAR) (BAR) (BAR))))) NIC>