Eval.hs (22714B)
1 module Eval where 2 3 import Frontend.ContractDesugar 4 import Parser 5 import Research 6 7 import Data.List (partition, (\\), elemIndex, foldl') 8 import Data.Map () 9 import Data.Set (Set) 10 import Debug.Trace (trace) 11 12 import qualified Data.Foldable as F () 13 import qualified Data.Map as Map 14 import qualified Data.Set as Set 15 16 data DB 17 = BVar Int 18 | BFree String 19 | BLam DB 20 | BApp DB DB 21 | BLeaf 22 | BStem DB 23 | BFork DB DB 24 | BStr String 25 | BInt Integer 26 | BList [DB] 27 | BEmpty 28 deriving (Eq, Show) 29 30 type Uses = [Bool] 31 32 evalSingle :: Env -> TricuAST -> Env 33 evalSingle env term 34 | SDef name params body <- term 35 = let res = evalASTSync env (if null params then body else SLambda params body) 36 in case Map.lookup name env of 37 Just existingValue 38 | existingValue == res -> env 39 | otherwise 40 -> Map.insert "!result" res (Map.insert name res env) 41 Nothing 42 -> Map.insert "!result" res (Map.insert name res env) 43 | SDefAnn name args _ body <- term 44 = let params = annotatedBinders args 45 res = evalASTSync env (if null params then body else SLambda params body) 46 in case Map.lookup name env of 47 Just existingValue 48 | existingValue == res -> env 49 | otherwise 50 -> Map.insert "!result" res (Map.insert name res env) 51 Nothing 52 -> Map.insert "!result" res (Map.insert name res env) 53 | SApp func arg <- term 54 = let res = apply (evalASTSync env func) (evalASTSync env arg) 55 in Map.insert "!result" res env 56 | SVar name Nothing <- term 57 = case Map.lookup name env of 58 Just v -> Map.insert "!result" v env 59 Nothing -> errorWithoutStackTrace $ "Variable " ++ name ++ " not defined" 60 | SVar name (Just hash) <- term 61 = errorWithoutStackTrace $ "Hash-specific variable lookup not supported in local evaluation: " ++ name ++ "#" ++ hash 62 | otherwise 63 = let res = evalASTSync env term 64 in Map.insert "!result" res env 65 66 evalTricu :: Env -> [TricuAST] -> Env 67 evalTricu env x = go env (reorderDefs env (map recoverParams (desugarContracts x))) 68 where 69 go env' [] = env' 70 go env' [def] = 71 let updatedEnv = evalSingle env' def 72 in Map.insert "!result" (result updatedEnv) updatedEnv 73 go env' (def:xs) = 74 evalTricu (evalSingle env' def) xs 75 76 -- | Ensure the contract kernel is bound. If the environment already defines 77 -- 'kernel', leave it alone. Otherwise, bind 'kernel' to 'defaultKernel' if 78 -- that is available. This lets the default kernel live in a .tri file while 79 -- still providing a fallback for code that imports the base library. 80 injectKernel :: Env -> Env 81 injectKernel env = 82 case Map.lookup "kernel" env of 83 Just _ -> env 84 Nothing -> 85 case Map.lookup "defaultKernel" env of 86 Just k -> Map.insert "kernel" k env 87 Nothing -> env 88 89 evalASTSync :: Env -> TricuAST -> T 90 evalASTSync env term = case term of 91 SLambda _ _ -> evalASTSync env (elimLambda term) 92 SLet name val body -> evalASTSync env (SApp (SLambda [name] body) val) 93 SVar name Nothing -> case Map.lookup name env of 94 Just v -> v 95 Nothing -> errorWithoutStackTrace $ "Variable " ++ name ++ " not defined" 96 SVar name (Just hash) -> 97 case Map.lookup (name ++ "#" ++ hash) env of 98 Just v -> v 99 Nothing -> errorWithoutStackTrace $ 100 "Variable " ++ name ++ " with hash " ++ hash ++ " not found in environment" 101 TLeaf -> Leaf 102 TStem t -> Stem (evalASTSync env t) 103 TFork t u -> Fork (evalASTSync env t) (evalASTSync env u) 104 SApp t u -> apply (evalASTSync env t) (evalASTSync env u) 105 SStr s -> ofString s 106 SInt n -> ofNumber n 107 SList xs -> ofList (map (evalASTSync env) xs) 108 SEmpty -> Leaf 109 _ -> errorWithoutStackTrace $ "Unexpected AST term: " ++ show term 110 111 evalAST :: Env -> TricuAST -> IO T 112 evalAST env ast = return $ evalASTSync env ast 113 114 recoverParams :: TricuAST -> TricuAST 115 recoverParams (SDef name [] (SLambda params body)) = SDef name params body 116 recoverParams term = term 117 118 annotatedBinders :: [DefArg] -> [String] 119 annotatedBinders [] = [] 120 annotatedBinders (DefBinder name _ : rest) = name : annotatedBinders rest 121 annotatedBinders (DefPhantom _ : rest) = annotatedBinders rest 122 123 elimLambda :: TricuAST -> TricuAST 124 elimLambda = go 125 where 126 go (SLet name val body) = go (SApp (SLambda [name] body) val) 127 go term 128 | etaReduction term = go (etaReduceResult term) 129 | triagePattern term = _TRI 130 | composePattern term = _B 131 | lambdaList term = go (lambdaListResult term) 132 | nestedLambda term = nestedLambdaResult term 133 | application term = applicationResult term 134 | isSList term = slistTransform term 135 | otherwise = term 136 137 etaReduction (SLambda [v] (SVar x Nothing)) = v == x 138 etaReduction (SLambda [v] (SApp f (SVar x Nothing))) = v == x && not (usesBinder v f) 139 etaReduction _ = False 140 141 triagePattern (SLambda [a] (SLambda [b] (SLambda [c] body))) = 142 toDB [c,b,a] body == triageBodyDB 143 triagePattern _ = False 144 145 composePattern (SLambda [f] (SLambda [g] (SLambda [x] body))) = 146 toDB [x,g,f] body == composeBodyDB 147 composePattern _ = False 148 149 lambdaList (SLambda [_] (SList _)) = True 150 lambdaList _ = False 151 152 nestedLambda (SLambda (_:_) _) = True 153 nestedLambda _ = False 154 155 application (SApp _ _) = True 156 application _ = False 157 158 etaReduceResult (SLambda [_] (SVar _ Nothing)) = _I 159 etaReduceResult (SLambda [_] (SApp f _)) = f 160 etaReduceResult _ = error "etaReduceResult: unexpected shape" 161 162 lambdaListResult (SLambda [v] (SList xs)) = 163 SLambda [v] (foldr wrapTLeaf TLeaf xs) 164 where 165 wrapTLeaf m r = SApp (SApp TLeaf m) r 166 lambdaListResult _ = error "lambdaListResult: expected SLambda [v] (SList xs)" 167 168 nestedLambdaResult (SLambda (v:vs) body) 169 | null vs = 170 let body' = go body 171 db = toDB [v] body' 172 in toSKIKiselyov db 173 | otherwise = go (SLambda [v] (SLambda vs body)) 174 nestedLambdaResult _ = error "nestedLambdaResult: expected SLambda (_:_) _" 175 176 applicationResult (SApp f g) = SApp (go f) (go g) 177 applicationResult _ = error "applicationResult: expected SApp _ _" 178 179 isSList (SList _) = True 180 isSList _ = False 181 182 slistTransform :: TricuAST -> TricuAST 183 slistTransform (SList xs) = foldr (\m r -> SApp (SApp TLeaf (go m)) r) TLeaf xs 184 slistTransform ast = ast -- Should not be reached 185 186 _S, _K, _I, _R, _C, _B, _T, _TRI :: TricuAST 187 _S = parseSingle "t (t (t t t)) t" 188 _K = parseSingle "t t" 189 _I = parseSingle "t (t (t t)) t" 190 _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))" 191 _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)))" 192 _B = parseSingle "t (t (t t (t (t (t t t)) t))) (t t)" 193 _T = SApp _C _I 194 _TRI = parseSingle "t (t (t t (t (t (t t t))))) t" 195 196 triageBody :: String -> String -> String -> TricuAST 197 triageBody a b c = SApp (SApp TLeaf (SApp (SApp TLeaf (SVar a Nothing)) (SVar b Nothing))) (SVar c Nothing) 198 composeBody :: String -> String -> String -> TricuAST 199 composeBody f g x = SApp (SVar f Nothing) (SApp (SVar g Nothing) (SVar x Nothing)) 200 201 isFree :: String -> TricuAST -> Bool 202 isFree x t = Set.member x (freeVars t) 203 204 freeVars :: TricuAST -> Set String 205 freeVars (SVar v Nothing) = Set.singleton v 206 freeVars (SVar v (Just _)) = Set.singleton v 207 freeVars (SApp t u) = Set.union (freeVars t) (freeVars u) 208 freeVars (SLambda vs body) = Set.difference (freeVars body) (Set.fromList vs) 209 freeVars (SLet name val body) = 210 Set.union (freeVars val) (Set.delete name (freeVars body)) 211 freeVars (SDef _ params body) = Set.difference (freeVars body) (Set.fromList params) 212 freeVars (SDefAnn _ args ret body) = 213 Set.difference 214 (Set.unions 215 [ freeVars body 216 , freeVarsDefArgs args 217 , maybe Set.empty freeVarsViewExpr ret 218 , Set.singleton "withContract" 219 ]) 220 (Set.fromList (annotatedBinders args)) 221 freeVars (TStem t) = freeVars t 222 freeVars (TFork t u) = Set.union (freeVars t) (freeVars u) 223 freeVars (SList xs) = foldMap freeVars xs 224 freeVars _ = Set.empty 225 226 freeVarsViewExpr :: ViewExpr -> Set String 227 freeVarsViewExpr (VEName s) = Set.singleton s 228 freeVarsViewExpr (VEVar s) = Set.singleton s 229 freeVarsViewExpr (VEApp f a) = Set.union (freeVarsViewExpr f) (freeVarsViewExpr a) 230 freeVarsViewExpr (VEList es) = Set.unions (map freeVarsViewExpr es) 231 freeVarsViewExpr (VEForall _ e) = freeVarsViewExpr e 232 freeVarsViewExpr (VEExists _ e) = freeVarsViewExpr e 233 freeVarsViewExpr _ = Set.empty 234 235 freeVarsDefArgs :: [DefArg] -> Set String 236 freeVarsDefArgs = Set.unions . map go 237 where 238 go (DefBinder _ mAnn) = maybe Set.empty freeVarsViewExpr mAnn 239 go (DefPhantom ann) = freeVarsViewExpr ann 240 241 reorderDefs :: Env -> [TricuAST] -> [TricuAST] 242 reorderDefs env defs 243 | not (null missingDeps) = 244 errorWithoutStackTrace $ 245 "Missing dependencies detected: " ++ show missingDeps 246 | otherwise = orderedDefs ++ others 247 where 248 (defsOnly, others) = partition isDef defs 249 defNames = [ defName def | def <- defsOnly ] 250 251 defsWithFreeVars = [(def, freeVars def) | def <- defsOnly] 252 253 graph = buildDepGraph defsOnly 254 sortedDefs = sortDeps graph 255 defMap = Map.fromList [(defName def, def) | def <- defsOnly] 256 orderedDefs = map (defMap Map.!) sortedDefs 257 258 freeVarsDefs = foldMap snd defsWithFreeVars 259 freeVarsOthers = foldMap freeVars others 260 allFreeVars = freeVarsDefs <> freeVarsOthers 261 validNames = Set.fromList defNames `Set.union` Set.fromList (Map.keys env) 262 missingDeps = Set.toList (allFreeVars `Set.difference` validNames) 263 264 isDef SDef {} = True 265 isDef SDefAnn {} = True 266 isDef _ = False 267 268 buildDepGraph :: [TricuAST] -> Map.Map String (Set.Set String) 269 buildDepGraph topDefs 270 | not (null conflictingDefs) = 271 errorWithoutStackTrace $ 272 "Conflicting definitions detected: " ++ show conflictingDefs 273 | otherwise = 274 Map.fromList 275 [ (defName def, depends topDefs def) 276 | def <- topDefs] 277 where 278 defsMap = Map.fromListWith (++) 279 [(defName def, [(defName def, defBody def)]) | def <- topDefs] 280 281 conflictingDefs = 282 [ name 283 | (name, defs) <- Map.toList defsMap 284 , let bodies = map snd defs 285 , not $ all (== head bodies) (tail bodies) 286 ] 287 288 sortDeps :: Map.Map String (Set.Set String) -> [String] 289 sortDeps graph = go [] Set.empty (Map.keys graph) 290 where 291 go sorted _sortedSet [] = sorted 292 go sorted sortedSet remaining = 293 let ready = [ name | name <- remaining 294 , let deps = Map.findWithDefault Set.empty name graph 295 , Set.isSubsetOf deps sortedSet ] 296 notReady = remaining \\ ready 297 in if null ready 298 then errorWithoutStackTrace 299 "ERROR: Cyclic dependency detected and prohibited.\n\ 300 \RESOLVE: Use nested lambdas." 301 else go (sorted ++ ready) 302 (Set.union sortedSet (Set.fromList ready)) 303 notReady 304 305 defName :: TricuAST -> String 306 defName (SDef name _ _) = name 307 defName (SDefAnn name _ _ _) = name 308 defName _ = error "defName: expected definition" 309 310 defBody :: TricuAST -> TricuAST 311 defBody (SDef _ _ body) = body 312 defBody (SDefAnn _ _ _ body) = body 313 defBody _ = error "defBody: expected definition" 314 315 depends :: [TricuAST] -> TricuAST -> Set.Set String 316 depends topDefs def@SDef {} = 317 Set.intersection 318 (Set.fromList [defName d | d <- topDefs]) 319 (freeVars def) 320 depends topDefs def@SDefAnn {} = 321 Set.intersection 322 (Set.fromList [defName d | d <- topDefs]) 323 (freeVars def) 324 depends _ _ = Set.empty 325 326 result :: Env -> T 327 result r = case Map.lookup "!result" r of 328 Just a -> a 329 Nothing -> errorWithoutStackTrace "No !result field found in provided env" 330 331 mainResult :: Env -> T 332 mainResult r = case Map.lookup "main" r of 333 Just a -> a 334 Nothing -> errorWithoutStackTrace "No valid definition for `main` found." 335 336 findVarNames :: TricuAST -> [String] 337 findVarNames ast = case ast of 338 SVar name _ -> [name] 339 SApp a b -> findVarNames a ++ findVarNames b 340 SLambda args body -> findVarNames body \\ args 341 SLet name val body -> findVarNames val ++ (findVarNames body \\ [name]) 342 SDef name args body -> name : (findVarNames body \\ args) 343 SDefAnn name args _ body -> name : (findVarNames body \\ annotatedBinders args) 344 _ -> [] 345 346 -- Convert named TricuAST to De Bruijn form 347 toDB :: [String] -> TricuAST -> DB 348 toDB env = \case 349 SVar v _ -> maybe (BFree v) BVar (elemIndex v env) 350 SLambda vs b -> 351 let env' = reverse vs ++ env 352 body = toDB env' b 353 in foldr (\_ acc -> BLam acc) body vs 354 SApp f a -> BApp (toDB env f) (toDB env a) 355 TLeaf -> BLeaf 356 TStem t -> BStem (toDB env t) 357 TFork l r -> BFork (toDB env l) (toDB env r) 358 SStr s -> BStr s 359 SInt n -> BInt n 360 SList xs -> BList (map (toDB env) xs) 361 SEmpty -> BEmpty 362 SLet name val body -> toDB env (SApp (SLambda [name] body) val) 363 SDef{} -> error "toDB: unexpected SDef at this stage" 364 SDefAnn{} -> error "toDB: unexpected SDefAnn at this stage" 365 SImport _ _ -> BEmpty 366 367 -- Does a term depend on the current binder (level 0)? 368 dependsOnLevel :: Int -> DB -> Bool 369 dependsOnLevel lvl = \case 370 BVar k -> k == lvl 371 BLam t -> dependsOnLevel (lvl + 1) t 372 BApp f a -> dependsOnLevel lvl f || dependsOnLevel lvl a 373 BStem t -> dependsOnLevel lvl t 374 BFork l r -> dependsOnLevel lvl l || dependsOnLevel lvl r 375 BList xs -> any (dependsOnLevel lvl) xs 376 _ -> False 377 378 -- Collect free *global* names (i.e., unbound) 379 freeDBNames :: DB -> Set String 380 freeDBNames = \case 381 BFree s -> Set.singleton s 382 BVar _ -> mempty 383 BLam t -> freeDBNames t 384 BApp f a -> freeDBNames f <> freeDBNames a 385 BLeaf -> mempty 386 BStem t -> freeDBNames t 387 BFork l r -> freeDBNames l <> freeDBNames r 388 BStr _ -> mempty 389 BInt _ -> mempty 390 BList xs -> foldMap freeDBNames xs 391 BEmpty -> mempty 392 393 -- Helper: "is the binder named v used in body?" 394 usesBinder :: String -> TricuAST -> Bool 395 usesBinder v body = dependsOnLevel 0 (toDB [v] body) 396 397 -- Expected DB bodies for the named special patterns (under env [a,b,c] -> indices 2,1,0) 398 triageBodyDB :: DB 399 triageBodyDB = 400 BApp (BApp BLeaf (BApp (BApp BLeaf (BVar 2)) (BVar 1))) (BVar 0) 401 402 composeBodyDB :: DB 403 composeBodyDB = 404 BApp (BVar 2) (BApp (BVar 1) (BVar 0)) 405 406 -- Convert DB -> TricuAST for subterms that contain NO binders (no BLam, no BVar) 407 fromDBClosed :: DB -> TricuAST 408 fromDBClosed = \case 409 BFree s -> SVar s Nothing 410 BApp f a -> SApp (fromDBClosed f) (fromDBClosed a) 411 BLeaf -> TLeaf 412 BStem t -> TStem (fromDBClosed t) 413 BFork l r -> TFork (fromDBClosed l) (fromDBClosed r) 414 BStr s -> SStr s 415 BInt n -> SInt n 416 BList xs -> SList (map fromDBClosed xs) 417 BEmpty -> SEmpty 418 -- Anything bound would be a logic error if we call this correctly. 419 BLam _ -> error "fromDBClosed: unexpected BLam" 420 BVar _ -> error "fromDBClosed: unexpected bound variable" 421 422 -- DB-native bracket abstraction over the innermost binder (level 0). 423 -- This mirrors your old toSKI, but is purely index-driven. 424 toSKIDB :: DB -> TricuAST 425 toSKIDB t 426 | not (dependsOnLevel 0 t) = SApp _K (fromDBClosed t) 427 toSKIDB (BVar 0) = _I 428 toSKIDB (BApp n u) = SApp (SApp _S (toSKIDB n)) (toSKIDB u) 429 toSKIDB (BStem t) = toSKIDB (BApp BLeaf t) 430 toSKIDB (BFork l r) = toSKIDB (BApp (BApp BLeaf l) r) 431 toSKIDB (BList xs) = toSKIDB (foldr (\m r -> BApp (BApp BLeaf m) r) BLeaf xs) 432 toSKIDB other = error $ "toSKIDB: unsupported DB term: " ++ show other 433 434 app2 :: TricuAST -> TricuAST -> TricuAST 435 app2 f x = SApp f x 436 437 app3 :: TricuAST -> TricuAST -> TricuAST -> TricuAST 438 app3 f x y = SApp (SApp f x) y 439 440 -- Core converter that *does not* perform the λ-step; it just returns (Γ, d). 441 -- Supported shapes: variables, applications, closed literals (Leaf/Int/Str/Empty), 442 -- closed lists. For anything where the binder occurs under structural nodes 443 -- (Stem/Fork/List-with-use), we deliberately bail so the caller can fall back. 444 kisConv :: DB -> Either String (Uses, TricuAST) 445 kisConv = \case 446 BVar 0 -> Right ([True], _I) 447 BVar n | n > 0 -> do 448 (g,d) <- kisConv (BVar (n - 1)) 449 Right (False:g, d) 450 BVar n -> Right ([], SVar ("BVar" ++ show n) Nothing) 451 BFree s -> Right ([], SVar s Nothing) 452 BApp e1 e2 -> do 453 (g1,d1) <- kisConv e1 454 (g2,d2) <- kisConv e2 455 let g = zipWithDefault False (||) g1 g2 -- <- propagate Γ outside (#) 456 d = kisHash (g1,d1) (g2,d2) -- <- (#) yields only the term 457 Right (g, d) 458 -- Treat closed constants as free 'combinator leaves' (no binder use). 459 BLeaf -> Right ([], TLeaf) 460 BStr s -> Right ([], SStr s) 461 BInt n -> Right ([], SInt n) 462 BEmpty -> Right ([], SEmpty) 463 -- Closed list: allowed. If binder is used anywhere, we punt to fallback. 464 BList xs 465 | any (dependsOnLevel 0) xs -> Left "List with binder use: fallback" 466 | otherwise -> Right ([], SList (map fromDBClosed xs)) 467 -- For structural nodes, only allow if *closed* wrt the binder. 468 BStem t 469 | dependsOnLevel 0 t -> Left "Stem with binder use: fallback" 470 | otherwise -> Right ([], TStem (fromDBClosed t)) 471 BFork l r 472 | dependsOnLevel 0 l || dependsOnLevel 0 r -> Left "Fork with binder use: fallback" 473 | otherwise -> Right ([], TFork (fromDBClosed l) (fromDBClosed r)) 474 -- We shouldn't see BLam under elim; treat as unsupported so we fallback. 475 BLam _ -> Left "Nested lambda under body: fallback" 476 477 -- Application combiner with K-optimization (lazy weakening). 478 -- Mirrors Lynn's 'optK' rules: choose among S, B, C, R based on leading flags. 479 -- η-aware (#) with K-optimization (adapted from TS kiselyov_eta) 480 kisHash :: (Uses, TricuAST) -> (Uses, TricuAST) -> TricuAST 481 kisHash (g1, d1) (g2, d2) = 482 case g1 of 483 [] -> case g2 of 484 [] -> SApp d1 d2 485 True:gs2 -> if isId2 (g2, d2) 486 then d1 487 else kisHash ([], SApp _B d1) (gs2, d2) 488 False:gs2 -> kisHash ([], d1) (gs2, d2) 489 490 True:gs1 -> case g2 of 491 [] -> if isId2 (g1, d1) 492 then SApp _T d2 493 else kisHash ([], SApp _R d2) (gs1, d1) 494 _ -> 495 if isId2 (g1, d1) && case g2 of { False:_ -> True; _ -> False } 496 then kisHash ([], _T) (drop1 g2, d2) 497 else 498 -- NEW: coalesce the longest run of identical head pairs and apply bulk op once 499 let ((h1, h2), count) = headPairRun g1 g2 500 g1' = drop count g1 501 g2' = drop count g2 502 in case (h1, h2) of 503 (False, False) -> 504 kisHash (g1', d1) (g2', d2) 505 (False, True) -> 506 let d1' = kisHash ([], bulkB count) (g1', d1) 507 in kisHash (g1', d1') (g2', d2) 508 (True, False) -> 509 let d1' = kisHash ([], bulkC count) (g1', d1) 510 in kisHash (g1', d1') (g2', d2) 511 (True, True) -> 512 let d1' = kisHash ([], bulkS count) (g1', d1) 513 in kisHash (g1', d1') (g2', d2) 514 515 False:gs1 -> case g2 of 516 [] -> kisHash (gs1, d1) ([], d2) 517 _ -> 518 if isId2 (g1, d1) && case g2 of { False:_ -> True; _ -> False } 519 then kisHash ([], _T) (drop1 g2, d2) 520 else case g2 of 521 True:gs2 -> 522 let d1' = kisHash ([], _B) (gs1, d1) 523 in kisHash (gs1, d1') (gs2, d2) 524 False:gs2 -> 525 kisHash (gs1, d1) (gs2, d2) 526 where 527 drop1 (_:xs) = xs 528 drop1 [] = [] 529 530 531 toSKIKiselyov :: DB -> TricuAST 532 toSKIKiselyov body = 533 case kisConv body of 534 Right ([], d) -> SApp _K d 535 Right (True:_ , d) -> d 536 Right (False:g, d) -> kisHash ([], _K) (g, d) -- no snd 537 Left _ -> starSKIBCOpEtaDB body -- was: toSKIDB body 538 539 zipWithDefault :: a -> (a -> a -> a) -> [a] -> [a] -> [a] 540 zipWithDefault d f [] ys = map (f d) ys 541 zipWithDefault d f xs [] = map (\x -> f x d) xs 542 zipWithDefault d f (x:xs) (y:ys) = f x y : zipWithDefault d f xs ys 543 544 isNode :: TricuAST -> Bool 545 isNode t = case t of 546 TLeaf -> True 547 _ -> False 548 549 isApp2 :: TricuAST -> Maybe (TricuAST, TricuAST) 550 isApp2 (SApp a b) = Just (a, b) 551 isApp2 _ = Nothing 552 553 isKop :: TricuAST -> Bool 554 isKop t = case isApp2 t of 555 Just (a,b) -> isNode a && isNode b 556 _ -> False 557 558 -- detects the two canonical I-shapes in the tree calculus: 559 -- △ (△ (△ △)) x OR △ (△ △ △) △ 560 isId :: TricuAST -> Bool 561 isId t = case isApp2 t of 562 Just (ab, c) -> case isApp2 ab of 563 Just (a, b) | isNode a -> 564 case isApp2 b of 565 Just (b1, b2) -> 566 (isNode b1 && isKop b2) || 567 (isKop b1 && isNode b2 && isNode c) 568 _ -> False 569 _ -> False 570 _ -> False 571 572 -- head-True only, tail empty, and term is identity 573 isId2 :: (Uses, TricuAST) -> Bool 574 isId2 (True:[], t) = isId t 575 isId2 _ = False 576 577 -- Bulk helpers built from SKI (no new primitives) 578 bPrime :: TricuAST 579 bPrime = SApp _B _B -- B' = B B 580 581 cPrime :: TricuAST 582 cPrime = SApp (SApp _B (SApp _B _C)) _B -- C' = B (B C) B 583 584 sPrime :: TricuAST 585 sPrime = SApp (SApp _B (SApp _B _S)) _B -- S' = B (B S) B 586 587 bulkB :: Int -> TricuAST 588 bulkB n | n <= 1 = _B 589 | otherwise = SApp bPrime (bulkB (n - 1)) 590 591 bulkC :: Int -> TricuAST 592 bulkC n | n <= 1 = _C 593 | otherwise = SApp cPrime (bulkC (n - 1)) 594 595 bulkS :: Int -> TricuAST 596 bulkS n | n <= 1 = _S 597 | otherwise = SApp sPrime (bulkS (n - 1)) 598 599 headPairRun :: [Bool] -> [Bool] -> ((Bool, Bool), Int) 600 headPairRun g1 g2 = 601 case zip g1 g2 of 602 [] -> ((False, False), 0) 603 (h:rest) -> (h, 1 + length (takeWhile (== h) rest)) 604 605 -- DB-native star_skibc_op_eta (adapted from strategies.mts), binder = level 0 606 starSKIBCOpEtaDB :: DB -> TricuAST 607 starSKIBCOpEtaDB t 608 | not (dependsOnLevel 0 t) = SApp _K (fromDBClosed t) 609 starSKIBCOpEtaDB (BVar 0) = _I 610 starSKIBCOpEtaDB (BApp e1 e2) 611 -- if binder not in right: use C 612 | not (dependsOnLevel 0 e2) 613 = SApp (SApp _C (starSKIBCOpEtaDB e1)) (fromDBClosed e2) 614 -- if binder not in left: 615 | not (dependsOnLevel 0 e1) 616 = case e2 of 617 -- η case: \x. f x ==> f 618 BVar 0 -> fromDBClosed e1 619 _ -> SApp (SApp _B (fromDBClosed e1)) (starSKIBCOpEtaDB e2) 620 -- otherwise: S 621 | otherwise 622 = SApp (SApp _S (starSKIBCOpEtaDB e1)) (starSKIBCOpEtaDB e2) 623 -- Structural nodes with binder underneath: fall back to plain SKI (rare) 624 starSKIBCOpEtaDB other = toSKIDB other