Dace

DACE: a minimal table/column DSL for reproducing the data-completion examples of Wang, Dillig & Singh, "Synthesis of Data Completion Scripts using Finite Tree Automata" (OOPSLA 2017), with aeon's FTA backend. A table is modeled as one or more Column globals (native Python lists); a missing cell holds the sentinel -999999. A synthesis task fills a missing cell given its index: the hole is `def fill (i:Int) : Int := ?` and the FTA composes the navigation/relational primitives below (plus arithmetic and conditionals) to reproduce the @example / @csv input-output rows.
Table of Contents

Types

Column

(type)
type Column

Functions

col_at

Value of cell i.
def col_at (c : Column) (i : Int) : Int

is_missing

Whether a value is the missing-cell sentinel.
def is_missing (x : Int) : Bool

prev_nonmissing

Previous non-missing value strictly before index i (sentinel if none).
def prev_nonmissing (c : Column) (i : Int) : Int

next_nonmissing

Next non-missing value strictly after index i (sentinel if none).
def next_nonmissing (c : Column) (i : Int) : Int

has_prev_nonmissing

Whether any non-missing cell exists strictly before index i.
def has_prev_nonmissing (c : Column) (i : Int) : Bool

prev_sameid

Previous non-missing value (before i) in `vals` whose row has the same id as row i in `ids` (sentinel if none) -- a relational predicate over cells.
def prev_sameid (ids : Column) (vals : Column) (i : Int) : Int

up_find_value

Index of the nearest cell at-or-above i whose value is v (-1 if none) -- the upward spatial path of Example 2.3.
def up_find_value (c : Column) (i : Int) (v : Int) : Int

down_first_nonzero

First non-zero value at-or-below index k (0 if none) -- the downward path that Example 2.3 turns onto after the upward search.
def down_first_nonzero (c : Column) (k : Int) : Int

group_count

Number of entries sharing row i's group id -- the COUNT-over-a-range of Example 2.4.
def group_count (groups : Column) (i : Int) : Int