tricu/src/Eval.hs

module Eval where

import ContentStore
import Parser
import Research

import Control.Monad (foldM)
import Data.List (partition, (\\), elemIndex, foldl')
import Data.Map  ()
import Data.Set  (Set)
import Database.SQLite.Simple

import qualified Data.Foldable as F ()
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Data.Text as T

data DB
  = BVar Int
  | BFree String
  | BLam DB
  | BApp DB DB
  | BLeaf
  | BStem DB
  | BFork DB DB
  | BStr String
  | BInt Integer
  | BList [DB]
  | BEmpty
  deriving (Eq, Show)

type Uses = [Bool]

evalSingle :: Env -> TricuAST -> Env
evalSingle env term
  | SDef name [] body <- term
  = case Map.lookup name env of
      Just existingValue
        | existingValue == evalASTSync env body -> env
        | otherwise
        -> let res = evalASTSync env body
           in Map.insert "!result" res (Map.insert name res env)
      Nothing
        -> let res = evalASTSync env body
           in Map.insert "!result" res (Map.insert name res env)
  | SApp func arg <- term
  = let res = apply (evalASTSync env func) (evalASTSync env arg)
    in Map.insert "!result" res env
  | SVar name Nothing <- term
  = case Map.lookup name env of
      Just v -> Map.insert "!result" v env
      Nothing -> errorWithoutStackTrace $ "Variable " ++ name ++ " not defined"
  | SVar name (Just hash) <- term
  = errorWithoutStackTrace $ "Hash-specific variable lookup not supported in local evaluation: " ++ name ++ "#" ++ hash
  | otherwise
  = let res = evalASTSync env term
    in Map.insert "!result" res env

evalTricu :: Env -> [TricuAST] -> Env
evalTricu env x = go env (reorderDefs env x)
  where
    go env' []     = env'
    go env' [def]    =
      let updatedEnv = evalSingle env' def
      in Map.insert "!result" (result updatedEnv) updatedEnv
    go env' (def:xs) =
      evalTricu (evalSingle env' def) xs

evalASTSync :: Env -> TricuAST -> T
evalASTSync env term = case term of
  SLambda _ _ -> evalASTSync env (elimLambda term)
  SVar name Nothing -> case Map.lookup name env of
    Just v -> v
    Nothing -> errorWithoutStackTrace $ "Variable " ++ name ++ " not defined"
  SVar name (Just hash) ->
    case Map.lookup (name ++ "#" ++ hash) env of
      Just v -> v
      Nothing -> errorWithoutStackTrace $
        "Variable " ++ name ++ " with hash " ++ hash ++ " not found in environment"
  TLeaf -> Leaf
  TStem t -> Stem (evalASTSync env t)
  TFork t u -> Fork (evalASTSync env t) (evalASTSync env u)
  SApp t u -> apply (evalASTSync env t) (evalASTSync env u)
  SStr s -> ofString s
  SInt n -> ofNumber n
  SList xs -> ofList (map (evalASTSync env) xs)
  SEmpty -> Leaf
  _ -> errorWithoutStackTrace $ "Unexpected AST term: " ++ show term

evalAST :: Maybe Connection -> Map.Map String T.Text -> TricuAST -> IO T
evalAST mconn selectedVersions ast = do
  let varNames = collectVarNames ast
  resolvedEnv <- resolveTermsFromStore mconn selectedVersions varNames
  return $ evalASTSync resolvedEnv ast

collectVarNames :: TricuAST -> [(String, Maybe String)]
collectVarNames = go []
  where
    go acc (SVar name mhash) = (name, mhash) : acc
    go acc (SApp t u) = go (go acc t) u
    go acc (SLambda vars body) =
      let boundVars = Set.fromList vars
          collected = go [] body
      in acc ++ filter (\(name, _) -> not $ Set.member name boundVars) collected
    go acc (TStem t) = go acc t
    go acc (TFork t u) = go (go acc t) u
    go acc (SList xs) = foldl' go acc xs
    go acc _ = acc

resolveTermsFromStore :: Maybe Connection -> Map.Map String T.Text -> [(String, Maybe String)] -> IO Env
resolveTermsFromStore Nothing _ _ = return Map.empty
resolveTermsFromStore (Just conn) selectedVersions varNames = do
  foldM (\env (name, mhash) -> do
    term <- resolveTermFromStore conn selectedVersions name mhash
    case term of
      Just t -> return $ Map.insert (getVarKey name mhash) t env
      Nothing -> return env
      ) Map.empty varNames
  where
    getVarKey name Nothing = name
    getVarKey name (Just hash) = name ++ "#" ++ hash

resolveTermFromStore :: Connection -> Map.Map String T.Text -> String -> Maybe String -> IO (Maybe T)
resolveTermFromStore conn selectedVersions name mhash = case mhash of
  Just hashPrefix -> do
    versions <- termVersions conn name
    let matchingVersions = filter (\(hash, _, _) ->
          T.isPrefixOf (T.pack hashPrefix) hash) versions
    case matchingVersions of
      [] -> return Nothing
      [(_, term, _)] -> return $ Just term
      _ -> return Nothing
  Nothing -> case Map.lookup name selectedVersions of
    Just hash -> loadTree conn hash
    Nothing -> do
      versions <- termVersions conn name
      case versions of
        [] -> return Nothing
        [(_, term, _)] -> return $ Just term
        _ -> return $ Just (head (map (\(_, t, _) -> t) versions))

elimLambda :: TricuAST -> TricuAST
elimLambda = go
  where
    go term
      | etaReduction term   = go (etaReduceResult term)
      | triagePattern term  = _TRI
      | composePattern term = _B
      | lambdaList term     = go (lambdaListResult term)
      | nestedLambda term   = nestedLambdaResult term
      | application term    = applicationResult term
      | isSList term        = slistTransform term
      | otherwise           = term

    etaReduction (SLambda [v] (SApp f (SVar x Nothing))) = v == x && not (usesBinder v f)
    etaReduction _ = False

    triagePattern (SLambda [a] (SLambda [b] (SLambda [c] body))) =
      toDB [c,b,a] body == triageBodyDB
    triagePattern _ = False

    composePattern (SLambda [f] (SLambda [g] (SLambda [x] body))) =
      toDB [x,g,f] body == composeBodyDB
    composePattern _ = False

    lambdaList (SLambda [_] (SList _)) = True
    lambdaList _ = False

    nestedLambda (SLambda (_:_) _) = True
    nestedLambda _ = False

    application (SApp _ _) = True
    application _ = False

    etaReduceResult (SLambda [_] (SApp f _)) = f
    etaReduceResult _ = error "etaReduceResult: expected SLambda [v] (SApp f _)"

    lambdaListResult (SLambda [v] (SList xs)) =
      SLambda [v] (foldr wrapTLeaf TLeaf xs)
      where
        wrapTLeaf m r = SApp (SApp TLeaf m) r
    lambdaListResult _ = error "lambdaListResult: expected SLambda [v] (SList xs)"

    nestedLambdaResult (SLambda (v:vs) body)
      | null vs   =
          let body' = go body
              db    = toDB [v] body'
          in toSKIKiselyov db
      | otherwise = go (SLambda [v] (SLambda vs body))
    nestedLambdaResult _ = error "nestedLambdaResult: expected SLambda (_:_) _"

    applicationResult (SApp f g) = SApp (go f) (go g)
    applicationResult _ = error "applicationResult: expected SApp _ _"

    isSList (SList _) = True
    isSList _         = False

    slistTransform :: TricuAST -> TricuAST
    slistTransform (SList xs) = foldr (\m r -> SApp (SApp TLeaf (go m)) r) TLeaf xs
    slistTransform ast = ast -- Should not be reached

_S, _K, _I, _R, _C, _B, _T, _TRI :: TricuAST
_S   = parseSingle "t (t (t t t)) t"
_K   = parseSingle "t t"
_I   = parseSingle "t (t (t t)) t"
_R   = parseSingle "(t (t (t t (t (t (t (t (t (t (t t (t (t (t t t)) t))) (t (t (t t (t t))) (t (t (t t t)) t)))) (t t (t t))))))) (t t))"
_C   = parseSingle "(t (t (t (t (t t (t (t (t t t)) t))) (t (t (t t (t t))) (t (t (t t t)) t)))) (t t (t t)))"
_B   = parseSingle "t (t (t t (t (t (t t t)) t))) (t t)"
_T   = SApp _C _I
_TRI = parseSingle "t (t (t t (t (t (t t t))))) t"

triageBody  :: String -> String -> String -> TricuAST
triageBody a b c   = SApp (SApp TLeaf (SApp (SApp TLeaf (SVar a Nothing)) (SVar b Nothing))) (SVar c Nothing)
composeBody :: String -> String -> String -> TricuAST
composeBody f g x  = SApp (SVar f Nothing) (SApp (SVar g Nothing) (SVar x Nothing))

isFree :: String -> TricuAST -> Bool
isFree x t = Set.member x (freeVars t)

-- Keep old freeVars for compatibility with reorderDefs which still uses TricuAST
freeVars :: TricuAST -> Set String
freeVars (SVar v Nothing) = Set.singleton v
freeVars (SVar v (Just _)) = Set.singleton v
freeVars (SApp t u) = Set.union (freeVars t) (freeVars u)
freeVars (SLambda vs body) = Set.difference (freeVars body) (Set.fromList vs)
freeVars (TStem t) = freeVars t
freeVars (TFork t u) = Set.union (freeVars t) (freeVars u)
freeVars (SList xs) = foldMap freeVars xs
freeVars _ = Set.empty

reorderDefs :: Env -> [TricuAST] -> [TricuAST]
reorderDefs env defs
  | not (null missingDeps) =
      errorWithoutStackTrace $
        "Missing dependencies detected: " ++ show missingDeps
  | otherwise = orderedDefs ++ others
  where
    (defsOnly, others) = partition isDef defs
    defNames = [ name | SDef name _ _ <- defsOnly ]

    defsWithFreeVars = [(def, freeVars body) | def@(SDef _ _ body) <- defsOnly]

    graph = buildDepGraph defsOnly
    sortedDefs = sortDeps graph
    defMap = Map.fromList [(name, def) | def@(SDef name _ _) <- defsOnly]
    orderedDefs = map (defMap Map.!) sortedDefs

    freeVarsDefs = foldMap snd defsWithFreeVars
    freeVarsOthers = foldMap freeVars others
    allFreeVars = freeVarsDefs <> freeVarsOthers
    validNames = Set.fromList defNames `Set.union` Set.fromList (Map.keys env)
    missingDeps = Set.toList (allFreeVars `Set.difference` validNames)

    isDef SDef {} = True
    isDef _       = False

buildDepGraph :: [TricuAST] -> Map.Map String (Set.Set String)
buildDepGraph topDefs
  | not (null conflictingDefs) =
      errorWithoutStackTrace $
        "Conflicting definitions detected: " ++ show conflictingDefs
  | otherwise =
      Map.fromList
        [ (name, depends topDefs (SDef name [] body))
        | SDef name _ body <- topDefs]
  where
    defsMap = Map.fromListWith (++)
      [(name, [(name, body)]) | SDef name _ body <- topDefs]

    conflictingDefs =
      [ name
      | (name, defs) <- Map.toList defsMap
      , let bodies = map snd defs
      , not $ all (== head bodies) (tail bodies)
      ]

sortDeps :: Map.Map String (Set.Set String) -> [String]
sortDeps graph = go [] Set.empty (Map.keys graph)
  where
    go sorted _sortedSet [] = sorted
    go sorted sortedSet remaining =
      let ready = [ name | name <- remaining
                        , let deps = Map.findWithDefault Set.empty name graph
                        , Set.isSubsetOf deps sortedSet ]
          notReady = remaining \\ ready
      in if null ready
         then errorWithoutStackTrace
          "ERROR: Cyclic dependency detected and prohibited.\n\
          \RESOLVE: Use nested lambdas."
         else go (sorted ++ ready)
                 (Set.union sortedSet (Set.fromList ready))
                 notReady

depends :: [TricuAST] -> TricuAST -> Set.Set String
depends topDefs (SDef _ _ body) =
  Set.intersection
    (Set.fromList [n | SDef n _ _ <- topDefs])
    (freeVars body)
depends _ _ = Set.empty

result :: Env -> T
result r = case Map.lookup "!result" r of
  Just a -> a
  Nothing -> errorWithoutStackTrace "No !result field found in provided env"

mainResult :: Env -> T
mainResult r = case Map.lookup "main" r of
  Just  a -> a
  Nothing -> errorWithoutStackTrace "No valid definition for `main` found."

findVarNames :: TricuAST -> [String]
findVarNames ast = case ast of
  SVar name _ -> [name]
  SApp a b -> findVarNames a ++ findVarNames b
  SLambda args body -> findVarNames body \\ args
  SDef name args body -> name : (findVarNames body \\ args)
  _ -> []

-- Convert named TricuAST to De Bruijn form
toDB :: [String] -> TricuAST -> DB
toDB env = \case
  SVar v _     -> maybe (BFree v) BVar (elemIndex v env)
  SLambda vs b ->
    let env' = reverse vs ++ env
        body = toDB env' b
    in foldr (\_ acc -> BLam acc) body vs
  SApp f a     -> BApp (toDB env f) (toDB env a)
  TLeaf        -> BLeaf
  TStem t      -> BStem (toDB env t)
  TFork l r    -> BFork (toDB env l) (toDB env r)
  SStr s       -> BStr s
  SInt n       -> BInt n
  SList xs     -> BList (map (toDB env) xs)
  SEmpty       -> BEmpty
  SDef{}       -> error "toDB: unexpected SDef at this stage"
  SImport _ _  -> BEmpty

-- Does a term depend on the current binder (level 0)?
dependsOnLevel :: Int -> DB -> Bool
dependsOnLevel lvl = \case
  BVar k      -> k == lvl
  BLam t      -> dependsOnLevel (lvl + 1) t
  BApp f a    -> dependsOnLevel lvl f || dependsOnLevel lvl a
  BStem t     -> dependsOnLevel lvl t
  BFork l r   -> dependsOnLevel lvl l || dependsOnLevel lvl r
  BList xs    -> any (dependsOnLevel lvl) xs
  _           -> False

-- Collect free *global* names (i.e., unbound)
freeDBNames :: DB -> Set String
freeDBNames = \case
  BFree s   -> Set.singleton s
  BVar _    -> mempty
  BLam t    -> freeDBNames t
  BApp f a  -> freeDBNames f <> freeDBNames a
  BLeaf     -> mempty
  BStem t   -> freeDBNames t
  BFork l r -> freeDBNames l <> freeDBNames r
  BStr _    -> mempty
  BInt _    -> mempty
  BList xs  -> foldMap freeDBNames xs
  BEmpty    -> mempty

-- Helper: "is the binder named v used in body?"
usesBinder :: String -> TricuAST -> Bool
usesBinder v body = dependsOnLevel 0 (toDB [v] body)

-- Expected DB bodies for the named special patterns (under env [a,b,c] -> indices 2,1,0)
triageBodyDB :: DB
triageBodyDB =
  BApp (BApp BLeaf (BApp (BApp BLeaf (BVar 2)) (BVar 1))) (BVar 0)

composeBodyDB :: DB
composeBodyDB =
  BApp (BVar 2) (BApp (BVar 1) (BVar 0))

-- Convert DB -> TricuAST for subterms that contain NO binders (no BLam, no BVar)
fromDBClosed :: DB -> TricuAST
fromDBClosed = \case
  BFree s   -> SVar s Nothing
  BApp f a  -> SApp (fromDBClosed f) (fromDBClosed a)
  BLeaf     -> TLeaf
  BStem t   -> TStem (fromDBClosed t)
  BFork l r -> TFork (fromDBClosed l) (fromDBClosed r)
  BStr s    -> SStr s
  BInt n    -> SInt n
  BList xs  -> SList (map fromDBClosed xs)
  BEmpty    -> SEmpty
  -- Anything bound would be a logic error if we call this correctly.
  BLam _    -> error "fromDBClosed: unexpected BLam"
  BVar _    -> error "fromDBClosed: unexpected bound variable"

-- DB-native bracket abstraction over the innermost binder (level 0).
-- This mirrors your old toSKI, but is purely index-driven.
toSKIDB :: DB -> TricuAST
toSKIDB t
  | not (dependsOnLevel 0 t) = SApp _K (fromDBClosed t)
toSKIDB (BVar 0)             = _I
toSKIDB (BApp n u)           = SApp (SApp _S (toSKIDB n)) (toSKIDB u)
toSKIDB (BStem t)             = toSKIDB (BApp BLeaf t)
toSKIDB (BFork l r)           = toSKIDB (BApp (BApp BLeaf l) r)
toSKIDB (BList xs)            = toSKIDB (foldr (\m r -> BApp (BApp BLeaf m) r) BLeaf xs)
toSKIDB other                 = error $ "toSKIDB: unsupported DB term: " ++ show other

app2 :: TricuAST -> TricuAST -> TricuAST
app2 f x = SApp f x

app3 :: TricuAST -> TricuAST -> TricuAST -> TricuAST
app3 f x y = SApp (SApp f x) y

-- Core converter that *does not* perform the λ-step; it just returns (Γ, d).
-- Supported shapes: variables, applications, closed literals (Leaf/Int/Str/Empty),
-- closed lists. For anything where the binder occurs under structural nodes
-- (Stem/Fork/List-with-use), we deliberately bail so the caller can fall back.
kisConv :: DB -> Either String (Uses, TricuAST)
kisConv = \case
  BVar 0     -> Right ([True], _I)
  BVar n | n > 0 -> do
    (g,d) <- kisConv (BVar (n - 1))
    Right (False:g, d)
  BVar n     -> Right ([], SVar ("BVar" ++ show n) Nothing)
  BFree s    -> Right ([], SVar s Nothing)
  BApp e1 e2 -> do
    (g1,d1) <- kisConv e1
    (g2,d2) <- kisConv e2
    let g = zipWithDefault False (||) g1 g2   -- <- propagate Γ outside (#)
        d = kisHash (g1,d1) (g2,d2)           -- <- (#) yields only the term
    Right (g, d)
  -- Treat closed constants as free 'combinator leaves' (no binder use).
  BLeaf      -> Right ([], TLeaf)
  BStr s     -> Right ([], SStr s)
  BInt n     -> Right ([], SInt n)
  BEmpty     -> Right ([], SEmpty)
  -- Closed list: allowed. If binder is used anywhere, we punt to fallback.
  BList xs
    | any (dependsOnLevel 0) xs -> Left "List with binder use: fallback"
    | otherwise                 -> Right ([], SList (map fromDBClosed xs))
  -- For structural nodes, only allow if *closed* wrt the binder.
  BStem t
    | dependsOnLevel 0 t -> Left "Stem with binder use: fallback"
    | otherwise          -> Right ([], TStem (fromDBClosed t))
  BFork l r
    | dependsOnLevel 0 l || dependsOnLevel 0 r -> Left "Fork with binder use: fallback"
    | otherwise                                -> Right ([], TFork (fromDBClosed l) (fromDBClosed r))
  -- We shouldn't see BLam under elim; treat as unsupported so we fallback.
  BLam _      -> Left "Nested lambda under body: fallback"

-- Application combiner with K-optimization (lazy weakening).
-- Mirrors Lynn's 'optK' rules: choose among S, B, C, R based on leading flags.
-- η-aware (#) with K-optimization (adapted from TS kiselyov_eta)
kisHash :: (Uses, TricuAST) -> (Uses, TricuAST) -> TricuAST
kisHash (g1, d1) (g2, d2) =
  case g1 of
    [] -> case g2 of
      []            -> SApp d1 d2
      True:gs2      -> if isId2 (g2, d2)
                         then d1
                         else kisHash ([], SApp _B d1) (gs2, d2)
      False:gs2     -> kisHash ([], d1) (gs2, d2)

    True:gs1 -> case g2 of
      []            -> if isId2 (g1, d1)
                         then SApp _T d2
                         else kisHash ([], SApp _R d2) (gs1, d1)
      _ ->
        if isId2 (g1, d1) && case g2 of { False:_ -> True; _ -> False }
          then kisHash ([], _T) (drop1 g2, d2)
        else
          -- NEW: coalesce the longest run of identical head pairs and apply bulk op once
          let ((h1, h2), count) = headPairRun g1 g2
              g1' = drop count g1
              g2' = drop count g2
          in case (h1, h2) of
               (False, False) ->
                 kisHash (g1', d1) (g2', d2)
               (False, True)  ->
                 let d1' = kisHash ([], bulkB count) (g1', d1)
                 in  kisHash (g1', d1') (g2', d2)
               (True, False)  ->
                 let d1' = kisHash ([], bulkC count) (g1', d1)
                 in  kisHash (g1', d1') (g2', d2)
               (True, True)   ->
                 let d1' = kisHash ([], bulkS count) (g1', d1)
                 in  kisHash (g1', d1') (g2', d2)

    False:gs1 -> case g2 of
      []            -> kisHash (gs1, d1) ([], d2)
      _             ->
        if isId2 (g1, d1) && case g2 of { False:_ -> True; _ -> False }
          then kisHash ([], _T) (drop1 g2, d2)
        else case g2 of
          True:gs2   ->
            let d1' = kisHash ([], _B) (gs1, d1)
            in  kisHash (gs1, d1') (gs2, d2)
          False:gs2  ->
            kisHash (gs1, d1) (gs2, d2)
  where
    drop1 (_:xs) = xs
    drop1 []     = []


toSKIKiselyov :: DB -> TricuAST
toSKIKiselyov body =
  case kisConv body of
    Right ([], d)          -> SApp _K d
    Right (True:_ , d)     -> d
    Right (False:g, d)     -> kisHash ([], _K) (g, d)  -- no snd
    Left _                 -> starSKIBCOpEtaDB body   -- was: toSKIDB body

zipWithDefault :: a -> (a -> a -> a) -> [a] -> [a] -> [a]
zipWithDefault d f []     ys     = map (f d) ys
zipWithDefault d f xs     []     = map (\x -> f x d) xs
zipWithDefault d f (x:xs) (y:ys) = f x y : zipWithDefault d f xs ys

isNode :: TricuAST -> Bool
isNode t = case t of
  TLeaf -> True
  _     -> False

isApp2 :: TricuAST -> Maybe (TricuAST, TricuAST)
isApp2 (SApp a b) = Just (a, b)
isApp2 _          = Nothing

isKop :: TricuAST -> Bool
isKop t = case isApp2 t of
  Just (a,b) -> isNode a && isNode b
  _          -> False

-- detects the two canonical I-shapes in the tree calculus:
--   △ (△ (△ △)) x    OR    △ (△ △ △) △
isId :: TricuAST -> Bool
isId t = case isApp2 t of
  Just (ab, c) -> case isApp2 ab of
    Just (a, b) | isNode a ->
      case isApp2 b of
        Just (b1, b2) ->
          (isNode b1 && isKop b2) ||
          (isKop b1 && isNode b2 && isNode c)
        _ -> False
    _ -> False
  _ -> False

-- head-True only, tail empty, and term is identity
isId2 :: (Uses, TricuAST) -> Bool
isId2 (True:[], t) = isId t
isId2 _            = False

-- Bulk helpers built from SKI (no new primitives)
bPrime :: TricuAST
bPrime = SApp _B _B                            -- B' = B B

cPrime :: TricuAST
cPrime = SApp (SApp _B (SApp _B _C)) _B        -- C' = B (B C) B

sPrime :: TricuAST
sPrime = SApp (SApp _B (SApp _B _S)) _B        -- S' = B (B S) B

bulkB :: Int -> TricuAST
bulkB n | n <= 1    = _B
        | otherwise = SApp bPrime (bulkB (n - 1))

bulkC :: Int -> TricuAST
bulkC n | n <= 1    = _C
        | otherwise = SApp cPrime (bulkC (n - 1))

bulkS :: Int -> TricuAST
bulkS n | n <= 1    = _S
        | otherwise = SApp sPrime (bulkS (n - 1))

headPairRun :: [Bool] -> [Bool] -> ((Bool, Bool), Int)
headPairRun g1 g2 =
  case zip g1 g2 of
    []       -> ((False, False), 0)
    (h:rest) -> (h, 1 + length (takeWhile (== h) rest))

-- DB-native star_skibc_op_eta (adapted from strategies.mts), binder = level 0
starSKIBCOpEtaDB :: DB -> TricuAST
starSKIBCOpEtaDB t
  | not (dependsOnLevel 0 t) = SApp _K (fromDBClosed t)
starSKIBCOpEtaDB (BVar 0)     = _I
starSKIBCOpEtaDB (BApp e1 e2)
  -- if binder not in right: use C
  | not (dependsOnLevel 0 e2)
  = SApp (SApp _C (starSKIBCOpEtaDB e1)) (fromDBClosed e2)
  -- if binder not in left:
  | not (dependsOnLevel 0 e1)
  = case e2 of
      -- η case: \x. f x  ==>  f
      BVar 0 -> fromDBClosed e1
      _      -> SApp (SApp _B (fromDBClosed e1)) (starSKIBCOpEtaDB e2)
  -- otherwise: S
  | otherwise
  = SApp (SApp _S (starSKIBCOpEtaDB e1)) (starSKIBCOpEtaDB e2)
-- Structural nodes with binder underneath: fall back to plain SKI (rare)
starSKIBCOpEtaDB other        = toSKIDB other