633 lines
23 KiB
Haskell
633 lines
23 KiB
Haskell
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
|
|
|
|
-- | Evaluate a single AST term using a local environment augmented by
|
|
-- lazily-resolved store terms.
|
|
evalASTWithEnv :: Maybe Connection -> Env -> TricuAST -> IO T
|
|
evalASTWithEnv mconn localEnv ast = do
|
|
let varNames = collectVarNames ast
|
|
storeEnv <- resolveTermsFromStore mconn Map.empty varNames
|
|
let combinedEnv = Map.union localEnv storeEnv
|
|
return $ evalASTSync combinedEnv ast
|
|
|
|
-- | Store-aware version of 'evalSingle'.
|
|
evalSingleWithStore :: Maybe Connection -> Env -> TricuAST -> IO Env
|
|
evalSingleWithStore mconn env term
|
|
| SDef name [] body <- term = do
|
|
res <- evalASTWithEnv mconn env body
|
|
case Map.lookup name env of
|
|
Just existingValue
|
|
| existingValue == res -> return env
|
|
| otherwise -> return $ Map.insert "!result" res (Map.insert name res env)
|
|
Nothing -> return $ Map.insert "!result" res (Map.insert name res env)
|
|
| otherwise = do
|
|
res <- evalASTWithEnv mconn env term
|
|
return $ Map.insert "!result" res env
|
|
|
|
-- | Store-aware version of 'evalTricu'. Does not preload the entire
|
|
-- content store; terms are resolved on demand as variables are
|
|
-- encountered.
|
|
evalTricuWithStore :: Maybe Connection -> Env -> [TricuAST] -> IO Env
|
|
evalTricuWithStore mconn env x = go env (reorderDefs env x)
|
|
where
|
|
go env' [] = return env'
|
|
go env' [def] = do
|
|
updatedEnv <- evalSingleWithStore mconn env' def
|
|
return $ Map.insert "!result" (result updatedEnv) updatedEnv
|
|
go env' (def:xs) = do
|
|
updatedEnv <- evalSingleWithStore mconn env' def
|
|
evalTricuWithStore mconn updatedEnv xs
|
|
|
|
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
|