commit a2d0fd09a94bd98750de24bab00135112e4928cb
parent 267d8a85c82327ea75ccb3efc9cd5b8bdfcac5ae
Author: James Eversole <james@eversole.co>
Date: Tue, 5 May 2026 14:51:42 -0500
Picking development back up
Diffstat:
7 files changed, 413 insertions(+), 124 deletions(-)
diff --git a/README.md b/README.md
@@ -10,6 +10,10 @@ tricu is the word for "tree" in Lojban: `(x1) is a tree of species/cultivar (x2)
Tree Calculus was discovered by [Barry Jay](https://github.com/barry-jay-personal/blog). The addition of Triage rules were suggested by [Johannes Bader](https://johannes-bader.com/). Johannes is also the creator of [treecalcul.us](https://treecalcul.us) which has a great intuitive code playground using his language LambAda.
+## Versioning
+
+This really is a repo for experimentation so I'm not doing anything sane with the versioning for now. If I decide to stabilize the project we'll start anew at 2.0.
+
## REPL examples
```
diff --git a/flake.nix b/flake.nix
@@ -9,26 +9,42 @@
outputs = { self, nixpkgs, flake-utils }:
flake-utils.lib.eachDefaultSystem (system:
let
- pkgs = nixpkgs.legacyPackages.${system};
- packageName = "tricu";
- containerPackageName = "${packageName}-container";
-
- customGHC = pkgs.haskellPackages.ghcWithPackages (hpkgs: with hpkgs; [
- megaparsec
- ]);
+ pkgs = nixpkgs.legacyPackages.${system};
+ packageName = "tricu";
haskellPackages = pkgs.haskellPackages;
+ hsLib = pkgs.haskell.lib;
+
+ tricuPackage =
+ haskellPackages.callCabal2nix packageName self {};
+
+ tricuTests =
+ hsLib.overrideCabal tricuPackage (old: {
+ doCheck = true;
+
+ configureFlags = (old.configureFlags or []) ++ [
+ "--enable-tests"
+ ];
- enableSharedExecutables = false;
- enableSharedLibraries = false;
+ checkPhase = ''
+ runHook preCheck
+ ./Setup test tricu-tests --show-details=direct
+ runHook postCheck
+ '';
+ });
- tricu = pkgs.haskell.lib.justStaticExecutables self.packages.${system}.default;
+ customGHC = haskellPackages.ghcWithPackages (hpkgs: with hpkgs; [
+ megaparsec
+ ]);
in {
+ packages.${packageName} = tricuPackage;
+ packages.default = tricuPackage;
+
+ packages.test = tricuTests;
- packages.${packageName} =
- haskellPackages.callCabal2nix packageName self rec {};
+ checks.${packageName} = tricuTests;
+ checks.default = tricuTests;
- packages.default = self.packages.${system}.${packageName};
defaultPackage = self.packages.${system}.default;
devShells.default = pkgs.mkShell {
@@ -39,9 +55,10 @@
customGHC
upx
];
- inputsFrom = builtins.attrValues self.packages.${system};
- };
- devShell = self.devShells.${system}.default;
+ inputsFrom = [
+ tricuPackage
+ ];
+ };
});
}
diff --git a/src/ContentStore.hs b/src/ContentStore.hs
@@ -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
diff --git a/src/Eval.hs b/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
diff --git a/src/Research.hs b/src/Research.hs
@@ -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)
-
- _ -> error "invalid merkle node payload"
+ in NFork (decodeUtf8 (encode l)) (decodeUtf8 (encode r))
-
--- | 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
diff --git a/test/Spec.hs b/test/Spec.hs
@@ -32,10 +32,10 @@ tests = testGroup "Tricu Tests"
, providedLibraries
, fileEval
, modules
--- , demos
+ , demos
, decoding
- , elimLambdaSingle
- , stressElimLambda
+ , elimLambdaSingle
+ , stressElimLambda
]
lexer :: TestTree
diff --git a/tricu.cabal b/tricu.cabal
@@ -1,8 +1,8 @@
cabal-version: 1.12
name: tricu
-version: 1.0.0
-description: A micro-language for exploring Tree Calculus
+version: 1.1.0
+description: A language for exploring Tree Calculus
author: James Eversole
maintainer: james@eversole.co
copyright: James Eversole
@@ -27,6 +27,7 @@ executable tricu
base >=4.7
, aeson
, ansi-terminal
+ , base16-bytestring
, base64-bytestring
, bytestring
, cereal
@@ -71,6 +72,7 @@ test-suite tricu-tests
base >=4.7
, aeson
, ansi-terminal
+ , base16-bytestring
, base64-bytestring
, bytestring
, cereal
