Schema.hs

{-# LANGUAGE OverloadedStrings #-}

-- | Schema for persisting srtree e-graphs.
--
-- Two logical sections, potentially in separate DB files:
--   * E-graph section (dataset-agnostic, read-only during fitting):
--     @meta@, @enode@, @enode_child@, @eclass@, @eclass_node@,
--     @cstore_page@, @frontier@
--   * Dataset-fit section (per-dataset, write-heavy during fitting):
--     @dataset@, @dataset_fit@, @expression_index@
--
-- 'structureSchemaSQL' is the DDL for a structure-only egraph DB.
-- 'egraphSchemaSQL' is the legacy combined DDL (structure + dataset tables).
-- 'fitSchemaSQL' is the DDL for a per-dataset fit DB (no FK to eclass).
module Algorithm.EqSat.Storage.Schema
  ( structureSchemaSQL
  , egraphSchemaSQL
  , fitSchemaSQL
  , createSchema
  , createSchemaStructure
  , createSchemaFit
  ) where

import Data.Text (Text)

import Algorithm.EqSat.Storage.Backend (SqlBackend(..))

-- | DDL for a structure-only egraph database.
--
-- This is the split-DB egraph section: no dataset/fit tables, so an egraph DB
-- written in split mode contains no per-dataset data at rest.
structureSchemaSQL :: [Text]
structureSchemaSQL =
  [ "CREATE TABLE IF NOT EXISTS meta ("
    <> " key TEXT PRIMARY KEY,"
    <> " value TEXT NOT NULL)"
  , "CREATE TABLE IF NOT EXISTS enode ("
    <> " key TEXT PRIMARY KEY,"
    <> " op TEXT NOT NULL,"
    <> " op_detail TEXT,"
    <> " a INTEGER,"
    <> " b INTEGER,"
    <> " x REAL)"
  , "CREATE TABLE IF NOT EXISTS enode_child ("
    <> " enode_key TEXT NOT NULL REFERENCES enode(key) ON DELETE CASCADE,"
    <> " child_eid INTEGER NOT NULL,"
    <> " cnt INTEGER NOT NULL DEFAULT 1,"
    <> " PRIMARY KEY (enode_key, child_eid))"
  , "CREATE TABLE IF NOT EXISTS enode_parent ("
    <> " child_eid INTEGER NOT NULL,"
    <> " enode_key TEXT NOT NULL,"
    <> " parent_eid INTEGER NOT NULL,"
    <> " PRIMARY KEY (child_eid, enode_key))"
  , "CREATE TABLE IF NOT EXISTS eclass ("
    <> " eid INTEGER PRIMARY KEY,"
    <> " canonical INTEGER NOT NULL,"
    <> " height INTEGER NOT NULL DEFAULT 0)"
  , "CREATE TABLE IF NOT EXISTS eclass_node ("
    <> " eid INTEGER NOT NULL REFERENCES eclass(eid) ON DELETE CASCADE,"
    <> " enode_key TEXT NOT NULL REFERENCES enode(key) ON DELETE CASCADE,"
    <> " PRIMARY KEY (eid, enode_key))"
  , "CREATE TABLE IF NOT EXISTS cstore_page ("
    <> " key INTEGER PRIMARY KEY,"
    <> " blob BLOB NOT NULL)"
  , "CREATE TABLE IF NOT EXISTS frontier ("
    <> " eid INTEGER PRIMARY KEY REFERENCES eclass(eid) ON DELETE CASCADE,"
    <> " updated_at TEXT)"
  ]

-- | Dataset/fit tables used by the legacy combined egraph DB (with FKs to
-- @eclass@) and by 'importEqs'.
datasetSchemaSQL :: [Text]
datasetSchemaSQL =
  [ "CREATE TABLE IF NOT EXISTS dataset ("
    <> " id INTEGER PRIMARY KEY,"
    <> " name TEXT NOT NULL UNIQUE,"
    <> " created TEXT)"
  , "CREATE TABLE IF NOT EXISTS dataset_fit ("
    <> " dataset_id INTEGER NOT NULL REFERENCES dataset(id) ON DELETE CASCADE,"
    <> " eid INTEGER NOT NULL REFERENCES eclass(eid) ON DELETE CASCADE,"
    <> " fitness REAL,"
    <> " dl REAL,"
    <> " theta TEXT,"
    <> " size INTEGER NOT NULL DEFAULT 0,"
    <> " evaluated INTEGER NOT NULL DEFAULT 0,"
    <> " fitted INTEGER NOT NULL DEFAULT 0,"
    <> " stale INTEGER NOT NULL DEFAULT 0,"
    <> " updated_at TEXT,"
    <> " PRIMARY KEY (dataset_id, eid))"
  , "CREATE TABLE IF NOT EXISTS expression_index ("
    <> " expression_key TEXT PRIMARY KEY,"
    <> " eclass INTEGER NOT NULL REFERENCES eclass(eid) ON DELETE CASCADE,"
    <> " dataset_id INTEGER REFERENCES dataset(id) ON DELETE CASCADE,"
    <> " first_seen TEXT)"
  ]

-- | DDL for the legacy combined egraph database (structure + dataset tables).
-- Kept for backward compatibility with importEqs and old DB files.
egraphSchemaSQL :: [Text]
egraphSchemaSQL = structureSchemaSQL <> datasetSchemaSQL

-- | DDL for a per-dataset fit database.
-- No FK to eclass (e-graph lives in a separate DB).
fitSchemaSQL :: [Text]
fitSchemaSQL =
  [ "CREATE TABLE IF NOT EXISTS dataset ("
    <> " id INTEGER PRIMARY KEY,"
    <> " name TEXT NOT NULL UNIQUE,"
    <> " created TEXT)"
  , "CREATE TABLE IF NOT EXISTS dataset_fit ("
    <> " dataset_id INTEGER NOT NULL REFERENCES dataset(id) ON DELETE CASCADE,"
    <> " eid INTEGER NOT NULL,"
    <> " fitness REAL,"
    <> " dl REAL,"
    <> " theta TEXT,"
    <> " size INTEGER NOT NULL DEFAULT 0,"
    <> " evaluated INTEGER NOT NULL DEFAULT 0,"
    <> " fitted INTEGER NOT NULL DEFAULT 0,"
    <> " stale INTEGER NOT NULL DEFAULT 0,"
    <> " updated_at TEXT,"
    <> " PRIMARY KEY (dataset_id, eid))"
  , "CREATE TABLE IF NOT EXISTS expression_index ("
    <> " expression_key TEXT PRIMARY KEY,"
    <> " eclass INTEGER NOT NULL,"
    <> " dataset_id INTEGER REFERENCES dataset(id) ON DELETE CASCADE,"
    <> " first_seen TEXT)"
  ]

-- | Create (or ensure) the legacy combined egraph schema on the given backend.
createSchema :: SqlBackend db => db -> IO ()
createSchema = createSchemaDb

-- | Create (or ensure) the structure-only egraph schema on the given backend.
createSchemaStructure :: SqlBackend db => db -> IO ()
createSchemaStructure = createSchemaDbStructure

-- | Create (or ensure) the fit schema on the given backend.
createSchemaFit :: SqlBackend db => db -> IO ()
createSchemaFit = createSchemaDbFit