DataFrame

General tabular API: pandas orchestration + Array column bridge. ``DataFrame`` is a linear, opaque handle over a pandas ``DataFrame``. Relational work (I/O, select, join, groupby, null handling) stays in pandas. Dense numeric columns cross into ``Array`` via ``with_col`` / ``set_col`` / ``map_col`` so ``@llvm`` / ``@gpu`` kernels can run on contiguous buffers without compiling pandas itself. Machine-learning pipelines (``MLCore``, ``Learning*``) sit on top of this module.
Imports
open Array;
Table of Contents

Types

DataFrame

(type) linear
linear type DataFrame

DataFramePair

(type) linear
Linear pair from ``copy`` — unpack both with ``with_pair``.
linear type DataFramePair

DataFrameCol

(type) linear
Result of ``with_col``: frame + extracted numeric column.
linear type DataFrameCol

Functions

_df

def _df : Unit

read_csv

def read_csv (path : String) (expected_rows : Int | expected_rows ≥ 0) (expected_cols : Int | expected_cols ≥ 1) : {df : DataFrame | df_nrows df = expected_rows && df_ncols df = expected_cols}

to_csv

def to_csv (1 df : DataFrame) (path : String) : Unit

copy

def copy (1 df : DataFrame) : {pr : DataFramePair | pair_nrows pr = df_nrows df && pair_ncols pr = df_ncols df}

fst_df

def fst_df (1 pr : DataFramePair) : {df : DataFrame | df_nrows df = pair_nrows pr && df_ncols df = pair_ncols pr}

snd_df

def snd_df (1 pr : DataFramePair) : {df : DataFrame | df_nrows df = pair_nrows pr && df_ncols df = pair_ncols pr}

with_col

def with_col (1 df : DataFrame) (name : String) : {w : DataFrameCol | wc_nrows w = df_nrows df && wc_ncols w = df_ncols df}

wc_frame

def wc_frame (1 w : DataFrameCol) : {df : DataFrame | df_nrows df = wc_nrows w && df_ncols df = wc_ncols w}

wc_array

def wc_array (1 w : DataFrameCol) : {col : (Array Float) | size col = wc_nrows w}

nrows

def nrows (borrow df : DataFrame) : {n : Int | n = df_nrows df}

ncols

def ncols (borrow df : DataFrame) : {n : Int | n = df_ncols df}

columns

def columns (borrow df : DataFrame) : (Array String)

has_col

def has_col (borrow df : DataFrame) (name : String) : Bool

head

def head (1 df : DataFrame) (n : Int | n ≥ 0) : {r : DataFrame | df_ncols r = df_ncols df}

select

def select (1 df : DataFrame) (1 cols : (Array String)) : DataFrame

drop

def drop (1 df : DataFrame) (1 cols : (Array String)) : DataFrame

rename

def rename (1 df : DataFrame) (old : String) (new : String) : {r : DataFrame | df_nrows r = df_nrows df && df_ncols r = df_ncols df}

filter_rows

def filter_rows (1 df : DataFrame) (column : String) (pred : (x : Float) → Bool) : {r : DataFrame | df_ncols r = df_ncols df && df_nrows r ≤ df_nrows df}

dropna

def dropna (1 df : DataFrame) : {r : DataFrame | df_ncols r = df_ncols df}

fillna

def fillna (1 df : DataFrame) (value : Float) : {r : DataFrame | df_nrows r = df_nrows df && df_ncols r = df_ncols df}

sort_values

def sort_values (1 df : DataFrame) (column : String) (ascending : Bool) : {r : DataFrame | df_nrows r = df_nrows df && df_ncols r = df_ncols df}

concat

def concat (1 left : DataFrame) (1 right : DataFrame | df_ncols right = df_ncols left) : {out : DataFrame | df_ncols out = df_ncols left}

join

def join (1 left : DataFrame) (1 right : DataFrame) (on : String) (how : String) : DataFrame

groupby_agg

def groupby_agg (1 df : DataFrame) (by : String) (column : String) (how : String) : DataFrame

assign_const

def assign_const (1 df : DataFrame) (name : String) (value : Float) : {r : DataFrame | df_nrows r = df_nrows df}

col_as_array

def col_as_array (borrow df : DataFrame) (name : String) : {col : (Array Float) | size col = df_nrows df}

set_col

def set_col (1 df : DataFrame) (name : String) (1 col : (Array Float)) : {r : DataFrame | df_nrows r = size col}

map_col

Extract → transform → write back in one step (``f`` may be an ``@llvm`` kernel).
def map_col (1 df : DataFrame) (name : String) (f : (1 col : (Array Float)) → (Array Float)) : DataFrame

dispose

def dispose (1 df : DataFrame) : Unit

with_pair

def with_pair (1 token : DataFramePair) ( 1 consume : (1 left : DataFrame | df_nrows left = pair_nrows token && df_ncols left = pair_ncols token) → (1 right : DataFrame | df_nrows right = pair_nrows token && df_ncols right = pair_ncols token) → b ) : b

with_column

def with_column (1 token : DataFrameCol) ( 1 consume : (1 frame : DataFrame | df_nrows frame = wc_nrows token && df_ncols frame = wc_ncols token) → (1 column : (Array Float) | size column = wc_nrows token) → b ) : b

Uninterpreted

Functions declared as def f ... = uninterpreted: only their signature is known to the verifier; they have no body.

df_nrows

uninterpreted
Logical shape measures (SMT only; runtime witnesses below).
def df_nrows : (df : DataFrame) → Int

df_ncols

uninterpreted
def df_ncols : (df : DataFrame) → Int

pair_nrows

uninterpreted
def pair_nrows : (pr : DataFramePair) → Int

pair_ncols

uninterpreted
def pair_ncols : (pr : DataFramePair) → Int

wc_nrows

uninterpreted
def wc_nrows : (w : DataFrameCol) → Int

wc_ncols

uninterpreted
def wc_ncols : (w : DataFrameCol) → Int