Picking development back up
Merge Kiselyov optimizations and De Bruijn indices General clean up
This commit is contained in:
@@ -3,17 +3,17 @@ module ContentStore where
|
||||
import Research
|
||||
import Parser
|
||||
|
||||
import Control.Monad (foldM, forM)
|
||||
import Control.Monad (foldM, forM_, void)
|
||||
import Data.ByteString (ByteString)
|
||||
import Data.List (nub, sort)
|
||||
import Data.Maybe (catMaybes, fromJust)
|
||||
import Data.Maybe (catMaybes, fromMaybe)
|
||||
import Data.Text (Text)
|
||||
import Database.SQLite.Simple
|
||||
import Database.SQLite.Simple.FromRow (FromRow(..), field)
|
||||
import System.Directory (createDirectoryIfMissing, getXdgDirectory, XdgDirectory(..))
|
||||
import System.FilePath ((</>), takeDirectory)
|
||||
|
||||
import qualified Data.ByteString as BS
|
||||
|
||||
import qualified Data.Map as Map
|
||||
import qualified Data.Text as T
|
||||
|
||||
@@ -47,7 +47,6 @@ initContentStore = do
|
||||
execute_ conn "CREATE TABLE IF NOT EXISTS terms (\
|
||||
\hash TEXT PRIMARY KEY, \
|
||||
\names TEXT, \
|
||||
\term_data BLOB, \
|
||||
\metadata TEXT, \
|
||||
\created_at INTEGER DEFAULT (strftime('%s','now')), \
|
||||
\tags TEXT DEFAULT '')"
|
||||
@@ -83,8 +82,8 @@ storeTerm conn newNamesStrList term = do
|
||||
[] -> do
|
||||
let allNamesToStore = serializeNameList newNamesTextList
|
||||
execute conn
|
||||
"INSERT INTO terms (hash, names, term_data, metadata, tags) VALUES (?, ?, ?, ?, ?)"
|
||||
(termHashText, allNamesToStore, BS.pack [], metadataText, T.pack "")
|
||||
"INSERT INTO terms (hash, names, metadata, tags) VALUES (?, ?, ?, ?)"
|
||||
(termHashText, allNamesToStore, metadataText, T.pack "")
|
||||
[(Only currentNamesText)] -> do
|
||||
let currentNamesList = parseNameList currentNamesText
|
||||
let combinedNamesList = currentNamesList ++ newNamesTextList
|
||||
@@ -92,7 +91,7 @@ storeTerm conn newNamesStrList term = do
|
||||
execute conn
|
||||
"UPDATE terms SET names = ?, metadata = ? WHERE hash = ?"
|
||||
(allNamesToStore, metadataText, termHashText)
|
||||
_ -> error $ "Multiple terms with same hash? " ++ show (length existingNamesQuery)
|
||||
_ -> errorWithoutStackTrace $ "Multiple terms with same hash? " ++ show (length existingNamesQuery)
|
||||
|
||||
return termHashText
|
||||
|
||||
@@ -108,11 +107,11 @@ loadTree conn h
|
||||
where
|
||||
buildTree :: Node -> IO T
|
||||
buildTree (NStem childHash) = do
|
||||
child <- fromJust <$> loadTree conn childHash
|
||||
child <- fromMaybe (errorWithoutStackTrace "BUG: stored hash not found") <$> loadTree conn childHash
|
||||
return (Stem child)
|
||||
buildTree (NFork lHash rHash) = do
|
||||
left <- fromJust <$> loadTree conn lHash
|
||||
right <- fromJust <$> loadTree conn rHash
|
||||
left <- fromMaybe (errorWithoutStackTrace "BUG: stored hash not found") <$> loadTree conn lHash
|
||||
right <- fromMaybe (errorWithoutStackTrace "BUG: stored hash not found") <$> loadTree conn rHash
|
||||
return (Fork left right)
|
||||
|
||||
-- | Store all nodes of a Merkle DAG by traversing the Term and building/storing nodes.
|
||||
@@ -161,14 +160,14 @@ listStoredTerms :: Connection -> IO [StoredTerm]
|
||||
listStoredTerms conn =
|
||||
query_ conn (selectStoredTermFields <> " ORDER BY created_at DESC")
|
||||
|
||||
storeEnvironment :: Connection -> Env -> IO [(String, Text)]
|
||||
storeEnvironment :: Connection -> Env -> IO ()
|
||||
storeEnvironment conn env = do
|
||||
let defs = Map.toList $ Map.delete "!result" env
|
||||
let groupedDefs = Map.toList $ Map.fromListWith (++) [(term, [name]) | (name, term) <- defs]
|
||||
|
||||
forM groupedDefs $ \(term, namesList) -> do
|
||||
hashVal <- storeTerm conn namesList term
|
||||
return (head namesList, hashVal)
|
||||
forM_ groupedDefs $ \(term, namesList) -> case namesList of
|
||||
n:ns -> void $ storeTerm conn namesList term
|
||||
_ -> errorWithoutStackTrace "storeEnvironment: empty names list"
|
||||
|
||||
loadTerm :: Connection -> String -> IO (Maybe T)
|
||||
loadTerm conn identifier = do
|
||||
|
||||
392
src/Eval.hs
392
src/Eval.hs
@@ -4,14 +4,32 @@ import ContentStore
|
||||
import Parser
|
||||
import Research
|
||||
|
||||
import Control.Monad (forM_, foldM)
|
||||
import Data.List (partition, (\\))
|
||||
import Control.Monad (foldM)
|
||||
import Data.List (partition, (\\), elemIndex, foldl')
|
||||
import Data.Map (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
|
||||
import Data.List (foldl')
|
||||
|
||||
data DB
|
||||
= BVar Int -- bound (0 = nearest binder)
|
||||
| BFree String -- free/global
|
||||
| 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
|
||||
@@ -119,45 +137,59 @@ resolveTermFromStore conn selectedVersions name mhash = case mhash of
|
||||
case versions of
|
||||
[] -> return Nothing
|
||||
[(_, term, _)] -> return $ Just term
|
||||
_ -> return $ Just $ (\(_, t, _) -> t) $ head versions
|
||||
_ -> return $ Just $ (\(_, t, _) -> t) $ case versions of (_:_) -> head versions; _ -> error "resolveTermFromStore: unexpected empty versions list"
|
||||
|
||||
elimLambda :: TricuAST -> TricuAST
|
||||
elimLambda = go
|
||||
where
|
||||
go term
|
||||
| etaReduction term = elimLambda $ etaReduceResult term
|
||||
| etaReduction term = go (etaReduceResult term)
|
||||
| triagePattern term = _TRI
|
||||
| composePattern term = _B
|
||||
| lambdaList term = elimLambda $ lambdaListResult term
|
||||
| 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 (isFree v f)
|
||||
etaReduction (SLambda [v] (SApp f (SVar x Nothing))) = v == x && not (usesBinder v f)
|
||||
etaReduction _ = False
|
||||
etaReduceResult (SLambda [_] (SApp f _)) = f
|
||||
|
||||
triagePattern (SLambda [a] (SLambda [b] (SLambda [c] body))) = body == triageBody a b c
|
||||
-- triage: \a b c -> TLeaf (TLeaf a b) c (checked in DB with a↦2, b↦1, c↦0)
|
||||
triagePattern (SLambda [a] (SLambda [b] (SLambda [c] body))) =
|
||||
toDB [c,b,a] body == triageBodyDB
|
||||
triagePattern _ = False
|
||||
|
||||
composePattern (SLambda [f] (SLambda [g] (SLambda [x] body))) = body == composeBody f g x
|
||||
-- compose: \f g x -> f (g x) (checked in DB with f↦2, g↦1, x↦0)
|
||||
composePattern (SLambda [f] (SLambda [g] (SLambda [x] body))) =
|
||||
toDB [x,g,f] body == composeBodyDB
|
||||
composePattern _ = False
|
||||
|
||||
lambdaList (SLambda [_] (SList _)) = True
|
||||
lambdaList _ = False
|
||||
lambdaListResult (SLambda [v] (SList xs)) = SLambda [v] (foldr wrapTLeaf TLeaf xs)
|
||||
wrapTLeaf m r = SApp (SApp TLeaf m) r
|
||||
|
||||
nestedLambda (SLambda (_:_) _) = True
|
||||
nestedLambda _ = False
|
||||
nestedLambdaResult (SLambda (v:vs) body)
|
||||
| null vs = toSKI v (go body) -- Changed elimLambda to go
|
||||
| otherwise = go (SLambda [v] (SLambda vs body)) -- Changed elimLambda to go
|
||||
|
||||
application (SApp _ _) = True
|
||||
application _ = False
|
||||
applicationResult (SApp f g) = SApp (go f) (go g) -- Changed elimLambda to go
|
||||
|
||||
-- rewrites
|
||||
etaReduceResult (SLambda [_] (SApp f _)) = f
|
||||
|
||||
lambdaListResult (SLambda [v] (SList xs)) =
|
||||
SLambda [v] (foldr wrapTLeaf TLeaf xs)
|
||||
where
|
||||
wrapTLeaf m r = SApp (SApp TLeaf m) r
|
||||
|
||||
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))
|
||||
|
||||
applicationResult (SApp f g) = SApp (go f) (go g)
|
||||
|
||||
isSList (SList _) = True
|
||||
isSList _ = False
|
||||
@@ -166,27 +198,23 @@ elimLambda = go
|
||||
slistTransform (SList xs) = foldr (\m r -> SApp (SApp TLeaf (go m)) r) TLeaf xs
|
||||
slistTransform ast = ast -- Should not be reached if isSList is the guard
|
||||
|
||||
toSKI x (SVar y Nothing)
|
||||
| x == y = _I
|
||||
| otherwise = SApp _K (SVar y Nothing)
|
||||
toSKI x (SApp m n) = SApp (SApp _S (toSKI x m)) (toSKI x n)
|
||||
toSKI x (SLambda [y] body) = toSKI x (toSKI y body) -- This should ideally not happen if lambdas are fully eliminated first
|
||||
toSKI _ sl@(SList _) = SApp _K (go sl) -- Ensure SList itself is transformed if somehow passed to toSKI directly
|
||||
toSKI _ term = SApp _K term
|
||||
_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"
|
||||
|
||||
_S = parseSingle "t (t (t t t)) t"
|
||||
_K = parseSingle "t t"
|
||||
_I = parseSingle "t (t (t t)) t"
|
||||
_B = parseSingle "t (t (t t (t (t (t t t)) t))) (t t)"
|
||||
_TRI = parseSingle "t (t (t t (t (t (t t t))))) t"
|
||||
|
||||
triageBody a b c = SApp (SApp TLeaf (SApp (SApp TLeaf (SVar a Nothing)) (SVar b Nothing))) (SVar c Nothing)
|
||||
composeBody f g x = SApp (SVar f Nothing) (SVar g Nothing) -- Note: This might not be the standard B combinator body f(g x)
|
||||
triageBody a b c = SApp (SApp TLeaf (SApp (SApp TLeaf (SVar a Nothing)) (SVar b Nothing))) (SVar c Nothing)
|
||||
composeBody f g x = SApp (SVar f Nothing) (SApp (SVar g Nothing) (SVar x Nothing))
|
||||
|
||||
isFree :: String -> TricuAST -> Bool
|
||||
isFree x = Set.member x . freeVars
|
||||
isFree x t = Set.member x (freeVars t)
|
||||
|
||||
freeVars :: TricuAST -> Set.Set String
|
||||
-- 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)
|
||||
@@ -273,22 +301,6 @@ mainResult r = case Map.lookup "main" r of
|
||||
Just a -> a
|
||||
Nothing -> errorWithoutStackTrace "No valid definition for `main` found."
|
||||
|
||||
evalWithEnv :: Env -> Maybe Connection -> Map.Map String T.Text -> TricuAST -> IO T
|
||||
evalWithEnv env mconn selectedVersions ast = do
|
||||
let varNames = findVarNames ast
|
||||
resolvedEnv <- case mconn of
|
||||
Just conn -> foldM (\e name ->
|
||||
if Map.member name e
|
||||
then return e
|
||||
else do
|
||||
mterm <- resolveTermFromStore conn selectedVersions name Nothing
|
||||
case mterm of
|
||||
Just term -> return $ Map.insert name term e
|
||||
Nothing -> return e
|
||||
) env varNames
|
||||
Nothing -> return env
|
||||
return $ evalASTSync resolvedEnv ast
|
||||
|
||||
findVarNames :: TricuAST -> [String]
|
||||
findVarNames ast = case ast of
|
||||
SVar name _ -> [name]
|
||||
@@ -296,3 +308,285 @@ findVarNames ast = case ast of
|
||||
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 (BList xs) =
|
||||
let anyUses = any (dependsOnLevel 0) xs
|
||||
in if not anyUses
|
||||
then SApp _K (SList (map fromDBClosed xs))
|
||||
else SList (map toSKIDB xs)
|
||||
toSKIDB other
|
||||
| not (dependsOnLevel 0 other) = SApp _K (fromDBClosed other)
|
||||
toSKIDB other = _K `SApp` TLeaf
|
||||
|
||||
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)
|
||||
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"
|
||||
BFree s -> Right ([], SVar s Nothing)
|
||||
|
||||
-- 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))
|
||||
|
||||
-- Count how many leading pairs (a,b) repeat at the head of zip g1 g2
|
||||
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
|
||||
|
||||
@@ -1,11 +1,11 @@
|
||||
module Research where
|
||||
|
||||
import Data.ByteArray (convert)
|
||||
import Data.Char (chr, ord)
|
||||
import Data.ByteString.Base16 (decode, encode)
|
||||
import Data.List (intercalate)
|
||||
import Data.Map (Map)
|
||||
import Data.Text (Text, replace, unpack)
|
||||
import Data.Word (Word8)
|
||||
import Data.Text (Text, replace, pack)
|
||||
import Data.Text.Encoding (decodeUtf8, encodeUtf8)
|
||||
import System.Console.CmdArgs (Data, Typeable)
|
||||
|
||||
import qualified Data.ByteString as BS
|
||||
@@ -76,36 +76,21 @@ data Node
|
||||
-- Fork: 0x02 || left_hash (32 bytes) || right_hash (32 bytes)
|
||||
serializeNode :: Node -> BS.ByteString
|
||||
serializeNode NLeaf = BS.pack [0x00]
|
||||
serializeNode (NStem h) = BS.pack [0x01] <> hexToBytes h
|
||||
serializeNode (NFork l r) = BS.pack [0x02] <> hexToBytes l <> hexToBytes r
|
||||
serializeNode (NStem h) = BS.pack [0x01] <> go (decode (encodeUtf8 h))
|
||||
where go (Left _) = error "Research.serializeNode: invalid hex hash"
|
||||
go (Right bs) = bs
|
||||
serializeNode (NFork l r) = BS.pack [0x02] <> go (decode (encodeUtf8 l)) <> go (decode (encodeUtf8 r))
|
||||
where go (Left _) = error "Research.serializeNode: invalid hex hash"
|
||||
go (Right bs) = bs
|
||||
|
||||
-- | Hash a node per the Merkle content-addressing spec.
|
||||
-- hash = SHA256( "tricu.merkle.node.v1" <> 0x00 <> node_payload )
|
||||
nodeHash :: Node -> MerkleHash
|
||||
nodeHash node = bytesToHex (sha256WithPrefix (serializeNode node))
|
||||
nodeHash node = decodeUtf8 (encode (sha256WithPrefix (serializeNode node)))
|
||||
where sha256WithPrefix payload =
|
||||
convert . (hash :: BS.ByteString -> Digest SHA256) $ utf8Tag <> BS.pack [0x00] <> payload
|
||||
utf8Tag = BS.pack $ map fromIntegral $ BS.unpack "tricu.merkle.node.v1"
|
||||
|
||||
-- | Convert a Hex Text hash into raw ByteString (2 hex chars per byte)
|
||||
hexToBytes :: Text -> BS.ByteString
|
||||
hexToBytes h = BS.pack $ map combinePair pairs
|
||||
where
|
||||
chars = unpack h
|
||||
pairs = chunkPairs chars
|
||||
chunkPairs :: String -> [(Char, Char)]
|
||||
chunkPairs (c1:c2:rest) = (c1, c2) : chunkPairs rest
|
||||
chunkPairs [] = []
|
||||
chunkPairs _ = error "hexToBytes: odd number of hex digits"
|
||||
combinePair :: (Char, Char) -> Word8
|
||||
combinePair (c1, c2) = fromIntegral (hexDigitToInt c1 * 16 + hexDigitToInt c2)
|
||||
hexDigitToInt :: Char -> Int
|
||||
hexDigitToInt c
|
||||
| '0' <= c && c <= '9' = ord c - ord '0'
|
||||
| 'a' <= c && c <= 'f' = ord c - ord 'a' + 10
|
||||
| 'A' <= c && c <= 'F' = ord c - ord 'A' + 10
|
||||
| otherwise = error $ "Invalid hex digit: " ++ show c
|
||||
|
||||
-- | Deserialize a Node from canonical bytes.
|
||||
deserializeNode :: BS.ByteString -> Node
|
||||
deserializeNode bs =
|
||||
@@ -115,26 +100,14 @@ deserializeNode bs =
|
||||
|
||||
Just (0x01, rest)
|
||||
| BS.length rest == 32 ->
|
||||
NStem $ bytesToHex rest
|
||||
NStem $ decodeUtf8 (encode rest)
|
||||
|
||||
Just (0x02, rest)
|
||||
| BS.length rest == 64 ->
|
||||
let (l, r) = BS.splitAt 32 rest
|
||||
in NFork (bytesToHex l) (bytesToHex r)
|
||||
in NFork (decodeUtf8 (encode l)) (decodeUtf8 (encode r))
|
||||
|
||||
_ -> error "invalid merkle node payload"
|
||||
|
||||
|
||||
-- | Convert 32-byte ByteString back to hex Text
|
||||
bytesToHex :: BS.ByteString -> Text
|
||||
bytesToHex bs = T.pack $ concatMap byteToHexChars $ BS.unpack bs
|
||||
where
|
||||
byteToHexChars :: Word8 -> String
|
||||
byteToHexChars w = [hexDigit (fromIntegral w `div` 16), hexDigit (fromIntegral w `mod` 16)]
|
||||
hexDigit :: Int -> Char
|
||||
hexDigit n
|
||||
| n < 10 = chr (ord '0' + n)
|
||||
| otherwise = chr (ord 'a' + n - 10)
|
||||
_ -> errorWithoutStackTrace "invalid merkle node payload"
|
||||
|
||||
-- | Build a Merkle DAG from a Tree Calculus term.
|
||||
buildMerkle :: T -> Node
|
||||
|
||||
Reference in New Issue
Block a user